Evaluator E2 Descent termination contract consumer (post-Substrate descent_execution_proof)

[briansrls]

Opened from session-dashboard for session wise-boar-420.

[briansrls]

Review metadata

• Provider / model: codex / unknown
• Commit: 0ab7fd07 · Trigger: schedule
• Thinking: 220s wall

---

BLOCKING (1)

Root Cause

• src/v3/compiler/src/lib.rs DescentExecutionProof.per_path is a string-keyed parallel path list disconnected from Cluster.intra_cluster_calls → key proof entries by the authoritative call/transform handle or verify exact cluster-call coverage from the Dag before executing.

⚠️ The descent consumer needs to reject partial or unrelated proof maps before this can safely land.

[briansrls]

BLOCKING: discharge_descent_obligation accepts any non-empty per_path map instead of proving coverage against the authoritative Cluster.intra_cluster_calls, so incomplete descent evidence can execute despite the Decidability/Facts-Flow-Forward termination contract.

[briansrls]

Mgr review (cannot self-approve via GitHub since worker pushes under same git author). Marked ready-for-review per dashboard escalation; worker left in draft after CI green.

Diff inspection:

• Rust evaluator-side mirrors of StrictEvidence / NonStrictEvidence / DescentResidual / DescentExecutionProof with explicit comment that the .dag carrier in src/v3/std/termination.dag is the authority and the mirror exists only because the eager Rust evaluator cannot yet call generated std block bodies. Matches the v3-staging shim pattern and the brief's "signature drift: bare Dag per v3 std .dag convention" note.
• descent_execution_proof stub returns Err(DescentResidual::EvidenceIncomplete) — matches carrier semantics on main ("Body fail-closed: Err { value: EvidenceIncomplete } until producer wires per-path Strict aggregation"). Production behavior is unchanged from the prior STOP; success path reachable only via test seam.
• eval_loop consumes the proof at the descent entry point via eval_loop_with_descent_execution_proof; Err(_) preserves the existing EvalError::LoopBoundDescentResidual STOP family (no decomposition needed). discharge_descent_obligation checks cluster + port + per-path coverage of all intra_cluster_calls.
• Tests cover all 4 shapes the brief required plus a bonus per-path coverage check:
  • eval_loop_descent_bound_with_strict_per_path_proof_succeeds (success)
  • eval_loop_descent_bound_evidence_incomplete_fails_closed
  • eval_loop_descent_bound_evidence_unknown_non_increasing_fails_closed
  • eval_loop_descent_bound_evidence_unknown_descent_unknown_fails_closed
  • eval_loop_descent_bound_incomplete_per_path_coverage_fails_closed (bonus defensive shape)
• One observation worth surfacing (not blocking): on the success path, the loop body executes exactly once (count = 1). The brief did not specify iteration count semantics for descent; single-iteration is the simplest honest interpretation (proof-discharge → body once). If the intent is body-to-convergence under per-path Strict descent, that's a follow-on. Worth a comment in the implementation to mark the dissolution target.
• All 4 CI checks SUCCESS per dashboard digest.

No BLOCKING comments. Will merge under Mgr standing-authority after green CI + 30-min sit per Director-ratified policy. The single-iteration observation above is worth a one-line dissolution-target comment in the code if convenient; otherwise non-blocking.

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 7630dbe4 · Trigger: schedule
• Comparison: origin/main @ 118badd9 ... review/pr-2190-7630dbe4 @ 7630dbe4
• Thinking: 67s wall

---

Findings

None that rise to a documented invariant violation with diff evidence. The change keeps substrate authority explicit (mirrors are labeled as such in lib.rs), leaves the live descent_execution_proof path fail-closed via EvidenceIncomplete (lib.rs lines 122–127), and adds focused unit tests around injectable eval_loop_with_descent_execution_proof (lib.rs test section).

Verdict

APPROVE — The diff wires the evaluator to the termination proof shape, checks cluster/port and per–intra-cluster-call map coverage before running the body once, and stays aligned with the stub semantics already declared in src/v3/std/termination.dag. No P2 duplicate-authority issue: the .dag types remain the authority; the Rust enums are an documented mirror for the non-generated evaluator path.

Exploratory observations (optional)

• EvalError granularity: proof_fn errors are collapsed with map_err(|_| …) at lib.rs:425–431, so EvidenceUnknown(…) vs EvidenceIncomplete is not visible on the public EvalError surface. That may be intentional for E5; if callers ever need DB-1-style differentiated diagnostics, the residual would need to be carried on EvalError rather than dropped at the boundary.
• docs/modeling-discipline.md §4: NonStrictEvidence / DescentResidual use mirror doc comments but not the explicit 🟢/🟡/🔴 checkpoint style; classification already lives on termination.dag, so this is polish rather than substance.

