Repository navigation
docs(evaluator): add E2 descent proof consumer brief #1854
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Merged
Merged
Changes from all commits
Commits
Show all changes
4 commits
Select commit
Hold shift + click to select a range
ea203dc
docs: add E2 descent proof consumer brief
briansrls ba32bd1
Merge remote-tracking branch 'origin/main' into docs/e2-descent-proof…
briansrls 9fcbfe0
Merge remote-tracking branch 'origin/main' into docs/e2-descent-proof…
briansrls 0e2b67b
docs: refresh EVAL-2 descent authority refs
briansrls File filter
Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
There are no files selected for viewing
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
| Original file line number | Diff line number | Diff line change |
|---|---|---|
| @@ -0,0 +1,125 @@ | ||
| # 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 EVAL-2 / E5 `LoopBound::Descent` residual closure. | ||
|
|
||
| **Dispatch trigger:** Substrate merges a proof authority with the shape: | ||
|
|
||
| ```text | ||
| descent_execution_proof( | ||
| dag: Dag, | ||
| cluster: ClusterId, | ||
| measure: PortId, | ||
| ) -> Result<DescentExecutionProof, DescentResidual> | ||
| ``` | ||
|
|
||
| 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. | ||
|
|
||
| ## Live Source Authority | ||
|
|
||
| - [`r3-pr-e5-loopbound-descent-stop-packet.md`](r3-pr-e5-loopbound-descent-stop-packet.md) | ||
| 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<DescentExecutionProof, DescentResidual>` | ||
| 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`. | ||
| - `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. | ||
Oops, something went wrong.
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
BLOCKING: The Source Authority section names missing docs (
r3-pr-e5-loopbound-descent-stop-packet.mdand../r3-program-plan.md), so the worker would dispatch from unverifiable authorities rather than live R3 evaluator/readiness docs (INVARIANTS P1).