Skip to content

substrate_gap_parser_grammar_closed - #2818

Merged
briansrls merged 24 commits into
mainfrom
session/tidy-bee-578
May 13, 2026
Merged

briansrls merged 24 commits into
mainfrom
session/tidy-bee-578

Conversation

@briansrls

@briansrls briansrls commented May 13, 2026 •

Copy link
Copy Markdown
Contributor

SG-0 hand-path delta: +1

SG-0 pairing: (c) dispatch remainder for substrate_gap_parser_grammar_closed / gate #60 row tracked gunbc#2818

Summary

This PR lands the Phase 2.1 parser and lowering slice for ROADMAP gate #60 (substrate_gap_parser_grammar_closed): user-facing Int<N> / UInt<N> / Real<N> / Nat<N> in angle brackets parse as TypeAngleArg (width literals are not peers of full SurfaceType, so let x: 64 = … stays unrepresentable), lower to Compose<Algebra, MachineWidth<N>> with a literal phantom width where N is in the allowed machine-width set, and register the new hermetic integration test in the SG-0 hand-authored census. Parser control flow remains authored in parse_parser_body.txt and emitted via regen_parse; parse_surface.dag is the surface-schema authority; regen_runtime_mirrors.py and regen_bootstrap snapshots were refreshed so substrate and embedded Dag::new() stay aligned.

Per-PR dissolution gate (required for new/expanded hand-Rust under v3/)

  • Exactly one disposition: SG-0 census ratchet — one new path in EXPECTED_HAND_AUTHORED_TEST (src/v3/compiler/tests/integration/sg0_census_test.rs) for r3_gate_60_phase2_width_nat_parser_test.rs, with machine-authored scripts/ci-merge/sg0-pr-body-append.2818.txt so CI reads the required SG-0 hand-path delta / pairing lines.

SG-0 net-shrink discipline

The two column-0 lines appear at the top of this description (also mirrored in scripts/ci-merge/sg0-pr-body-append.2818.txt for the workflow prepend).

Per-PR debt-paydown receipt

Test plan

  • cargo test -p v3-compiler gate_60
  • cargo test -p v3-compiler sg0_census
  • cargo clippy -p v3-compiler --all-targets -- -D warnings
  • cargo fmt --all --check
  • cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap -- --verify

@briansrls
briansrls marked this pull request as ready for review May 13, 2026 01:55
@briansrls

Copy link
Copy Markdown
Contributor Author

Codex review (10645 / REQUEST_CHANGES) — bare IntLit as type

Verified: The finding was valid on the prior shape: parse_atom_type accepted any leading IntLit as SurfaceType::WidthNatLiteral, which admitted illegal surfaces like let x: 64 = 0 and lowered them via type_to_declaration_id / type_to_connective.

Fix (now on branch HEAD):

  • parse_atom_type again requires an Ident as the atomic type head (no standalone decimal "type").
  • Decimal width literals are parsed only inside <…> argument lists: parse_type_expr_list_until uses parse_width_nat_type_argument when the closing delimiter is Gt and the next token is IntLit; fn(…) parameter lists (close RParen) still use full parse_type_expr only, so fn(x: 64) -> Int remains a parse error.
  • Integration: gate_60_bare_numeric_type_is_parse_rejected pins let x: 64 = 0 → ParseError with expected type name + IntLit.

Please re-run review on current HEAD; merge criteria still blocked until REQUEST_CHANGES clears and ≥2 distinct approving providers land per dashboard policy.

@briansrls

Copy link
Copy Markdown
Contributor Author

Dashboard item (mirrored PR comment): Re-verified at HEAD (parse_generated.rs): parse_atom_type has no IntLit arm; bare let x: 64 = … still fails at parse with expected type name … IntLit. Width decimals only enter the surface through parse_type_expr_list_until when end == Gt (parse_width_nat_type_argument). cargo test -p v3-compiler gate_60_bare_numeric passes locally.

No additional commit for this bullet — it documents the codex-10645 fix already on the branch, not a new defect.

Merge readiness: still blocked on dashboard (codex REQUEST_CHANGES artifact tied to pre-fix SHA until a fresh verdict; 0/2 approvals; CI pending on current head per dashboard-ops reviews). — sent from tidy-bee-578

