Skip to content

Add DSL design digest: shareable overview of compilation stages and test generation - #45

Closed
briansrls wants to merge 3 commits into
mainfrom
claude/dsl-design-digest-Dmqes
Closed

briansrls wants to merge 3 commits into
mainfrom
claude/dsl-design-digest-Dmqes

Conversation

@briansrls

Copy link
Copy Markdown
Contributor

Distills the 4,000+ line dsl-design.md into a concise walkthrough covering:

  • The 9-stage compilation pipeline and what each stage proves/generates
  • Two end-to-end examples (makegen and GCP credential chain)
  • The 4-bucket test obligation model (Execution, Contract, Coverage, Hygiene)
  • How types-as-DAGs power automatic boundary value generation
  • The C1-C11 compiler-enforced policies and their free checks

https://claude.ai/code/session_01Yaa838K73c7K9aD521tEaU

…est generation

Distills the 4,000+ line dsl-design.md into a concise walkthrough covering:
- The 9-stage compilation pipeline and what each stage proves/generates
- Two end-to-end examples (makegen and GCP credential chain)
- The 4-bucket test obligation model (Execution, Contract, Coverage, Hygiene)
- How types-as-DAGs power automatic boundary value generation
- The C1-C11 compiler-enforced policies and their free checks

https://claude.ai/code/session_01Yaa838K73c7K9aD521tEaU
Adds sections on the original Go DAG motivations, the Guarantee
Hierarchy (push everything to compile time), the arc from Go → Rust →
V3 fractal DAG → DSL, comparisons to existing systems (Rust borrow
checker, protobuf, Terraform, Bazel, Haskell), the "proof once"
principle, and the node contract. Restructured from 10 to 14 sections.

https://claude.ai/code/session_01Yaa838K73c7K9aD521tEaU
Rewrites sections 9+ of the design digest:

- Three-column comparison (hand-rolled Go / .dag / emitted Go) for the
  GCP Secret Manager credential chain, showing structural similarity
  and where they diverge
- Section on what the Graph IR encodes that Go can't: cardinality as
  proof, guard narrowing (predicate entailment), resource conflict
  detection, transport boundary classification
- Section on common behaviors at the DSL level vs opaque Go helpers
  (content_upsert pattern vs UpsertFile function, credential_chain
  pattern, retry as language construct), with comparison tables
- Appendix A with ~300 lines of hypothetical generated Go test code
  across all four buckets, with inline comments showing which graph
  property derived each test

Removes salesy line-count compression tables.

https://claude.ai/code/session_01Yaa838K73c7K9aD521tEaU
@briansrls briansrls closed this Feb 18, 2026
briansrls added a commit that referenced this pull request May 10, 2026
- Document module_lets_pairwise_rhs_independent false for len<2 vs dependency.
- Reuse expand_behavior_backward_ports in bind_rhs_subgraph_contains_branch_or_loop.
- Match on claim index so gate #43 vs #44/#45 is obvious (addresses review misread).

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
Resolve test_runner.rs: keep R3 gate #47 sequential witness alongside main's
gate #45 branch-arms serialize witness constants and dispatch.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
… lens witnesses)

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
…ch fixture

Composer exploratory note: auto_parallelism_pending_lens / _expected were orphaned after gate #45 moved to the branch-arms emit witness.

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
* feat(v3): R3 gate #44 dependent binds schedule sequential witness

Wire LensOutputEquals name bridge auto_parallelism_bind_cluster_schedule_tag:
ordered top-level program binds use the same selector as Rust program-mode emit;
if a later bind transitively depends on an earlier bind value port, the tag is 0
(sequential required), else 1.

Expose program_mode_top_level_value_binds_for_lens_runner for shared ordering.

Update auto_parallelism_dependent_binds_emit_sequential claim with real dependent
program and expected 0; integration test expects Pass for gate #44 only.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 gate #44: auto parallelism dependent binds emit sequential

* fix(v3): gate #44 dispatch without lens-name bridge (ratchet)

canonical_lens_bridge_ratchet_test forbids lens_decl.name == Some("…") arms.

Replace name-keyed branch with BindClusterScheduleProgramInput input role (fixture-local
empty type) plus unary Dag->Int lens signature check. Optional role: fixtures without
the type skip the branch so ProgramOutputBind/cost tests keep strict role errors.