[briansrls]

Verified against current head dc7f220. No code change needed for this approve review: the live descent_execution_proof bridge still fails closed with EvidenceIncomplete, residuals intentionally collapse into the existing LoopBoundDescentResidual STOP family for this E2 slice, and cluster/port plus per-intra-cluster-call coverage checks are present before body execution.\n\n— sent from wise-boar-420

[briansrls]

Review metadata

• Provider / model: cursor / composer-2
• Commit: 44f4d62b · Trigger: schedule
• Comparison: origin/main @ 4ac0cfd3 ... review/pr-2190-44f4d62b @ 44f4d62b
• Thinking: 31s wall

---

Findings

• src/v3/compiler/src/lib.rs:393-396 — Rustdoc on eval_loop says LoopBound::Descent “consumes the substrate descent_execution_proof carrier” and then runs the body after the obligation is discharged. In the same diff, descent_execution_proof (122-127) ignores the dag and always returns Err(DescentResidual::EvidenceIncomplete), so the default public path never reads substrate proof data and never discharges the bound. That reads as aspirational / live-state drift relative to INVARIANTS.md (“Documentation Describes Live State” under P1-related rules) and the honesty bar in CODING.md (“Interfaces are precise contracts”). NON-BLOCKING: tighten rustdoc to describe today’s fail-closed stub and name the hook as the future substrate-backed producer, or split “intended contract” vs “current behavior.”

Verdict

APPROVE_WITH_COMMENTS — The wiring is coherent: single-authority comments for the .dag mirrors (90-93, 113-115), fail-closed descent (425-431, 452-474), injectable proof_fn for tests (412-417), and focused regression tests replacing the old blanket descent failure. The only concrete rubric issue in the diff is the overstated eval_loop documentation versus the stub producer.

Exploratory (optional)

• When a real proof producer lands, descent_proof_path_key (477-478) must stay aligned with whatever the substrate uses for per_path keys; today it’s TransformRef’s node id as decimal text — worth confirming against std.termination when that boundary is implemented.

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 44f4d62b · Trigger: manual
• Comparison: main @ 4ac0cfd3 ... session/wise-boar-420 @ 5cdb3cb9
• Conversation: View conversation

---

1. Story of the diff

This PR keeps the eager Rust evaluator’s production descent-loop path fail-closed while carving out the consumer shape for a future generated std.termination::descent_execution_proof provider. It adds Rust-side mirror carriers for strict evidence, non-strict evidence, residuals, and the execution proof, explicitly naming the .dag carrier as the authority and the Rust copy as an evaluator bridge until generated std block bodies are callable (src/v3/compiler/src/lib.rs:90, src/v3/compiler/src/lib.rs:92, src/v3/compiler/src/lib.rs:93). eval_loop now delegates to an injected proof-function helper: cardinality loops still decode a count, while descent loops request a proof, discharge cluster/measure/per-path coverage, then execute the current E2-scoped single descent step (src/v3/compiler/src/lib.rs:403, src/v3/compiler/src/lib.rs:425, src/v3/compiler/src/lib.rs:432, src/v3/compiler/src/lib.rs:433). The tests move from one “descent residual” assertion to a focused constructed-loop fixture plus proof-success and fail-closed residual cases (src/v3/compiler/src/lib.rs:949, src/v3/compiler/src/lib.rs:2254, src/v3/compiler/src/lib.rs:2294, src/v3/compiler/src/lib.rs:2330).

2. Invariant categories

