diff --git a/docs/briefs/b4-1-declarationref-consumer-migration-worker.md b/docs/briefs/b4-1-declarationref-consumer-migration-worker.md new file mode 100644 index 00000000000..ca78fd70fd5 --- /dev/null +++ b/docs/briefs/b4-1-declarationref-consumer-migration-worker.md @@ -0,0 +1,235 @@ +# B4.1a — `DeclarationRef` consumer migration for runner identity bridges `(M, Tier 1)` + +> **Worker brief.** Reports through Director (`zesty-bear-812`). +> First B4 Phase 1 sub-brief from +> [`docs/briefs/b4-identity-carrier-substrate-pass.md`](b4-identity-carrier-substrate-pass.md). +> This is a consumer-migration brief, not a carrier-landing brief: +> `DeclarationRef` already exists at `src/v3/spec/v3_l1.dag`. +> This brief covers the runner-facing §0.1/§0.2/§0.3 portion of the +> parent B4.1 scope. §0.5 and §0.7 are explicitly owned by named +> follow-up briefs below. + +## Read first + +- **[`src/v3/spec/v3_l1.dag:62-69`](../../src/v3/spec/v3_l1.dag)** — + live `DeclarationRef` authority. A record field typed as + `DeclarationRef` lowers identifier/dotted-path field values to + `FieldValue::Reference(DeclarationId)`. +- **[`src/v3/compiler/src/lower.rs:2824`](../../src/v3/compiler/src/lower.rs)** — + lowerer support for the `DeclarationRef` sentinel; the + `FieldValue::Reference` returns are currently at `:2844` and + `:2854`. +- **[`src/v3/std/verification.dag`](../../src/v3/std/verification.dag)** — + existing verification consumers: `LensOutputEquals`, + `DifferentialEquals`, `MockBackedInvariant`, etc. already carry + `DeclarationRef` fields. +- **[`src/v3/compiler/src/test_runner.rs:20-48`](../../src/v3/compiler/src/test_runner.rs)** — + canonical `named_function_count.dag` `include_str!` bridge and + fixture-filename routing comments, including + `cost_bind_for_claim_file`. +- **[`src/v3/compiler/src/test_runner.rs:1589-1765`](../../src/v3/compiler/src/test_runner.rs)** — + `LensOutputEquals` program-input sentinel path. +- **[`src/v3/compiler/src/test_runner.rs:1829-1866`](../../src/v3/compiler/src/test_runner.rs)** — + `DifferentialEquals` program-input sentinel path. +- **[`src/v3/compiler/tests/fixtures/r1_gates.dag`](../../src/v3/compiler/tests/fixtures/r1_gates.dag)** + and **[`src/v3/compiler/tests/t_demo/t_demo_fixtures.dag`](../../src/v3/compiler/tests/t_demo/t_demo_fixtures.dag)** — + fixture declarations that currently define/use + `r1_lens_output_input_from_program`. +- **`feedback_groundedness_gates_lenses`**, + **`feedback_no_metadata_markers`**, and + **`feedback_construction_over_ratchets`**. + +## Existing-authority audit + +`DeclarationRef` is already landed and consumed. Grep audit: + +- `src/v3/spec/v3_l1.dag` declares `type DeclarationRef {}`. +- `src/v3/std/verification.dag` imports it and uses it for + `LensOutputEquals.lens_ref`, `input_ref`, `expected_ref`, + `DifferentialEquals.subject_ref`, `oracle_ref`, `input_ref`, and + other verification payloads. +- `src/v3/std/emit_model.dag`, `src/v3/std/resources.dag`, + `src/v3/std/substrate.dag`, and `src/v3/spec/python.dag` already + use `DeclarationRef`. +- `lower.rs` resolves fields whose declared type walks to + `DeclarationRef` into `FieldValue::Reference`. + +Conclusion: do **not** add a new universal declaration-reference +carrier. The runner slice of the remaining B4.1 work is a +role/consumer migration on top of the existing `DeclarationRef`: +replace runner-local sentinel and filename bridges with structural +references that identify the program input role and canonical lens +declaration without string dispatch. + +## Parent B4.1 Scope Split + +The parent brief defines B4.1 as the `DeclarationRef` consumer +migration for §0.1, §0.2, §0.3, §0.5, and §0.7. This worker brief is +therefore named **B4.1a** and covers only the runner identity bridges: + +- **§0.1 / §0.3 program-input and canonical-lens identity** in + `test_runner.rs`. +- **§0.2 output-bind identity** in `cost_bind_for_claim_file` / + `TestClaim.file_name` routing. + +The remaining parent B4.1 sites are tracked as named follow-ups: + +- **B4.1b — structural type-alias carrier for §0.5.** Owns the + `span.file == "dsl/std/types.dag"` type-alias bridge at + `lower.rs:836`. Trigger: author and dispatch immediately after + B4.1a lands or earlier if an implementation touch in `lower.rs` + reaches the type-alias bridge. Acceptance must remove the + path-equality check or replace this brief with a Director-approved + substrate carrier if plain `DeclarationRef` is insufficient. +- **B4.1c — structural declaration-source carrier for §0.7.** Owns + `declaration_name_preference_rank(&span.file)` in `dag.rs:2781` + plus the lowerer call sites at `lower.rs:1460-1461` and + `lower.rs:1555-1556`. Trigger: author and dispatch after B4.1a or + any time declaration collision/preference behavior is edited. + Acceptance must dissolve the file-suffix preference table into a + structural declaration-source fact, or explicitly STOP with + Grounding/Zero-Floor if the carrier is broader than `DeclarationRef` + plus a role layer. + +## Frame + +The current runner has three different facts collapsed into strings: + +1. **Program input identity.** `r1_lens_output_input_from_program` + means "the input value is the claim program DAG reflected from + `TestClaim.source`", not an ordinary declaration value. The current + code compares declaration names to this sentinel. +2. **Canonical lens identity.** `named_function_count` uses + `include_str!("../lenses/named_function_count.dag")` and + filename checks to recover the canonical lens program. +3. **Output-bind identity.** `cost_bind_for_claim_file` maps + `TestClaim.file_name` to ordinary bind names such as + `merge_sort_out` and `lane_e_diff_out`. This is a fixture-filename + bridge for "which bind is the asserted output?", not a property of + the source program. + +Plain `DeclarationRef` already carries "this field names a +declaration" but it does not, by itself, distinguish ordinary +declaration values from the special program-input role, nor does it +load the referenced lens program, nor does it say which bind is the +claim output. B4.1a should land the smallest structural role layer +needed by the runner, then migrate the consumers. + +## Slice + +1. **Model the program-input role structurally.** + - Prefer a typed declaration in `src/v3/std/verification.dag` + that represents the program-input carrier/role used by + lens-output and differential checks. + - The runner should detect this role by `DeclarationId` or typed + `ValueBody`/meta-tag shape, not by the name + `r1_lens_output_input_from_program`. + - Keep the public fixture surface compatible only if the carrier is + explicit and structural; do not introduce a replacement sentinel + string. + +2. **Model canonical lens identity structurally.** + - Audit whether an existing `DeclarationRef` in the claim payload + can point directly at the canonical lens declaration loaded from + the same compiled fixture DAG. + - If not, land the minimal runner/lens registry carrier in + `std.verification` or a more appropriate existing std/spec file. + - Delete or confine the `include_str!` canonical-lens bridge once + the runner can obtain the referenced lens program structurally. + +3. **Model output-bind identity structurally (§0.2).** + - Replace `cost_bind_for_claim_file(TestClaim.file_name)` with a + structural reference from the claim payload to the output bind + declaration. + - Prefer a `DeclarationRef` field (or a typed role wrapper over a + `DeclarationRef`) that names the exact bind declaration whose + value port should be compared. + - If the current verification payload cannot express "this bind is + the claim output" without a broader role model, STOP and split a + named B4.1a-runner-output follow-up brief before implementation. + - Do not replace the file-name map with another string-to-string + registry. + +4. **Migrate `LensOutputEquals`.** + - Replace `PROGRAM_INPUT_SENTINEL` checks at + `test_runner.rs:1594`, `:1617`, `:1642`, and `:1709` with the + structural program-input role. + - Preserve fail-closed behavior for ordinary `input_ref` + declarations with missing value bodies. + +5. **Migrate `DifferentialEquals`.** + - Replace the `PROGRAM_INPUT_SENTINEL` check at + `test_runner.rs:1855` with the same structural program-input + role. + +6. **Update fixtures and tests.** + - Rewrite `r1_gates.dag`, `r1_gates.template.dag`, and + `t_demo_fixtures.dag` to use the structural carrier. + - Add regression coverage that an ordinary declaration named like + the old sentinel is not treated as program input unless it carries + the structural role. + - Add regression coverage that an ordinary fixture filename no + longer selects a claim output bind unless the claim carries the + structural output-bind reference. + +## Acceptance + +- [ ] No `PROGRAM_INPUT_SENTINEL` constant remains in `test_runner.rs`. +- [ ] `test_runner.rs` no longer dispatches on the literal + `"r1_lens_output_input_from_program"`. +- [ ] Canonical lens lookup no longer depends on fixture filename or + `include_str!` once the referenced lens identity is structurally + available. If this proves to require a separate registry carrier, + STOP and split that registry carrier as B4.1a-lens-registry. +- [ ] `cost_bind_for_claim_file` and its `TestClaim.file_name` routing + are removed or split into a named B4.1a-runner-output follow-up + before any runner migration PR proceeds. +- [ ] Claim output-bind selection is carried by a structural + `DeclarationRef`/role reference, not by fixture filename or bind + name strings. +- [ ] Fixtures use `DeclarationRef` plus the new structural role layer; + no replacement sentinel string is introduced. +- [ ] Regression test proves name-only spoofing of the old sentinel + does not select the program-input path. +- [ ] Regression test proves filename-only spoofing does not select an + output bind without the structural output-bind reference. +- [ ] `cargo test --workspace --exclude v2-compiler-tests` passes. +- [ ] `cargo clippy --all-targets -- -D warnings` clean. +- [ ] `cargo fmt --all --check` clean. +- [ ] DB-8 fixed-point converges bit-identically, or any intentional + std/verification fixture drift is recorded and approved by + Director. + +## STOP-AND-ESCALATE + +- **Plain `DeclarationRef` is insufficient and the needed role layer + wants a broader substrate change** (for example, a generic + `RoleRef` or declaration metadata model). Stop and re-scope with + Director/Zero-Floor before editing consumers. +- **Canonical lens identity requires loading a second DAG by path.** + Do not replace one `include_str!` bridge with another string registry; + split a structural lens-registry carrier brief. +- **§0.5 type-alias or §0.7 declaration-source work is pulled into + this runner PR.** Stop and split to B4.1b or B4.1c unless Director + explicitly expands this brief. +- **A fixture cannot express the program-input role without a string + sentinel.** Stop; the carrier is under-specified. +- **DB-8 drifts unexpectedly.** Stop immediately. + +## Non-goals + +- Not touching B4.2 fold-shape carrier or the `lens_apply.rs` + `std/algebra.dag` skip. +- Not touching B4.3 emit-helper carriers. +- Not touching B4.4 extdeps fixture-set carrier. +- Not touching B4.1b §0.5 type-alias bridge. +- Not touching B4.1c §0.7 declaration-source/file-preference rank. + +## Reporting + +Single PR for B4.1a once implemented. Title: +`fix(v3): B4.1a migrate runner identity bridges to DeclarationRef roles`. +PR body must cite this brief, include the existing-authority audit +above, and record whether canonical lens identity stayed in B4.1a or +was split to B4.1a-lens-registry. Director must queue B4.1b and B4.1c +before closing the parent B4.1 DeclarationRef migration.