# 50 — Wall workflow and contract registry (in development)

> **Status: in development (2026-10-06, wall-directed wave).** Documents the
> wall-hell escape workflow (observe → classify → model → falsify → contract),
> the six wall classes and which tool may be used for each, the capture-request
> discipline, and the contract registry (`harness/contracts.py`,
> `harness/run_contracts.py`) that turns every solved wall into a re-runnable
> regression.
>
> Development-only: the registry re-runs offline tooling; it never touches a
> GPU, kernel module, mdev, guest or network, and it adds no measurement
> capability of its own. Fidelity stays what each wrapped tool claims (L0/L1;
> `06-ACCURACY.md`).
>
> **See also:** `47-VALIDATION-PREDICATE-PROBE.md` (`valprobe`),
> `46-SURGICAL-REHOST.md` (`rehost`), `48-GMMU-WALK-AND-LAUNCH-AUDIT.md`
> (`gmmu_walk`, `launch_audit`), `45-RM-RPC-CAPTURE-AND-REPLAY.md`
> (`rm_capture`), `19-CONTROL-DISCOVERY.md`, `40-NEW-VERSION-TRIAGE.md`,
> `25-VALUE-VALIDATION.md`, `27-TOOL-AUDIT.md`, `49-SIMULATION-SURFACE-MAP.md`,
> the private simulator handoff
> [`../../../../handoff-simulator.md`](../../../../handoff-simulator.md)
> §30–33 (read it when available; agents without private access skip it), and
> `open-iov/docs/eng-ops.md` §2/§6 (admission and automation safety).

## 1. Why this exists: wall-hell has a shape

The GR campaign's dominant cost is **wall-hell**: one blocking problem after
another, each paying supervised hardware cycles (5–6 min each, plus fail-safe
discipline) to learn one fact. The toolset now solves several wall classes
offline and deterministically (`docs/25` §3 records the measured value), but
knowledge kept only as prose is re-learned by the next agent and re-tested on
silicon by the next campaign. This document fixes two things:

1. **A wall is classified before it is worked.** Each wall belongs to exactly
   one of six classes; only the tool that measures that class may answer it.
   Most expensive wall errors are *domain-crossing inferences* (section 3).
2. **A wall is not closed until it is a contract.** The answer becomes a
   declarative, re-runnable check over the existing tool entry point
   (section 6), so the next firmware bump or tool change is caught by
   `make test` instead of another cycle.

The registry is a **consumer** of proven tools, not a new probing capability:
it wraps `valprobe`, `rehost`, `gmmu_walk`, `launch_audit` and `rm_capture`
entry points as-is (docs/49 §4 lists their proven value).

## 2. Wall taxonomy — six classes

