Repository navigation
fix(r3): correct SubValueRelation algebra claim - #1543
Merged
Merged
Conversation
This was referenced May 2, 2026
Contributor
Author
|
Review metadata
Findings: None. The diff only updates comments in Verdict: APPROVE — Narrow documentation correction; aligns comments with real semantics and avoids a misleading bounded-lattice claim. No rubric violations observed in the diff. |
Contributor
Author
|
Review metadata
1. Story of the diffThis PR corrects the substrate-facing explanation around 2. Invariant categories
Compliant — the diff touches a substrate-adjacent std
Compliant — Modeling Faithfulness / single-authority are improved here: the diff stops presenting
N/A — the diff does not change Rust implementation code, function signatures, helper placement, error/result shapes, or method/free-function structure.
N/A — this is a comment-only correction to an algebra claim; no executable behavior or public test contract changed, so a regression test would not have a changed runtime surface to pin.
N/A — the diff does not reference or alter a locked design decision; it narrows local commentary around existing helpers.
Compliant — no new scaffold, TODO, bridge, or temporary representation is introduced; the replacement wording makes the non-inhabitance explicit and avoids leaving a deferred generic-constant promise as an implied bridge ( 3. VerdictAPPROVE. The PR is a narrow comment-only correction that reduces an overclaimed algebraic contract without introducing new substrate shape, implementation code, tests, or debt. I found no invariant or discipline violation in the changed lines. |
This was referenced May 3, 2026
briansrls
added a commit
that referenced
this pull request
May 3, 2026
Same root cause as the parent commit's bootstrap_generated.rs regen: PR #1543 edited src/v3/std/induction.dag without refreshing the paired parse-corpus manifest hash. CI v3 check on the prior commit caught the manifest staleness: on_disk: induction.dag ... 546f74c63c189c50 fresh: induction.dag ... e405e1549cf2fe08 Pure refresh via: cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored Single line changed; only induction.dag's hash. No other corpus entry moved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
PR #1543 modified `src/v3/std/induction.dag` to correct a SubValueRelation algebra claim but did not refresh the SG-2 parser-corpus snapshot, leaving the committed manifest hash stale relative to the actual file. The v3 suite's `handwritten_parse_snapshot_matches_manifest` reproduced this on the merge into this branch — refreshing via the documented helper. Generated by: cargo test -p v3-compiler --test integration \\ refresh_handwritten_parse_snapshot_manifest -- --ignored Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
#1557) * chore(v3): regen bootstrap_generated.rs after #1543 induction.dag edit PR #1543 (SubValueRelation algebra correction) edited induction.dag without the paired regen of bootstrap_generated.rs. The on-disk snapshot ratchet caught the drift on main HEAD: span offsets 12177,12677 vs expected 12138,12638 around induction.dag declarations. Pure regen output; no hand edits. R3 Debt Receipt - Debt paid: bootstrap-snapshot drift introduced by #1543. - Debt found + routed: paired-regen-on-substrate-edit invariant should be enforced by pre-merge CI rather than caught only after merge by the on-disk ratchet. Routed to R3 Substrate (jolly-ram-908 #1130) for invariant gate authoring. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore(v3): refresh parse_corpus_manifest.txt for induction.dag Same root cause as the parent commit's bootstrap_generated.rs regen: PR #1543 edited src/v3/std/induction.dag without refreshing the paired parse-corpus manifest hash. CI v3 check on the prior commit caught the manifest staleness: on_disk: induction.dag ... 546f74c63c189c50 fresh: induction.dag ... e405e1549cf2fe08 Pure refresh via: cargo test -p v3-compiler refresh_handwritten_parse_snapshot_manifest -- --ignored Single line changed; only induction.dag's hash. No other corpus entry moved. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 3, 2026
briansrls
added a commit
that referenced
this pull request
May 3, 2026
PR #1543 modified `src/v3/std/induction.dag` (SubValueRelation algebra correction) but did not regenerate the committed bootstrap snapshot. v3 CI's `regen_bootstrap --verify` gate flagged span-offset drift in the induction.dag entry on this branch. Regenerated via the documented helper. Generated by: cargo run -p v3-compiler --features bootstrap-regen-fresh \\ --bin regen_bootstrap Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
… constructors (#1551) * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): add Magnitude opaque carrier (T-Numeric-Construction Slice 1) * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): T-Numeric-Construction Slice 2 — Nat = Semiring<Magnitude> * fix(std/nat): document tracked-scaffold dissolution trigger to CommutativeSemiring<T> Reviewer flagged: Nat denotationally inhabits CommutativeSemiring (commutative mul) but algebra.dag declares only Semiring<T>. Per modeling-philosophy (layer concept introductions; sharpen via stronger algebras as separate slices), this is the closest honest algebra surface today. Adding a P5 tracked-scaffold note pinning the dissolution trigger so the future algebra-strength sharpening slice is visible at the use site. * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * chore: apply cargo fmt * revert(std): drop Int = AbelianGroup<Nat> alias pivot; add GroupCompletion<M> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4360232423) after two reviewers flagged a sharp M9 modeling-faithfulness finding: with the standard parametric reading of `AbelianGroup<T>`, T is the carrier of group operations including `inverse: fn(T) -> T`. With T = Nat, that denotes 'every Nat has an additive inverse' — false for ℕ. ℤ is derived from ℕ via Grothendieck construction; ℤ's carrier is not ℕ itself. Reverted in this commit: - dsl/std/integer.dag: type Int = Int64 restored; AbelianGroup/Nat imports removed. - src/v3/compiler/tests/integration/common/substrate_receipts.rs: receipt walks Int (= Int64) again; legacy comment restored. - src/v3/compiler/tests/integration/m1_substrate_test.rs: test renamed back to bootstrap_int_add_walk_reaches_ordered_ring_add_nobody_arrow. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: the AbelianGroup<Nat>-blessing ratchet (int_default_alias_resolves_to_abelian_group_over_nat) removed entirely per Director's 'do not keep a ratchet that blesses AbelianGroup<Nat>' guard. - bootstrap_*_generated.rs regenerated to track reverted integer.dag. Added in this commit: - docs/audit/t-numeric-construction-group-completion-6q.md: 6Q substrate- introduction audit for the prerequisite GroupCompletion<M> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per design doc 'no quotient/sign- magnitude representation' boundary. Once GroupCompletion<M> lands, Slice 3 becomes a single-line edit: type Int = GroupCompletion<Nat>. * fix(test): revert stale parse_corpus_manifest row for integer.dag Director caught: the PR's manifest still carried the alias-pivot bytes (16/12179/9c6a1d94...) for dsl/std/integer.dag, but integer.dag itself is reverted to origin/main state (15/11459/a2942a07...). Restore the manifest row so the PR diff is docs-only (the GroupCompletion<M> audit). * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * WIP: tidy-tern-769 * feat(std): GroupCompletion<M> opaque-atom substrate-introduction Ships the prerequisite carrier construction from the audit at docs/audit/t-numeric-construction-group-completion-6q.md (#1422 audit receipt). Strictly Shape C — bare opaque atom in dsl/std/algebra.dag, parameterized by <M>, no fields, no algebra inhabitance. - dsl/std/algebra.dag: type GroupCompletion<M> declared after AbelianGroup<T>, with full header documenting hard boundaries (no quotient-of-pairs, no sign-magnitude, no mechanical AbelianGroup-witness derivation) + the constrained-inhabitance tracked-scaffold note (M : CommutativeMonoid is denotational; future parametric where-clause syntax dissolves the gap). - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet group_completion_is_bare_opaque_atom_with_one_type_parameter pinning span (algebra.dag), connective shape (Conj { children: [] }), type_params count (1), and absent value_body. - bootstrap_*_generated.rs regenerated; parse-corpus manifest refreshed for the new algebra.dag bytes. Per dispatch on inbox #1288 #4361921687: did NOT pivot Int (Slice 3 stays deferred), did NOT introduce quotient/sign-magnitude carrier facts, did NOT claim mechanical AbelianGroup witness derivation. The future Slice 3 edit becomes type Int = AbelianGroup<GroupCompletion<Nat>> per the audit's Q6 single-authority resolution. * feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> Pivot the default Int alias to the canonical Q6 single-authority form per docs/audit/t-numeric-construction-group-completion-6q.md. Now that GroupCompletion<M> is a substrate carrier (#1448), the construction-chain layer-3 algebra is honest under standard parametric reading: T = GroupCompletion<Nat> (derived carrier; opaque atom) AbelianGroup<T> (algebra witness; inverse: T -> T well-defined) Fixed-width rows (Int8..Int128, UInt8..UInt128) stay on OrderedRing<Word*>/Semiring<Word*>. Word* storage carriers remain storage refinements, not alternate Int/Nat/Magnitude/GroupCompletion authorities. - dsl/std/integer.dag: type Int = AbelianGroup<GroupCompletion<Nat>>; imports Nat, AbelianGroup, GroupCompletion. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet int_default_alias_resolves_to_abelian_group_over_group_completion_of_nat pinning the two-step Instantiation chain (AbelianGroup template, carrier = GroupCompletion<Nat>, GroupCompletion's input = Nat). - src/v3/compiler/tests/integration/common/substrate_receipts.rs + m1_substrate_test.rs: legacy Int → OrderedRing receipt repointed to walk Int64 directly (the OrderedRing<Word64> chain it pinned now lives at the fixed-width row, not the default alias). - bootstrap_*_generated.rs regenerated; parse_corpus_manifest.txt refreshed. Per Director's guardrail (dispatch on inbox #1288 #4362239705): no consumer migration of legacy Int64/OrderedRing<Word*> chain in this PR; no quotient/sign-magnitude representation; no tokenizer/literal/refinement syntax work. Total downstream impact: one ratchet rename + manifest refresh — within the 'ratchets/generated outputs' scope explicitly authorized by the dispatch. * chore: apply cargo fmt * fix(test): pin transform_callable_unsupported_in_e3_slice to Bool not Int CI caught: Slice 3's pivot of `Int` from alias to direct Instantiation made `callable_runtime_arity(Int) = Some(3)` (AbelianGroup's Conj children), which fires the push_transform arity assertion when the test feeds 0 inputs. The test's subject is eval_node's rejection of Callable transforms — the declaration is incidental. Switch to `Bool` (Disj), whose `callable_runtime_arity` resolves to None and is stable across future numeric-substrate edits. * chore: apply cargo fmt * feat(std): T-Numeric-Construction Slice 4 — Rational = Field<Int> Adds layer 4 of the construction chain authored in docs/design-numeric-construction.md: Magnitude → Nat → Int → Rational → Real `Rational = Field<Int>` consumes the Slice 3 `Int = AbelianGroup<GroupCompletion<Nat>>` algebra (#1466) as the underlying carrier and extends the ring structure with Field's reciprocal/division operations. Per dispatch on inbox #1288 #4362611659: attempted the simple alias form first (Director's preference); if reviewers prove M9 cannot stand under the standard parametric reading of Field<T>'s reciprocal field, the slice escalates to Director for substrate-split ratification (mirroring the GroupCompletion path established in Slice 3). - dsl/std/rational.dag (new): module std.rational; type Rational = Field<Int>. Long header documents the executable-completeness gap (Field<Int> denotes reciprocal: fn(Int) -> Int which is denotationally undefined for non-units in ℤ) as a P5 tracked scaffold with named dissolution trigger (FieldOfFractions<R> derived-carrier or NonZero/Result reciprocal refinement), consistent with the prior #1370 audit's deferred completeness gap. - src/v3/compiler/src/bootstrap_regen_fresh.rs: rational.dag wired into std_fixtures (between integer.dag and string_type.dag). - src/v3/compiler/tests/integration.rs: parse-corpus extended; new parser smoke handwritten_parser_accepts_rational_dag. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new ratchet rational_resolves_to_field_over_int pinning span (rational.dag), outer Field instantiation, and Int carrier (alias-chain walk through the construction-chain Int alias). - src/v3/compiler/tests/integration/parse_corpus_manifest.txt: refreshed. - bootstrap_*_generated.rs regenerated. Hard boundaries respected: - No NonZero/Result reciprocal semantics in this PR (deferred per dispatch). - No refinement syntax. - No consumer migration. - No tokenizer/literal-grammar work. * chore: apply cargo fmt * revert(std): drop Rational = Field<Int> alias pivot; add FieldOfFractions<R> 6Q audit Director ratified Option 2 substrate-split (inbox #1288 #4362643231) after the same M9 modeling-faithfulness finding that retired AbelianGroup<Nat>: under the standard parametric reading of Field<T>, T is the carrier of field operations including reciprocal: fn(T) -> T. With T = Int, that denotes 'every Int has a multiplicative inverse' — false for ℤ (only ±1 are units). ℚ is the field of fractions derived from ℤ; ℚ's carrier is not Int itself. Reverted in this commit: - dsl/std/rational.dag: deleted (was authoring the false alias). - src/v3/compiler/src/bootstrap_regen_fresh.rs: rational.dag fixture registration removed. - src/v3/compiler/tests/integration.rs: parse-corpus + parser smoke reverted. - src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: rational_resolves_to_field_over_int ratchet removed (per Director's 'remove any ratchet that blesses Field<Int>' guard). - bootstrap_*_generated.rs regenerated to track the revert. - parse_corpus_manifest.txt restored to origin/main state. Added in this commit: - docs/audit/t-numeric-construction-field-of-fractions-6q.md: 6Q substrate-introduction audit for the prerequisite FieldOfFractions<R> algebra surface. Recommends Shape C (opaque atom; carrier-representation deferred to per-target emission) per Director's 'no pair/quotient numerator-denominator representation' boundary and the GroupCompletion precedent (#1448). Once Shape C lands, Slice 4 becomes a one-line edit: type Rational = Field<FieldOfFractions<Int>>. * WIP: tidy-tern-769 * test(v3): add per_call_descent_evidence_is_single_lookup_authority ratchet T-E-P-Producer-Broadening gate (2) — e_p_call_pattern_lookup_authoritative (per Director's path-(1) selection on inbox #1288 #4363830953). Pins per_call_descent_evidence as the single lookup authority for per-call SubValueRelation evidence over TransformTarget::Callable transforms. Behavioral cardinality assertion: - Every Callable transform in the user fixture file appears in exactly one CallDescentEvidence entry (uniqueness; no parallel producer appending duplicates). - The producer's emitted set (filtered to fixture file) equals the enumerated Callable-transform set in the fixture (totality; producer is not silently dropping call sites). - Every entry corresponds to a real Callable-targeted transform (no synthetic entries from a parallel walker). Visibility unchanged: SubValueRelation enum constructors stay pub for existing test usage (m2_substrate_inhabitance_test.rs:577 and the new e_p tests construct SubValueUnknown directly); the producer helpers classify_call_argument and arithmetic_descent_relation are already private to dag.rs. No producer broadening, no substrate carrier introduction, no lens consumer in this slice. Per dispatch (#1288 #4363830953): S-sized ratchet only; gates (1) and (3) tracked as separate slices. * test(v3): expand E-P gate-2 fixture to exercise cross-template branch Reviewer caught: gate (2) single-authority claim must hold for both branches of per_call_descent_evidence's match (caller_template == callee_template self-recursion AND resolved cross-template fail-closed), but the prior fixture only had countdown self-recursion. A future producer that adds a parallel walker for cross-template evidence (rather than going through the existing fail-closed path) would slip past a self-recursion-only ratchet. Restored the two-function fixture (countdown + caller→helper) so the sanity-floor assertion >= 2 Callable transforms exercises both branches, and the coverage-equality assertion enforces single-authority over the cross-template fail-closed path too. Verified locally with RUST_MIN_STACK=33554432: test passes. * polish(test): trim duplicate comments + dead let; align module doc with span-scoped oracle Cursor exploratory feedback (#1514): two duplicate comment blocks merged into one, no-op 'let _ = ();' placeholder dropped (subsumed by neighbour comment), variable renamed owned_callable_transforms → fixture_callable_transforms (span-based, not body-bind-based) for accuracy, module doc bullet rewritten to describe the span-scoped oracle the code actually uses. No behavioral change; tightens local-readability of the ratchet. * fix(v3): reject duplicate fields in expression-position named-variant constructors `lower_record_to_structural` (data body) and `lower_record_literal_expr` (anonymous record expression) already rejected duplicate field labels before type-field projection. `lower_variant_record_expr` — the path for named-constructor record payloads at expression position, e.g. `Ready { code: 1, code: 2, retry: false }` inside an fn body — silently projected via `find()` over the literal's fields, dropping the second occurrence and constructing a normal payload. Mirror the duplicate-detection pattern from `lower_record_literal_expr` (HashSet pre-pass returning a typed ResolveError on collision) so the third record-shape lowering path now also fails closed. Adds `expr_named_variant_duplicate_payload_fields_fail_closed` covering the previously-silent expression-context path; the existing `data_body_named_variant_duplicate_payload_fields_fail_closed` covers the data-body context. Closes the "Duplicate record-literal fields silently accepted" row of docs/debt/r3-debt-paydown-ledger-2026-05-02.md. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: refresh parse_corpus_manifest after induction.dag content change PR #1543 modified `src/v3/std/induction.dag` to correct a SubValueRelation algebra claim but did not refresh the SG-2 parser-corpus snapshot, leaving the committed manifest hash stale relative to the actual file. The v3 suite's `handwritten_parse_snapshot_matches_manifest` reproduced this on the merge into this branch — refreshing via the documented helper. Generated by: cargo test -p v3-compiler --test integration \\ refresh_handwritten_parse_snapshot_manifest -- --ignored Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * chore: refresh bootstrap_generated.rs after induction.dag content change PR #1543 modified `src/v3/std/induction.dag` (SubValueRelation algebra correction) but did not regenerate the committed bootstrap snapshot. v3 CI's `regen_bootstrap --verify` gate flagged span-offset drift in the induction.dag entry on this branch. Regenerated via the documented helper. Generated by: cargo run -p v3-compiler --features bootstrap-regen-fresh \\ --bin regen_bootstrap Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
2 tasks done
briansrls
added a commit
that referenced
this pull request
May 3, 2026
Bundle 1 + 4b dispatch closure receipts: - row 77 (duplicate record-literal fields) → Retired by PR #1551 - row 91 (SubValueRelation BoundedLattice claim) → Retired by PR #1543 Bundle 3 Phase 1 progress: - row 85 (method-template consumer migration) → Partial; PR #1549 audit landed; Phase 2 in flight (#1560, #1561) Per-PR Debt-Paydown receipt against rows 77, 85, 91. Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
briansrls
added a commit
that referenced
this pull request
May 3, 2026
…l blocked (#1569) * docs(r3): retire rows 77, 91 + Phase-1 partial-close row 85 Bundle 1 + 4b dispatch closure receipts: - row 77 (duplicate record-literal fields) → Retired by PR #1551 - row 91 (SubValueRelation BoundedLattice claim) → Retired by PR #1543 Bundle 3 Phase 1 progress: - row 85 (method-template consumer migration) → Partial; PR #1549 audit landed; Phase 2 in flight (#1560, #1561) Per-PR Debt-Paydown receipt against rows 77, 85, 91. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> * docs(r3): correct row-85 framing — #1568 is oracle-only, Gap 4/5 still blocked Per Director correction (#828 reply 4365998510): #1568 is a Rust projection / test-oracle helper only, not the Phase-2 consumer-surface closure. Gap 4 (build-step consumer surface) + Gap 5 remain blocked on substrate build-pipeline support for ephemeral generated-source-root .dag imports (tied to #1558 dissolution-first reframe), or on a Gap 5 design that avoids that surface. Records the routing of all 5 gaps from the #1549 Phase 1 audit: - Gap 1, Gap 2: active in Substrate - Gap 3: reference-only via BootstrapAuthority carrier #1554 (landed) - Gap 4, Gap 5: blocked, calm-tern Phase 2 leaf migration parked Per-PR Debt-Paydown receipt against ledger row 85. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com> --------- Co-authored-by: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
This was referenced May 3, 2026
briansrls
added a commit
that referenced
this pull request
May 4, 2026
The ci job header already promised the #1543 fail-closed gate but the Rust/cache/regen steps were missing. Add them and drop the duplicate verify from the v3 job. Co-authored-by: Cursor <cursoragent@cursor.com>
This was referenced May 5, 2026
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
src/v3/std/induction.dagsoSubValueRelationno longer claimsBoundedLatticeinhabitancemeet_sub_valueas the conservative fail-closed merge helper andjoin_sub_valueas an optimistic auxiliary helperDebt receipt
docs/debt/r3-debt-paydown-ledger-2026-05-02.mdrowSubValueRelation bounded-lattice law violation; retired by stopping the invalidBoundedLatticeclaim perdocs/audit/sub-value-relation-bounded-lattice-claim.mdPath B.Validation
cargo test -p v3-compiler --test integration m2_substrate_inhabitance_test::e_p_runtime_mirror_matches_induction_carrier_shape -- --exactcargo fmt --all --checkgit diff --check