1. LAYER MODEL (substrate vs implementation). Compliant — the diff does not alter dag.rs or .dag substrate declarations; it adds an evaluator-side consumer mirror, and the mirror’s comment names the .dag carrier as authority (src/v3/compiler/src/lib.rs:92) while the default provider remains fail-closed with Err(DescentResidual::EvidenceIncomplete) (src/v3/compiler/src/lib.rs:127).
2. INVARIANTS.md + modeling-discipline.md. Compliant — fail-closed is preserved: missing/non-strict proof output maps to EvalError::LoopBoundDescentResidual (src/v3/compiler/src/lib.rs:425, src/v3/compiler/src/lib.rs:426), and accepted proof must match cluster, measure port, and every intra-cluster call path before returning Ok(()) (src/v3/compiler/src/lib.rs:459, src/v3/compiler/src/lib.rs:460, src/v3/compiler/src/lib.rs:461, src/v3/compiler/src/lib.rs:464).
3. CODING.md. Finding — typed handles over raw ids / clear interfaces. src/v3/compiler/src/lib.rs:119: pub per_path: HashMap<String, StrictEvidence>, makes proof-path identity a raw string, and src/v3/compiler/src/lib.rs:478: transform.node_id().raw().to_string() defines the accepted format from a raw node id. That leaves the proof contract dependent on string formatting rather than a typed path witness such as TransformRef, NodeId, or a private-constructor DescentProofPathKey. This is non-blocking for this PR because the production provider still returns EvidenceIncomplete (src/v3/compiler/src/lib.rs:127), but it should be tightened before any real producer can return Ok(DescentExecutionProof).
4. TESTING.md. Compliant — tests are hermetic and behavior-focused: descent_loop_fixture constructs the minimal Dag shape under test (src/v3/compiler/src/lib.rs:949), the success case asserts strict per-path proof discharge (src/v3/compiler/src/lib.rs:2254), and separate tests cover incomplete path coverage, incomplete evidence, non-increasing evidence, and unknown descent evidence (src/v3/compiler/src/lib.rs:2294, src/v3/compiler/src/lib.rs:2330, src/v3/compiler/src/lib.rs:2360, src/v3/compiler/src/lib.rs:2394).
5. LOCKED DESIGN DECISIONS. N/A — the diff does not modify locked design docs or introduce a visible divergence from a locked decision; it consumes the existing descent-proof concept from implementation code only.
6. TRACKED vs UNTRACKED DEBT. Compliant — the Rust mirror is documented as a bridge to the .dag authority (src/v3/compiler/src/lib.rs:90, src/v3/compiler/src/lib.rs:92), bounded to the eager evaluator’s current inability to call generated std block bodies (src/v3/compiler/src/lib.rs:93), and the temporary runtime scope is explicitly named as one descent step until the follow-on descent producer/runtime lands (src/v3/compiler/src/lib.rs:433, src/v3/compiler/src/lib.rs:435).

3. Verdict

APPROVE_WITH_COMMENTS

The diff preserves fail-closed production behavior and adds focused tests for the new consumer seam. The one cleanup I would make before this grows a real proof producer is to replace the raw String proof-path key with a typed identity carrier so the termination proof contract is enforced by the API rather than by node-id string convention.

[briansrls]

Verified against current head 5cdb3cb and src/v3/std/termination.dag. The raw String observation is accurate, but I am not changing it in this PR because the authoritative carrier shipped as DescentExecutionProof.per_path: Map<String, StrictEvidence> and its comment explicitly names String keys as the bootstrap bridge until branch identifiers gain a structural carrier. The Rust evaluator mirror is intentionally shape-compatible with that carrier; replacing it with TransformRef/NodeId/private key here would make the consumer no longer consume #2147 as shipped.\n\nThe consumer does contain the string convention behind descent_proof_path_key and remains fail-closed until a real producer exists. Tightening the carrier to a typed path identity should happen with the substrate producer/carrier follow-on, not in this consumer-only PR.\n\n— sent from wise-boar-420

[briansrls]

Review metadata

• Provider / model: claude / claude-opus-4-7
• Commit: 5cdb3cb9 · Trigger: schedule
• Comparison: origin/main @ 4ac0cfd3 ... review/pr-2190-5cdb3cb9 @ 5cdb3cb9
• Thinking: 35s wall

---

Findings

• None blocking. The mirror types at src/v3/compiler/src/lib.rs:90-118 (StrictEvidence/NonStrictEvidence/DescentResidual/DescentExecutionProof) are flagged as parallel representations of std.termination::*, but the doc comment names the dissolution trigger ("until the eager Rust evaluator can call generated std block bodies"), so this reads as a tracked bridge rather than a duplication violation.
• Non-blocking observation: descent_proof_path_key (lib.rs:478) keys the per-path map by raw NodeId of the call's transform. The std type is named per_path, suggesting paths-through-cluster, not call sites. Coverage check at lib.rs:466 only verifies each intra_cluster_call.transform has some StrictEvidence entry — there's no check that the proof contains only known calls, and no check that StrictEvidence::Strict is actually the value (the enum is single-variant today, so this is moot, but if NonStrictEvidence ever migrates in, the contains_key check would silently accept it). Worth tightening when the producer lands.
• Non-blocking: the success branch hard-codes count = 1 (lib.rs:435) with the comment "Body-to-convergence semantics belong to the follow-on descent producer/runtime." Documented and bounded — fine as scaffold, but the test eval_loop_descent_bound_with_strict_per_path_proof_succeeds asserts Value::Int(7) purely because of that 1-step shortcut; a future producer change will need to update that assertion. Not a defect.

Verdict

APPROVE — narrowly scoped E2 consumer slice. Default hook is fail-closed, all four residual variants have regression tests, and the Rust mirror is explicitly flagged as a temporary consumer with a named dissolution trigger. No invariant violations grounded in the diff.

[briansrls]

