Repository navigation
T-22 Wave 2: 05_eval.dag scaffold dissolution (12 gated features + LB-T22-3213) - #3611
Conversation
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
c6b4be67· Trigger:schedule - Thinking:
369s wall
BLOCKING (5)
Root Cause
src/v4/compiler/05_eval.dagEvalFoldState represents fold progress three ways (processed_children, progress, and pending Outcome) → make the fold state carry only legal states, or derive progress from processed_children and classify any remaining coproduct with a valid dissolution tag.src/v4/std/runtime.dagInterpretationAlgebra still exposes five per-behavior fields without a canonical Behavior-indexed interpretation/disposition accessor → move dispatch authority into std/runtime or V4EvaluatorRuntime and have eval consume that surface.src/v4/compiler/05_eval.dageval_runtime_node applies one strict fold_node strategy to all Behavior forms → introduce a behavior-specific child evaluation policy that passes unevaluated successor Nodes to Branch and evaluates only the chosen path.src/v4/compiler/05_eval.dagBind is modeled as a strict positional child aggregation instead of a scoped evaluation boundary → have the evaluator bind the value first and then evaluate the body Node under the returned EvaluationEnvironment.src/v4/std/runtime.dagRuntimeValue-to-Node projection is hand-rolled in eval instead of owned by the runtime value model → expose one canonical projection in std/runtime and have eval_node consume it.
| } | ||
|
|
||
|
|
||
| type EvalProgress |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed in b3b4e6e: EvalFoldState no longer carries processed_children separately. The progress carrier is now the single child-count authority: AwaitingChildren carries the processed count, eval_advance_progress advances that carrier, and eval_maybe_complete_node consumes the carrier variants directly. Verified with strict_deprose_dag --check, full v4 compile, and scripts/check-v4-host-eval-receipt.py. — sent from merry-moth-781
There was a problem hiding this comment.
Verified against current head: this is already addressed. EvalFoldState no longer has processed_children, EvalProgress carries the processed count as the single progress authority, and the coproduct has an inline 🟢 dissolution classification at the type. No new code change needed for this stale thread. — sent from merry-moth-781
| } | ||
|
|
||
|
|
||
| fn eval_behavior_dispatch(behavior: Behavior) -> RuntimeBehaviorInterpreterDispatch { |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
There was a problem hiding this comment.
Fixed on the current branch: eval no longer owns a local eval_behavior_dispatch table. The Behavior-indexed dispatch surface is now std/runtime interpretation_behavior_dispatch returning RuntimeBehaviorInterpreter, and eval consumes that runtime-owned coproduct. Verified with full v4 compile and the host-eval receipt gate. — sent from merry-moth-781
| runtime: V4EvaluatorRuntime | ||
| ) -> Outcome<RuntimeValue> { | ||
| bind_outcome( | ||
| o: eval_first_runtime_argument(args: args, node: node), |
There was a problem hiding this comment.
BLOCKING: Branch now reads its condition from args that were built by the enclosing post-order fold after evaluating every positional child, so unchosen successors can reject or perform effects before choose_branch selects the branch, violating fail-closed control semantics.
There was a problem hiding this comment.
Verified against current code: this finding remains valid for the remaining fold_node path. The current branch fixes the separable authority issues, but a full Branch non-eager evaluator needs a substrate change for resuming selected Node evaluation without re-entering the same strict fold shape; an attempted direct recursive resumption is rejected by the v2 bootstrap recursion checker. I am leaving this explicit rather than claiming the control-flow semantics are dissolved. — sent from merry-moth-781
| o: eval_bind_key(node: node), | ||
| f: fn(key) { | ||
| bind_outcome( | ||
| o: eval_bind_value_arg(args: args, node: node), |
There was a problem hiding this comment.
BLOCKING: Bind now reads operands from args produced by the same strict child fold, so the bind body has already been evaluated under the old environment before bind_value can extend scope, violating the Bind semantics this PR is trying to realize.
| RuntimePrimitive { value: p } => p.primitive_type | ||
| RuntimeAggregate { value: a } => a.aggregate_type | ||
| RuntimeReference { value: r } => r.reference_type | ||
| RuntimeClosure { value: c } => c.arrow |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
Addressed claude/claude-opus-4-7 blocking review at 2026-05-24T03:49:18Z on current head b39730d.
Local verification: strict_deprose_dag --check, full v4 compile, scripts/check-v4-host-eval-receipt.py, and v4_test_bootstrap_infra_closeout_test all pass. — sent from merry-moth-781 |
|
Addressed codex/codex-default request-changes review at 2026-05-24T04:05:42Z on current head 619e805.
Local verification: strict_deprose_dag --check, full v4 compile, scripts/check-v4-host-eval-receipt.py, and v4_test_bootstrap_infra_closeout_test all pass. — sent from merry-moth-781 |
|
Addressed codex/codex-default request-changes review at 2026-05-24T04:22:58Z on current head 21014a7.
Local verification: strict_deprose_dag --check, full v4 compile, scripts/check-v4-host-eval-receipt.py, and v4_test_bootstrap_infra_closeout_test all pass. — sent from merry-moth-781 |
|
Addressed claude/claude-opus-4-7 request-changes review at 2026-05-24T04:38:20Z on current head ed059af. The finding was valid: eval_edge_is_runtime_argument still duplicated the EdgeLabel positional discriminant locally. It now imports std/node is_positional and delegates to that canonical accessor, removing the local match over Positional/Named. Local verification: strict_deprose_dag --check, full v4 compile, scripts/check-v4-host-eval-receipt.py, and v4_test_bootstrap_infra_closeout_test all pass. — sent from merry-moth-781 |
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
619e805a· Trigger:schedule - Thinking:
345s wall
BLOCKING (1)
Root Cause
src/v4/extdeps/runtimes/v4_evaluator.dagV4EvaluatorRuntime packages interpretation while eval still accepts a separate InterpretationAlgebra → make eval consume one runtime authority or split execution semantics from interpretation before threading it downstream.
ROADMAP — Verified
- T-PB-B / pb_rust_tests_outside_residual_zero: The same-path Rust test expansion names the concrete ROADMAP row and a generated/TestClaim dissolution trigger, satisfying the P5 receipt gate.
| environment: environment, | ||
| runtime: runtime | ||
| ) | ||
| }, |
There was a problem hiding this comment.
Invariant violation: BLOCKING: eval_runtime_node now threads V4EvaluatorRuntime beside a separate InterpretationAlgebra even though the runtime bundle also owns interpretation, allowing divergent behavior authorities in violation of P2 single authority.
|
Addressed briansrls/codex blocking review at 2026-05-24T04:48:31Z on current head f5206ba.
Also replied to the stale EvalProgress thread: current code has no processed_children field and carries the inline 🟢 classification on EvalProgress. Local verification: strict_deprose_dag --check, full v4 compile, scripts/check-v4-host-eval-receipt.py, and v4_test_bootstrap_infra_closeout_test all pass. — sent from merry-moth-781 |
Consolidates session/deep-bear-704 into consolidated/correctness-sweep.
AI-5 InferredFacts illegal-state dissolution:
- src/v4/compiler/04_infer.dag: InferredFacts restructured from
{resolved_type, inhabits, descent, canonical} to {grounding: CanonicalGrounding,
descent}; new gate fn canonical_grounding_admits_infer_facts; new accessors
inferred_facts_resolved_type/algebra_ref/canonical_witness/descent;
inferred_facts_from_grounding returns Outcome<InferredFacts>
- src/v4/std/constraints.dag: CanonicalGrounding as sole production path
AI-7 TestClaimCacheKey restructuring:
- src/v4/compiler/05_eval.dag: TestClaimCacheKey<T> carries hash_staging:
TestClaimCacheKeyStagingPlaceholder; import non_empty from v4.std.algebra
AI-13 SurfaceSugarKind scaffold marker upgrades:
- src/v4/compiler/03_normalize.dag, 00_compile.dag: updated scaffold markers
AI-14 LexPattern/GrammarExpr parallel ASTs:
- src/v4/compiler/01_tokenize.dag: scaffold comments updated to HEAD standard
AI-15/R1-2 translate source gap, R1-3 constraints singleton-MVP,
R1-4 Lens apply_lens stub, R1-5 eval loop:
- src/v4/compiler/06_translate.dag, 02_parse.dag: updates
- src/v4/test/claim/lens_common/infer_fixture.dag: removes algebra_witness_symbol
and canonical_evidence_symbol params; adds claim_canonical_grounding,
claim_inferred_facts_witness, claim_inferred_facts_from_nodes
Conflict resolution: eval conflicts resolved in favour of HEAD (T-22 Wave 2
#3611 is more complete); 01_tokenize.dag comment conflicts took HEAD's dissolution
markers; 04_infer.dag took branch's explanatory comment for InferredFacts shape.
Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com>
…iler pipeline correctness (#3636) * squash-merge PR #3557: Generative TestClaim categories lane Consolidates session/quiet-moth-603 into consolidated/correctness-sweep. Changes from PR #3557: - src/v4/lens/testgen.dag: add AlgebraLawCase type + algebra_law_manual_claim_case helper, testgen_emit_algebra_law_claim, add algebra_law_subject_for_manual_anchor (subset not already on main), add Generator.kind field - src/v4/test/claim/generated/algebra_law_conformance.dag: new generated corpus of Nat algebra law TestClaims (law_nat_add_left_identity, add_associativity, mul_annihilator) - src/v4/test/claim/generated/testgen_category_wishlist.dag: new dispatch ledger (3 pending + 4 dispatched non-tautological generator categories; TestgenOracleBasis type, dissolve-on-arrival) - docs/design-testgen-generative-categories.md: design doc for non-tautological generator categories - src/v4/std/verification.dag: add test_claim_coproduct_variant function - src/v3/compiler/tests/integration/v4_lens_testgen_dag_smoke_test.rs: expanded smoke receipts - src/v3/compiler/tests/integration/v4_test_bootstrap_infra_closeout_test.rs: new assertions for wishlist + algebra law case helpers - src/v4/TASKS.md: T-19 follow-up task entries - scripts/check_t19_testgen_activation.py: testgen activation check script - INVARIANTS.md: updated smoke-test receipt row for testgen - scripts/v4-mvp1-e2e-gate.sh: cargo run exit-status fix Conflict resolution: DiagnosticExhaustiveness variant shape conflict resolved in favour of HEAD (omitted_variant: TestClaimCoproductVariant from T-19 #3561). Branch's DiagnosticExhaustivenessSubject type removed; coproduct_exhaustiveness.dag and testgen_category_wishlist.dag updated to use HEAD's omitted_variant shape. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * squash-merge PR #3587: compiler pipeline correctness sweep Consolidates session/deep-bear-704 into consolidated/correctness-sweep. AI-5 InferredFacts illegal-state dissolution: - src/v4/compiler/04_infer.dag: InferredFacts restructured from {resolved_type, inhabits, descent, canonical} to {grounding: CanonicalGrounding, descent}; new gate fn canonical_grounding_admits_infer_facts; new accessors inferred_facts_resolved_type/algebra_ref/canonical_witness/descent; inferred_facts_from_grounding returns Outcome<InferredFacts> - src/v4/std/constraints.dag: CanonicalGrounding as sole production path AI-7 TestClaimCacheKey restructuring: - src/v4/compiler/05_eval.dag: TestClaimCacheKey<T> carries hash_staging: TestClaimCacheKeyStagingPlaceholder; import non_empty from v4.std.algebra AI-13 SurfaceSugarKind scaffold marker upgrades: - src/v4/compiler/03_normalize.dag, 00_compile.dag: updated scaffold markers AI-14 LexPattern/GrammarExpr parallel ASTs: - src/v4/compiler/01_tokenize.dag: scaffold comments updated to HEAD standard AI-15/R1-2 translate source gap, R1-3 constraints singleton-MVP, R1-4 Lens apply_lens stub, R1-5 eval loop: - src/v4/compiler/06_translate.dag, 02_parse.dag: updates - src/v4/test/claim/lens_common/infer_fixture.dag: removes algebra_witness_symbol and canonical_evidence_symbol params; adds claim_canonical_grounding, claim_inferred_facts_witness, claim_inferred_facts_from_nodes Conflict resolution: eval conflicts resolved in favour of HEAD (T-22 Wave 2 #3611 is more complete); 01_tokenize.dag comment conflicts took HEAD's dissolution markers; 04_infer.dag took branch's explanatory comment for InferredFacts shape. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: remove unused non_empty import from 05_eval.dag * fix: restore coproduct_exhaustiveness_missing_variant check (revert stale DiagnosticExhaustivenessSubject strings) Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: drop stale t19_ prefix from wishlist check needle (symbol renamed in HEAD design) * fix: update coproduct_exhaustiveness check needles to omitted_variant design * fix: update 05_eval.dag to new InferredFacts API; drop t19_ prefix from algebra_law_anchor_mismatch - Replace dissolved inferred_facts_resolved_type_matches/inhabitance_well_grounded/canonical_well_grounded calls in eval_runtime_value_acceptance_witness with inferred_facts_resolved_type equality check and canonical_grounding_admits_infer_facts (new 04_infer.dag API) - Declare algebra_law_anchor_mismatch symbol and replace undefined t19_algebra_law_anchor_mismatch reference in testgen.dag Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: enforce InferredFactsEntry node==grounding.node invariant; add T-19 AlgebraLaw receipt to TASKS.md Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PM May 22 * fix: add facts.grounding.node == node guard in inferred_facts_for_eval Eval consumption point must verify the map hit is for the correct node. `canonical_grounding_admits_infer_facts` only checks grounding internal consistency; it does not guard against a map returning facts whose grounding.node diverges from the lookup key. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: add P5 receipt for T-19 AlgebraLaw expansion in INVARIANTS.md SG-0 table Per INVARIANTS.md P5 Mechanism (b): expanded hand-Rust under src/v3/ requires a checkable receipt. The AlgebraLaw Nat corpus assertions in v4_test_bootstrap_infra_closeout_test.rs land in this PR; the deferral lane is TASKS.md §T-19 (algebra_law_conformance.dag corpus) + ROADMAP.md Nine lanes row T-PB-B. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: make facts_map_from_entries fail-closed via Outcome Previously, facts_map_from_entries silently dropped InferredFactsEntry items where entry.node != entry.facts.grounding.node. This compensated for the free constructibility of InferredFactsEntry (P2 boundary gap) without surfacing the violation diagnostically. Now: the fold rejects with infer_canonical_grounding_incoherent_diagnostic on any invariant-violating entry, and infer() threads the Outcome. admitted_inferred_facts_entry remains the primary enforcement point; facts_map_from_entries is the secondary fail-closed gate that makes invariant violations visible as Rejected rather than silent drops. Addresses codex RC on bc16ae7: InferredFactsEntry remained freely constructible and map construction compensated with a nondiagnostic filter. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: replace bare [] with typed helper in facts_map_from_entries The v4 compiler cannot infer the element type of [] when it appears as a record field value inside Accepted { value: [], ... }. Introduce empty_inferred_facts_entry_list() -> List<InferredFactsEntry> (matching the existing empty_edge_list / empty_canonical_symbol_set pattern) and use it as the fold init. Fixes Lens-CI semantic compile failure on d1299ea. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: add P5 receipt for PR #3636 anchor-strip + AlgebraLaw subject helper guard in INVARIANTS.md - Updates Generator field name from t19_anchor to anchor in existing ratchet description - Appends PR #3636 same-file receipt: renamed tests, new kind/anchor assertions, assert_six_algebra_law_subject_paths_in_testgen, forbidden nat_algebra_law_subject_symbol_* checks, and generalized generator_field_ty / between helpers Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix: update stale T19-prefix type names in INVARIANTS.md testgen row - Rename test fn refs: t19_anchor_field_is_manual_key → anchor_field_is_claim_anchor_key, concept_projection_matches_claim_t19_anchor → _claim_anchor, generator_carries_claim_kind_and_classification → _classification_and_anchor - Update description: T19ManualAnchorKey → ManualAnchorKey, Generator.t19_anchor → Generator.anchor, T19ClaimAnchorKey → ClaimAnchorKey, TestClaim.t19_anchor → TestClaim.anchor, T19ManualClaimAnchor → ManualClaimAnchor, T19ManualAnchorAbsent → ManualAnchorAbsent, T19GeneratedClaimAnchor → GeneratedClaimAnchor - Update inline carrier description: Generator.t19_anchor: T19ClaimAnchorKey → Generator.anchor: ClaimAnchorKey Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PM May 22 * fix: strip stale T19 names from closeout + testgen INVARIANTS rows (cursor RC #17566) Line 374 (v4_test_bootstrap_infra_closeout_test.rs): update 7 test fn names (t19_testgen_concept_surface_stays_closed_and_classified → testgen_..., etc.) and 6 type names (T19ManualAnchorKey → ManualAnchorKey, TestClaim.t19_anchor → .anchor, t19_manual_claim_anchor → manual_claim_anchor, T19GeneratedCoproductExhaustiveness, T19GeneratedClaimAnchor, T19ClaimAnchorKey). Line 383 (v4_lens_testgen_dag_smoke_test.rs): simplify PR #3636 receipt section to remove all from→to rename references; receipt now describes current ratchet state only. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * fix(04_infer): adapt merge-conflict resolution to our InferredFacts struct layout The merge of main (PR #3646) erroneously took code that references `facts.inhabits.algebra` and `inferred_facts_canonical_grounding_coherent`, both of which belong to main's refactored InferredFacts struct. Our branch carries `InferredFacts { grounding, descent }`, so the guards must use `inferred_facts_algebra_ref(facts: facts).algebra` and `canonical_grounding_admits_infer_facts(grounding: facts.grounding)` instead. Co-Authored-By: Claude Sonnet 4.6 <noreply@anthropic.com> * WIP: PM May 22 * WIP: PM May 22 * WIP: PM May 22 * WIP: PM May 22 --------- Co-authored-by: Claude Sonnet 4.6 <noreply@anthropic.com>
Summary
Dissolves the twelve
05_eval.dagT-22 Wave 2 gated scaffolds by wiring eval through the runtime interpretation path: runtime-value projection foreval_node, realized Branch/Bind resumption, runtime control terminalization, acceptance witness modeling, behavior dispatch, progress carrier tracking, runtime edge-role handling, and parameterized Outcome equality consumption.LB-T22-3213 remains intentionally yellow outside
05_eval.dag:pipeline_rejections.dagkeeps the typed-input bridge and cache-hash placeholders pending the real B1content_hashsubstrate. This PR does not fabricate hash authority.Test plan
python3 scripts/strict_deprose_dag.py --check— passed./opt/rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/cargo run -p v2-compiler --bin v2-compiler -- compile --source-root src/v4 --output-dir /tmp/gunbc-v4-compile-t22 --target rust— passed, 0 diagnostics./opt/rustup/toolchains/1.93.0-aarch64-unknown-linux-gnu/bin/cargo test -p v3-compiler --test integration v4_test_bootstrap_infra_closeout_test -- --quiet— passed, 12 tests.Claim receipts exercised:
v4_test_bootstrap_infra_closeout_testcoverage for the T-22 eval closeout surface, including the updatedeval_noderuntime-value-to-Node projection expectation.