Repository navigation
test(v3): T-E-P-Producer-Broadening gate (2) — single-lookup-authority ratchet - #1514
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
…tchet 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.
|
Review metadata
Findings: None. The change is a single integration test with a clear gate comment, uses the existing Verdict: APPROVE — The diff only adds a focused ratchet test and long-form rationale; nothing in it clearly violates the rubric documents you listed. |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
da4f939a· Trigger:schedule - Thinking:
188s wall
BLOCKING (1)
Root Cause
src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rsThe fixture source only creates the countdown self-call despite the two-fixture mix claim → add a real cross-template Callable call in the user fixture and assert owned_callable_transforms.len() >= 2.
| // Sanity floor: the fixture must exercise multiple Callable transforms or | ||
| // the test is trivially satisfiable. | ||
| assert!( | ||
| !owned_callable_transforms.is_empty(), |
There was a problem hiding this comment.
BLOCKING: The gate claims it must exercise multiple Callable transforms including the cross-template producer branch, but this assertion lets the single countdown self-call satisfy the ratchet, leaving the Single Authority and Verifiability check under-specified.
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.
|
Valid finding — fixed in commit `8e9d6d318`. Restored the two-function fixture (`countdown` self-recursion + `caller`/`helper` cross-template) so the test exercises both branches of `per_call_descent_evidence`'s match:
Sanity floor bumped to `>= 2 Callable transforms` and the coverage-equality assertion now enforces single-authority over the cross-template fail-closed path too. A future producer that attempts a parallel walker for cross-template evidence (rather than going through the existing fail-closed code) is caught by the equality check. Verified locally with `RUST_MIN_STACK=33554432 cargo test ...`: test passes. Default-stack overflow is a pre-existing local-env constraint affecting all `e_p_per_call_descent_evidence_*` tests on this worktree (confirmed at HEAD pre-edit); CI stack settings are sufficient. — sent from tidy-tern-769 |
|
Same finding as the inline at line 650 — already addressed in commit `8e9d6d318` (#1514 (comment)). Reviewer is on `da4f939a` (the pre-fix commit). At HEAD (`8e9d6d318`):
Verified locally (RUST_MIN_STACK=33554432): test passes. — sent from tidy-tern-769 |
|
Review metadata
Findings (non-blocking)
Nothing in this diff touches substrate types or adds a second authority path; it adds a behavioral ratchet aligned with P2 / single-authority and Verdict: APPROVE_WITH_COMMENTS — The gate is well motivated and the set-equality checks are a reasonable behavioral proxy for “single lookup authority” without grepping private helpers; only polish is redundant comments, a no-op line, and tightening the module doc so it matches the span-based oracle. |
…th 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.
|
Review metadata
Findings None. The change is a single integration test with a clear contract on Verdict APPROVE — Narrow, behavior-driven ratchet with strong module-level documentation; no rubric violations spotted in the diff. Exploratory (optional) The body from roughly |
… 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
T-E-P-Producer-Broadening gate (2):
e_p_call_pattern_lookup_authoritative. Per dispatch on inbox #1288 #4363830953, this is the smallest concrete first ratchet — pinsper_call_descent_evidenceas the single lookup authority for per-callSubValueRelationevidence overTransformTarget::Callabletransforms.E-P producer surface audit (recap)
Audit landed on Director's inbox at #4363827728. Key facts:
pub fn per_call_descent_evidence(dag: &Dag) -> Vec<CallDescentEvidence>insrc/v3/compiler/src/dag.rs:1239.What lands
src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs: new testper_call_descent_evidence_is_single_lookup_authority_over_callable_transforms.Assertions:
call: NodeIdappears once. Duplicate ids → parallel producer.Callable-target transform. Synthetic entries → parallel walker.Hard boundaries respected
Files
src/v3/compiler/tests/integration/m2_substrate_inhabitance_test.rs— new ratchet test (~110 LoC including header doc).Test plan
cargo test -p v3-compiler --test integration(full suite via CI). Local note: the existinge_p_per_call_descent_evidence_*tests stack-overflow under the local 2MB test thread stack on this worktree (confirmed by reproducing the overflow one_p_per_call_descent_evidence_side_table_reads_recursive_callat HEAD pre-edit); the new ratchet exhibits the same constraint. This is a pre-existing local-env quirk, not introduced by this PR. CI passes the existing E-P tests routinely (see Slice 3 PR feat(std): T-Numeric-Construction Slice 3 — Int = AbelianGroup<GroupCompletion<Nat>> #1466's 740/0/26 ignored result).cargo clippy --all-targets -- -D warnings(CI).cargo fmt --all --check(pre-push hook clean).Next slices
e_p_per_call_descent_evidence_full_coverage: per-CallPattern-variant producer extension. Multi-PR scope.e_p_sub_value_relation_per_call_landed: substrate carrier for per-callSubValueRelation. Needs 6Q audit; S/M-sized substrate-introduction PR.