From ea203dcac0a87e2c89f0907aaba069e4ca79f2da Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 18:51:12 +0000 Subject: [PATCH 1/2] docs: add E2 descent proof consumer brief --- .../r3-pr-e2-descent-proof-consumer-worker.md | 118 ++++++++++++++++++ 1 file changed, 118 insertions(+) create mode 100644 docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md diff --git a/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md b/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md new file mode 100644 index 00000000000..9d72b242db6 --- /dev/null +++ b/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md @@ -0,0 +1,118 @@ +# R3 PR-E E2 — Descent Execution Proof Consumer Worker + +**Status:** pre-authored worker brief. Do not dispatch until the substrate +`descent_execution_proof` carrier/query lands or Director/Substrate explicitly +names an equivalent authority. + +**Lane:** R3 Evaluator E5 residual closure / E2 consumer wiring. + +**Dispatch trigger:** Substrate merges a proof authority with the shape: + +```text +descent_execution_proof( + dag: Dag, + cluster: ClusterId, + measure: PortId, +) -> Result +``` + +or an explicitly ratified equivalent that lets the evaluator distinguish +certified `LoopBound::Descent` execution from missing, unknown, incomplete, or +non-strict evidence without inferring proof facts locally. + +## Source Authority + +- [`r3-pr-e5-loopbound-descent-stop-packet.md`](r3-pr-e5-loopbound-descent-stop-packet.md) + is the active STOP receipt. +- [`docs/r3-program-plan.md`](../r3-program-plan.md) EVAL-2 names the resume + contract and fail-closed residual classes. +- `src/v3/compiler/src/lib.rs` currently returns + `EvalError::LoopBoundDescentResidual { node, cluster, measure }` from + `eval_loop` for `LoopBound::Descent`. +- `src/v3/std/substrate.dag` owns the live + `LoopBound::Descent { cluster: ClusterId, measure: PortId }` shape plus the + cluster/member/call topology carriers. + +## Goal + +Replace the evaluator's unconditional `LoopBound::Descent` residual with a +narrow consumer of the substrate proof query: + +- certified descent loops execute through the existing loop evaluator path; +- uncertified descent loops continue to fail closed with a typed residual; +- the evaluator never computes, approximates, or repairs termination evidence. + +This is a consumer slice. The proof producer, evidence lattice, cluster +coverage, and per-call evidence broadening remain Substrate-owned. + +## Required Implementation Shape + +In `eval_loop`, when `node.bound` is `LoopBound::Descent { cluster, measure }`: + +1. Call the substrate-owned proof query with the current `Dag`, `cluster`, and + `measure`. +2. If the query returns a certified proof token, execute the loop body using + the existing evaluator frame/accumulator discipline. Reuse the existing + cardinality-loop execution helpers where possible, but do not reinterpret + descent as `LoopBound::Cardinality`. +3. If the query returns a residual such as missing, unknown, incomplete, or + non-strict evidence, return a fail-closed `EvalError` carrying the existing + `node`, `cluster`, and `measure` context plus the proof residual if the + landed substrate type exposes one. +4. Preserve stack restoration behavior on success and failure. + +If the landed substrate API does not expose an executable bound/schedule for +the certified loop, STOP. The evaluator cannot invent an iteration count or +termination schedule from proof existence alone. + +## Hard Bars + +Do not: + +- widen `LoopBound`; +- add evaluator-local proof inference; +- call `per_call_descent_evidence` directly as a substitute for the proof + query unless Substrate explicitly makes it the proof query; +- reinterpret `Descent` as cardinality or default to zero/one iteration; +- add runner behavior or `TestPredicate` arms; +- change parser, lowerer, or substrate carriers; +- add a second termination-evidence mirror in evaluator code; +- collapse residual classes into string matching. + +Any of those needs a STOP back to Substrate/Director. + +## Acceptance + +The PR must include focused evaluator tests for: + +1. Certified descent proof executes the loop body and returns the expected + accumulator value. +2. Missing/unknown/incomplete/non-strict proof residuals fail closed without + executing the body. +3. The old unconditional `LoopBoundDescentResidual` behavior is replaced only + for certified proof tokens. +4. Stack/frame restoration remains correct after certified execution and after + residual failure. +5. The evaluator does not call any local proof-inference helper or evidence + side table directly unless that helper is the ratified substrate proof + authority. + +Validation should include the narrow evaluator test target that covers +`eval_loop` plus repository format/check commands required by touched files. + +## Non-Goals + +- Substrate proof carrier design. +- Per-call descent evidence broadening. +- Termination lens behavioral parity. +- TC3 producer/evaluation-step work. +- `LoopBound::Cardinality` refactors. +- Runner predicate changes. + +## Handoff Notes + +If the substrate authority lands under a different name than +`descent_execution_proof`, update this brief before dispatch with the exact +function/type names and residual variants. The dispatch decision should be +mechanical once the proof token gives the evaluator both permission and enough +execution information to run the descent loop without fabricating proof facts. From 0e2b67bcaf103f42e74e55de420a7835be20bc3d Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Wed, 6 May 2026 19:08:56 +0000 Subject: [PATCH 2/2] docs: refresh EVAL-2 descent authority refs --- .../r3-pr-e2-descent-proof-consumer-worker.md | 19 +++++++++++++------ 1 file changed, 13 insertions(+), 6 deletions(-) diff --git a/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md b/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md index 9d72b242db6..2b57028433d 100644 --- a/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md +++ b/docs/briefs/r3-pr-e2-descent-proof-consumer-worker.md @@ -1,10 +1,10 @@ -# R3 PR-E E2 — Descent Execution Proof Consumer Worker +# R3 Evaluator EVAL-2 — Descent Execution Proof Consumer Worker **Status:** pre-authored worker brief. Do not dispatch until the substrate `descent_execution_proof` carrier/query lands or Director/Substrate explicitly names an equivalent authority. -**Lane:** R3 Evaluator E5 residual closure / E2 consumer wiring. +**Lane:** R3 Evaluator EVAL-2 / E5 `LoopBound::Descent` residual closure. **Dispatch trigger:** Substrate merges a proof authority with the shape: @@ -20,12 +20,19 @@ or an explicitly ratified equivalent that lets the evaluator distinguish certified `LoopBound::Descent` execution from missing, unknown, incomplete, or non-strict evidence without inferring proof facts locally. -## Source Authority +## Live Source Authority - [`r3-pr-e5-loopbound-descent-stop-packet.md`](r3-pr-e5-loopbound-descent-stop-packet.md) - is the active STOP receipt. -- [`docs/r3-program-plan.md`](../r3-program-plan.md) EVAL-2 names the resume - contract and fail-closed residual classes. + is the active E5 STOP receipt for `LoopBound::Descent`. +- [`r3-pr-e5-loop-readiness-audit.md`](r3-pr-e5-loop-readiness-audit.md) + records cardinality loop execution as live and keeps Descent outside the + cardinality slice. +- [`docs/r3-program-plan.md`](../r3-program-plan.md) EVAL-2 and + Q-EVAL-Descent-Termination-Contract name the live resume contract: + Substrate lands + `descent_execution_proof(&Dag, ClusterId, PortId) -> Result` + with `Missing | Unknown | Incomplete | NonStrict` fail-closed residuals; + the evaluator consumes the proof token only. - `src/v3/compiler/src/lib.rs` currently returns `EvalError::LoopBoundDescentResidual { node, cluster, measure }` from `eval_loop` for `LoopBound::Descent`.