diff --git a/Makefile b/Makefile index a4b05b507..730a409a0 100644 --- a/Makefile +++ b/Makefile @@ -630,6 +630,15 @@ fmt: cargo fmt --all # Run clippy + fmt check (used by CI) +.PHONY: verify-dma +verify-dma: ## Run the DMA memcpy verification campaign (docs/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. Each exits nonzero on failure. + python3 docs/verification/dma/dma-oracle/test_oracle.py + python3 docs/verification/dma/audit_gate_transcription.py + python3 docs/verification/dma/dma-chip/z3_dma_verify.py + lint: cargo fmt --check --all cargo clippy --workspace --all-targets -- -D warnings -A clippy::op_ref diff --git a/docs/verification/dma/README.md b/docs/verification/dma/README.md new file mode 100644 index 000000000..9a48b1709 --- /dev/null +++ b/docs/verification/dma/README.md @@ -0,0 +1,183 @@ +# DMA memcpy — oracle + gate-proved chip + +Verification artifacts for the DMA memcpy accelerator (PR #874). Same shape as +the BLAKE3 campaign (PR #903, branch `feat/blake3-accelerator`): an independent +Python reference model with external anchors, a z3 gate over the AIR's +constraints, a specification with a soundness ledger, and an executable +transcription audit tying all three to the Rust. + +**Scope of the branch.** No shipped constraint, column, bus interaction or +executor path changes. Outside this directory it touches three files: +`prover/src/tests/dma_tests.rs` (two tests driving the real trace-builder +decomposition against the oracle's emitted vectors), a `#[cfg(test)]` accessor in +`prover/src/tables/trace_builder.rs` that exposes that decomposition to the test +(following the `epoch_touched_cells` pattern already in that file), and a +`verify-dma` target in the `Makefile`. Diffed against its base branch +`feat/dma-memcpy`; against `main` you will also see all of PR #874, which is not +merged yet. + +## Why these are here and not in `thoughts/` + +PR #903 keeps its equivalent artifacts under `thoughts/blake3/`, force-added past +a `.gitignore` rule. That rule is deliberate: **PR #863 added `thoughts/` to +`.gitignore` and deleted the working-note files that had leaked into it** — commit +`f2def578`, subject *"chore: keep working notes out of the tree"*, plus more +deletions in the squash `d83b4d9e` (at least four files across the two). +`thoughts/` is where a coding agent dumps scratch, and the maintainers decided +scratch does not belong in the repo. They were right. + +These files are not scratch, and the distinction is testable rather than +rhetorical: all three scripts run unattended, exit nonzero on failure, need one +`pip install`, and the oracle's emitted row table is `include_str!`-ed by a Rust +test that drives the real trace-builder decomposition — so a regenerated oracle is +a compile-time input, not a note. `make verify-dma` runs all three. So they live in +`docs/`, which is tracked on purpose, under a name that says what they are. + +Honest caveat: **no CI workflow runs them yet.** The branch establishes +runnability and wires the fixture into `cargo test`; scheduling the Python side in +CI is a separate call for whoever owns the workflow budget. + +The reason to commit them at all is the one #903 states: two earlier campaigns in +this repo wrote their verification work to a session scratchpad under +`/private/tmp/...` and lost it, and the BLAKE3 files had to be reconstructed by +replaying tool calls out of subagent transcripts. **A gate nobody can rerun is a +claim, not evidence.** Everything here runs from a clean checkout. + +## Contents + +| file | what it is | +|---|---| +| `dma-oracle/dma_ref.py` | the reference model: byte semantics, row decomposition, MEMW multiset, guest chunking | +| `dma-oracle/test_oracle.py` | five-anchor validation harness; emits the canonical vectors | +| `dma-oracle/canonical_dma_rows.txt` | line-oriented row table, `include_str!`-ed by the Rust test | +| `dma-oracle/ORACLE.md` | anchor results, the chip-contract map, open questions | +| `dma-oracle/canonical_dma_vectors.json` | 10 pinned vectors with full column expansions | +| `dma-chip/DESIGN.md` | the constraint system + §7 soundness ledger | +| `dma-chip/IMPLEMENTATION.md` | what ships, what was verified, what is still open | +| `dma-chip/z3_dma_verify.py` | the soundness gate | +| `TRANSCRIPTION-AUDIT.md` | does the gate assert what the Rust says? | +| `audit_gate_transcription.py` | the executable half of that audit (100 claims) | + +## Results, 2026-08-11 + +``` +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] mutation sweep 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 (~96 s on z3 5.0.0) + +audit: 100 claims, 0 findings; mutation-tested against 6 source mutants, 6 caught + +rust: cargo test -p lambda-vm-prover --lib dma 18 passed +``` + +`make verify-dma` runs all three. Full gate transcript in `dma-chip/DESIGN.md` §9. + +## What the gate proves, in one paragraph + +Given the modelled lookup contracts and given that bus balance means multiset +equality: every satisfying assignment of one DMA row does what the oracle says +(`tail = count < 8`, `end = count == 0`, `src_incr = src + width` without +wrapping `2^64`, `count_decr = count − width` wrapping only on the terminal row); +among groups containing exactly one head row, the only bus-balanced multi-row +structure at depth ≤ 5 is a single chain whose data rows tile `[src, src+n)` +exactly once with the greedy widths; each of the **ten** range checks and lookups +involved is individually necessary, each with a named forgery; and the AIR accepts +every honest trace for every length `0..256`. + +The gate is honest about four things it cannot see — bus wiring, the memory +consistency argument (hence overlap ordering), LogUp soundness, and trace length. +The first is what `audit_gate_transcription.py` exists for. + +## No open soundness gap — and a retracted finding worth reading about + +The board is clean: no residual, no known hole in the chip. An independent +security scan, deliberately blinded to these artifacts, reached the same +conclusion and independently re-derived all ten items of `DESIGN.md` §7. + +An earlier version of this campaign reported one — "RESIDUAL R1", that `count`'s +limb split was unconstrained on non-head rows — and published it as the headline +result across five documents. **It was wrong**, and the story is the most useful +thing here. The gate modelled the `DmaNext` hop as one equation on a packed +64-bit value; the bus actually binds **two 32-bit elements** with separate alpha +powers, so the limbs are pinned and the alias the gate exhibited is unreachable. +`DESIGN.md` §7 carries the full account. + +Three transferable lessons: + +* **The direction of a modelling error decides its cost.** Weaker than the AIR ⇒ + false alarms, never false proofs; every UNSAT survived the correction. Stronger + than the AIR ⇒ false proofs that no positive anchor can catch. Classify every + gap before trusting any result. +* **A phantom finding induces real damage.** Working around R1 led to asserting + `count ≤ 256` on *every* row of the field-exact chain check, when the AIR bounds + only the head — a genuine over-strong assumption, in the dangerous direction. +* **A proposed fix that is a no-op means the gap isn't there.** R1's second fix + was "receive `count` as `DWordHL`", which changes nothing under the real + semantics. + +## Method notes worth reusing + +**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)` — `lt.rs` range-checks `lhs[1]` and `lhs[2]` but not the bare +`LHS_0` word, so the contract form would hide which limbs are actually pinned. +**But apply the same rule to the bus itself, which is what the retracted R1 got +wrong:** "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()` rather than assumed. +The audit's §G now asserts it. + +**Negative controls must be paired with the check they can actually break.** +Three of the original eight reported UNSAT because they dropped a premise and +re-ran a check whose reference said nothing about it — a control that cannot fail. +And a multi-row check needs *its own* controls: Layer 2 shipped with neither a +positive (is the premise set even satisfiable?) nor a negative one. Both are on +the board now. `TRANSCRIPTION-AUDIT.md` §4. + +**Do not negate a modular equality that carries a witness quotient.** The gate's +first run reported a bogus SAT on its main check for exactly this reason: +`Not(a − b == k·2^64)` is satisfiable by picking a nonzero `k`. Under negation, +spell the claim out witness-free. (Encoding note in `FieldRow`.) + +**Field-exact, over integers, linear.** Every column is an `Int` in `[0, p)`, +modular equalities carry explicit quotients, and `x·(1−x) = 0` becomes +`x ∈ {0,1}` (exact for `x < p` prime). A bit-vector model cannot answer a +"is a range check missing?" question at all, since it bounds the unconstrained +column for free — but the naive `%p` encoding is nonlinear and the first version +of this gate timed out on its own main check. The rewrite is what made the +5410-row completeness sweep affordable. + +**Mutation-test the audit, not just the model.** Five source mutants; one was +initially missed, because the check asserted an error variant was *mentioned* +rather than that the guard existed — a `if false` guard passed. That is precisely +the defect class the audit exists to catch, found in the audit itself. + +## Where to send the next reviewer + +1. **The `Memw` ordering argument for unaligned 8-byte accesses.** A misaligned + DMA copy generates one on nearly every row, and the snapshot/overlap story + rests entirely on `T+1` reads preceding `T+2` writes per address. Nobody has + checked it. Largest remaining gap around this feature, and not DMA's to fix. +2. **Assumptions A1–A4** (`DESIGN.md` §Assumptions), centrally rather than + per-chip. `IS_WORD` appears across ~10 spec chapters *exclusively* inside + `[[assumptions]]`, with no interaction, no template and no 2³² table — so the + spec asserts a range obligation for nearly every address, register value and + timestamp in the VM without naming a discharger. That vacuum is what an earlier + draft of `DESIGN.md` filled by inventing labels for it. +3. **`spec/memw.typ`'s `value` obligation**, which it assigns to "the system as a + whole", i.e. to nobody. DMA is a concrete sender for which no chip discharges it. +4. **For PR #874, not this branch:** `end·(1 − tail) = 0` would close the + `count = 7` seven-byte-truncation hole inside the AIR instead of leaving it + entirely to the `Alu` bus (defense-in-depth — the pin is sound today); DMA is + the only high-volume table with no `max_rows`/chunking; and there is no + `spec/dma.typ`. diff --git a/docs/verification/dma/TRANSCRIPTION-AUDIT.md b/docs/verification/dma/TRANSCRIPTION-AUDIT.md new file mode 100644 index 000000000..01adbbb7d --- /dev/null +++ b/docs/verification/dma/TRANSCRIPTION-AUDIT.md @@ -0,0 +1,307 @@ +# Transcription audit — does the DMA gate assert what the Rust actually says? + +The gate (`dma-chip/z3_dma_verify.py`) proves things about a **model**. Every +UNSAT it reports 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. + +That is not hypothetical. The EC campaign's equivalent audit +(`thoughts/ec-recover-opt/gate/TRANSCRIPTION-AUDIT.md`, referenced by PR #903) found three premises its gate +asserted about the chip and never read, one of them hiding a working forgery, +and the BLAKE3 campaign's found that its "free range check" was declared rather +than derived (PR #903's `thoughts/blake3/GATE-TRANSCRIPTION-AUDIT.md` F1). Both were found by +reading the source against the model, not by running the model. + +## Verdict + +**No drift.** 100 textual and structural claims, 0 findings +(`python3 audit_gate_transcription.py`, against the working tree at `ef9e7526` +plus this branch). Per-section counts are printed by the script; §1 quotes that +output rather than restating it. + +**No residual.** An earlier version of this audit carried one — "R1", that +`count`'s limb split was unconstrained on non-head rows — and it was **wrong**: +`DmaNext` binds each 64-bit value as two 32-bit bus elements, not one packed +field element, so the limbs are pinned. §6 below is now the account of that error +rather than a finding, and §1 records the audit gap that let it through: the +audit checked that the packing *names* appeared and never that the element counts +aligned. Section **G** now does. + +**One structural asymmetry worth naming.** Unlike BLAKE3, this campaign's +`DESIGN.md` was written *after* the Rust, so it cannot independently disagree +with it. The independent notion of "correct" comes entirely from the oracle +(`dma-oracle/`, anchored on libc `memmove` and CPython, neither of which knows +this repo exists) and from the audit script keeping the design, the gate and the +Rust textually pinned to each other. Anyone re-reviewing should treat +`DESIGN.md` as *evidence about the gate*, not as evidence about the chip. + +## §1 — What was checked, and how hard + +`audit_gate_transcription.py` is deliberately **textual** — regex over the Rust +source — rather than a Rust test. The point is to catch a change in `dma.rs` that +nobody reflected in this directory, and a Rust test would be edited in the same +commit as the code it guards. + +Counts below are the script's own output, not prose. An earlier version stated +them by hand and got **five of six wrong** — apportioned to sum to the real total +of 83 rather than measured, which is exactly the "declared, not derived" defect +this file exists to catch. The script now prints them. + +``` + A. constants 10 claims every number the oracle and gate hard-code + B. columns 28 claims the full dma::cols layout, NUM_COLUMNS, density + C. constraints 10 claims each index, template, operands, the degree bound, + and that no index exists the gate does not model + D. buses 23 claims 23 interactions, bus mix, every multiplicity, and + the four wiring facts the gate cannot see + E. executor 5 claims the ecall validates what the oracle validates, + in that order + F. generator 7 claims the padding row is the row the oracle describes + G. bus packing 14 claims element counts per Packing and DmaNext tuple + alignment -- the section whose absence hid R1 + H. fixture pinning 3 claims the Rust test consumes the oracle's output +``` + +### Sensitivity — the audit was mutation-tested + +An audit that cannot fail is not an audit. Five mutants were applied to copies of +the source and the script re-run; all five are caught: + +| 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 | needed a strengthened check | +| **`num_bus_elements(DWordHL)` `2 → 1`** | 1 | **the mutant that was not caught at all** | +| a `rustfmt`-style reflow of `if tail { 1 } else { 8 }` | **0** | must NOT fire — see below | + +Two of these are the point of the section. + +**The `num_bus_elements` mutant was not caught before**, because §D checked only +that the strings `DWordWL`/`DWordHL` appeared in the two tuples and never that +their element counts aligned. That is the gap the retracted R1 came through, and +it is a textbook instance of the failure this file is written to prevent: the gate +asserted a premise about the bus that nothing ever read from the source. §G now +asserts the element count of every `Packing` variant, that no variant folds a +64-bit value into one element, that `DWordHL` accumulates two halves at +consecutive alpha powers, and that both `DmaNext` tuples carry 8 elements. + +**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 — dead code. `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. + +The executor mutant also needed strengthening: the original asserted only that the +`DmaMemcpyChunkTooLarge` variant appeared before the `checked_add` calls, which a +guard rewritten to `if false` satisfies. It now requires the literal predicate. +**Three of the seven mutants were initially missed, in a file whose entire job is +catching exactly this.** + +## §2 — Per-premise table (gate ↔ design ↔ Rust) + +| gate premise | modelled as | discharged by | verified where | +|---|---|---|---| +| `IsHalfword[h]` ⟹ `h < 2^16` | hard range bound under `mu == 1` | preprocessed table; the contract *is* the range | audit D: all 12 sends present, on the right columns, at multiplicity `mu` | +| `Zero[v] → z` | `v = x + 256y + 65536z`, x,y bytes, z<16, `z = (v == 0)` | `bitwise.rs` `generate_bitwise_row` | audit A (domain), D (the send's shape, the four `-1` coefficients) | +| Zero **domain** `v < 2^20` | asserted at gate import | halfword bounds put the argument in `[0, 262140]` | gate module assert; audit A | +| `Alu[a,b,LT] → o` | `lt.rs`'s own columns and carries, **not** `o = (a **`IS_WORD` has no discharger.** It appears across ~10 chip TOMLs +> **exclusively** inside `[[assumptions]]` blocks — never as `kind = "interaction"` +> or `kind = "template"` — and `spec/bitwise.typ` offers only MSB8/MSB16/ZERO/ +> ARE_BYTES/IS_HALF/IS_B20, a 2^32 table being infeasible. So the spec asserts a +> range obligation for essentially every address, register value and timestamp in +> the VM without saying how it is met or which chip owns it per sender. **That +> vacuum is what this campaign filled by inventing two label names, and the next +> chip author will fill it the same way.** It wants either a +> `= Range-check provenance` chapter or a per-sender naming requirement. + +Related and equally ownerless: `spec/memw.typ:42-45` concedes that `value` range +checks "are necessary for the consistency of the system as a whole" and documents +the types "as a reading help". DMA is a concrete sender for which no chip +discharges it. An obligation owned by everyone is owned by nobody. + +## §6 — The retracted finding, and what it cost + +This section used to be a finding. It is now the account of an error, kept because +the error is more instructive than the finding would have been. + +**What was claimed.** That `DmaNext` "equates packed field elements", so `count`'s +limb split was unconstrained on non-head rows, and a Goldilocks alias +(`COUNT_1 = 2^32−1`, `COUNT_0 = V+1`, packed ≡ V mod p) would pass the chain while +`lt.rs` saw an integer near `2^64` and returned `tail = 0` — a row claiming an +eight-byte width where fewer than eight bytes remained, blocked only by trace +length. Two fixes were recommended. + +**Why it was wrong.** `Packing::num_bus_elements()` returns **2** for both +`DWordWL` ("2× Direct") and `DWordHL` ("2× Word2L"), and +`accumulate_fingerprint_with` gives each element its own alpha power. No `Packing` +variant contains a `2^32` shift, so a 64-bit value is never one bus element +anywhere in this codebase. Both `DmaNext` tuples are `1+1+2+2+2 = 8` elements and +align pairwise, so balance forces `COUNT_0 = cd₀ + 2^16·cd₁` **and** +`COUNT_1 = cd₂ + 2^16·cd₃`. With the sender's four halfwords `IsHalfword`-checked, +the receiver's limbs are 32-bit for free. Under the corrected link the alias is +UNSAT and the successor's count is pinned exactly. + +**Four things to take from it.** + +1. **Classify the direction of every modelling gap.** A model *weaker* than the + AIR yields false alarms but never false proofs — every UNSAT on the board + survived the correction, having been proven under weaker hypotheses than + reality supplies. A model *stronger* than the AIR is the one that yields a + false proof no positive anchor can catch. +2. **A phantom finding causes real damage.** Working around R1 led to asserting + `count ≤ 256` on *every* row of the field-exact chain check when the AIR bounds + only the head — the one genuinely over-strong assertion in the gate, i.e. the + dangerous direction, introduced to accommodate something that did not exist. +3. **A proposed fix that is a no-op means the gap is not there.** R1's second fix + was "receive `count` as `DWordHL`", which changes nothing under the real + semantics. That should have stopped the write-up. +4. **The audit's coverage gap is the root cause, not the gate's model.** §D pinned + the tuples' column names and multiplicities and never their packing semantics, + so "83 claims, 0 findings" never tested the one fact R1 rested on. §G exists + now, and the `num_bus_elements(DWordHL) 2 → 1` mutant is in the regression set. + +## §7 — Still open (report-only, outside this audit's scope) + +1. **The memory-consistency argument.** The whole snapshot/overlap story rests on + `T+1` reads strictly preceding `T+2` writes per address. The gate cannot see + timestamps; the audit script checks the constants are `+1`/`+2` and that the + offset only touches the low limb; the oracle's `write_before_read` and + `interleaved` mutants cover the model side. Nobody has checked the `Memw` + table's ordering argument for *unaligned 8-byte* accesses, which is what a + misaligned DMA copy generates on nearly every row. +2. **`count_table_lengths`** — the disk-spill sizing pass. The PR's own + `count_table_lengths_drift_tests.rs` covers DMA; not re-derived here. +3. **The multi-call case.** Layer 2 proves the tiling among groups containing + exactly one head row. `ChainRow` carries no timestamp, so two DMA calls in one + trace are out of model; the `ts` carried in both `DmaNext` tuples is what + separates them, and it is guarded only textually (audit §D). +4. **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. +5. **Two ecalls at one timestamp.** Ruled out by CPU timestamps being strictly + increasing per instruction. Asserted, not verified here, and it is what the + `DmaNext` timestamp binding relies on. + +## §8 — Reproducing + +```sh +python3 docs/verification/dma/dma-oracle/test_oracle.py # anchors + emit vectors +python3 docs/verification/dma/dma-chip/z3_dma_verify.py # the gate (add --quick to shorten) +python3 docs/verification/dma/audit_gate_transcription.py # this audit +cargo test -p lambda-vm-prover --lib dma # the Rust side, incl. the vector test +``` + +`make verify-dma` runs all three. `z3-solver` is the only dependency +(`pip install z3-solver`; validated on 5.0.0 — the audit alone needs no solver). +The gate takes ~96 s for the full board on 5.0.0, dominated by the completeness +sweep; on 4.12.2 it takes ~1210 s and two queries blow their budgets and report +`unknown`, which is scored as **failure** everywhere. The oracle exits 2 when it +ran but an anchor skipped, so a degraded run is distinguishable from a clean one. +No CI workflow schedules any of this yet. diff --git a/docs/verification/dma/audit_gate_transcription.py b/docs/verification/dma/audit_gate_transcription.py new file mode 100644 index 000000000..a62f94609 --- /dev/null +++ b/docs/verification/dma/audit_gate_transcription.py @@ -0,0 +1,609 @@ +""" +Executable half of the transcription audit: does the gate model the Rust that +was actually written? + +The gate (`dma-chip/z3_dma_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_gate_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 `docs/verification/dma/`, so the repo root is three up. +DEFAULT_REPO = os.path.abspath(os.path.join(HERE, "..", "..", "..")) + +sys.path.insert(0, os.path.join(HERE, "dma-oracle")) +sys.path.insert(0, os.path.join(HERE, "dma-chip")) +import dma_ref as ref # noqa: E402 + +#: The three gate constants this audit cross-checks. Duplicated deliberately +#: rather than imported: importing `z3_dma_verify` drags in `z3`, and ~80 of the +#: 83 claims here are textual and need no solver at all -- so a machine without +#: z3 could not run the audit even to check column indices. `audit_constants` +#: asserts these against the gate's own values when the module IS importable. +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) + + a.ok("no Packing variant folds a 64-bit value into one bus element", + not re.search(r"Packing::\w+ => 1,\s*// 2x", body), + "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") + 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, "docs/verification/dma/dma-oracle/" + "canonical_dma_rows.txt").splitlines()) > 20) + + +# --------------------------------------------------------------------------- + +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/docs/verification/dma/dma-chip/DESIGN.md b/docs/verification/dma/dma-chip/DESIGN.md new file mode 100644 index 000000000..e774a4fac --- /dev/null +++ b/docs/verification/dma/dma-chip/DESIGN.md @@ -0,0 +1,457 @@ +# DMA memcpy chip — constraint-system & bus design + +> **Provenance, read this first.** This document is written *after* +> `prover/src/tables/dma.rs` (PR #874) — unlike a design-first campaign, where the +> spec precedes the code and the gate proves the design. It is the specification +> **recovered from the implementation**, and it is what `z3_dma_verify.py` +> checks. That ordering has one consequence worth stating plainly: a design +> document derived from the code cannot find a disagreement between them by +> itself. `../audit_gate_transcription.py` is what keeps this file and the Rust +> from drifting, and the oracle (`../dma-oracle/`) is what supplies an +> independent notion of "correct" that neither the code nor this file defines. + +## 1. What the chip proves + +One `memcpy(dst, src, n)` ecall, `n ≤ 256`, moved off the CPU trace. The guest's +strong `memcpy` symbol chunks arbitrary lengths into ecalls of at most 256 +bytes; the executor performs each chunk natively; this table proves it. + +The claim, stated as the oracle states it (`../dma-oracle/dma_ref.py`): + +> For an ecall at timestamp `T` whose registers hold `(x10, x11, x12) = +> (dst, src, n)`, the trace contains memory operations that read every byte of +> `[src, src+n)` at `T+1` and write the same bytes to `[dst, dst+n)` at `T+2`, +> each byte exactly once, in the greedy chunking `[8]*(n/8) + [1]*(n%8)`, and +> nothing else. + +Three separable obligations fall out, and the gate answers them separately: + +| obligation | mechanism | gate check | +|---|---|---| +| a copied byte cannot change | the read tuple and the write tuple reference the **same** `value` columns | not a proof obligation at all — structural. Audited textually (`../audit_gate_transcription.py` §D) | +| the copy covers exactly `[src, src+n)`, once | row chaining through `DmaNext` + `Zero` end detection + the `LT` width pin | MAIN 0–3, CHAIN, CHAIN-F | +| one ecall cannot add unbounded rows | the first row proves `count < 257` on the `Alu` bus | MAIN 2c | + +## 2. Row layout decision + +A row copies **eight bytes while `count ≥ 8`, otherwise one byte**. The design +is cloned from `commit.rs`: recursive/streaming, one row per chunk, rows chained +by a bus rather than by a transition constraint. + +Why not one row per byte: 257 rows per maximal ecall (256 data + 1 terminal) +instead of 33. +Why not one row per whole copy: the row would need `n` value columns for an +unbounded `n`, and 8-byte-wide memory operations are the widest the `Memw` +table serves. + +Why the 1-byte tail rather than 4/2/1 halving: 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 width selector and a +width-to-`w2/w4/w8` decode. + +The cost, stated precisely (an earlier draft had this wrong in both directions): +a copy of `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 +the maximal `n = 255`, 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 (halving needs `popcount(n % 8) ≤ 3`), not the 7 an earlier draft claimed +by comparing against a zero-tail design instead of against the alternative it was +arguing with. + +## 3. Column layout (32 columns) + +| columns | name | packing | range provenance | +|---|---|---|---| +| 0–1 | `timestamp` | DWordWL | the `Ecall` receiver (the CPU's own timestamp) | +| 2–3 | `src` | DWordWL | head row: **assumption A1** (see §Assumptions). Non-head rows: *derived* — the `DmaNext` link binds each 32-bit limb against the predecessor's `IsHalfword`-checked halfwords (§5.1) | +| 4–7 | `src_incr` | DWordHL | `IsHalfword` ×4, multiplicity `mu` | +| 8–9 | `dst` | DWordWL | as `src` | +| 10–13 | `dst_incr` | DWordHL | `IsHalfword` ×4 | +| 14–15 | `count` | DWordWL | head row: **assumption A2**. Non-head rows: *derived*, same mechanism as `src` | +| 16–19 | `count_decr` | DWordHL | `IsHalfword` ×4 | +| 20 | `first` | Bit | constraint 0 | +| 21 | `end` | Bit | constraint 1 | +| 22 | `tail` | Bit | constraint 2 | +| 23–30 | `value[8]` | Byte-ish | **nothing** — they ride only the `Memw` tuples; lanes 1–7 are forced to zero on tail rows by constraints 11–17 | +| 31 | `mu` | Bit | constraint 3 | + +`src_incr`/`dst_incr`/`count_decr` are `DWordHL` (four 16-bit halfwords) and not +`DWordWL` **because they need a range check**, and `IsHalfword` is the cheapest +one available. Their halves are what makes `emit_add_pair_no_overflow`'s +`carry_1 = 0` mean "no wrap" instead of "the high word happens to be `2^32`" — +proved necessary by the width audit (§8.1). + +`value[0..8]` carry no range check of their own, and the reason is **not** that +the receiving table checks them — `spec/memw.typ` says the opposite in as many +words: *"Our assumptions do not explicitly cover any range checks for the `value` +column."* (An earlier draft cited `keccak.rs` here as authority for relying on +the receiver. That was 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.) + +The actual argument is narrower and specific to this chip: the `T+1` read tuple +carries `old == value` **against real memory** (§5, bus 22), so each lane is +pinned to the byte the memory argument says is at that address. Lanes are not +free field elements; they are whatever memory already held. + +What that does **not** cover is the tail case: on a one-byte row the memory tuple +must be the canonical `w8 = 0` encoding, so lanes 1–7 must be zero, hence +constraints 11–17. + +## 4. Constraints (18, all degree 2) + +`DmaConstraints` does not override `max_degree`, so it declares the default 2. +Every constraint below is degree 2, and the gate's encoding notes record why: +each carry is a *linear* expression in the columns (`step = 8 − 7·tail` is +linear, and `carry_0` feeds `carry_1` linearly), so booleanity on a carry and a +`boolean × column` product are both quadratic and nothing is cubic. + +| idx | constraint | template | +|---|---|---| +| 0–3 | `first`, `end`, `tail`, `mu` are bits | `emit_is_bit` | +| 4 | `(first + end)·(1 − mu) = 0` | inline | +| 5–6 | `src + step = src_incr`, no `2^64` wrap on active non-terminal rows | `emit_add_pair_no_overflow(MU, END)` | +| 7–8 | `dst + step = dst_incr`, same | `emit_add_pair_no_overflow(MU, END)` | +| 9–10 | `count_decr + step = count` (**wrap permitted**) | `emit_add_pair` | +| 11–17 | `tail · value[i] = 0`, `i = 1..7` | inline | + +Two asymmetries are load-bearing and must not be "tidied": + +**Constraint 9–10 is the plain pair on purpose.** The terminal row holds +`count = 0` and `count_decr = 0 − 1 = 0xFFFF_FFFF_FFFF_FFFF`; a no-overflow form +would reject it. The gate's MAIN 2 is precisely the statement that this +permission is safe: **the count subtraction wraps only on the terminal row**, +because `tail` is pinned to `count < 8` so `step ≤ count` on every row with +`count ≥ 1`. Take the pin away and the wrap becomes reachable on a data row, +which is the seven-byte truncation in §8.1. + +**Constraints 5–8 are the no-overflow form on purpose.** Without it a chain +could walk `src` past `2^64` and continue at low addresses, which the executor +rejects (`checked_add`) and the AIR would not — an executor/AIR divergence, and +a copy that touches unrelated memory. Gate control `drop_no_overflow_src`. + +`emit_add_pair_no_overflow`'s gate is `mu − end`: terminal and padding rows +leave `carry_1` free, because their computed successor is consumed by nobody +(the `DmaNext` send has the same multiplicity). + +## 5. Bus interactions (23) + +| # | bus | dir | multiplicity | tuple | +|---|---|---|---|---| +| 1 | `Ecall` | recv | `first` | `[ts, DMA_LO32, DMA_HI32]` | +| 2 | `DmaNext` | send | `mu − end` | `[ts, src_incr, dst_incr, count_decr]` | +| 3 | `DmaNext` | recv | `mu − first` | `[ts, src, dst, count]` | +| 4–15 | `IsHalfword` | send | `mu` | each halfword of `count_decr`, `src_incr`, `dst_incr` | +| 16 | `Zero` | send | `mu` | `[4·65535 − Σ count_decr, end]` | +| 17–19 | `Memw` | send | `first` | register reads of x10, x11, x12 | +| 20 | `Alu` | send | `mu` | `[count, 8, LT] → tail` | +| 21 | `Alu` | send | `first` | `[count, 257, LT] → 1` | +| 22 | `Memw` | send | `mu − end` | read `src` at `T+1`, `w8 = 1 − tail`, `old == value` | +| 23 | `Memw` | send | `mu − end` | write `dst` at `T+2`, same `value` columns | + +### 5.1 `DmaNext` carries the timestamp in **both** tuples + +Non-negotiable, and for the reason the BLAKE3 design review found the hard way: +without a per-call binding in both halves of an internal bus, rows belonging to +two different calls can be spliced into each other's chains and the multiset +still balances. Here the timestamp is that binding, and CPU timestamps are +strictly increasing per instruction, so two DMA ecalls never share one. + +### 5.2 End detection: one `Zero` lookup, four halfwords + +`end = 1` iff `4·65535 − (cd₀+cd₁+cd₂+cd₃) = 0`, i.e. iff all four halfwords are +`0xFFFF`, i.e. iff `count_decr = 2^64 − 1`, i.e. (with the width pin) iff +`count = 0`. One lookup instead of four. + +Two premises hold it up, and the width audit separates them: +* the `IsHalfword` bounds — a sum can only identify the all-`0xFFFF` word while + each summand is in range. Drop them and `(0xFFFF+d, 0xFFFF−d, 0xFFFF, 0xFFFF)` + reaches the same sum with a totally different `count_decr`, so `end` is + claimable at a nonzero count. Since an `end` row's two `Memw` sends have + multiplicity `mu − end = 0`, **it emits no memory operations at all** — a + silently truncated copy with every bus balanced. +* the receiving table's **domain**. `bitwise.rs` serves `Zero[v]` only for + `v = x + 256y + 65536z` with `x,y` bytes and `z < 16`, i.e. `v < 2^20`. The + send's argument lies in `[0, 262140]` under the halfword bounds, comfortably + inside; a send outside would have no partner row at all. The gate asserts + `4·65535 < 2^20` at import. + +### 5.3 The width pin + +`Alu[count, 8, LT] → tail` at multiplicity `mu` is the only thing that stops the +prover choosing a convenient partition. §8.1 shows what a free `tail` buys. + +### 5.4 The per-call bound + +`Alu[count, 257, LT] → 1` at multiplicity `first`. `dma.rs` takes the constant +*from the executor* (`DMA_MEMCPY_MAX_BYTES as EXECUTOR_DMA_MEMCPY_MAX_BYTES`) +rather than restating it, so the bound the AIR proves cannot drift from the +bound execution enforces. That is the un-driftable form and the audit checks it +stays that way. + +### 5.5 Value binding is structural, not proved + +The read tuple and the write tuple are built from the same `value_columns()`. +Nothing needs to prove `read == write`, because there is one set of columns. +This is the strongest kind of argument available and also the kind a solver +cannot see, so it is audited textually (`§D` of the audit script), together with +the facts that the read carries `old == value`, that the offsets are `+1`/`+2`, +and that `w8 = 1 − tail` on both. + +## 6. Overlap and the two timestamps + +All reads at `T+1`, all writes at `T+2`, both as AIR constants. That is what +gives an overlapping copy snapshot (`memmove`) semantics: the memory-consistency +argument orders per-address accesses by timestamp, so every read sees +pre-ecall memory. The executor matches by copying through a fixed scratch buffer. + +**Caveat the oracle records as O2:** the snapshot is per ecall, not per +`memcpy`. Chunk *k+1* reads memory chunk *k* already wrote, so a guest-level +`memcpy` of more than 256 bytes is a forward copy, not a `memmove`. That is +in-contract for `memcpy`, but it means "the DMA ecall has memmove semantics" +must not be repeated at the C level. + +## 7. Soundness-critical spots a change must not touch + +1. **`DmaNext` timestamp in both tuples** (§5.1). Removing it splices calls. +2. **`IsHalfword` on all twelve halfwords** (§5.2, §8.1). 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`** (§4). Swapping either direction breaks the terminal row or + admits an address wrap. +4. **`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. +5. **The `Alu` width pin** (§5.3). Gone, the prover partitions at will, and + `count = 7, tail = 0` truncates seven bytes. +6. **`tail · value[i] = 0`** (§3). Gone, a one-byte row's memory tuple carries + seven unconstrained field elements into the `Memw` bus. +7. **The bound constant taken from the executor** (§5.4). Restating it invites + the AIR bound and the execution bound to drift. +8. **One `first` per timestamp**, supplied by the `Ecall` receiver against the + CPU's single send. Two heads at one timestamp would unbalance `Ecall`. +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. It is worth knowing this is where termination comes from. +10. **The `DmaNext` tuples' element alignment** (§5.1). Both tuples are 8 bus + elements and align pairwise; that is what makes the link a per-limb binding + and hence what supplies the range provenance in §3 for every non-head row. + A packing change on either side silently changes what the bus binds. + +### The limb binding, and the finding that turned out not to exist + +`DmaNext` does **not** compare packed 64-bit values. `Packing::num_bus_elements()` +(`crypto/stark/src/lookup.rs:227-241`) returns **2** for both `DWordWL` ("2× Direct") +and `DWordHL` ("2× Word2L"), and each element gets its own alpha power. 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) +``` + +Since the sender's four `count_decr` halfwords are `IsHalfword`-checked at +multiplicity `mu`, **the receiver's limbs are 32-bit for free** — no extra range +check needed. Same for `src` and `dst`. This is what §3's "derived" entries mean, +and it is why MAIN 3 is an unconditional claim rather than a disjunction. + +**Recorded because the campaign got this wrong first.** An earlier version of the +gate modelled the hop as one equation on the fully packed value, which is +strictly *weaker* than the AIR: it let the receiver re-split its limbs and so +manufactured an alias (`COUNT_1 = 2³²−1`, `COUNT_0 = V+1`, packed ≡ V mod p) +that the real bus rejects. That phantom was published here as "RESIDUAL R1 — the +one live gap", with two recommended fixes. It has been struck. Two things worth +keeping from the episode: + +* **The direction of a modelling error decides what it costs.** A model weaker + than the AIR yields false alarms but never false proofs — every UNSAT the gate + reported survived the correction, having been proven under weaker hypotheses + than reality supplies. A model *stronger* than the AIR is the dangerous one. +* **A proposed fix that is a no-op is evidence the gap is not there.** R1's + second fix was "receive `count` as `DWordHL`", which under the real semantics + changes nothing. That should have been caught at authoring time. + +`../audit_gate_transcription.py` §G now asserts the element counts and the tuple +alignment directly; its absence is what let the phantom through, since the audit +previously checked only that the packing *names* appeared. + +## Assumptions + +Obligations on the **caller**, not checks this chip performs. Real spec chapters +render this section (`render_chip_assumptions`); its absence from an earlier draft +is why two caller obligations got mislabelled as receiver checks in §3. + +| id | assumption | discharged by | status | +|---|---|---|---| +| **A1** | the head row's `src`/`dst` limbs are 32-bit words | `spec/src/memw.toml`: `[[assumptions]] IS_WORD[base_address[i]]`. `memw.rs:257-262` justifies its own bound via *the CPU table*; DMA is a non-CPU sender, so that argument does not extend here | **not discharged locally.** Non-DMA-specific — every table sending an address depends on it | +| **A2** | the head row's `count` limbs are 32-bit words | `spec/src/memw_register.toml`: `[[assumptions]] IS_WORD[val[i]]`. MEMW_R's only range-check interaction is on the timestamp delta | **not discharged locally.** The gate's `drop_reg32` control shows what it buys: without it the `count < 257` lookup caps only a residue class | +| **A3** | `IS_WORD` on the timestamp, so `ts₀ + 2` does not carry into the high limb | `spec/src/memw.toml` timestamp assumption. In practice the CPU stride is 4 and `T = 4i+4`, so the `+1`/`+2` cannot carry — but nothing in the DMA AIR constrains it | 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 | + +A1/A2 are the **head row only**. Every other row's limbs are derived (§7 above). +Note the irony worth recording: the phantom R1 reported a gap on non-head rows, +where the bus in fact pins the limbs, while the real obligation sits on the head +row, which has no `DmaNext` receive at all. + +`spec/` has a broader problem here, flagged for the spec rather than this chip: +`IS_WORD` appears across ~10 chapters **exclusively** inside `[[assumptions]]`, +never as an interaction or template, and `spec/bitwise.typ` offers no 2³² table. +So the spec asserts a range obligation for nearly every address, register value +and timestamp in the VM without naming a discharger. That vacuum is what an +earlier draft of this document filled by inventing the labels "MEMW-ADDR32" and +"REG-32", and the next chip author will fill it the same way. + +## Padding + +Real spec chapters render this too (`render_chip_padding_table`), and the DMA +padding row is not all-zero, so it is worth writing down. + +`generate_dma_trace` pads to the next power of two, minimum 4, with: + +| column | value | why | +|---|---|---| +| `mu` | 0 | kills all 23 bus interactions | +| `first`, `end` | 0 | forced by constraint 4 once `mu = 0` | +| `count` | 1 | constraints 9–10 are **unconditional**, so padding must satisfy them | +| `tail` | 1 | so `step = 1` and `count_decr = count − 1 = 0` | +| `src_incr`, `dst_incr` | 1 | so the low carry is 0 rather than −1 | +| everything else | 0 | | + +The gate's completeness sweep pins exactly this row (`dma_ref.padding_columns`), +and `dma_padding_row_cannot_claim_first_or_end` covers the one constraint that +stops a padding row masquerading as a copy's head or terminal row. + +## 8. Gate + +`z3_dma_verify.py`. Two layers (field-exact single/paired rows; integer and +field-exact multi-row chains with `DmaNext` as a free bijection rather than an +assumed chain), eight negative controls, a field-level width audit, and an +oracle-pinned completeness sweep over every length `0..256`. + +What it cannot see, stated in its own docstring: bus **wiring** (covered by +`../audit_gate_transcription.py`, whose §G now includes the packing/element-count +claims whose absence let a phantom finding through), the memory consistency +argument and hence overlap ordering (covered on the model side by the oracle's +`write_before_read` mutant), and LogUp soundness (assumed). Layer 2's scope is +also bounded: it proves the tiling among groups containing exactly **one head +row**, because `ChainRow` does not model the timestamp that separates two calls. + +### 8.1 The width audit — three bound-necessity results + +Each is run twice, with the bound and without, so "the bound is necessary" is a +measured claim rather than an assertion. These are the concrete forgeries §3, §4 +and §5 refer to: + +| 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, and an `end` row emits no memory operations. A silently truncated copy. | +| `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 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, which is also why an earlier draft of this audit wrote +the forgery at `count = 3` and was wrong — it is not reachable there. + +## 9. Gate results + +Verbatim from `python3 z3_dma_verify.py` (full board, no `--quick`), 2026-08-11, +z3 5.0.0 — **pasted, not retyped**. An earlier draft hand-condensed this block +while the document argued that a gate nobody can rerun is a claim rather than +evidence; a retyped transcript is the wrong shape for that argument. + +``` +============================================================================ +DMA memcpy chip -- z3 gate +============================================================================ + 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 5410 honest 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_gate_transcription.py. + + OVERALL: PASS +``` + +### What is and isn't proven + +**Proven.** Given the modelled contracts (`IsHalfword`, `Zero` including its +domain, `Alu[LT]` as `lt.rs`'s own constraints, the `DmaNext` per-limb binding of +§7) and assumptions A1–A4, and given that bus balance means multiset equality: +every satisfying assignment of one DMA 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; every one of the **ten** range checks and lookups involved is individually +necessary, each with a named forgery; Layer 2's own 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`. + +**Not proven.** Assumptions A1–A4 (§Assumptions) — the head row's limb +canonicality and the timestamp bound, all of which are caller obligations the +spec states and no chip discharges locally. The memory consistency argument and +therefore overlap ordering for unaligned 8-byte accesses. LogUp soundness. The +multi-call case (Layer 2 models one head row). And that the *Rust* implements this +design — that is `../audit_gate_transcription.py`'s 100 textual claims plus the +PR's own end-to-end prove/verify and forgery tests. diff --git a/docs/verification/dma/dma-chip/IMPLEMENTATION.md b/docs/verification/dma/dma-chip/IMPLEMENTATION.md new file mode 100644 index 000000000..e3b9b7b04 --- /dev/null +++ b/docs/verification/dma/dma-chip/IMPLEMENTATION.md @@ -0,0 +1,150 @@ +# DMA memcpy chip — implementation notes + +Companion to `DESIGN.md`: what the shipped Rust does, where the verification +artifacts touch it, and what is still open. The order of events here is the +reverse of the BLAKE3 campaign's — the Rust (PR #874) came first and this +directory was added on top (PR: `feat/dma-memcpy-formal-verification`), so this +file records **what was verified about existing code**, not deltas from a design. + +## What ships in PR #874 + +| piece | file | +|---|---| +| the ecall | `executor/src/vm/instruction/execution.rs`, `SyscallNumbers::DmaMemcpy` | +| the table | `prover/src/tables/dma.rs` (32 columns, 18 constraints, 23 bus interactions) | +| the trace replay | `prover/src/tables/trace_builder.rs`, `collect_dma_memcpy_ops` | +| the no-overflow template | `prover/src/constraints/templates.rs`, `emit_add_pair_no_overflow` | +| the guest stub | `syscalls/src/syscalls.rs`, the strong `memcpy` symbol | + +Syscall number `u64::MAX - 2`; ABI `memcpy(dst = x10, src = x11, n = x12)` with +`n ≤ 256`; `FIXED_TABLE_COUNT` **11 → 12** (PR #876's hint table landed on +`main` in between, so the 10 → 11 in #874's own PR body is now stale). + +## What this branch adds + +| piece | file | +|---|---| +| the reference model (four levels) | `../dma-oracle/dma_ref.py` | +| the validation harness (five anchors) | `../dma-oracle/test_oracle.py` | +| 10 pinned vectors with full column expansions | `../dma-oracle/canonical_dma_vectors.json` | +| the recovered specification + soundness ledger | `DESIGN.md` | +| the z3 gate | `z3_dma_verify.py` | +| the transcription audit (100 claims) | `../audit_gate_transcription.py` | +| the audit's findings and residuals | `../TRANSCRIPTION-AUDIT.md` | +| two Rust tests driving the real decomposition | `prover/src/tests/dma_tests.rs` | +| a `#[cfg(test)]` accessor for that decomposition | `prover/src/tables/trace_builder.rs` | +| a `verify-dma` target | `Makefile` | + +No change to any shipped constraint, column, bus interaction or executor path. +The only non-test Rust is a `#[cfg(test)]` function in `trace_builder.rs`, which +compiles out of the library entirely; it exists because the row decomposition and +its `MemoryState`/`RegisterState` operands are module-private, and testing the +public `generate_dma_trace` instead is what made the first version of these tests +vacuous (that function only formats an already-decomposed op list into columns). +The file already used this pattern for `epoch_touched_cells`. + +## Gates run + +**Oracle → external anchors.** `python3 ../dma-oracle/test_oracle.py`, full: +3855 cases against libc `memmove`, 3855 against CPython slice assignment, the +row-level/byte-level replay equivalence over all 257 lengths × 15 overlap +configurations, chunking over 1100 lengths, and a 6-mutant sensitivity sweep. +`VALIDATED`. + +**Gate → the design.** `python3 z3_dma_verify.py`, full board, z3 5.0.0, ~96 s: +six Layer-1 checks UNSAT, six Layer-2 chain checks UNSAT (four integer, two +field-exact) plus four positive and three negative Layer-2 controls, 10/10 +premise controls SAT, 6/6 width-audit rows as expected, and a completeness sweep +of 5153 honest rows + 257 padding rows over every length `0..256`. +`OVERALL: PASS`. Verbatim transcript in `DESIGN.md` §9. + +The solver is **not** pinned, and that is a real caveat: the queries are +version-independent in meaning, but older solvers are far slower on the +field-exact chain (`CHAIN-F 2` measured 0.45 s on 5.0.0 against 7.60 s on 4.12.2, +17×), so on 4.12.2 the whole board takes ~1210 s and two queries blow their +budgets and report `unknown`. **`unknown` is scored as failure everywhere, never +as success**, so an old solver produces a false alarm and never a false proof — +and the gate now prints its solver version, warns when it is older than the +validated one, and prints a legend saying `unknown` means a timeout rather than a +soundness problem. + +**Audit → the Rust.** `python3 ../audit_gate_transcription.py`: **100 claims, 0 +findings**, per-section counts printed by the script rather than documented by +hand. Mutation-tested against six source mutants, all six caught — including the +one that matters most, `num_bus_elements(DWordHL) 2 → 1`, whose absence from the +audit is what let the retracted R1 through. Two of the six needed the check +strengthened before they were caught (`../TRANSCRIPTION-AUDIT.md` §1). Source is +whitespace-normalised before literal matching, so a `rustfmt` reflow no longer +produces a spurious finding, and the audit no longer imports the solver (~80 of +its claims need no z3). + +**Rust → the oracle.** `cargo test -p lambda-vm-prover --lib dma`: 18 tests +pass, including the two new ones +(`dma_trace_matches_oracle_row_decomposition` over seven pinned structural cases, +and `dma_maximum_chunk_is_thirty_three_rows_with_no_tail`). + +## The retracted finding + +An earlier version of this campaign reported "RESIDUAL R1" — that `count`'s limb +split was unconstrained on non-head rows — and made it the headline result across +five documents. **It does not exist.** `DmaNext` binds each 64-bit value as two +32-bit bus elements with separate alpha powers, not as one packed field element, +so the limbs are pinned by the predecessor's `IsHalfword`-checked halfwords. The +gate's weaker model manufactured an alias the real bus rejects. Full account and +the transferable lessons: `DESIGN.md` §7. + +What it cost, beyond the retraction: working around the phantom led to asserting +`count ≤ 256` on *every* row of the field-exact chain check when the AIR bounds +only the head — a genuine over-strong assumption, which is the direction that +yields false proofs. Both are fixed; the bound is now derived from the head row +through the limb-wise link, as MAIN 3 proves. + +## Premises the gate assumes and this campaign does not discharge + +These are **caller obligations the spec states**, not checks the receiver +performs — `spec/src/memw.toml` and `spec/src/memw_register.toml` both carry them +as `[[assumptions]] IS_WORD[...]`. An earlier draft of `DESIGN.md` had the +direction backwards and invented the labels "MEMW-ADDR32"/"REG-32" for them; +they are now A1–A4 in `DESIGN.md` §Assumptions. + +They bind the **head row only** — every other row's limbs are derived through the +`DmaNext` link. The gate's `drop_reg32` control shows what A2 buys: without it, +`Alu[count, 257, LT] → 1` caps only a residue class, not the count. + +None is DMA-specific; every table that sends an address, a register value or a +timestamp leans on them, and `IS_WORD` has no named discharger anywhere in the +spec. That argues for settling it once, centrally. + +## Known limits of the verification, restated plainly + +* The gate cannot see bus **wiring**, timestamps, or LogUp soundness. The first is + covered by the audit script's §D and §G, the second partly by the oracle's + `write_before_read`/`interleaved` mutants. §G is new, and its absence is what + let the retracted R1 through. +* The chain checks run at depth ≤ 5 (integer) and ≤ 3 (field-exact), and prove + the tiling **among groups containing exactly one head row**. `ChainRow` carries + no timestamp, so the multi-call case is out of model rather than covered; the + `ts` in both `DmaNext` tuples is what separates two calls, and it is guarded + textually by the audit. The general depth case rests on MAIN 2's wrap lemma plus + the strict decrease of `count`. +* **Nobody has checked the `Memw` ordering argument for unaligned 8-byte + accesses**, which is what a misaligned DMA copy generates on nearly every row. + That is the largest remaining gap around this feature and it is not DMA's to + fix. `../TRANSCRIPTION-AUDIT.md` §7 item 1. +* `DESIGN.md` was recovered from the implementation, so it cannot independently + disagree with it. The independent notion of "correct" is the oracle's, and the + audit script is what keeps the three artifacts pinned together. + +## Reproducing + +```sh +pip install z3-solver # validated on 5.0.0 +python3 docs/verification/dma/dma-oracle/test_oracle.py # anchors, emits the vectors +python3 docs/verification/dma/dma-chip/z3_dma_verify.py # the gate (--quick to shorten) +python3 docs/verification/dma/audit_gate_transcription.py # 83 transcription claims +cargo test -p lambda-vm-prover --lib dma # the Rust side +``` + +`make verify-dma` runs all three. Each exits nonzero on failure; the oracle exits +**2** when it ran but an anchor skipped, so a degraded run is distinguishable from +a clean one. No CI workflow schedules them yet — that is a separate call. diff --git a/docs/verification/dma/dma-chip/z3_dma_verify.py b/docs/verification/dma/dma-chip/z3_dma_verify.py new file mode 100644 index 000000000..75124f194 --- /dev/null +++ b/docs/verification/dma/dma-chip/z3_dma_verify.py @@ -0,0 +1,1045 @@ +""" +Formal (z3) assume-guarantee gate for the DMA memcpy chip (PR #874). + +Method (mirrors blake3-chip/z3_blake_verify.py from PR #903, branch feat/blake3-accelerator): + * 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. They are toggles, every +negative control shows what breaks without them, and ../TRANSCRIPTION-AUDIT.md +records where each is discharged. + +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_gate_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_dma_verify.py # the full board + python3 z3_dma_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_gate_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_gate_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.join(os.path.dirname(os.path.abspath(__file__)), + "..", "dma-oracle")) + 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) + if solve(r.C + _pins(r, ref.row_columns(row))) != sat: + return False, f"n={n} row {index}: the AIR REJECTS an honest row" + checked += 1 + r = FieldRow(f"pad{n}", prem) + if solve(r.C + _pins(r, ref.padding_columns())) != sat: + return False, f"n={n}: the AIR REJECTS the padding row" + checked += 1 + return True, f"{checked} honest rows 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_gate_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() + 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() + 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) + print(f" {'PASS' if sweep_ok else 'FAIL'} {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_gate_transcription.py.", flush=True) + ok = (layer1_ok and layer2_ok and layer2_controls_ok and controls_ok + and audit_ok and sweep_ok) + 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/docs/verification/dma/dma-oracle/ORACLE.md b/docs/verification/dma/dma-oracle/ORACLE.md new file mode 100644 index 000000000..1912fc798 --- /dev/null +++ b/docs/verification/dma/dma-oracle/ORACLE.md @@ -0,0 +1,227 @@ +# DMA memcpy oracle + +Independent reference model for the DMA memcpy ecall, and the record of what it +is anchored on. + +## 1. Validation status: **VALIDATED** + +Run 2026-08-11, `python3 test_oracle.py` (full, no `--quick`): + +``` +[1] libc memmove PASS 3855 cases x overlap/alignment +[2] CPython slice assignment PASS 3855 cases x overlap/alignment +[3] row/bus level <-> byte level PASS 257 lengths x 15 overlaps +[4] guest stub chunking PASS 1100 lengths +[5] mutation sweep PASS all 8 mutants caught +VALIDATION STATUS: VALIDATED + emitted 10 canonical vectors -> canonical_dma_vectors.json + canonical_dma_rows.txt +``` + +Anchors 1 and 2 are **genuinely non-circular**: the platform C library and +CPython's `bytearray` slice assignment are two implementations of `memmove` that +share no code with `dma_ref.py` and no code with each other. libc in particular +is the definition the guest's `compiler_builtins` `memcpy` was replacing, which +is what makes it the right anchor for this campaign rather than a convenient one. + +Anchor 3 is the one the chip depends on, and it 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 is what makes 1–4 worth running. + +The harness reports what actually ran, in three ways: a missing dependency SKIPs +only its own anchor and never cascades; the banner names the anchors it is *not* +anchored on; and **the status token itself carries any reduction** +(`PARTIALLY VALIDATED (1 anchor(s) skipped)`, `VALIDATED (--quick, reduced +sweeps)`) with a distinct **exit code 2**, because a CI job or a human greps for +the word "VALIDATED" and a degraded run must not print it bare. + +The cascade guard is not just the `None` case: `find_library` returning a path does +not mean it loads — it can hand back a GNU ld linker script, an arch-mismatched +ldconfig hit, or a path that has since gone. An uncaught `OSError` there used to +kill the run before anchors 2–5 and before any banner printed. + +## 2. The four levels + +`dma_ref.py` deliberately writes each level as its own function rather than +sharing a helper, so they can be checked against each other. + +### 2.1 Byte level — `memcpy_ref(memory, dst, src, n)` + +The C `memmove` contract on a sparse byte-addressed memory. Snapshot the whole +source, then write. Unwritten memory reads as zero, matching the VM. + +Preconditions, in the executor's own order (`validate`): + +``` +n > 256 -> reject (DmaMemcpyChunkTooLarge) +dst + n >= 2^64 -> reject (AddressOverflow) +src + n >= 2^64 -> reject (AddressOverflow) +``` + +The order matters: an oversized call that would *also* wrap reports the chunk +error, and the audit script asserts the Rust rejects in that order too. + +### 2.2 Row level — `row_widths(n)`, `row_decomposition(...)` + +```python +widths, remaining = [], n +while remaining != 0: + width = 8 if remaining >= 8 else 1 + widths.append(width) + remaining -= width +``` + +Written as the greedy loop, **not** as the closed form +`[8]*(n//8) + [1]*(n%8)`, because the AIR decides one row at a time from the +remaining count (`tail = count < 8`). That the closed form agrees is a property +anchor 3 checks (`(d)`), not an assumption the model makes. + +`row_decomposition` adds the two flag columns and one terminal row: + +| | `src` | `dst` | `count` | `first` | `end` | +|---|---|---|---|---|---| +| data row k | `src + Σw 256` | `Alu[count, 257, LT] → 1`, multiplicity `first` | +| `validate`'s wrap checks | `emit_add_pair_no_overflow` on `src` and `dst` | +| `row_widths`' `remaining >= 8` | `Alu[count, 8, LT] → tail`, multiplicity `mu` | +| `width` | `step = 8 − 7·tail` | +| row k → row k+1 | `DmaNext` send `[ts, src_incr, dst_incr, count_decr]` / receive `[ts, src, dst, count]` | +| terminal row | `Zero[4·65535 − Σ count_decr] → end` | +| snapshot ordering | the AIR constants `T+1` (reads) and `T+2` (writes) | +| "the same bytes" | one set of `value` columns feeding both `Memw` tuples | +| zero-padded `value` | `tail · value[i] = 0`, `i = 1..7` | + +## 4. Canonical vectors + +`canonical_dma_vectors.json`, regenerated by the harness. Ten cases chosen so +every structural case appears exactly once: + +| 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: `n = 7` is seven one-byte rows plus a +terminal, eight rows to move seven bytes. "maximum chunk" is the only case with +**no tail row at all**, which is why it is pinned — 256 is 8-aligned, so +`n % 8 = 0` and the last data row is a wide one. + +Each vector carries its full row-and-column expansion under `rows[i].columns` +(generated by `dma_ref.row_columns`), which is what the z3 gate's completeness +sweep pins. + +The Rust side consumes the companion **`canonical_dma_rows.txt`**, emitted next to +the JSON: one `|`-separated record per line, so `include_str!` plus `split('|')` is +the whole parser. That file exists because the prover crate has no JSON parser and +a hand-rolled scanner over nested JSON is exactly the fragile coupling that goes +stale silently — the first attempt broke on `rows[i].columns` repeating the +`src`/`dst`/`count` keys. Embedding it means a regenerated oracle is a +compile-time input to `cargo test`, not a note; an earlier version hand-transcribed +7 of the 10 vectors into Rust literals with nothing enforcing the transcription. + +## 5. Mutation sweep (anchor 5) + +Every mutant must be caught by the anchor it targets. All six are: + +| mutant | caught by | +|---|---| +| `memcpy_ref` without snapshot | **anchor 1** (libc), at `n=7 delta=1` | +| `memcpy_ref` without snapshot | **anchor 2** (CPython), at `n=8 delta=1` | +| `row_widths` = all ones | anchor 3(d): disagrees with the closed form | +| `row_widths` = always wide | anchor 3: widths do not sum to `n` | +| `row_widths` tail off by one (`>` for `>=`) | anchor 3(d) | +| MEMW write before read | anchor 3(a) via `replay_memw`, **only on the overlapping deltas** | +| MEMW reads/writes interleaved per chunk | anchor 3(a), same | +| `chunk_ecalls` at 257 | anchor 4: a chunk exceeds the executor's bound | + +The two timestamp mutants are the reason `DELTAS` includes `0, ±1, ±7, ±8, ±9` +and not only disjoint ranges: on non-overlapping buffers, reading after writing +is indistinguishable from reading before. + +The first two mutants exist because **anchors 1 and 2 originally had no control at +all** — every mutant targeted `row_widths`/`memw_ops`/`chunk_ecalls`, i.e. anchors +3 and 4, so nothing demonstrated that the two external differentials could fail. +`memcpy_ref` is reached through the module rather than an injection point, so +those two mutants swap it via `_with_memcpy_ref` instead. + +## 6. Open questions and known limitations + +**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. Those are the memory argument's own obligations. + +**O2 — the per-ecall snapshot is not a `memcpy`-level `memmove`.** Chunk *k+1* +reads memory chunk *k* already wrote, so `guest_memcpy` is a forward copy. For +`dst < src` and for non-overlapping ranges it agrees with `memmove`; for +`dst > src` with an overlap wider than 256 bytes it does not. In contract for +`memcpy`, and 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, which is outside both the oracle and the +gate; the audit script checks the wiring. + +**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 plus the vector test in +`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. They are not part of the copy semantics, +but they are part of the trace, and the audit script is the only thing looking at +them. + +## 7. File manifest + +| file | what it is | +|---|---| +| `dma_ref.py` | the four-level reference model | +| `test_oracle.py` | five-anchor validation harness; emits both vector files | +| `canonical_dma_vectors.json` | 10 pinned vectors with full column expansions (the gate's input) | +| `canonical_dma_rows.txt` | the same vectors, line-oriented (the Rust test's input) | +| `ORACLE.md` | this file | diff --git a/docs/verification/dma/dma-oracle/canonical_dma_rows.txt b/docs/verification/dma/dma-oracle/canonical_dma_rows.txt new file mode 100644 index 000000000..38c9980b5 --- /dev/null +++ b/docs/verification/dma/dma-oracle/canonical_dma_rows.txt @@ -0,0 +1,70 @@ +# Generated by test_oracle.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/docs/verification/dma/dma-oracle/canonical_dma_vectors.json b/docs/verification/dma/dma-oracle/canonical_dma_vectors.json new file mode 100644 index 000000000..e24063db0 --- /dev/null +++ b/docs/verification/dma/dma-oracle/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/docs/verification/dma/dma-oracle/dma_ref.py b/docs/verification/dma/dma-oracle/dma_ref.py new file mode 100644 index 000000000..bd46aecf2 --- /dev/null +++ b/docs/verification/dma/dma-oracle/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_oracle.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_oracle.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/docs/verification/dma/dma-oracle/test_oracle.py b/docs/verification/dma/dma-oracle/test_oracle.py new file mode 100644 index 000000000..de0e308c7 --- /dev/null +++ b/docs/verification/dma/dma-oracle/test_oracle.py @@ -0,0 +1,513 @@ +""" +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_oracle.py # run everything, emit the vectors + python3 test_oracle.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" + + +# --------------------------------------------------------------------------- +# [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 = [] + for name, run in mutants: + try: + ok, _ = run() + except (AssertionError, ref.DmaRejected): + ok = False # replay_memw or the executor bound caught it + if ok: + survivors.append(name) + print(f" mutant {name:32s} -> {'SURVIVED (bad)' if ok else 'caught'}") + if survivors: + return False, f"{len(survivors)} mutant(s) survived: {', '.join(survivors)}" + return True, f"all {len(mutants)} mutants caught" + + +# --------------------------------------------------------------------------- +# 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_oracle.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 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] mutation sweep", 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/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..f2d065697 100644 --- a/prover/src/tests/dma_tests.rs +++ b/prover/src/tests/dma_tests.rs @@ -130,6 +130,239 @@ 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. +/// +/// `docs/verification/dma/dma-oracle/test_oracle.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!("../../../docs/verification/dma/dma-oracle/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(); + 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), + }); + } + "row" => { + assert_eq!(f.len(), 6, "canonical rows: bad row line {line:?}"); + let vector = vectors + .last_mut() + .expect("canonical rows: a row line preceded every 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. + for vector in &vectors { + assert_eq!( + vector.rows.len() as u64, + vector.rows.iter().map(|_| 1u64).sum::(), + "{}: row bookkeeping", + vector.name + ); + } + 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"); + + 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); + 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: three register reads at T, then every source read + // strictly before every destination write. This two-phase split is what + // gives an overlapping copy its snapshot semantics, and no other test in + // this module looks at it. + 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), + "{}: register reads are at T", + 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 = data.iter().filter(|o| o.timestamp == 0x31).count(); + let writes = data.iter().filter(|o| o.timestamp == 0x32).count(); + assert_eq!( + (reads, writes), + (vector.rows.len(), vector.rows.len()), + "{}: all reads at T+1 and all writes at T+2", + vector.name + ); + } +} + +/// 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 +/// `ops.len() == 33` against a locally computed `count / 8 + 1` would hold even +/// if `DMA_MEMCPY_MAX_BYTES` changed, so the expectation is derived from the +/// executor's own row formula instead. +#[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;