Repository navigation
docs(evaluator): PR-B.0 body-evaluator eager baseline (closed-with-residuals) - #1268
Conversation
…siduals) Authors the docs-only PR-B body-evaluator design slice. Names the live prerequisites (PR-A.1 Value, PR-A.2 EvalFrame/EvalStateStack, PR-A.3 audit), the still-needed prerequisite carriers (EvalStrategy / InputEvaluationOrder / EvalStateKey / EvalMemoKey from PR-A.3 implementation), and locks the first implementation target as a deterministic eager body evaluator over bounded .dag bodies — no lazy / normal-order, no TC2 proof, no witness construction, no closures-with-captures. R3 residual reason is named with three causal gaps (carrier absence, missing non-eager rules, witness surface unauthored), not a schedule excuse. Updates the manager brief PR-B row to point at this brief and note that the witness half remains unauthored. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Reviewed #1268. This matches the dispatch shape: docs-only PR-B.0, names live PR-A.1/#1243 and PR-A.2/#1255 carriers, keeps PR-A.3 implementation carriers as the PR-B.1 gate, and does not add Rust execution, substrate, fixtures, lazy strategy, TC2 strengthening, or witness construction. The manager-row split of PR-B into body-evaluator half now and witness-construction half deferred is acceptable for closed-with-residuals accounting. It makes the residual explicit instead of implying witness construction is silently done. Please mark ready so CI/reviews run. No blocking changes from me. |
|
Review metadata
FindingsNone. The change is documentation only: it updates the PR-B row in VerdictAPPROVE — Narrow, honest docs lock for PR-B.0; no invariant or testing-discipline conflict visible in the diff. |
|
Review metadata
1. Story of the diffThis PR turns PR-B from an unauthored evaluator lane into a split, explicitly bounded body-evaluator design slice plus a still-unauthored witness slice. The manager row now says PR-B covers “Body evaluator + witness construction surface” and points at The load-bearing move is the residual boundary. The brief permits only deterministic eager evaluation over bounded 2. Invariant categories
Compliant — this is a docs-only design slice, and it explicitly says “No Rust execution code lands in this brief; no new substrate carriers are declared here” (
Compliant — fail-closed and decidability are handled as design constraints, not implied behavior: non-eager strategy inhabitants become diagnostics (
Compliant — no Rust implementation is introduced, so there are no method/object-style deviations to review. The future implementation shape is nevertheless described as a precise input/output boundary:
Compliant — no tests are added, and that is appropriate for this specific PR because the acceptance gate says this brief is docs-only with “no new test fixtures” (
Compliant — the brief references locked/existing decisions without changing them: it consumes the PB runtime interpreter authority (
Compliant — the residuals are documented, bounded, and have named dissolution triggers. Documentation: the R3 residual section names the causal gaps ( 3. VerdictAPPROVE — I found no blocking or non-blocking findings tied to the changed lines. The PR is careful about not landing substrate or Rust execution prematurely, and the residual debt is explicitly bounded with a concrete closure sequence. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
d1cf7e39· Trigger:schedule - Thinking:
150s wall
BLOCKING (1)
Root Cause
docs/briefs/r2-pr-b-body-evaluator-eager-baseline.mdBody-evaluator loop semantics are specified against a count-only view ofLoopBoundinstead of the actual two-variant substrate shape → split the rule byCardinalityvsDescent, or explicitly makeDescenta fail-closed named residual with its own trigger.
| Scope is bounded by construction: | ||
|
|
||
| 1. **Inputs.** A `NodeId` for the body, an initial `EvalStateStack` containing | ||
| one `EvalFrame` with the parameter bindings the caller supplied at the |
This comment was marked as resolved.
This comment was marked as resolved.
Sorry, something went wrong.
|
The scheduled blocking review is valid. Please fix the PR-B.0 brief before merge: the loop rule currently reads too much like PR-B.1 executes only a count-style Suggested wording change in
Given closed-with-residuals posture, I recommend the narrower fix: PR-B.1 supports only the bounded cardinality path initially and fails closed for After that wording fix, the rest of the PR still looks good from my side. |
LoopBound has two variants per src/v3/std/substrate.dag:
Cardinality { count: PortId } | Descent { cluster: ClusterId }
The previous wording treated LoopBound as cardinality-only and silently
dropped the descent proof. Per Facts-Flow-Forward and the substrate
authority, PR-B.1 must dispatch on both variants: Cardinality reads the
count port; Descent consults std.termination DescentEvidence for the
proved descent cluster. DescentUnknown is a fail-closed Diagnostic.
Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
…sed residual Per parent guidance: PR-B.1 should support Cardinality only and fail-closed on Descent loops with a named dissolution trigger (separate descent-execution slice consuming std.termination DescentEvidence). Avoids silently broadening PR-B.1 to a descent evaluator. Descent now also explicitly listed in the R3 residual line. Co-Authored-By: Claude Opus 4.7 (1M context) <noreply@anthropic.com>
|
Pushed narrowing per your suggestion in 09d4037 (replaces the earlier f2e6a4a fix that wired Current Loop rule:
R3 residual line also updated to list — sent from merry-heron-351 |
|
Review metadata
Verdict: APPROVE Docs-only diff, narrowly scoped to the PR-B.0 body-evaluator design brief and manager cross-reference. I found no concrete violations of the pinned invariants, modeling discipline, coding, or testing guidance. The residuals are documented, bounded, and have named triggers, especially around PR-A.3 carriers and |
|
Review metadata
Findings: None. The diff is documentation only ( Verdict: APPROVE — Narrow, well-bounded design brief with explicit fail-closed and residual boundaries; no concrete rubric violations in the diff. |
|
Review metadata
1. Story of the diffThis PR turns PR-B from an unauthored evaluator lane into a docs-only design slice for the body-evaluator half of runtime materialization. The manager row now splits PR-B into “body evaluator” and “witness construction,” marking only the body half as authored and leaving witness construction explicitly unauthored ( 2. Invariant categories
Compliant — docs-only; it explicitly says “No Rust execution code lands in this brief; no new substrate carriers are declared here” (
Compliant — fail-closed and facts-flow-forward are handled directly: future PR-B.1 must error on every non-eager/non-bounded case (
N/A — no Rust code is changed. The brief does constrain future code toward structured outputs and typed diagnostics by requiring
Compliant — this PR intentionally adds no tests because it is a docs-only design lock with no executable behavior or fixtures (
Compliant — the brief consumes existing authorities instead of silently altering them: it points to the PB runtime interpreter design for evaluation rules, runtime carrier briefs/files for
Compliant — the residuals are tracked, bounded, and have named triggers. The 3. VerdictAPPROVE. The PR is a clean docs-only design slice: it narrows PR-B.0 to an eager baseline, names the missing prerequisites, and treats unsupported execution paths as explicit residuals rather than silent implementation freedom. I found no diff-line-supported invariant violation. |
|
Review metadata
1. Story of the diffThis PR turns PR-B from an unauthored evaluator-design slot into a split body-evaluator/witness lane. The manager table now records that the body half has a PR-B.0 design slice while leaving witness construction explicitly unauthored ( 2. Invariant categories
3. VerdictAPPROVE. I found no blocking or non-blocking findings against the diff. The PR is a clean docs-only design lock: it narrows PR-B.0 to a shippable body-evaluator baseline, defers execution where carrier authority is absent, and names fail-closed residuals rather than normalizing partial evaluator behavior. |
briansrls
left a comment
briansrls
left a comment
There was a problem hiding this comment.
Review metadata
- Provider / model:
codex/unknown - Commit:
77c82e6a· Trigger:schedule - Thinking:
177s wall
Non-blocking — Strengths
docs/briefs/r2-pr-b-body-evaluator-eager-baseline.mdDocs-only PR-B.0 stays within design scope, names PR-A.3 carrier prerequisites, and tracks lazy/TC2/witness/descent execution as bounded R3 residuals instead of silently broadening PR-B.1.docs/briefs/r2-evaluator-manager.mdThe manager row now separates the body-evaluator half from the witness-construction half, matching the brief’s residual boundary.
✅ No blocking concerns; the prior LoopBound facts-flow-forward issue is addressed and the remaining gaps are explicitly deferred.
|
Already addressed at HEAD
— sent from merry-heron-351 |
1 participant
Summary
Docs-only PR-B body-evaluator design slice per Director dispatch. Authors
docs/briefs/r2-pr-b-body-evaluator-eager-baseline.mdand updates the manager brief PR-B row.R2 closure target for body evaluation is closed-with-residuals: design lock + carrier-prerequisite naming ship in R2; full executable evaluation, lazy/TC2, and witness construction are R3 residuals.
Brief contents
Value/NamedField, feat(evaluator): PR-A.1 runtime Value coproduct #1243), PR-A.2 (EvalFrame/EvalStateStack, feat(evaluator): PR-A.2 EvalFrame / EvalStateStack carriers #1255), PR-A.3 audit.EvalStrategy,InputEvaluationOrder,EvalStateKey,EvalMemoKey..dagbodies.ApplicativeOrder { LeftFirst }only. NoEvalThunk, noNormalOrder, no TC2 strengthening, no witness construction, no closures-with-captures.Out of scope
Test plan
🤖 Generated with Claude Code