diff --git a/docs/briefs/r2-pb-canonical-lens-bridge-disposition.md b/docs/briefs/r2-pb-canonical-lens-bridge-disposition.md index 1b138d5c81c..b128a111aec 100644 --- a/docs/briefs/r2-pb-canonical-lens-bridge-disposition.md +++ b/docs/briefs/r2-pb-canonical-lens-bridge-disposition.md @@ -78,6 +78,6 @@ Either path is a substrate-level change outside PB authoring authority. PB terri - T-Bridge-Retirement distribution map: [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" T-Bridge-Retirement row. - Adjacent worker brief (already-retired §0.1/§0.2 carriers): [`b4-1-declarationref-consumer-migration-worker.md`](b4-1-declarationref-consumer-migration-worker.md). - Identity-carrier substrate pass: [`b4-identity-carrier-substrate-pass.md`](b4-identity-carrier-substrate-pass.md). -- Substrate-fact-introduction procedure (escalation path): `INVARIANTS.md:86` §"Procedure: substrate-fact introduction". +- Substrate-fact-introduction procedure (escalation path): `INVARIANTS.md:94` §"Procedure: substrate-fact introduction". - P2 cross-`Dag` reflection invariant (the constraint that holds the bridge in place): `INVARIANTS.md` §P2; runtime comment block at `src/v3/compiler/src/test_runner.rs:1762-1772` + `:1832-1833`. - Gating R3 lane: T-LensProducer-Retirement (PB-Runtime interpreter-as-data sub-gate); see [`r3-structure.md`](../r3-structure.md) §"Lane structure". diff --git a/docs/briefs/r2-pure-bootstrap-manager.md b/docs/briefs/r2-pure-bootstrap-manager.md index 47024091165..9146eb335b3 100644 --- a/docs/briefs/r2-pure-bootstrap-manager.md +++ b/docs/briefs/r2-pure-bootstrap-manager.md @@ -34,7 +34,7 @@ | R3 Lane | Size | Description | |---|---|---| | **T-LensProducer-Retirement** | XL | Three program-sized hand-Rust files retired via PB-Runtime + PB-1 patterns per [`docs/design-pb-runtime-interpreter.md`](../design-pb-runtime-interpreter.md) (Items 4+5 LANDED via #1176). **Internal sub-gates** per [§5.1 — R3-T-LensProducer-Retirement sub-gates](../design-pb-runtime-interpreter.md): (i) `lens_apply.rs` retired (gated on PB-Runtime interpreter-as-data per §3); (ii) `lens_testgen.rs` retired (same gate as `lens_apply.rs`); (iii) `regen_lens.rs` retired (gated on PB-1 bin-shim emit pattern per §4.2 — distinct gate). **PB-Runtime foundation already landed:** ExecuteCommand typed-outcome hardening (#1049) + T-PB-B boundary coverage (#1082). The 5-primitive constraint (per §3.1) names `Node | Conj | Disj | Cardinality | Bit` as the DAG-processor execution vocabulary (the dispatch primitives PB-Runtime operates over; not the 5 L1 `Behavior` variants `Value | Transform | Branch | Loop | Bind` which `Node` carries — different scopes per §3.1 mapping note). PB-Runtime ≡ R2-Evaluator's runtime model expressed as `.dag` (load-bearing distinction per §2 — dissolution-shaped, not parallel). Closure ledger reports sub-gate progress; lane is one program. **Plus advanced lifetime analyzer cases d/e/f** (closures, async lifetimes, self-referential/Pin) folded in per `design-emission-model.md` Open call 2 — the lifetime analyzer is structurally what replaces `lens_apply.rs`'s reflection work, so advanced cases land alongside retirement. | -| **BinShim instances + emit pattern + retirement dispatch** *(NEW; Item 5 ownership per #1176 §5.4)* | S | NOT YET AUTHORED — PB Manager owns per-shim `BinShim` instance declarations under `dsl/std/runtime/bin_shims/` + the bin-shim emit pattern + retirement dispatch (replaces hand-Rust `bin/regen_*` shims). Substrate Manager owns the `BinShim` carrier-type shape itself (additional fields, signature refinement) — generalized carrier-shape evolution escalates via INVARIANTS §P1 substrate-fact-introduction procedure. `regen_lens.rs` retirement (T-LensProducer-Retirement sub-gate iii) gates on this lane closing. Per §5.4 boundary: PB owns instance-row authoring + retirement; Substrate owns carrier-type evolution. | +| **BinShim instances + emit pattern + retirement dispatch** *(NEW; Item 5 ownership per #1176 §5.4)* | S | PLANNING BRIEF AUTHORED at [`r3-pb-binshim-retirement-worker.md`](r3-pb-binshim-retirement-worker.md) (PROPOSAL; dispatch-gated). PB Manager owns per-shim `BinShim` instance declarations under `dsl/std/runtime/bin_shims/` + the bin-shim emit pattern + retirement dispatch (replaces hand-Rust `bin/regen_*` shims). Substrate Manager owns the `BinShim` carrier-type shape itself (additional fields, signature refinement) — generalized carrier-shape evolution escalates via INVARIANTS §P1 substrate-fact-introduction procedure. `regen_lens.rs` retirement (T-LensProducer-Retirement sub-gate iii) gates on this lane closing. Per §5.4 boundary: PB owns instance-row authoring + retirement; Substrate owns carrier-type evolution. | | **T-FixedPoint** | M | `compiler.dag` compiles to bit-identical stage0 Rust + bit-identical emitted artifacts; R1's `pb_self_compile_fixed_point` gate closes under stronger interpretation. Depends on R2-Evaluator + SG-0 zero from T-LensProducer-Retirement. | | **T-Tier3-Dissolution** *(may share with Tier 3 Manager continuing post-R2)* | M | Four hand-Rust mirrors of `.dag` types retired (mirror bodies replaced by Evaluator-backed authority inside `dag.rs` / `dag/effects.rs` / `workflow_idempotency.rs`); **consumer count / mirror-symbol count reaches zero**. SG-0 delta is reported and **usually 0** because the hand-authored file remains on the census after mirror-block retirement — SG-0 reaches 0 through broader PB-Substrate / generated-file retirement + T-LensProducer-Retirement. | | **3 distributed bridge retirements** *(part of T-Bridge-Retirement distribution map; see Cross-program below)* | varies | (3) canonical lens-name dispatch — lens-producer-retirement adjacent; (4) `include_str!` side channels (e.g., `pipeline_authority.rs`) — compiler-internal bootstrap; (5) `patch_lower_helpers_*` residual — Tier 2 retirement lineage; #1014 was first slice. Verification Manager owns the unified `bridge_retirement_ledger_zero` ledger gate; PB owns retirement work for these 3 bridges. | @@ -118,6 +118,7 @@ Authored: - Pre-R1 PB program briefs (in `pure-bootstrap-zero-manager.md`, archives on R2 promotion); content migration here covers post-R1 deliverables only. - [`r2-pb-tier3-mirror-dissolution-workers.md`](r2-pb-tier3-mirror-dissolution-workers.md) — termination, computation, induction, and effect-carrier mirror dissolution worker pack. - [`r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md) — T-FixedPoint planning artifact (PROPOSAL; dispatch-gated on R2-Evaluator + SG-0=0 from T-LensProducer-Retirement). +- [`r3-pb-binshim-retirement-worker.md`](r3-pb-binshim-retirement-worker.md) — BinShim instances + emit pattern + retirement dispatch planning artifact (PROPOSAL; dispatch-gated on R2-Evaluator + Item 4 PB-Runtime + Substrate-owned `BinShim` carrier + §7.3 `CensusListConstant`/filter disposition). Pending — pre-spawn Director-authored per inbox #828 coordination split; post-spawn manager-authored autonomously: - `kernel_algebra_profile` worker brief (gated on Substrate Manager `ValueBody::Map` consumer plumbing) diff --git a/docs/briefs/r3-pb-binshim-retirement-worker.md b/docs/briefs/r3-pb-binshim-retirement-worker.md new file mode 100644 index 00000000000..7e743571ce6 --- /dev/null +++ b/docs/briefs/r3-pb-binshim-retirement-worker.md @@ -0,0 +1,129 @@ +# R3 PB — BinShim instances + emit pattern + retirement dispatch (PB-owned planning brief) + +**Status:** PROPOSAL (planning artifact, dispatch-gated). Authored 2026-04-29 by PB Manager continuation per the "NOT YET AUTHORED" cell at [`docs/briefs/r2-pure-bootstrap-manager.md`](r2-pure-bootstrap-manager.md) line 37 and the Item 5 ownership lock from [`docs/design-pb-runtime-interpreter.md`](../design-pb-runtime-interpreter.md) §5.4 (LANDED via #1176/#1186). + +**Owning manager:** Pure Bootstrap Manager (R2 → R3 continuation per `r3-structure.md` §"Manager structure" Item 1). + +**Lane size:** S (per `r2-pure-bootstrap-manager.md` R3 continuation table). + +**This is a planning artifact — not a dispatch order.** Worker dispatch is gated; see §"Dispatch preconditions" + §"STOP conditions". PB Manager re-reads this brief at gate-clear to issue worker dispatch. + +## Scope + +PB owns three deliverables for the bin-shim class of T-LensProducer-Retirement sub-gate iii (`regen_lens_dot_rs_retired`): + +1. **Per-shim `BinShim` instance declarations** under `dsl/std/runtime/bin_shims/` — one `data _shim: BinShim = { ... }` per existing PB-owned hand-Rust bin (§4.1 of the design doc names `regen_lens.rs` as the canonical first target; §4.1 also names other regen drivers as the broader class). Each instance is a pure-data witness of the existing pipeline's load/compile/write composition. +2. **The bin-shim emit pattern** — a `.dag` emitter program (analogous in shape to `dsl/extdeps/languages/rust/emit.dag` per design doc §4.2) that translates `BinShim` declarations to Rust files headed `// AUTO-GENERATED from — DO NOT EDIT.`. +3. **Retirement dispatch** — once (1) and (2) land, dispatch the per-bin retirement workers in the order called out by §4.3, starting with `regen_lens.rs` as canonical first cut (sub-gate iii of T-LensProducer-Retirement; see §5.1). + +PB does **not** own and **must not** edit: + +- The `BinShim` carrier-type shape (additional fields, signature refinement of `entry: () -> std.process.ProcessExit`, etc.) — that's Substrate Manager territory per §5.4 boundary; generalized carrier-shape evolution escalates via `INVARIANTS.md` §P1 substrate-fact-introduction procedure. +- The PB-Runtime interpreter-as-data implementation (Item 4 / sub-gates i + ii — `lens_apply.rs` and `lens_testgen.rs` retirement). Those are separate and gated separately. +- The §7.3 `CensusListConstant` / filter-predicate substrate question (see §"Substrate gap" below). + +## First slice — `regen_lens.rs` + +Per design doc §4.3 the dissolution path is: + +1. Author `data regen_lens_shim: BinShim = { name: "regen_lens", entry: regen_lens, ... }` in `dsl/std/runtime/bin_shims/regen_lens.dag`. +2. Land the `BinShim` emitter (deliverable 2). Emitter generates `src/v3/compiler/src/bin/regen_lens.rs` from the `.dag` declaration. +3. Verify behavioral equivalence vs the current hand-Rust shim (per §7.2 fixture; **not** byte-identity — the emitted form carries an `AUTO-GENERATED` header and may differ in formatting / comment shape). +4. Retire the hand-Rust file. +5. SG-0 census drops one entry (`regen_lens.rs`); ratchet `EXPECTED_HAND_AUTHORED_NON_TEST` count goes down by one. + +Subsequent bin-shims (other `regen_*.rs` drivers, `self_host_fixed_point.rs` to the extent it's bin-shim-shaped, etc.) follow the same template, dispatched serially by PB Manager. The lane closes when every PB-owned hand-Rust bin in `src/v3/compiler/src/bin/` is either retired via this pattern or has a Director-approved continuing exception. + +## Dependencies / gates + +Per design doc §5.4 + §7 + the broader R3 Evaluator-gated lane discipline in [`docs/r3-structure.md`](../r3-structure.md): + +1. **R2-Evaluator landed.** §5.4 calls out Evaluator Manager as co-author of the convergence path. PB-Runtime mirrors the Evaluator's runtime-value model; without Evaluator the bin-shim emitter and the §7.2 equivalence fixture have no runtime to verify against. +2. **Item 4 (PB-Runtime interpreter-as-data) landed.** Item 5 (this lane) inherits Item 4's runtime-value vocabulary; the bin-shim emitter is "one of many `.dag` emitters" per §6 anti-bridge invariant #4, sharing the same fold-over-`Lens` substrate. +3. **Substrate-owned `BinShim` carrier type live.** The `type BinShim { ... }` sketch in design doc §4.2 is the locked design; Substrate Manager lands the carrier (in `dsl/std/runtime/bin_shim.dag` or wherever Substrate picks per their dispatch). PB cannot author instance declarations against a carrier that doesn't exist. +4. **`std.process.ProcessExit` substrate live.** Design doc §4.2 names this as the structural contract for translating `.dag` program return values into host process exit codes. Already declared per design doc reference; verify on dispatch. +5. **No-new-bin-shim-hand-Rust fixture's substrate prerequisite.** §7.3 names a substrate gap: neither `expected_hand_authored_bin_shims` `CensusListConstant` nor a filter-predicate-over-`expected_hand_authored_non_test` exists today (current `CensusListConstant` values per design doc §7.3 are `expected_hand_authored_non_test` and `expected_hand_authored_test` only). Substrate Manager picks the §P1 disposition (new constant vs filter predicate vs `CensusSubsetCount` reuse) when this lane dispatches; PB does not pre-empt that choice. + +These dependencies are cumulative: R2-Evaluator → Item 4 (PB-Runtime) → BinShim carrier + ProcessExit live → bin-shim instances/emitter (this lane) → per-shim retirement. + +## Acceptance — what a future implementation PR must prove + +Per design doc §7. The locked TestClaim names are authoritative; do not rename: + +### `pb_runtime_equivalent_to_evaluator_on_corpus` (§7.1) + +Owner: Item 4 lane (out of this brief's scope, but cited because §5.1 makes Item 4 a precondition). PB-Runtime evaluation of every `.dag` program in the certification corpus equals R2-Evaluator's evaluation of the same program. Substrate the bin-shim lane consumes; not authored here. + +### `regen_lens_bin_shim_emits_behaviorally_equivalent_to_hand_rust` (§7.2) + +Behavioral equivalence (NOT byte-identity per anti-bridge invariant #1) between the emitted Rust from `data regen_lens_shim: BinShim` and the current hand-Rust `regen_lens.rs`. Authoring shape per design doc: + +```dag +test_claim { + name: "regen_lens_bin_shim_emits_behaviorally_equivalent_to_hand_rust" + ... // shape locked in design doc §7.2 +} +``` + +If the existing `TestPredicate` envelope at `src/v3/std/verification.dag:108-235` cannot express "behavioral equivalence between emitted and hand-Rust binaries," this is a **substrate gap** — escalate per `INVARIANTS.md` §P1 to Substrate Manager. PB does not invent a new `TestPredicate` variant from this lane. + +### `no_new_bin_shim_hand_rust` (§7.3) + +Closed-set retirement gate: hand-Rust bin-shim count never exceeds the documented retirement schedule. Substrate prerequisite is **not yet live** (see §"Dependencies" item 5); this gate is unauthorable until Substrate Manager picks the §P1 disposition. + +### Other behavioral acceptance bullets (per dispatch directive) + +- **Behavioral equivalence to hand Rust.** Covered by §7.2 above. +- **No new hand-Rust bin shim.** Covered by §7.3 above (substrate-gated). +- **Generated file is not editable authority.** Emitted bin-shim files carry the `// AUTO-GENERATED from — DO NOT EDIT.` header per design doc §4.2; SG-0 census already enforces "hand-authored `// AUTO-GENERATED` header does not slip through" (per `sg0_census_test.rs` header rule). The retirement PR must add the per-shim emit path to `REGEN_OUTPUTS` in `src/v3/compiler/build.rs` so the SG-0 partition counts the file as generated. +- **SG-0 delta.** For each retired bin-shim, `EXPECTED_HAND_AUTHORED_NON_TEST` shrinks by one; `GENERATED_FILES` (via `REGEN_OUTPUTS`) grows by one. The retirement PR must update both atomically. + +## Non-goals + +This lane explicitly does NOT cover: + +- **T-FixedPoint implementation** (#1169 lane; gated separately). +- **`lens_apply.rs` / `lens_testgen.rs` retirement** — Item 4 sub-gates i + ii. Different runtime substrate (PB-Runtime interpreter-as-data); this lane consumes Item 4 but does not implement it. +- **PB-Runtime interpreter-as-data implementation** — Item 4. This lane assumes Item 4 has landed. +- **Substrate-owned `BinShim` carrier-shape edits** — additional fields, refining `entry: () -> std.process.ProcessExit` beyond the locked signature, etc. Escalate to Substrate Manager via §P1 if the retirement work surfaces a real shape gap. +- **§7.3 `CensusListConstant` / filter-predicate substrate authoring** — Substrate Manager territory per §P1 disposition. This lane consumes whatever Substrate authors; it does not pre-empt the choice. + +## Dispatch preconditions + +PB Manager dispatches per-shim retirement workers when **a single readiness check** confirms all of: + +1. R2 close signal (R2 Release Manager closure ledger) — same precondition as the other 7 Evaluator-gated R3 lanes per `docs/r3-structure.md` §"R3 worker dispatch precondition". +2. R2-Evaluator landed and stable. +3. **Item 4 (PB-Runtime interpreter-as-data) sub-gate green** — `pb_runtime_equivalent_to_evaluator_on_corpus` evaluates true. +4. **Substrate-owned `BinShim` carrier type live on main** — `type BinShim { ... }` declared per design doc §4.2 (verify by grep at dispatch). +5. **Substrate-owned `CensusListConstant` / filter disposition for §7.3 picked** — without this, the `no_new_bin_shim_hand_rust` gate is unauthorable and the closed-set discipline is unenforceable. + +If any of (1)-(5) is unmet, this brief stays in PROPOSAL state; PB Manager does not dispatch. + +## STOP conditions + +Worker MUST STOP and escalate to PB Manager (which escalates to Director if cross-program) when: + +- **`BinShim` carrier shape pressure.** Authoring a `data _shim: BinShim = { ... }` instance reveals that the locked carrier shape (per design doc §4.2) cannot express the bin's actual entry-function signature or pipeline composition. That's a Substrate-owned carrier-shape evolution per §5.4 boundary; signal Substrate Manager via §P1 — do not extend the carrier from this lane. +- **No fitting `TestPredicate` variant for §7.2 equivalence.** If "behavioral equivalence between emitted Rust and hand-Rust binary" cannot compose from existing variants at `src/v3/std/verification.dag:108-235`, that's a substrate gap — §P1 to Substrate Manager. Do not invent a new variant here. +- **Emit-pattern divergence from `dsl/extdeps/languages/rust/emit.dag` shape.** Per anti-bridge invariant #4 the `BinShim` emitter "is one of many `.dag` emitters; its shape mirrors `dsl/extdeps/languages/rust/emit.dag`." If the retirement worker finds itself authoring parallel emit logic, STOP — that's a sign the carrier or pattern is wrong. +- **§7.3 substrate disposition not yet live.** If the substrate prerequisite (item (5) above) hasn't landed, the lane cannot close even if the per-shim retirement is mechanically successful — `no_new_bin_shim_hand_rust` would be unauthorable. Surface this to Substrate Manager + R3 Release Manager rather than working around it. +- **SG-0 census drift the wrong way.** Per `feedback_ratchet_only_down`: if the retirement PR does not net-decrease the hand-Rust bin-shim count, that's a defect in the work, not a ratchet to relax. + +## Cross-program signals + +- **Evaluator Manager** — runtime-value model convergence (§5.4 cross-program coordination); PB-Runtime mirrors Evaluator's value model. Per-shim authoring confirms the mirror; deviation is a co-design escalation, not unilateral PB authority. +- **Substrate Manager** — `BinShim` carrier-shape evolution (§5.4 boundary), §7.3 `CensusListConstant` / filter-predicate disposition (§7.3 substrate prerequisite), any new `TestPredicate` variant proposed by §7.2's equivalence requirement. +- **R3 Release Manager** (when authored) — sub-gate progress reporting per `r2-pure-bootstrap-manager.md` §"Reporting cadence" (closure-ledger reports T-LensProducer-Retirement sub-gate progress within the one-program lane). +- **Director** — scope-change escalations (e.g., a bin-shim that needs Director-approved continuing exception rather than retirement); §P1 escalation arbitration if Substrate disposition stalls. + +## Cross-refs + +- Parent manager brief: [`docs/briefs/r2-pure-bootstrap-manager.md`](r2-pure-bootstrap-manager.md) — R3 continuation row "BinShim instances + emit pattern + retirement dispatch" (line 37) + Locked design decisions §"PB-Runtime interpreter-as-data + PB-1 bin-shim emit pattern (LANDED via #1176)" (line 62 onwards). +- Design lock: [`docs/design-pb-runtime-interpreter.md`](../design-pb-runtime-interpreter.md) — §4.1 bin-shim class enumeration; §4.2 `BinShim` carrier-shape sketch + emitter shape; §4.3 dissolution path; §4.4 first-time-bootstrap compatibility; §5.1 R3-T-LensProducer-Retirement sub-gate decomposition; §5.4 PB/Substrate/Evaluator boundary; §6 anti-bridge invariants; §7.2 BinShim equivalence fixture; §7.3 No-new-bin-shim-hand-Rust fixture (with substrate prerequisite call-out). +- T-LensProducer-Retirement parent lane: [`docs/r3-structure.md`](../r3-structure.md) §"Lane structure" T-LensProducer-Retirement row. +- Sibling R3-PB lane (separate scope, gated separately): T-FixedPoint planning brief — [`docs/briefs/r3-pb-t-fixedpoint-worker.md`](r3-pb-t-fixedpoint-worker.md). +- Substrate-fact-introduction procedure (escalation path): `INVARIANTS.md:94` §"Procedure: substrate-fact introduction". +- SG-0 census authority + generated-file partition: `src/v3/compiler/tests/integration/sg0_census_test.rs` (`EXPECTED_HAND_AUTHORED_NON_TEST` + `GENERATED_FILES`); `src/v3/compiler/build.rs` `REGEN_OUTPUTS`. +- First-shim source (unchanged until retirement): `src/v3/compiler/src/bin/regen_lens.rs`. +- Existing emitter shape reference (per anti-bridge invariant #4): `dsl/extdeps/languages/rust/emit.dag`. diff --git a/docs/briefs/r3-pb-t-fixedpoint-worker.md b/docs/briefs/r3-pb-t-fixedpoint-worker.md index 8ff99573ade..7ed6acf4c59 100644 --- a/docs/briefs/r3-pb-t-fixedpoint-worker.md +++ b/docs/briefs/r3-pb-t-fixedpoint-worker.md @@ -210,6 +210,6 @@ When the R3 Verification Manager spawns (per `r3-structure.md` §"Manager struct - B5 audit (TC3 dependency): [`docs/briefs/r2-release-b5-loop-construction-closure-audit-worker.md`](r2-release-b5-loop-construction-closure-audit-worker.md) - P4 Decidability (TC3 formal home): `INVARIANTS.md:236` §P4 - Termination carrier: `dsl/std/termination.dag` (`DescentEvidence` / BoundedLattice) -- Substrate-fact-introduction procedure (TC3 escalation path): `INVARIANTS.md:86` §"Procedure: substrate-fact introduction" +- Substrate-fact-introduction procedure (TC3 escalation path): `INVARIANTS.md:94` §"Procedure: substrate-fact introduction" - Strong-normalization theorem source (off-main at authoring): PR #1178 `docs/design-substrate-lambda-calculus-grounding.md` §"Strong normalization for the typed fragment" - TC3 transition target: R3 Verification Manager (per `docs/r3-structure.md` §"Manager structure" Item 2)