Repository navigation
feat(std): GroupCompletion<M> opaque-atom substrate-introduction - #1448
Conversation
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
# Conflicts: # src/v3/compiler/src/bootstrap_generated.rs # src/v3/compiler/src/bootstrap_generated_without_parse_surface.rs
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.
|
Review metadata
Verdict: APPROVE — Diff is narrowly scoped: one opaque-atom type |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
9c53d06e· Trigger:schedule - Thinking:
210s wall
Non-blocking — Strengths
dsl/std/algebra.dagClassified as (d) mixed; the substrate change keeps GroupCompletion as a single opaque carrier and documents the bounded constrained-inhabitance scaffold with a named dissolution trigger.src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rsThe ratchet test pins the relevant substrate facts: std placement, no representation fields, one type parameter, and no value_body.
✅ No blocking concerns.
|
Review metadata
Verdict: APPROVE — Narrow, well-scoped substrate introduction. The diff adds a single opaque atom Notes (not findings):
Nothing in the diff violates INVARIANTS / modeling-discipline / CODING / TESTING. |
…ompletion<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.
…ompletion<Nat>> (#1466) * 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
…ions<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>>.
…tions<R> design receipt (#1470) * 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>>.
…y ratchet (#1514) * 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.
… 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>
Summary
Ships the prerequisite carrier construction from the Slice 3 prerequisite audit (#1422). Authority:
docs/audit/t-numeric-construction-group-completion-6q.md. Strictly Shape C — bare opaque atom indsl/std/algebra.dag, parameterized by<M>, no fields, no algebra inhabitance.What lands
dsl/std/algebra.dag:Plus a long header documenting:
GroupCompletion<M>is only the carrier. The algebra witness for Slice 3 will beAbelianGroup<GroupCompletion<Nat>>(standard parametric reading;T = GroupCompletion<M>).<M> : CommutativeMonoidstructurally. Bounded denotationally — Slice 3's only intended consumer isGroupCompletion<Nat>, andNat = Semiring<Magnitude>carries commutative-monoid laws via Semiring's add+zero+commutativity-on-add. Named dissolution trigger: when constrained-inhabitance lands, tighten to<M> : CommutativeMonoid.(M, M) / ~; no sign-magnitude(Sign, M); no mechanicalAbelianGroup-witness derivation declared at this layer.Structural ratchet
src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs::group_completion_is_bare_opaque_atom_with_one_type_parameter:span.file == "dsl/std/algebra.dag"(audit's preferred home).connectiveisTypeConnective::Conj { children: [] }— bare opaque atom with no fields. A non-empty Conj would admit structural representation facts (quotient/sign-magnitude) the audit rejects.type_params.len() == 1(the<M>input type-parameter).value_body.is_none()— opaque type declaration, not a data declaration.Same shape as Slice 1's Magnitude precedent (bare opaque atom; algebra inhabitance attached at use sites, not baked into the carrier).
Hard boundaries respected (per dispatch on inbox #1288 #4361921687)
Intalias pivot in this PR — Slice 3 stays deferred.AbelianGroup-witness derivation — current substrate cannot express algebra-inhabitance over a parametric carrier; the inhabitance lens is a follow-up.dsl/std/algebra.dagfor proximity toAbelianGroup<T>).Files
dsl/std/algebra.dag— newtype GroupCompletion<M>with header.src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs— new structural ratchet.src/v3/compiler/tests/integration/parse_corpus_manifest.txt— refreshed foralgebra.dag's new bytes.src/v3/compiler/src/bootstrap_{std_,}generated{,_without_parse_surface}.rs— regenerated.Test plan
cargo run -p v3-compiler --features bootstrap-regen-fresh --bin regen_bootstrap(clean).cargo test -p v3-compiler --test integration -- group_completion_is_bare_opaque_atom_with_one_type_parameter handwritten_parse_snapshot_matches_manifest(2/0).cargo build --workspaceclean.cargo test -p v3-compiler --lib -- --skip execute_command_timebound(225/0).cargo test -p v3-compiler --test integration(running).cargo clippy --all-targets -- -D warnings.cargo fmt --all --check(pre-push hook clean).Next slice
Once this lands, Slice 3 becomes a one-line
dsl/std/integer.dagedit:plus a structural ratchet pinning the new shape, plus consumer-edit verification within the dispatch's "ratchets/generated outputs" guardrail.