| Class | The question it covers | Measures it DIRECTLY | Must NOT be used to infer it | Artifact a correct answer leaves |
|---|---|---|---|---|
| **a. firmware boot/status** | Did the firmware reach rung Bx? Where is it stuck, with what stop reason/status word? | `sim/gsp_boot.py` rungs B0–B3, `harness/triage.py` (identity/probe/native_boot), probe sessions, `greeneye probe` first-fault report | engine memory tools (`gmmu_walk`, `launch_audit`) and predicate probes (`valprobe`) | `greeneye-session/1` with the rung, stop PC/status and first-fault address |
| **b. RM server behaviour** | What does the server read/write/wait on for this input; which branch/gate decides accept vs refuse; what state does a handler need? | `valprobe` (one firmware predicate branch with crafted state), `rehost` (one whole function; first missing state is the finding), `rm_capture` decode for what the client actually sent | engine-execution claims from hooks/predicate verdicts; `gmmu_walk`/`launch_audit` for server logic | valprobe/rehost report + session: entry, seeded state, stubs, labelled outcome, stop/fault |
| **c. engine memory contract** | Can the engine reach each leg of this submission (ring, QMD destination, param/program, release slot, semaphore) with the required access, and at which PA? | `launch_audit` (per-leg verdict against the engine's table view), `gmmu_walk` (the leaf mapping behind one VA) | host shadow bookkeeping as proof of engine reachability; server-side hooks; `valprobe` | `greeneye-launch-audit/1` spec+report with per-leg `ok`/`pa_mismatch`/`unmapped`/`access_denied` |
| **d. engine execution/dispatch** | Did the front-end/engine consume the entry, dispatch the method, write the release/semaphore? | Supervised capture + post-mortem decode (the only authority); `launch_audit` answers only its *address* leg | anything in this tool: no GR/PBDMA model exists by design (`docs/49` §6); page tables cannot prove method dispatch; a silent ring cannot be inferred from an all-`ok` audit | capture with the engine-side consumption evidence (GPFIFO GET/PUT movement, method/QMD execution, release/semaphore state) + post-mortem |
| **e. guest-driver/protocol interface** | What did the guest driver send (fn/cmd/params), and does a replay/another version differ? | `rm_capture` decode/compare/stimulus (send-side logs), guest diagnostics (`open-iov/tools/guest-diag`) | firmware predicate/branch results as a substitute for the driver's wire traffic; `gsp_boot` rungs | `greeneye-rm-rpc-capture/1` + `greeneye-rm-rpc-compare/1` and a stimulus JSON |
| **f. version skew/portability** | Did the image/code/behaviour move between versions, and which change explains it? | `harness/triage.py` (full chain), `harness/version_diff.py` (sections + symbols + M1–M6 skeleton), `./risc-v-gsp-rm-debugger.sh probe <image>` first-touch diff | one version's green run as portability proof; a `skipped` step read as a pass | triage report + version diff + one recorded `compare` session pair (self-diff zero) |

Two rules fall out of the table:

* **Class (d) has no offline tool, by design.** Do not attempt to simulate it:
  the simulator makes no L2/L3 claims (`docs/06`). The offline contribution is
  the *address leg* (class c) and the *server leg* (class b).
* **A wall usually names its own class in one sentence.** If two classes seem
  to fit (e.g. "the launch is silent"), split the question: address leg →
  (c), method execution → (d), server prewrite → (b). One wall = one class =
  one decidable question.

## 3. The evidence ladder and the no-cross-domain rule

### 3.1 Observe → classify → model → falsify → contract

| Stage | What happens | Exit test |
|---|---|---|
| **1. Observe** | Collect only evidence that can discriminate: one bounded session/probe/capture, named stimulus, recorded artifacts | The observed fact is replayable and has a session/report path |
| **2. Classify** | Assign exactly one wall class (section 2) and name the metric the question is really asking (M1–M6, `docs/06` §5) | The class's DIRECT tool exists and is reachable offline; if not, record the gap (section 10) |
| **3. Model** | Run the class's tool with crafted/captured state (predicate branch, rehost, walk, audit, decode) | A result that could have come out the other way (a verdict, not a confirmation) |
| **4. Falsify** | Try to break the model: inverse variant, mutated spec, second run for determinism, one-bit differential (`docs/14`) | The falsifier fails to overturn the model; the determinism `compare` is empty |
| **5. Contract** | Pin the decisive run as a registry contract with an explicit expectation | `python3 harness/run_contracts.py --fast` passes and the contract can fail if the tool changes |

The ladder is the OODA loop of `docs/15` made runnable: model is Orient,
falsify is Decide, contract is Act/regress. Skipping stage 4 is how a
misread wall survives (the FECS refusal was initially misread as a V6
limitation until the predicate matrix falsified it; handoff PART 95).

### 3.2 Never infer across domains

The rule is absolute for claims that would change the product:

* **Host bookkeeping cannot prove engine execution.** The engine may read a
  different PA than the one the post-mortem checks — that is exactly what
  `launch_audit`'s `pa_mismatch` exists to expose. Only a capture shows what
  the engine did (class d).
* **Page tables cannot prove method dispatch.** `gmmu_walk` proves a mapping
  exists; a silent launch with all legs `ok` means the silence is downstream
  of translation (front-end/engine/context), not that the method ran
  (`docs/48` §3).
* **A predicate verdict cannot prove the whole handler path.** `valprobe` runs
  one branch with the minimum state; the full handler may early-out earlier
  or additional gates may exist downstream (`docs/47` §2; `docs/46` §5).
* **A decoded client record cannot prove what the server replied.**
  `rm_capture` is send-side; captures currently have no reply sequence
  (`docs/45` §7).
* **A demo-surface result is not RM state.** `control_discovery`/`reach` on
  the demo surface classify demo dispatch; the RM surface waits for H1.3/H2.2
  (`docs/19` §9).
* **One version's behaviour is not portability.** A new image requires the
  class-(f) chain, even when one scenario passes.

Every claim in a handoff/write-up carries its class and its tool so a reviewer
can see the domain it came from.

## 4. Per-tool honesty table

Wraps the audits in `docs/27` and the limits in each tool doc. "L0/L1" means
instruction/memory fidelity only; no timing (L2) and no device-environment
(L3) claim (`docs/06` §2).

| Tool | What it MEASURES | What it does NOT measure | Known failure modes |
|---|---|---|---|
| `valprobe` (docs/47) | The branch one firmware predicate takes with crafted register/memory state plus at most one recorded stub; the verdict is a labelled outcome address | Whole-handler behaviour, RM object state, boot state, timing | Wrong entry/state ⇒ `fault` (first missing state) or `unlabelled` outcome; a stub can mask a dependency that would change the branch; crafted state is not what a live caller supplies |
| `rehost` (docs/46) | One bounded firmware function with crafted args/memory/snapshots; the first missing state is the finding | Service loops, interrupts/scheduling, MMIO semantics, timing | `budget`/timeout usually means entry is mid-function or loops; argument conventions must be caller-supplied; lenient unknown MMIO can mask environment dependence |
| `gmmu_walk` (docs/48) | The leaf PA/page-size/aperture/access for a VA through a raw table view; exact fault otherwise | Access ordering, execution, timing; video-memory high bits (`pa_complete: false`) | Wrong root/view ⇒ fail-closed faults; 64K dual path is modelled, not live-validated; incomplete view reports `unmapped`, never "unreachable" |
| `launch_audit` (docs/48) | Per-leg class of a submission's engine-visible memory contract vs host bookkeeping (`ok`/`pa_mismatch`/`unmapped`/`access_denied`) | Whether the engine actually executed/dispatched; anything downstream of the address path | Needs a real capture spec; missing table pages read as `unmapped` (capture error, not engine truth); no fixture ⇒ demo only |
| `rm_capture` (docs/45) | Decode of real client RPC log tags into records; compare of two captures; replay stimulus preparation | Server replies/event ordering; handles/addresses (omitted from stimuli); anything >192 B payloads until the helper chunks | Unknown tags/truncated payloads (`truncated: true`) are not replayable; send-side only; caller-address symbolisation deferred |
| `control_discovery` / `reach` (docs/19) | Unknown command-id classification on a surface; a reachability route with bounded timeout and required args | RM object state/behaviour (surface waits for H1.3/H2.2); dead-code proofs | A timeout is "not reached under this stimulus", never unreachability; long handlers may classify by entry hit with empty effects; trap/fault cause mapping is a documented fidelity gap |
| `triage` / `version_diff` (docs/21, docs/40) | Image identity/sections/symbols/probe/first-touch and M1–M6 diff between two versions | Silicon behaviour; a raw `.fwimage` boots only to its early fault by design; `skipped` is not `pass` | Missing baseline ⇒ `version_diff` step `skipped`; RM 610 refuses without human approval (exit 3); first-touch differences need attribution to profile vs logic before any conclusion |

## 5. Capture-request discipline: one capture, one decidable question

Supervised captures are the scarcest resource; a vague request burns a cycle
and still leaves ambiguity. The rules:

1. **State the question as one falsifiable sentence.** "Does the engine's PDB
   resolve the inline-QMD destination VA to the host shadow PA?" — not
   "capture more launch data".
2. **Write the acceptance test before asking.** Name the tool and the exact
   report field that will decide it (e.g. `launch_audit run --spec` leg
   verdict; `rm_capture compare` row deltas). If no existing consumer parses
   the data, the capture is not ready.
3. **List the exact pages/registers, byte-exact.** Prefixes without
   pretty-printing: PDB root, each level (PDE2/PDE1/PDE0), the leaf table(s),
   the submission pointers (GPFIFO ring, `SET_INLINE_QMD_ADDRESS_A/B`, QMD
   param/program/release-slot, report semaphore), and the shadow/chunk pages
   the engine might write. A well-formed example: the launch-audit request
   that listed the channel PDB tree + the `rmcall_gr_shadow` chunk DMAs
   (simulator handoff §32; the private request holds the concrete PA list).
4. **Include the comparison basis.** The host/shadow bookkeeping for the same
   VAs, so `pa_mismatch` is decidable; a second consumer's view for the same
   object if the question is interface alignment.
5. **One question per capture.** Two questions ⇒ two lists; bundling makes a
   partial answer unreadable.
6. **Prefer the existing ingestion format.** Raw pages → `greeneye-launch-
   audit-spec/1`; RPC logs → the `rm_capture` tag grammar
   (`harness/rm_capture.py --print-capture-hints`). Do not invent a format
   that no tool reads.
7. **On a failed capture, record the fidelity gap, not a guess.** Missing
   pages or truncated payloads become a new request or an unknowns-ledger row
   (section 8), never an attribution.
8. **Gates.** The capture itself is supervised, human-run physical work
   (`SIMULATOR-WORK-BOUNDARY.txt`); simulator tooling only prepares the spec
   and reads the artifact afterwards.

Anti-patterns: "capture more logs" (no acceptance test); pretty-printed
tables instead of raw bytes (breaks byte-exact ingestion); one dump for two
questions; capturing without the host-side bookkeeping map (nothing to
classify against); re-capturing because the previous request lacked the
release slot PA.

## 6. The contract registry

### 6.1 Concept

Every solved wall becomes a **contract**: a declarative record that pins the
proven tool entry point and the expectation observed when the wall was
solved. New walls run the registry first - a failure localises the regression
to one class in seconds; only then is a new probe/capture justified.

| Contract field | Meaning |
|---|---|
| `name` | stable id, e.g. `fecs-predicate-matrix` |
| `wall_class` | one of a–f (section 2) |
| `doc` | the tool/wall documentation reference |
| `entry` | the exact existing entry point wrapped, e.g. `harness.valprobe:run_spec(fecs_spec())` |
| `expect` | the pass condition in words (falsifiable) |
| `speed` | `fast` (runs in `make test`) or `slow` (only `--all`/`--name`) |
| `requires` | input paths; absent ⇒ `skip`, never `pass` |

Rules for adding one: wrap an **existing** entry point (no new measurement
logic); the expectation must be able to fail; keep fast contracts small
(seconds total); one wall class per contract; link the doc; and if the wall
has a public write-up, link it too. A contract without a falsifier is prose.

### 6.2 Commands

```bash
python3 harness/run_contracts.py                     # fast contracts (make test path)
python3 harness/run_contracts.py --all               # fast + slow
python3 harness/run_contracts.py --json dumps/contracts.json
python3 harness/run_contracts.py --fast --name gmmu-golden-vector   # single contract
python3 -m unittest tests.test_contracts -v          # fast contracts as a test
```

The runner prints pass/fail per contract and per-wall-class coverage (classes
with zero contracts are shown, so gaps stay visible); exit status is nonzero
if any selected contract fails; a `skip` is a missing prerequisite, not a
pass. Schema: `greeneye-contract-run/1`.

### 6.3 Shipped contracts (2026-10-06)

| Contract | Class | Wraps | Expectation | Speed |
|---|---|---|---|---|
| `fecs-predicate-matrix` | b | `harness.valprobe.run_spec(fecs_spec())` | 15/15 PROMOTE_CTX predicate variants labelled, 0 failed | fast |
| `fecs-predicate-determinism` | b | `harness.valprobe.run_demo()` | matrix twice, identical verdicts | slow |
| `rehost-demo` | b | `harness.rehost.run_demo()` | demo function returns the expected sum twice | fast |
| `gmmu-golden-vector` | c | `sim.gmmu_walk.run_demo()` | 5/5 captured VAs → logged DMA addresses | fast |
| `launch-audit-captured-contract` | c | `harness.launch_audit.run_demo()` | captured contract all `ok`; QMD hypotheses yield `pa_mismatch` + `unmapped` | fast |
| `rm-capture-decode-demo` | e | `harness.rm_capture.run_demo()` | synthetic capture decodes/compares/yields stimulus | fast |

Coverage gaps, stated honestly: class **a** and **f** have tools (`triage`,
`version_diff`, boot rungs) but no contract yet because a meaningful fast
expectation needs a pinned baseline pair (that is the queued golden-matrix
build, handoff §30); class **d** has no offline contract by design (section
2). Classes b/c/e are covered by the five fast contracts; `make test` runs
them.

## 7. Admission note (eng-ops §2)

The registry/runner is admitted per `open-iov/docs/eng-ops.md` §2:

| Field | Value |
|---|---|
| **Scenario** | Wall-directed loop: after a wall is solved offline, the answer must survive as a regression; before a new wall is worked, the known walls are re-checked; and every firmware/tool change must show whether a solved wall moved. |
| **Measurable outcome** | `greeneye-contract-run/1` summary: pass/fail/skip per contract + per-wall-class coverage; exit code and JSON artifact; `tests/test_contracts.py` in the suite. |
| **Baseline** | Re-running the same demos by hand per wall, or not re-running them at all; per-tool costs are recorded in `docs/25` §3 (0.2–6.0 s per demo path vs 5–6 min per supervised cycle). |
| **Evaluation threshold** | Keep if: (1) every fast contract passes in ≤ 10 s total in `make test`; (2) each newly solved wall gets exactly one contract within the same session; (3) a deliberate tool change can make a contract fail (falsifier proven by a synthetic failing case in `tests/test_contracts.py`). |
| **Failure signal** | A contract that cannot pin a concrete expectation; two contracts measuring the same thing; a fast contract exceeding the time budget; contracts added faster than walls are solved; or a wall re-opened with the registry green (meaning the contract did not capture the decisive run). On the first signal, prune or rewrite the contract before adding new ones. |

## 8. Unknowns ledger (practice)

Open questions that no current tool answers live in an **unknowns ledger**:
one row per question, with a discriminating experiment. The ledger itself is
maintained by the campaign **outside this tool**; this document describes
only the practice. Row shape:

| Field | Meaning |
|---|---|
| Question | one falsifiable sentence |
| Discriminating experiment | the run that decides it, with the class (a–f) |
| Tool / capture | the registry entry, probe spec, or supervised capture request (section 5) |
| Status | `open` → `probe-ready` (spec exists) → `answered` → `contract` (registry) or `closed` (no action) |
| Evidence | session/report path once answered |

Rules: a row moves to `answered` only with an artifact, and to `contract`
when the decisive run can be pinned (section 6); if the experiment needs a
class-(d) fact, the row says so and waits for a supervised capture rather
than a simulator guess; when a tool that already exists answers the row, a
new tool is not built (`eng-ops.md` §2 core rule).

## 9. Worked examples

* **FECS promote wall (2026-10-06, class b).** Live refusals (`0x1f`) looked
  like a V6 channel limitation. Observe: refusal reproduced in logs.
  Classify: firmware predicate (b). Model: `valprobe` crafted variants —
  refuse iff the shared slot is non-NULL, regardless of aperture/size.
  Falsify: `slot NULL` and sysmem-attr variants accept; a second matrix run
  is identical. Contract: `fecs-predicate-matrix` +
  `fecs-predicate-determinism`. Result: the refusal is the shared one-shot
  rule, triggered by the campaign's own earlier promote; FECS is exonerated
  (handoff PART 95; `docs/47` §3).
* **Launch silence (`qmd_rel=5`, class c → d).** Classify: the address leg is
  (c), method execution is (d). Model: `launch_audit` over the captured
  channel fixture partitions `ok`/`pa_mismatch`/`unmapped`; the downstream
  question is not simulatable. Falsify: pending the real
  `greeneye-launch-audit-spec/1` raw-page capture (section 5). Contract:
  `launch-audit-captured-contract` covers the fixture today; the real-spec
  validation is handoff §31 item V1.
* **Construct/state walls (`0x40`/`0x52a8b04`, class b).** `rehost` runs the
  function and stops at the first missing state — the finding, not a defect.
  The missing piece is the RM-object state-seeding fixture (handoff §30 ask
  #1); until it exists those walls have no contract, and the registry run
  before starting them shows exactly that gap (class b has only demo/known
  inputs).
* **Engine dispatch (class d).** No offline contract exists by design. The
  registry's coverage line for class d is the reminder that the answer must
  come from a supervised capture + post-mortem, with `launch_audit` used
  only for its address leg.

## 10. Limits, status and open items

* **Status (2026-10-06).** Registry, runner and tests implemented; 6
  contracts (5 fast, 1 slow) at `greeneye-contract-run/1`; fast run ≈ 2 s;
  `tests/test_contracts.py` green. Coverage: b (3), c (2), e (1); a/f/d
  open as described in §6.3.
* The registry measures nothing new: if a wrapped tool's own demo/test is
  wrong, the contract inherits that error. The `docs/25` demos and the
  per-tool test modules remain the deeper checks.
* No timing, security or device-environment claim (L0/L1 only); injected
  code, modified images and dumps stay development-only.
* Open items: pin the class-a/f contracts once a stable baseline pair exists
  (golden matrices, handoff §30/§31); re-validate the launch-audit contract
  against the first real `greeneye-launch-audit-spec/1`; add a contract only
  when the wall it closes has an artifact.