Restores v3 CI canonical_lens_name_dispatch_arms_pinned.

Co-authored-by: Cursor <cursoragent@cursor.com>

* chore: apply cargo fmt (test_runner)

Co-authored-by: Cursor <cursoragent@cursor.com>

* test(v3): key R3 batch gate #44 assertion off claim name

Avoid coupling Pass vs pending-lens Fail expectations to suite index order
(TESTING.md cost-of-change); branch on claim names after claim_name check.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 gate #44: auto parallelism dependent binds emit sequential

* chore: sync Cargo.lock for v3-compiler dev-dependencies

Co-authored-by: Cursor <cursoragent@cursor.com>

* fix(v3): refresh parse corpus manifest for verification.dag growth

BindClusterScheduleProgramInput added one parsed item to std.verification;
handwritten_parse_snapshot_matches_manifest pins corpus hashes.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 gate #44: auto parallelism dependent binds emit sequential

* fix(v3): regen bootstrap and parse manifest for gate #44 emit witness

Drop unused lens_has_unary_dag_to_int_signature after BindClusterScheduleProgramInput removal.

Co-authored-by: Cursor <cursoragent@cursor.com>

* chore: apply cargo fmt (test_runner)

Co-authored-by: Cursor <cursoragent@cursor.com>

* chore(v3): remove unused pending parallelism placeholders from R3 batch fixture

Composer exploratory note: auto_parallelism_pending_lens / _expected were orphaned after gate #45 moved to the branch-arms emit witness.

Co-authored-by: Cursor <cursoragent@cursor.com>

* WIP: R3 gate #44: auto parallelism dependent binds emit sequential

---------

Co-authored-by: Cursor <cursoragent@cursor.com>
briansrls added a commit that referenced this pull request May 10, 2026
…2648)

* docs(r3): §1.8 ledger-receipt sync — 2026-05-10 batch (V Mgr lane)

Flip §1.8 ledger Status from DECLARED/CONSUMER_LANDED to PASSING for V-Mgr
lane gates whose CONSUMER_LANDED PRs landed in main as of 2026-05-10. Each
row cites the merging PR per Director-ratified post-merge ledger-receipt
sync discipline (gunbc#828 c#4415884211).

Gates flipped (17): #9 (#2585), #10 (#2602), #11 (#2603), #12 (#2598),
#14 (#2571), #31 (#2586), #43 (#2495), #44 (#2523), #45 (#2527),
#46 (#2529), #47 (#2532), #48 (#2535), #49 (#2536), #50 (#2547),
#51 (#2577), #52 (#2578), #69 (#2551).

Skipped per discipline: #15 (PR #2604 not landed); #35 already PASSING.

Doc-only; no code or test changes. Closes #2640.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* docs(r3): preserve corpus-quantified + canvas-deferral qualifiers on rows #9/#10/#11

Reviewer (claude-opus-4-7 on PR #2648) flagged that the prior status text
on rows #9, #10, #11 carried Director/PM-ratified semantic qualifiers that
must not be silently elided when citing a new slice receipt:

- #9 `l4_emit_eval_match`: §1.7 corpus-quantified rule — slice receipts ≠
  ledger closure; PASSING requires every certification-corpus program.
  Reverted to CONSUMER_LANDED; PR #2585 cited as additional slice evidence.
- #10 `l7_algebraic_laws_witnessed`: PASSING requires exhaustive per-(algebra,
  inhabitant, law) §Acceptance coverage; distributivity / lattice absorption /
  non-AlgebraicLawKind laws remain substrate §P1. Reverted to CONSUMER_LANDED;
  PR #2602 cited as incremental advancement.
- #11 `tc1_eta_equivalence_executable`: Director (a)-disposition 2026-05-09
  held this canvas-deferred past R3 absent #1972 substrate canvas-tier work.
  Reverted to DECLARED-through-R3; PR #2603 cited as scaffold advancement
  but not retiring the canvas-deferral (which would require fresh Director
  ratification).

Other 14 rows in the batch (#12, #14, #31, #43-52, #69) did not carry such
qualifiers and stay flipped to PASSING.

Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>

* Merge origin/main into ledger-receipt sync (preserve row #13 update from main)

---------

Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
@briansrls
briansrls deleted the claude/dsl-design-digest-Dmqes branch June 1, 2026 18:41
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

2 participants