Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 1 addition & 1 deletion docs/briefs/r2-evaluator-cadence-verification-matrix.md
Original file line number Diff line number Diff line change
Expand Up @@ -23,7 +23,7 @@ Make **Evaluator-side** gate status, **next allowed** work shape, and **forbidde
|---|---|---|---|---|---|
| **PR-A.1 — runtime `Value` + `NamedField`** | Evaluator Manager + **Worker A** (substrate/runtime module) | **Landed** — observable `Value` / `NamedField` live in `src/v3/std/runtime.dag` per [`r2-pr-a-runtime-value-model.md`](r2-pr-a-runtime-value-model.md) PR-A.1 + PB §3.2; [PR #1243](https://github.com/gunb-ai/gunbc/pull/1243) followed the dependency recorded in [`r2-pr-a1-runtime-value-dependency-audit.md`](r2-pr-a1-runtime-value-dependency-audit.md). | PB-Runtime shape match; L1 `ValueBehavior` marker remains distinct. | Consume the carrier from `v3.std.runtime`; strengthen downstream gates when PR-A.3 strategy/memo carriers land (PR-A.2 carriers already in `runtime.dag`). | No reopening `RuntimeValue`; no `ClosureValue`; no body execution. |
| **PR-A.2 — `EvalFrame` / `EvalStateStack`** | **Worker C / merry-heron-351** | **Landed** — `EvalFrame` / `EvalStateStack` live in `src/v3/std/runtime.dag` per [PR #1255](https://github.com/gunb-ai/gunbc/pull/1255) (merged dependency audit [PR #1222](https://github.com/gunb-ai/gunbc/pull/1222)). | PR-A.1 carriers; **unique-binding** `Map<PortId, Value>` disposition per PR-A brief (fail-closed map, not duplicate-admitting lists). | Mirror / consume landed carriers in evaluator wiring **without** new observable `Value` variants; tighten gates when PR-A.3 lands. | No `Value` inhabitants for closures; no skipping unique-binding carrier discipline. |
| **PR-A.3 — strategy / memoization** | Substrate carrier owner + Worker A test surface | **Eager strategy carrier landed; memo-key surface remains** — `EvalStrategy` / `InputEvaluationOrder` live in `src/v3/std/runtime.dag` with generated-full-bootstrap coverage; [`r2-pr-a3-strategy-memoization-audit.md`](r2-pr-a3-strategy-memoization-audit.md) remains the decision surface, and [`r2-pr-a3-implementation-blocker-audit.md`](r2-pr-a3-implementation-blocker-audit.md) is the historical receipt for the parser gap resolved by [PR #1286](https://github.com/gunb-ai/gunbc/pull/1286). Substrate owns remaining carrier declarations; Worker A owns non-overlapping follow-on tests. | Live `EvalFrame` / `EvalStateStack`, `EvalStrategy`, and `InputEvaluationOrder` in `src/v3/std/runtime.dag`; remaining PR-A.3 carrier surface is structural `EvalMemoKey` / `EvalStateKey` from the PR-A.0 sketch in [`r2-pr-a-runtime-value-model.md`](r2-pr-a-runtime-value-model.md). | Land structural memo-key carriers per audit in the Substrate-owned declaration slice; add Worker A generated-full-bootstrap tests for memo-key carrier shape after declarations land; add `EvalThunk` / lazy only with TC2 obligations understood. | No memoization that caches partial diagnostics as `Value`; no orphan strategy labels outside closed carriers; no name-only state fingerprints; no fake variants / alias workaround. |
| **PR-A.3 — strategy / memoization** | Substrate carrier owner + Worker A test surface | **Carrier surface landed** — `EvalStrategy` / `InputEvaluationOrder` and structural `EvalStateKey` / `EvalMemoKey` live in `src/v3/std/runtime.dag` with generated-full-bootstrap coverage; [`r2-pr-a3-strategy-memoization-audit.md`](r2-pr-a3-strategy-memoization-audit.md) remains the decision surface, and [`r2-pr-a3-implementation-blocker-audit.md`](r2-pr-a3-implementation-blocker-audit.md) is the historical receipt for the parser gap resolved by [PR #1286](https://github.com/gunb-ai/gunbc/pull/1286). | Live `EvalFrame` / `EvalStateStack`, `EvalStrategy`, `InputEvaluationOrder`, `EvalStateKey`, and `EvalMemoKey` in `src/v3/std/runtime.dag`; `EvalMemoKey` keys by `DeclarationId`, `NodeId`, structural `EvalStateKey`, and the closed strategy carrier. | Consume the closed eager strategy and structural memo-key carriers in PR-B/W1 as needed; add `EvalThunk` / lazy only with TC2 obligations understood. | No memoization that caches partial diagnostics as `Value`; no orphan strategy labels outside closed carriers; no name-only state fingerprints; no fake variants / alias workaround. |
| **PR-B — body evaluator** | Evaluator (worker brief pending) | **Not authored / not started** — [`r2-evaluator-manager.md`](r2-evaluator-manager.md) table. | **PR-A.1 through PR-A.3** for runtime/evaluator state; **worker dispatch** on implementation sub-lanes still joint-gated on **PR-E + R1 close** per manager option (c). | Author PR-B **design** brief after PR-A substrate is real; **no** implementation until PR-A chain + manager dispatch gates clear. | No structural body execution before frames + strategy boundary exist. |
| **PR-D — cross-target harness** | Evaluator Manager | **Design lock introduced** — [`docs/design-cross-target-equivalence.md`](../design-cross-target-equivalence.md); **slice 0 + slice 1 landed** — `Compiles` + `DifferentialEquals` scaffold per [`r2-pr-d-cross-target-equivalence-harness-primitives.md`](r2-pr-d-cross-target-equivalence-harness-primitives.md). | **Slice 2** gated: R2-T-Ground-**LanguageSpec**, **all Shape A targets grounded**, **T-Verification-L4-L7-Direct corpus** (that brief Dependencies table). | **Next:** docs-only updates, R3 corpus planning against the design lock, or Director-approved **existing** `ForAllTargets` claim wiring **only** when those deps are live and cited; otherwise keep deferral. | **No** L5 corpus execution at R2; **no** concrete target enumeration without live deps; **no** new `TestPredicate` variants (INVARIANTS P1). |
| **PR-E E9 — cross-target harness consumption** | Evaluator / PR-E lane | **Readiness-audit only** — [`r3-pr-e9-cross-target-harness-consumption-readiness.md`](r3-pr-e9-cross-target-harness-consumption-readiness.md) records that current main is not implementation-ready. | PR-D slice 0 + slice 1; PR-D design lock; **blocked** on LanguageSpec, all Shape A targets, L4/L7 corpus seed, and typed structural observation. | Keep docs/blocker rows current until all gates are cited together; then a single Director-approved `ForAllTargets` receipt may consume the existing PR-D/L5 fixture home. | No runner implementation; no target enumeration; no raw stdout/byte equality; no new predicate or substrate carrier. |
Expand Down
19 changes: 10 additions & 9 deletions docs/briefs/r2-pr-b-body-evaluator-eager-baseline.md
Original file line number Diff line number Diff line change
Expand Up @@ -169,20 +169,21 @@ These are **not** in PR-B.0 design lock and **not** in PR-B.1 implementation:

## R3 residual reason

Full evaluator execution cannot ship in R2 because:

1. **Strategy carriers absent at HEAD.** `EvalStrategy`,
`InputEvaluationOrder`, `EvalStateKey`, `EvalMemoKey` are audited but not
declared. Without the strategy carrier PR-B.1 has nothing to read, and
without `EvalMemoKey` the memoization boundary is undeclared. The
PR-A.3 audit explicitly lists these as the implementation-side gap.
2. **Execution semantics for non-eager strategies undeclared.** `NormalOrder`
The former PR-A.3 carrier absence is closed: `EvalStrategy`,

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: The new "carrier absence is closed" statement leaves this same brief's carrier-authority and still-needed-prerequisite sections saying strategy/memo carriers are undeclared, creating duplicate PR-B.1 gate authority contrary to INVARIANTS P1/P2.

`InputEvaluationOrder`, `EvalStateKey`, and `EvalMemoKey` live in
`src/v3/std/runtime.dag`, so PR-B.1 may read the closed eager strategy and
structural memo-key boundary rather than inventing a local no-memo or
string-key convention.

Full evaluator execution still cannot ship in R2 because:

1. **Execution semantics for non-eager strategies undeclared.** `NormalOrder`
has no rule, no thunk capture point, and no TC2 comparison obligation
(PR-A.3 audit §EvalStrategy). Until those land, the evaluator cannot
honor any inhabitant of `EvalStrategy` other than `ApplicativeOrder /
LeftFirst`, which means TC2 cannot strengthen and PR-D harness execution
cannot run two strategies for differential receipts.
3. **Witness construction surface unauthored.** The witness half of PR-B has
2. **Witness construction surface unauthored.** The witness half of PR-B has
no design lock yet. Even with PR-B.1 landed, witness emission for
downstream consumers (R3 lens producers, cross-target reflection
consumers) is not in scope here.
Expand Down
9 changes: 4 additions & 5 deletions docs/briefs/r3-v-l4-l7-direct-readiness-audit.md
Original file line number Diff line number Diff line change
Expand Up @@ -16,7 +16,7 @@ and [`r3-v-l4-l7-direct-scaffold-notes.md`](r3-v-l4-l7-direct-scaffold-notes.md)
|---|---|---|
| PR-A.2 frame state | `src/v3/std/runtime.dag` declares `EvalFrame { bindings: Map<PortId, Value> }` and `EvalStateStack { frames: List<EvalFrame> }`; Rust side has `EvalFrame<V>` / `EvalStateStack<V>` helpers in `src/v3/compiler/src/lib.rs`. | Landed enough for environment shape; no longer a blanket Lane 1 blocker. |
| PR-A.3 strategy carriers | `EvalStrategy = ApplicativeOrder { input_order: InputEvaluationOrder }` and `InputEvaluationOrder = LeftFirst` are now declared in `runtime.dag`. | The eager/left-first strategy identity is live. |
| PR-A.3 memo carriers | `EvalStateKey` and `EvalMemoKey` are still absent from `runtime.dag`. | Memoization identity remains open; do not claim PR-A.3 complete. Slice 1 can proceed only if PR-B.2 chooses no-memo or cites a Director-approved memo deferral. |
| PR-A.3 memo carriers | `EvalStateKey { state: EvalStateStack }` and `EvalMemoKey { program: DeclarationId, node: NodeId, state_key: EvalStateKey, strategy: EvalStrategy }` are declared in `runtime.dag`. | Structural memo-key identity is live; this audit's former memo-carrier blocker is closed. |
| PR-B body evaluator | `r2-pr-b-body-evaluator-eager-baseline.md` and `r2-pr-b-1-eager-evaluator-implementation-seed.md` are design/seed briefs; no full eager evaluator entry point is visible on main. | `dag_eval_output` cannot be a real producer yet. |
| PR-E E2 environment | EvalFrame/Bind environment helpers landed on main via #1374. | Removes a frame API gap, but not the body-execution gap. |
| PR-B.2/W1 runner extension | `r2-pr-b-2-runner-extension-bundle.md` owns `rust_emit_output` + `dag_eval_output`. `test_runner.rs::eval_differential_equals` still accepts only `(v3_program_cost, v2_oracle_cost)`. | L4 fixture row should wait for W1 producer dispatch, not invent a local predicate or stdout convention. |
Expand Down Expand Up @@ -68,10 +68,9 @@ variant is needed for slice 1.

The open question is sequencing, not predicate shape. `rust_emit_output` can
land independently of body evaluation, but `dag_eval_output` requires a real
PR-B.1 eager evaluator. Because `EvalStateKey` / `EvalMemoKey` are absent at
HEAD, the implementation brief must either wait for those memo carriers or
explicitly scope slice 1 to no-memo eager evaluation under Director approval.
Without that disposition, `dag_eval_output` would still be a fabricated oracle.
PR-B.1 eager evaluator and W1 producer wiring. The PR-A.3 structural memo-key
carriers are now declared, so this audit's former no-memo carve-out question is
no longer the blocking gate for `dag_eval_output`.

Cross-program flag: this is the same structural-observation/value-normalization
surface called out by the Lane 2 readiness work. The shared comparator should
Expand Down
12 changes: 6 additions & 6 deletions docs/briefs/r3-v-l4-l7-direct-readiness-reaudit-post-e5.md
Original file line number Diff line number Diff line change
Expand Up @@ -15,7 +15,7 @@ worker is not dispatch-ready until W1 wires `rust_emit_output` and
|---|---|---|
| PR-A.2 frames | `src/v3/std/runtime.dag:76-90` declares `EvalFrame { bindings: Map<PortId, Value> }` and `EvalStateStack { frames: List<EvalFrame> }`. | Still landed; not a blocker. |
| PR-A.3 eager strategy | `src/v3/std/runtime.dag:93-103` declares `EvalStrategy = ApplicativeOrder { input_order: InputEvaluationOrder }` and `InputEvaluationOrder = LeftFirst`. | Eager/left-first strategy identity is live. |
| PR-A.3 memo carriers | `src/v3/std/runtime.dag:86` mentions `EvalMemoKey` as PR-A.3-owned future work, but the live declarations jump from `EvalStateStack` to `EvalStrategy` at `src/v3/std/runtime.dag:89-98`; `git grep` finds no `type EvalStateKey` or `type EvalMemoKey` declaration at HEAD. | Memo identity remains absent. A no-memo eager carve-out still needs Director/runner-owner framing. |
| PR-A.3 memo carriers | `src/v3/std/runtime.dag` declares `EvalStateKey { state: EvalStateStack }` and `EvalMemoKey { program: DeclarationId, node: NodeId, state_key: EvalStateKey, strategy: EvalStrategy }`. | Structural memo identity is live. The former no-memo eager carve-out gate is closed; W1 producer wiring remains the blocker. |
| Body evaluator | `src/v3/compiler/src/lib.rs:547-553` exposes `pub fn evaluate_body(...) -> Result<Value, EvalError>`. Tests cover the shell at `src/v3/compiler/src/lib.rs:820-829` and branch dispatch at `src/v3/compiler/src/lib.rs:1344-1373`. | The old "no body evaluator entry point" blocker is closed. |
| W1 producer fixture | `src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag:19-23` still defines `rust_emit_output` / `dag_eval_output` as `miss_int_lookup()` placeholders, and the fixture header at `:1-4` says runner support is intentionally NYI until wiring lands. | The structural fixture exists, but producers are not real. |
| W1 runner extension | `src/v3/compiler/src/test_runner.rs:2336-2344` still accepts only `(v3_program_cost, v2_oracle_cost)` for `DifferentialEquals`; any other pairing returns `NotYetImplemented`. | `rust_emit_output` / `dag_eval_output` remain unwired. This is the blocking gate. |
Expand All @@ -32,9 +32,9 @@ The four #1392 fire criteria now evaluate as:
2. **`dag_eval_output` backed by real evaluator:** **Partially.** `evaluate_body`
exists and has E5-era runtime coverage, but no `dag_eval_output` producer
calls it from `TestRunner`.
3. **Memo gap closed or explicitly deferred:** **Still open.** No
`EvalStateKey` / `EvalMemoKey` declarations exist; an eager no-memo carve-out
is plausible but not sufficient without W1 producer wiring.
3. **Memo gap closed or explicitly deferred:** **Closed.** `EvalStateKey` /

Copy link
Copy Markdown
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

BLOCKING: Marking the memo gap closed while the dispatch paragraph still requires an explicit no-memo eager scope leaves incompatible W1 gates in one readiness audit, violating live-state documentation and boundary discipline.

`EvalMemoKey` declarations now exist with structural state and closed
strategy fields; W1 producer wiring remains independently required.
4. **Worker brief preserves failure taxonomy and fixture path:** **Yes.** The
existing fixture path remains
`src/v3/compiler/tests/fixtures/r3_verification_l4_emit_eval_match.dag`, and
Expand All @@ -56,8 +56,8 @@ Recommended trigger for re-engagement:
`NotYetImplemented` branch; and
- `dag_eval_output` invokes the real eager evaluator path rather than fixture
lookup or placeholder `miss_int_lookup()`; and
- the no-memo eager carve-out is explicitly recorded, or `EvalStateKey` /
`EvalMemoKey` carriers land.
- `EvalMemoKey` is consumed as the declared structural memo identity if W1 uses
memoization; no string/name-only state key is introduced.

Until then, cool-crab / Lane 1 implementation should stay on hold. The concrete
blocker is no longer evaluator critical mass; it is the W1 producer bridge
Expand Down
Loading
Loading