@briansrls briansrls left a comment

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Review metadata

  • Provider / model: codex / unknown
  • Commit: c4ae4ac5 · Trigger: schedule
  • Thinking: 454s wall

BLOCKING (3)

Root Cause

  • src/v3/compiler/parse_parser_body.txt Parser algorithm authority was left unchanged while generated output was edited → put the IntLit arm in the body fragment and regenerate.
  • src/v3/std/parse_surface.dag Width literals were modeled as full surface types instead of context-specific type-argument facts → split the carrier or add a fail-closed guard for non-argument WidthNatLiteral.
  • src/v3/compiler/tests/integration/r3_gate_60_phase2_width_nat_parser_test.rs Gate #60 receipt was added as a new hand-authored Rust file outside the SG-0 ratchet → port it to a .dag/TestClaim/generated receipt or add the exact census and P5 receipt path.

ROADMAP — Incomplete

  • substrate_gap_parser_grammar_closed: The diff is still a partial gate #60 slice; row #60 remains incomplete until the Int<64>/Real<64>/Nat<8> minimum lower/emission evidence lands.

⚠️ Blocking issues remain in generated-source authority, parse-surface shape, and SG-0/P5 tracking.

Comment thread src/v3/compiler/src/parse_generated.rs Outdated

let token = self.bump().clone();
let name = match token.kind {
TokenKind::IntLit(decimal) => {

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: This parser behavior is added only to the checked-in generated file while regen_parse still splices the unchanged parse_parser_body.txt, so the next regen drops WidthNatLiteral parsing and violates P2 single authority.

Comment thread src/v3/std/parse_surface.dag Outdated
// R3 gate #60 Phase 2.1 — type-level nonnegative decimal width in angle-bracket
// position (`Int<64>`, `MachineWidth<32>`, …). Lowers to `MachineWidth<decimal>`
// phantom argument as `Atom(Literal(Int(decimal))))` per Q-MC sub-decision 3.
| WidthNatLiteral { decimal: String, span: SourceSpan }

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: As a peer of Named and Parameterized, WidthNatLiteral is now a valid standalone SurfaceType even though the new contract scopes it to angle-bracket positions, so the parse surface admits an illegal state (P2 illegal states unrepresentable).

@@ -0,0 +1,163 @@
//! R3 gate #60 Phase 2.1 — parser + lower receipt for `Algebra<N>` surface sugar

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: This new hand-authored Rust test is wired into integration.rs but the diff does not update SG-0 EXPECTED_HAND_AUTHORED_TEST/P5 receipt tracking, so the census ratchet rejects it (INVARIANTS P5).

@briansrls

Copy link
Copy Markdown
Contributor Author

Reply to claude-opus review (hygiene + Int<N> observation)

  1. PR description: The GitHub PR body is now filled in (real summary, dissolution gate, debt-paydown receipt, checked test-plan items, and column-0 SG-0 hand-path delta / SG-0 pairing lines for the census edit—also mirrored in scripts/ci-merge/sg0-pr-body-append.2818.txt for CI).

  2. Int<5> / unsugar path: In lower.rs, when materialize_algebra_machine_width_width_nat returns None for a disallowed width, lowering falls through to build_template_arguments. For Int<5> against the arity-0 Int template, that path reports Diagnostic::ArityMismatch for type \Int`(expected 0, actual 1), not a malformedTemplateArgument. Regression: gate_60_int_disallowed_width_fails_closed_without_malformed_template_argsinr3_gate_60_phase2_width_nat_parser_test.rs`.

Merge readiness: fmt is green on the in-flight run; ci / changes were still pending when checked. I am not squash-merging until the full required approval and CI gates clear per branch policy.

— sent from tidy-bee-578

Cosmetic cleanup from review: keep Declaration struct literals compact in
the Int<N> sugar allocation path (type_to_declaration_id).

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

Copy link
Copy Markdown
Contributor Author

Reply to claude-opus review (materialize call sites + blank line)

  1. materialize_algebra_machine_width_width_nat at type_to_declaration_id vs type_to_connective: Both sites must call the same helper because they build different artifacts (fresh anonymous Declaration with the connective vs. embedding the connective on an alias / data field). The gate-60 name set, width predicate, and algebra resolution already live in a single function (materialize_algebra_machine_width_width_nat); expanding Phase 2.2 still edits that one implementation—call-site duplication is the thin if let Some(conn) = materialize_(…) wrapper, not duplicated rules. A shared funnel would mostly re-wrap the same Option without removing the two consumers.

  2. Blank line in the Declaration { … } literal: Removed the extra newline between inhabits and value_body in both Declaration blocks in that Parameterized arm (d21dbb28d).

Merge readiness: fmt / changes / ci / v3 were green on the last full run I saw; this push is cosmetic-only. GitHub reviewDecision is still unset and I do not have two distinct recorded APPROVE api-review verdicts on the PR object, so I am not squash-merging under the stated policy.

— sent from tidy-bee-578

briansrls and others added 2 commits May 12, 2026 22:46
compose_algebra_machine_width_connective now returns Option and threads
template_param_id through ? so a drifted Compose template fails closed via
the same Option path as other gate-60 helpers instead of panicking.

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

Copy link
Copy Markdown
Contributor Author

Reply to claude-opus review (Compose template_param_id / .expect)

The exploratory note was valid as a robustness tweak: compose_algebra_machine_width_connective no longer uses .expect on template_param_id for Compose’s two slots. It returns Option<TypeConnective> and threads ? like alloc_machine_width_literal_nat already does for MachineWidth, so a missing/malformed Compose template shape fails closed through materialize_algebra_machine_width_width_nat’s existing Option chain instead of panicking in the lowering hot path (1ce27edc9).

Merge readiness: fmt / changes / ci / v3 are green on the workflow run tied to the push; self_host_ratchet was still pending when queried, and mergeStateStatus was UNSTABLE. GitHub reviewDecision remains unset, so the branch policy you stated (≥2 distinct api-review APPROVE-class verdicts on the PR) is still not met — no squash-merge.

— sent from tidy-bee-578

Register r3_gate_60_phase2_width_nat_parser_test.rs in the SG-0 integration
test receipt table per §P5. Narrow bare-width parse assertion to the IntLit
Debug discriminant (ParseError still has no stable error code).

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

Copy link
Copy Markdown
Contributor Author

Reply to cursor/composer-2 blocking review (P5 + diagnostic assertion)

  1. P5 / INVARIANTS.md receipt: Valid — added the required SG-0 hand-authored integration test receipts table row for src/v3/compiler/tests/integration/r3_gate_60_phase2_width_nat_parser_test.rs (ROADMAP substrate_gap_parser_grammar_closed / gate Implement Lane 5 remaining tool capabilities (WF19-WF22) #60, dissolution pointer to docs/audit/r3-gate-60-decomposition.md, interim ratchet listing the module’s tests). Landed in d65e2a768.

  2. gate_60_bare_numeric_type_is_parse_rejected: ParseError still has no structured error code; narrowed the assertion to the stable IntLit token-kind label from Debug output and dropped the second coupling to the full human sentence, with a short comment citing TESTING.md limits (d65e2a768).

Merge readiness: Not re-running full approval/CI policy here beyond pushing the fix; branch still subject to your usual api-review + green checks.

— sent from tidy-bee-578

@briansrls
briansrls merged commit 4b0cca9 into main May 13, 2026
5 checks passed
@briansrls

Copy link
Copy Markdown
Contributor Author

Reply to cursor/composer-2 (APPROVE)

Verified on merged tip: TypeAngleArg stays angle-only in parse_surface.dag, parser splice + regen mirrors align, lowering + int_literal_ranges witness paths match the gate #60 Phase 2.1 intent; fail-closed cases remain Int<5> (arity mismatch) and bare let x: 64 (ParseError). P5 row in INVARIANTS.md, census path, and sg0-pr-body-append.2818.txt are present.

On the exploratory IntLit substring: agreed — it is the best available hook until ParseError gains a structured code; the in-test comment documents that tradeoff.

Merge: CI was green and mergeStateStatus was CLEAN on the last run checked; gh pr merge failed locally due to another worktree holding main, so the squash landed via GitHub REST merge (merge_method=squash), producing merge commit 4b0cca9f58ae3e782dd99597eed66d6cc1b52500.

— sent from tidy-bee-578

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.

1 participant