From 63e081438fa0e99c0797233d9769326c8e2ef361 Mon Sep 17 00:00:00 2001 From: Brian Searls Date: Mon, 4 May 2026 18:05:43 +0000 Subject: [PATCH] docs(r3): audit execution predicate collapse --- ...te-command-foralltargets-collapse-audit.md | 180 ++++++++++++++++++ 1 file changed, 180 insertions(+) create mode 100644 docs/briefs/r3-v-execute-command-foralltargets-collapse-audit.md diff --git a/docs/briefs/r3-v-execute-command-foralltargets-collapse-audit.md b/docs/briefs/r3-v-execute-command-foralltargets-collapse-audit.md new file mode 100644 index 00000000000..25ae1226674 --- /dev/null +++ b/docs/briefs/r3-v-execute-command-foralltargets-collapse-audit.md @@ -0,0 +1,180 @@ +# R3 Verification - ExecuteCommand / ForAllTargets Collapse Audit + +**Status:** AUDIT RECEIPT - docs-only. This audits the duplicate execution +predicate shape in `src/v3/std/verification.dag`; it does not edit substrate, +the Rust runner, PB-Runtime, or target fixtures. + +**Scope:** `TestPredicate::ExecuteCommand`, `TestPredicate::ForAllTargets`, and +their current consumers in: + +- `src/v3/std/verification.dag` +- `src/v3/compiler/src/test_runner.rs` +- `src/v3/compiler/src/lens_testgen.rs` +- `src/v3/compiler/tests/` + +## Contract Restatement + +`verification.dag` currently declares two scaffold variants with the same raw +record shape: + +```dag +| ExecuteCommand { + command: String + args: List + expect_exit_code: Int + } + +| ForAllTargets { + command: String + args: List + expect_exit_code: Int + } +``` + +The comments already name the intended collapse: one capability-typed execution +fact plus a scope dimension, not two parallel `String / List / Int` +records. The audit question is whether that collapse can be implemented as a +Verification-side rewrite, or whether Substrate/PB/target-spec ownership must +land typed execution capability facts first. + +## Current Implementation Audit + +### Substrate Surface + +`ExecuteCommand` is a singleton host-process scaffold. Its inline comments say +the raw command string is tolerated only until audited tools/capabilities are +bound from the target-spec layer instead of opaque `String` command lines. + +`ForAllTargets` is a per-emission-target scaffold. Its inline comments say the +claim source stays on `TestClaim.source` / `TestClaim.file_name`, while the +variant repeats the same raw command triple only as a temporary shell check for +each known target. + +The two variants therefore differ in scope, not in execution capability shape. + +### Runner Surface + +`ExecuteCommand` is live in the Rust runner: + +- `parse_execute_command_fields` parses positional or record payloads into + `(command, args, expect_exit_code)`. +- `run_claim` dispatches the `ExecuteCommand` variant to `eval_execute_command`. +- `eval_execute_command` first requires a clean compile of `TestClaim.source`, + then runs `evaluate_execute_command_exit_code`. +- The host runner has typed outcomes in `ExecuteCommandHostOutcome` and maps + policy rejection, spawn failure, setup failure, timeout, signal, and exit-code + mismatch into `ClaimResult`. +- M1.5 testgen shares the same parser and evaluates `ExecuteCommand` through + `evaluate_execute_command_m1_5`; only matched exit code vs mismatch is treated + as propositional true/false. + +`ForAllTargets` is not live in the Rust runner: + +- `run_claim` has no `ForAllTargets` arm, so it falls to + `NotYetImplemented("TestPredicate:: is not wired in the Rust runner yet")`. +- `m1_5_testgen_test.rs` explicitly treats `ForAllTargets` as runner-deferred. +- `r3_verification_l4_l7_l5_skeleton_test.rs` asserts the L5 fixture reaches + `NotYetImplemented`. +- `docs/briefs/r3-v-l5-corpus-readiness-audit.md` independently records that + the current raw command triple is insufficient for strict L5 value + observation. + +## Carrier Collapse Predicate Sketch + +The eventual substrate shape should factor the duplicate record into two axes: +execution capability and execution scope. + +```dag +type ExecutionScope + = Once + | PerEmissionTarget + +type ExecutionCapability { + tool: ToolRef + args: List + expect_exit_code: Int +} + +type TestPredicate + = ... + | Execution { + capability: ExecutionCapability + scope: ExecutionScope + } +``` + +`ToolRef` / `Capability` is load-bearing. If the collapse keeps +`command: String`, the duplicate record shape shrinks but the opacity bridge +does not: command identity, sandbox policy, target applicability, and allowed +argv shape remain outside substrate. + +Required structural facts: + +| Fact | Exists today? | Current authority | +|---|---:|---| +| Singleton execution scope | Yes, implicit | `ExecuteCommand` variant label | +| Per-target execution scope | Yes, implicit | `ForAllTargets` variant label | +| Raw command / args / expected exit | Yes | duplicated variant fields | +| Typed host outcome classification | Yes, Rust-only | `ExecuteCommandHostOutcome` in `test_runner.rs` | +| Typed execution capability / tool reference | No | named as dissolution trigger in `verification.dag` | +| Target applicability / target set | Not in this carrier | L5 / LanguageSpec / target-spec work | +| Per-target runner semantics | No | `ForAllTargets` currently NYI | + +## Consumer Surface Enumeration + +| Consumer | Current dependency | Collapse impact | +|---|---|---| +| `src/v3/std/verification.dag` | Declares both scaffold variants with duplicate fields. | Must replace both variants with one scoped execution carrier, or add successor carrier while old variants remain compatibility scaffolds. | +| `test_runner.rs::parse_execute_command_fields` | Parses the raw triple for `ExecuteCommand`. | Becomes a parser for `ExecutionCapability`, ideally consuming typed tool/capability refs instead of strings. | +| `test_runner.rs::run_claim` | Dispatches `ExecuteCommand`; `ForAllTargets` falls through to NYI. | Needs one `Execution` arm that branches on `ExecutionScope`; `PerEmissionTarget` still requires target enumeration and per-target artifact execution. | +| `test_runner.rs::eval_execute_command` | Singleton clean-compile gate plus host process execution. | Can serve `ExecutionScope::Once`; cannot by itself implement per-target compilation/dispatch. | +| `test_runner.rs::ExecuteCommandHostOutcome` and helpers | Typed host-process outcome carrier. | Reusable for the singleton and each per-target child execution; not a substitute for typed capability identity. | +| `m1_5_testgen_test.rs` | Evaluates `ExecuteCommand`; treats `ForAllTargets` as deferred. | Must update generated predicate construction and interpreter boundary once successor variant exists. | +| `.dag` fixtures using `ExecuteCommand` | PB-Runtime / R1/R1C-E host receipts. | Need mechanical migration to `Execution { scope: Once, ... }` after compatibility decision. | +| `.dag` fixtures using `ForAllTargets` | L5 scaffold fixture only; expected NYI today. | Need migration to `Execution { scope: PerEmissionTarget, ... }`, but strict execution still waits on L5 target semantics. | +| Docs / readiness briefs | Several docs call `ForAllTargets` scaffold and raw command triple insufficient. | Should be updated with whichever successor carrier Substrate/PB ratifies. | + +## Conversion Cost Classification + +| Classification | Verdict | Rationale | +|---|---|---| +| **(a) Verification-side rewrite-only** | **No for the intended collapse** | Verification could mechanically merge the two variants into `Execution { command: String, args, expect_exit_code, scope }`, but that preserves the raw command identity bridge the current comments explicitly name as a dissolution target. It also would not make `PerEmissionTarget` runnable. | +| **(b) Substrate carrier extension** | **Yes** | A typed `ToolRef` / `Capability` / `ExecutionCapability` carrier is missing. The substrate must decide how commands are named, which args are structural, and how sandbox/target applicability is represented. | +| **(c) Cross-program PB / target-spec coordination** | **Yes** | PB-Runtime owns the host execution runner shape; L5 / target-spec work owns per-emission-target compilation and target set semantics. A single scoped carrier crosses both surfaces. | + +## Verdict + +**Routing needed before conversion.** + +The duplicate record shape is real, but the safe fix is not a Verification-only +enum rewrite. A rewrite that keeps `String` command identity would satisfy the +surface "one variant" shape while preserving the underlying opacity bridge. +Likewise, collapsing the variants without per-target semantics would hide the +fact that `ForAllTargets` is still intentionally `NotYetImplemented`. + +Recommended routing: + +1. **Substrate / PB-Runtime:** define `ExecutionCapability` with typed + `ToolRef` / capability identity, argv shape, expected outcome, and host + policy authority. +2. **Substrate / Verification:** define `ExecutionScope = Once | + PerEmissionTarget` and the successor `TestPredicate::Execution` shape, with + an explicit compatibility plan for existing `ExecuteCommand` fixtures. +3. **L5 / target-spec:** define how `PerEmissionTarget` enumerates target + artifacts and observes per-target results; do not encode that as repeated raw + shell commands. +4. **Verification follow-on:** after those facts land, migrate runner dispatch + and fixtures from `ExecuteCommand` / `ForAllTargets` to `Execution`. + +## Debt Receipt + +This audit does not close a Debt-Paydown row directly. + +Debt found + routed: the F12 duplicate-record-shape pattern requires +Substrate/PB/target-spec routing for typed execution capability and scoped +target execution semantics before the two variants can collapse without +preserving the raw command bridge. + +## Test Plan + +- `git diff --check`