diff --git a/Makefile b/Makefile index a4b05b507..7a8b309a1 100644 --- a/Makefile +++ b/Makefile @@ -630,6 +630,36 @@ fmt: cargo fmt --all # Run clippy + fmt check (used by CI) +.PHONY: verify-dma +verify-dma: ## Run the DMA memcpy formal-verification gate (formal_verification/dma) + @# Oracle anchors + vector emission, the z3 soundness gate, and the + @# transcription audit. Needs `pip install z3-solver` (validated on 5.0.0); + @# the audit alone needs no solver. + @# Exit codes: 1 = failure (abort), 2 = ran but degraded (an external anchor + @# was unavailable). Only 1 should stop the run -- otherwise a machine without + @# a loadable libc would skip the audit and the gate, neither of which needs it. + python3 formal_verification/dma/test_ref.py || [ $$? -eq 2 ] + python3 formal_verification/dma/audit_transcription.py + @# The gate, then a freshness check on its committed transcript. Without the + @# diff, `verify.log` is a claim about a run nobody repeats -- it could drift + @# from the gate silently, which is the same "declared, not derived" defect the + @# audit script exists to catch. The `solver:` line is excluded because it names + @# the local z3 build: pinning it would turn any version bump into a spurious + @# red, and a spurious red is how a check gets deleted rather than fixed. + @out=$$(mktemp); st=$$(mktemp); \ + { python3 formal_verification/dma/z3_verify.py 2>&1; echo $$? > $$st; } | tee $$out; \ + if [ "$$(cat $$st)" != "0" ]; then rm -f $$out $$st; exit 1; fi; \ + grep -v '^ solver:' formal_verification/dma/verify.log > $$out.committed; \ + grep -v '^ solver:' $$out > $$out.fresh; \ + if diff -u $$out.committed $$out.fresh; then \ + echo " verify.log matches this run."; \ + else \ + echo " FAIL: verify.log no longer matches the gate. Regenerate with:"; \ + echo " python3 formal_verification/dma/z3_verify.py > formal_verification/dma/verify.log"; \ + rm -f $$out $$st $$out.committed $$out.fresh; exit 1; \ + fi; \ + rm -f $$out $$st $$out.committed $$out.fresh + lint: cargo fmt --check --all cargo clippy --workspace --all-targets -- -D warnings -A clippy::op_ref diff --git a/formal_verification/dma/README.md b/formal_verification/dma/README.md new file mode 100644 index 000000000..8b20a3f5b --- /dev/null +++ b/formal_verification/dma/README.md @@ -0,0 +1,618 @@ +# DMA memcpy — oracle + z3 gate + +Machine-checks that the DMA memcpy chip (PR #874) copies the bytes it claims to. +Same home and shape as `formal_verification/keccak/` (PR #923): one flat +directory per verified chip, one README carrying the method, a committed run log. + +**Verification code only — no constraint, trace or performance change.** The one +exception is `prover/src/tests/dma_tests.rs`, which consumes this directory's +emitted fixture, plus a `#[cfg(test)]` accessor in `prover/src/tables/trace_builder.rs` +and a `verify-dma` target in the `Makefile`. + +```sh +make verify-dma # all three, from the repo root +pip install z3-solver # the only dependency; validated on 5.0.0 +``` + +**The degraded-run contract**, because a CI job or a human greps for the word +`VALIDATED` and a partial run must not print it bare: + +| exit | meaning | +|---|---| +| 0 | full board green, or `--quick` green (status token says `VALIDATED (--quick, reduced sweeps)`) | +| 1 | a real failure — a mutant survived, an anchor disagreed, or a solver returned `unknown` | +| 2 | **ran but degraded**: an external anchor was unavailable. Status token says `PARTIALLY VALIDATED (n anchor(s) skipped)` | + +A missing dependency SKIPs only its own anchor and never cascades, the banner +names the anchors it is *not* anchored on, and **a mutant whose target anchor +skipped is reported `NOT RUN`, never `caught`** — scoring a skip as a catch +credits a mutant to a check that never ran, which is exactly what happened until +it was fixed: an unloadable libc printed `PASS all 8 mutants caught` while +running six. `make verify-dma` tolerates exit 2 and aborts on exit 1. + +The gate scores `unknown` as **failure** everywhere. On z3 5.0.0 the full board +is ~92 s; on 4.12.2 it takes ~1210 s and two queries blow their budgets, so a +solver timeout is reported as `TIMEOUT` and distinguished from a rejection — an +earlier version would have printed "the AIR REJECTS an honest row" on a slow box. + +| file | what it is | +|---|---| +| `dma_ref.py` | the oracle: four levels of reference model, no repo code | +| `test_ref.py` | anchors the oracle against libc and CPython; emits the fixtures | +| `tamper_test.py` | are those anchors sensitive? eight deliberate defects | +| `z3_verify.py` | the gate: field-exact model of the AIR | +| `audit_transcription.py` | 104 claims tying gate, spec and Rust together | +| `verify.log` | the gate's own output, committed | +| `canonical_dma_rows.txt` | pinned vectors, `include_str!`-ed by the Rust test | +| `canonical_dma_vectors.json` | the same vectors with full per-row column expansions | + +## Results + +``` +oracle: [1] libc memmove PASS 3855 cases x overlap/alignment + [2] CPython slice assignment PASS 3855 cases + [3] row/bus level <-> byte level PASS 257 lengths x 15 overlaps + [4] guest stub chunking PASS 1100 lengths + [5] tamper tests PASS 8/8 mutants caught + VALIDATION STATUS: VALIDATED + +gate: layer 1 (row semantics) PASS 6/6 UNSAT + layer 2 (chain structure) PASS 4 integer + 2 field-exact UNSAT + layer 2 controls PASS 4 positive + 3 negative + negative controls PASS 10/10 SAT + width audit (bound necessity) PASS 6/6 + completeness sweep PASS 5153 honest + 257 padding rows + OVERALL: PASS (~92 s on z3 5.0.0) + +audit: 104 claims, 0 findings; mutation-tested against 9 source mutants +rust: cargo test -p lambda-vm-prover --lib tests::dma_tests 10 passed +``` + +Full gate transcript in `verify.log`, which is the gate's own stdout, **pasted not +retyped** — including the `solver:` line, which an earlier version silently +dropped while the surrounding sentence claimed the block was verbatim. The +`## Results` block above is hand-copied from it and nothing enforces that; if you +regenerate, replace both. + +**`--lib dma` is 18 tests, but 7 need guest ELFs** — run +`make compile-programs-rust` first (RISC-V target) or use the narrower filter +above. `make verify-dma` runs no cargo. + +## The method + +Four levels, each checkable against the next, so no level is trusted on its own. + +1. **Byte semantics** (`memcpy_ref`) — the C `memmove` contract. Anchored against + the platform libc and CPython slice assignment, 3855 cases each over every + length `0..256` × 15 overlap configurations. Genuinely non-circular: neither + shares code with this model or with the other. +2. **Row decomposition** (`row_decomposition`) — the row sequence the AIR is + obliged to contain. Written as the greedy loop the AIR actually performs + (`tail = count < 8`), *not* the closed form; that they agree is checked, not + assumed. +3. **MEMW multiset** (`memw_ops`) — three register reads at `T`, every source read + at `T+1`, every destination write at `T+2`. `replay_memw` runs this back down + to level 1 and raises if a read's recorded value disagrees with memory, so a + mis-ordered op list fails loudly instead of quietly producing the right answer. +4. **Guest chunking** (`chunk_ecalls`) — the `memcpy` stub's loop, `min(remaining, 256)`. + +The gate then models the AIR itself: **every committed column a free Goldilocks +element, every constraint an equation mod p, every lookup modelled as the +constraints of the table that receives it** — not as its advertised contract. +Assert `output != oracle(input)` and ask z3: UNSAT means the row does what the +oracle says; SAT is a counterexample. A bit-vector model cannot do this job — the +question is whether a range check is *missing*, and BV silently bounds an +unconstrained column, so the bug disappears. + +Two layers: field-exact single/paired rows prove the row abstraction, then a +multi-row layer takes that abstraction and models `DmaNext` as a **free bijection** +between senders and receivers rather than an assumed chain — which is where +"a source row skipped forward", "the copy ended early" and "a disjoint cycle also +balances the bus" get answered. + +## The oracle's independence, and its limits + +Anchors 1 and 2 are genuinely non-circular: the platform C library and CPython's +`bytearray` slice assignment are two `memmove` implementations sharing no code with +`dma_ref.py` or with each other. libc in particular is the definition the guest's +`compiler_builtins` `memcpy` was replacing, which makes it the right anchor rather +than a convenient one. Anchor 3 is the one the chip depends on and has no external +counterpart — it is the only check that the row sequence the AIR proves is the byte +copy the guest asked for. Anchor 5 (the tamper sweep) is what makes 1–4 worth running. + +**The one thing the reference is not independent of: the row decomposition itself.** +The greedy `8-while-≥8-then-1` rule is a design decision, and the oracle transcribes +it from the same place the AIR gets it. What the oracle proves is that this +decomposition *implements the byte copy*; it cannot tell you the decomposition is +the right one, and it would not catch a design where both the AIR and the oracle +chunked differently but consistently. That is why the Rust test +`dma_trace_matches_oracle_row_decomposition` exists — it pins the trace builder's +decomposition against the emitted vectors rather than against a recomputation. + +Known limitations, carried forward verbatim in intent: + +- **O1 — the model does not model the memory table.** `replay_memw` enforces read + faithfulness at its own timestamp; it does not model per-address ordering of + *multi-byte* accesses, unaligned 8-byte operations, or the `Memw` width decode. +- **O2 — the per-ecall snapshot is not a `memcpy`-level `memmove`.** Chunk *k+1* + reads what chunk *k* wrote. Agrees with `memmove` for `dst < src` and for + disjoint ranges; disagrees for `dst > src` with an overlap wider than 256 bytes. + In contract for `memcpy` — anchor 4 deliberately excludes overlap for this + reason — but the claim "the DMA ecall has memmove semantics" must not be repeated + at the C level. +- **O3 — `value` bytes are modelled as integers, not range-checked bytes.** The + oracle emits `0..255` because it reads them out of a byte memory; the AIR gets its + byte range from the `Memw` receiver, outside both oracle and gate. +- **O4 — the anchors test the semantics, not the executor.** `dma_ref` is a model of + `execution.rs` checked against libc; that `execution.rs` matches it is covered by + the PR's own 256-case proptest and `executor/src/tests/dma_tests.rs`, not by + anything here. +- **O5 — register reads are modelled as three ops at `T` and nothing more.** The + old-value/old-timestamp fields, and the fact that the DMA table *writes back* the + same value it read, are not modelled. Not part of the copy semantics, but part of + the trace — the audit script is the only thing looking at them. + +### The canonical vectors + +Ten cases, chosen so every structural case appears exactly once. Regenerated by the +harness into `canonical_dma_vectors.json` (full per-row column expansion, the gate's +input) and `canonical_dma_rows.txt` (line-oriented, the Rust test's input). + +| name | dst | src | n | rows | MEMW ops | +|---|---|---|---|---|---| +| empty | 0x1000 | 0x2000 | 0 | 1 | 3 | +| single byte | 0x1000 | 0x2000 | 1 | 2 | 5 | +| one wide row | 0x1000 | 0x2000 | 8 | 2 | 5 | +| wide plus tail | 0x1000 | 0x2000 | 9 | 3 | 7 | +| widest tail | 0x1000 | 0x2000 | 7 | 8 | 17 | +| unaligned body and tail | 0x2005 | 0x1003 | 27 | 7 | 15 | +| forward overlap | 0x3004 | 0x3000 | 24 | 4 | 9 | +| backward overlap | 0x3000 | 0x3004 | 24 | 4 | 9 | +| page crossing | 0x0FFC | 0x1FFC | 16 | 3 | 7 | +| maximum chunk | 0x1000 | 0x2000 | 256 | 33 | 67 | + +"widest tail" is the expensive shape: eight rows to move seven bytes. "maximum +chunk" is the only case with **no tail row at all** — 256 is 8-aligned — which is +why it is pinned. The two files exist separately because the prover crate has no +JSON parser, and a hand-rolled scanner over nested JSON is the fragile coupling that +goes stale silently: the first attempt broke on `rows[i].columns` repeating the +`src`/`dst`/`count` keys. An earlier version hand-transcribed 7 of the 10 vectors +into Rust literals with nothing enforcing the transcription. + +## The chip, as recovered from the implementation + +`spec/dma.typ` (PR #931) is the normative chapter; this section is what the gate +checks and agrees with it except where noted. + +**Row layout.** A row copies eight bytes while `count ≥ 8`, otherwise one byte; +the design is cloned from `commit.rs` — one row per chunk, rows chained by a bus +rather than by a transition constraint. Not one row per byte: 257 rows per +maximal ecall instead of 33. Not one row per copy: the row would need `n` value +columns for unbounded `n`, and 8 bytes is the widest operation `Memw` serves. The +1-byte tail rather than 4/2/1 halving because a `tail` **bit** selects between +exactly two widths, so `step = 8 − 7·tail` stays linear and every constraint stays +degree 2; halving would need a two-bit selector and a width-to-`w2/w4/w8` decode. + +The cost, stated precisely (an earlier draft had this wrong in both directions): +`n` bytes takes `n/8` wide rows, `n % 8` tail rows and one terminal row. So tail +rows are 0% for the 8-aligned lengths that dominate, `7/39 = 17.9%` at `n = 255` +(the longest length that *has* a tail — the maximal `n = 256` has none), and +**`7/8 = 87.5%` at the genuine worst case `n = 7`**, where every data row is a +tail row. Against 4/2/1 halving the delta is at most 4 rows, not the 7 an earlier +draft claimed by comparing against a zero-tail design instead of against the +alternative it was arguing with. + +**32 columns.** `timestamp` (DWordWL), `src`/`dst` (DWordWL), `src_incr`/`dst_incr`/ +`count_decr` (DWordHL — the halfword split exists *because* they need +`IsHalfword`), `count` (DWordWL), `first`/`end`/`tail`/`mu` (Bit), `value[8]`. +(The spec says 31, typing `timestamp` as a `Word`; the Rust carries two limbs. A +spec-wide convention, not a DMA discrepancy.) + +**18 constraints, all degree 2.** Machine-measured, not declared: +`constraint_set_tests_b.rs` runs `check_table` which tree-measures every emitted +expression against `max_degree()`. + +| idx | constraint | +|---|---| +| 0-3 | `first`, `end`, `tail`, `mu` are bits | +| 4 | `(first + end)·(1 − mu) = 0` | +| 5-6, 7-8 | `src`/`dst` `+ step`, no `2^64` wrap on active non-terminal rows | +| 9-10 | `count_decr + step = count` — **the plain pair; wrap permitted** | +| 11-17 | `tail · value[i] = 0` | + +**23 bus interactions.** 1 `Ecall` receive (`first`), 2 `DmaNext` (`mu−end` send / +`mu−first` receive), 12 `IsHalfword` (`mu`), 1 `Zero` (`mu`), 3 `Memw` register +reads (`first`), 2 `Alu` LT, 2 `Memw` data ops (`mu−end`). + +### Soundness ledger — ten spots a change must not touch + +1. **`DmaNext` carries the timestamp in both tuples.** Removing it splices two + calls' rows into each other's chains with the multiset still balancing — the + failure the BLAKE3 design review found the hard way. +2. **`IsHalfword` on all twelve halfwords.** Each one is either an end-detection + forgery or a wrapped address. +3. **`emit_add_pair` (plain) on `count`, `emit_add_pair_no_overflow` on + `src`/`dst`.** Swapping either direction breaks the terminal row or admits an + address wrap. Detail below. +4. **`mu − end` on both data `Memw` sends.** Detail below. +5. **The `Alu` width pin.** Gone, the prover partitions at will and + `count = 7, tail = 0` truncates seven bytes. +6. **`tail · value[i] = 0`.** Gone, a one-byte row carries seven unconstrained + field elements into the `Memw` bus. +7. **The bound constant is taken from the executor.** `dma.rs` imports + `DMA_MEMCPY_MAX_BYTES as EXECUTOR_DMA_MEMCPY_MAX_BYTES` rather than restating + `257`, so the bound the AIR proves cannot drift from the bound execution + enforces. Restating it invites exactly that drift; the audit checks it stays + imported. +8. **One `first` per timestamp**, supplied by the `Ecall` receiver against the + CPU's single send — two heads at one timestamp would unbalance `Ecall`. This is + what makes Layer 2's "exactly one head row" a real scope restriction rather + than an arbitrary one: the bus is what enforces it, outside the gate's model. +9. **The single-`end` obligation is implicit**, not a constraint: a chain with no + terminal row has one more `DmaNext` send than receive, so the bus does not + balance. Worth knowing that this is where termination comes from — and that + bus counting alone rules out only an *open* chain, never a closed cycle. That + is item 3's second job. +10. **The `DmaNext` tuples' element alignment.** Both are 8 bus elements and align + pairwise; that is what makes the link a per-limb binding and hence what + supplies the range provenance for every non-head row. A packing change on + either side silently changes what the bus binds. Audit §G, and see + "The retracted finding". + +Three of these are asymmetries that will look like untidiness to the next reader: + +- **Constraint 9-10 is the plain add pair on purpose.** The terminal row holds + `count = 0`, `count_decr = 0 − 1 = 2^64−1`; a no-overflow form would reject it. + MAIN 2 is exactly the statement that this permission is safe — the subtraction + can only wrap where `end = 1`, because `tail` is pinned to `count < 8`. +- **Constraints 5-8 are the no-overflow form on purpose**, and for two reasons. + The obvious one: a chain could otherwise walk `src` past `2^64` and continue at + low addresses, which the executor rejects and the AIR would not. The more + important one: `src_incr = src + step` over the **integers** with `step ≥ 1` + makes `src` strictly increase, so no bijective matching can close a **ring** — + a cycle of `mu=1, first=end=0` rows would otherwise send and receive one tuple + each, balance every bus, consume no `Ecall`, and still emit a read and a write + per row. The counting argument alone ("no terminal row ⇒ one more send than + receive") rules out only an *open* chain. +- **`mu − end` on both data `Memw` sends.** This is what makes a wrongly claimed + `end` a *silent* truncation rather than an unbalanced bus, and it is why end + detection carries the weight it does. + +**End detection.** `end = 1` iff `4·65535 − Σ count_decr_i = 0`, i.e. iff all four +halfwords are `0xFFFF`. One `Zero` lookup instead of four. It rests on the +`IsHalfword` bounds — drop them and `(0xFFFF+d, 0xFFFF−d, 0xFFFF, 0xFFFF)` reaches +the same sum with a different `count_decr`, so `end` becomes claimable at a nonzero +count — and on the receiving table's **domain**: `bitwise.rs` serves `Zero[v]` only +for `v < 2^20`, and the send lands in `[0, 262140]`. + +**Value binding is structural, not proved.** The read and write tuples are built +from the same `value_columns()`; nothing needs to prove `read == write` because +there is one set of columns. On a one-byte row lanes 1-7 must be zero +(constraints 11-17) so the `Memw` tuple is the canonical single-byte encoding — +note this is *canonicalisation*, not a forgery closed: `memw.toml` gates the +per-lane memory tokens on `w2`/`w4`/`write8`, so on a tail row those lanes never +reach the memory argument at all. + +**Why the value lanes carry no range check of their own**, since this is the kind +of gap that is usually a bug. The reason is **not** that the receiving table +checks them. `spec/memw.typ:42-45` declines to: *"these properties are necessary +for the consistency of the system as a whole"* — i.e. somebody must, and it says +who only in the negative. That obligation is **A5** below. + +The actual argument is narrower and specific to this chip: the `T+1` read tuple +carries `old == value` **against real memory**, so each lane is pinned to whatever +byte the memory argument says is at that address. The lanes are not free field +elements; they are whatever memory already held. This chip *propagates* byte-ness +rather than establishing it. + +> **Do not cite `keccak.rs` as authority for relying on the receiver here.** An +> earlier draft did, and it is backwards: `keccak.rs:355-378` emits four +> `AreBytes` senders for its address bytes **precisely because** the receiver does +> not pin them, and its comment spells out the forgery — keeping a linear +> combination's field value correct while encoding non-byte values in the +> individual cells. That file is evidence for the opposite conclusion. + +**Overlap.** All reads at `T+1`, all writes at `T+2`, both AIR constants, giving +snapshot (`memmove`) semantics per ecall. **Not** per guest `memcpy`: chunk *k+1* +reads what chunk *k* wrote, so a copy over 256 bytes is a forward copy. In +contract for `memcpy`, but the `memmove` property must not be claimed at the C level. + +## Assumptions + +Obligations on the **caller**, not checks this chip performs. + +| id | assumption | discharged by | status | +|---|---|---|---| +| **A1** | `src`/`dst` limbs are 32-bit wherever a `Memw` data op fires | `spec/src/memw.toml`: `[[assumptions]] IS_WORD[base_address[i]]`. `memw.rs` justifies its own bound via *the CPU table*; DMA is a non-CPU sender | not discharged locally. Load-bearing only on the head row — elsewhere the `DmaNext` link derives it, which is why the gate's `memw_addr32` toggle is **inert and carries no control on purpose** | +| **A2** | `count` limbs are 32-bit on the head row | `spec/src/memw_register.toml`: `[[assumptions]] IS_WORD[val[i]]` | not discharged locally; `drop_reg32` shows what it buys — without it the `count < 257` lookup caps only a residue class | +| **A3** | `ts₀ + 2` stays in `Word` range | the CPU's timestamp stride is 4 and `T = 4i+4`, so it cannot carry | not discharged locally; benign at the current stride | +| **A4** | two DMA ecalls never share a timestamp | CPU timestamps strictly increase per instruction | holds by construction; it is what the `DmaNext` timestamp binding relies on | +| **A5** | domain-0 cells hold bytes | nothing here, and nothing in `memw.rs` — `spec/memw.typ:42-45` assigns it to "the consistency of the system as a whole" | **not discharged, and not DMA's to discharge.** This chip *propagates* byte-ness rather than establishing it | + +`spec/` has a broader problem: `IS_WORD` appears across 12 chapters **exclusively** +inside `[[assumptions]]`, never as an interaction or template, and no 2³² table +exists. So the spec asserts a range obligation for nearly every address, register +value and timestamp in the VM without naming a discharger. An obligation owned by +everyone is owned by nobody. + +## Padding + +`generate_dma_trace` pads to the next power of two, minimum 4, and the row is +**not** all-zero: constraints 9-10 are unconditional, so `count = 1`, `tail = 1` +(hence `step = 1`), `count_decr = 0`, and `src_incr = dst_incr = 1` because +`ADDNW`'s low-limb carry is constrained on every row. `mu = 0` kills all 23 +interactions; constraint 4 then forces `first = end = 0`. The gate's completeness +sweep pins exactly this row. + +## What the gate proves, and what it does not + +**Proves**, given the modelled contracts and given that bus balance means multiset +equality: every satisfying assignment of one row does what the oracle says; among +groups with exactly one head row, the only bus-balanced multi-row structure at +depth ≤ 5 is a single chain tiling `[src, src+n)` exactly once with the greedy +widths; ten of the eleven modelled premises are individually necessary — each has a +negative control (`drop_*`) that returns SAT, i.e. exhibits a concrete forgery, when +that premise alone is removed, and three of the ten are spelled out in full below; +Layer 2's premise set is satisfiable and sensitive to each field of the bus tuple; +and the AIR accepts every honest trace for every length `0..256`. + +The eleventh, `memw_addr32` (assumption A1), has **no control on purpose**: dropping +it leaves every check on the board unchanged, because the limb-wise `DmaNext` link +derives well-formedness from the sender's `IsHalfword` checks instead. A control that +cannot fail is worse than no control. The gate's docstring previously claimed "every +negative control shows what breaks without them", which was false for exactly this +premise. + +**On the depth bound.** The chain checks run at depth ≤ 5 (integer) and ≤ 3 +(field-exact). The general depth case is not machine-checked; it rests on MAIN 2's +wrap lemma plus the strict decrease of `count`, which together bound the chain +length. Treat depth ≤ 5 as the checked case and that argument as the reason to +believe it generalises — not as a proof that it does. + +**Does not prove**: assumptions A1–A5. The memory-consistency argument, hence +overlap ordering for unaligned 8-byte accesses — the largest remaining gap around +this feature, and not DMA's to close. LogUp soundness. The multi-call case +(Layer 2 models one head row; two ecalls are separated by the `ts` both `DmaNext` +tuples carry, which the integer abstraction does not model). And that the *Rust* +implements this — that is `audit_transcription.py`'s 104 textual claims plus the +end-to-end prove/verify and forgery tests. + +### The named forgeries — what each bound actually buys + +Each is run twice, with the bound and without, so "the bound is necessary" is a +measured claim rather than an assertion. + +| result | with the bound | without | +|---|---|---| +| `Σ count_decr = 4·65535 ⟺ count_decr = 2^64−1` | unsat (the identity holds) | **sat** — `(0xFFFF+d, 0xFFFF−d, 0xFFFF, 0xFFFF)` reaches the same sum with a different `count_decr`, so `end` is claimable at a nonzero count. An `end` row's two `Memw` sends have multiplicity `mu − end = 0`, so **it emits no memory operations at all**: a silently truncated copy with every bus balanced | +| `carry_1 = 0 ⟹ src + width < 2^64` | unsat (pinned) | **sat** — at `src1 = 2^32−1` the high half can be exactly `2^32`, which the `IsHalfword` pair forbids and an unbounded pair does not. The row hands on a *wrapped* address that the executor's `checked_add` rejects | +| the `LT` width pin blocks `count = 7, end = 1` | unsat | **sat** — a free `tail` takes `tail = 0`, so `step = 8`, so `count_decr = 7 − 8 = 0xFFFF…`, so `end = 1`. **Seven requested bytes silently not copied** | + +The last one is worth reading twice. `end` requires `count = step − 1`, so a free +`tail` buys exactly `count = 7` and no other value — the two constraints compose to +leave precisely one hole. That is also why an earlier draft wrote this forgery at +`count = 3` and was wrong: it is not reachable there. + +### Which mechanism rejects each shipped forgery + +The four forgery tests in `prover/src/tests/prove_elfs_tests.rs` only observe that +verification fails. The gate says *which mechanism* blocks each — the more useful +fact, and the one that tells you what a future refactor would break. + +| shipped Rust forgery test | what it perturbs | the mechanism that rejects it | gate check | +|---|---|---|---| +| `forged_early_end_rejected` | `END := 1` on a data row | the `Zero` lookup (the sum no longer reads zero) **and** the three sends gated on `mu − end`, which vanish — so `DmaNext` and both `Memw` buses unbalance too. Not the `Zero` bus alone, as an earlier version of this table said | MAIN 1, and its `drop_zero_end` / `drop_halfword_count_decr` controls | +| `forged_wide_tail_rejected` | `TAIL := 1` on a wide row | **overdetermined — at least five independent mechanisms reject it.** Row-locally: `step = 8 − 7·tail` breaks the *ungated* idx-9 `emit_add_pair` on `count`; idx 5-6 and 7-8 fail identically; idx 11-17 (`tail·value[i] = 0`) fail whenever the eight copied bytes are not all zero. On the buses: the `Alu` width pin (bus 20, multiplicity `mu`) sends `[count, 8, 0, LT, TAIL, 0]`, so with `TAIL = 1` on a `count ≥ 8` row it asks `lt.rs` for output 1 where that table holds 0 — no matching row, `Alu` unbalances; and `w8 = 1 − tail` changes the `Memw` width | MAIN 0 | +| `forged_intermediate_source_rejected` | `SRC_0` **and** `SRC_INCR_0` shifted together | **nothing row-local** — the row's own ADD stays satisfied. The predecessor's `DmaNext` tuple no longer matches, and the source read no longer matches memory | CHAIN / CHAIN-F, exactly the check that treats `DmaNext` as a free bijection rather than an assumed chain | +| `forged_value_rejected` | `VALUE[0]` | **not the copy relation** — read and write still agree with each other, because they are one set of columns. What rejects it is the `Memw` read no longer matching memory | **none.** Audit §D pins the one-set-of-columns wiring; no solver query establishes this one | + +Two rows repay attention. `forged_intermediate_source_rejected` is the case where +per-row soundness is genuinely insufficient and the chain argument does the work — +which is why the gate builds the bijection model instead of assuming rows are +chained. And `forged_value_rejected` passes for a reason **no solver query +establishes**: the only thing behind it is a textual fact about how two bus tuples +are constructed. That asymmetry is why the gate and the audit are separate artifacts. + +> **How the `forged_wide_tail` cell got written, kept because it is instructive.** +> An earlier version credited the `Alu` width pin alone. A review called that +> incomplete, and the replacement over-corrected into *"**Not** the `Alu` width +> pin"* — which is false; the pin does reject it, by the argument in the cell. The +> chain was: a finder wrote "the Alu lookup is not what blocks it", that was +> accepted without checking, and it was then sharpened into an explicit negation. +> **An overstatement became a falsehood by being propagated.** When a mechanism is +> overdetermined, "X rejects it" and "Y rejects it" are both true, and the tempting +> edit — replacing one with the other — is the one that introduces the error. +> Prefer "at least these", never "not that". + +## The transcription audit + +The gate proves things about a **model**. Everything it proves is worthless if the +model and `prover/src/tables/dma.rs` have drifted, and the dangerous direction is a +model **stronger** than the object it models: it yields UNSAT where the real table +is forgeable, and no positive anchor can catch it, because honest inputs satisfy a +correct model and an over-strong one equally well. + +`audit_transcription.py` therefore reads the Rust and asserts, textually: + +``` +A. constants 10 every number the oracle and gate hard-code +B. columns 28 the full dma::cols layout, NUM_COLUMNS, density +C. constraints 10 each index, template, operands, the degree bound, and that + no index exists the gate does not model +D. buses 23 23 interactions, bus mix, every multiplicity, and the wiring + facts the gate cannot see +E. executor 5 the ecall validates what the oracle validates, in that order +F. generator 7 the padding row is the row the oracle describes +G. bus packing 17 element counts per Packing, and DmaNext tuple ALIGNMENT +H. fixture 4 the Rust test consumes the oracle's current output +``` + +Counts are **printed by the script**, not documented by hand — an earlier version +stated them in prose and got five of six wrong, apportioned to sum to the real +total instead of measured, which is the "declared, not derived" defect this file +exists to catch. + +It is deliberately textual rather than a Rust test: the point is to catch a change +in `dma.rs` that nobody reflected here, and a Rust test would be edited in the same +commit as the code it guards. Source is whitespace-normalised before literal +matching, so a `rustfmt` reflow does not produce a spurious red — which matters, +because a spurious red is how a check gets deleted rather than fixed. + +**Mutation-tested, and it needed it.** An audit that cannot fail is not an audit. +Nine semantic mutants plus one must-not-fire control, applied to copies of the +**Rust** source with the script re-run. (Distinct from `tamper_test.py`'s eight +mutants, which perturb the **Python oracle** to test the anchors — two separate +regression sets, and both happen to be about the same size.) + +| mutant | findings | notes | +|---|---|---| +| `timestamp_with_offset(2)` → `(1)` on the write tuple | 1 | | +| the write tuple's `value_columns()` → eight zero constants | 1 | | +| one `halfword(cols::COUNT_DECR_0)` send deleted | 3 | | +| `DMA_MEMCPY_MAX_BYTES + 1` → `+ 2` in the bound lookup | 1 | | +| the executor's `if n > DMA_MEMCPY_MAX_BYTES` guard → `if false` | 1 | **initially missed** — needed a strengthened check | +| `num_bus_elements(DWordHL)` `2 → 1` | 2 | **initially missed entirely** — this is the gap R1 came through | +| `num_bus_elements(DWordHHW)` `2 → 1` | 2 | added later: the first §G guard was **dark for this arm** (see below) | +| `DmaNext` receiver tuple reordered (`SRC_0`↔`DST_0`) | 1 | **initially missed** — §D pinned membership, not order | +| `DmaNext` sender tuple reordered (`SRC_INCR_0`↔`DST_INCR_0`) | 1 | **initially missed**, same cause | +| a `rustfmt`-style reflow of `if tail { 1 } else { 8 }` | **0** | must NOT fire | + +**Four of the nine were initially missed, in a file whose entire job is catching +exactly this.** The causes are worth naming because they are all the same species — +a check that cannot fail: + +- The executor mutant: the check asserted the `DmaMemcpyChunkTooLarge` variant + appeared *before* the `checked_add` calls, which a guard rewritten to `if false` + satisfies. It now requires the literal predicate. +- The packing mutants: §D checked only that the strings `DWordWL`/`DWordHL` + *appeared* in the two tuples, never that their element counts aligned. §G exists + now, and **it took three tries to make live** — which is the most on-thesis fact in + this file. The first searched ASCII `2x` where the source writes `2×` (U+00D7), so + it could never match. The second searched `Packing::\w+ => 1, // 2×`, matching only + arms whose comment *begins* `2×` — dark for `DWordHHW` ("Direct + Word2L") and + `DWordWHH`, both equally 64-bit, which is why the `DWordHHW` mutant is in the table + above. The third keys off the source's own `// Compounds` section marker, so all + seven compound arms are covered and a newly added variant is covered by default. + A guard written to close a gap was itself dark, twice, in a row. +- The two ordering mutants: bus tuples were pinned by membership and not by ordinal + position, so a swap silently re-paired every field the gate models. + +**The reflow mutant must produce zero findings, and used to produce two.** The +literal checks match fragments like `if tail { 1 } else { 8 }`, and `rustfmt` breaks +those across lines the moment one grows past `max_width`. The original guard, +`src.replace("\n", " ")`, collapsed the newline but left the indentation, so it +could never match a reflowed form. `read()` now whitespace-normalises. This matters +because the script is meant to run unattended: **a spurious red is how a check gets +deleted rather than fixed.** + +## Lessons worth carrying to the next gate + +**Model the receiving table's constraints, not its advertised contract.** The gate +models `Alu[a,b,LT] → o` as `lt.rs`'s own columns and carries rather than as +`o = (a < b)`. Apply the same rule to the **bus itself**: "how many field elements +does this value cross the bus as?" is a premise like any other and must be read +from `num_bus_elements()`, never assumed. That one omission produced a phantom +finding published as this campaign's headline result — see below. + +**Classify the direction of every modelling gap.** Weaker than the AIR ⇒ false +alarms, never false proofs. Stronger ⇒ false proofs no positive anchor can catch. +Say which, in the verdict. + +**Pair each negative control with the check that premise is load-bearing for.** +Dropping a premise and re-running a check whose reference never mentioned it yields +UNSAT — a control that cannot fail. Three of the original eight had this bug. And a +multi-row check needs its *own* positive control: `Not(property)` returning UNSAT is +worthless if the premise set is unsatisfiable. + +**Never negate a modular equality carrying a witness quotient.** `Not(a − b == k·m)` +is satisfiable by picking a nonzero `k`. Spell such claims out witness-free. + +**Field-exact, over integers, linear.** Columns are `Int` in `[0, p)`, modular +equalities carry explicit quotients, and `x·(1−x) = 0` becomes `x ∈ {0,1}` (exact +for `x < p` prime). The naive `%p` encoding is nonlinear and timed out on the main +check; this rewrite is what made a 5410-row completeness sweep affordable. + +**When a mechanism is overdetermined, prefer "at least these", never "not that".** +A forgery rejected by five independent mechanisms invites the edit that credits one +and denies another — and that edit is how an incomplete claim becomes a false one. + +## The retracted finding + +An earlier version reported a residual — that `count`'s limb split was +unconstrained on non-head rows — and made it the headline across five documents. +**It was wrong**, and the story is the most transferable thing here. + +`DmaNext` does not compare packed 64-bit values. `Packing::num_bus_elements()` +returns **2** for both `DWordWL` ("2× Direct") and `DWordHL` ("2× Word2L"), each +element gets its own alpha power, and **no `Packing` variant contains a 2³² shift** +— so a 64-bit value is never one bus element anywhere in this codebase. Both tuples +are `1+1+2+2+2 = 8` elements and align pairwise, so balance imposes two equations +per value: + +``` +receiver.COUNT_0 == sender.cd₀ + 2¹⁶·cd₁ (low word) +receiver.COUNT_1 == sender.cd₂ + 2¹⁶·cd₃ (high word) +``` + +With the sender's halfwords `IsHalfword`-checked, the receiver's limbs are 32-bit +**for free**. Modelling the hop as one equation is strictly weaker than the AIR: it +lets the receiver re-split its limbs, manufacturing an alias the real bus rejects. + +Three things to keep: + +- Every UNSAT survived the correction, having been proven under weaker hypotheses + than reality supplies. The error direction was the safe one. +- **A phantom finding causes real damage.** Working around it led to asserting + `count ≤ 256` on *every* row of the field-exact chain check when the AIR bounds + only the head — a genuinely over-strong assertion, in the dangerous direction, + added to accommodate something that did not exist. +- **A proposed fix that is a no-op means the gap is not there.** The recommended + fix was "receive `count` as `DWordHL`", which changes nothing under the real + semantics. That should have stopped the write-up. + +§G now asserts the element counts and the tuple alignment directly. Its absence is +what let the phantom through, and `spec/dma.typ`, written independently, reaches the +same conclusion by a different route. + +## Where to send the next reviewer + +1. **The `Memw` ordering argument for unaligned 8-byte accesses.** A misaligned copy + generates one on nearly every row, and the whole snapshot story rests on `T+1` + reads preceding `T+2` writes per address. Nobody has checked it. +2. **A1–A5 centrally**, rather than per chip. `IS_WORD` has no discharger anywhere. +3. **For PR #874, not here:** `end·(1 − tail) = 0` would close the + `count = 7, tail = 0` truncation inside the AIR instead of leaving it to the + `Alu` bus (defence in depth — the pin is sound today), and DMA is the only + high-volume table with no `max_rows`/chunking. + +### Still open, report-only + +Recorded rather than closed, so the next reviewer does not have to rediscover them. + +1. **`replay_dma_memcpy_for_sizing`** (`trace_builder.rs:1090`) is a + `#[cfg(feature = "disk-spill")]` duplicate of the payload logic in + `collect_dma_memcpy_ops` — lines 1117, 1140 and 1160-1168 mirror 1006, 1033 and + 1060. `dma_ops_for_test` calls the primary directly, so **none of this + directory's mutation coverage reaches the mirror**; the five payload mutations + the Rust tests catch would all survive there. `count_table_lengths_drift_tests` + is the only thing touching it and it compares row counts, not payload fields. + Deduplicating is a change to shipped code and therefore out of scope for a + verification-only branch. +2. **`count_table_lengths`** — the disk-spill sizing pass. Covered by the PR's own + `count_table_lengths_drift_tests.rs`; not re-derived here. +3. **The `n = 0` ecall.** One row, both `first` and `end`, no `DmaNext` traffic, no + memory operations. Pinned by the completeness sweep and by + `empty_dma_call_is_a_single_first_and_terminal_row`, but it is the row shape most + likely to be broken by a future multiplicity change, because **every + multiplicity on it is zero** — nothing about it is load-bearing until it is. +4. **Two ecalls at one timestamp.** Ruled out by CPU timestamps strictly increasing + per instruction (A4). Asserted, not verified here, and it is what the `DmaNext` + timestamp binding rests on. +5. **The `## Results` block is still hand-copied.** `verify.log` is no longer on + this list — `make verify-dma` now diffs the gate's live output against the + committed transcript and fails if they disagree, so that file cannot go stale + silently. The `## Results` block above aggregates four sources by hand and can. + +No CI workflow runs any of this yet; `make verify-dma` is the entry point. +Two cross-references point at siblings that are **not merged**: +`formal_verification/keccak/` (PR #923) and `spec/dma.typ` (PR #931). diff --git a/formal_verification/dma/audit_transcription.py b/formal_verification/dma/audit_transcription.py new file mode 100644 index 000000000..8cb9ca7d2 --- /dev/null +++ b/formal_verification/dma/audit_transcription.py @@ -0,0 +1,684 @@ +""" +Executable half of the transcription audit: does the gate model the Rust that +was actually written? + +The gate (`z3_verify.py`) proves things about a MODEL. Everything +it proves is worthless if the model and `prover/src/tables/dma.rs` have drifted, +and the dangerous drift direction is a model STRONGER than the object it +models -- it yields UNSAT where the real table is forgeable, and no positive +anchor can catch it, because honest inputs satisfy a correct model and an +over-strong one equally well. (In the EC campaign the equivalent audit found +three premises the gate asserted about the chip and never read, one of them +hiding a working forgery.) + +So this script reads the Rust and asserts, textually and structurally: + + A. CONSTANTS -- every number the oracle and gate hard-code appears in the + Rust with that value. + B. COLUMNS -- the column layout the gate assumes is the layout `dma::cols` + declares, including `NUM_COLUMNS`. + C. CONSTRAINTS -- each constraint index the gate models is emitted, at that + index, by the template the gate modelled, with the operands + the gate used; and no constraint index exists that the gate + does not model. + D. BUSES -- the 23 interactions, their bus ids, their multiplicities and + the wiring facts the gate explicitly CANNOT see: that the + source read and the destination write reference the SAME + `value` columns, that their timestamp offsets are +1 and +2, + that `w8 = 1 - tail` on both, and that a read carries + `old == value`. + E. EXECUTOR -- the ecall validates what the oracle validates, in that order. + F. GENERATOR -- `generate_dma_trace`'s padding row is the row the oracle's + `padding_columns()` describes. + +It is deliberately textual (regex over the source) rather than a Rust test: the +point is to catch a change in `dma.rs` that nobody reflected here, and a Rust +test would be edited in the same commit as the code it guards. + + python3 audit_transcription.py [--repo /path/to/lambda_vm] +""" + +import os +import re +import sys + +HERE = os.path.dirname(os.path.abspath(__file__)) +#: This script lives at `formal_verification/dma/`, so the repo root is two up. +DEFAULT_REPO = os.path.abspath(os.path.join(HERE, "..", "..")) + +sys.path.insert(0, HERE) +import dma_ref as ref # noqa: E402 + +#: Gate constants this audit cross-checks, duplicated rather than imported: +#: importing `z3_verify` drags in `z3`, and EVERY claim here is textual and +#: needs no solver -- so a machine without z3 can still run the whole audit. +#: The duplication is the cost of that, and it is a real one: nothing detects +#: drift between these values and the gate's. They are all derived constants +#: (Goldilocks, its 2^32 inverse, the executor's chunk bound), so drift would +#: mean one of the two is simply wrong, and `audit_constants` checks each against +#: the Rust independently -- which is the property that matters. +GATE_P = 2**64 - 2**32 + 1 +GATE_INV_2_32 = pow(2**32, -1, GATE_P) +GATE_MAX_BYTES = 256 +GATE_ZERO_SUM = 4 * 65535 +GATE_ZERO_DOMAIN = 2**20 + + +class Audit: + """A findings collector. Nothing raises; everything is reported.""" + + def __init__(self): + self.checks = 0 + self.findings = [] + + def ok(self, claim, condition, detail=""): + self.checks += 1 + if not condition: + self.findings.append((claim, detail)) + return condition + + def report(self): + print("=" * 76) + print(f"{self.checks} claims checked, {len(self.findings)} finding(s)") + print("=" * 76) + for claim, detail in self.findings: + print(f" FINDING {claim}") + if detail: + print(f" {detail}") + if not self.findings: + print(" no drift between the Rust, the oracle and the gate") + return not self.findings + + +def read(repo, relative): + """Read a source file, whitespace-normalised for literal matching. + + Two things this fixes. (a) ENCODING: every Rust file here contains non-ASCII + (em-dashes), and the locale default is not always UTF-8, so a bare `open()` + can die with `UnicodeDecodeError` under `LC_ALL=C` with coercion disabled. + (b) FORMATTING: the literal checks below match source fragments like + `if tail { 1 } else { 8 }`, and `rustfmt` reflows those across lines the + moment a line grows past `max_width`. An earlier version tried + `src.replace("\n", " ")`, which collapses the newline but leaves the + indentation, so it could never match a reflowed form -- the guard was dead + code and a purely cosmetic reformat produced spurious findings. Since this + script is meant to run in CI, a spurious red is how it gets deleted. + + Collapsing all runs of whitespace to one space makes every literal check + reflow-insensitive. Line-oriented claims use `read_raw` instead. + """ + return re.sub(r"\s+", " ", read_raw(repo, relative)) + + +def read_raw(repo, relative): + """The file verbatim, for claims that depend on line structure.""" + path = os.path.join(repo, relative) + with open(path, encoding="utf-8") as f: + return f.read() + + +# --------------------------------------------------------------------------- +# A. Constants +# --------------------------------------------------------------------------- + +def audit_constants(a, repo): + execution = read(repo, "executor/src/vm/instruction/execution.rs") + dma = read(repo, "prover/src/tables/dma.rs") + templates = read(repo, "prover/src/constraints/templates.rs") + syscalls = read(repo, "syscalls/src/syscalls.rs") + + m = re.search(r"pub const DMA_MEMCPY_MAX_BYTES:\s*u64\s*=\s*(\d+)", execution) + a.ok("DMA_MEMCPY_MAX_BYTES matches the oracle and gate", m and + int(m.group(1)) == ref.DMA_MEMCPY_MAX_BYTES == GATE_MAX_BYTES, + f"rust={m.group(1) if m else '?'} oracle={ref.DMA_MEMCPY_MAX_BYTES} gate={GATE_MAX_BYTES}") + + m = re.search(r"pub const DMA_MEMCPY_SYSCALL_NUMBER:\s*u64\s*=\s*u64::MAX\s*-\s*(\d+)", execution) + a.ok("DMA_MEMCPY_SYSCALL_NUMBER is u64::MAX - 2", m and + (2**64 - 1 - int(m.group(1))) == ref.DMA_MEMCPY_SYSCALL_NUMBER) + + m = re.search(r"const DMA_MEMCPY_MAX_BYTES:\s*usize\s*=\s*(\d+)", syscalls) + a.ok("the guest stub's chunk bound equals the executor's", m and + int(m.group(1)) == ref.DMA_MEMCPY_MAX_BYTES, + "a stub that chunks larger than the executor accepts would abort the guest") + + m = re.search(r"pub const INV_SHIFT_32:\s*u64\s*=\s*(\d+)", templates) + a.ok("INV_SHIFT_32 is the true inverse of 2^32 mod p, and the gate has it", + m and int(m.group(1)) == GATE_INV_2_32 + and (int(m.group(1)) * 2**32) % GATE_P == 1) + + # The table takes its bound FROM the executor rather than restating it -- + # the property that makes the AIR bound and the execution bound un-driftable. + a.ok("dma.rs re-exports the executor's bound instead of restating it", + "DMA_MEMCPY_MAX_BYTES as EXECUTOR_DMA_MEMCPY_MAX_BYTES" in dma + and re.search(r"pub const DMA_MEMCPY_MAX_BYTES:\s*u64\s*=\s*" + r"EXECUTOR_DMA_MEMCPY_MAX_BYTES", dma) is not None) + + a.ok("the Zero sender's constant is 4 * 65535, as the gate assumes", + "LinearTerm::Constant(4 * 65535)" in dma + and GATE_ZERO_SUM == 4 * 65535) + + # The Zero receiver's domain: bitwise packs x + 256y + 65536z with z 4 bits. + bitwise = read(repo, "prover/src/tables/bitwise.rs") + a.ok("the Zero send stays inside the bitwise table's ZERO domain", + "65536 * z" in bitwise.replace("65536 * cols::Z", "65536 * z") + or "coefficient: 65536" in bitwise, + "the receiver packs x + 256y + 65536z with z < 16, i.e. arguments < 2^20") + a.ok("4 * 65535 fits that domain", GATE_ZERO_SUM < GATE_ZERO_DOMAIN) + + a.ok("the row widths the gate uses are the widths dma.rs uses", + "if tail { 1 } else { 8 }" in dma.replace("\n", " ") + or re.search(r"let width = if tail \{ 1 \} else \{ 8 \}", dma) is not None, + f"gate uses {1}/{8}") + a.ok("the AIR's step expression is 8 - 7*tail", + "AddLinearTerm::Constant(8)" in dma and "coefficient: -7" in dma) + + +# --------------------------------------------------------------------------- +# B. Column layout +# --------------------------------------------------------------------------- + +EXPECTED_COLUMNS = { + "TIMESTAMP_0": 0, "TIMESTAMP_1": 1, + "SRC_0": 2, "SRC_1": 3, + "SRC_INCR_0": 4, "SRC_INCR_1": 5, "SRC_INCR_2": 6, "SRC_INCR_3": 7, + "DST_0": 8, "DST_1": 9, + "DST_INCR_0": 10, "DST_INCR_1": 11, "DST_INCR_2": 12, "DST_INCR_3": 13, + "COUNT_0": 14, "COUNT_1": 15, + "COUNT_DECR_0": 16, "COUNT_DECR_1": 17, "COUNT_DECR_2": 18, "COUNT_DECR_3": 19, + "FIRST": 20, "END": 21, "TAIL": 22, "VALUE_0": 23, "MU": 31, + "NUM_COLUMNS": 32, +} + + +def audit_columns(a, repo): + dma = read(repo, "prover/src/tables/dma.rs") + declared = {m.group(1): int(m.group(2)) for m in + re.finditer(r"pub const (\w+):\s*usize\s*=\s*(\d+);", dma)} + for name, index in EXPECTED_COLUMNS.items(): + a.ok(f"column {name} is at {index}", declared.get(name) == index, + f"declared at {declared.get(name)}") + a.ok("VALUE is the eight columns starting at VALUE_0", + re.search(r"pub const VALUE:\s*\[usize;\s*8\]", dma) is not None + and dma.count("VALUE_0 +") == 7) + # Every column the gate models, and nothing more. `mu` at 31 with `value` + # at 23..30 means the layout is exactly full: 32 columns, none spare. + a.ok("the layout is dense: 24 named + 8 value = NUM_COLUMNS", + declared.get("NUM_COLUMNS") == declared.get("MU") + 1 == 32) + + +# --------------------------------------------------------------------------- +# C. Constraints +# --------------------------------------------------------------------------- + +#: (index, what the gate models at that index) +EXPECTED_CONSTRAINTS = [ + (0, "emit_is_bit FIRST"), + (1, "emit_is_bit END"), + (2, "emit_is_bit TAIL"), + (3, "emit_is_bit MU"), + (4, "(first + end) * (1 - mu)"), + (5, "emit_add_pair_no_overflow src + step = src_incr"), + (7, "emit_add_pair_no_overflow dst + step = dst_incr"), + (9, "emit_add_pair count_decr + step = count"), + (11, "tail * value[i] for i in 1..8"), +] + + +def audit_constraints(a, repo): + dma = read(repo, "prover/src/tables/dma.rs") + body = dma.split("impl ConstraintSet")[1] + + a.ok("idx 0-3 are the four booleanity constraints, in the gate's order", + re.search(r"emit_is_bit\(b, 0, cols::FIRST", body) and + re.search(r"emit_is_bit\(b, 1, cols::END", body) and + re.search(r"emit_is_bit\(b, 2, cols::TAIL", body) and + re.search(r"emit_is_bit\(b, 3, cols::MU", body)) + + a.ok("idx 4 is (first + end) * (1 - mu)", + re.search(r"emit_base\(4,\s*\(first \+ end\) \* \(one - mu\)\)", body) is not None, + "the gate rewrites this as Implies(mu == 0, first == 0 and end == 0)") + + a.ok("idx 5 is the NO-OVERFLOW add on src, gated by (MU, END)", + re.search(r"emit_add_pair_no_overflow\(\s*b,\s*5,\s*cols::MU,\s*cols::END,", + body) is not None) + a.ok("idx 7 is the NO-OVERFLOW add on dst, gated by (MU, END)", + re.search(r"emit_add_pair_no_overflow\(\s*b,\s*7,\s*cols::MU,\s*cols::END,", + body) is not None) + a.ok("idx 9 is the PLAIN add on count (wrap permitted, unconditional)", + re.search(r"emit_add_pair\(\s*b,\s*9,\s*&\[\],", body) is not None, + "the gate relies on this being the plain form: the terminal row holds 0 - 1") + + a.ok("src/dst adds read src as DWordWL and src_incr as DWordHL", + "AddOperand::dword(cols::SRC_0)" in body + and "AddOperand::from_dword_hl(cols::SRC_INCR_0)" in body + and "AddOperand::dword(cols::DST_0)" in body + and "AddOperand::from_dword_hl(cols::DST_INCR_0)" in body) + a.ok("the count add has count_decr on the LHS and count as the SUM", + re.search(r"emit_add_pair\(\s*b,\s*9,\s*&\[\],\s*" + r"&AddOperand::from_dword_hl\(cols::COUNT_DECR_0\),\s*" + r"&step,\s*&AddOperand::dword\(cols::COUNT_0\),", body) is not None, + "reversing it would make count_decr the sum and break the terminal row") + + a.ok("idx 11..17 zero the seven unused value lanes on a tail row", + re.search(r"emit_base\(11 \+ i - 1,\s*tail\.clone\(\) \* b\.main\(0, column\)\)", + body) is not None + and ".skip(1)" in body) + + # No constraint index outside what the gate models. + emitted = sorted({int(m.group(1)) for m in re.finditer(r"emit_base\((\d+)", body)} + | {int(m.group(1)) for m in + re.finditer(r"emit_is_bit\(b, (\d+)", body)} + | {int(m.group(1)) for m in + re.finditer(r"emit_add_pair(?:_no_overflow)?\(\s*b,\s*(\d+)", body)}) + a.ok("DmaConstraints does not raise max_degree above the default 2", + "fn max_degree" not in body, + "the gate's encoding rewrites `boolean * expr` products as implications, " + "which is exact only while every such product has a boolean factor -- a " + "degree-3 constraint would mean that rewrite lost something") + + a.ok("no constraint index exists that the gate does not model", + emitted == [0, 1, 2, 3, 4, 5, 7, 9, 11], + f"emitted anchors: {emitted}; the pairs also occupy 6, 8, 10 and the " + f"lane loop 12..17") + + +# --------------------------------------------------------------------------- +# D. Buses -- including the wiring the gate cannot see +# --------------------------------------------------------------------------- + +def audit_buses(a, repo): + dma = read(repo, "prover/src/tables/dma.rs") + buses = dma.split("pub fn bus_interactions")[1].split("/// An `IsHalfword`")[0] + + # The twelve IsHalfword sends are built by the `halfword()` helper below the + # list, so they appear as calls rather than as literal `BusInteraction::`s. + inline = buses.count("BusInteraction::") + via_helper = len(re.findall(r"\bhalfword\(cols::\w+\)", buses)) + a.ok("there are 23 bus interactions", inline + via_helper == 23, + f"found {inline} inline + {via_helper} via halfword() = {inline + via_helper}") + + counts = {bus: len(re.findall(rf"BusId::{bus}\b", buses)) for bus in + ("Ecall", "DmaNext", "Zero", "Memw", "Alu")} + counts["IsHalfword"] = via_helper + a.ok("bus mix is 1 Ecall, 2 DmaNext, 12 IsHalfword, 1 Zero, 5 Memw, 2 Alu", + counts == {"Ecall": 1, "DmaNext": 2, "IsHalfword": 12, "Zero": 1, + "Memw": 5, "Alu": 2}, str(counts)) + + a.ok("the Ecall interaction is a RECEIVER with multiplicity `first`", + re.search(r"BusInteraction::receiver\(\s*BusId::Ecall,\s*" + r"Multiplicity::Column\(cols::FIRST\)", buses) is not None) + a.ok("DmaNext sends with `mu - end` and receives with `mu - first`", + "let mu_minus_end = Multiplicity::Diff(cols::MU, cols::END);" in dma + and "let mu_minus_first = Multiplicity::Diff(cols::MU, cols::FIRST);" in dma + and re.search(r"sender\(\s*BusId::DmaNext,\s*mu_minus_end", buses) + and re.search(r"receiver\(\s*BusId::DmaNext,\s*mu_minus_first", buses)) + + a.ok("both DmaNext tuples carry the timestamp", + buses.split("BusId::DmaNext")[1].count("TIMESTAMP_0") == 1 + and buses.split("BusId::DmaNext")[2].count("TIMESTAMP_0") == 1, + "without it, rows of two different ecalls could be spliced -- the " + "exact hole the BLAKE3 design review found in its internal bus") + + a.ok("the send carries the INCREMENTED triple and the receive the plain one", + all(name in buses.split("BusId::DmaNext")[1] for name in + ("SRC_INCR_0", "DST_INCR_0", "COUNT_DECR_0")) + and all(name in buses.split("BusId::DmaNext")[2] for name in + ("SRC_0", "DST_0", "COUNT_0"))) + + a.ok("all twelve IsHalfword sends are on count_decr, src_incr and dst_incr", + sorted(re.findall(r"halfword\(cols::(\w+)\)", buses)) == + sorted([f"COUNT_DECR_{i}" for i in range(4)] + + [f"SRC_INCR_{i}" for i in range(4)] + + [f"DST_INCR_{i}" for i in range(4)]), + "these are the range checks MAIN 1 and the width audit prove " + "load-bearing; losing one is a forgeable end flag or a wrapped address") + a.ok("IsHalfword sends have multiplicity `mu`", + re.search(r"BusId::IsHalfword,\s*Multiplicity::Column\(cols::MU\)", dma) + is not None) + + a.ok("the Zero send has multiplicity `mu` and pairs the sum with END", + re.search(r"sender\(\s*BusId::Zero,\s*Multiplicity::Column\(cols::MU\)", + buses) is not None + and "column: cols::COUNT_DECR_3" in buses + and "start_column: cols::END" in buses) + a.ok("all four count_decr halfwords enter the Zero sum with coefficient -1", + len(re.findall(r"coefficient: -1,\s*column: cols::COUNT_DECR_\d", buses)) == 4) + + a.ok("the three register reads are x10=dst, x11=src, x12=count", + re.search(r"memw_register_read\(20, cols::DST_0, cols::DST_1\)", buses) + and re.search(r"memw_register_read\(22, cols::SRC_0, cols::SRC_1\)", buses) + and re.search(r"memw_register_read\(24, cols::COUNT_0, cols::COUNT_1\)", buses), + "base_address = 2*reg; these are the sends REG-32 is discharged by") + a.ok("register reads have multiplicity `first`", + len(re.findall(r"BusId::Memw,\s*Multiplicity::Column\(cols::FIRST\)", buses)) == 3) + + a.ok("the tail LT lookup is count vs 8 with output `tail`, multiplicity mu", + re.search(r"BusId::Alu,\s*Multiplicity::Column\(cols::MU\)", buses) + and "BusValue::constant(8)" in buses + and "start_column: cols::TAIL" in buses) + a.ok("the bound LT lookup is count vs MAX+1 with output pinned to 1, " + "multiplicity first", + "BusValue::constant(DMA_MEMCPY_MAX_BYTES + 1)" in buses + and re.search(r"BusId::Alu,\s*Multiplicity::Column\(cols::FIRST\)", buses) + is not None) + + # ---- the wiring facts the gate explicitly cannot see ------------------- + read_tuple = buses.split("// 22. MEMW read")[1].split("// 23.")[0] + write_tuple = buses.split("// 23. MEMW write")[1] + + a.ok("the read tuple carries value_columns() TWICE (old and value)", + read_tuple.count("value_columns()") == 1 + and "tuple.extend(values.iter().cloned())" in read_tuple + and "tuple.append(&mut values)" in read_tuple, + "old == value is what makes the source read non-mutating") + a.ok("the write tuple carries the SAME value_columns()", + "tuple.extend(value_columns())" in write_tuple, + "THIS is why a copied byte cannot change: one set of columns feeds " + "both memory tuples, so the gate never has to prove read == write") + a.ok("value_columns() is exactly cols::VALUE, packed Direct", + re.search(r"fn value_columns\(\).*?cols::VALUE \.iter\(\)" + r".*?packing: Packing::Direct", dma) is not None, + "note the source is whitespace-normalised by `read`, so this pattern " + "matches the reflow-insensitive form") + + a.ok("the read is at T+1 and the write at T+2", + "timestamp_with_offset(1)" in read_tuple + and "timestamp_with_offset(2)" in write_tuple, + "all reads strictly before all writes is what gives an overlapping " + "copy snapshot semantics; the gate cannot see timestamps") + a.ok("timestamp_with_offset only offsets the LOW limb", + re.search(r"fn timestamp_with_offset.*?cols::TIMESTAMP_0.*?" + r"LinearTerm::Constant\(offset\)", dma, re.S) is not None + and read_tuple.count("cols::TIMESTAMP_1") == 1, + "a +1/+2 that could carry into the high limb would break ordering") + + a.ok("both data tuples set w2 = 0, w4 = 0 and w8 = 1 - tail", + read_tuple.count("BusValue::constant(0)") >= 2 + and write_tuple.count("BusValue::constant(0)") >= 2 + and read_tuple.count("column: cols::TAIL") == 1 + and write_tuple.count("column: cols::TAIL") == 1, + "w8 = 1 - tail is the only link between the width the AIR proves and " + "the number of bytes the memory table moves") + a.ok("both data tuples have multiplicity `mu - end`", + len(re.findall(r"BusInteraction::sender\(BusId::Memw, mu_minus_end", buses)) == 2, + "an `end` row therefore emits NO memory operation -- the premise the " + "truncation forgeries in MAIN 1 and the width audit turn on") + a.ok("the read addresses src and the write addresses dst", + "start_column: cols::SRC_0" in read_tuple + and "start_column: cols::DST_0" in write_tuple) + a.ok("both data tuples are non-register accesses", + "// is_register" in read_tuple and "// is_register" in write_tuple) + + +# --------------------------------------------------------------------------- +# G. Bus packing -- element counts and tuple alignment +# --------------------------------------------------------------------------- + +def audit_packing(a, repo): + """How many BUS ELEMENTS each packing produces, and whether the two DmaNext + tuples align element-for-element. + + THIS SECTION EXISTS BECAUSE ITS ABSENCE HID A FALSE FINDING. The audit used + to check only that the strings `DWordWL`/`DWordHL` appeared in the sender and + receiver tuples. It never checked how many bus elements those packings + produce -- and the gate had assumed a 64-bit value crosses the bus as ONE + field element. It does not: both are 2 elements with separate alpha powers, + so the binding is per 32-bit limb. The gate's weaker model manufactured an + alias the real bus rejects, and that phantom was published as the campaign's + headline residual. A model weaker than the AIR yields false alarms; the + lesson is that "how wide is one bus element" is a premise like any other and + must be read from the source, not assumed. + """ + lookup = read(repo, "crypto/stark/src/lookup.rs") + + body = lookup[lookup.index("pub fn num_bus_elements"):] + body = body[:body.index("pub fn columns")] + expected = {"Direct": 1, "Word2L": 1, "Word4L": 1, "DWordWL": 2, + "DWordHHW": 2, "DWordWHH": 2, "DWordHL": 2, "DWordBL": 2, + "QuadHL": 4, "QuadWL": 4} + for name, count in expected.items(): + a.ok(f"num_bus_elements(Packing::{name}) == {count}", + re.search(rf"Packing::{name} => {count},", body) is not None) + + # This guard is deliberately independent of the `expected` dict above: that + # dict pins the variants that exist TODAY, while this one must also reject a + # newly added compound that folds its inputs into a single element. So it + # keys off the source's own `// Compounds` section marker rather than off a + # per-variant comment. + # + # Two earlier versions were dead. The first searched for ASCII "2x" where the + # source writes "2×" (U+00D7), so it could never match. The second searched + # `Packing::\w+ => 1, // 2×`, which only covers arms whose comment begins + # "2×" -- it stayed dark for DWordHHW ("Direct + Word2L") and DWordWHH, both + # equally 64-bit. A dead guard inside the very section added to close the + # packing-assumption gap, twice over. + # + # Mutating any of the seven compound arms `2 → 1` (or `4 → 1`) now produces + # TWO findings: the per-variant claim above and this one. + compounds = body[body.index("// Compounds"):] + compounds = compounds[:compounds.index("}")] + a.ok("no Packing variant folds a 64-bit value into one bus element", + not re.search(r"Packing::\w+ => 1,", compounds), + "if one ever did, DmaNext would bind packed values and the gate's link " + "model would have to change with it") + + # Each element gets its own alpha power. + accum = lookup[lookup.index("Packing::DWordHL => {"):] + accum = accum[:accum.index("// 2× Word4L")] + a.ok("DWordHL accumulates two Word2L halves at consecutive alpha powers", + "alpha_powers[alpha_offset]" in accum + and "alpha_powers[alpha_offset + 1]" in accum + and "shifts.shift_16" in accum) + + # The two DmaNext tuples must have equal element counts and align pairwise. + dma = read(repo, "prover/src/tables/dma.rs") + buses = dma.split("pub fn bus_interactions")[1] + send = buses[buses.index("sender( BusId::DmaNext"):] + send = send[:send.index("BusInteraction::receiver( BusId::DmaNext")] + recv = buses[buses.index("receiver( BusId::DmaNext"):] + recv = recv[:recv.index("// 4-7.")] + + def elements(tup): + n = 0 + for packing, count in (("Packing::DWordHL", 2), ("Packing::DWordWL", 2), + ("Packing::Direct", 1)): + n += tup.count(packing) * count + return n + + a.ok("both DmaNext tuples carry the same number of bus elements", + elements(send) == elements(recv) == 8, + f"sender={elements(send)} receiver={elements(recv)}; a mismatch would " + f"misalign every field and silently change what the bus binds") + # ORDER, not just membership. §D checks that the right column names appear in + # each tuple and the block above checks the element counts -- neither pins the + # PAIRING, while the gate's `dmanext_link()` hard-codes it (sender low word <-> + # receiver low word, src<->src, dst<->dst, count<->count). Swapping SRC_0 and + # DST_0 in the receiver used to leave this audit at "0 findings" while the gate + # kept asserting src_incr<->src about a table that now binds src_incr<->dst. + # That is the same class as the assumption that produced the retracted R1: a + # premise about the bus taken on faith rather than read from the source. + def ordinal(tup, names): + """The order in which `names` first appear in a tuple's source text.""" + seen = [(tup.index(n), n) for n in names if n in tup] + return [n for _, n in sorted(seen)] + + a.ok("the DmaNext sender orders its values ts, src_incr, dst_incr, count_decr", + ordinal(send, ("cols::SRC_INCR_0", "cols::DST_INCR_0", "cols::COUNT_DECR_0")) + == ["cols::SRC_INCR_0", "cols::DST_INCR_0", "cols::COUNT_DECR_0"], + "the gate pairs these positionally with the receiver's src/dst/count") + a.ok("the DmaNext receiver orders its values ts, src, dst, count", + ordinal(recv, ("cols::SRC_0", "cols::DST_0", "cols::COUNT_0")) + == ["cols::SRC_0", "cols::DST_0", "cols::COUNT_0"], + "a swap here silently re-pairs every field the gate models") + a.ok("both DmaNext tuples put the timestamp first, in the same order", + ordinal(send, ("cols::TIMESTAMP_0", "cols::TIMESTAMP_1")) + == ordinal(recv, ("cols::TIMESTAMP_0", "cols::TIMESTAMP_1")) + == ["cols::TIMESTAMP_0", "cols::TIMESTAMP_1"]) + + a.ok("the sender uses DWordHL x3 and the receiver DWordWL x3", + send.count("Packing::DWordHL") == 3 + and recv.count("Packing::DWordWL") == 3, + "so the aligned pairs are (incr low word, src low word) and " + "(incr high word, src high word) -- a per-limb binding") + + +# --------------------------------------------------------------------------- +# E. Executor +# --------------------------------------------------------------------------- + +def audit_executor(a, repo): + execution = read(repo, "executor/src/vm/instruction/execution.rs") + body = execution.split("SyscallNumbers::DmaMemcpy => {")[1].split("SyscallNumbers::Hint")[0] + + a.ok("the operands are read from x10, x11, x12 as dst, src, n", + re.search(r"let dst = registers\.read\(10\)", body) + and re.search(r"let src = registers\.read\(11\)", body) + and re.search(r"let n = registers\.read\(12\)", body)) + a.ok("the chunk bound is an actual guard on n, not just a reachable error", + re.search(r"if n > DMA_MEMCPY_MAX_BYTES\s*\{", body) is not None, + "checking only that the error variant is mentioned would pass for a " + "guard rewritten to `if false`") + a.ok("the chunk bound is rejected BEFORE the range checks, as the oracle's " + "`validate` orders it", + body.index("DmaMemcpyChunkTooLarge") < body.index("checked_add")) + a.ok("both ranges are checked for wrap", + "dst.checked_add(n)" in body and "src.checked_add(n)" in body) + a.ok("the copy goes through a snapshot buffer, reads before writes", + body.index("memory.load_byte") < body.index("memory.store_byte") + and "let mut bytes = [0u8; DMA_MEMCPY_MAX_BYTES as usize]" in body, + "this is the implementation choice that makes an overlapping copy a " + "memmove; the oracle's write_before_read mutant is its negative control") + + +# --------------------------------------------------------------------------- +# F. Trace generator +# --------------------------------------------------------------------------- + +def audit_generator(a, repo): + dma = read(repo, "prover/src/tables/dma.rs") + gen = dma.split("pub fn generate_dma_trace")[1].split("/// Helper: a MEMW")[0] + + a.ok("rows are padded to a power of two, minimum 4", + "next_power_of_two().max(4)" in gen) + a.ok("width selection is `tail = count < 8` then 1 or 8", + "let tail = op.count < 8;" in gen and "if tail { 1 } else { 8 }" in gen) + a.ok("src_incr/dst_incr use wrapping_add and count_decr wrapping_sub", + "op.src.wrapping_add(width)" in gen + and "op.dst.wrapping_add(width)" in gen + and "op.count.wrapping_sub(width)" in gen, + "wrapping is correct here BECAUSE the AIR rejects the wraps that " + "matter: no_overflow on src/dst, and the count wrap only on `end`") + + padding = gen.split("for row_idx in n..num_rows")[1] + expected = ref.padding_columns() + a.ok("the padding row sets COUNT_0 = 1", "cols::COUNT_0, FE::one()" in padding + and expected["count"] == [1, 0]) + a.ok("the padding row sets SRC_INCR_0 = DST_INCR_0 = 1", + "cols::SRC_INCR_0, FE::one()" in padding + and "cols::DST_INCR_0, FE::one()" in padding + and expected["src_incr"][0] == expected["dst_incr"][0] == 1) + a.ok("the padding row sets TAIL = 1", "cols::TAIL, FE::one()" in padding + and expected["tail"] == 1) + a.ok("the padding row leaves MU, FIRST, END and COUNT_DECR at zero", + "cols::MU" not in padding and "cols::FIRST" not in padding + and "cols::END" not in padding and "cols::COUNT_DECR" not in padding + and expected["mu"] == 0 and expected["count_decr"] == [0, 0, 0, 0], + "the gate's completeness sweep pins exactly this row; if the " + "generator changes it, the sweep must be re-run") + + +# --------------------------------------------------------------------------- +# H. Fixture pinning +# --------------------------------------------------------------------------- + +def audit_fixture(a, repo): + """The Rust test consumes the oracle's emitted table, not a transcription. + + Previously `prover/src/tests/dma_tests.rs` carried a hand-typed copy of the + canonical vectors with a comment saying "do not edit by hand: rerun the + oracle and re-transcribe" -- and nothing enforced it, so regenerating the + vectors from a changed model left the Rust literals stale and green. + """ + tests = read(repo, "prover/src/tests/dma_tests.rs") + a.ok("dma_tests.rs embeds the oracle's row table with include_str!", + "include_str!" in tests and "canonical_dma_rows.txt" in tests, + "otherwise a regenerated oracle is a silent no-op on the Rust side") + a.ok("dma_tests.rs drives the real decomposition, not the trace formatter", + "dma_ops_for_test" in tests, + "`generate_dma_trace` only formats an already-decomposed op list into " + "columns, so asserting against it proves nothing about the row split") + a.ok("the emitted row table exists and is non-trivial", + len(read_raw(repo, "formal_verification/dma/canonical_dma_rows.txt").splitlines()) > 20) + + # FRESHNESS, not just presence. Greping for `include_str!` proves the Rust + # reads a fixture; it does not prove the fixture is what the current oracle + # emits. `test_ref.py`'s regeneration gate is `if not failed`, so a run that + # only *skipped* an anchor (PARTIALLY VALIDATED, exit 2) or ran `--quick` + # still rewrites the fixture, while a run with a real failure leaves a stale + # one behind with the Rust test still green. Re-derive the table and compare. + # + # Caveat: this hand-duplicates `emit_row_table`'s line format and memory + # seeding. That is the price of not importing the emitter (which would make + # the check circular), but it means a deliberate format change to the emitter + # produces a finding here until this block is updated to match. + sys.path.insert(0, os.path.join(repo, "formal_verification/dma")) + committed = read_raw(repo, "formal_verification/dma/canonical_dma_rows.txt") + try: + import test_ref as harness + rows = [] + for name, dst, src, n in harness.CANONICAL_CASES: + memory = {src + i: (i * 7 + 3) & 0xFF for i in range(n)} + decomposed = ref.row_decomposition(0x30, dst, src, n, memory) + data = [r for r in decomposed if not r.end] + rows.append(f"vector|{name}|{dst}|{src}|{n}|{len(data)}") + for r in data: + rows.append(f"row|{r.src}|{r.dst}|{r.count}|" + f"{1 if r.tail else 0}|{r.width}") + a.ok("the checked-in row table matches what the oracle emits today", + [line for line in committed.splitlines() if not line.startswith("#")] == rows, + "regenerate with `python3 test_ref.py`") + except ImportError as exc: + a.ok("the oracle harness is importable so the fixture can be re-derived", + False, f"could not import test_ref: {exc}") + + +# --------------------------------------------------------------------------- + +def main(): + repo = DEFAULT_REPO + if "--repo" in sys.argv: + at = sys.argv.index("--repo") + 1 + if at >= len(sys.argv): + sys.exit("--repo needs a path") + repo = sys.argv[at] + # Fail with a diagnosis rather than a bare FileNotFoundError deep in a check. + for marker in ("prover/src/tables/dma.rs", "crypto/stark/src/lookup.rs"): + if not os.path.exists(os.path.join(repo, marker)): + sys.exit(f"{repo} does not look like a lambda_vm checkout " + f"(missing {marker})") + print(f"auditing {repo}") + + a = Audit() + # The per-section claim counts are PRINTED, not documented by hand. An + # earlier version stated them in TRANSCRIPTION-AUDIT.md and got five of six + # wrong -- apportioned to sum to the real total instead of measured, which is + # the "declared, not derived" defect this file exists to catch. Now the doc + # quotes this output. + for name, fn in (("A. constants", audit_constants), + ("B. columns", audit_columns), + ("C. constraints", audit_constraints), + ("D. buses", audit_buses), + ("E. executor", audit_executor), + ("F. generator", audit_generator), + ("G. bus packing", audit_packing), + ("H. fixture pinning", audit_fixture)): + before, before_checks = len(a.findings), a.checks + fn(a, repo) + n = a.checks - before_checks + status = "ok" if len(a.findings) == before else f"{len(a.findings) - before} finding(s)" + print(f" {name:20s} {n:3d} claims {status}") + sys.exit(0 if a.report() else 1) + + +if __name__ == "__main__": + main() diff --git a/formal_verification/dma/canonical_dma_rows.txt b/formal_verification/dma/canonical_dma_rows.txt new file mode 100644 index 000000000..ce1b386fe --- /dev/null +++ b/formal_verification/dma/canonical_dma_rows.txt @@ -0,0 +1,70 @@ +# Generated by test_ref.py — do not edit by hand. +# Consumed by prover/src/tests/dma_tests.rs via include_str!. +# vector|name|dst|src|count|data_rows row|src|dst|count|tail|width +vector|empty|4096|8192|0|0 +vector|single byte|4096|8192|1|1 +row|8192|4096|1|1|1 +vector|one wide row|4096|8192|8|1 +row|8192|4096|8|0|8 +vector|wide plus tail|4096|8192|9|2 +row|8192|4096|9|0|8 +row|8200|4104|1|1|1 +vector|widest tail|4096|8192|7|7 +row|8192|4096|7|1|1 +row|8193|4097|6|1|1 +row|8194|4098|5|1|1 +row|8195|4099|4|1|1 +row|8196|4100|3|1|1 +row|8197|4101|2|1|1 +row|8198|4102|1|1|1 +vector|unaligned body and tail|8197|4099|27|6 +row|4099|8197|27|0|8 +row|4107|8205|19|0|8 +row|4115|8213|11|0|8 +row|4123|8221|3|1|1 +row|4124|8222|2|1|1 +row|4125|8223|1|1|1 +vector|forward overlap|12292|12288|24|3 +row|12288|12292|24|0|8 +row|12296|12300|16|0|8 +row|12304|12308|8|0|8 +vector|backward overlap|12288|12292|24|3 +row|12292|12288|24|0|8 +row|12300|12296|16|0|8 +row|12308|12304|8|0|8 +vector|page crossing|4092|8188|16|2 +row|8188|4092|16|0|8 +row|8196|4100|8|0|8 +vector|maximum chunk|4096|8192|256|32 +row|8192|4096|256|0|8 +row|8200|4104|248|0|8 +row|8208|4112|240|0|8 +row|8216|4120|232|0|8 +row|8224|4128|224|0|8 +row|8232|4136|216|0|8 +row|8240|4144|208|0|8 +row|8248|4152|200|0|8 +row|8256|4160|192|0|8 +row|8264|4168|184|0|8 +row|8272|4176|176|0|8 +row|8280|4184|168|0|8 +row|8288|4192|160|0|8 +row|8296|4200|152|0|8 +row|8304|4208|144|0|8 +row|8312|4216|136|0|8 +row|8320|4224|128|0|8 +row|8328|4232|120|0|8 +row|8336|4240|112|0|8 +row|8344|4248|104|0|8 +row|8352|4256|96|0|8 +row|8360|4264|88|0|8 +row|8368|4272|80|0|8 +row|8376|4280|72|0|8 +row|8384|4288|64|0|8 +row|8392|4296|56|0|8 +row|8400|4304|48|0|8 +row|8408|4312|40|0|8 +row|8416|4320|32|0|8 +row|8424|4328|24|0|8 +row|8432|4336|16|0|8 +row|8440|4344|8|0|8 diff --git a/formal_verification/dma/canonical_dma_vectors.json b/formal_verification/dma/canonical_dma_vectors.json new file mode 100644 index 000000000..e24063db0 --- /dev/null +++ b/formal_verification/dma/canonical_dma_vectors.json @@ -0,0 +1,6891 @@ +[ + { + "name": "empty", + "timestamp": 48, + "dst": 4096, + "src": 8192, + "count": 0, + "widths": [], + "data_rows": 0, + "rows": [ + { + "src": 8192, + "dst": 4096, + "count": 0, + "first": true, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8192, + 0 + ], + "src_incr": [ + 8193, + 0, + 0, + 0 + ], + "dst": [ + 4096, + 0 + ], + "dst_incr": [ + 4097, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 1, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4096 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8192 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 0 + ], + "is_write": false + } + ] + }, + { + "name": "single byte", + "timestamp": 48, + "dst": 4096, + "src": 8192, + "count": 1, + "widths": [ + 1 + ], + "data_rows": 1, + "rows": [ + { + "src": 8192, + "dst": 4096, + "count": 1, + "first": true, + "end": false, + "tail": true, + "width": 1, + "value": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8192, + 0 + ], + "src_incr": [ + 8193, + 0, + 0, + 0 + ], + "dst": [ + 4096, + 0 + ], + "dst_incr": [ + 4097, + 0, + 0, + 0 + ], + "count": [ + 1, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 1, + "value": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8193, + "dst": 4097, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8193, + 0 + ], + "src_incr": [ + 8194, + 0, + 0, + 0 + ], + "dst": [ + 4097, + 0 + ], + "dst_incr": [ + 4098, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4096 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8192 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 1 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8192, + "timestamp": 49, + "width": 1, + "value": [ + 3 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4096, + "timestamp": 50, + "width": 1, + "value": [ + 3 + ], + "is_write": true + } + ] + }, + { + "name": "one wide row", + "timestamp": 48, + "dst": 4096, + "src": 8192, + "count": 8, + "widths": [ + 8 + ], + "data_rows": 1, + "rows": [ + { + "src": 8192, + "dst": 4096, + "count": 8, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8192, + 0 + ], + "src_incr": [ + 8200, + 0, + 0, + 0 + ], + "dst": [ + 4096, + 0 + ], + "dst_incr": [ + 4104, + 0, + 0, + 0 + ], + "count": [ + 8, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 8200, + "dst": 4104, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8200, + 0 + ], + "src_incr": [ + 8201, + 0, + 0, + 0 + ], + "dst": [ + 4104, + 0 + ], + "dst_incr": [ + 4105, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4096 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8192 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 8 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8192, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4096, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + } + ] + }, + { + "name": "wide plus tail", + "timestamp": 48, + "dst": 4096, + "src": 8192, + "count": 9, + "widths": [ + 8, + 1 + ], + "data_rows": 2, + "rows": [ + { + "src": 8192, + "dst": 4096, + "count": 9, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8192, + 0 + ], + "src_incr": [ + 8200, + 0, + 0, + 0 + ], + "dst": [ + 4096, + 0 + ], + "dst_incr": [ + 4104, + 0, + 0, + 0 + ], + "count": [ + 9, + 0 + ], + "count_decr": [ + 1, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 8200, + "dst": 4104, + "count": 1, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 59, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8200, + 0 + ], + "src_incr": [ + 8201, + 0, + 0, + 0 + ], + "dst": [ + 4104, + 0 + ], + "dst_incr": [ + 4105, + 0, + 0, + 0 + ], + "count": [ + 1, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 59, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8201, + "dst": 4105, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8201, + 0 + ], + "src_incr": [ + 8202, + 0, + 0, + 0 + ], + "dst": [ + 4105, + 0 + ], + "dst_incr": [ + 4106, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4096 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8192 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 9 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8192, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8200, + "timestamp": 49, + "width": 1, + "value": [ + 59 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4096, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4104, + "timestamp": 50, + "width": 1, + "value": [ + 59 + ], + "is_write": true + } + ] + }, + { + "name": "widest tail", + "timestamp": 48, + "dst": 4096, + "src": 8192, + "count": 7, + "widths": [ + 1, + 1, + 1, + 1, + 1, + 1, + 1 + ], + "data_rows": 7, + "rows": [ + { + "src": 8192, + "dst": 4096, + "count": 7, + "first": true, + "end": false, + "tail": true, + "width": 1, + "value": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8192, + 0 + ], + "src_incr": [ + 8193, + 0, + 0, + 0 + ], + "dst": [ + 4096, + 0 + ], + "dst_incr": [ + 4097, + 0, + 0, + 0 + ], + "count": [ + 7, + 0 + ], + "count_decr": [ + 6, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 1, + "value": [ + 3, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8193, + "dst": 4097, + "count": 6, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 10, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8193, + 0 + ], + "src_incr": [ + 8194, + 0, + 0, + 0 + ], + "dst": [ + 4097, + 0 + ], + "dst_incr": [ + 4098, + 0, + 0, + 0 + ], + "count": [ + 6, + 0 + ], + "count_decr": [ + 5, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 10, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8194, + "dst": 4098, + "count": 5, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 17, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8194, + 0 + ], + "src_incr": [ + 8195, + 0, + 0, + 0 + ], + "dst": [ + 4098, + 0 + ], + "dst_incr": [ + 4099, + 0, + 0, + 0 + ], + "count": [ + 5, + 0 + ], + "count_decr": [ + 4, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 17, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8195, + "dst": 4099, + "count": 4, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 24, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8195, + 0 + ], + "src_incr": [ + 8196, + 0, + 0, + 0 + ], + "dst": [ + 4099, + 0 + ], + "dst_incr": [ + 4100, + 0, + 0, + 0 + ], + "count": [ + 4, + 0 + ], + "count_decr": [ + 3, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 24, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8196, + "dst": 4100, + "count": 3, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 31, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8196, + 0 + ], + "src_incr": [ + 8197, + 0, + 0, + 0 + ], + "dst": [ + 4100, + 0 + ], + "dst_incr": [ + 4101, + 0, + 0, + 0 + ], + "count": [ + 3, + 0 + ], + "count_decr": [ + 2, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 31, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8197, + "dst": 4101, + "count": 2, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 38, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8197, + 0 + ], + "src_incr": [ + 8198, + 0, + 0, + 0 + ], + "dst": [ + 4101, + 0 + ], + "dst_incr": [ + 4102, + 0, + 0, + 0 + ], + "count": [ + 2, + 0 + ], + "count_decr": [ + 1, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 38, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8198, + "dst": 4102, + "count": 1, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 45, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8198, + 0 + ], + "src_incr": [ + 8199, + 0, + 0, + 0 + ], + "dst": [ + 4102, + 0 + ], + "dst_incr": [ + 4103, + 0, + 0, + 0 + ], + "count": [ + 1, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 45, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 8199, + "dst": 4103, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8199, + 0 + ], + "src_incr": [ + 8200, + 0, + 0, + 0 + ], + "dst": [ + 4103, + 0 + ], + "dst_incr": [ + 4104, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4096 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8192 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 7 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8192, + "timestamp": 49, + "width": 1, + "value": [ + 3 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8193, + "timestamp": 49, + "width": 1, + "value": [ + 10 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8194, + "timestamp": 49, + "width": 1, + "value": [ + 17 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8195, + "timestamp": 49, + "width": 1, + "value": [ + 24 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8196, + "timestamp": 49, + "width": 1, + "value": [ + 31 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8197, + "timestamp": 49, + "width": 1, + "value": [ + 38 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8198, + "timestamp": 49, + "width": 1, + "value": [ + 45 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4096, + "timestamp": 50, + "width": 1, + "value": [ + 3 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4097, + "timestamp": 50, + "width": 1, + "value": [ + 10 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4098, + "timestamp": 50, + "width": 1, + "value": [ + 17 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4099, + "timestamp": 50, + "width": 1, + "value": [ + 24 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4100, + "timestamp": 50, + "width": 1, + "value": [ + 31 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4101, + "timestamp": 50, + "width": 1, + "value": [ + 38 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4102, + "timestamp": 50, + "width": 1, + "value": [ + 45 + ], + "is_write": true + } + ] + }, + { + "name": "unaligned body and tail", + "timestamp": 48, + "dst": 8197, + "src": 4099, + "count": 27, + "widths": [ + 8, + 8, + 8, + 1, + 1, + 1 + ], + "data_rows": 6, + "rows": [ + { + "src": 4099, + "dst": 8197, + "count": 27, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4099, + 0 + ], + "src_incr": [ + 4107, + 0, + 0, + 0 + ], + "dst": [ + 8197, + 0 + ], + "dst_incr": [ + 8205, + 0, + 0, + 0 + ], + "count": [ + 27, + 0 + ], + "count_decr": [ + 19, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 4107, + "dst": 8205, + "count": 19, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4107, + 0 + ], + "src_incr": [ + 4115, + 0, + 0, + 0 + ], + "dst": [ + 8205, + 0 + ], + "dst_incr": [ + 8213, + 0, + 0, + 0 + ], + "count": [ + 19, + 0 + ], + "count_decr": [ + 11, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "mu": 1 + } + }, + { + "src": 4115, + "dst": 8213, + "count": 11, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4115, + 0 + ], + "src_incr": [ + 4123, + 0, + 0, + 0 + ], + "dst": [ + 8213, + 0 + ], + "dst_incr": [ + 8221, + 0, + 0, + 0 + ], + "count": [ + 11, + 0 + ], + "count_decr": [ + 3, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "mu": 1 + } + }, + { + "src": 4123, + "dst": 8221, + "count": 3, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 171, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4123, + 0 + ], + "src_incr": [ + 4124, + 0, + 0, + 0 + ], + "dst": [ + 8221, + 0 + ], + "dst_incr": [ + 8222, + 0, + 0, + 0 + ], + "count": [ + 3, + 0 + ], + "count_decr": [ + 2, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 171, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 4124, + "dst": 8222, + "count": 2, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 178, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4124, + 0 + ], + "src_incr": [ + 4125, + 0, + 0, + 0 + ], + "dst": [ + 8222, + 0 + ], + "dst_incr": [ + 8223, + 0, + 0, + 0 + ], + "count": [ + 2, + 0 + ], + "count_decr": [ + 1, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 178, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 4125, + "dst": 8223, + "count": 1, + "first": false, + "end": false, + "tail": true, + "width": 1, + "value": [ + 185, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4125, + 0 + ], + "src_incr": [ + 4126, + 0, + 0, + 0 + ], + "dst": [ + 8223, + 0 + ], + "dst_incr": [ + 8224, + 0, + 0, + 0 + ], + "count": [ + 1, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 1, + "value": [ + 185, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + }, + { + "src": 4126, + "dst": 8224, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 4126, + 0 + ], + "src_incr": [ + 4127, + 0, + 0, + 0 + ], + "dst": [ + 8224, + 0 + ], + "dst_incr": [ + 8225, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 8197 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 4099 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 27 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4099, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4107, + "timestamp": 49, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4115, + "timestamp": 49, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4123, + "timestamp": 49, + "width": 1, + "value": [ + 171 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4124, + "timestamp": 49, + "width": 1, + "value": [ + 178 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4125, + "timestamp": 49, + "width": 1, + "value": [ + 185 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8197, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + }, + { + "is_register": false, + "address": 8205, + "timestamp": 50, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": true + }, + { + "is_register": false, + "address": 8213, + "timestamp": 50, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": true + }, + { + "is_register": false, + "address": 8221, + "timestamp": 50, + "width": 1, + "value": [ + 171 + ], + "is_write": true + }, + { + "is_register": false, + "address": 8222, + "timestamp": 50, + "width": 1, + "value": [ + 178 + ], + "is_write": true + }, + { + "is_register": false, + "address": 8223, + "timestamp": 50, + "width": 1, + "value": [ + 185 + ], + "is_write": true + } + ] + }, + { + "name": "forward overlap", + "timestamp": 48, + "dst": 12292, + "src": 12288, + "count": 24, + "widths": [ + 8, + 8, + 8 + ], + "data_rows": 3, + "rows": [ + { + "src": 12288, + "dst": 12292, + "count": 24, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12288, + 0 + ], + "src_incr": [ + 12296, + 0, + 0, + 0 + ], + "dst": [ + 12292, + 0 + ], + "dst_incr": [ + 12300, + 0, + 0, + 0 + ], + "count": [ + 24, + 0 + ], + "count_decr": [ + 16, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 12296, + "dst": 12300, + "count": 16, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12296, + 0 + ], + "src_incr": [ + 12304, + 0, + 0, + 0 + ], + "dst": [ + 12300, + 0 + ], + "dst_incr": [ + 12308, + 0, + 0, + 0 + ], + "count": [ + 16, + 0 + ], + "count_decr": [ + 8, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "mu": 1 + } + }, + { + "src": 12304, + "dst": 12308, + "count": 8, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12304, + 0 + ], + "src_incr": [ + 12312, + 0, + 0, + 0 + ], + "dst": [ + 12308, + 0 + ], + "dst_incr": [ + 12316, + 0, + 0, + 0 + ], + "count": [ + 8, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "mu": 1 + } + }, + { + "src": 12312, + "dst": 12316, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12312, + 0 + ], + "src_incr": [ + 12313, + 0, + 0, + 0 + ], + "dst": [ + 12316, + 0 + ], + "dst_incr": [ + 12317, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 12292 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 12288 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 24 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12288, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12296, + "timestamp": 49, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12304, + "timestamp": 49, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12292, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + }, + { + "is_register": false, + "address": 12300, + "timestamp": 50, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": true + }, + { + "is_register": false, + "address": 12308, + "timestamp": 50, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": true + } + ] + }, + { + "name": "backward overlap", + "timestamp": 48, + "dst": 12288, + "src": 12292, + "count": 24, + "widths": [ + 8, + 8, + 8 + ], + "data_rows": 3, + "rows": [ + { + "src": 12292, + "dst": 12288, + "count": 24, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12292, + 0 + ], + "src_incr": [ + 12300, + 0, + 0, + 0 + ], + "dst": [ + 12288, + 0 + ], + "dst_incr": [ + 12296, + 0, + 0, + 0 + ], + "count": [ + 24, + 0 + ], + "count_decr": [ + 16, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 12300, + "dst": 12296, + "count": 16, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12300, + 0 + ], + "src_incr": [ + 12308, + 0, + 0, + 0 + ], + "dst": [ + 12296, + 0 + ], + "dst_incr": [ + 12304, + 0, + 0, + 0 + ], + "count": [ + 16, + 0 + ], + "count_decr": [ + 8, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "mu": 1 + } + }, + { + "src": 12308, + "dst": 12304, + "count": 8, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12308, + 0 + ], + "src_incr": [ + 12316, + 0, + 0, + 0 + ], + "dst": [ + 12304, + 0 + ], + "dst_incr": [ + 12312, + 0, + 0, + 0 + ], + "count": [ + 8, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "mu": 1 + } + }, + { + "src": 12316, + "dst": 12312, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 12316, + 0 + ], + "src_incr": [ + 12317, + 0, + 0, + 0 + ], + "dst": [ + 12312, + 0 + ], + "dst_incr": [ + 12313, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 12288 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 12292 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 24 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12292, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12300, + "timestamp": 49, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12308, + "timestamp": 49, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": false + }, + { + "is_register": false, + "address": 12288, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + }, + { + "is_register": false, + "address": 12296, + "timestamp": 50, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": true + }, + { + "is_register": false, + "address": 12304, + "timestamp": 50, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": true + } + ] + }, + { + "name": "page crossing", + "timestamp": 48, + "dst": 4092, + "src": 8188, + "count": 16, + "widths": [ + 8, + 8 + ], + "data_rows": 2, + "rows": [ + { + "src": 8188, + "dst": 4092, + "count": 16, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8188, + 0 + ], + "src_incr": [ + 8196, + 0, + 0, + 0 + ], + "dst": [ + 4092, + 0 + ], + "dst_incr": [ + 4100, + 0, + 0, + 0 + ], + "count": [ + 16, + 0 + ], + "count_decr": [ + 8, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 8196, + "dst": 4100, + "count": 8, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8196, + 0 + ], + "src_incr": [ + 8204, + 0, + 0, + 0 + ], + "dst": [ + 4100, + 0 + ], + "dst_incr": [ + 4108, + 0, + 0, + 0 + ], + "count": [ + 8, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "mu": 1 + } + }, + { + "src": 8204, + "dst": 4108, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8204, + 0 + ], + "src_incr": [ + 8205, + 0, + 0, + 0 + ], + "dst": [ + 4108, + 0 + ], + "dst_incr": [ + 4109, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4092 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8188 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 16 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8188, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8196, + "timestamp": 49, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4092, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4100, + "timestamp": 50, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": true + } + ] + }, + { + "name": "maximum chunk", + "timestamp": 48, + "dst": 4096, + "src": 8192, + "count": 256, + "widths": [ + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8, + 8 + ], + "data_rows": 32, + "rows": [ + { + "src": 8192, + "dst": 4096, + "count": 256, + "first": true, + "end": false, + "tail": false, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8192, + 0 + ], + "src_incr": [ + 8200, + 0, + 0, + 0 + ], + "dst": [ + 4096, + 0 + ], + "dst_incr": [ + 4104, + 0, + 0, + 0 + ], + "count": [ + 256, + 0 + ], + "count_decr": [ + 248, + 0, + 0, + 0 + ], + "first": 1, + "end": 0, + "tail": 0, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "mu": 1 + } + }, + { + "src": 8200, + "dst": 4104, + "count": 248, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8200, + 0 + ], + "src_incr": [ + 8208, + 0, + 0, + 0 + ], + "dst": [ + 4104, + 0 + ], + "dst_incr": [ + 4112, + 0, + 0, + 0 + ], + "count": [ + 248, + 0 + ], + "count_decr": [ + 240, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "mu": 1 + } + }, + { + "src": 8208, + "dst": 4112, + "count": 240, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8208, + 0 + ], + "src_incr": [ + 8216, + 0, + 0, + 0 + ], + "dst": [ + 4112, + 0 + ], + "dst_incr": [ + 4120, + 0, + 0, + 0 + ], + "count": [ + 240, + 0 + ], + "count_decr": [ + 232, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "mu": 1 + } + }, + { + "src": 8216, + "dst": 4120, + "count": 232, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 171, + 178, + 185, + 192, + 199, + 206, + 213, + 220 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8216, + 0 + ], + "src_incr": [ + 8224, + 0, + 0, + 0 + ], + "dst": [ + 4120, + 0 + ], + "dst_incr": [ + 4128, + 0, + 0, + 0 + ], + "count": [ + 232, + 0 + ], + "count_decr": [ + 224, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 171, + 178, + 185, + 192, + 199, + 206, + 213, + 220 + ], + "mu": 1 + } + }, + { + "src": 8224, + "dst": 4128, + "count": 224, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 227, + 234, + 241, + 248, + 255, + 6, + 13, + 20 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8224, + 0 + ], + "src_incr": [ + 8232, + 0, + 0, + 0 + ], + "dst": [ + 4128, + 0 + ], + "dst_incr": [ + 4136, + 0, + 0, + 0 + ], + "count": [ + 224, + 0 + ], + "count_decr": [ + 216, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 227, + 234, + 241, + 248, + 255, + 6, + 13, + 20 + ], + "mu": 1 + } + }, + { + "src": 8232, + "dst": 4136, + "count": 216, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 27, + 34, + 41, + 48, + 55, + 62, + 69, + 76 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8232, + 0 + ], + "src_incr": [ + 8240, + 0, + 0, + 0 + ], + "dst": [ + 4136, + 0 + ], + "dst_incr": [ + 4144, + 0, + 0, + 0 + ], + "count": [ + 216, + 0 + ], + "count_decr": [ + 208, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 27, + 34, + 41, + 48, + 55, + 62, + 69, + 76 + ], + "mu": 1 + } + }, + { + "src": 8240, + "dst": 4144, + "count": 208, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 83, + 90, + 97, + 104, + 111, + 118, + 125, + 132 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8240, + 0 + ], + "src_incr": [ + 8248, + 0, + 0, + 0 + ], + "dst": [ + 4144, + 0 + ], + "dst_incr": [ + 4152, + 0, + 0, + 0 + ], + "count": [ + 208, + 0 + ], + "count_decr": [ + 200, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 83, + 90, + 97, + 104, + 111, + 118, + 125, + 132 + ], + "mu": 1 + } + }, + { + "src": 8248, + "dst": 4152, + "count": 200, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 139, + 146, + 153, + 160, + 167, + 174, + 181, + 188 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8248, + 0 + ], + "src_incr": [ + 8256, + 0, + 0, + 0 + ], + "dst": [ + 4152, + 0 + ], + "dst_incr": [ + 4160, + 0, + 0, + 0 + ], + "count": [ + 200, + 0 + ], + "count_decr": [ + 192, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 139, + 146, + 153, + 160, + 167, + 174, + 181, + 188 + ], + "mu": 1 + } + }, + { + "src": 8256, + "dst": 4160, + "count": 192, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 195, + 202, + 209, + 216, + 223, + 230, + 237, + 244 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8256, + 0 + ], + "src_incr": [ + 8264, + 0, + 0, + 0 + ], + "dst": [ + 4160, + 0 + ], + "dst_incr": [ + 4168, + 0, + 0, + 0 + ], + "count": [ + 192, + 0 + ], + "count_decr": [ + 184, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 195, + 202, + 209, + 216, + 223, + 230, + 237, + 244 + ], + "mu": 1 + } + }, + { + "src": 8264, + "dst": 4168, + "count": 184, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 251, + 2, + 9, + 16, + 23, + 30, + 37, + 44 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8264, + 0 + ], + "src_incr": [ + 8272, + 0, + 0, + 0 + ], + "dst": [ + 4168, + 0 + ], + "dst_incr": [ + 4176, + 0, + 0, + 0 + ], + "count": [ + 184, + 0 + ], + "count_decr": [ + 176, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 251, + 2, + 9, + 16, + 23, + 30, + 37, + 44 + ], + "mu": 1 + } + }, + { + "src": 8272, + "dst": 4176, + "count": 176, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 51, + 58, + 65, + 72, + 79, + 86, + 93, + 100 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8272, + 0 + ], + "src_incr": [ + 8280, + 0, + 0, + 0 + ], + "dst": [ + 4176, + 0 + ], + "dst_incr": [ + 4184, + 0, + 0, + 0 + ], + "count": [ + 176, + 0 + ], + "count_decr": [ + 168, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 51, + 58, + 65, + 72, + 79, + 86, + 93, + 100 + ], + "mu": 1 + } + }, + { + "src": 8280, + "dst": 4184, + "count": 168, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 107, + 114, + 121, + 128, + 135, + 142, + 149, + 156 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8280, + 0 + ], + "src_incr": [ + 8288, + 0, + 0, + 0 + ], + "dst": [ + 4184, + 0 + ], + "dst_incr": [ + 4192, + 0, + 0, + 0 + ], + "count": [ + 168, + 0 + ], + "count_decr": [ + 160, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 107, + 114, + 121, + 128, + 135, + 142, + 149, + 156 + ], + "mu": 1 + } + }, + { + "src": 8288, + "dst": 4192, + "count": 160, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 163, + 170, + 177, + 184, + 191, + 198, + 205, + 212 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8288, + 0 + ], + "src_incr": [ + 8296, + 0, + 0, + 0 + ], + "dst": [ + 4192, + 0 + ], + "dst_incr": [ + 4200, + 0, + 0, + 0 + ], + "count": [ + 160, + 0 + ], + "count_decr": [ + 152, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 163, + 170, + 177, + 184, + 191, + 198, + 205, + 212 + ], + "mu": 1 + } + }, + { + "src": 8296, + "dst": 4200, + "count": 152, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 219, + 226, + 233, + 240, + 247, + 254, + 5, + 12 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8296, + 0 + ], + "src_incr": [ + 8304, + 0, + 0, + 0 + ], + "dst": [ + 4200, + 0 + ], + "dst_incr": [ + 4208, + 0, + 0, + 0 + ], + "count": [ + 152, + 0 + ], + "count_decr": [ + 144, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 219, + 226, + 233, + 240, + 247, + 254, + 5, + 12 + ], + "mu": 1 + } + }, + { + "src": 8304, + "dst": 4208, + "count": 144, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 19, + 26, + 33, + 40, + 47, + 54, + 61, + 68 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8304, + 0 + ], + "src_incr": [ + 8312, + 0, + 0, + 0 + ], + "dst": [ + 4208, + 0 + ], + "dst_incr": [ + 4216, + 0, + 0, + 0 + ], + "count": [ + 144, + 0 + ], + "count_decr": [ + 136, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 19, + 26, + 33, + 40, + 47, + 54, + 61, + 68 + ], + "mu": 1 + } + }, + { + "src": 8312, + "dst": 4216, + "count": 136, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 75, + 82, + 89, + 96, + 103, + 110, + 117, + 124 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8312, + 0 + ], + "src_incr": [ + 8320, + 0, + 0, + 0 + ], + "dst": [ + 4216, + 0 + ], + "dst_incr": [ + 4224, + 0, + 0, + 0 + ], + "count": [ + 136, + 0 + ], + "count_decr": [ + 128, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 75, + 82, + 89, + 96, + 103, + 110, + 117, + 124 + ], + "mu": 1 + } + }, + { + "src": 8320, + "dst": 4224, + "count": 128, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 131, + 138, + 145, + 152, + 159, + 166, + 173, + 180 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8320, + 0 + ], + "src_incr": [ + 8328, + 0, + 0, + 0 + ], + "dst": [ + 4224, + 0 + ], + "dst_incr": [ + 4232, + 0, + 0, + 0 + ], + "count": [ + 128, + 0 + ], + "count_decr": [ + 120, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 131, + 138, + 145, + 152, + 159, + 166, + 173, + 180 + ], + "mu": 1 + } + }, + { + "src": 8328, + "dst": 4232, + "count": 120, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 187, + 194, + 201, + 208, + 215, + 222, + 229, + 236 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8328, + 0 + ], + "src_incr": [ + 8336, + 0, + 0, + 0 + ], + "dst": [ + 4232, + 0 + ], + "dst_incr": [ + 4240, + 0, + 0, + 0 + ], + "count": [ + 120, + 0 + ], + "count_decr": [ + 112, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 187, + 194, + 201, + 208, + 215, + 222, + 229, + 236 + ], + "mu": 1 + } + }, + { + "src": 8336, + "dst": 4240, + "count": 112, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 243, + 250, + 1, + 8, + 15, + 22, + 29, + 36 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8336, + 0 + ], + "src_incr": [ + 8344, + 0, + 0, + 0 + ], + "dst": [ + 4240, + 0 + ], + "dst_incr": [ + 4248, + 0, + 0, + 0 + ], + "count": [ + 112, + 0 + ], + "count_decr": [ + 104, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 243, + 250, + 1, + 8, + 15, + 22, + 29, + 36 + ], + "mu": 1 + } + }, + { + "src": 8344, + "dst": 4248, + "count": 104, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 43, + 50, + 57, + 64, + 71, + 78, + 85, + 92 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8344, + 0 + ], + "src_incr": [ + 8352, + 0, + 0, + 0 + ], + "dst": [ + 4248, + 0 + ], + "dst_incr": [ + 4256, + 0, + 0, + 0 + ], + "count": [ + 104, + 0 + ], + "count_decr": [ + 96, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 43, + 50, + 57, + 64, + 71, + 78, + 85, + 92 + ], + "mu": 1 + } + }, + { + "src": 8352, + "dst": 4256, + "count": 96, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 99, + 106, + 113, + 120, + 127, + 134, + 141, + 148 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8352, + 0 + ], + "src_incr": [ + 8360, + 0, + 0, + 0 + ], + "dst": [ + 4256, + 0 + ], + "dst_incr": [ + 4264, + 0, + 0, + 0 + ], + "count": [ + 96, + 0 + ], + "count_decr": [ + 88, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 99, + 106, + 113, + 120, + 127, + 134, + 141, + 148 + ], + "mu": 1 + } + }, + { + "src": 8360, + "dst": 4264, + "count": 88, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 155, + 162, + 169, + 176, + 183, + 190, + 197, + 204 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8360, + 0 + ], + "src_incr": [ + 8368, + 0, + 0, + 0 + ], + "dst": [ + 4264, + 0 + ], + "dst_incr": [ + 4272, + 0, + 0, + 0 + ], + "count": [ + 88, + 0 + ], + "count_decr": [ + 80, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 155, + 162, + 169, + 176, + 183, + 190, + 197, + 204 + ], + "mu": 1 + } + }, + { + "src": 8368, + "dst": 4272, + "count": 80, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 211, + 218, + 225, + 232, + 239, + 246, + 253, + 4 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8368, + 0 + ], + "src_incr": [ + 8376, + 0, + 0, + 0 + ], + "dst": [ + 4272, + 0 + ], + "dst_incr": [ + 4280, + 0, + 0, + 0 + ], + "count": [ + 80, + 0 + ], + "count_decr": [ + 72, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 211, + 218, + 225, + 232, + 239, + 246, + 253, + 4 + ], + "mu": 1 + } + }, + { + "src": 8376, + "dst": 4280, + "count": 72, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 11, + 18, + 25, + 32, + 39, + 46, + 53, + 60 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8376, + 0 + ], + "src_incr": [ + 8384, + 0, + 0, + 0 + ], + "dst": [ + 4280, + 0 + ], + "dst_incr": [ + 4288, + 0, + 0, + 0 + ], + "count": [ + 72, + 0 + ], + "count_decr": [ + 64, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 11, + 18, + 25, + 32, + 39, + 46, + 53, + 60 + ], + "mu": 1 + } + }, + { + "src": 8384, + "dst": 4288, + "count": 64, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 67, + 74, + 81, + 88, + 95, + 102, + 109, + 116 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8384, + 0 + ], + "src_incr": [ + 8392, + 0, + 0, + 0 + ], + "dst": [ + 4288, + 0 + ], + "dst_incr": [ + 4296, + 0, + 0, + 0 + ], + "count": [ + 64, + 0 + ], + "count_decr": [ + 56, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 67, + 74, + 81, + 88, + 95, + 102, + 109, + 116 + ], + "mu": 1 + } + }, + { + "src": 8392, + "dst": 4296, + "count": 56, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 123, + 130, + 137, + 144, + 151, + 158, + 165, + 172 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8392, + 0 + ], + "src_incr": [ + 8400, + 0, + 0, + 0 + ], + "dst": [ + 4296, + 0 + ], + "dst_incr": [ + 4304, + 0, + 0, + 0 + ], + "count": [ + 56, + 0 + ], + "count_decr": [ + 48, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 123, + 130, + 137, + 144, + 151, + 158, + 165, + 172 + ], + "mu": 1 + } + }, + { + "src": 8400, + "dst": 4304, + "count": 48, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 179, + 186, + 193, + 200, + 207, + 214, + 221, + 228 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8400, + 0 + ], + "src_incr": [ + 8408, + 0, + 0, + 0 + ], + "dst": [ + 4304, + 0 + ], + "dst_incr": [ + 4312, + 0, + 0, + 0 + ], + "count": [ + 48, + 0 + ], + "count_decr": [ + 40, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 179, + 186, + 193, + 200, + 207, + 214, + 221, + 228 + ], + "mu": 1 + } + }, + { + "src": 8408, + "dst": 4312, + "count": 40, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 235, + 242, + 249, + 0, + 7, + 14, + 21, + 28 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8408, + 0 + ], + "src_incr": [ + 8416, + 0, + 0, + 0 + ], + "dst": [ + 4312, + 0 + ], + "dst_incr": [ + 4320, + 0, + 0, + 0 + ], + "count": [ + 40, + 0 + ], + "count_decr": [ + 32, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 235, + 242, + 249, + 0, + 7, + 14, + 21, + 28 + ], + "mu": 1 + } + }, + { + "src": 8416, + "dst": 4320, + "count": 32, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 35, + 42, + 49, + 56, + 63, + 70, + 77, + 84 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8416, + 0 + ], + "src_incr": [ + 8424, + 0, + 0, + 0 + ], + "dst": [ + 4320, + 0 + ], + "dst_incr": [ + 4328, + 0, + 0, + 0 + ], + "count": [ + 32, + 0 + ], + "count_decr": [ + 24, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 35, + 42, + 49, + 56, + 63, + 70, + 77, + 84 + ], + "mu": 1 + } + }, + { + "src": 8424, + "dst": 4328, + "count": 24, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 91, + 98, + 105, + 112, + 119, + 126, + 133, + 140 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8424, + 0 + ], + "src_incr": [ + 8432, + 0, + 0, + 0 + ], + "dst": [ + 4328, + 0 + ], + "dst_incr": [ + 4336, + 0, + 0, + 0 + ], + "count": [ + 24, + 0 + ], + "count_decr": [ + 16, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 91, + 98, + 105, + 112, + 119, + 126, + 133, + 140 + ], + "mu": 1 + } + }, + { + "src": 8432, + "dst": 4336, + "count": 16, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 147, + 154, + 161, + 168, + 175, + 182, + 189, + 196 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8432, + 0 + ], + "src_incr": [ + 8440, + 0, + 0, + 0 + ], + "dst": [ + 4336, + 0 + ], + "dst_incr": [ + 4344, + 0, + 0, + 0 + ], + "count": [ + 16, + 0 + ], + "count_decr": [ + 8, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 147, + 154, + 161, + 168, + 175, + 182, + 189, + 196 + ], + "mu": 1 + } + }, + { + "src": 8440, + "dst": 4344, + "count": 8, + "first": false, + "end": false, + "tail": false, + "width": 8, + "value": [ + 203, + 210, + 217, + 224, + 231, + 238, + 245, + 252 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8440, + 0 + ], + "src_incr": [ + 8448, + 0, + 0, + 0 + ], + "dst": [ + 4344, + 0 + ], + "dst_incr": [ + 4352, + 0, + 0, + 0 + ], + "count": [ + 8, + 0 + ], + "count_decr": [ + 0, + 0, + 0, + 0 + ], + "first": 0, + "end": 0, + "tail": 0, + "value": [ + 203, + 210, + 217, + 224, + 231, + 238, + 245, + 252 + ], + "mu": 1 + } + }, + { + "src": 8448, + "dst": 4352, + "count": 0, + "first": false, + "end": true, + "tail": true, + "width": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "columns": { + "timestamp": [ + 48, + 0 + ], + "src": [ + 8448, + 0 + ], + "src_incr": [ + 8449, + 0, + 0, + 0 + ], + "dst": [ + 4352, + 0 + ], + "dst_incr": [ + 4353, + 0, + 0, + 0 + ], + "count": [ + 0, + 0 + ], + "count_decr": [ + 65535, + 65535, + 65535, + 65535 + ], + "first": 0, + "end": 1, + "tail": 1, + "value": [ + 0, + 0, + 0, + 0, + 0, + 0, + 0, + 0 + ], + "mu": 1 + } + } + ], + "memw": [ + { + "is_register": true, + "address": 20, + "timestamp": 48, + "width": 2, + "value": [ + 4096 + ], + "is_write": false + }, + { + "is_register": true, + "address": 22, + "timestamp": 48, + "width": 2, + "value": [ + 8192 + ], + "is_write": false + }, + { + "is_register": true, + "address": 24, + "timestamp": 48, + "width": 2, + "value": [ + 256 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8192, + "timestamp": 49, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8200, + "timestamp": 49, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8208, + "timestamp": 49, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8216, + "timestamp": 49, + "width": 8, + "value": [ + 171, + 178, + 185, + 192, + 199, + 206, + 213, + 220 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8224, + "timestamp": 49, + "width": 8, + "value": [ + 227, + 234, + 241, + 248, + 255, + 6, + 13, + 20 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8232, + "timestamp": 49, + "width": 8, + "value": [ + 27, + 34, + 41, + 48, + 55, + 62, + 69, + 76 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8240, + "timestamp": 49, + "width": 8, + "value": [ + 83, + 90, + 97, + 104, + 111, + 118, + 125, + 132 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8248, + "timestamp": 49, + "width": 8, + "value": [ + 139, + 146, + 153, + 160, + 167, + 174, + 181, + 188 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8256, + "timestamp": 49, + "width": 8, + "value": [ + 195, + 202, + 209, + 216, + 223, + 230, + 237, + 244 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8264, + "timestamp": 49, + "width": 8, + "value": [ + 251, + 2, + 9, + 16, + 23, + 30, + 37, + 44 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8272, + "timestamp": 49, + "width": 8, + "value": [ + 51, + 58, + 65, + 72, + 79, + 86, + 93, + 100 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8280, + "timestamp": 49, + "width": 8, + "value": [ + 107, + 114, + 121, + 128, + 135, + 142, + 149, + 156 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8288, + "timestamp": 49, + "width": 8, + "value": [ + 163, + 170, + 177, + 184, + 191, + 198, + 205, + 212 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8296, + "timestamp": 49, + "width": 8, + "value": [ + 219, + 226, + 233, + 240, + 247, + 254, + 5, + 12 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8304, + "timestamp": 49, + "width": 8, + "value": [ + 19, + 26, + 33, + 40, + 47, + 54, + 61, + 68 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8312, + "timestamp": 49, + "width": 8, + "value": [ + 75, + 82, + 89, + 96, + 103, + 110, + 117, + 124 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8320, + "timestamp": 49, + "width": 8, + "value": [ + 131, + 138, + 145, + 152, + 159, + 166, + 173, + 180 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8328, + "timestamp": 49, + "width": 8, + "value": [ + 187, + 194, + 201, + 208, + 215, + 222, + 229, + 236 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8336, + "timestamp": 49, + "width": 8, + "value": [ + 243, + 250, + 1, + 8, + 15, + 22, + 29, + 36 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8344, + "timestamp": 49, + "width": 8, + "value": [ + 43, + 50, + 57, + 64, + 71, + 78, + 85, + 92 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8352, + "timestamp": 49, + "width": 8, + "value": [ + 99, + 106, + 113, + 120, + 127, + 134, + 141, + 148 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8360, + "timestamp": 49, + "width": 8, + "value": [ + 155, + 162, + 169, + 176, + 183, + 190, + 197, + 204 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8368, + "timestamp": 49, + "width": 8, + "value": [ + 211, + 218, + 225, + 232, + 239, + 246, + 253, + 4 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8376, + "timestamp": 49, + "width": 8, + "value": [ + 11, + 18, + 25, + 32, + 39, + 46, + 53, + 60 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8384, + "timestamp": 49, + "width": 8, + "value": [ + 67, + 74, + 81, + 88, + 95, + 102, + 109, + 116 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8392, + "timestamp": 49, + "width": 8, + "value": [ + 123, + 130, + 137, + 144, + 151, + 158, + 165, + 172 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8400, + "timestamp": 49, + "width": 8, + "value": [ + 179, + 186, + 193, + 200, + 207, + 214, + 221, + 228 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8408, + "timestamp": 49, + "width": 8, + "value": [ + 235, + 242, + 249, + 0, + 7, + 14, + 21, + 28 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8416, + "timestamp": 49, + "width": 8, + "value": [ + 35, + 42, + 49, + 56, + 63, + 70, + 77, + 84 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8424, + "timestamp": 49, + "width": 8, + "value": [ + 91, + 98, + 105, + 112, + 119, + 126, + 133, + 140 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8432, + "timestamp": 49, + "width": 8, + "value": [ + 147, + 154, + 161, + 168, + 175, + 182, + 189, + 196 + ], + "is_write": false + }, + { + "is_register": false, + "address": 8440, + "timestamp": 49, + "width": 8, + "value": [ + 203, + 210, + 217, + 224, + 231, + 238, + 245, + 252 + ], + "is_write": false + }, + { + "is_register": false, + "address": 4096, + "timestamp": 50, + "width": 8, + "value": [ + 3, + 10, + 17, + 24, + 31, + 38, + 45, + 52 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4104, + "timestamp": 50, + "width": 8, + "value": [ + 59, + 66, + 73, + 80, + 87, + 94, + 101, + 108 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4112, + "timestamp": 50, + "width": 8, + "value": [ + 115, + 122, + 129, + 136, + 143, + 150, + 157, + 164 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4120, + "timestamp": 50, + "width": 8, + "value": [ + 171, + 178, + 185, + 192, + 199, + 206, + 213, + 220 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4128, + "timestamp": 50, + "width": 8, + "value": [ + 227, + 234, + 241, + 248, + 255, + 6, + 13, + 20 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4136, + "timestamp": 50, + "width": 8, + "value": [ + 27, + 34, + 41, + 48, + 55, + 62, + 69, + 76 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4144, + "timestamp": 50, + "width": 8, + "value": [ + 83, + 90, + 97, + 104, + 111, + 118, + 125, + 132 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4152, + "timestamp": 50, + "width": 8, + "value": [ + 139, + 146, + 153, + 160, + 167, + 174, + 181, + 188 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4160, + "timestamp": 50, + "width": 8, + "value": [ + 195, + 202, + 209, + 216, + 223, + 230, + 237, + 244 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4168, + "timestamp": 50, + "width": 8, + "value": [ + 251, + 2, + 9, + 16, + 23, + 30, + 37, + 44 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4176, + "timestamp": 50, + "width": 8, + "value": [ + 51, + 58, + 65, + 72, + 79, + 86, + 93, + 100 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4184, + "timestamp": 50, + "width": 8, + "value": [ + 107, + 114, + 121, + 128, + 135, + 142, + 149, + 156 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4192, + "timestamp": 50, + "width": 8, + "value": [ + 163, + 170, + 177, + 184, + 191, + 198, + 205, + 212 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4200, + "timestamp": 50, + "width": 8, + "value": [ + 219, + 226, + 233, + 240, + 247, + 254, + 5, + 12 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4208, + "timestamp": 50, + "width": 8, + "value": [ + 19, + 26, + 33, + 40, + 47, + 54, + 61, + 68 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4216, + "timestamp": 50, + "width": 8, + "value": [ + 75, + 82, + 89, + 96, + 103, + 110, + 117, + 124 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4224, + "timestamp": 50, + "width": 8, + "value": [ + 131, + 138, + 145, + 152, + 159, + 166, + 173, + 180 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4232, + "timestamp": 50, + "width": 8, + "value": [ + 187, + 194, + 201, + 208, + 215, + 222, + 229, + 236 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4240, + "timestamp": 50, + "width": 8, + "value": [ + 243, + 250, + 1, + 8, + 15, + 22, + 29, + 36 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4248, + "timestamp": 50, + "width": 8, + "value": [ + 43, + 50, + 57, + 64, + 71, + 78, + 85, + 92 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4256, + "timestamp": 50, + "width": 8, + "value": [ + 99, + 106, + 113, + 120, + 127, + 134, + 141, + 148 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4264, + "timestamp": 50, + "width": 8, + "value": [ + 155, + 162, + 169, + 176, + 183, + 190, + 197, + 204 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4272, + "timestamp": 50, + "width": 8, + "value": [ + 211, + 218, + 225, + 232, + 239, + 246, + 253, + 4 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4280, + "timestamp": 50, + "width": 8, + "value": [ + 11, + 18, + 25, + 32, + 39, + 46, + 53, + 60 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4288, + "timestamp": 50, + "width": 8, + "value": [ + 67, + 74, + 81, + 88, + 95, + 102, + 109, + 116 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4296, + "timestamp": 50, + "width": 8, + "value": [ + 123, + 130, + 137, + 144, + 151, + 158, + 165, + 172 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4304, + "timestamp": 50, + "width": 8, + "value": [ + 179, + 186, + 193, + 200, + 207, + 214, + 221, + 228 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4312, + "timestamp": 50, + "width": 8, + "value": [ + 235, + 242, + 249, + 0, + 7, + 14, + 21, + 28 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4320, + "timestamp": 50, + "width": 8, + "value": [ + 35, + 42, + 49, + 56, + 63, + 70, + 77, + 84 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4328, + "timestamp": 50, + "width": 8, + "value": [ + 91, + 98, + 105, + 112, + 119, + 126, + 133, + 140 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4336, + "timestamp": 50, + "width": 8, + "value": [ + 147, + 154, + 161, + 168, + 175, + 182, + 189, + 196 + ], + "is_write": true + }, + { + "is_register": false, + "address": 4344, + "timestamp": 50, + "width": 8, + "value": [ + 203, + 210, + 217, + 224, + 231, + 238, + 245, + 252 + ], + "is_write": true + } + ] + } +] diff --git a/formal_verification/dma/dma_ref.py b/formal_verification/dma/dma_ref.py new file mode 100644 index 000000000..be8614934 --- /dev/null +++ b/formal_verification/dma/dma_ref.py @@ -0,0 +1,339 @@ +""" +Independent reference model for the DMA memcpy ecall (PR #874). + +Three levels, deliberately written as three separate functions so they can be +checked against each other rather than sharing a helper: + + 1. BYTE level -- `memcpy_ref`: the C `memcpy`/`memmove` contract. Snapshot + the source, then write. This is the semantics a guest is + entitled to, and the only level a guest can observe. + 2. ROW level -- `row_decomposition`: the row sequence the DMA AIR table is + obliged to contain for one ecall. Eight bytes per row while + `count >= 8`, then one byte per row, then one terminal row. + 3. BUS level -- `memw_ops`: the MEMW multiset a correct trace must emit -- + three register reads at T, every source read at T+1, every + destination write at T+2. + +`replay_memw` runs level 3 back down to level 1, which is what makes the row +decomposition falsifiable: `replay_memw(memw_ops(...)) == memcpy_ref(...)` must +hold for every length and every overlap configuration, and the mutants in +`test_ref.py` must break it. + +`chunk_ecalls` is the fourth level above all of these: the guest's strong +`memcpy` symbol (`syscalls/src/syscalls.rs`) is a loop that issues one ecall per +<= `DMA_MEMCPY_MAX_BYTES` bytes, so a guest-visible `memcpy` of arbitrary length +is a *composition* of the above. + +NOTHING here reads the Rust implementation. The constants and the ABI are +transcribed from it (`executor/src/vm/instruction/execution.rs`, +`prover/src/tables/{dma.rs,trace_builder.rs}`); the transcription is audited in +`../TRANSCRIPTION-AUDIT.md`. +""" + +from dataclasses import dataclass, field + +# --------------------------------------------------------------------------- +# Constants (transcribed; asserted against the Rust source by the audit script) +# --------------------------------------------------------------------------- + +#: `executor::vm::instruction::execution::DMA_MEMCPY_SYSCALL_NUMBER` +DMA_MEMCPY_SYSCALL_NUMBER = (1 << 64) - 3 # u64::MAX - 2 + +#: `executor::vm::instruction::execution::DMA_MEMCPY_MAX_BYTES` +DMA_MEMCPY_MAX_BYTES = 256 + +#: Address space; both `src + n` and `dst + n` must stay inside it. +ADDRESS_SPACE = 1 << 64 + +#: The wide row width, and the tail row width. +WIDE_WIDTH = 8 +TAIL_WIDTH = 1 + +#: Argument registers. memcpy(dst = x10, src = x11, n = x12). +REG_DST, REG_SRC, REG_COUNT = 10, 11, 12 + +#: MEMW timestamp offsets relative to the ecall timestamp T. +TS_REGISTERS = 0 +TS_READ = 1 +TS_WRITE = 2 + + +class DmaRejected(Exception): + """The executor refuses the ecall (`n` too large, or a wrapping range).""" + + +# --------------------------------------------------------------------------- +# Level 1 -- byte semantics +# --------------------------------------------------------------------------- + +def validate(dst: int, src: int, n: int) -> None: + """The executor's three preconditions, in its own order. + + `n > MAX` is rejected first, so the chunk-bound error is what a guest sees + for an oversized call even if the range would also have wrapped. + """ + if n > DMA_MEMCPY_MAX_BYTES: + raise DmaRejected(f"chunk has {n} bytes; maximum per ecall is {DMA_MEMCPY_MAX_BYTES}") + if dst + n >= ADDRESS_SPACE: + raise DmaRejected("destination range wraps the address space") + if src + n >= ADDRESS_SPACE: + raise DmaRejected("source range wraps the address space") + + +def memcpy_ref(memory: dict, dst: int, src: int, n: int) -> dict: + """`memmove(dst, src, n)` on a sparse byte-addressed memory. + + Reads the whole source before writing anything, so overlapping regions get + snapshot semantics -- the executor copies through a fixed scratch buffer for + exactly this reason. Unwritten memory reads as zero, matching the VM. + + Returns a NEW memory; the input is not mutated. + """ + validate(dst, src, n) + snapshot = [memory.get(src + i, 0) for i in range(n)] + out = dict(memory) + for i, byte in enumerate(snapshot): + out[dst + i] = byte + return out + + +# --------------------------------------------------------------------------- +# Level 2 -- row decomposition +# --------------------------------------------------------------------------- + +def row_widths(n: int) -> list: + """The width of each data row, in order. + + Greedy and deliberately *not* `[8]*(n//8) + [1]*(n%8)`: the AIR decides one + row at a time from the remaining count (`tail = count < 8`), so the model + decides one row at a time too. That the closed form agrees is a property the + harness checks, not an assumption the model makes. + """ + widths, remaining = [], n + while remaining != 0: + width = WIDE_WIDTH if remaining >= WIDE_WIDTH else TAIL_WIDTH + widths.append(width) + remaining -= width + return widths + + +@dataclass +class DmaRow: + """One row of the DMA table. Mirrors `prover::tables::dma::DmaOperation`.""" + timestamp: int + src: int + dst: int + count: int + first: bool + end: bool + value: list = field(default_factory=lambda: [0] * 8) + + @property + def tail(self) -> bool: + """`tail` is a *derived* column: the AIR pins it with an LT lookup.""" + return self.count < WIDE_WIDTH + + @property + def width(self) -> int: + return TAIL_WIDTH if self.tail else WIDE_WIDTH + + +def row_decomposition(timestamp: int, dst: int, src: int, n: int, memory: dict = None) -> list: + """The rows a correct DMA trace must contain for one ecall, in chain order. + + One data row per copied chunk plus exactly one terminal row (`count == 0`, + `end = 1`). `first` marks the head. `value` holds the copied bytes, + zero-padded past the row's width -- the AIR forces those lanes to zero on + tail rows, so the model must produce them zeroed too. + + `memory` is only needed to fill `value`; omit it for a shape-only model. + """ + validate(dst, src, n) + memory = memory or {} + rows, offset, remaining = [], 0, n + while remaining != 0: + width = WIDE_WIDTH if remaining >= WIDE_WIDTH else TAIL_WIDTH + value = [memory.get(src + offset + i, 0) for i in range(width)] + [0] * (8 - width) + rows.append(DmaRow( + timestamp=timestamp, + src=src + offset, + dst=dst + offset, + count=remaining, + first=not rows, + end=False, + value=value, + )) + offset += width + remaining -= width + rows.append(DmaRow( + timestamp=timestamp, + src=src + n, + dst=dst + n, + count=0, + first=not rows, # true only for n == 0: one row that is both + end=True, + value=[0] * 8, + )) + return rows + + +# --------------------------------------------------------------------------- +# Level 3 -- the MEMW multiset +# --------------------------------------------------------------------------- + +@dataclass(frozen=True) +class MemwOp: + """One memory-bus operation. `is_write=False` leaves memory unchanged.""" + is_register: bool + address: int + timestamp: int + width: int + value: tuple + is_write: bool + + +def memw_ops(timestamp: int, dst: int, src: int, n: int, memory: dict) -> list: + """Every MEMW operation one DMA ecall must put on the bus. + + Order matters only through the timestamps: registers at T, *all* source + reads at T+1, *all* destination writes at T+2. The two-phase split is what + makes overlap well defined -- see `test_ref.py`'s `write_before_read` + mutant, which is caught only by the overlapping cases. + """ + validate(dst, src, n) + ops = [ + MemwOp(True, 2 * REG_DST, timestamp + TS_REGISTERS, 2, (dst,), False), + MemwOp(True, 2 * REG_SRC, timestamp + TS_REGISTERS, 2, (src,), False), + MemwOp(True, 2 * REG_COUNT, timestamp + TS_REGISTERS, 2, (n,), False), + ] + reads, writes, offset = [], [], 0 + for width in row_widths(n): + chunk = tuple(memory.get(src + offset + i, 0) for i in range(width)) + reads.append(MemwOp(False, src + offset, timestamp + TS_READ, width, chunk, False)) + writes.append(MemwOp(False, dst + offset, timestamp + TS_WRITE, width, chunk, True)) + offset += width + return ops + reads + writes + + +def replay_memw(ops: list, memory: dict) -> dict: + """Apply a MEMW list to memory in timestamp order. Reads must be faithful. + + Raises if a read op's recorded value disagrees with memory at its + timestamp -- that is the memory-consistency argument the MEMW table proves, + modelled here so a mis-ordered op list fails loudly instead of quietly + producing the right answer. + """ + out = dict(memory) + for op in sorted(ops, key=lambda o: o.timestamp): + if op.is_register: + continue + if op.is_write: + for i, byte in enumerate(op.value): + out[op.address + i] = byte + else: + seen = tuple(out.get(op.address + i, 0) for i in range(op.width)) + if seen != op.value: + raise AssertionError( + f"read at {op.address:#x}@{op.timestamp} recorded {op.value}, memory has {seen}" + ) + return out + + +# --------------------------------------------------------------------------- +# Level 4 -- the guest stub's chunking loop +# --------------------------------------------------------------------------- + +def chunk_ecalls(dst: int, src: int, n: int) -> list: + """The `(dst, src, count)` triples the guest's `memcpy` stub issues. + + Transcribed from the inline assembly in `syscalls/src/syscalls.rs`: while + bytes remain, take `min(remaining, MAX)`, ecall, then advance both pointers + by the chunk. `n == 0` issues no ecall at all (the leading `beqz`). + """ + calls, offset, remaining = [], 0, n + while remaining != 0: + chunk = min(remaining, DMA_MEMCPY_MAX_BYTES) + calls.append((dst + offset, src + offset, chunk)) + offset += chunk + remaining -= chunk + return calls + + +def guest_memcpy(memory: dict, dst: int, src: int, n: int) -> tuple: + """What a guest calling `memcpy` observes: the memory effect and the return. + + NOTE the semantics change at this level. Per chunk the copy is a snapshot, + but *across* chunks it is not: chunk k+1 reads memory chunk k already wrote. + That is plain forward `memmove`, correct for `dst < src` and for + non-overlapping ranges, and NOT a `memmove` for `dst > src` with an overlap + of more than `MAX` bytes. `memcpy`'s contract does not cover overlap, so + this is in-contract -- but it means the DMA ecall's per-call snapshot is not + a `memmove` guarantee at the C level. Recorded in ORACLE.md as O2. + """ + out = dict(memory) + for chunk_dst, chunk_src, chunk_n in chunk_ecalls(dst, src, n): + out = memcpy_ref(out, chunk_dst, chunk_src, chunk_n) + return out, dst + + +# --------------------------------------------------------------------------- +# Column encodings -- the AIR's view of a row +# --------------------------------------------------------------------------- + +def dword_wl(value: int) -> list: + """`DWordWL`: two 32-bit words, little-endian. `set_dword_wl`.""" + return [value & 0xFFFF_FFFF, (value >> 32) & 0xFFFF_FFFF] + + +def dword_hl(value: int) -> list: + """`DWordHL`: four 16-bit halfwords, little-endian. `set_dword_hl`.""" + return [(value >> (16 * i)) & 0xFFFF for i in range(4)] + + +def row_columns(row: DmaRow) -> dict: + """Every committed column of one DMA row, by name. + + This is the object the z3 gate pins for its positive controls and the + object the Rust trace generator must produce; keeping it here (rather than + inside the gate) is what lets the gate's completeness sweep be an + *oracle-driven* check instead of a self-consistency check. + """ + width = row.width + return { + "timestamp": dword_wl(row.timestamp), + "src": dword_wl(row.src), + "src_incr": dword_hl((row.src + width) % ADDRESS_SPACE), + "dst": dword_wl(row.dst), + "dst_incr": dword_hl((row.dst + width) % ADDRESS_SPACE), + "count": dword_wl(row.count), + "count_decr": dword_hl((row.count - width) % ADDRESS_SPACE), + "first": int(row.first), + "end": int(row.end), + "tail": int(row.tail), + "value": list(row.value), + "mu": 1, + } + + +def padding_columns() -> dict: + """The padding row the trace generator emits (`generate_dma_trace`). + + `mu = 0` kills every bus interaction, but the arithmetic constraints on + `count_decr` are unconditional, so padding must still satisfy them: + `count = 1`, `tail = 1` (width 1), `count_decr = 0`. `src_incr`/`dst_incr` + are 1 so their low carry is zero rather than `-1`. + """ + return { + "timestamp": [0, 0], + "src": [0, 0], + "src_incr": [1, 0, 0, 0], + "dst": [0, 0], + "dst_incr": [1, 0, 0, 0], + "count": [1, 0], + "count_decr": [0, 0, 0, 0], + "first": 0, + "end": 0, + "tail": 1, + "value": [0] * 8, + "mu": 0, + } diff --git a/formal_verification/dma/tamper_test.py b/formal_verification/dma/tamper_test.py new file mode 100644 index 000000000..778b7dd1c --- /dev/null +++ b/formal_verification/dma/tamper_test.py @@ -0,0 +1,160 @@ +""" +Tamper tests: are the oracle's anchors sensitive, or do they pass vacuously? + +Split out of `test_ref.py` so the two jobs are separable, following the shape +PR #923 established for `formal_verification/` (`test_ref.py` checks the model, +`tamper_test.py` checks the checks). Each mutant below is a deliberate defect in +`dma_ref`; every one must be caught by the anchor it targets, and a mutant whose +anchor SKIPped is reported `NOT RUN` rather than credited as caught. + + python3 tamper_test.py # full + python3 tamper_test.py --quick # shorter sweeps + +Imported by `test_ref.py` so `python3 test_ref.py` still runs the whole board. +""" + +import sys + +import dma_ref as ref +from test_ref import ( + MAX, anchor_chunking, anchor_libc, anchor_row_level, anchor_slice_assign, +) + +# --------------------------------------------------------------------------- +# [5] mutation sweep -- are the anchors above sensitive? +# --------------------------------------------------------------------------- + +def _mutant_all_ones(n): + return [1] * n + + +def _mutant_always_wide(n): + return [8] * ((n + 7) // 8) + + +def _mutant_off_by_one_tail(n): + widths, remaining = [], n + while remaining != 0: + width = 8 if remaining > 8 else 1 # `>` instead of `>=` + widths.append(min(width, remaining)) + remaining -= widths[-1] + return widths + + +def _mutant_write_before_read(timestamp, dst, src, n, memory): + """Reads at T+2, writes at T+1: the copy stops being a snapshot.""" + ops = ref.memw_ops(timestamp, dst, src, n, memory) + return [ + op if op.is_register else + type(op)(op.is_register, op.address, + timestamp + (1 if op.is_write else 2), + op.width, op.value, op.is_write) + for op in ops + ] + + +def _mutant_interleaved(timestamp, dst, src, n, memory): + """Each chunk written immediately after it is read (per-chunk timestamps).""" + out = [op for op in ref.memw_ops(timestamp, dst, src, n, memory) if op.is_register] + offset = 0 + for i, width in enumerate(ref.row_widths(n)): + chunk = tuple(memory.get(src + offset + j, 0) for j in range(width)) + out.append(ref.MemwOp(False, src + offset, timestamp + 1 + 2 * i, width, chunk, False)) + out.append(ref.MemwOp(False, dst + offset, timestamp + 2 + 2 * i, width, chunk, True)) + offset += width + return out + + +def _mutant_no_snapshot(memory, dst, src, n): + """Copy byte-by-byte with no snapshot: correct for disjoint ranges, wrong for + a backward overlap. The control for anchors 1 and 2, which had none -- + every other mutant targets `row_widths`/`memw_ops`/`chunk_ecalls`, i.e. + anchors 3 and 4, so nothing demonstrated the two external differentials can + fail at all.""" + ref.validate(dst, src, n) + out = dict(memory) + for i in range(n): + out[dst + i] = out.get(src + i, 0) + return out + + +def _mutant_chunk_257(dst, src, n): + calls, offset, remaining = [], 0, n + while remaining != 0: + c = min(remaining, MAX + 1) # one byte over the executor's bound + calls.append((dst + offset, src + offset, c)) + offset += c + remaining -= c + return calls + + +def _with_memcpy_ref(replacement, run): + """Temporarily swap `dma_ref.memcpy_ref`, so anchors 1/2 can be mutated too. + + Those two anchors call it through the module rather than via an injection + point, so unlike `row_widths`/`memw_ops` they cannot be parameterised. + """ + original = ref.memcpy_ref + ref.memcpy_ref = replacement + try: + return run() + finally: + ref.memcpy_ref = original + + +def anchor_mutations(quick: bool): + """Every mutant must be caught by the anchor it targets.""" + mutants = [ + ("memcpy_ref without snapshot", lambda: _with_memcpy_ref( + _mutant_no_snapshot, lambda: anchor_libc(quick))), + ("memcpy_ref without snapshot (slice)", lambda: _with_memcpy_ref( + _mutant_no_snapshot, lambda: anchor_slice_assign(quick))), + ("row_widths = all ones", lambda: anchor_row_level(quick, widths=_mutant_all_ones)), + ("row_widths = always wide", lambda: anchor_row_level(quick, widths=_mutant_always_wide)), + ("row_widths tail off by one", lambda: anchor_row_level(quick, widths=_mutant_off_by_one_tail)), + ("memw write before read", lambda: anchor_row_level(quick, ops=_mutant_write_before_read)), + ("memw read/write interleaved", lambda: anchor_row_level(quick, ops=_mutant_interleaved)), + ("chunk_ecalls at MAX+1", lambda: anchor_chunking(quick, chunk=_mutant_chunk_257)), + ] + survivors, not_run = [], [] + for name, run in mutants: + try: + ok, _ = run() + except (AssertionError, ref.DmaRejected): + ok = False # replay_memw or the executor bound caught it + # THREE states, not two. An anchor that SKIPped returns `ok is None`, and + # `if ok:` would score that as "caught" -- a mutant credited to a check + # that never ran. That is exactly the cascade this module's docstring + # promises cannot happen, and it bit the two `memcpy_ref` mutants, whose + # anchors (libc, CPython) are the ones that can be unavailable. + if ok is None: + not_run.append(name) + verdict = "NOT RUN (anchor skipped)" + elif ok: + survivors.append(name) + verdict = "SURVIVED (bad)" + else: + verdict = "caught" + print(f" mutant {name:32s} -> {verdict}") + if survivors: + return False, f"{len(survivors)} mutant(s) survived: {', '.join(survivors)}" + if not_run: + return None, (f"{len(mutants) - len(not_run)}/{len(mutants)} caught; " + f"{len(not_run)} not run: {', '.join(not_run)}") + return True, f"all {len(mutants)} mutants caught" + + + +def main(): + quick = "--quick" in sys.argv + print("=" * 72) + print("DMA memcpy oracle -- tamper tests" + (" (--quick)" if quick else "")) + print("=" * 72) + ok, detail = anchor_mutations(quick) + label = {True: "PASS", False: "FAIL", None: "PARTIAL"}[ok] + print(f"\n {label} {detail}") + sys.exit(0 if ok is True else (2 if ok is None else 1)) + + +if __name__ == "__main__": + main() diff --git a/formal_verification/dma/test_ref.py b/formal_verification/dma/test_ref.py new file mode 100644 index 000000000..15bf04302 --- /dev/null +++ b/formal_verification/dma/test_ref.py @@ -0,0 +1,409 @@ +""" +Validation harness for `dma_ref.py`, and the emitter for the canonical vectors. + +Five independent anchors. Each one SKIPs on its own if its dependency is +missing; a missing anchor never cascades into the others and never lets the +banner claim more than actually ran (the two harness defects the BLAKE3 +campaign had to fix after the fact -- see README.md). + + [1] libc `memmove` -- an implementation nobody here wrote + [2] CPython slice assign -- a second such implementation + [3] row/bus <-> byte level -- the decomposition really implements the copy + [4] chunking composition -- the guest stub really implements a long memcpy + [5] mutation sweep -- the anchors above are sensitive, not vacuous + +Anchors 1 and 2 pin the *semantics*. Anchor 3 is the one the chip depends on: +it is the only check that the row sequence the AIR proves is the byte copy the +guest asked for. Anchor 5 is what makes 1-4 worth running. + + python3 test_ref.py # run everything, emit the vectors + python3 test_ref.py --quick # skip the exhaustive length sweeps +""" + +import ctypes +import ctypes.util +import json +import os +import random +import sys + +import dma_ref as ref +from dma_ref import DMA_MEMCPY_MAX_BYTES as MAX + +HERE = os.path.dirname(os.path.abspath(__file__)) +VECTORS = os.path.join(HERE, "canonical_dma_vectors.json") +ROW_TABLE = os.path.join(HERE, "canonical_dma_rows.txt") + +#: Overlap configurations every sweep runs. `delta = dst - src`. +#: 0 is the aliasing case; +-1/+-7 straddle a wide row; +-8 is exactly one row; +#: +-9/+-64 are the near cases; +-2048 is disjoint. +#: Bounded by REGION/4 so `src_off + delta` and `+ MAX` stay inside the buffer -- +#: an out-of-range offset would make the libc anchor read past its own buffer and +#: "pass" on garbage. +DELTAS = [0, 1, -1, 7, -7, 8, -8, 9, -9, 64, -64, 255, -255, 2048, -2048] + +BASE = 0x10_0000 +REGION = 8192 +#: Every sweep copies from here, so both overlap directions have room. +SRC_OFF = REGION // 2 +MID = BASE + SRC_OFF + +assert all(0 <= SRC_OFF + d and SRC_OFF + d + MAX <= REGION for d in DELTAS), \ + "a delta would put the destination outside the test region" + + +def _region(seed: int, size: int) -> dict: + """A deterministic pseudo-random byte region based at `BASE`.""" + rng = random.Random(seed) + return {BASE + i: rng.randrange(256) for i in range(size)} + + +# --------------------------------------------------------------------------- +# [1] libc memmove +# --------------------------------------------------------------------------- + +def anchor_libc(quick: bool): + """Differential against the platform C library's own `memmove`. + + Genuinely non-circular: `dma_ref.memcpy_ref` and libc share no code, and + libc is the definition the guest's compiler-builtin `memcpy` was replacing. + Overlap is included, which is where `memcpy` and `memmove` diverge and + where the executor's snapshot buffer is the deciding implementation choice. + """ + path = ctypes.util.find_library("c") + if path is None: + return None, "libc not found" + # `find_library` returning a path does NOT mean it loads: it can hand back a + # GNU ld linker script (`libc.so`), an arch-mismatched hit from the ldconfig + # cache, or a path that has since gone (chroot, slim container). An uncaught + # OSError here killed the whole run before anchors 2-5 and before any banner + # printed -- breaking this module's "a missing anchor never cascades" promise. + try: + libc = ctypes.CDLL(path) + libc.memmove.restype = ctypes.c_void_p + libc.memmove.argtypes = [ctypes.c_void_p, ctypes.c_void_p, ctypes.c_size_t] + except (OSError, AttributeError) as exc: + return None, f"libc at {path} is not loadable ({exc})" + + cases = 0 + lengths = range(0, MAX + 1) if not quick else [0, 1, 7, 8, 9, 15, 16, 255, MAX] + for n in lengths: + for delta in DELTAS: + src_off = SRC_OFF + dst_off = src_off + delta + initial = _region(n * 131 + delta, REGION) + + buf = ctypes.create_string_buffer( + bytes(initial.get(BASE + i, 0) for i in range(REGION)), REGION) + libc.memmove(ctypes.byref(buf, dst_off), ctypes.byref(buf, src_off), n) + expected = list(buf.raw[:REGION]) + + got = ref.memcpy_ref(initial, BASE + dst_off, BASE + src_off, n) + actual = [got.get(BASE + i, 0) for i in range(REGION)] + if actual != expected: + return False, f"n={n} delta={delta}: disagrees with libc memmove" + cases += 1 + return True, f"{cases} cases x overlap/alignment, all agree" + + +# --------------------------------------------------------------------------- +# [2] CPython slice assignment +# --------------------------------------------------------------------------- + +def anchor_slice_assign(quick: bool): + """Differential against `bytearray[a:b] = bytearray[c:d]`. + + CPython materialises the right-hand slice first, so this is a `memmove` too, + written by yet another set of hands. Cheap, and it catches a snapshot bug + even on a platform whose libc anchor is unavailable. + """ + cases = 0 + lengths = range(0, MAX + 1) if not quick else [0, 1, 8, 9, 200, MAX] + for n in lengths: + for delta in DELTAS: + src_off = SRC_OFF + dst_off = src_off + delta + initial = _region(n * 977 + delta, REGION) + + buf = bytearray(initial.get(BASE + i, 0) for i in range(REGION)) + buf[dst_off:dst_off + n] = buf[src_off:src_off + n] + + got = ref.memcpy_ref(initial, BASE + dst_off, BASE + src_off, n) + if [got.get(BASE + i, 0) for i in range(REGION)] != list(buf): + return False, f"n={n} delta={delta}: disagrees with slice assignment" + cases += 1 + return True, f"{cases} cases x overlap/alignment, all agree" + + +# --------------------------------------------------------------------------- +# [3] row/bus level <-> byte level +# --------------------------------------------------------------------------- + +def anchor_row_level(quick: bool, widths=None, ops=None): + """The decomposition the AIR proves implements the copy the guest asked for. + + Four claims, all over every length 0..MAX x every overlap configuration: + (a) replaying the MEMW multiset reproduces `memcpy_ref` byte for byte; + (b) the row widths sum to `n` and the row `src`/`dst`/`count` sequence is + exactly `src + prefix`, `dst + prefix`, `n - prefix`; + (c) there is exactly one `first` row and exactly one `end` row, the `end` + row has `count == 0`, and no other row does; + (d) the greedy width loop equals the closed form `[8]*(n//8) + [1]*(n%8)`. + + `widths`/`ops` are injection points for the mutation sweep. + """ + widths = widths or ref.row_widths + ops = ops or ref.memw_ops + + lengths = range(0, MAX + 1) if not quick else [0, 1, 7, 8, 9, 16, 27, 255, MAX] + for n in lengths: + if widths(n) != [8] * (n // 8) + [1] * (n % 8): + return False, f"n={n}: greedy widths disagree with the closed form" + if sum(widths(n)) != n: + return False, f"n={n}: widths sum to {sum(widths(n))}" + + for delta in DELTAS: + src = MID + dst = MID + delta + initial = _region(n * 31 + delta, REGION) + + replayed = ref.replay_memw(ops(1000, dst, src, n, initial), initial) + expected = ref.memcpy_ref(initial, dst, src, n) + if replayed != expected: + return False, f"n={n} delta={delta}: MEMW replay != memcpy_ref" + + rows = ref.row_decomposition(1000, dst, src, n, initial) + if sum(1 for r in rows if r.first) != 1: + return False, f"n={n}: not exactly one first row" + if sum(1 for r in rows if r.end) != 1: + return False, f"n={n}: not exactly one end row" + if not rows[-1].end or rows[-1].count != 0: + return False, f"n={n}: last row is not the terminal row" + if any(r.count == 0 for r in rows[:-1]): + return False, f"n={n}: a data row has count == 0" + + offset = 0 + for row, width in zip(rows[:-1], widths(n)): + if (row.src, row.dst, row.count, row.width) != ( + src + offset, dst + offset, n - offset, width): + return False, f"n={n} delta={delta}: row at offset {offset} is wrong" + if row.value[width:] != [0] * (8 - width): + return False, f"n={n}: unused value lanes are not zero" + offset += width + return True, f"{len(list(lengths))} lengths x {len(DELTAS)} overlaps, replay == memcpy_ref" + + +# --------------------------------------------------------------------------- +# [4] the guest stub's chunking +# --------------------------------------------------------------------------- + +def anchor_chunking(quick: bool, chunk=None): + """`chunk_ecalls` composed over the reference is a `memcpy` of any length. + + Three claims: no chunk exceeds the bound (an oversized chunk is what the + executor rejects); the chunk count is `ceil(n / MAX)`; and for + non-overlapping ranges the composition equals a single `memcpy_ref`. + Overlap is deliberately excluded here -- see `guest_memcpy`'s docstring and + ORACLE.md O2. + """ + chunk = chunk or ref.chunk_ecalls + lengths = list(range(0, 1100)) if not quick else [0, 1, 255, MAX, 257, 512, 1000] + for n in lengths: + calls = chunk(0x2_0000, 0x1_0000, n) + if any(c > MAX for (_, _, c) in calls): + return False, f"n={n}: a chunk exceeds {MAX} bytes" + if len(calls) != (n + MAX - 1) // MAX: + return False, f"n={n}: {len(calls)} chunks, expected {(n + MAX - 1) // MAX}" + if sum(c for (_, _, c) in calls) != n: + return False, f"n={n}: chunks cover {sum(c for (_, _, c) in calls)} bytes" + + initial = _region(n, REGION) + composed = dict(initial) + for cdst, csrc, cn in calls: + composed = ref.memcpy_ref(composed, cdst, csrc, cn) + # The whole-length expectation cannot come from `memcpy_ref` -- that + # models ONE ecall and rejects n > MAX. Spell the copy out instead. + expected = dict(initial) + for i in range(n): + expected[0x2_0000 + i] = initial.get(0x1_0000 + i, 0) + if composed != expected: + return False, f"n={n}: chunked copy != a plain byte-by-byte copy" + + effect, returned = ref.guest_memcpy(initial, 0x2_0000, 0x1_0000, n) + if returned != 0x2_0000: + return False, f"n={n}: memcpy must return dst" + if effect != expected: + return False, f"n={n}: guest_memcpy disagrees with a plain copy" + return True, f"{len(lengths)} lengths, chunk count and composition both exact" + + +# --------------------------------------------------------------------------- +# Canonical vectors +# --------------------------------------------------------------------------- + +#: Hand-picked so every structural case is covered exactly once: empty, a lone +#: tail byte, a full wide row, wide+tail, the widest tail (7), an unaligned +#: unaligned-overlapping copy, both overlap directions, a page-crossing copy, +#: and the maximum chunk (which has no tail row at all). +CANONICAL_CASES = [ + ("empty", 0x1000, 0x2000, 0), + ("single byte", 0x1000, 0x2000, 1), + ("one wide row", 0x1000, 0x2000, 8), + ("wide plus tail", 0x1000, 0x2000, 9), + ("widest tail", 0x1000, 0x2000, 7), + ("unaligned body and tail", 0x2005, 0x1003, 27), + ("forward overlap", 0x3004, 0x3000, 24), + ("backward overlap", 0x3000, 0x3004, 24), + ("page crossing", 0x0FFC, 0x1FFC, 16), + ("maximum chunk", 0x1000, 0x2000, MAX), +] + + +def emit_vectors(): + """Write `canonical_dma_vectors.json`: the pinned cases with their full + row-and-column expansion, so the Rust side can be checked against this + model without re-deriving it.""" + vectors = [] + for name, dst, src, n in CANONICAL_CASES: + memory = {src + i: (i * 7 + 3) & 0xFF for i in range(n)} + rows = ref.row_decomposition(0x30, dst, src, n, memory) + vectors.append({ + "name": name, + "timestamp": 0x30, + "dst": dst, + "src": src, + "count": n, + "widths": ref.row_widths(n), + "data_rows": len(rows) - 1, + "rows": [ + { + "src": r.src, "dst": r.dst, "count": r.count, + "first": r.first, "end": r.end, "tail": r.tail, + "width": r.width, "value": r.value, + "columns": ref.row_columns(r), + } + for r in rows + ], + "memw": [ + { + "is_register": o.is_register, "address": o.address, + "timestamp": o.timestamp, "width": o.width, + "value": list(o.value), "is_write": o.is_write, + } + for o in ref.memw_ops(0x30, dst, src, n, memory) + ], + }) + with open(VECTORS, "w") as f: + json.dump(vectors, f, indent=1) + f.write("\n") + emit_row_table(vectors) + return vectors + + +def emit_row_table(vectors): + """Write `canonical_dma_rows.txt`: the same vectors, line-oriented. + + The JSON is the rich artifact — it carries the full per-row column expansion + the z3 gate pins. This file exists because the Rust side has no JSON parser + (the prover crate has no `serde_json`, and adding a dependency for a fixture + is not worth it), and a hand-rolled scanner over nested JSON is exactly the + kind of fragile coupling that goes stale silently: the first attempt broke on + the `columns` sub-object repeating the `src`/`dst`/`count` keys. + + One record per line, `|`-separated, so `include_str!` + `split('|')` is the + whole parser and a malformed line is a hard error: + + vector||||| + row||||| + """ + lines = [ + "# Generated by test_ref.py — do not edit by hand.", + "# Consumed by prover/src/tests/dma_tests.rs via include_str!.", + "# vector|name|dst|src|count|data_rows row|src|dst|count|tail|width", + ] + for vector in vectors: + data_rows = [r for r in vector["rows"] if not r["end"]] + lines.append("vector|{}|{}|{}|{}|{}".format( + vector["name"], vector["dst"], vector["src"], + vector["count"], len(data_rows))) + for row in data_rows: + lines.append("row|{}|{}|{}|{}|{}".format( + row["src"], row["dst"], row["count"], + 1 if row["tail"] else 0, row["width"])) + with open(ROW_TABLE, "w") as f: + f.write("\n".join(lines) + "\n") + + +# --------------------------------------------------------------------------- + +def _anchor_mutations(quick: bool): + """Delegates to `tamper_test.py`, imported late to avoid a circular import.""" + from tamper_test import anchor_mutations + return anchor_mutations(quick) + + +def main(): + quick = "--quick" in sys.argv + print("=" * 72) + print("DMA memcpy oracle -- validation harness" + (" (--quick)" if quick else "")) + print("=" * 72) + + anchors = [ + ("[1] libc memmove", anchor_libc), + ("[2] CPython slice assignment", anchor_slice_assign), + ("[3] row/bus level <-> byte level", anchor_row_level), + ("[4] guest stub chunking", anchor_chunking), + ("[5] tamper tests (tamper_test.py)", _anchor_mutations), + ] + results = {} + for name, run in anchors: + print(f"\n {name}") + ok, detail = run(quick) + results[name] = ok + label = {True: "PASS", False: "FAIL", None: "SKIP"}[ok] + print(f" {label} {detail}") + + print("\n" + "=" * 72) + ran = [n for n, ok in results.items() if ok is not None] + failed = [n for n, ok in results.items() if ok is False] + skipped = [n for n, ok in results.items() if ok is None] + if failed: + status = "NOT VALIDATED" + elif not ran: + status = "NOT VALIDATED" + elif skipped: + status = "PARTIALLY VALIDATED" + else: + status = "VALIDATED" + # The token itself carries any reduction. A CI job or a human greps for + # "VALIDATED", so a degraded or shortened run must not print the bare word. + qualifiers = [] + if skipped: + qualifiers.append(f"{len(skipped)} anchor(s) skipped") + if quick: + qualifiers.append("--quick, reduced sweeps") + suffix = f" ({'; '.join(qualifiers)})" if qualifiers else "" + print(f"VALIDATION STATUS: {status}{suffix}") + print(f" anchored on : {', '.join(n for n in ran if results[n]) or 'nothing'}") + if skipped: + print(f" NOT anchored on: {', '.join(skipped)}") + if failed: + print(f" FAILING : {', '.join(failed)}") + if quick: + print(" NOTE: --quick skipped the exhaustive 0..256 length sweeps.") + + if not failed: + vectors = emit_vectors() + print(f"\n emitted {len(vectors)} canonical vectors -> " + f"{os.path.basename(VECTORS)} + {os.path.basename(ROW_TABLE)}") + + print("=" * 72) + # Distinct exit codes: 0 full board, 1 a real failure, 2 ran but degraded. + # A skipped external anchor used to exit 0, indistinguishable from a clean run. + if failed: + sys.exit(1) + sys.exit(2 if skipped else 0) + + +if __name__ == "__main__": + main() diff --git a/formal_verification/dma/verify.log b/formal_verification/dma/verify.log new file mode 100644 index 000000000..f3d78817a --- /dev/null +++ b/formal_verification/dma/verify.log @@ -0,0 +1,70 @@ +============================================================================ +DMA memcpy chip -- z3 gate +============================================================================ + solver: z3 5.0.0 + legend: unsat = proved | sat = counterexample found | unknown = TIMED OUT (failure) + +=== LAYER 1: field-exact rows === + MAIN 0 row == oracle row -> unsat (want unsat) + MAIN 1 end <=> count == 0 -> unsat (want unsat) + MAIN 2 count wraps only on terminal row -> unsat (want unsat) + MAIN 2b one-byte row has zero lanes 1..7 -> unsat (want unsat) + MAIN 2c one ecall asks for <= 256 bytes -> unsat (want unsat) + MAIN 3 successor exact + well formed -> unsat (want unsat) + +=== LAYER 2: chain structure, DmaNext as a free bijection === + CHAIN 2 rows, any balanced structure -> unsat (want unsat) + CHAIN 3 rows, any balanced structure -> unsat (want unsat) + CHAIN 4 rows, any balanced structure -> unsat (want unsat) + CHAIN 5 rows, any balanced structure -> unsat (want unsat) + CHAIN-F 2 rows, field-exact -> unsat (want unsat) + CHAIN-F 3 rows, field-exact -> unsat (want unsat) + + -- Layer 2 controls -- + positive: 2-row premise set satisfiable -> sat (want sat) + positive: 3-row premise set satisfiable -> sat (want sat) + positive: 4-row premise set satisfiable -> sat (want sat) + positive: 2-row field-exact premise set -> sat (want sat) + negative: drop `count` from the tuple -> sat (want sat) + negative: drop `src` from the tuple -> sat (want sat) + negative: drop `dst` from the tuple -> sat (want sat) + +=== NEGATIVE CONTROLS -- drop one premise, expect a forgery === + drop_halfword_count_decr -> sat (want sat) + drop_halfword_src_incr -> sat (want sat) + drop_zero_end -> sat (want sat) + drop_lt_tail -> sat (want sat) + drop_no_overflow_src -> sat (want sat) + drop_tail_lane_zero -> sat (want sat) + drop_lt_bound -> sat (want sat) + drop_reg32 -> sat (want sat) + drop_halfword_dst_incr -> sat (want sat) + drop_no_overflow_dst -> sat (want sat) + +=== WIDTH AUDIT -- bound necessity at the boundary (field level) === + Zero sum identity, bounds present -> unsat (want unsat) + Zero sum identity, bounds DROPPED -> sat (want sat) + no-overflow, halfword bounds present -> unsat (want unsat) + no-overflow, halfword bounds DROPPED -> sat (want sat) + truncation at count=7, LT pin present -> unsat (want unsat) + truncation at count=7, LT pin DROPPED -> sat (want sat) + +=== POSITIVE CONTROLS -- oracle-pinned completeness sweep === + PASS 5153 honest rows + 257 padding rows over 257 lengths, all accepted + +============================================================================ +VERDICT +============================================================================ + layer 1 (row semantics) : True + layer 2 (chain structure) : True + layer 2 controls (pos + neg) : True + negative controls all SAT : True (10/10) + width audit (bound necessity) : True + completeness sweep SAT : True + + Scope: Layer 2 proves the tiling among groups with exactly ONE head + row. Two DMA calls are separated by the `ts` in both DmaNext tuples, + which `ChainRow` does not model -- see `check_chain`'s docstring and + the textual guard in audit_transcription.py. + + OVERALL: PASS diff --git a/formal_verification/dma/z3_verify.py b/formal_verification/dma/z3_verify.py new file mode 100644 index 000000000..c18bcdb96 --- /dev/null +++ b/formal_verification/dma/z3_verify.py @@ -0,0 +1,1070 @@ +""" +Formal (z3) assume-guarantee gate for the DMA memcpy chip (PR #874). + +Method (mirrors the keccak gate in `formal_verification/keccak/z3_verify.py` (PR #923)): + * every committed column of the table is a FREE variable; + * every eval constraint and every bus lookup becomes an equation over those + free variables; + * the row's OUTPUT is whatever the constraints force. We assert + `output != reference(input)` and ask z3 for a counterexample: + UNSAT -> for every constraint-satisfying assignment the row does what + the oracle says (correctly and tightly constrained); + SAT -> the constraints permit a wrong row (under-constrained). + +TWO LAYERS, and the split is deliberate. + + Layer 1 (field-exact, one or two rows). Every column is an element of + Goldilocks `p = 2^64 - 2^32 + 1`, every constraint is an equation mod p, and + each carry is extracted the way the templates extract it, + `carry = (lhs + rhs - sum) * 2^-32`. A bit-vector model CANNOT do this job: + the whole question here is whether a range check is missing, and in a bounded + BV model an unconstrained column is silently bounded, so the bug disappears. + Layer 1 proves the ROW ABSTRACTION -- `width = 8 - 7*tail`, `tail = count < 8`, + `end = (count == 0)`, `src_incr = src + width` without wrapping, + `count_decr = (count - width) mod 2^64` -- as INTEGER relations, out of the + field-level constraints alone. + + Layer 2 (many rows). Takes the row abstraction as given, adds the `DmaNext` + bus as a free BIJECTION between senders and receivers (not as an assumed + chain), and proves the only balanced structure is a single chain whose data + rows tile `[src, src + n)` exactly once with the oracle's widths. This is + where "a source row skipped forward", "the copy ended early" and "a disjoint + cycle of rows also balances the bus" get answered. Run at the integer level + for depth, and re-run field-exact at small depth so the abstraction step is + not taken on trust. + +MODELLED CONTRACTS. Every lookup is modelled by the CONSTRAINTS OF THE TABLE +THAT RECEIVES IT, not by its advertised contract -- an advertised contract is +exactly the kind of premise that turns out to be declared and never derived +(finding F1 of GATE-TRANSCRIPTION-AUDIT.md of PR #903 (branch feat/blake3-accelerator), which in the EC +campaign hid a working forgery): + + IsHalfword[h] h in [0, 2^16). Preprocessed, so the contract IS the + range. + Zero[v] -> is_zero `bitwise.rs`: the argument decomposes as + v = X + 256*Y + 65536*Z with X,Y bytes and Z in [0,16), + and the OUTPUT column is 1 iff X = Y = Z = 0. (X/Y/Z are + the table's own digit columns; the output is a separate + column, `cols::ZERO`. Do not reuse the name `z` for both, + as an earlier draft of this docstring did.) NOTE THE + DOMAIN -- the table only has rows for v < 2^20, so a send + outside it has no partner at all. + Alu[a,b,LT] -> o `lt.rs`'s own columns: a free `lhs_sub_rhs` of four + IsHalfword halves, two carries with booleanity, + `out = carry_1`, `lhs.hi = lhs[1] + 2^16*lhs[2]` with + both halves range-checked. NOT `o = (a < b)`. This is + what makes the `LHS_0` aliasing question below visible + at all: `lt.rs` range-checks `lhs[1]` and `lhs[2]` but + NOT the bare `LHS_0` word. + Memw(addr, ...) the base-address limbs are 32-bit (MEMW-ADDR32) + Memw register read the three argument registers' limbs are 32-bit and equal + the register file's value (REG-32) + +The last two are PREMISES THIS GATE DOES NOT PROVE. README.md +records where each is discharged. Their control coverage is asymmetric, and +saying so is the point: + + REG-32 (A2) IS load-bearing -- `drop_reg32` flips `check_row_budget` to sat, + because a bound lookup on a residue class caps only the residue. + MEMW-ADDR32 (A1) is INERT for every claim this board makes: dropping it leaves + MAIN 0/1/2/2b/2c/3, both chain layers and the sweep unchanged. It is + modelled because the AIR really does carry those sends, but nothing here + leans on it -- the limb-wise `DmaNext` link derives well-formedness from + the sender's IsHalfword checks instead. It therefore has NO negative + control, deliberately: a control that cannot fail is worse than none, and + an earlier version of this docstring claimed "every negative control shows + what breaks without them", which was false for exactly this premise. + +WHAT THE GATE CANNOT SEE (same disclaimer shape as the BLAKE3 gate): + * bus WIRING -- that the read tuple and the write tuple really reference the + same `value` columns, that the timestamp offsets really are +1 and +2, that + the multiplicities really are `mu - end` / `first` / `mu`. Those are textual + facts about `dma.rs`, checked by audit_transcription.py. + * the MEMW consistency argument, hence the snapshot semantics of an + overlapping copy. That is a timestamp-ordering property of the memory + table; the oracle's `write_before_read` mutant covers the model side. + * LogUp soundness. Bus balance is assumed to mean multiset equality. + * the multi-call case. Layer 2 proves the tiling among groups containing + exactly ONE head row; `ChainRow` carries no timestamp, and the `ts` in both + `DmaNext` tuples is what separates two ecalls' rows. + + python3 z3_verify.py # the full board + python3 z3_verify.py --quick # shorter completeness sweep and chains +""" + +import os +import sys + +from z3 import ( + And, Distinct, If, Implies, Int, IntVal, Not, Or, Solver, Sum, get_version, + get_version_string, sat, unknown, unsat, +) + +#: Solver version this board is known green on. NOT a hard pin -- the queries are +#: version-independent in meaning -- but older solvers are dramatically slower on +#: the field-exact chain (`CHAIN-F 2` measured 0.45 s on 5.0.0 vs 7.60 s on +#: 4.12.2, 17x), so they blow the per-query budgets and report `unknown`. +#: `unknown` is scored as FAILURE everywhere, never as success, so an old solver +#: gives a false alarm and never a false proof -- but the operator deserves to be +#: told which it is looking at. +VALIDATED_Z3 = (5, 0, 0) + +# --------------------------------------------------------------------------- +# Constants -- transcribed from the Rust; audit_transcription.py +# asserts each one against the source. +# --------------------------------------------------------------------------- + +P = 2**64 - 2**32 + 1 # Goldilocks +INV_2_32 = pow(2**32, -1, P) # `templates::INV_SHIFT_32` +B16, B32, B64 = 2**16, 2**32, 2**64 + +WIDE_WIDTH, TAIL_WIDTH = 8, 1 +MAX_BYTES = 256 # `DMA_MEMCPY_MAX_BYTES` +ZERO_SUM = 4 * 65535 # the constant in the Zero sender's linear term +ZERO_DOMAIN = 2**20 # bitwise ZERO covers x + 256y + 65536z, z < 16 + +assert INV_2_32 == 18446744065119617026, "INV_SHIFT_32 transcription is wrong" +assert ZERO_SUM < ZERO_DOMAIN, "the Zero send can leave the receiving table's domain" + + +class Premises: + """Which assume-guarantee premises are switched on. + + Every field names a lookup or range check that exists in `dma.rs`, or in a + table `dma.rs` sends to. Turning one off is a negative control: the gate + then reports the forgery that check is the sole obstacle to. + """ + + NAMES = ( + "halfword_src_incr", "halfword_dst_incr", "halfword_count_decr", + "memw_addr32", "reg32", "lt_tail", "lt_bound", "zero_end", + "no_overflow_src", "no_overflow_dst", "tail_lane_zero", + ) + + def __init__(self, **off): + for name in self.NAMES: + setattr(self, name, True) + for name, value in off.items(): + assert name in self.NAMES, f"unknown premise {name}" + setattr(self, name, value) + + +#: Default per-query solver budget. Never leave a query unbounded: an unlucky +#: solver version or platform then HANGS a CI job instead of failing it, and a +#: hang is far harder to diagnose than a timeout (measured: the whole board takes +#: ~96 s on z3 5.0.0 but ~1210 s on 4.12.2, where two queries blew their budgets). +DEFAULT_TIMEOUT_MS = 120_000 + +_EQ_COUNTER = [0] + + +def eq_mod(lhs, rhs, modulus): + """`lhs == rhs (mod modulus)` as a linear constraint with a witness quotient. + + See the ENCODING NOTE in `FieldRow`: this is exactly `(lhs - rhs) % m == 0`, + written so the query stays in linear integer arithmetic. + """ + _EQ_COUNTER[0] += 1 + k = Int(f"q{_EQ_COUNTER[0]}") + return lhs - rhs == k * modulus + + +def dmanext_link(sender, receiver): + """The `DmaNext` bus binding, ELEMENT BY ELEMENT. + + THIS IS THE FACT AN EARLIER VERSION OF THIS GATE GOT WRONG, and the error + produced a phantom soundness finding that was published as the campaign's + headline result. It is worth stating precisely. + + `Packing::num_bus_elements()` (`crypto/stark/src/lookup.rs:227-241`) returns + **2** for both `DWordWL` ("2x Direct") and `DWordHL` ("2x Word2L"), and + `accumulate_fingerprint_with` (`:305-340`) gives each element its own alpha + power. No `Packing` variant contains a `2^32` shift at all, so **a 64-bit + value is never a single bus element anywhere in this codebase.** + + Both DmaNext tuples are therefore 8 elements (`1+1+2+2+2`) and align + pairwise, so bus balance imposes TWO independent equations per 64-bit value: + + receiver.src0 == sender.si0 + 2^16*si1 (low word) + receiver.src1 == sender.si2 + 2^16*si3 (high word) + + Modelling it as one equation on the fully packed value is strictly WEAKER + than the AIR: it lets the receiver re-split the limbs freely, which + manufactures an alias (`cnt1 = 2^32-1`, `cnt0 = V+1`) that the real bus + rejects. Since the sender's halfwords are IsHalfword-bounded, the limb-wise + form gives the receiver 32-bit limbs *for free* — no extra range check + needed, which is why the "fix" that earlier version recommended (receive + `count` as `DWordHL`) was a no-op, and why a no-op fix should have been + read as evidence that the gap wasn't there. + """ + return [ + eq_mod(sender.ts0, receiver.ts0, P), + eq_mod(sender.ts1, receiver.ts1, P), + eq_mod(sender.hl_lo(sender.si), receiver.src0, P), + eq_mod(sender.hl_hi(sender.si), receiver.src1, P), + eq_mod(sender.hl_lo(sender.di), receiver.dst0, P), + eq_mod(sender.hl_hi(sender.di), receiver.dst1, P), + eq_mod(sender.hl_lo(sender.cd), receiver.cnt0, P), + eq_mod(sender.hl_hi(sender.cd), receiver.cnt1, P), + ] + + +def solve(assertions, timeout_ms=DEFAULT_TIMEOUT_MS): + s = Solver() + if timeout_ms: + s.set("timeout", timeout_ms) + for a in assertions: + s.add(a) + return s.check() + + +# =========================================================================== +# Layer 1 -- field-exact model of a row +# =========================================================================== + +class FieldRow: + """One DMA row, every column a free Goldilocks element. + + Column names track `dma::cols` exactly. Lookups are placed under their own + multiplicity: a lookup with multiplicity zero constrains NOTHING, and + asserting it anyway would make the model stronger than the AIR -- the + dangerous direction, since an over-strong model yields UNSAT where the real + object is forgeable. + """ + + def __init__(self, tag: str, prem: Premises): + self.tag, self.prem, self.n = tag, prem, 0 + self.C = [] + + self.ts0, self.ts1 = self.col("ts0"), self.col("ts1") + self.src0, self.src1 = self.col("src0"), self.col("src1") + self.si = [self.col(f"si{i}") for i in range(4)] + self.dst0, self.dst1 = self.col("dst0"), self.col("dst1") + self.di = [self.col(f"di{i}") for i in range(4)] + self.cnt0, self.cnt1 = self.col("cnt0"), self.col("cnt1") + self.cd = [self.col(f"cd{i}") for i in range(4)] + self.first = self.col("first") + self.end = self.col("end") + self.tail = self.col("tail") + self.value = [self.col(f"value{i}") for i in range(8)] + self.mu = self.col("mu") + + self._constraints() + self._lookups() + + # -- plumbing ---------------------------------------------------------- + # + # ENCODING NOTE. Two rewrites keep the model inside linear integer + # arithmetic, where z3 is fast. Both are exact, not approximations: + # + # `a == b (mod p)` becomes `a - b == k*p` for a fresh unbounded integer + # k. Identical semantics to `(a - b) % p == 0`, but linear in the + # columns (p is a constant), so no div/mod machinery is introduced. + # + # `x*(1 - x) == 0 (mod p)` becomes `x == 0 or x == 1`. Exact because p + # is prime and every column is already confined to [0, p): the + # product vanishes mod p only if one factor does, giving x = 0 or + # x = 1 in that interval. Keeping the literal quadratic instead makes + # every query nonlinear over a 64-bit prime, which is what the first + # version of this gate died of. + # + # Products of a BOOLEAN column with anything else are likewise rewritten as + # implications (`mu*(...)` -> `Implies(mu == 1, ...)`), which is exact once + # the column is known boolean. + + def col(self, name: str): + """A committed column: a free field element in [0, p).""" + v = Int(f"{self.tag}_{name}") + self.C.append(And(v >= 0, v < P)) + return v + + def aux(self, name: str): + """A virtual value (a carry, or another table's column). Also in [0,p).""" + self.n += 1 + v = Int(f"{self.tag}_{name}_{self.n}") + self.C.append(And(v >= 0, v < P)) + return v + + def feq(self, lhs, rhs): + """`lhs == rhs` in the field, as `lhs - rhs == k*p`.""" + self.n += 1 + k = Int(f"{self.tag}_k{self.n}") + self.C.append(lhs - rhs == k * P) + + def is_bit(self, x): + """`x*(1-x) = 0` for a column already in [0, p): x is 0 or 1.""" + self.C.append(Or(x == 0, x == 1)) + + def scoped(self, condition, body): + """Assert what `body` appends only where `condition` holds. + + Used for every bus lookup, so that a multiplicity-zero interaction + contributes nothing. + """ + mark = len(self.C) + body() + added, self.C[mark:] = self.C[mark:], [] + self.C.append(Implies(condition, And(*added))) + + # -- packings ---------------------------------------------------------- + def wl(self, lo, hi): + return lo + B32 * hi + + def hl_lo(self, h): + return h[0] + B16 * h[1] + + def hl_hi(self, h): + return h[2] + B16 * h[3] + + def hl(self, h): + return self.hl_lo(h) + B32 * self.hl_hi(h) + + @property + def step_lo(self): + """`step = 8 - 7*tail`, the `AddOperand::linear` in `DmaConstraints`.""" + return 8 - 7 * self.tail + + @property + def src(self): + return self.wl(self.src0, self.src1) + + @property + def dst(self): + return self.wl(self.dst0, self.dst1) + + @property + def count(self): + return self.wl(self.cnt0, self.cnt1) + + @property + def src_incr(self): + return self.hl(self.si) + + @property + def dst_incr(self): + return self.hl(self.di) + + @property + def count_decr(self): + return self.hl(self.cd) + + @property + def width(self): + return If(self.tail == 1, IntVal(TAIL_WIDTH), IntVal(WIDE_WIDTH)) + + # -- eval constraints -------------------------------------------------- + def _add_pair(self, lhs_lo, lhs_hi, rhs_lo, rhs_hi, sum_lo, sum_hi, + name, no_overflow): + """`templates::emit_add_pair[_no_overflow]`. + + `carry_0 = (lhs.lo + rhs.lo - sum.lo) * 2^-32` is always boolean. + `carry_1 = (lhs.hi + rhs.hi + carry_0 - sum.hi) * 2^-32` is boolean in + the plain form, and forced to ZERO on active non-terminal rows + (`mu - end == 1`) in the no-overflow form -- leaving it a free field + element on terminal and padding rows, whose successor is not consumed. + """ + c0 = self.aux(f"{name}_c0") + self.feq(lhs_lo + rhs_lo - sum_lo, c0 * B32) + self.is_bit(c0) + c1 = self.aux(f"{name}_c1") + self.feq(lhs_hi + rhs_hi + c0 - sum_hi, c1 * B32) + if no_overflow: + # `(mu - end) * carry_1 == 0`, with mu and end boolean. + self.C.append(Implies(self.mu - self.end == 1, c1 == 0)) + else: + self.is_bit(c1) + + def _constraints(self): + """`DmaConstraints::eval`, index by index.""" + for x in (self.first, self.end, self.tail, self.mu): # idx 0-3 + self.is_bit(x) + # idx 4: `(first + end)*(1 - mu) == 0` -- an inactive row cannot claim + # first or end. With all three boolean this is exactly: + self.C.append(Implies(self.mu == 0, And(self.first == 0, self.end == 0))) + # idx 5-6, 7-8: src and dst advance by `step` without wrapping 2^64 + self._add_pair(self.src0, self.src1, self.step_lo, 0, + self.hl_lo(self.si), self.hl_hi(self.si), "src", + self.prem.no_overflow_src) + self._add_pair(self.dst0, self.dst1, self.step_lo, 0, + self.hl_lo(self.di), self.hl_hi(self.di), "dst", + self.prem.no_overflow_dst) + # idx 9-10: count_decr + step = count. The PLAIN pair, so it MAY wrap -- + # which is what lets the terminal row hold `0 - 1`. + self._add_pair(self.hl_lo(self.cd), self.hl_hi(self.cd), self.step_lo, 0, + self.cnt0, self.cnt1, "cnt", False) + # idx 11-17: `tail * value[i] == 0` -- unused lanes are zero on a + # one-byte row (`tail` boolean, so the product form is this): + if self.prem.tail_lane_zero: + for lane in self.value[1:]: + self.C.append(Implies(self.tail == 1, lane == 0)) + + # -- lookups ----------------------------------------------------------- + def _lt(self, lhs_lo, lhs_hi, rhs_lo, name): + """`Alu[lhs, rhs, LT] -> out`, as `lt.rs`'s own constraints. + + `lhs`/`rhs` cross the bus as DWordHHW -> [lo32, hi32]. The hi limb is + `LHS_1 + 2^16*LHS_2` with both halves range-checked (IsHalfword on + `[1]`, MSB16 -- whose argument is a halfword -- on `[2]`), so the hi + limb is genuinely 32-bit. `LHS_0` is a bare `Word` column, pinned only + through the carry relation; keeping that faithful is the whole point of + modelling the table instead of its contract. + """ + sub = [self.aux(f"{name}_sub{i}") for i in range(4)] + for h in sub: + self.C.append(h < B16) # IsHalfword[sub[i]] + h1, h2 = self.aux(f"{name}_h1"), self.aux(f"{name}_h2") + self.C.append(h1 < B16) # IsHalfword[lhs[1]] + self.C.append(h2 < B16) # MSB16[lhs[2]] + self.feq(lhs_hi, h1 + B16 * h2) + + sub_lo, sub_hi = sub[0] + B16 * sub[1], sub[2] + B16 * sub[3] + c0 = self.aux(f"{name}_c0") + self.feq(rhs_lo + sub_lo - lhs_lo, c0 * B32) + self.is_bit(c0) + c1 = self.aux(f"{name}_c1") + self.feq(0 + sub_hi + c0 - lhs_hi, c1 * B32) + self.is_bit(c1) + return c1 # unsigned lt == carry_1 + + def _zero(self, arg, out): + """`Zero[arg] -> out`, as the receiving `bitwise.rs` row. + + `arg` must decompose as `x + 256y + 65536z` with x,y bytes and z in + [0,16), i.e. `arg` must lie IN THE TABLE'S DOMAIN [0, 2^20). An `arg` + outside it has no partner row, which is a completeness failure rather + than a soundness hole -- but it means the halfword bounds on + `count_decr` are doing two jobs at once, and the width audit separates + them. + """ + x, y, z = self.aux("zx"), self.aux("zy"), self.aux("zz") + self.C.append(x < 256) + self.C.append(y < 256) + self.C.append(z < 16) + self.feq(arg, x + 256 * y + 65536 * z) + self.feq(out, If(And(x == 0, y == 0, z == 0), IntVal(1), IntVal(0))) + + def _lookups(self): + p, active = self.prem, self.mu == 1 + # IsHalfword senders, multiplicity mu. + for columns, present in ((self.cd, p.halfword_count_decr), + (self.si, p.halfword_src_incr), + (self.di, p.halfword_dst_incr)): + if present: + for h in columns: + self.C.append(Implies(active, h < B16)) + # MEMW data ops, multiplicity mu - end: bind the base-address limbs. + if p.memw_addr32: + for limb in (self.src0, self.src1, self.dst0, self.dst1): + self.C.append(Implies(self.mu - self.end == 1, limb < B32)) + # MEMW register reads, multiplicity first: bind all three arguments. + if p.reg32: + for limb in (self.src0, self.src1, self.dst0, self.dst1, + self.cnt0, self.cnt1): + self.C.append(Implies(self.first == 1, limb < B32)) + # Bus 16: end detection. + if p.zero_end: + self.scoped(active, lambda: self._zero(ZERO_SUM - Sum(self.cd), self.end)) + # Bus 20: tail = (count < 8). + if p.lt_tail: + self.scoped(active, lambda: self.feq( + self.tail, self._lt(self.cnt0, self.cnt1, IntVal(WIDE_WIDTH), "lt_tail"))) + # Bus 21: the first row proves count < MAX + 1. + if p.lt_bound: + self.scoped(self.first == 1, lambda: self.feq( + 1, self._lt(self.cnt0, self.cnt1, IntVal(MAX_BYTES + 1), "lt_bound"))) + + # -- the reference and the invariant ----------------------------------- + def reference(self): + """What an active row must do, from `dma_ref.row_columns`. + + Stated over the INTEGERS, which is only meaningful where the limbs are + genuine 32-bit words -- `well_formed()` is that hypothesis, and + `check_invariant_propagates` is what shows it holds chain-wide. + + NOTE the `count_decr` clause is spelled as an explicit two-way + disjunction rather than through `eq_mod`. This predicate is asserted + NEGATED, and a modular equality carrying a free witness quotient becomes + vacuously satisfiable under negation (pick a nonzero quotient) -- which + is exactly how the first run of this gate reported a bogus SAT. Both + representatives are in range here (`count_decr` is a bounded dword and + `count - width` lies in `[-8, 2^64)`), so the disjunction is exact and + witness-free. + """ + return And( + self.tail == If(self.count < WIDE_WIDTH, IntVal(1), IntVal(0)), + self.end == If(self.count == 0, IntVal(1), IntVal(0)), + Or(self.count_decr == self.count - self.width, + self.count_decr == self.count - self.width + B64), + Implies(self.end == 0, + And(self.src_incr == self.src + self.width, + self.src + self.width < B64, + self.dst_incr == self.dst + self.width, + self.dst + self.width < B64)), + ) + + def well_formed(self): + """The limbs are genuine 32-bit words. + + Supplied on the head row by REG-32 and on every data row by + MEMW-ADDR32 (addresses only); for `count` on a non-head row it is a + CONCLUSION, not a hypothesis -- see `check_invariant_propagates`. + """ + return And(*[x < B32 for x in + (self.src0, self.src1, self.dst0, self.dst1, + self.cnt0, self.cnt1)]) + + +# --------------------------------------------------------------------------- +# Layer 1 checks +# --------------------------------------------------------------------------- + +def check_row(prem=None, timeout_ms=180_000): + """MAIN 0 -- an active, well-formed row does exactly what the oracle says.""" + prem = prem or Premises() + r = FieldRow("row", prem) + return solve(r.C + [r.mu == 1, r.well_formed(), Not(r.reference())], timeout_ms) + + +def check_end_detection(prem=None, timeout_ms=180_000): + """MAIN 1 -- `end` fires if and only if `count == 0`. + + Split out from MAIN 0 because it is the single thing standing between the + table and a silently truncated copy: an `end` row's memory sends have + multiplicity `mu - end = 0`, so a row that wrongly claims `end` emits no + reads and no writes at all, and every bus still balances. + """ + prem = prem or Premises() + r = FieldRow("endr", prem) + wrong = Or(And(r.end == 1, r.count != 0), And(r.end == 0, r.count == 0)) + return solve(r.C + [r.mu == 1, r.well_formed(), wrong], timeout_ms) + + +def check_wrap_only_terminal(prem=None, timeout_ms=180_000): + """MAIN 2 -- the `count` subtraction wraps only on the terminal row. + + The lemma the chain argument rests on. `count_decr` uses the PLAIN add pair, + so `count - width` is allowed to wrap modulo 2^64; if it could wrap on a row + that still sends to `DmaNext`, `count` would stop being strictly decreasing + along the chain and a cycle of rows that balances the bus while copying + nothing (or copying twice) becomes thinkable. UNSAT says a wrapping row + always has `end = 1`, and an `end` row sends nothing. + """ + prem = prem or Premises() + r = FieldRow("wrap", prem) + return solve(r.C + [r.mu == 1, r.well_formed(), + r.count < r.width, r.end == 0], timeout_ms) + + +def check_tail_lanes(prem=None, timeout_ms=180_000): + """MAIN 2b -- a one-byte row carries seven zero lanes. + + LABELLED HONESTLY: this is a TRANSCRIPTION check, not a composed solver + result. It is UNSAT from `Implies(tail == 1, lane == 0)` alone, with no other + AIR fact participating, and its negative control is `sat` for the same + trivial reason. Kept because the property matters and the pair documents it, + but it earns no credit as evidence about the constraint system -- the textual + equivalent in `audit_transcription.py` is the real guard. + + `value[1..8]` ride the MEMW tuple of a `w8 = 1 - tail` operation, so on a + tail row the memory table must see the canonical one-byte encoding. Nothing + else pins those lanes: they are not XOR-consumed and not range-checked, so + without constraints 11-17 they are free field elements appearing in a bus + tuple -- the aliasing shape `keccak.rs` documents for its address bytes. + """ + prem = prem or Premises() + r = FieldRow("lanes", prem) + return solve(r.C + [r.mu == 1, r.tail == 1, + Or(*[lane != 0 for lane in r.value[1:]])], timeout_ms) + + +def check_row_budget(prem=None, timeout_ms=180_000): + """MAIN 2c -- one ecall cannot ask for more than MAX_BYTES bytes. + + This is the bound that keeps a single guest instruction from adding an + unbounded number of rows to a continuation epoch, and it is the only claim + in the table that needs BOTH the first-row LT lookup (bus 21) and REG-32: + the lookup caps the packed count, and REG-32 is what makes the packed count + a genuine 64-bit integer rather than one representative of a residue class. + Deliberately does NOT assume `well_formed()` -- that would hand REG-32 to + the query for free and make its control vacuous. + """ + prem = prem or Premises() + r = FieldRow("budget", prem) + return solve(r.C + [r.mu == 1, r.first == 1, r.count > MAX_BYTES], timeout_ms) + + +def check_invariant_propagates(prem=None, timeout_ms=600_000): + """MAIN 3 -- well-formedness and the exact count cross a `DmaNext` hop. + + `DmaNext` binds each 64-bit value as TWO 32-bit elements, not one packed + field element (see `dmanext_link`, which documents the error an earlier + version of this gate made here). So the successor cannot re-split its limbs: + with the sender's halfwords IsHalfword-bounded, the receiver's `count0` and + `count1` are each pinned to a genuine 32-bit word. + + The claim is therefore unconditional -- no disjunctive escape branch: + + successor.count == predecessor.count - width AND successor well formed + + Proving it once on the head row (where the register read supplies + well-formedness) proves it for the whole chain, which is what licenses + Layer 2's integer abstraction. + """ + prem = prem or Premises() + a, b = FieldRow("inv_a", prem), FieldRow("inv_b", prem) + link = [ + a.mu == 1, a.end == 0, a.well_formed(), a.count <= MAX_BYTES, + b.mu == 1, b.first == 0, + ] + dmanext_link(a, b) + holds = And(b.count == a.count - a.width, b.well_formed()) + return solve(a.C + b.C + link + [Not(holds)], timeout_ms) + + +def completeness_sweep(prem=None, quick=False): + """MAIN 4 -- every honest trace is accepted (no false rejection). + + For each length the ORACLE pins every column of every row (plus the padding + row the generator emits) and asks whether the constraint system is + satisfiable. A failure is a completeness bug: the AIR would reject a copy + the executor performs. This is also the gate's non-vacuity check -- if the + constraint set were contradictory, every UNSAT above would be worthless. + """ + sys.path.insert(0, os.path.dirname(os.path.abspath(__file__))) + import dma_ref as ref + + prem = prem or Premises() + lengths = list(range(0, MAX_BYTES + 1)) if not quick else [0, 1, 7, 8, 9, 16, 27, 255, 256] + checked = 0 + for n in lengths: + memory = {0x2000 + i: (i * 7 + 3) & 0xFF for i in range(n)} + rows = ref.row_decomposition(0x30, 0x1000, 0x2000, n, memory) + for index, row in enumerate(rows): + r = FieldRow(f"cs{n}_{index}", prem) + verdict = solve(r.C + _pins(r, ref.row_columns(row))) + # `unknown` is a TIMEOUT, not a rejection. Scoring `!= sat` would print + # "the AIR REJECTS an honest row" for a slow solver -- a false + # accusation against the chip, and exactly the confusion the board's + # legend exists to prevent. Distinguish the two. + if verdict == unknown: + return None, (f"n={n} row {index}: solver TIMED OUT " + f"(not a rejection -- raise the budget or use a newer z3)") + if verdict != sat: + return False, f"n={n} row {index}: the AIR REJECTS an honest row" + checked += 1 + r = FieldRow(f"pad{n}", prem) + verdict = solve(r.C + _pins(r, ref.padding_columns())) + if verdict == unknown: + return None, f"n={n}: solver TIMED OUT on the padding row (not a rejection)" + if verdict != sat: + return False, f"n={n}: the AIR REJECTS the padding row" + checked += 1 + return True, (f"{checked - len(lengths)} honest rows + {len(lengths)} padding rows " + f"over {len(lengths)} lengths, all accepted") + + +def _pins(r: FieldRow, cols: dict): + pins = [ + r.ts0 == cols["timestamp"][0], r.ts1 == cols["timestamp"][1], + r.src0 == cols["src"][0], r.src1 == cols["src"][1], + r.dst0 == cols["dst"][0], r.dst1 == cols["dst"][1], + r.cnt0 == cols["count"][0], r.cnt1 == cols["count"][1], + r.first == cols["first"], r.end == cols["end"], + r.tail == cols["tail"], r.mu == cols["mu"], + ] + pins += [r.si[i] == cols["src_incr"][i] for i in range(4)] + pins += [r.di[i] == cols["dst_incr"][i] for i in range(4)] + pins += [r.cd[i] == cols["count_decr"][i] for i in range(4)] + pins += [r.value[i] == cols["value"][i] for i in range(8)] + return pins + + +# =========================================================================== +# Layer 2 -- the chain, with DmaNext as a free bijection +# =========================================================================== + +class ChainRow: + """One row, abstracted to the integer relations Layer 1 proved. + + Using the abstraction instead of re-deriving the field model keeps the + multi-row query tractable. The composition is valid because MAIN 0/1/2/3 + establish exactly these relations on every reachable row (with R1 as the + stated residual). + """ + + def __init__(self, tag): + self.src, self.dst = Int(f"{tag}_src"), Int(f"{tag}_dst") + self.count, self.first = Int(f"{tag}_count"), Int(f"{tag}_first") + self.C = [ + And(self.src >= 0, self.src < B64), + And(self.dst >= 0, self.dst < B64), + And(self.count >= 0, self.count < B64), + Or(self.first == 0, self.first == 1), + ] + + @property + def width(self): + return If(self.count < WIDE_WIDTH, IntVal(TAIL_WIDTH), IntVal(WIDE_WIDTH)) + + @property + def end(self): + return If(self.count == 0, IntVal(1), IntVal(0)) + + @property + def src_incr(self): + return self.src + self.width + + @property + def dst_incr(self): + return self.dst + self.width + + @property + def count_decr(self): + return self.count - self.width + + def no_overflow(self): + return Implies(self.end == 0, + And(self.src_incr < B64, self.dst_incr < B64)) + + +def check_chain(n_rows, prem=None, timeout_ms=300_000, premises_only=False, + drop_link=None): + """CHAIN -- the only bus-balanced structure is the oracle's decomposition. + + `n_rows` active rows. `DmaNext` is NOT assumed to be a chain: every row with + `end = 0` sends one tuple, every row with `first = 0` receives one, and bus + balance means a BIJECTION between those sets -- modelled as a free injective + index map plus tuple equality. A cycle, a fork, a skipped source row or a + duplicated one would be just as balanced a priori. The Ecall bus supplies + "exactly one row may be `first`" (the CPU sends its tuple once). + + SCOPE, stated precisely: the `Ecall` bus supplies at most one `first` row + **per timestamp**, not one per trace -- a real trace with k DMA calls has k + head rows. `ChainRow` carries no timestamp field, so this check cannot + express the property that separates two calls' rows (the `ts` in both + DmaNext tuples, which `audit_transcription.py` pins textually). + What is proved is therefore: *among a group of active rows containing + exactly one head row*, the only bus-balanced structure is the reference + tiling. Dropping the single-head premise makes this `sat`, so the + multi-call case is genuinely out of model rather than covered. + + The tiling predicate asserts four facts: data-row widths summing to the head + count, every data interval inside `[src, src + count)`, the intervals + pairwise disjoint, and `dst - src` constant. Together they say the copy moves + byte `j` of the source to byte `j` of the destination, for every + `j < count`, exactly once. (The greedy width rule is not concluded here -- + it is baked into `ChainRow.width` as a definition, discharged by MAIN 0.) + """ + prem = prem or Premises() + rows = [ChainRow(f"c{n_rows}_{i}") for i in range(n_rows)] + C = [c for r in rows for c in r.C] + if prem.no_overflow_src: + C += [r.no_overflow() for r in rows] + + # Ecall bus: exactly one head. + C.append(Sum([r.first for r in rows]) == 1) + # DmaNext balance: #senders == #receivers. + senders = [If(r.end == 0, IntVal(1), IntVal(0)) for r in rows] + C.append(Sum(senders) == Sum([1 - r.first for r in rows])) + + # sigma[j] = the sender matched to receiver j; a distinct negative sentinel + # for the head so `Distinct` still expresses injectivity over receivers. + sigma = [Int(f"s{n_rows}_{j}") for j in range(n_rows)] + for j, row in enumerate(rows): + C.append(Implies(row.first == 1, sigma[j] == -1 - j)) + C.append(Implies(row.first == 0, And(sigma[j] >= 0, sigma[j] < n_rows))) + for k, sender in enumerate(rows): + # `drop_link` omits one field of the DmaNext tuple -- the Layer 2 + # negative control, showing the bijection's contents are what force + # the tiling and not the bijection's mere existence. + tuple_eqs = [sender.end == 0] + if drop_link != "src": + tuple_eqs.append(sender.src_incr == row.src) + if drop_link != "dst": + tuple_eqs.append(sender.dst_incr == row.dst) + if drop_link != "count": + tuple_eqs.append(sender.count_decr == row.count) + C.append(Implies(And(row.first == 0, sigma[j] == k), And(*tuple_eqs))) + C.append(Distinct(*sigma)) + + head_count = Sum([If(r.first == 1, r.count, IntVal(0)) for r in rows]) + head_src = Sum([If(r.first == 1, r.src, IntVal(0)) for r in rows]) + head_skew = Sum([If(r.first == 1, r.dst - r.src, IntVal(0)) for r in rows]) + if prem.lt_bound: + C.append(head_count <= MAX_BYTES) + + if premises_only: + return solve(C, timeout_ms) + + data = lambda r: r.end == 0 # noqa: E731 + tiling = And( + Sum([If(data(r), r.width, IntVal(0)) for r in rows]) == head_count, + And(*[Implies(data(r), And(r.src >= head_src, + r.src + r.width <= head_src + head_count)) + for r in rows]), + And(*[Implies(And(data(rows[i]), data(rows[j])), + Or(rows[i].src + rows[i].width <= rows[j].src, + rows[j].src + rows[j].width <= rows[i].src)) + for i in range(n_rows) for j in range(i + 1, n_rows)]), + And(*[Implies(data(r), r.dst - r.src == head_skew) for r in rows]), + ) + return solve(C + [Not(tiling)], timeout_ms) + + +def check_chain_field(n_rows, prem=None, timeout_ms=900_000, premises_only=False): + """CHAIN-F -- the same question, field-exact, at small depth. + + The integer chain takes the row abstraction on trust. This one does not: it + builds `n_rows` full `FieldRow`s, links them with the field-level `DmaNext` + bijection, anchors the head with REG-32 plus the bound lookup, and asks for + any group whose copied byte total differs from the head count. Small `n` + only -- these queries are nonlinear over a 64-bit prime and get expensive + fast -- but it means the abstraction step is confirmed rather than assumed. + """ + prem = prem or Premises() + rows = [FieldRow(f"f{n_rows}_{i}", prem) for i in range(n_rows)] + C = [c for r in rows for c in r.C] + C += [r.mu == 1 for r in rows] + C.append(Sum([r.first for r in rows]) == 1) + C.append(Sum([If(r.end == 0, IntVal(1), IntVal(0)) for r in rows]) + == Sum([1 - r.first for r in rows])) + C.append(Sum([r.end for r in rows]) == 1) + + sigma = [Int(f"fs{n_rows}_{j}") for j in range(n_rows)] + for j, row in enumerate(rows): + C.append(Implies(row.first == 1, sigma[j] == -1 - j)) + C.append(Implies(row.first == 0, And(sigma[j] >= 0, sigma[j] < n_rows))) + for k, sender in enumerate(rows): + C.append(Implies(And(row.first == 0, sigma[j] == k), + And(*([sender.end == 0] + dmanext_link(sender, row))))) + C.append(Distinct(*sigma)) + # Head anchor, and NOTHING MORE. Only the head row gets well-formedness (the + # register read) and a count bound (the `Alu` lookup at multiplicity + # `first`); every other row's limbs and count are *derived* through the + # limb-wise link, per MAIN 3. An earlier version asserted + # `r.count <= MAX_BYTES` for EVERY row in order to sidestep a phantom + # residual -- which was the one genuinely over-strong assertion in this gate, + # and over-strong assertions are the direction that yields a bogus UNSAT. + for r in rows: + C.append(Implies(r.first == 1, r.well_formed())) + + head_count = Sum([If(r.first == 1, r.count, IntVal(0)) for r in rows]) + covered = Sum([If(r.end == 0, r.width, IntVal(0)) for r in rows]) + if premises_only: + # Positive control: is the premise set satisfiable at all? `Not(tiling)` + # returning UNSAT is worthless if `C` is itself contradictory. + return solve(C, timeout_ms) + return solve(C + [covered != head_count], timeout_ms) + + +# =========================================================================== +# Width audit -- field-level bound necessity at the concrete boundary +# =========================================================================== + +def audit_end_detection_bound(drop_bound: bool): + """Is `sum(count_decr) == 4*65535 <=> count_decr == 0xFFFF_FFFF_FFFF_FFFF`? + + The Zero send collapses four halfwords into ONE sum. With the IsHalfword + bounds the only way to reach `4*65535` is all four at `0xFFFF`. Drop them + and `(0xFFFF+d, 0xFFFF-d, 0xFFFF, 0xFFFF)` hits the same sum with a totally + different `count_decr`, so `end` can be claimed at a nonzero count -- and an + `end` row emits no memory operations. 'unsat' means the identity holds. + """ + s = Solver() + s.set("timeout", DEFAULT_TIMEOUT_MS) # never leave a query unbounded (see above) + cd = [Int(f"ae_cd{i}") for i in range(4)] + for h in cd: + s.add(h >= 0, h < P) + if not drop_bound: + s.add(h < B16) + s.add(eq_mod(Sum(cd), ZERO_SUM, P)) + # The forged quantity is compared through its RESIDUE, not through a negated + # modular equality: negating an equality that carries a free witness + # quotient is vacuous (see `FieldRow.reference`). + residue = Int("ae_res") + s.add(residue >= 0, residue < P) + s.add(eq_mod(cd[0] + B16 * cd[1] + B32 * cd[2] + B32 * B16 * cd[3], residue, P)) + s.add(residue != (B64 - 1) % P) + return str(s.check()) + + +def audit_no_overflow_bound(drop_bound: bool): + """Does `carry_1 == 0` really mean `src + width < 2^64`? + + `carry_1 = (src1 + carry_0 - src_incr.hi) * 2^-32`, so `carry_1 == 0` says + `src_incr.hi == src1 + carry_0` -- and at `src1 = 2^32 - 1` with a carry + that is exactly `2^32`, which the IsHalfword pair forbids and an unbounded + pair does not. The row then hands on a WRAPPED address that the executor's + `checked_add` would have rejected. 'unsat' means the bound pins it. + """ + s = Solver() + s.set("timeout", DEFAULT_TIMEOUT_MS) # never leave a query unbounded (see above) + src0, src1, c0 = Int("an_src0"), Int("an_src1"), Int("an_c0") + si = [Int(f"an_si{i}") for i in range(4)] + step = WIDE_WIDTH + s.add(src0 >= 0, src0 < B32, src1 >= 0, src1 < B32) + for h in si: + s.add(h >= 0, h < P) + if not drop_bound: + s.add(h < B16) + s.add(Or(c0 == 0, c0 == 1)) + s.add(eq_mod(src0 + step - (si[0] + B16 * si[1]), c0 * B32, P)) + s.add(eq_mod(src1 + c0, si[2] + B16 * si[3], P)) # carry_1 == 0 + s.add(src0 + B32 * src1 + step >= B64) # the range DOES wrap + return str(s.check()) + + +def audit_tail_pin(drop_pin: bool): + """Is the LT lookup the only thing stopping a SEVEN-byte truncation? + + `end` is claimed via the Zero check, which needs `count_decr` to be + all-`0xFFFF`, i.e. `count == step - 1`. With `tail` free a row may take + `tail = 0`, hence `step = 8`, hence `count == 7` satisfies it -- and an + `end` row emits NO memory operations at all, because both its MEMW sends + have multiplicity `mu - end`. Seven requested bytes are silently not copied + while every bus balances. + + The count is 7 and not some smaller number for a reason worth recording: + the two constraints compose, so `count = step - 1` is the ONLY reachable + forgery here, and `step` in {1, 8} makes 7 the only value a free `tail` buys. + 'unsat' means the LT pin blocks it. + """ + r = FieldRow("tp" + ("_drop" if drop_pin else ""), + Premises(lt_tail=not drop_pin)) + return str(solve(r.C + [r.mu == 1, r.well_formed(), r.count == 7, r.end == 1])) + + +# =========================================================================== + +def check_solver_version(): + """Warn loudly if the solver is older than the one this board was green on.""" + current = get_version()[:3] + if current < VALIDATED_Z3: + print(f" !! z3 {get_version_string()} is older than the validated " + f"{'.'.join(map(str, VALIDATED_Z3))}.", flush=True) + print(" !! The queries mean the same thing, but older solvers are much " + "slower on the", flush=True) + print(" !! field-exact chain and may report `unknown` (= TIMED OUT, " + "scored as failure).", flush=True) + print(" !! An `unknown` is a budget problem, NOT a soundness problem.", + flush=True) + return False + return True + + +def main(): + quick = "--quick" in sys.argv + print("=" * 76, flush=True) + print("DMA memcpy chip -- z3 gate" + (" (--quick)" if quick else ""), flush=True) + print("=" * 76, flush=True) + print(f" solver: z3 {get_version_string()}", flush=True) + check_solver_version() + print(" legend: unsat = proved | sat = counterexample found | " + "unknown = TIMED OUT (failure)", flush=True) + + print("\n=== LAYER 1: field-exact rows ===", flush=True) + row = check_row() + print(f" MAIN 0 row == oracle row -> {row} (want unsat)", flush=True) + endd = check_end_detection() + print(f" MAIN 1 end <=> count == 0 -> {endd} (want unsat)", flush=True) + wrap = check_wrap_only_terminal() + print(f" MAIN 2 count wraps only on terminal row -> {wrap} (want unsat)", flush=True) + lanes = check_tail_lanes() + print(f" MAIN 2b one-byte row has zero lanes 1..7 -> {lanes} (want unsat)", flush=True) + budget = check_row_budget() + print(f" MAIN 2c one ecall asks for <= {MAX_BYTES} bytes -> {budget} (want unsat)", flush=True) + inv = check_invariant_propagates() + print(f" MAIN 3 successor exact + well formed -> {inv} (want unsat)", flush=True) + layer1_ok = all(x == unsat for x in (row, endd, wrap, lanes, budget, inv)) + + print("\n=== LAYER 2: chain structure, DmaNext as a free bijection ===", flush=True) + chain = {} + for n_rows in ((2, 3, 4) if quick else (2, 3, 4, 5)): + chain[n_rows] = check_chain(n_rows) + print(f" CHAIN {n_rows} rows, any balanced structure -> {chain[n_rows]} (want unsat)", flush=True) + field_chain = {} + for n_rows in ((2,) if quick else (2, 3)): + field_chain[n_rows] = check_chain_field(n_rows) + print(f" CHAIN-F {n_rows} rows, field-exact -> {field_chain[n_rows]} (want unsat)", flush=True) + layer2_ok = all(x == unsat for x in list(chain.values()) + list(field_chain.values())) + + # Layer 2 needs its own controls. `Not(tiling)` returning unsat proves + # nothing if the premise set is itself unsatisfiable, and an earlier version + # of this board had neither a positive nor a negative control here. + print("\n -- Layer 2 controls --", flush=True) + l2_pos = {n: check_chain(n, premises_only=True) for n in (2, 3, 4)} + l2_posf = check_chain_field(2, premises_only=True) + for n, res in l2_pos.items(): + print(f" positive: {n}-row premise set satisfiable -> {res} (want sat)", flush=True) + print(f" positive: 2-row field-exact premise set -> {l2_posf} (want sat)", flush=True) + l2_neg = {f: check_chain(3, drop_link=f) for f in ("count", "src", "dst")} + for field, res in l2_neg.items(): + print(f" negative: drop `{field}` from the tuple{'':<7}-> {res} (want sat)", flush=True) + layer2_controls_ok = (all(r == sat for r in l2_pos.values()) and l2_posf == sat + and all(r == sat for r in l2_neg.values())) + + print("\n=== NEGATIVE CONTROLS -- drop one premise, expect a forgery ===", flush=True) + # Each control drops ONE premise and re-runs the check that premise is + # load-bearing for. Pairing matters: dropping `tail_lane_zero` and re-running + # MAIN 0 would report unsat, because MAIN 0's reference says nothing about + # the value lanes -- a control that cannot fail is not a control. + controls = { + "drop_halfword_count_decr": check_row(Premises(halfword_count_decr=False)), + "drop_halfword_src_incr": check_row(Premises(halfword_src_incr=False)), + "drop_zero_end": check_end_detection(Premises(zero_end=False)), + "drop_lt_tail": check_row(Premises(lt_tail=False)), + "drop_no_overflow_src": check_row(Premises(no_overflow_src=False)), + "drop_tail_lane_zero": check_tail_lanes(Premises(tail_lane_zero=False)), + "drop_lt_bound": check_row_budget(Premises(lt_bound=False)), + "drop_reg32": check_row_budget(Premises(reg32=False)), + # Previously undropped premises. `halfword_dst_incr` and `no_overflow_dst` + # are the dst-side mirrors of checks only ever demonstrated on src, and + # `DESIGN.md`'s "all twelve halfwords, each one" needs all three families. + "drop_halfword_dst_incr": check_row(Premises(halfword_dst_incr=False)), + "drop_no_overflow_dst": check_row(Premises(no_overflow_dst=False)), + } + for name, res in controls.items(): + print(f" {name:28s} -> {res} (want sat)", flush=True) + controls_ok = all(res == sat for res in controls.values()) + + print("\n=== WIDTH AUDIT -- bound necessity at the boundary (field level) ===", flush=True) + audit = { + "Zero sum identity, bounds present": (audit_end_detection_bound(False), "unsat"), + "Zero sum identity, bounds DROPPED": (audit_end_detection_bound(True), "sat"), + "no-overflow, halfword bounds present": (audit_no_overflow_bound(False), "unsat"), + "no-overflow, halfword bounds DROPPED": (audit_no_overflow_bound(True), "sat"), + "truncation at count=7, LT pin present": (audit_tail_pin(False), "unsat"), + "truncation at count=7, LT pin DROPPED": (audit_tail_pin(True), "sat"), + } + for name, (got, want) in audit.items(): + print(f" {name:40s} -> {got:6s} (want {want})", flush=True) + audit_ok = all(got == want for got, want in audit.values()) + + print("\n=== POSITIVE CONTROLS -- oracle-pinned completeness sweep ===", flush=True) + sweep_ok, sweep_detail = completeness_sweep(quick=quick) + label = {True: "PASS", False: "FAIL", None: "TIMEOUT"}[sweep_ok] + print(f" {label} {sweep_detail}", flush=True) + + print("\n" + "=" * 76, flush=True) + print("VERDICT", flush=True) + print("=" * 76, flush=True) + print(f" layer 1 (row semantics) : {layer1_ok}", flush=True) + print(f" layer 2 (chain structure) : {layer2_ok}", flush=True) + print(f" layer 2 controls (pos + neg) : {layer2_controls_ok}", flush=True) + print(f" negative controls all SAT : {controls_ok} " + f"({sum(1 for r in controls.values() if r == sat)}/{len(controls)})") + print(f" width audit (bound necessity) : {audit_ok}", flush=True) + print(f" completeness sweep SAT : {sweep_ok}", flush=True) + print("\n Scope: Layer 2 proves the tiling among groups with exactly ONE head", flush=True) + print(" row. Two DMA calls are separated by the `ts` in both DmaNext tuples,", flush=True) + print(" which `ChainRow` does not model -- see `check_chain`'s docstring and", flush=True) + print(" the textual guard in audit_transcription.py.", flush=True) + ok = (layer1_ok and layer2_ok and layer2_controls_ok and controls_ok + and audit_ok and sweep_ok is True) + if quick: + print("\n NOTE: --quick shortened the completeness sweep and the chain depths.", flush=True) + print(f"\n OVERALL: {'PASS' if ok else 'FAIL -- investigate above'}", flush=True) + sys.exit(0 if ok else 1) + + +if __name__ == "__main__": + main() diff --git a/prover/src/tables/trace_builder.rs b/prover/src/tables/trace_builder.rs index 41c596820..912aed91f 100644 --- a/prover/src/tables/trace_builder.rs +++ b/prover/src/tables/trace_builder.rs @@ -2368,6 +2368,36 @@ pub(crate) fn build_initial_image_paged(elf: &Elf, private_input: &[u8]) -> Page image } +/// Test helper exposing the DMA row decomposition to `prover/src/tests`. +/// +/// [`collect_dma_memcpy_ops`] is private and its `MemoryState`/`RegisterState` +/// operands are module-private, so a unit test cannot reach the decomposition +/// otherwise — and testing `generate_dma_trace` instead proves nothing about it, +/// since that function only formats an already-decomposed op list into columns. +/// `source` seeds the source region so the emitted `value` lanes are meaningful. +#[cfg(test)] +pub(crate) fn dma_ops_for_test( + timestamp: u64, + dst: u64, + src: u64, + count: u64, + source: &[u8], +) -> (Vec, Vec) { + let mut memory_state = MemoryState::new(); + for (i, &byte) in source.iter().enumerate() { + memory_state.write_byte(src + i as u64, byte, 1); + } + let mut register_state = RegisterState::new(0); + register_state.write(10, dst, 1); + register_state.write(11, src, 1); + register_state.write(12, count, 1); + let op = CpuOperation { + timestamp, + ..Default::default() + }; + collect_dma_memcpy_ops(&op, &mut memory_state, &mut register_state) +} + /// Test helper for computing one epoch's local-to-global touched cells without /// building every trace table. #[cfg(test)] diff --git a/prover/src/tests/dma_tests.rs b/prover/src/tests/dma_tests.rs index a88b90019..c8421384a 100644 --- a/prover/src/tests/dma_tests.rs +++ b/prover/src/tests/dma_tests.rs @@ -130,6 +130,361 @@ fn dma_bus_interactions_count() { assert_eq!(bus_interactions().len(), 23); } +/// The canonical vectors, embedded from the validated oracle so the fixture +/// cannot drift from the model that generated it. +/// +/// `formal_verification/dma/test_ref.py` emits this file next to the +/// richer JSON; it is anchored on libc `memmove`, CPython slice assignment, and a +/// row-level vs byte-level replay equivalence over every length 0..=256. +/// Embedding it — rather than hand-transcribing — is what makes a regenerated +/// oracle a compile-time input to these tests instead of a silent no-op. +/// +/// Line format, one record per line: +/// `vector|||||` +/// `row|||||` +const CANONICAL_ROWS: &str = + include_str!("../../../formal_verification/dma/canonical_dma_rows.txt"); + +/// One case parsed out of the canonical row table. +struct OracleVector { + name: String, + src: u64, + dst: u64, + count: u64, + /// Per data row: `(src, dst, count, tail, width)`. + rows: Vec<(u64, u64, u64, bool, u64)>, +} + +/// Parses [`CANONICAL_ROWS`]. Any malformed line is a panic, so a restructured +/// or truncated fixture fails loudly rather than silently matching nothing. +fn parse_canonical_vectors() -> Vec { + fn num(field: &str, line: &str) -> u64 { + field + .parse() + .unwrap_or_else(|_| panic!("canonical rows: bad number {field:?} in {line:?}")) + } + + let mut vectors: Vec = Vec::new(); + let mut declared_rows: Vec = Vec::new(); + for line in CANONICAL_ROWS.lines() { + let line = line.trim(); + if line.is_empty() || line.starts_with('#') { + continue; + } + let f: Vec<&str> = line.split('|').collect(); + match f[0] { + "vector" => { + assert_eq!(f.len(), 6, "canonical rows: bad vector line {line:?}"); + vectors.push(OracleVector { + name: f[1].to_string(), + dst: num(f[2], line), + src: num(f[3], line), + count: num(f[4], line), + rows: Vec::with_capacity(num(f[5], line) as usize), + }); + declared_rows.push(num(f[5], line)); + } + "row" => { + assert_eq!(f.len(), 6, "canonical rows: bad row line {line:?}"); + let vector = vectors + .last_mut() + .expect("canonical rows: a row line appeared before any vector line"); + vector.rows.push(( + num(f[1], line), + num(f[2], line), + num(f[3], line), + num(f[4], line) == 1, + num(f[5], line), + )); + } + other => panic!("canonical rows: unknown record type {other:?}"), + } + } + // The declared data-row count must match the rows that followed. An earlier + // version compared `rows.len()` against a sum of ones — always true — so the + // emitter's declared count was dead data and a fixture claiming 99 rows for a + // 2-row vector stayed green. + for (vector, declared) in vectors.iter().zip(&declared_rows) { + assert_eq!( + vector.rows.len() as u64, + *declared, + "{}: fixture declares {declared} data rows but {} followed", + vector.name, + vector.rows.len() + ); + } + vectors +} + +/// The trace builder's row decomposition equals the oracle's. +/// +/// This calls [`dma_ops_for_test`], which drives the real +/// `collect_dma_memcpy_ops` — the function that actually performs the greedy +/// `8-while-count>=8-then-1` split. An earlier version of this test drove +/// `generate_dma_trace` instead and was **vacuous**: that function only formats +/// an already-decomposed op list into columns, so the test asserted the +/// formatter echoed back the fixture the test itself had built. Mutating the +/// production width rule (`remaining >= 8` -> `remaining > 8`) left it green. +/// +/// Acceptance criterion for any future change here: that mutation must fail this +/// test. +#[test] +fn dma_trace_matches_oracle_row_decomposition() { + use crate::tables::trace_builder::dma_ops_for_test; + + let vectors = parse_canonical_vectors(); + assert_eq!(vectors.len(), 10, "expected all ten canonical vectors"); + // Pin the CONTENT too, not just the count: a fixture that degenerated every + // vector to `count = 0` would still have ten entries, and every assertion in + // the loop below would then be a no-op on zero data rows. + let mut lengths: Vec = vectors.iter().map(|v| v.count).collect(); + lengths.sort_unstable(); + assert_eq!( + lengths, + vec![0, 1, 7, 8, 9, 16, 24, 24, 27, 256], + "canonical vector lengths changed — regenerate the fixture and re-read this test" + ); + // Derived from the lengths by the greedy rule, not hardcoded — a hand-typed + // total is the same "declared, not derived" defect this campaign exists to + // catch, and my first attempt at it was wrong (55 for an actual 57). + let expected_rows: usize = lengths.iter().map(|n| (n / 8 + n % 8) as usize).sum(); + assert_eq!( + vectors.iter().map(|v| v.rows.len()).sum::(), + expected_rows, + "total data rows across the fixture" + ); + + for vector in &vectors { + // Seed the source region the same way the oracle's emitter does. + let source: Vec = (0..vector.count).map(|i| (i * 7 + 3) as u8).collect(); + let (memw_ops, rows) = + dma_ops_for_test(0x30, vector.dst, vector.src, vector.count, &source); + + let data_rows: Vec<_> = rows.iter().filter(|r| !r.end).collect(); + assert_eq!( + data_rows.len(), + vector.rows.len(), + "{}: builder emitted {} data rows, oracle says {}", + vector.name, + data_rows.len(), + vector.rows.len() + ); + + let mut covered = 0u64; + for (row, &(src, dst, count, tail, width)) in data_rows.iter().zip(&vector.rows) { + assert_eq!( + (row.src, row.dst, row.count), + (src, dst, count), + "{}: row at offset {covered} is (src {:#x}, dst {:#x}, count {}), oracle says ({src:#x}, {dst:#x}, {count})", + vector.name, + row.src, + row.dst, + row.count + ); + // `tail`/`width` are derived, so this is the greedy rule itself. + assert_eq!( + row.count < 8, + tail, + "{}: row at offset {covered} disagrees on tail", + vector.name + ); + assert_eq!( + row.value[width as usize..], + [0u8; 8][width as usize..], + "{}: unused value lanes must be zero", + vector.name + ); + for lane in 0..width as usize { + assert_eq!( + row.value[lane], + source[(covered + lane as u64) as usize], + "{}: copied byte at offset {} is wrong", + vector.name, + covered + lane as u64 + ); + } + covered += width; + } + assert_eq!( + covered, vector.count, + "{}: rows cover {covered} bytes of {}", + vector.name, vector.count + ); + + // Exactly one first row and one terminal row, and the terminal row lands + // past the copied range. + assert_eq!( + rows.iter().filter(|r| r.first).count(), + 1, + "{}", + vector.name + ); + assert_eq!(rows.iter().filter(|r| r.end).count(), 1, "{}", vector.name); + // Position, not just count: `first` carries the Ecall receive, the three + // register reads and the `count < MAX + 1` bound, so moving it off the head + // row matters. Counting alone let that mutation through. + assert!( + rows[0].first, + "{}: the head row must be `first`", + vector.name + ); + assert!( + !rows[1..].iter().any(|r| r.first), + "{}: no row after the head may claim `first`", + vector.name + ); + assert!( + rows.iter().all(|r| r.timestamp == 0x30), + "{}: every row of one ecall shares its timestamp", + vector.name + ); + let terminal = rows.last().expect("terminal row"); + assert!(terminal.end && terminal.count == 0, "{}", vector.name); + assert_eq!( + (terminal.src, terminal.dst), + (vector.src + vector.count, vector.dst + vector.count), + "{}: terminal row addresses", + vector.name + ); + + // The MEMW payload. Asserting COUNTS here is not enough: the two phases + // emit equal numbers of operations, so counting alone is satisfied by + // swapping the two timestamps, by flipping `is_read`, or by a wrong + // address or value. Each of those mutations previously survived. Assert + // the fields, and assert the ORDERING as an ordering. + let registers: Vec<_> = memw_ops.iter().filter(|o| o.is_register).collect(); + assert_eq!(registers.len(), 3, "{}: three register reads", vector.name); + assert!( + registers.iter().all(|o| o.timestamp == 0x30 && o.is_read), + "{}: register operands are read at T", + vector.name + ); + assert_eq!( + registers.iter().map(|o| o.base_address).collect::>(), + vec![20, 22, 24], + "{}: registers are x10/x11/x12 at base 2*reg", + vector.name + ); + + let data: Vec<_> = memw_ops.iter().filter(|o| !o.is_register).collect(); + assert_eq!( + data.len(), + 2 * vector.rows.len(), + "{}: one read and one write per data row", + vector.name + ); + let reads: Vec<_> = data.iter().filter(|o| o.is_read).collect(); + let writes: Vec<_> = data.iter().filter(|o| !o.is_read).collect(); + assert_eq!( + (reads.len(), writes.len()), + (vector.rows.len(), vector.rows.len()), + "{}: is_read splits the data ops evenly", + vector.name + ); + + // Bind `is_read` to the phase DIRECTLY. Without this, flipping both flags + // is caught only indirectly: it relabels the phases, so the ordering and + // address assertions below fail instead — and the address one degenerates + // when src == dst. Pin each flag to the timestamp that defines its phase. + assert!( + reads.iter().all(|o| o.timestamp == 0x31), + "{}: every op flagged is_read must be a T+1 source read", + vector.name + ); + assert!( + writes.iter().all(|o| o.timestamp == 0x32), + "{}: every op not flagged is_read must be a T+2 destination write", + vector.name + ); + + // Every read strictly before every write — the property that gives an + // overlapping copy its snapshot semantics. Stated as max(read) < min(write) + // so swapping the two timestamps cannot satisfy it. + if !vector.rows.is_empty() { + let last_read = reads.iter().map(|o| o.timestamp).max().expect("reads"); + let first_write = writes.iter().map(|o| o.timestamp).min().expect("writes"); + assert!( + last_read < first_write, + "{}: every source read must precede every destination write \ + (last read {last_read}, first write {first_write})", + vector.name + ); + assert_eq!( + (last_read, first_write), + (0x31, 0x32), + "{}: reads at T+1, writes at T+2", + vector.name + ); + } + + // Addresses, widths and values, per phase and in offset order. + let mut offset = 0u64; + for (i, &(src, dst, _, _, width)) in vector.rows.iter().enumerate() { + let read = reads[i]; + let write = writes[i]; + assert_eq!( + (read.base_address, u64::from(read.width)), + (src, width), + "{}: read {i} addresses src with the row's width", + vector.name + ); + assert_eq!( + (write.base_address, u64::from(write.width)), + (dst, width), + "{}: write {i} addresses dst with the row's width", + vector.name + ); + for lane in 0..width as usize { + let expected = u32::from(source[(offset + lane as u64) as usize]); + assert_eq!( + read.value[lane], expected, + "{}: read {i} lane {lane} is not the source byte", + vector.name + ); + assert_eq!( + write.value[lane], expected, + "{}: write {i} lane {lane} does not carry the copied byte", + vector.name + ); + } + offset += width; + } + } +} + +/// The maximum chunk is 33 rows with no tail row, derived from the constant +/// rather than from the test's own loop bound. +/// +/// 256 is 8-aligned, so `count % 8 == 0` and every data row is a wide one — the +/// row-count bound the `Alu[count, 257, LT]` lookup exists to enforce. Asserting +/// The expectation below is still computed locally from `DMA_MEMCPY_MAX_BYTES` +/// rather than read out of production code: `trace_builder`'s own +/// `count / 8 + count % 8` feeds only a `Vec::with_capacity` hint and does not +/// drive the loop, so asserting against it would prove nothing. What makes this +/// test non-vacuous is that `rows` comes from the real decomposition, so the +/// greedy width rule and the terminal row are both exercised. +#[test] +fn dma_maximum_chunk_has_no_tail_row() { + use crate::tables::dma::DMA_MEMCPY_MAX_BYTES as MAX; + use crate::tables::trace_builder::dma_ops_for_test; + + let source: Vec = (0..MAX).map(|i| i as u8).collect(); + let (_, rows) = dma_ops_for_test(0x30, 0x1000, 0x2000, MAX, &source); + + // `trace_builder`'s own formula: data_rows = count / 8 + count % 8. + let expected_data_rows = MAX / 8 + MAX % 8; + assert_eq!( + rows.len() as u64, + expected_data_rows + 1, + "expected {expected_data_rows} data rows plus one terminal row" + ); + assert!( + rows.iter().filter(|r| !r.end).all(|r| r.count >= 8), + "no data row may be a tail row when the length is 8-aligned" + ); + assert!(rows.last().expect("terminal").end); +} + #[test] fn dma_constraints_count_and_indices() { use crate::tables::dma::DmaConstraints;