Interface contract — pipeline boundary API

This contract is the hinge: everything below it is the checked pipeline (simulation, differential testing, trace conformance, firmware chain); everything above it (driver, GDScript bindings, web backend/frontend) talks only through these functions. Pre/post-conditions are stated, not assumed.

`add32(a: uint32, b: uint32) -> {result: uint32, flags: {cf,pf,af,zf,sf,of}}`

The arithmetic core. All upper layers use this signature.

Pre-conditions: a, b are 32-bit unsigned integers (0 ≤ a,b < 2³²). No other pre-conditions.
Post-conditions (all must hold on return):
- result = (a + b) mod 2³² (wraparound; \addmod{a}{b}{2^{32}})
- cf = 1 iff a + b ≥ 2³² (carry-out of bit 31)
- pf = 1 iff result[7:0] has even parity
- af = 1 iff (a[3:0] + b[3:0]) > 0xF (carry-out of bit 3)
- zf = 1 iff result = 0
- sf = result[31]
- of = 1 iff (carry into bit 31) XOR (carry out of bit 31)
Checked by: differential-log.txt (silicon vs C model vs GHDL, 140/140), contract-check.log (7/7 clauses × 10 vectors).

`recover(bytes) -> behavior_spec`

Recovers a behavioral specification from raw binary bytes.

Pre-conditions: bytes is a non-empty byte string; the target ISA is x86-32 (32-bit mode). For the canonical demo: bytes[0:2] = 01 D8.
Post-conditions:
- returns a behavior_spec record with fields: address, mnemonic ("ADD"), operands (dst="EAX", src="EBX"), semantics ("EAX <- (EAX+EBX) mod 2^32; update CF,PF,AF,ZF,SF,OF"), ir (%result = add.i32 %a, %b / store.i32 %result, %destination).
- the returned semantics must satisfy the add32 post-conditions above when lowered (checked by the differential oracle, not by assertion).
Implemented by: stage1 binary analysis (sample.md, sample-analysis.json); the e1 router demo feeds the decoded operation ("unsigned addition") into this contract as the ALP candidate semantics.

`verify(trace) -> verdict`

Checks a recorded execution trace against the invariants.

Pre-conditions: trace is a sequence of records with fields cycle,state,a_in,b_in,result,cf,pf,af,zf,sf,of,done; state ∈ {FETCH, DECODE, EXECUTE, WRITEBACK}.
Post-conditions: returns verdict = {pass: bool, violations: [...]} where pass is true iff the recorded trace satisfies all checks: (a) every EXECUTE row's result/flags match the add32 post-conditions; (b) flags equal values recomputed from the operands; (c) state transitions ⊆ {FETCH→FETCH, FETCH→DECODE, DECODE→EXECUTE, EXECUTE→WRITEBACK, WRITEBACK→FETCH}; (d) no privileged-state rows (vacuously true for this machine); (e) done = 1 exactly on WRITEBACK rows.
Precision: a passing verdict means the recorded traces satisfy the checks, NOT that every possible execution does (trace conformance).
Implemented by: sql-checks.sql → sql-results.txt (check-a 0/10 violations, check-b 0, check-c 0, check-d vacuous, check-e 0/0/10).

Error behavior

recover on unrecognized bytes: returns a spec with mnemonic = "UNKNOWN"; never throws, never guesses semantics.
verify on a malformed trace: pass = false with a violations entry naming the malformed record; it does not silently skip records.
add32 has no failure mode within its pre-conditions (total function on 32-bit inputs).