Execution-verify a claim (ripcord)

The ripcord thesis in its smallest unit: no claim is canonical until execution backs it. This skill is the loop that turns one decompile-derived hypothesis into an execution-verified contract — run many times, it is how the contract ledger grows. Prerequisite: the target is already in the warehouse and function-level emulatable (if not, run firmware-bringup first).

Operating rules

• Confidence discipline. Separate what the firmware did (observed: register/memory/MMIO deltas in the trace) from what a stub invented (a reply value — unverified until hardware). Separate an internal selector/dispatch code from a wire-level hardware transaction. Never log an inferred reply as fact. (See notes/confidence-scheme.md.)
• One claim per cycle. A contract is a single falsifiable statement with a spec you can run. If the claim is compound ("the engine does X, Y, and Z"), split it — each part promotes or refutes on its own evidence.
• A refutation is a result, not a failure. If the trace contradicts the claim, record the correction with a supersedes link to the wrong contract. A wrong turn is a row with a pointer, not a silent edit.

The loop

1. State the claim as one falsifiable sentence with a concrete, observable prediction (a byte on a bus, a value at an address, a call edge taken).
2. Find the entry + context. Locate the function/region (scripts/query over functions / peripheral_xrefs; scripts/analysis/disasm.py for the prologue). Determine the register context and any memory globals the real caller/boot would have set. For a handler reached past a blocking primitive, enter post-receive and stage inputs via --mem (see the technique catalog in the firmware-bringup skill).
3. Run it. scripts/renode/emulate_function.py --target T --entry <pc> --stop <after-the-observable> --reg <ctx> --mem <globals/inputs> --run. Cap --duration/--timeout; if it spins, the trace explodes — diagnose the stall (a poll on an unmodeled peripheral, a scheduler yield) and either model it or NOP-patch past it (--mem 0x<callsite>=0xBF00BF00).
4. Diff the trace against the prediction. Read the mmio_events summary and the raw build/<T>_fn_*_trace.log: the exact bytes on the bus, the contiguous SRAM writes, the dispatch target taken. Match or mismatch is the verdict. Delete the trace when done.
5. Record the contract. Update the ledger at build/contracts.sqlite:
   • inspect: scripts/contracts/ledger.py list / show <id>;
   • a claim enters decompile-derived; running its spec is what promotes it to provenance='execution-verified' (scripts/contracts/ledger.py verify <id> where a runnable spec exists). New contracts / appended evidence are added through the ledger's Python API (add_contract) or, for an evidence append on an already-verified contract, a direct SQL UPDATE of the evidence field (the ||-delimited append pattern). Tag the new evidence with date, the exact emulation command, and what was observed vs. still inferred.

Output

Report: the claim, the emulation invocation, the decisive trace evidence (bytes/addresses), the verdict (confirmed / refuted+corrected / partial — and exactly which part remains decompile-derived or hardware- bound), and the ledger contract id touched. If the claim concerned a hardware-boundary reply value the stub supplied, say so plainly: structure is execution-verified, the value is not — that is the hardware ceiling, see HARDWARE_HANDOFF.md.