Verified against current head 5cdb3cb. No code change needed for this approve review: the mirror remains documented as an evaluator bridge to the .dag authority, descent_proof_path_key is intentionally aligned with the current Map<String, StrictEvidence> carrier, and the one-step descent behavior is explicitly documented as E2 consumer scope pending follow-on producer/runtime semantics.\n\n— sent from wise-boar-420

[briansrls]

Review metadata

• Provider / model: openai-pro / gpt-5-5-pro
• Commit: 5cdb3cb9 · Trigger: manual
• Conversation: View conversation

---

1. Story of the diff

This PR changes eager loop evaluation from “all descent bounds are residual” into “descent bounds may discharge through an injected termination-proof consumer.” It adds local Rust mirrors for std.termination proof/result carriers, keeps the live default hook fail-closed with Err(DescentResidual::EvidenceIncomplete) at src/v3/compiler/src/lib.rs:122-127, and routes eval_loop through eval_loop_with_descent_execution_proof at src/v3/compiler/src/lib.rs:405-410. For LoopBound::Descent, the evaluator calls the proof hook, checks that the proof matches the loop’s cluster/measure and covers every intra-cluster call at src/v3/compiler/src/lib.rs:461-467, then executes the loop body once as the current E2 consumer scope at src/v3/compiler/src/lib.rs:435-438. The tests replace the old single “descent fails closed” case with a minimal descent-loop fixture and focused cases for strict proof success, missing per-path coverage, incomplete proof, and both non-strict evidence residuals.

2. Invariant categories

1. LAYER MODEL (substrate vs implementation).

Compliant — this does not add or mutate Dag substrate declarations; it is an implementation-side evaluator consumer over existing substrate handles (ClusterId is imported at src/v3/compiler/src/lib.rs:60, and the injected proof hook consumes ClusterId/PortId at src/v3/compiler/src/lib.rs:419). The comments also keep .dag as the named authority: src/v3/compiler/src/lib.rs:92: /// The \.dag carrier is the authority; this mirror exists only because.

1. INVARIANTS.md + modeling-discipline.md.

Compliant — fail-closed is handled directly: the live proof hook returns Err(DescentResidual::EvidenceIncomplete) at src/v3/compiler/src/lib.rs:127, hook failures map to EvalError::LoopBoundDescentResidual at src/v3/compiler/src/lib.rs:427-433, and a proof only discharges when cluster, measure, and all intra-cluster paths match at src/v3/compiler/src/lib.rs:461-467. That is the right shape for “consumer exists, producer not live yet.”

1. CODING.md.

Finding (NON-BLOCKING) — src/v3/compiler/src/lib.rs:119: pub per_path: HashMap<String, StrictEvidence>, plus src/v3/compiler/src/lib.rs:480: transform.node_id().raw().to_string() makes stringified raw node IDs the path-identity contract for this proof consumer. That diverges from the typed-handle discipline: the cluster already contains typed transform refs, but the proof boundary now requires future producers to reproduce this exact string serialization. Prefer a typed key in the Rust mirror, such as TransformRef, NodeId, or a small DescentProofPathKey newtype with one conversion boundary if the generated .dag carrier must remain string-shaped.

1. TESTING.md.

Compliant — the tests are behavior-driven and focused: the success case is named eval_loop_descent_bound_with_strict_per_path_proof_succeeds at src/v3/compiler/src/lib.rs:2256, missing coverage is isolated at src/v3/compiler/src/lib.rs:2296, incomplete evidence at src/v3/compiler/src/lib.rs:2332, and the two non-strict residual variants at src/v3/compiler/src/lib.rs:2362 and src/v3/compiler/src/lib.rs:2396. The shared helper constructs a minimal Dag shape directly at src/v3/compiler/src/lib.rs:951-989 rather than compiling a broad source fixture.

1. LOCKED DESIGN DECISIONS.

N/A — the diff does not edit thesis/design docs or alter a line marked locked; it implements an evaluator hook against existing termination/descent substrate concepts.

1. TRACKED vs UNTRACKED DEBT.

Compliant — the temporary Rust mirror is documented, bounded, and given a dissolution condition: the mirror exists because the eager Rust evaluator cannot yet call generated std block bodies at src/v3/compiler/src/lib.rs:92-93, and the live hook remains fail-closed until the substrate producer emits per-path strict evidence at src/v3/compiler/src/lib.rs:395-397. I would still fold the string-key concern from CODING into that same bridge cleanup so the eventual generated consumer does not inherit a raw-ID string convention.

3. Verdict

APPROVE_WITH_COMMENTS

The termination-proof consumer shape is fail-closed, scoped, and well-tested. The only issue I see is non-blocking implementation hygiene around HashMap<String, ...>/raw node ID serialization as a proof-path identity boundary; it is worth tightening before the producer lands, but it does not make this consumer unsafe on its own.