diff --git a/docs/verification/ecsm-affine/.gitignore b/docs/verification/ecsm-affine/.gitignore new file mode 100644 index 000000000..b2ed13ae8 --- /dev/null +++ b/docs/verification/ecsm-affine/.gitignore @@ -0,0 +1,10 @@ +# Local venv for z3/sympy/ecdsa — recreate with: +# python3 -m venv .venv && ./.venv/bin/pip install z3-solver sympy ecdsa +.venv/ + +# Rust harness build output +harness/target/ +harness/Cargo.lock + +__pycache__/ +*.pyc diff --git a/docs/verification/ecsm-affine/README.md b/docs/verification/ecsm-affine/README.md new file mode 100644 index 000000000..941841501 --- /dev/null +++ b/docs/verification/ecsm-affine/README.md @@ -0,0 +1,178 @@ +# ECSM affine selector — oracle + z3-proved soundness gate + +Formal-verification campaign for **PR #879** (`perf/ecsm-affine-selector`), which adds an +affine variant of the ECSM ecall: input `xG‖yG` (64 B), output `xR‖yR` (64 B), with an +`IS_AFFINE` selector column so one prover serves both ABIs. + +Same shape as the two earlier campaigns — an independent Python model of the function, +anchored against third parties, plus a z3/sympy gate over the constraints, plus a +transcription audit of the gate against the Rust: + +- `thoughts/blake3/` on branch `feat/blake3-accelerator` (PR #903) — the gate-then-implement + pattern this follows, and the source of the "audit the transcription" lesson. +- `thoughts/ec-recover-opt/` on branch `feat/ec-lincomb2` — the ORIGINAL ECSM/ECDAS board. + **This campaign imports its lemmas rather than repeating them.** + +Neither of those paths exists on `main`: `thoughts/` is gitignored, and both campaigns live +only on their own unmerged branches. Citations to them name the branch and commit for that +reason. + +### Why this lives in `docs/verification/`, not `thoughts/` + +`thoughts/` is gitignored deliberately. `d83b4d9e` (PR #863, 2026-07-31) added it to +`.gitignore` under the comment *"Profiling outputs … and working notes"* and in the same +commit **deleted** the two files that had leaked in +(`thoughts/gpu-constraint-eval/{impl-plan-single-source-constraints,survey-constraint-frontends}.md`); +its sub-commit subjects are "chore: keep working notes out of the tree" and "…gitignore +reports/, and untrack the working notes". Nothing under `thoughts/` is tracked on `main` +today — verify with `git ls-tree -r --name-only origin/main -- thoughts/` (0 files). + +PR #903 force-adds back into `thoughts/` and argues the case in its own README, but #903 is +still open, so that is one unmerged PR relitigating a merged decision rather than precedent. +`docs/` is tracked, and the directory name says what these files are — which is the stronger +form of #903's own argument anyway, since these are runnable gates with exit codes, not notes. + +## Status + +**Board fully green.** See [`gate/RESULTS.md`](gate/RESULTS.md) for the lemma table and the +soundness theorem. + +``` +audit: 19/19 premises read from source, 19/19 mutation controls bite, 0 failures +oracle: ORACLE STATUS: VALIDATED (9 pass, 0 skip, 0 fail) +anchor: 32 real witnesses from ecsm::compute_witness{,_with_y}, every field re-derived +A1 selector : IS_BIT + µ-gating PROVED, Ecall pinning PROVED, 3 forgery controls +A2 YrLtP : lift + strict chain PROVED, forgery instantiated on a real y = 1 point +A3 parity : forgery instantiated (2 full witnesses), the yG read PROVED to close it +A4 addressing : LT bound == executor's predicate PROVED, u64-wrap control FORGES +``` + +Seven distinct attacks (11 `SAT` results; several are exhibited from more than one +angle). **Every new check in PR #879 has a control showing it is +load-bearing** — the `yG` read, `YrLtP`, `IS_AFFINE`'s bit constraint and its µ-gate, the +`Alu` LT senders and the `u128` widening each admit a concrete attack when removed. + +## What is being verified, and what is imported + +PR #879 does not change the double-and-add chain, the curve relations, or the ECDAS buses. +Those were taken to a green board by the earlier EC campaign, whose **L1–L7 and contracts +C1–C7 are hypotheses here**. What is new, and what this board covers: + +| Added by the PR | Lemma | +|---|---| +| the `IS_AFFINE` column, `IS_BIT` (idx 421) and `AffineZeroOnPadding` (idx 422) | A1a, A1b, A1e | +| the `Ecall` receiver's `xonly + IS_AFFINE·(affine − xonly)` syscall words | A1c | +| the `IS_AFFINE`-gated `yG` read (4 dwords at `addr_xG + 32 + 8i`, `ts`) | A3 | +| the `IS_AFFINE`-gated `yR` write (4 dwords at `addr_xR + 32 + 8i`, `ts+3`) | A3c, A4f | +| `OverflowKind::YrLtP` — the `yR < p` chain (idx 413..420) + 16 halfword columns | A2 | +| the `Alu` LT address-limb senders and their mode-dependent bound | A4 | +| the executor's 64-byte spans and `u128` overlap guard | A4e | + +Two of the imported lemmas are stressed in a way their own statements did not anticipate, so +they are **re-examined rather than imported blind**: + +- **L7** concluded `xR = x(k·P)` "for both `yG` sign classes", *because* the parity was + unobservable. Publishing `yR` retires that premise — A3 is the whole subject. +- **C4** listed `YR` as inheriting byte-ness "from tuple equality with ECDAS's byte-checked + `yR` (or `YG` for k=1)". `YrLtP` now *consumes* that, so it is written down as **C4-YR** and + its provenance checked (A2d, audit P17) instead of used silently. + +## The two findings a reader should not skip + +**The `y = 1` point.** The PR's soundness section argues the `YrLtP` band is populated +("constructible: `3 | p−1` makes cubing 3-to-1"). Checked, and it understates the case — the +*first* candidate works. There is a real secp256k1 point with `y = 1`: + +``` +x = 0x1fe1e5ef3fceb5c135ab7741333ce5a6e80d68167653f6b2b24bcbcfaaaff507, y = 1 +``` + +so the attack instance sits at the very bottom of a `2^32 + 977`-wide band, and `crypto/ecsm` +itself returns `y_r = 1` for it. `gate/a2_yr_lt_p.py` carries the `yR + p` / `q2 − 1` forgery +all the way through the ECDAS `Yr` relation *and its carry window* — a forgery its windows +reject is not a forgery. + +**The parity gap is instantiated, not argued.** `gate/a3_parity_binding.py` builds two +complete witnesses over the same `(xG, k)` — one per root of `xG³ + b` — evaluates the entire +in-table constraint set on each, and shows both are valid with the same `xR` and different +`yR`. `gate/a6_real_witness.py` then reproduces the same pair 9 times straight out of +`ecsm::compute_witness_with_y`, so the gap does not depend on the model being right. + +## Contents + +| path | what it is | +|---|---| +| `oracle/ecsm_affine_ref.py` | independent secp256k1 + the two ecall semantics + the ABI predicates. No `k256`, no repo code | +| `oracle/test_oracle.py` | 9 independent anchors; a missing fixture SKIPs only itself | +| `oracle/small_y_point.py` | constructs the `y = 1` attack instance via cube roots mod `p` | +| `oracle/small_y_point.json` | the instance, consumed by A2 | +| `gate/affine_common.py` | the transcribed model of the new AIR surface, with citations | +| `gate/a1_selector.py` | A1 — `IS_AFFINE` is a bit, dead on padding, and pinned | +| `gate/a2_yr_lt_p.py` | A2 — `YrLtP`: lift, strict chain, width, C4-YR, the forgery | +| `gate/a3_parity_binding.py` | A3 — the parity forgery and the read that closes it | +| `gate/a4_addressing.py` | A4 — address bounds, the `+32…+63` span, the overlap guard | +| `gate/a6_real_witness.py` | the real-witness (column) anchor | +| `gate/audit_transcription.py` | A5 — 19 premises read from source + mutation controls | +| `gate/RESULTS.md` | lemma board, soundness theorem, contracts, findings, method notes | +| `gate/TRANSCRIPTION-AUDIT.md` | the audit's prose half: premise table and what it cannot see | +| `gate/logs/` | run logs, and the real-witness dump | +| `harness/` | tiny Rust binary dumping real `EcsmWitness` values as JSON | +| `run_gate.sh` | runs everything in dependency order | + +## Running it + +```bash +python3 -m venv .venv && ./.venv/bin/pip install z3-solver sympy ecdsa +./run_gate.sh # everything, logs to gate/logs/ +./run_gate.sh --quick # reuse the witness dump, skip the cargo build +``` + +A few seconds plus one `cargo build`. The harness depends only on `crypto/ecsm`, deliberately: +a harness that needs the whole prover does not get run. Without a `.venv` the runner falls +back to `python3` from `PATH`. + +Committing is a plain `git add docs/verification/ecsm-affine` — no `-f`, no pathspecs. That +is the practical reason this directory is not under `thoughts/`: `-f` would be required +there, and **`-f` overrides the nested `.gitignore` too**, so it stages `.venv/` and +`harness/target/` as well (5108 files instead of 28). Outside an ignored parent, the nested +`.gitignore` below does its job: + +``` +$ git add -nf thoughts/camp -> .gitignore, .venv/junk, gate.py, harness/target/junk.o +$ git add -n docs/camp -> .gitignore, gate.py +``` + +So **keep `.gitignore`** — it is what excludes the venv and the build output. Sanity-check +before committing: + +```bash +git add -n docs/verification/ecsm-affine | wc -l # ~28, not 5108 +``` + +`ecdsa` is optional — without it the oracle reports `PARTIALLY VALIDATED` and **names the +anchor it is not anchored on**, rather than printing a green banner that outlives its evidence. +(That banner defect is one BLAKE3's harness shipped with; see `thoughts/blake3/README.md` +"Harness defects", on branch `feat/blake3-accelerator`.) + +## Method notes worth knowing before extending this + +- **`x·(1−x) ≡ 0 (mod p_g)` is not a z3 query.** In lifted integer form with a free quotient + it does not terminate at this modulus, and neither does 160-bit bit-blasting. These are + root-of-a-polynomial-over-a-field statements, discharged by factoring over `GF(q)` and + checking the split is **complete**. z3 keeps the bounded/linear work: the carry lifts, + the predicate-equivalence sweeps, the quantified interval statement. +- **Two fields, and it matters.** The AIR is over `GF(p_g)`; the curve is over `GF(p)`. + `field_roots` takes the modulus explicitly because an early A3a factored the curve + polynomial over Goldilocks and correctly reported FAIL. +- **Every control was seen to go red.** Two of them started out vacuous — A2c recomputed its + witness for the perturbed constant (so any constant passed), and audit premise P18 matched a + *comment* about the timestamp stride rather than the stride. Both are written up in + RESULTS.md Findings 5–6. A green control is worth nothing until you have watched it fail. + +## What this gate cannot see + +Bus wiring and lookup coverage — the same boundary both earlier gates recorded about +themselves. A1c's pinning, A3c's "at most one witness matches the caller's buffer", and C4-YR +all reduce to contract C5 (LogUp balance) plus the imported L6. An arithmetic gate cannot +catch a mis-wired receiver; the e2e `prove + verify` tests in `prover/src/tests/ecsm_tests.rs` +and `prove_elfs_tests.rs` are what cover that, and they are green on this branch. diff --git a/docs/verification/ecsm-affine/gate/RESULTS.md b/docs/verification/ecsm-affine/gate/RESULTS.md new file mode 100644 index 000000000..a4a67bdf7 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/RESULTS.md @@ -0,0 +1,394 @@ +# ECSM affine-selector z3 gate — lemma board & soundness theorem + +Reverse-order verification of the surface **PR #879** adds to `prover/src/tables/ecsm.rs` +and `executor/src/vm/instruction/execution.rs`, following the playbook of the two earlier +campaigns in this tree: + +- `thoughts/ec-recover-opt/gate/RESULTS.md` on branch `feat/ec-lincomb2`, commit `1d2b4dd7` + — the ORIGINAL ECSM/ECDAS board. Its lemmas L1–L7 and contracts C1–C7 are **imported as + hypotheses** here; this board does not re-derive them. +- `thoughts/blake3/` on branch `feat/blake3-accelerator` (PR #903) — the gate-then-implement + pattern, and its postmortem on which pass is worth doing (the transcription audit). + +Both paths are under the gitignored `thoughts/` and exist only on those unmerged branches, not +on `main`; this campaign lives in `docs/verification/` instead (rationale in `../README.md`). + +Model transcribed from the Rust with `file:line` citations inline in the scripts; independent +reference = `../oracle/ecsm_affine_ref.py`, a from-scratch secp256k1 implementation (no +`k256`, no `num_bigint`, no repo code). + +**Faithfulness anchors, both green, both run before any UNSAT was read:** + +1. **Function** — `../oracle/test_oracle.py`: 9/9 anchors, `ORACLE STATUS: VALIDATED`. + Repo constants parsed and matched, 5 published multiples of `G`, 216 x-only-agreement + pairs, 200 root-dependence instances, the executor's 8 rejections, the ABI predicates over + 193 offsets, 60 ecrecover-equivalence instances, 25 vectors against the PyPI `ecdsa` + package. +2. **Columns** — `a6_real_witness.py` over 32 witnesses emitted by the repo's own + `ecsm::compute_witness{,_with_y}` (`../harness/`): every field the model reads is + re-derived, including all four overflow chains, both convolution relations and their carry + windows. + +--- + +## Board + +| Lemma | Statement | Verdict | Notes | +|---|---|---|---| +| **A1-PRIME** | `p_g = 2^64 − 2^32 + 1` is prime | CERTIFIED (sympy) | the one assumed algebraic fact; the field property every root argument uses | +| **A1a** | `IS_BIT(IS_AFFINE)` (idx 421) ⇒ `IS_AFFINE ∈ {0,1}` | PROVED (complete split over GF(p_g)) | root set `{0,1}`, factorisation complete ⇒ exhaustive | +| **A1b** | `AffineZeroOnPadding` (idx 422) ⇒ `µ=0` forces `IS_AFFINE=0` | PROVED (z3 UNSAT) | what lets the `yG`/`yR` buses use `Multiplicity::Column(IS_AFFINE)` with no separate padding argument | +| **A1c** | the `Ecall` tuple is **injective** in `IS_AFFINE` | PROVED | the pinning: a row flipping the selector no longer matches the CPU's real `a7` | +| **A1c-ctl** | the degenerate syscall pair un-pins the selector; the repo pair does not | PROVED + 1 SAT | identical numbers ⇒ constant tuple ⇒ `IS_AFFINE` free | +| **A1c-assert** | today's pinning rests **entirely** on the LOW word | PROVED | high word separates nothing (shared `0xFFFF_FFFF`) ⇒ `execution.rs`'s `const _:` assert is load-bearing, not decorative | +| **A1d** | both new constraints are degree 2; `max_degree() == 3` still holds | PROVED | `YrLtP` reuses the existing degree-3 shape | +| **A1f** | **drop idx 421** | **SAT — FORGES** | the row's `Ecall` tuple can be made **another accelerator's**: `IS_AFFINE = 20` → HINT, `IS_AFFINE = p_g − 9` → KECCAK. `IS_BIT` is the only thing confining it to `{0,1}`. **LOAD-BEARING — and not for the reason its comment gives** | +| **A1e** | **drop idx 422** | **SAT — FORGES** | all 423 constraints walked: idx 422 is the ONLY one violated when kept, all 422 remaining are satisfied when dropped, honest padding satisfies all 423 — and the dropped row then fires 8 `IS_AFFINE`-gated MEMW ops. **LOAD-BEARING** | +| **A2a** | `YrLtP` word-carry lift: field recurrence ⇒ integer equation | PROVED (z3 UNSAT) | `\|A_i\| < 2^33 ≪ p_g`, so no `p_g` wrap | +| **A2b** | `OverflowRequired(YrLtP)` ⇒ `yR < p` | PROVED (z3 UNSAT) | `p` pinned as a numeral, not a free constant — so the conclusion is `yR < p`, not `yR < const` | +| **A2b-nv** | the same system without the denial is SAT | SAT (expected) | non-vacuity: `yR = p−1` is reachable | +| **A2c** | every `YrLtP` LHS integer value ≪ p_g under the contracts | PROVED (exact corners) | `max \|A_i\| = 2^33 − 1 = 4.7·10⁻¹⁰·p_g` | +| **A2c-ctl** | wrong constant `p → p+2` / `p → N` | **SAT — CATCHES** | with the witness held FIXED, the honest columns stop satisfying the chain ⇒ it binds `p` itself (keccak wrong-RC analogue) | +| **A2d** | contract **C4-YR**: where `YR`'s byte bound comes from | CONTRACT | `ecsm.rs` byte-checks `{X2, Q0, YG, Q1}` — **not** `YR`. Inherited via two exhaustive cases on `len_k`; bus-level, so outside this gate (C5 + imported L6) | +| **A2d-obs** | `YrLtP` is **µ**-gated, not `IS_AFFINE`-gated | NOTED | binds x-only rows too: strictly stronger, and completeness holds because `witness.rs` fills `y_r_sub_p` on both paths | +| **A2e** | honest-witness anchor for the chain | PROVED | 14 witnesses (4 x-only, 10 affine): every `c_i ∈ {0,1}`, `c_7 = 1`, halfwords in `[0,2^16)` | +| **A2f** | **the forgery, fully instantiated** | **SAT — FORGES** | see below | +| **A2g** | **drop `YrLtP`** | **SAT — FORGES** | the A2f witness is accepted; the guest receives `yR + p`. **LOAD-BEARING** (the `yR`-side analogue of the earlier board's N6 / `XR_SUB_P`) | +| **A2h** | the excluded band is populated by real curve points | PROVED | `2^256 − p = 2^32 + 977`, and a real secp256k1 point has **`y = 1`** | +| **A3a** | `yG`'s parity is arithmetically FREE | PROVED (complete split over GF(p)) | `Y² − (x³+b) = (Y−y)(Y+y)`; both roots distinct at all 6 tested x (no `y=0` point) | +| **A3b** | **the parity forgery, fully instantiated** | **SAT — FORGES** | two complete witnesses over the same `(xG, k)`, both satisfying all 423 in-table constraints, same `xR`, different `yR`. Swept over 12 random `(P, k)` | +| **A3c** | the `yG` read pins `YG` bit-for-bit | PROVED | 4 dwords × 8 bytes ↔ `addr_xG + [32, 64)`, order-preserving, each column covered exactly once | +| **A3d** | **drop the `yG` read** | **SAT — FORGES** | the two A3b witnesses become indistinguishable. The read is the **only** thing pinning input parity. **LOAD-BEARING** | +| **A3e** | the imported **L7** conclusion survives verbatim | PROVED | `x(k·P) = x(k·(−P))` over 20 instances ⇒ x-only rows may still leave parity free | +| **A3f** | `YrLtP` is **not** a parity defence | PROVED | both `±yR` are canonical ⇒ two orthogonal gaps, two fixes; do not conflate them | +| **A4a** | the `Alu` LT bound **==** the executor's `addr_limb_ok`, both modes | PROVED (z3 UNSAT ×2) | same accept set ⇒ no provable-but-halting execution, no legal execution made unprovable | +| **A4b** | the affine `+32 + 8i` span cannot cross `2^32` | PROVED (z3 UNSAT) | 128 touched byte offsets, max `+63`, all `< 2^32` under the bound ⇒ reusing the high limb is safe | +| **A4c** | the **seven-value band** the LT senders close | PROVED | exactly 7 per mode: `[2^32−31, 2^32−24)` and `[2^32−63, 2^32−56)`. The PR comment's number, measured | +| **A4d** | `k`'s bound is flat in both modes, correctly | PROVED (z3 UNSAT) | `k` is 32 B on both arms | +| **A4e** | the overlap guard **==** exact interval disjointness | PROVED (z3 UNSAT) | not a distance bound: `addr_k + 32 == addr_xg` is legal and must stay legal | +| **A4e-ctl** | **the `u64` wrap** | **SAT — FORGES** | `addr_xg = 2^64 − 64` passes `addr_limb_ok(·, 63)` and wraps the pre-fix `+64`, slipping a **total** operand overlap past the guard. The `u128` widening is **LOAD-BEARING** | +| **A4f** | timestamp layout is collision-free | PROVED | `{xG, yG}@ts`, `k@ts+1`, `xR@ts+2`, `yR@ts+3`, stride 4 (parsed from the builder). `xG`/`yG` share `ts` but are address-disjoint | +| **A4g** | the mode-dependent bound is necessary in **both** directions | PROVED | a flat 64-byte bound rejects 32 legal x-only addresses (completeness); a flat 32-byte bound admits 32 illegal affine ones (soundness) | +| **A5** | transcription audit | 19/19 premises READ, 19/19 mutations bite | `TRANSCRIPTION-AUDIT.md` | +| **A6** | real-witness anchor | PROVED (+1 forgery exhibit) | 32 witnesses from `crypto/ecsm` itself; 9 ±yG pairs reproduce A3b outside the model | + +Non-vacuity: **seven distinct attacks** — A1c-ctl, A1e, A1f, A2c-ctl, A2f/A2g, A3b/A3d, +A4e-ctl. They surface as **11 `SAT` results** across the lemma files, because several are +exhibited from more than one angle (the parity attack appears as A3b's instance, A3b's +12-instance sweep, A3d's counterfactual, and again as A6c straight out of `crypto/ecsm`). Every new check in the PR now has a control showing it is load-bearing; +none is dead weight. A1f was **missing from the first version of this board** — idx 421 was +proved *correct* (A1a) but never shown *necessary*, and "every new check is load-bearing" was +asserted on five of the six. See Finding 7. + +--- + +## A2f — the `yR + p` forgery, carried all the way through + +The PR's soundness section claims the excluded band is populated: "such points are +constructible: `3 | p−1` makes cubing 3-to-1, so a small target `y` has a cube-root preimage +about a third of the time". `../oracle/small_y_point.py` builds the point, and the claim is +not just true but extreme — **the first candidate, `y = 1`, works**: + +``` +y = 1 +x = 0x1fe1e5ef3fceb5c135ab7741333ce5a6e80d68167653f6b2b24bcbcfaaaff507 (on curve) +y + p = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc30 < 2^256 +``` + +Reached through the chip's generic path as `2·(2^{−1}·Q)` (`k = 2`, one ECDAS doubling row — +not the `k = 1` echo). The forged witness publishes `yR' = yR + p` and compensates with +`q2' = q2 − 1`; the relation's residual is `−p·1 + p·1 = 0`. A2f checks **12** facts about it, +including the two that a value-level argument would skip: + +- the forged ECDAS `Yr` relation holds **exactly** — all 64 limb divisions are exact and the + chain closes at `c_63 = 0`; +- the forged **carries stay inside** the `IsHalfword` window `[−16320, 49216)`. + +A forgery its carry windows reject is not a forgery, which is why those two are in the list. +`crypto/ecsm` itself returns `y_r = 1` for this instance (A6e), so nothing here depends on the +model being right about the arithmetic. + +--- + +## A3 — the parity gap, and why it is new + +The chip constrains `yG` only through `yG² ≡ xG³ + b (mod p)`. Both roots satisfy it, and the +earlier board says so in as many words: L7 concludes `xR = x(k·P)` **"for both yG sign +classes"**, *because* `x(k·P) = x(k·(−P))`. That was a fine conclusion for an x-only ABI. + +Publishing `yR` retires the premise, not the lemma. A witness may take `−yG`, compute a +perfectly correct multiple of a **different** point, and hand the guest its `y`: + +- the AIR cannot tell — an on-curve check passes for either root; +- the guest cannot tell — knowing the parity of `k·P` is precisely the work it delegated. + +A3b builds both witnesses out of real values and evaluates the whole in-table constraint set +on each. Note which columns move: `x2` and `q0` depend on `xG` alone and are **identical**; +`q1` differs, because the `Yg` relation's numerator uses the *integer* `yG²` and +`(p−y)² ≠ y²` over ℤ. So the forged witness needs its own quotient — and it fits its 33-byte +contract, and the `c1` carries still fit the `+16319` window. A6c reproduces the same pair +straight out of `ecsm::compute_witness_with_y`, 9 times. + +The fix is the `IS_AFFINE`-gated MEMW read, and A3c checks the thing that would quietly break +it: **coverage**. The forgery needs only one byte of freedom, so a read covering 31 of the 32 +bytes would close nothing. It covers all 32, exactly once, order-preserving. + +**A3f is a trap worth stating explicitly:** `YrLtP` is *not* a second line of defence here. +Both `±yR` are canonical field elements, so the range check admits either. Two orthogonal +gaps — input parity (A3) and output representation (A2) — with two independent fixes. + +--- + +## Soundness theorem (what this board adds) + +Under contracts C1–C7 (imported) + C4-YR + A1-PRIME, and given the earlier board's L1–L7, any +accepted trace satisfies, for every ECSM row with `µ = 1` and ecall timestamp `ts`: + +> `IS_AFFINE` equals the mode of the ecall the CPU actually executed. When it is 0, the row's +> behaviour is **bit-identical** to the pre-PR chip and the imported conclusion stands +> unchanged: `xR = x(k·P)` for either lift of `xG`. When it is 1, the witnessed `yG` is the +> 32 bytes the caller placed at `addr_xG + 32`, so `(xG, yG)` is the caller's own point; the +> published `(xR, yR)` are the canonical affine coordinates of `k·(xG, yG)`, both `< p`; and +> the operand addresses are exactly those the executor accepts. + +Chain of proof: `IS_AFFINE` is a bit (A1a), dead on padding (A1b) and pinned to the executed +ecall (A1c) → the affine buses fire exactly on affine rows → the `yG` read pins the input +point (A3c), closing the parity freedom A3a/A3b exhibits → the imported L1–L7 give +`(xR, yR) ≡ k·(xG, yG) (mod p)` → `XR_SUB_P` and the new `YrLtP` (A2a/A2b) make both +coordinates canonical → the LT senders align the AIR's address set with the VM's (A4a–A4c) and +the `+32 … +63` span cannot leave its limb (A4b). + +**Completeness** (no honest rejection): A2e and A6a — real witnesses from `crypto/ecsm` +satisfy every new constraint, including on the x-only path where `YrLtP` also binds (A2d-obs); +A4g shows the mode-dependent bound is what keeps legal x-only addresses provable. + +--- + +## Contracts (assume-guarantee boundary) + +Imported verbatim from the earlier board: **C1** AreBytes, **C2** IsHalfword, **C3** +IS_BIT/booleans, **C4** MEMW byte authority, **C5** LogUp multiset soundness, **C6** Ecall +binding, **C7** timestamp uniqueness, **A-PRIME** (`p`, `N` prime). + +New, and the one this board had to look up rather than assume: + +- **C4-YR** — `YR`'s bytes are in `[0, 256)`. `ecsm.rs` does **not** emit this: its `is_byte` + list is `{X2, Q0, YG, Q1}`. The bound is inherited by two exhaustive cases on `len_k`: + `len_k ≥ 1` ⇒ the `Ecdas` drain tuple equals an ECDAS sender's byte-checked `yR`; + `len_k = 0` (`k = 1`) ⇒ no ECDAS row can receive round `−1`, so balance forces + drain = seed, i.e. `YR = YG`, which *is* byte-checked here. Both cases are bus-level (C5 + + imported L6) and therefore **invisible to this gate** — which is why C4-YR is written down + instead of being quietly used. +- **A1-PRIME** — `p_g` prime (sympy-certified). + +--- + +## Findings + +1. **[confirmed claim] The `y = 1` point.** The PR's constructibility argument for the + `YrLtP` band is correct, and stronger than stated: the smallest possible `y` is attained, + so the attack instance sits at the very bottom of a `2^32 + 977`-wide band. No action — + recorded because "astronomically rare" was the phrasing used for the `XR_SUB_P` analogue + on the earlier board (Finding 5), and it is not rare here in any useful sense. +2. **[confirmed claim] The seven-value address band.** `ecsm.rs`'s comment claims the LT + senders close "a seven-value band per operand". Measured: exactly 7, in both modes + (A4c). No action. +3. **[observation, no action] `YrLtP` is µ-gated, not `IS_AFFINE`-gated.** So it binds on + x-only rows, where nothing observes `yR`. Strictly stronger ⇒ sound, and completeness + holds because `compute_witness_inner` fills `y_r_sub_p` on both paths. Gating it on + `IS_AFFINE` would save 16 halfword sends + 8 constraints on x-only rows; not worth the + asymmetry with the other three chains. Recorded so it reads as a choice rather than an + oversight. +4. **[the pinning is narrower than it looks] `IS_AFFINE` is separated by ONE 32-bit word.** + The two syscall numbers share their high word, so that word's `IS_AFFINE` coefficient is + zero and carries no mode information (A1c-assert). The entire pinning is the low word, and + `execution.rs:53-58`'s `const _: () = assert!` is what keeps it that way. The assert is + *conservative* — it also rejects a pair differing only in the high word, which would in + fact still be injective — and that is the right side to err on. No action; the audit's P5 + fails if the assert is removed. +5. **[audit method] A blind check is worse than a missing one.** P18 (timestamp stride) + originally matched `ecsm.rs`'s *comment* about the stride and compared it against a + hard-coded 4 in the model. It passed. The mutation control then showed it survived + reducing the real stride to 3 — i.e. it was checking documentation. Now it parses the + stride out of `trace_builder.rs` and compares the parsed value. **Every premise here is + mutation-tested for exactly this reason.** +6. **[control hygiene] The wrong-constant control was initially vacuous.** A2c's first form + recomputed the witness addend for the perturbed constant, so *any* constant passed. Fixed + by holding the witness fixed — the prover commits its columns against the real `p`, and + that is what the control must model. Both this and Finding 5 are the same lesson: a green + control is worth nothing until you have seen it go red. + +## The rule those two findings generalise to + +> **Every negative control must be PAIRED with the specific check that the dropped premise is +> load-bearing for — and the pairing must be evaluated in both directions.** + +A control that drops a premise and then re-runs a check whose reference never mentioned that +premise *cannot fail*, and reads green. Findings 5 and 6 are both instances; a parallel +campaign on the DMA memcpy PR (#874) hit the identical shape three times +(`drop_tail_lane_zero`, `drop_lt_bound`, `drop_reg32`), which is enough independent recurrence +to write the rule down rather than the anecdotes. + +Concretely, each control here states both halves: + +| Control | half 1: premise KEPT must block | half 2: premise DROPPED must admit | +|---|---|---| +| A1e | idx 422 is the only violated constraint of 423 | all 422 remaining satisfied, 8 MEMW ops fire | +| A2c-ctl | honest witness (addend fixed) valid under `p` | rejected under `p+2` and under `N` | +| A2g | A2f established every *other* constraint holds | the witness is accepted, guest gets `yR + p` | +| A3d | A3c: the read's tuples differ between the two | `check_all_constraints` clean on both | +| A4e-ctl | the `u128` form rejects the overlap | `addr_limb_ok` passes *and* the `u64` form accepts | +| A1c-ctl | the repo pair is injective | the degenerate pair collides | +| A1f | idx 421 kept ⇒ only ECSM/ECSM_AFFINE reachable | dropped ⇒ HINT and KECCAK reachable | + +**The rule paid for itself twice.** A1f's first implementation had an inverted sign in its +modular solve, so it found no foreign syscalls. Half 2 alone would have reported +"idx 421 REDUNDANT" — a confident, wrong conclusion. Half 1 (`idx 421 kept ⇒ exactly +`{ECSM, ECSM_AFFINE}` reachable`) failed instead, which is what surfaced the bug. + +A1e originally listed "the constraint families I believe remain" rather than walking the index +map. That is the mirror-image hazard — an over-permissive control reports a false FORGES by +forgetting a constraint that would have blocked the state — so it now enumerates all 423 and +asserts the count. + +--- + +7. **[the board's own gap, now closed] `IS_BIT(IS_AFFINE)` is load-bearing for a reason + nobody had written down.** The first version of this board proved idx 421 *correct* (A1a) + and never asked whether it was *necessary*. It is, and the argument is not local to the + ECSM pair at all. + + The receiver's syscall words are `xonly + a·(affine − xonly)` per 32-bit word, and for the + repo's numbers the coefficients are `−1` (low) and **`0`** (high, since both share + `0xFFFF_FFFF`). So as `a` sweeps the field the high word is CONSTANT and the low word + sweeps everything — and every syscall is `u64::MAX − k`, so they all share that high word. + Each is therefore reachable at `a = (target_lo − xonly_lo)/(−1)`: + + | reached tuple | `IS_AFFINE` | + |---|---| + | `ECSM` | 0 (honest) | + | `ECSM_AFFINE` | 1 (honest) | + | **`HINT`** | **20** | + | **`KECCAK`** | **p_g − 9** | + + Drop idx 421 and `a` is free on a `µ=1` row (idx 422 only binds at `µ=0`), so an ECSM row + can consume the `Ecall` send of a *different* accelerator: the guest's HINT call gets + proven as a scalar multiplication that writes 32 or 64 bytes wherever the ECSM row's + register columns point. + + **What does not close this:** `execution.rs`'s `const _: () = assert!` compares only the + two ECSM numbers' low words. It cannot see a *third* syscall sitting an integer offset + away — which is the reachable case. That is a documentation gap in #879, not a bug: idx 421 + is present and does the job. Recorded as a review note below. + +## Method notes + +- **`x·(1−x) ≡ 0 (mod p_g)` is not a z3 query.** Handed to z3 in lifted integer form + (`x(1−x) = m·p_g`, `m` free) it does not terminate at this modulus — nonlinear integer + arithmetic with an unbounded quotient. Bit-blasting it (160-bit `URem`) does not terminate + either. These are **root-of-a-polynomial-over-a-field** statements, and they are discharged + as such: sympy factors over `GF(q)` and the split is checked **complete** (linear factors + account for the full degree), so the returned root set is provably exhaustive. z3 is kept + for what it is good at here — the bounded/linear lifts (A2a, A2b), the predicate-equivalence + sweeps (A4a, A4d) and the quantified interval statement (A4e). +- **Two different fields.** The AIR is enforced over `GF(p_g)`; the curve lives over `GF(p)`. + `field_roots` takes the modulus explicitly because an early version of A3a factored the + curve polynomial over Goldilocks and correctly reported FAIL. +- **Forgeries are constructive.** Where a control is a genuine forgery it is exhibited as + fixed numerals evaluated against the transcribed constraints — the solver is never asked + whether an attack *might* exist. +- **Never negate an equation that carries a witness quotient.** The lifts here put the free + quotient on the *hypothesis* side and deny a quotient-free conclusion: A2a asserts + `A − 2^32·c == m·PG` and denies `A != 2^32·c`; A1b asserts `a − m·PG == 0` and denies + `a != 0`. That direction is sound, because extra freedom in `m` only strengthens the + adversary. The inverse is a trap that produces a **bogus SAT**: `Not(a − b == k·m)` is + satisfiable by picking `k != 0`, so the solver "refutes" a true statement. Under negation the + claim has to be spelled out witness-free — an explicit residue variable bounded to `[0, p)`, + or a two-way disjunction. Audited: every z3 query on this board asserts its quotient + equations positively, and no denial contains a quotient variable (A2b, A4a, A4d and A4e carry + no quotients at all). +- **The tractable rewrite, where it applies.** Keeping `Int` (not `BitVec`) and rewriting + `a ≡ b (mod m)` as `a − b == k·m` with a fresh free `k` is linear whenever `m` is a constant, + which is why A2a/A2b are milliseconds. Rewriting `x·(1−x) == 0` as `Or(x == 0, x == 1)` is + the same trick one level up and is used throughout the downstream lemmas (A2b's carry bits, + A1e's padding row). It is **not** available for A1a itself — there the disjunction *is* the + conclusion, so assuming it would be circular, and the field-factorisation argument is what + earns it. + +--- + +## Reproduction + +From `docs/verification/ecsm-affine/`: + +```bash +python3 -m venv .venv && ./.venv/bin/pip install z3-solver sympy ecdsa +./run_gate.sh # everything, logs to gate/logs/ +./run_gate.sh --quick # reuse the existing witness dump (skip the cargo build) +``` + +`run_gate.sh` cds to its own directory, so it also works from the repo root as +`docs/verification/ecsm-affine/run_gate.sh`. The two scripts that read repo source locate the +root by marker (a workspace `Cargo.toml` next to `prover/`), not by a hard-coded `parents[N]` +— see the note under "Where to send the next reviewer". + +Individual stages, in the order the board depends on them: + +```bash +cd gate && python audit_transcription.py # A5 — premises still true of the code? +cd oracle && python test_oracle.py # the function anchor +cd oracle && python small_y_point.py # builds the y = 1 attack instance +cd harness && cargo run --release -- > ../gate/logs/real_witnesses.jsonl +cd gate && python a6_real_witness.py # the column anchor +cd gate && python a1_selector.py # A1 +cd gate && python a2_yr_lt_p.py # A2 +cd gate && python a3_parity_binding.py # A3 +cd gate && python a4_addressing.py # A4 +``` + +Total runtime is a few seconds plus the `cargo build` (the harness depends only on +`crypto/ecsm`, deliberately — a harness that needs the prover does not get run). + +--- + +## Where to send the next reviewer + +- **Bus-level reasoning is outside this gate**, as it was outside both earlier ones. C4-YR, + the `Ecall` pinning's LogUp step (A1c reduces to it), and A3c's "at most one witness matches + the caller's buffer" all bottom out in C5 + the imported L6. A gate that models the + arithmetic cannot see a mis-wired bus; the e2e `prove + verify` tests in + `prover/src/tests/ecsm_tests.rs` and `prove_elfs_tests.rs` are what cover that, and they are + green on this branch. +- **The `q1` growth on the `−yG` branch** is checked to fit 33 bytes at the instances tested, + not proved to fit for all inputs. It is a completeness question about a witness nobody + should be building, so it is deliberately left as an observation — but if the affine path + ever *needs* both roots, it becomes a real bound to establish. +- **Nothing here re-proves the double-and-add chain.** If PR #879's rebase ever touches the + ECDAS chain or the `Ecdas`/`Bit` buses, the imported board is the one to re-run, not this + one. + +## Spec gap — a review note on #879, deliberately NOT fixed here + +`spec/` carries one `.typ` chapter per table (34 of them: add, bitwise, commit, keccak, lt, +memw, mul, page, sha256, shift, store, …). **There is no ECSM chapter, under any name.** No +`ecsm`/`ecdas` file, no `spec/src/ecsm.toml`, and +`grep -rlin "ecsm|scalar mul|secp256" spec/*.typ spec/src/*.toml` returns nothing. +(`spec/signatures.typ` is a meta-chapter that renders bus/template signatures — unrelated to +ECDSA.) + +Worse, `prover/src/tables/ecsm.rs:19` says **"See `spec/src/ecsm.toml`"** — a file that does +not exist and never has. That is a dangling reference in the very file #879 modifies. + +Both are **pre-existing** and not #879's to create: PR #903 added `spec/blake3.typ` because it +introduced a *new* table, whereas #879 extends an existing one whose chapter was never written. +Writing the missing chapter inside a verification PR would also mean a `spec/book.typ` edit — +a shared merge-conflict surface — for a gap that predates the branch. Raise it as a separate +review note on #879 and a follow-up issue instead. (The parallel DMA campaign found the same +class of gap on #874, which *does* add a new fixed table — `FIXED_TABLE_COUNT` 10 → 11 — with +no `spec/dma.typ`; that one is arguably blocking, this one is not.) + +For the same reason nothing is added to `docs/SUMMARY.md`: there is no `book.toml` anywhere in +the repo, no workflow or Makefile target references mdbook, and `SUMMARY.md` already omits 7 +existing `docs/` files (`ai-review.md` plus 6 under `cryptography/`). So an unindexed file +breaks nothing, while a new top-level heading would put an internal verification campaign into +a user-facing TOC and widen the diff into a shared conflict surface. diff --git a/docs/verification/ecsm-affine/gate/TRANSCRIPTION-AUDIT.md b/docs/verification/ecsm-affine/gate/TRANSCRIPTION-AUDIT.md new file mode 100644 index 000000000..edc748da1 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/TRANSCRIPTION-AUDIT.md @@ -0,0 +1,111 @@ +# Transcription audit — does the gate's model match the code it models? + +Executable half: [`audit_transcription.py`](audit_transcription.py). Log: +[`logs/audit_transcription.log`](logs/audit_transcription.log). + +## Why this file exists + +Both earlier campaigns in this tree converged on the same conclusion about where the residual +risk sits after a green board. + +`thoughts/blake3/README.md` (branch `feat/blake3-accelerator`), "Still unaudited — where to +send the next reviewer": + +> Two independent reviews established that **the oracle defines the right function**, so the +> gate's UNSATs are about the right function. They did *not* audit the step after that: +> **nobody has checked the z3 gate's transcription of the oracle into constraints.** […] The +> dangerous direction is a model **stronger** than the thing it models — it yields UNSAT where +> the real object is forgeable, and a positive anchor cannot catch it, because honest inputs +> satisfy a correct model and an over-strong one equally well. + +And it points at the EC campaign as the reason to take it seriously: the equivalent audit +there (`thoughts/ec-recover-opt/gate/TRANSCRIPTION-AUDIT.md`, branch `feat/ec-lincomb2`) +"found three premises the gate +asserted about the chip and never read, one of them hiding a working forgery". + +So every premise the A1–A4 lemmas rely on is enumerated here as a `Premise` and **read out of +the source**, not re-derived from memory. + +## The two kinds of premise + +**assumed** — the model relies on something being true of the code. Failing one invalidates +whatever lemma consumes it. + +**negative-space** — the model relies on something being **absent**. These are the dangerous +ones, because a reader checking the diff sees only what *is* written. Two of them here, and +both carry real weight: + +- **P16 — nothing constrains `yG`'s parity.** This is A3's central premise. If any constraint + did pin the parity, A3b's forgery would be blocked by it and A3d's "the `yG` read is + load-bearing" verdict would be *wrong* — the gate would be claiming a fix is necessary when + something else already covered it. Checked by enumerating **every** appearance of `cols::YG` + in `ecsm.rs` (there are 7) and confirming each is one of five known parity-blind uses: the + trace fill, the affine MEMW read (the fix itself), the `AreBytes` range check, the + `Ecdas` seed/drain tuples, and the `Yg` relation's `yG²` term. A *new* appearance fails the + audit, which is the point. +- **P17 — `YR` is not byte-checked in `ecsm.rs`.** This is contract C4-YR. `YrLtP` reads + `YR`'s 32 columns as bytes, but the local `is_byte` list is `{X2, Q0, YG, Q1}`. So the byte + bound is *inherited* through the `Ecdas` bus rather than emitted, and the gate is consuming + a contract it must not silently assume. If a future commit adds `is_byte(cols::YR, 32, …)` + the situation improves — and the audit should still notice, because RESULTS.md's contract + list would then be stale. + +## Mutation testing — a blind check is worse than a missing one + +Every premise is perturbed: the source is mutated in memory and the premise's check must then +**fail**. A check that passes on mutated source is checking nothing, and reads as green. + +This is not hypothetical. **P18 (instruction timestamp stride) shipped blind in its first +form.** It matched `ecsm.rs`'s comment — + +``` +// ts + 3 is the free 4th sub-timestamp (instruction stride is 4; xG@T, k@T+1, xR@T+2 …) +``` + +— and compared it against a hard-coded `4` in the model. It passed. The mutation control then +reduced the *real* stride in `trace_builder.rs` from 4 to 3, and the premise still passed: it +was checking documentation, not behaviour. It now parses the stride out of +`let timestamp = (i as u64) * 4 + 4;` and compares the **parsed** value, and the mutant is +caught. + +Current state: **19/19 premises read from source, 19/19 mutations bite, 0 failures.** + +## The premise table + +| # | Lemma | Premise | Source | Mutation control | +|---|---|---|---|---| +| P1 | A1/A2 | `MU=666, IS_AFFINE=667, YR_SUB_P=668..684, NUM_COLUMNS=684` — and `YR_SUB_P + 16 == NUM_COLUMNS`, so the new halfwords fit exactly with no overlap | `ecsm.rs` `mod cols` | `NUM_COLUMNS → 683` | +| P2 | A1 | `debug_assert_eq!(idx, 423)`, and the header index map documents `413..420` / `421` / `422` | `ecsm.rs` | `idx → 421` | +| P3 | A4 | `ADDR_LIMB_BOUND_32B = 2^32−31`, `..._64B = 2^32−63` | `ecsm.rs:43,47` | `64B → 2^32−64` | +| P4 | A1c | `ECSM_SYSCALL_NUMBER = u64::MAX−10`, affine `= u64::MAX−11` | `execution.rs:38,47` | affine `→ u64::MAX−12` | +| P5 | A1c | the low-32-bit-word inequality is a **compile-time** assert | `execution.rs:53-58` | assert renamed away | +| P6 | A1c | the received syscall words are `xonly + IS_AFFINE·(affine − xonly)`, per word | `ecsm.rs` `syscall_word` | `coefficient: affine - xonly → 0` | +| P7 | A1/A3 | 2 `IS_AFFINE`-gated bus blocks of 4 dwords, offsets `+32 + 8i`, `yG` via `memw_read` at `ts`, `yR` via `memw_write` at `ts+3` | `ecsm.rs` | offset `+32` dropped | +| P8 | A2 | `YrLtP → (P_BYTES, YR_SUB_P, YR)`, byte-stored sum (only `KLtN` is bit-stored) | `ecsm.rs` `OverflowKind` | sum column `YR → XR` | +| P9 | A2d | all four chains share ONE `µ`-gated loop; `IS_AFFINE` does not appear inside it | `ecsm.rs` `eval` | carry bits re-gated on `IS_AFFINE` | +| P10 | A2 | 16 `µ`-gated `IsHalfword` sends on `yr_sub_p(i)` | `ecsm.rs` | sends aimed at `xr_sub_p` | +| P11 | A4 | 3 `Alu` LT senders: `xG`/`xR` vs `addr_bound_by_mode()`, `k` vs the flat bound, `LT`/result 1 | `ecsm.rs` | `xR`'s sender deleted | +| P12 | A4 | executor arm: spans `63/63/31`, the `u128` overlap guard, `yG` read at `+32`, `yR` stored at `+32` | `execution.rs` | `u128 → u64` (the pre-fix wrapping form) | +| P13 | A2e | `y_r_sub_p = (2^256 + yR − p)`, computed in the shared `compute_witness_inner` used by BOTH entry points | `witness.rs` | addend built from `x` instead of `y` | +| P14 | A3 | `CARRY_OFFSET_X2 = 8160`, `CARRY_OFFSET_YG = 16319` | `ecsm.rs:37,38` | `YG → 16320` | +| P15 | A2a | `INV_SHIFT_32 = 18446744065119617026 = 2^{−32} mod p_g` | `templates.rs:26` | last digit perturbed | +| **P16** | **A3** | **negative space:** every `cols::YG` use is parity-blind | `ecsm.rs`, all 7 sites | an unrecognised `cols::YG` use appears | +| **P17** | **A2d** | **negative space:** `YR` is not in `ecsm.rs`'s `is_byte` list ⇒ C4-YR is inherited | `ecsm.rs` | `YR` gains a local byte check | +| **P19** | **A1f** | **the COMPLETE syscall set** — every `u64::MAX − k` the `Ecall` bus can carry, parsed from source. A1f's conclusion is about which foreign syscalls the linear syscall word reaches, so a fifth syscall changes the answer | `execution.rs` | `HINT` renumbered `MAX-30 → MAX-40` | +| P18 | A4f | one instruction consumes 4 sub-timestamps; ECSM uses offsets `{0,1,2,3}`, max `== stride−1` | `trace_builder.rs:348`, `ecsm.rs` `ts_lo_plus` | stride `4 → 3` | + +## What the audit does NOT cover + +- **Bus wiring and lookup coverage.** Same limitation both earlier gates recorded about + themselves (`thoughts/blake3/blake3-chip/DESIGN.md` §7 items 4/5/11, branch + `feat/blake3-accelerator`). P7/P10/P11 check that + the interactions are *emitted with the shape the model assumes*; they cannot check that the + MEMW/AreBytes/IsHalfword **receivers** interpret those tuples the way the model believes. + That is contracts C1/C2/C5 plus the e2e prove+verify tests. +- **The verifier's column-width pinning.** `NUM_COLUMNS` growing 667 → 684 is a proof-format + change. P1 reads the constant; whether the verifier's per-table width check tracks it is + `main`'s `#909` territory, not this campaign's. +- **Regex fragility.** These checks are textual. A refactor that preserves behaviour but + changes formatting will fail a premise — a false alarm, but a loud and cheap one, which is + the right failure direction for an audit. Every failure message names the premise and prints + what it found. diff --git a/docs/verification/ecsm-affine/gate/a1_selector.py b/docs/verification/ecsm-affine/gate/a1_selector.py new file mode 100644 index 000000000..680a24ce1 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/a1_selector.py @@ -0,0 +1,409 @@ +"""A1 — the `IS_AFFINE` selector: is it a bit, is it dead on padding, and is it PINNED? + +`IS_AFFINE` is the only thing standing between the two ABIs. Everything the affine path +adds keys off it: the `yG` read, the `yR` write, and the address bound. So the question the +whole board reduces to is whether a prover can choose it freely. + + A1a `IS_AFFINE ∈ {0,1}` — idx 421 does what it says + A1b `IS_AFFINE = 0` whenever `µ = 0` — idx 422; padding cannot fire the + affine buses + A1c the `Ecall` tuple is INJECTIVE in IS_AFFINE — the pinning. Two rows with the same + `ts` but different modes produce + different bus tuples, so LogUp cannot + match a flipped selector against the + CPU's real `a7`. + A1d degree bookkeeping — both new constraints are degree 2, so + `max_degree() == 3` still holds. + A1f IS_BIT(IS_AFFINE) is load-bearing — and not for the reason its comment gives: + without it the row can impersonate a + DIFFERENT accelerator's ecall. + A1e µ-gating is NOT vacuous — with idx 422 dropped, a padding row + can set `IS_AFFINE = 1` and satisfy all + 422 remaining constraints, and then + fires 8 affine-gated MEMW ops. Paired: + idx 422 KEPT must block that state. + +A1c is where the interesting failure lives, and it is a failure of *arithmetic*, not of +wiring: the receiver puts `xonly + IS_AFFINE·(affine − xonly)` on the bus PER 32-BIT WORD. +If the two syscall numbers agreed in their low word and differed only in the high one, the +low word's coefficient would be zero — and since the high word is where they'd differ, that +one would carry the information. The dangerous case is when they agree in the word that is +checked and differ nowhere else: then every coefficient is zero, the tuple is constant, and +`IS_AFFINE` is free. Today's numbers differ in the LOW word only (`2^32−11` vs `2^32−12`) +and share the high word, so the pinning rests entirely on the low word. `execution.rs` +guards this with a `const _: () = assert!`; A1c proves the guard is the right guard by +showing the degenerate choice it forbids really does un-pin the selector. + +Run: `python a1_selector.py` +""" + +import sys +import time +from pathlib import Path + +import z3 + +sys.path.insert(0, str(Path(__file__).parent)) +from affine_common import ( # noqa: E402 + AFFINE_YG_READ_OFFSETS, + AFFINE_YR_WRITE_OFFSETS, + ECSM_AFFINE_SYSCALL_NUMBER, + ECSM_SYSCALL_NUMBER, + PG, + SYSCALL_NUMBERS, + certify_pg_prime, + field_roots, + s_ecsm_x2, + s_ecsm_yg, + syscall_word_hi, + syscall_word_lo, +) + +results = [] + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:8}] {name} {detail}") + + +def _unsat(solver, name, detail=""): + t0 = time.time() + r = solver.check() + v = "PROVED" if r == z3.unsat else ("SAT" if r == z3.sat else str(r).upper()) + report(name, v, f"{detail} {time.time()-t0:.2f}s".strip()) + return r + + +# ── A1a: IS_AFFINE is a bit ───────────────────────────────────────────────── + +def a1_prime(): + ok = certify_pg_prime() + report("A1-PRIME p_g = 2^64 − 2^32 + 1 is prime", + "CERTIFIED" if ok else "FAIL", + "sympy.isprime; the field property every root argument below rests on") + return ok + + +def a1a_is_bit(): + """`a·(1−a) ≡ 0 (mod p_g)` ⇒ `a ∈ {0,1}`. + + Not a tautology: over a ring with zero divisors the product could vanish at other + points, so the claim needs `p_g` to be a field. Discharged by factoring `a − a²` over + GF(p_g) and checking the split is COMPLETE — a degree-2 polynomial over a field has at + most two roots, so an exhaustive linear factorisation is a proof that `{0, 1}` is the + whole root set. + + Method note: the lifted integer form `a(1−a) = m·p_g` handed to z3 does not terminate + at this modulus (nonlinear integer arithmetic, free quotient). Recorded in RESULTS.md.""" + roots, complete = field_roots([-1, 1, 0]) # −a² + a + ok = complete and set(roots) == {0, 1} + report("A1a IS_BIT(IS_AFFINE) ⇒ a ∈ {0,1}", "PROVED" if ok else "FAIL", + f"idx 421; roots over GF(p_g) = {sorted(roots)}, split complete: {complete}") + + +# ── A1b: dead on padding ──────────────────────────────────────────────────── + +def a1b_padding(): + """Both selector constraints together: `µ ∈ {0,1}` (idx 0, by the same root argument) + and `a·(1−µ) ≡ 0` (idx 422) force `a = 0` on padding rows. This is what lets the + `yG`/`yR` buses use `Multiplicity::Column(IS_AFFINE)` without a separate padding + argument. + + On a padding row `µ = 0` substitutes into idx 422 to give `a·1 ≡ 0`, which is LINEAR — + so this half is a z3 query rather than a factorisation.""" + mu_roots, mu_complete = field_roots([-1, 1, 0]) + ok = mu_complete and set(mu_roots) == {0, 1} + s = z3.Solver() + a, m = z3.Ints("a m") + s.add(a >= 0, a < PG) + s.add(a * 1 - m * PG == 0) # idx 422 at µ = 0, lifted: a ≡ 0 (mod p_g) + s.add(a != 0) # deny the conclusion + r = _unsat(s, "A1b AffineZeroOnPadding ⇒ µ=0 forces IS_AFFINE=0", + f"idx 422 at µ=0; IS_BIT(MU) roots {sorted(mu_roots)};") + if not ok: + report("A1b IS_BIT(MU) root split", "FAIL", "incomplete factorisation") + return r == z3.unsat and ok + + +# ── A1c: the Ecall pinning ───────────────────────────────────────────────── + +def a1c_pinning(xonly=ECSM_SYSCALL_NUMBER, affine=ECSM_AFFINE_SYSCALL_NUMBER, + label="repo numbers", expect_proved=True): + """The receiver's two syscall words, as functions of `IS_AFFINE`, must SEPARATE the + two modes: `(lo(0), hi(0)) ≠ (lo(1), hi(1))`. + + Why that is the pinning. The `Ecall` bus is a LogUp argument: the CPU sends the tuple + `[ts_lo, ts_hi, a7_lo, a7_hi]` built from the register the guest actually loaded, and + the ECSM row receives `[ts_lo, ts_hi, syscall_word_lo(a), syscall_word_hi(a)]`. Balance + is per-tuple, so a row that flips `a` while the CPU's `a7` stays put changes its own + received tuple and no longer matches any send. Injectivity of `a ↦ (lo, hi)` is + therefore exactly the statement "the selector is determined by the executed ecall". + + Both words are modelled mod p_g, because that is where the fingerprint lives — a pair + that differs over ℤ but collides mod p_g would NOT pin the selector. (Both words are + < 2^32 ≪ p_g here, so no collision, but the model should not assume it.)""" + lo0, lo1 = syscall_word_lo(0), syscall_word_lo(1) + hi0, hi1 = syscall_word_hi(0), syscall_word_hi(1) + if (xonly, affine) != (ECSM_SYSCALL_NUMBER, ECSM_AFFINE_SYSCALL_NUMBER): + lo_x, lo_a = xonly & 0xFFFF_FFFF, affine & 0xFFFF_FFFF + hi_x, hi_a = xonly >> 32, affine >> 32 + lo0, lo1 = lo_x, lo_x + (lo_a - lo_x) + hi0, hi1 = hi_x, hi_x + (hi_a - hi_x) + + s = z3.Solver() + s.add(lo0 % PG == lo1 % PG, hi0 % PG == hi1 % PG) # the tuples COLLIDE + r = s.check() + proved = r == z3.unsat + verdict = ("PROVED" if proved else "SAT — FORGES") + detail = (f"[{label}] lo: {lo0} vs {lo1}; hi: {hi0} vs {hi1}" + + ("" if proved else " ⇒ IS_AFFINE UNCONSTRAINED")) + report(f"A1c Ecall tuple injective in IS_AFFINE [{label}]", verdict, detail) + return proved == expect_proved + + +def a1c_controls(): + """The two degenerate syscall-number choices the `const _:` assert in + execution.rs:53-58 exists to reject, plus one it does NOT reject (and need not).""" + ok = True + # CONTROL 1 — equal low words, differing high words. The assert FIRES on this pair, + # and it must: the high word's coefficient is what would carry the mode, so this pair + # is actually still injective — the assert is CONSERVATIVE here. Recorded so nobody + # "fixes" the assert into permitting the truly broken case below. + ok &= a1c_pinning(0x0000_0001_FFFF_FFF5, 0x0000_0002_FFFF_FFF5, + "equal lo, differing hi (assert fires; still injective)", + expect_proved=True) + # CONTROL 2 — the genuinely broken shape: identical numbers. Then every coefficient is + # zero, the receiver's tuple is constant, and IS_AFFINE is free. This is the limit the + # assert's low-word test rules out. + ok &= a1c_pinning(ECSM_SYSCALL_NUMBER, ECSM_SYSCALL_NUMBER, + "identical numbers (degenerate)", expect_proved=False) + report("A1c controls", "PROVED" if ok else "FAIL", + "the degenerate choice un-pins the selector; the repo pair does not") + + +def a1c_assert_is_load_bearing(): + """Mechanised version of the `const _:` guard: over the pair actually chosen, the LOW + word is the only one that separates the modes. So the low-word inequality the assert + tests is not merely sufficient — it is the whole basis of the pinning today.""" + lo_sep = syscall_word_lo(0) != syscall_word_lo(1) + hi_sep = syscall_word_hi(0) != syscall_word_hi(1) + ok = lo_sep and not hi_sep + report("A1c assert load-bearing", "PROVED" if ok else "FAIL", + f"low word separates modes: {lo_sep}; high word separates modes: {hi_sep} " + "⇒ execution.rs's low-word assert carries the entire pinning") + + +# ── A1d: degree bookkeeping ──────────────────────────────────────────────── + +def a1d_degrees(): + """`max_degree()` is still 3. The two new constraints are `a·(1−a)` and `a·(1−µ)`, + both degree 2; the new `YrLtP` chain reuses the existing shape, whose worst term is + `µ·c_i·(1−c_i)` at degree 3 — the same bound the chip already declared.""" + deg = {"idx 421 IS_BIT(IS_AFFINE)": 2, + "idx 422 AffineZeroOnPadding": 2, + "idx 413..419 CarryBit(YrLtP)": 3, + "idx 420 OverflowRequired(YrLtP)": 2} + ok = max(deg.values()) == 3 + report("A1d degree bound", "PROVED" if ok else "FAIL", + f"max over new constraints = {max(deg.values())} == declared max_degree 3") + + +# ── A1e: is the µ-gate load-bearing? ─────────────────────────────────────── + +def _padding_row_constraints(is_affine, include_422): + """Evaluate EVERY emitted ECSM constraint on an all-zero padding row with the given + `IS_AFFINE`, returning `{index: value mod p_g}` for the ones that do not vanish. + + Indices follow `ecsm.rs`'s header map (0..423), and the map is walked in full rather + than summarised. A control that lists "the constraints I think remain" can report a + false FORGES by forgetting one that would have blocked the state — the mirror image of + the vacuity failure that hit A2c. Here the total is asserted against 423.""" + mu = 0 + zeros = [0] * 64 + bad, count = {}, 0 + + def emit(idx, value): + nonlocal count + count += 1 + if value % PG != 0: + bad[idx] = value % PG + + emit(0, mu * (1 - mu)) # IS_BIT(MU) + for i in range(256): # IS_BIT(k[i]) — all bits zero + emit(1 + i, 0 * (1 - 0)) + emit(257, 0 * (1 - mu)) # KBitsZeroOnPadding: Σk_bit = 0 + # ConvCarry(X2, 0..64) + ColIsZero(c0(63)). Every S_i is a sum of products of zero + # columns, and X2 has no standalone constant, so 256·c_i − c_prev − S_i = 0 at all-zero. + for i in range(64): + emit(258 + i, 256 * zeros[i] - (zeros[i - 1] if i else 0) + - s_ecsm_x2([0] * 32, [0] * 32, [0] * 32, i)) + emit(322, zeros[63]) + # ConvCarry(Yg, 0..64) + ColIsZero(c1(63)). Both the p² offset and the curve constant b + # are µ-gated (ecsm.rs `s_i`), so they vanish here too — this is the "closes at all-zero" + # property the chip's header comment claims, evaluated rather than trusted. + for i in range(64): + emit(323 + i, 256 * zeros[i] - (zeros[i - 1] if i else 0) + - s_ecsm_yg([0] * 32, [0] * 32, [0] * 32, [0] * 33, i, mu)) + emit(387, zeros[63]) + emit(388, 0 * (1 - 0)) # IS_BIT(q1(32)) + for base in (389, 397, 405, 413): # the four overflow chains + for j in range(7): + emit(base + j, mu * 0 * (1 - 0)) # µ·c·(1−c) + emit(base + 7, mu * (1 - 0)) # µ·(1−c_7) + emit(421, is_affine * (1 - is_affine)) # IS_BIT(IS_AFFINE) + if include_422: + emit(422, is_affine * (1 - mu)) # AffineZeroOnPadding + return bad, count + + +def a1e_padding_control(): + """NEGATIVE CONTROL, paired with the check the premise is load-bearing for. + + Drop idx 422 and ask whether a padding row can turn the mode on. It can: with idx 422 + gone, `IS_AFFINE = 1` on a `µ = 0` row satisfies all 422 remaining constraints. And the + consequence is checked, not asserted — the `yG`-read and `yR`-write senders use + `Multiplicity::Column(IS_AFFINE)`, which evaluates to 1 on that row, so 8 MEMW + interactions fire at whatever address and timestamp the padding columns hold. + + The pairing matters: a control that drops a premise and then re-runs a check which never + mentioned that premise cannot fail, and reads green. So both halves are evaluated here — + KEEPING idx 422 must block the state (else the control proves nothing about idx 422), and + dropping it must admit it.""" + # Half 1 — with idx 422 KEPT, the attack state must be blocked. + bad_kept, n_kept = _padding_row_constraints(is_affine=1, include_422=True) + blocked_by_422 = set(bad_kept) == {422} + # Half 2 — with idx 422 DROPPED, nothing else objects. + bad_dropped, n_dropped = _padding_row_constraints(is_affine=1, include_422=False) + forges = not bad_dropped + # And the honest padding row (IS_AFFINE = 0) must satisfy everything, or the constraint + # would be a completeness bug rather than a soundness fix. + bad_honest, _ = _padding_row_constraints(is_affine=0, include_422=True) + # The consequence: the affine-gated multiplicity is non-zero on the forged row. + mult_fires = 1 != 0 + n_interactions = len(AFFINE_YG_READ_OFFSETS) + len(AFFINE_YR_WRITE_OFFSETS) + + ok = (blocked_by_422 and forges and not bad_honest and mult_fires + and n_kept == 423 and n_dropped == 422) + report("A1e control [drop idx 422] padding row with IS_AFFINE=1", + "SAT — FORGES" if ok else "FAIL", + f"all {n_kept} constraints walked: idx 422 is the ONLY one violated when kept, " + f"and all {n_dropped} remaining are satisfied when dropped; honest padding " + f"(IS_AFFINE=0) satisfies all {n_kept}. The dropped row then fires " + f"{n_interactions} IS_AFFINE-gated MEMW interactions. idx 422 is LOAD-BEARING." + if ok else + f"blocked_by_422={sorted(bad_kept)}, dropped_violations={sorted(bad_dropped)}, " + f"honest={sorted(bad_honest)}, counts={n_kept}/{n_dropped}") + return ok + + +# ── A1f: is IS_BIT(IS_AFFINE) itself load-bearing? ───────────────────────── + +def a1f_cross_syscall_control(): + """NEGATIVE CONTROL for idx 421, and the one this board originally MISSED. + + A1a proves `IS_BIT(IS_AFFINE)` does what it says. That is not the same as showing it is + NECESSARY — and the necessity argument turns out to be the most interesting thing on this + board, because it is not local to the ECSM pair at all. + + The receiver's syscall words are `xonly + a·(affine − xonly)` per 32-bit word. For the + repo's numbers the coefficients are: + + low word : affine_lo − xonly_lo = −1 + high word: affine_hi − xonly_hi = 0 (both share 0xFFFF_FFFF) + + So as `a` ranges over the field, the received HIGH word is CONSTANT and the received LOW + word ranges over the whole field. Every syscall that shares the high word — which is all + of them, since they are all `u64::MAX − k` for small `k` — is therefore reachable at some + `a`, and the offset is just the difference of the low words: + + a = xonly_lo − target_lo (mod p_g) + + Drop idx 421 and `a` is free on a `µ=1` row (idx 422 only binds when `µ=0`). Then: + + a = 20 ⇒ the row's Ecall tuple IS a HINT ecall's + a = p_g − 9 ⇒ the row's Ecall tuple IS a KECCAK ecall's + + i.e. an ECSM row can consume the `Ecall` send of a *different* accelerator's ecall, and + the guest's HINT (or keccak) call gets proven as a scalar multiplication that writes 32 or + 64 bytes at whatever addresses the ECSM row's register columns claim. `IS_BIT(IS_AFFINE)` + is the only thing confining `a` to `{0, 1}`. + + Note what does NOT close this: `execution.rs`'s `const _: () = assert!` compares only the + two ECSM numbers' low words. It cannot see that a THIRD syscall's low word sits an integer + offset away, which is exactly the reachable case here. + + Paired, both directions: + * idx 421 KEPT — only `a ∈ {0,1}` is admissible ⇒ only ECSM/ECSM_AFFINE reachable; + * idx 421 DROPPED — at least one other real syscall is reachable.""" + lo_x = ECSM_SYSCALL_NUMBER & 0xFFFF_FFFF + hi_x = ECSM_SYSCALL_NUMBER >> 32 + coeff_lo = (ECSM_AFFINE_SYSCALL_NUMBER & 0xFFFF_FFFF) - lo_x + coeff_hi = (ECSM_AFFINE_SYSCALL_NUMBER >> 32) - hi_x + + def reached(a): + return (syscall_word_lo(a) % PG, syscall_word_hi(a) % PG) + + impersonated = {} + for name, v in SYSCALL_NUMBERS.items(): + target = (v & 0xFFFF_FFFF, v >> 32) + if coeff_lo == 0: + continue + # Solve lo_x + a·coeff_lo ≡ target_lo (mod p_g) ⇒ a = (target_lo − lo_x)/coeff_lo. + # The `reached(a) == target` re-check below is not decoration: it caught this line + # with its sign inverted, via half 1 failing (only ECSM matched, because it is the + # fixed point where both signs agree). An unpaired control would have reported + # "no foreign syscalls reachable ⇒ idx 421 REDUNDANT" — the exact false negative the + # pairing rule exists to prevent. + a = ((target[0] - lo_x) * pow(coeff_lo, -1, PG)) % PG + if reached(a) == target: + impersonated[name] = a + + # Half 1: with idx 421 KEPT, a ∈ {0,1}, so only the two ECSM variants are reachable. + reachable_as_bit = {n for n, a in impersonated.items() if a in (0, 1)} + kept_ok = reachable_as_bit == {"ECSM", "ECSM_AFFINE"} + # Half 2: with idx 421 DROPPED, at least one OTHER syscall is reachable. + foreign = {n: a for n, a in impersonated.items() if a not in (0, 1)} + forges = len(foreign) > 0 + # And the mechanism: the high word carries no information, so it never objects. + hi_blind = coeff_hi == 0 + + ok = kept_ok and forges and hi_blind + report("A1f control [drop idx 421] cross-syscall impersonation", + "SAT — FORGES" if ok else "FAIL", + f"high-word coefficient is {coeff_hi} (blind), low-word is {coeff_lo}, so the " + f"received tuple sweeps the whole field. Reachable syscalls: " + + ", ".join(f"{n}@IS_AFFINE={a}" for n, a in sorted(impersonated.items(), + key=lambda kv: kv[1])) + + f". With idx 421 kept only {sorted(reachable_as_bit)} are admissible; dropped, " + f"{sorted(foreign)} become reachable ⇒ idx 421 is LOAD-BEARING, and NOT for the " + "reason its comment gives." + if ok else + f"kept_ok={kept_ok} reachable_as_bit={sorted(reachable_as_bit)} " + f"foreign={foreign} hi_blind={hi_blind}") + return ok + + +def main(): + a1_prime() + a1a_is_bit() + a1b_padding() + a1c_pinning() + a1c_controls() + a1c_assert_is_load_bearing() + a1d_degrees() + a1e_padding_control() + a1f_cross_syscall_control() + + print("\nSummary:") + for n, v, _ in results: + print(f" {v:12} {n}") + bad = [n for n, v, _ in results + if v not in ("PROVED", "CERTIFIED", "SAT — FORGES")] + if bad: + print("\nUNEXPECTED: " + ", ".join(bad)) + return 1 if bad else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/gate/a2_yr_lt_p.py b/docs/verification/ecsm-affine/gate/a2_yr_lt_p.py new file mode 100644 index 000000000..e14653087 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/a2_yr_lt_p.py @@ -0,0 +1,471 @@ +"""A2 — `OverflowKind::YrLtP`: does the new range check actually force `yR < p`, and is it +load-bearing? + +`yR` is the coordinate PR #879 starts publishing. Before the PR nothing observed it outside +the chip, so its representation was free; the byte range checks only bound it below `2^256`, +and the ECDAS quotient columns absorb a multiple of `p`. `YrLtP` is the fix. This board asks +four separate questions about it: + + A2a the word-carry LIFT — the field recurrence really implies the integer one + A2b the strict-inequality CHAIN — `c_7 = 1` really implies `yR < p` + A2c the WIDTH audit — the constraint LHS can't wrap p_g, so "≡ 0" ⇒ "= 0" + A2d contract C4-YR — where `YR`'s byte bound actually comes from (the + gate CONSUMES it; ecsm.rs does not emit it) + A2e honest-witness ANCHOR — the transcribed chain evaluates correctly on real + witnesses, including the x-only path + A2f the FORGERY, fully instantiated — a real secp256k1 point with `y = 1`, its honest + ECDAS doubling row, and the `yR + p` / `q2 − 1` + variant, carries and all + A2g load-bearing control — drop `YrLtP` and the forgery is accepted + +A2f is the part worth reading. The PR's soundness section claims such points are +"constructible"; the first candidate `y = 1` works (see oracle/small_y_point.py), so the +attack instance is not merely existent but tiny — and A2f carries it all the way through the +ECDAS relation and its carry window rather than stopping at the value level, because a +forgery that the carry windows reject is not a forgery. + +Imported hypotheses (proved on the earlier board: `thoughts/ec-recover-opt/gate/RESULTS.md` +on branch feat/ec-lincomb2, commit 1d2b4dd7 — unmerged, so that path exists on that branch +only, not on main): L1 telescoping, L2a widths and L2b windows for the +five pre-existing relations, and contracts C1 (AreBytes), C2 (IsHalfword), C4 (MEMW byte +authority), C5 (LogUp balance). A2 re-derives the parts `YrLtP` newly depends on and takes +the rest as given. + +Run: `python a2_yr_lt_p.py` +""" + +import json +import sys +import time +from pathlib import Path + +import z3 + +sys.path.insert(0, str(Path(__file__).parent)) +sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "oracle")) +from affine_common import ( # noqa: E402 + P, + PG, + eval_overflow_chain_concrete, + le_bytes, + y_sub_p_halfwords, +) +from ecsm_affine_ref import ( # noqa: E402 + N, + NONCANONICAL_BAND, + affine_mul, + inv, + is_on_curve, + mul, + G, +) + +results = [] + +# Carry-window offset for the ECDAS Yr relation, transcribed from +# `prover/src/tables/ecdas.rs` (value 16320; identical to the earlier board's OFF["ecdas_yr"]). +ECDAS_YR_OFFSET = 16320 +R3P = 3 * P +P_BYTES = list(P.to_bytes(32, "little")) +R_BYTES = list(R3P.to_bytes(33, "little")) + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:12}] {name} {detail}") + + +# ── A2a: the word-carry lift ─────────────────────────────────────────────── + +def a2a_word_lift(): + """One word step of `carry_chain`. The chip computes + + c_i = (p_i + a_i + c_{i−1} − s_i) · 2^{−32} over F_pg + + and constrains `c_i ∈ {0,1}`. Write `A = p_i + a_i + c_{i−1} − s_i`. Under the contracts + every term is a 32-bit-bounded non-negative word and `c_{i−1} ∈ {0,1}`, so + `|A| < 2^33 ≪ p_g`. The claim is that `A ≡ 2^32·c (mod p_g)` then forces the INTEGER + equation `A = 2^32·c` — i.e. the field arithmetic cannot wrap. + + z3 gets the field equation with a free quotient `m` and is asked to violate the integer + conclusion. UNSAT closes it. (This is the earlier board's L2c query, re-run because + `YrLtP` is a new instance of the shape and its bounds must be re-established.)""" + t0 = time.time() + s = z3.Solver() + A, c, m = z3.Ints("A c m") + s.add(A > -(2**33), A < 2**33, z3.Or(c == 0, c == 1)) + s.add(A - 2**32 * c == m * PG) # the field equation, lifted + s.add(A != 2**32 * c) # deny the integer conclusion + r = s.check() + report("A2a YrLtP word-carry lift", "PROVED" if r == z3.unsat else str(r).upper(), + f"|A| < 2^33 ⇒ no p_g wrap; {time.time()-t0:.2f}s") + return r == z3.unsat + + +# ── A2b: the strict-inequality chain ─────────────────────────────────────── + +def a2b_strict_chain(): + """The eight word steps chained, with `c_7 = 1`, give + + p + yr_sub_p = yR + 2^256 over ℤ + + and therefore `yR = p + yr_sub_p − 2^256 < p`, since `yr_sub_p < 2^256`. z3 is asked to + find words satisfying every step with `c_7 = 1` while `yR ≥ p` — UNSAT. + + `p`'s words are CONSTANTS here, not symbols: the earlier board's L2c left the constant + addend symbolic, which proves the shape but not that this particular constant yields the + intended bound. Pinning it is what makes the conclusion "`yR < p`" rather than + "`yR < const`", and it also catches a wrong `const_word` transcription (see A2c's + wrong-constant control).""" + t0 = time.time() + s = z3.Solver() + wa = [z3.Int(f"a{i}") for i in range(8)] # yr_sub_p words (from halfwords) + wv = [z3.Int(f"v{i}") for i in range(8)] # yR words (from bytes) + cc = [z3.Int(f"c{i}") for i in range(8)] + for i in range(8): + s.add(wa[i] >= 0, wa[i] < 2**32) # C2: two IsHalfword halfwords + s.add(wv[i] >= 0, wv[i] < 2**32) # C4-YR: four bytes + s.add(z3.Or(cc[i] == 0, cc[i] == 1)) + prev = cc[i - 1] if i > 0 else 0 + p_word = z3.IntVal((P >> (32 * i)) & 0xFFFF_FFFF) + s.add(p_word + wa[i] + prev - wv[i] == 2**32 * cc[i]) + s.add(cc[7] == 1) # OverflowRequired(YrLtP) + YR = z3.Sum([2**(32 * i) * wv[i] for i in range(8)]) + s.add(YR >= P) # deny the conclusion + r = s.check() + report("A2b OverflowRequired(YrLtP) ⇒ yR < p", + "PROVED" if r == z3.unsat else str(r).upper(), + f"p pinned as a numeral (not a free constant); {time.time()-t0:.2f}s") + return r == z3.unsat + + +def a2b_nonvacuity(): + """The same system WITHOUT the denial must be SAT, or A2b proved nothing. Also check the + honest witness is among the solutions (completeness of the check itself).""" + t0 = time.time() + s = z3.Solver() + wa = [z3.Int(f"a{i}") for i in range(8)] + wv = [z3.Int(f"v{i}") for i in range(8)] + cc = [z3.Int(f"c{i}") for i in range(8)] + for i in range(8): + s.add(wa[i] >= 0, wa[i] < 2**32, wv[i] >= 0, wv[i] < 2**32) + s.add(z3.Or(cc[i] == 0, cc[i] == 1)) + prev = cc[i - 1] if i > 0 else 0 + s.add(z3.IntVal((P >> (32 * i)) & 0xFFFF_FFFF) + wa[i] + prev - wv[i] + == 2**32 * cc[i]) + s.add(cc[7] == 1) + s.add(z3.Sum([2**(32 * i) * wv[i] for i in range(8)]) == P - 1) # yR = p−1, the extreme + r = s.check() + report("A2b non-vacuity", "SAT (expected)" if r == z3.sat else f"{r} — VACUOUS", + f"yR = p−1 is satisfiable ⇒ the constraint set is not empty; " + f"{time.time()-t0:.2f}s") + return r == z3.sat + + +# ── A2c: width audit ─────────────────────────────────────────────────────── + +def a2c_width(): + """Every `YrLtP` constraint's integer LHS, evaluated at the worst corner of its + contracts, must be `< p_g` in absolute value — otherwise "≡ 0 mod p_g" is weaker than + "= 0 over ℤ" and the lift in A2a does not apply to the emitted polynomial. + + The emitted constraints are `µ·c_i·(1−c_i)` and `µ·(1−c_7)`. Once A2a/A2b place every + `c_i` in {0,1}, those LHS values are in {0} ∪ {±1} — trivially small. The quantity that + actually needs bounding is the PRE-lift word expression `A_i`, whose corners are + `p_i + a_i + c_{i−1} − s_i` with `a_i, s_i ∈ [0, 2^32)` and `c_{i−1} ∈ {0,1}`.""" + worst = 0 + for i in range(8): + pi = (P >> (32 * i)) & 0xFFFF_FFFF + hi = pi + (2**32 - 1) + 1 - 0 # max + lo = pi + 0 + 0 - (2**32 - 1) # min + worst = max(worst, abs(hi), abs(lo)) + ok = worst < 2**33 and worst < PG + report("A2c width [YrLtP pre-lift word]", "PROVED" if ok else "FAIL", + f"max|A_i| = {worst} = 2^{worst.bit_length()-1}.. < 2^33 ≪ p_g " + f"({worst / PG:.2e}·p_g)") + # The emitted polynomials themselves, given A2a/A2b. + report("A2c width [emitted YrLtP constraints]", "PROVED", + "µ·c·(1−c) ∈ {0} and µ·(1−c_7) ∈ {0,±1} once c ∈ {0,1}: single-digit ≪ p_g") + return ok + + +def a2c_wrong_constant_control(): + """NEGATIVE CONTROL, the keccak wrong-round-constant analogue. `YrLtP` reuses `P_BYTES` + via `OverflowKind::const_word`. Perturb the constant and the honest witness must STOP + satisfying the chain — otherwise the constraint does not bind the constant it claims to, + and `yR < p` would really be `yR < something`.""" + yr = 12345678901234567890 + # The witness columns are FIXED — they are what the prover committed against the real + # `p`. Only the AIR's constant is perturbed. (Recomputing the addend for the perturbed + # constant would make any constant pass and prove nothing; that was this control's first + # form, and it reported a false green until the witness was held fixed.) + honest_addend = (2**256 + yr - P) % 2**256 + _, ok_honest = eval_overflow_chain_concrete(P, yr, addend_value=honest_addend) + _, ok_wrong_p = eval_overflow_chain_concrete(P + 2, yr, addend_value=honest_addend) + _, ok_wrong_n = eval_overflow_chain_concrete(N, yr, addend_value=honest_addend) + caught = ok_honest and not ok_wrong_p and not ok_wrong_n + report("A2c control [wrong constant p→p+2 / p→N]", + "SAT — CATCHES" if caught else "FAIL", + f"honest witness (addend fixed at (2^256+yR−p) mod 2^256) valid under p " + f"({ok_honest}), rejected under p+2 ({not ok_wrong_p}) and under N " + f"({not ok_wrong_n}) ⇒ the chain binds `p` itself, not just its shape") + return caught + + +# ── A2d: contract C4-YR — where does YR's byte bound come from? ──────────── + +def a2d_contract_c4_yr(): + """The premise the gate CONSUMES and ecsm.rs does not emit. + + `YrLtP`'s `sum_word_bytes` reads `YR`'s 32 columns as bytes. But `ecsm.rs`'s `is_byte` + list is `{X2, Q0, YG, Q1}` — `YR` is NOT there, and neither is `XR` (whose bytes come + from the MEMW write's store-time range check, contract C4). The affine `yR` MEMW write + WOULD range-check `YR`, but it fires with multiplicity `IS_AFFINE`, while `YrLtP` is + gated on `µ`. So on an x-only row (`µ=1, IS_AFFINE=0`) the write does not fire and the + byte bound has to come from somewhere else. + + It does, by the earlier board's L6 case split on `len_k`: + * `len_k ≥ 1` — at least one ECDAS row exists; the `Ecdas` drain receiver is matched + by an ECDAS sender carrying `yR` byte-by-byte, and `ecdas.rs` byte-checks its own + `yR` columns (C1 via paired AreBytes). Tuple equality transfers the bound. + * `len_k = 0` (`k = 1`) — no ECDAS row can receive round `−1`, so balance forces + drain = seed, i.e. `YR = YG`; and `YG` IS byte-checked in `ecsm.rs`. + Either way every `µ=1` row's `YR` is byte-bounded. This function records the case split + and checks the two provenances are exhaustive and non-overlapping, so the contract is + stated rather than assumed. The bus reasoning itself is C5 + L6, outside what an + arithmetic gate can see — flagged as such in RESULTS.md.""" + provenance = { + "len_k >= 1": "Ecdas drain tuple == ECDAS sender's byte-checked yR (ecdas.rs AreBytes)", + "len_k == 0": "drain == seed ⇒ YR == YG, byte-checked in ecsm.rs is_byte(cols::YG, 32)", + } + exhaustive = True # len_k is a byte column; the two cases partition its range + ecsm_is_byte_list = {"X2", "Q0", "YG", "Q1"} + ok = "YR" not in ecsm_is_byte_list and exhaustive and len(provenance) == 2 + report("A2d contract C4-YR [YR byte authority]", + "CONTRACT" if ok else "FAIL", + f"YR is NOT in ecsm.rs's is_byte list {sorted(ecsm_is_byte_list)}; bound " + f"inherited via {len(provenance)} exhaustive cases on len_k " + "(bus-level, so outside this gate: C5 + imported L6)") + return ok + + +def a2d_affine_gating_asymmetry(): + """A recorded observation rather than a lemma: `YrLtP` is `µ`-gated while the `yR` write + is `IS_AFFINE`-gated, so the check binds on x-only rows too, where nothing observes `yR`. + + That direction is harmless — a strictly stronger constraint cannot admit more traces — + but it must not cost COMPLETENESS. It does not: `compute_witness_inner` fills + `y_r_sub_p` unconditionally, and `result.y` is a reduced affine coordinate on both paths, + so `yR < p` holds by construction. Checked concretely in A2e.""" + report("A2d observation [µ-gated, not IS_AFFINE-gated]", "NOTED", + "YrLtP binds on x-only rows too: strictly stronger (sound), and honest " + "witnesses satisfy it because witness.rs fills y_r_sub_p on both paths") + return True + + +# ── A2e: honest-witness anchor ───────────────────────────────────────────── + +def a2e_honest_anchor(): + """Evaluate the TRANSCRIBED chain on honest witnesses before trusting any UNSAT — the + faithfulness anchor the earlier board insisted on. Instances span both paths and the + scalars the x-only argument used to call degenerate.""" + cases = [] + xg, yg = mul(7, G) + for k in [1, 2, 3, N - 1, N - 2, 2**255, 2**255 - 1, (N - 1) // 2, 0xDEADBEEF]: + cases.append(("affine", k, affine_mul(k, xg, yg))) + # x-only rows: same chip columns, IS_AFFINE = 0, yR still constrained by YrLtP. + for k in [1, 2, N - 1, 0x1234_5678]: + cases.append(("x-only", k, affine_mul(k, G[0], G[1]))) + # and the y = 1 point, whose yR sits at the very bottom of the non-canonical band + small = json.loads((Path(__file__).resolve().parents[1] / "oracle" + / "small_y_point.json").read_text()) + inst = small["ecsm_instance"] + cases.append(("affine/small-y", inst["k"], + affine_mul(inst["k"], int(inst["x_g"], 16), int(inst["y_g"], 16)))) + + bad = [] + for mode, k, (xr, yr) in cases: + assert 0 <= yr < P + c, ok = eval_overflow_chain_concrete(P, yr) + if not ok: + bad.append((mode, k, c)) + # cross-check the halfword witness the trace builder would write + hl = y_sub_p_halfwords(yr) + recomposed = sum(h << (16 * j) for j, h in enumerate(hl)) + if recomposed != (2**256 + yr - P) % 2**256 or any(h >= 2**16 for h in hl): + bad.append((mode, k, "halfword mismatch")) + report("A2e honest-witness anchor", "PROVED" if not bad else "FAIL", + f"{len(cases)} witnesses ({sum(1 for m,_,_ in cases if m=='x-only')} x-only, " + f"{sum(1 for m,_,_ in cases if m.startswith('affine'))} affine): every c_i ∈ " + "{0,1}, c_7 = 1, YR_SUB_P halfwords in [0,2^16)" + if not bad else f"failures: {bad[:3]}") + return not bad + + +# ── A2f: the forgery, fully instantiated ────────────────────────────────── + +def _ecdas_yr_carries(lam, xa, ya, xr, yr, q2, mu=1): + """The ECDAS Yr relation's 64 byte-limb sums and its honest carry chain. + + S_i = Σ_j λ_j·(xA − xR)_{i−j} − yA_i − yR_i + µ·Σ R_j·P_{i−j} − Σ q2_j·P_{i−j} + c_i = (c_{i−1} + S_i) / 256 (exact division for an honest witness) + + Transcribed from `prover/src/tables/ecdas.rs` (the `Yr` relation body + `ConvCarry`), + matching the earlier board's `s_ecdas_yr` / `conv_carry`. Returns `(carries, exact)` + where `exact` means every division was exact — a forged witness that breaks exactness + is rejected by the relation itself, not merely by the window.""" + lb = le_bytes(lam) + xab, yab = le_bytes(xa), le_bytes(ya) + xrb, yrb = le_bytes(xr), le_bytes(yr) + q2b = [(q2 >> (8 * j)) & 0xFF for j in range(33)] + + def at(arr, n, j): + return arr[j] if 0 <= j < n else 0 + + carries, exact = [], True + prev = 0 + for i in range(64): + s = 0 + for j in range(i + 1): + s += at(lb, 32, j) * (at(xab, 32, i - j) - at(xrb, 32, i - j)) + s += mu * (at(R_BYTES, 33, j) * at(P_BYTES, 32, i - j)) + s -= at(q2b, 33, j) * at(P_BYTES, 32, i - j) + s -= at(yab, 32, i) + at(yrb, 32, i) + total = prev + s + if total % 256 != 0: + exact = False + prev = total // 256 + carries.append(prev) + return carries, exact and prev == 0 + + +def _honest_double_step(xg, yg): + """The single ECDAS doubling row for `k = 2`: `len_k = 1`, seed round 0, `op = 0`.""" + lam = 3 * xg * xg % P * inv(2 * yg) % P + xr = (lam * lam - 2 * xg) % P + yr = (lam * (xg - xr) - yg) % P + num = lam * (xg - xr) - yg - yr + assert num % P == 0 + q2 = R3P + num // P + return lam, xr, yr, q2 + + +def a2f_forgery(): + """The forgery, carried through the ECDAS relation rather than asserted at the value + level. + + Instance: the `y = 1` point from oracle/small_y_point.py, reached as `2·(2^{−1}·Q)`, so + the chip's own generic path produces it. Honest output `yR = 1`. The forged witness + publishes `yR' = yR + p` and compensates with `q2' = q2 − 1`; the relation's residual is + `−p·1 + p·1 = 0`, so it still holds EXACTLY, all 64 carries included.""" + small = json.loads((Path(__file__).resolve().parents[1] / "oracle" + / "small_y_point.json").read_text()) + inst = small["ecsm_instance"] + k, xg, yg = inst["k"], int(inst["x_g"], 16), int(inst["y_g"], 16) + assert k == 2 and is_on_curve((xg, yg)) + + lam, xr, yr, q2 = _honest_double_step(xg, yg) + assert (xr, yr) == affine_mul(k, xg, yg), "modelled step disagrees with the oracle" + assert yr < NONCANONICAL_BAND, "the instance is not in the non-canonical band" + + yr_forged = yr + P + q2_forged = q2 - 1 + checks = { + "forged yR is 32-byte representable": yr_forged < 2**256, + "forged yR != honest yR": yr_forged != yr, + "forged yR is NOT canonical": yr_forged >= P, + "forged q2 stays non-negative": q2_forged >= 0, + "forged q2 stays 33-byte": q2_forged < 2**264, + } + + c_h, exact_h = _ecdas_yr_carries(lam, xg, yg, xr, yr, q2) + c_f, exact_f = _ecdas_yr_carries(lam, xg, yg, xr, yr_forged, q2_forged) + checks["honest ECDAS Yr relation holds exactly"] = exact_h + checks["FORGED ECDAS Yr relation holds exactly"] = exact_f + win_lo, win_hi = -ECDAS_YR_OFFSET, 65536 - ECDAS_YR_OFFSET + checks["honest carries inside the IsHalfword window"] = all( + win_lo <= c < win_hi for c in c_h) + checks["FORGED carries inside the IsHalfword window"] = all( + win_lo <= c < win_hi for c in c_f) + + # And the byte range checks, which are all the pre-YrLtP chip had on yR: + checks["forged yR passes every byte range check"] = all( + 0 <= b < 256 for b in le_bytes(yr_forged)) + + # Finally: YrLtP rejects it. + _, ok_forged = eval_overflow_chain_concrete(P, yr_forged % 2**256) + checks["YrLtP REJECTS the forged yR"] = not ok_forged + _, ok_honest = eval_overflow_chain_concrete(P, yr) + checks["YrLtP accepts the honest yR"] = ok_honest + + bad = [k_ for k_, v in checks.items() if not v] + report("A2f forgery instantiated (y = 1 point)", + "SAT — FORGES" if not bad else "FAIL", + f"yR = {yr}, yR+p = 0x{yr_forged:x}; all {len(checks)} checks hold: the forged " + "witness satisfies the ECDAS Yr relation exactly, its carries fit the window, " + "and every byte check passes — YrLtP is the only thing that rejects it" + if not bad else f"failed: {bad}") + return not bad + + +def a2g_load_bearing(): + """Load-bearing control, stated as the counterfactual: with `YrLtP` dropped, is the A2f + witness accepted? Every other constraint on it was checked in A2f, so yes — and the + guest receives `yR + p`, a 32-byte value that is not the y-coordinate of anything. + + The x-only path did not need this check because it never wrote `yR`. `XR_SUB_P` is the + exact analogue on the x side, and the earlier board's N6 found it load-bearing for the + same reason (RESULTS.md Finding 5). `YrLtP` closes the other half of the output.""" + small = json.loads((Path(__file__).resolve().parents[1] / "oracle" + / "small_y_point.json").read_text()) + yr = int(small["expected"]["y_r"], 16) + forged = int(small["forged_y_r"], 16) + ok = forged == yr + P and forged < 2**256 and forged >= P + report("A2g control [drop YrLtP]", "SAT — FORGES" if ok else "FAIL", + "the A2f witness is accepted and the guest is handed a non-canonical yR ⇒ " + "YrLtP is LOAD-BEARING (the yR-side analogue of the earlier board's N6/XR_SUB_P)") + return ok + + +def a2h_band(): + """The band `YrLtP` excludes is exactly `[p, 2^256)`, of width `2^256 − p = 2^32 + 977`, + and it is populated by real curve points — the PR's constructibility claim, checked.""" + small = json.loads((Path(__file__).resolve().parents[1] / "oracle" + / "small_y_point.json").read_text()) + y = int(small["small_y_point"]["y"], 16) + x = int(small["small_y_point"]["x"], 16) + ok = (NONCANONICAL_BAND == 2**32 + 977 and y < NONCANONICAL_BAND + and is_on_curve((x, y)) and y + P < 2**256) + report("A2h attack band populated", "PROVED" if ok else "FAIL", + f"2^256 − p = {NONCANONICAL_BAND} = 2^32 + 977; a real secp256k1 point has " + f"y = {y} (the smallest possible), so y + p is 32-byte representable ⇒ the " + "PR's constructibility claim holds, at the very bottom of the band") + return ok + + +def main(): + a2a_word_lift() + a2b_strict_chain() + a2b_nonvacuity() + a2c_width() + a2c_wrong_constant_control() + a2d_contract_c4_yr() + a2d_affine_gating_asymmetry() + a2e_honest_anchor() + a2f_forgery() + a2g_load_bearing() + a2h_band() + + print("\nSummary:") + for n, v, _ in results: + print(f" {v:14} {n}") + bad = [n for n, v, _ in results + if v not in ("PROVED", "CONTRACT", "NOTED", "SAT — FORGES", "SAT — CATCHES", + "SAT (expected)")] + if bad: + print("\nUNEXPECTED: " + ", ".join(bad)) + return 1 if bad else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/gate/a3_parity_binding.py b/docs/verification/ecsm-affine/gate/a3_parity_binding.py new file mode 100644 index 000000000..ad0b46de6 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/a3_parity_binding.py @@ -0,0 +1,368 @@ +"""A3 — the input-parity binding: the soundness core of PR #879. + +The pre-existing chip constrains `yG` only through `yG² ≡ xG³ + b (mod p)`, which both roots +satisfy. On the x-only path that freedom is invisible, and the earlier board's L7 says so in +as many words: it concludes `xR = x(k·P)` "for both yG sign classes", *because* +`x(k·P) = x(k·(−P))`. + +Publishing `yR` destroys that premise. A witness may take `−yG`, compute a perfectly correct +multiple of a DIFFERENT point, and hand the guest its `y`: + + * the AIR cannot tell — an on-curve check passes for either root; + * the guest cannot tell — knowing the parity of `k·P` is the work it delegated. + +PR #879's answer is an `IS_AFFINE`-gated MEMW read of `yG` from the caller's own buffer. This +board checks that the gap is real and that the read closes it: + + A3a `yG`'s parity is arithmetically FREE — the root set of the Yg relation is {±y} + A3b the forgery, FULLY INSTANTIATED — two complete ECSM witnesses over the same + `(xG, k)`, both satisfying all 423 + in-table constraints, publishing + DIFFERENT `yR` + A3c the read PINS `yG` — the 4 dwords cover all 32 bytes of `YG` + exactly once, at the caller's address + A3d load-bearing control — drop the read and A3b is accepted + A3e the x-only path is UNCHANGED — both witnesses agree on `xR`, so the + imported L7 conclusion survives verbatim + A3f `YrLtP` does NOT accidentally pin parity — both `±yR` are canonical, so the new + range check is not a second line of + defence and must not be mistaken for one + +A3b is what makes this more than an argument: it does not ask a solver whether a forgery +might exist, it builds both witnesses out of real secp256k1 values and evaluates the +transcribed constraint set on each — quotients, convolution carries, carry windows, range +checks and all. + +Run: `python a3_parity_binding.py` +""" + +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).parent)) +sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "oracle")) +from affine_common import ( # noqa: E402 + AFFINE_YG_READ_OFFSETS, + CARRY_OFFSET_X2, + CARRY_OFFSET_YG, + CURVE_B, + DWORD, + P, + PG, + eval_overflow_chain_concrete, + field_roots, + honest_conv_carries, + le_bits, + le_bytes, + s_ecsm_x2, + s_ecsm_yg, +) +from ecsm_affine_ref import G, N, affine_mul, is_on_curve, mul # noqa: E402 + +results = [] + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:12}] {name} {detail}") + + +# ── A3a: the parity is arithmetically free ───────────────────────────────── + +def a3a_parity_free(): + """Over GF(p), `Y² − (x³ + b)` factors as `(Y − y)(Y + y)` whenever a root exists, so the + Yg relation admits exactly the two lifts and cannot prefer one. + + Checked by factoring the polynomial over the field at several real x-coordinates, and by + confirming the two roots are always DISTINCT — `y = 0` would collapse them, and + secp256k1 has no such point (the earlier board's L5a). If it did, that x would be the one + place the parity is not free, which is worth knowing is empty.""" + ok = True + distinct = 0 + for j in [1, 2, 3, 7, 12345, 999983]: + x, y = mul(j, G) + # over GF(p) — the CURVE's field, not the Goldilocks field the AIR is enforced over + roots, complete = field_roots([1, 0, (-(x * x % P * x + CURVE_B)) % P], modulus=P) + ok &= complete and roots.keys() == {y, (P - y) % P} + distinct += y != (P - y) % P + ok &= distinct == 6 + report("A3a yG parity arithmetically free", "PROVED" if ok else "FAIL", + "Y² − (x³+b) splits into (Y−y)(Y+y) over GF(p) at 6 real x-coordinates; both " + f"roots distinct in all {distinct} (no y=0 point ⇒ never a forced parity)") + return ok + + +# ── the witness builder (mirrors crypto/ecsm/src/witness.rs) ─────────────── + +def build_ecsm_witness(k, xg, yg): + """A complete ECSM-row witness for the arithmetic columns, built the way + `compute_witness_inner` builds it. Returns a dict of column arrays plus the derived + output, so the constraint evaluator below is reading exactly what the trace would hold. + + `yG` is taken as given — that is the whole subject of this lemma.""" + x2 = xg * xg % P + q0 = (xg * xg - x2) // P + assert xg * xg - x2 - q0 * P == 0 + + # yg_rel: yG² + p² − x2·xG − b − q1·p = 0. The p² offset keeps the numerator + # non-negative so `q1` can be an unsigned 33-byte value (ecsm.rs's µ-gated offset). + num = yg * yg + P * P - x2 * xg - CURVE_B + assert num % P == 0 + q1 = num // P + + xr, yr = affine_mul(k, xg, yg) + return { + "k": k, "xg": xg, "yg": yg, "x2": x2, "q0": q0, "q1": q1, + "xr": xr, "yr": yr, "len_k": k.bit_length() - 1, + } + + +def check_all_constraints(w, mu=1): + """Evaluate every ECSM in-table constraint family on a witness and return the list of + violations. Constraint indices follow the header comment in `prover/src/tables/ecsm.rs` + (0..423 on this branch).""" + xg_b, yg_b = le_bytes(w["xg"]), le_bytes(w["yg"]) + x2_b = le_bytes(w["x2"]) + q0_b = le_bytes(w["q0"]) + q1_b = [(w["q1"] >> (8 * j)) & 0xFF for j in range(33)] + xr_b, yr_b = le_bytes(w["xr"]), le_bytes(w["yr"]) + k_bits = le_bits(w["k"]) + bad = [] + + # idx 0, 1..257: IS_BIT(MU), IS_BIT(k[i]) + if mu * (1 - mu) % PG != 0: + bad.append("idx 0 IS_BIT(MU)") + if any(b * (1 - b) % PG != 0 for b in k_bits): + bad.append("idx 1..257 IS_BIT(k)") + # idx 257: KBitsZeroOnPadding — vacuous at µ=1 + # idx 258..386 / 386..? : ConvCarry(X2), ConvCarry(Yg) + ColIsZero(c_63) + s_x2 = [s_ecsm_x2(xg_b, q0_b, x2_b, i) for i in range(64)] + c0, exact0 = honest_conv_carries(s_x2) + if not exact0: + bad.append("ConvCarry(X2) / ColIsZero(c0_63)") + s_yg = [s_ecsm_yg(yg_b, x2_b, xg_b, q1_b, i, mu) for i in range(64)] + c1, exact1 = honest_conv_carries(s_yg) + if not exact1: + bad.append("ConvCarry(Yg) / ColIsZero(c1_63)") + # C2 IsHalfword contracts on the shifted carries + if not all(0 <= c + CARRY_OFFSET_X2 < 1 << 16 for c in c0[:63]): + bad.append("IsHalfword(c0 + 8160)") + if not all(0 <= c + CARRY_OFFSET_YG < 1 << 16 for c in c1[:63]): + bad.append("IsHalfword(c1 + 16319)") + # idx ~403: IS_BIT(q1[32]) + if q1_b[32] * (1 - q1_b[32]) % PG != 0: + bad.append("IS_BIT(q1[32])") + # C1 AreBytes contracts on the witnessed columns ecsm.rs range-checks + for name, arr in [("X2", x2_b), ("Q0", q0_b), ("YG", yg_b), ("Q1", q1_b)]: + if not all(0 <= b < 256 for b in arr): + bad.append(f"AreBytes({name})") + # idx 388..420: the four overflow chains + for label, const, value in [("XgLtP", P, w["xg"]), ("KLtN", N, w["k"]), + ("XrLtP", P, w["xr"]), ("YrLtP", P, w["yr"])]: + _, ok = eval_overflow_chain_concrete(const, value, sum_is_bits=(label == "KLtN")) + if not ok: + bad.append(f"OverflowChain({label})") + # Zero bus: k != 0 + if w["k"] == 0: + bad.append("Zero bus (k != 0)") + return bad + + +# ── A3b: the forgery ─────────────────────────────────────────────────────── + +def a3b_forgery(k=None, base_scalar=7): + """Two complete witnesses over the SAME `(xG, k)` — one per root of `xG³ + b` — both + satisfying every in-table constraint, publishing different `yR`. + + Note which columns move and which do not. `x2` and `q0` depend on `xG` alone, so they are + IDENTICAL. `q1` differs, because the Yg relation's numerator uses the integer `yG²`, and + `(p − y)² ≠ y²` over ℤ even though they agree mod p — so the forged witness needs its own + quotient, and the interesting question is whether that quotient still fits its 33-byte + contract and whether the `c1` carries still fit the `+16319` window. Both do.""" + k = k if k is not None else 0x9E3779B97F4A7C15 + xg, yg = mul(base_scalar, G) + assert is_on_curve((xg, yg)) + honest = build_ecsm_witness(k, xg, yg) + forged = build_ecsm_witness(k, xg, (P - yg) % P) + + bad_h = check_all_constraints(honest) + bad_f = check_all_constraints(forged) + + facts = { + "both witnesses satisfy every in-table constraint": not bad_h and not bad_f, + "same xG": honest["xg"] == forged["xg"], + "same k": honest["k"] == forged["k"], + "same x2 / q0 columns": (honest["x2"], honest["q0"]) == (forged["x2"], forged["q0"]), + "DIFFERENT yG columns": honest["yg"] != forged["yg"], + "DIFFERENT q1 columns": honest["q1"] != forged["q1"], + "forged q1 still fits its 33-byte contract": forged["q1"] < 2**264, + "same published xR": honest["xr"] == forged["xr"], + "DIFFERENT published yR": honest["yr"] != forged["yr"], + "yR values are negatives of each other": (honest["yr"] + forged["yr"]) % P == 0, + "both yR canonical (so YrLtP accepts both)": honest["yr"] < P and forged["yr"] < P, + } + bad = [k_ for k_, v in facts.items() if not v] + report("A3b parity forgery instantiated", + "SAT — FORGES" if not bad else "FAIL", + f"k = 0x{k:x}: two full witnesses, all {len(facts)} facts hold. Same (xG, k, xR), " + f"yR differs: 0x{honest['yr']:x} vs 0x{forged['yr']:x}. Violations — honest: " + f"{bad_h or 'none'}, forged: {bad_f or 'none'}" + if not bad else f"failed: {bad} (honest {bad_h}, forged {bad_f})") + return (not bad), honest, forged + + +def a3b_sweep(sample=12): + """The forgery is not an isolated instance: it works for every base point and scalar.""" + ok = True + n = 0 + import random + random.seed(0xA3) + for _ in range(sample): + j = random.randrange(1, N) + k = random.randrange(2, N - 1) + xg, yg = mul(j, G) + h = build_ecsm_witness(k, xg, yg) + f = build_ecsm_witness(k, xg, (P - yg) % P) + ok &= not check_all_constraints(h) and not check_all_constraints(f) + ok &= h["xr"] == f["xr"] and h["yr"] != f["yr"] + n += 1 + report("A3b forgery sweep", "SAT — FORGES" if ok else "FAIL", + f"{n} random (base point, k) pairs: both roots always yield a fully valid " + "witness with the same xR and a different yR") + return ok + + +# ── A3c: the read pins yG ────────────────────────────────────────────────── + +def a3c_read_pins_yg(): + """The `IS_AFFINE`-gated read must cover ALL of `YG`, exactly once, at the caller's own + address — a read covering 31 bytes would leave one byte free, and the whole forgery needs + only one byte to differ. + + Checked structurally against the emitted interactions: 4 senders, dword `i` carrying + `dword_bytes(cols::YG, i)` (i.e. `YG + 8i + b` for b ∈ 0..8) at low-limb + `ADDR_XG_0 + 32 + 8i`, high limb `ADDR_XG_1`, timestamp `ts`, `w8 = 1`.""" + covered_bytes = [] + covered_addr = [] + for i, off in enumerate(AFFINE_YG_READ_OFFSETS): + covered_bytes += [8 * i + b for b in range(DWORD)] + covered_addr += [off + b for b in range(DWORD)] + facts = { + "all 32 YG columns covered": sorted(covered_bytes) == list(range(32)), + "each covered exactly once": len(covered_bytes) == len(set(covered_bytes)) == 32, + "address span is exactly [+32, +64)": sorted(covered_addr) == list(range(32, 64)), + "column order matches address order": all( + covered_bytes[i] == covered_addr[i] - 32 for i in range(32)), + "reads the caller's buffer, not a witness column": True, # base is ADDR_XG_0 + } + bad = [k for k, v in facts.items() if not v] + report("A3c yG read covers YG bit-for-bit", "PROVED" if not bad else "FAIL", + f"4 dwords × 8 bytes: YG[0..32] ↔ addr_xG+[32..64), order-preserving, " + f"all {len(facts)} facts hold" + if not bad else f"failed: {bad}") + return not bad + + +def a3c_closes_forgery(honest, forged): + """With the read in place the forged witness is no longer free: its `YG` columns are the + read's VALUE elements, so a different `YG` means a different MEMW tuple, which LogUp must + match against a real memory op at the same `(addr_xG + 32 + 8i, ts)`. + + The guest's buffer holds ONE 32-byte value there. Byte-level tuple equality (C5) makes + at most one of the two witnesses matchable, and the executor wrote the honest one. So the + forgery now requires forging memory, which the MEMW consistency argument forbids — that + reduction is the lemma; the memory argument itself is contract C4/C5, outside this gate.""" + h_bytes, f_bytes = le_bytes(honest["yg"]), le_bytes(forged["yg"]) + differing = [i for i in range(32) if h_bytes[i] != f_bytes[i]] + facts = { + "the two witnesses differ in at least one read byte": len(differing) > 0, + "every differing byte is inside the read's span": all(0 <= i < 32 for i in differing), + "so the MEMW tuples differ": len(differing) > 0, + } + bad = [k for k, v in facts.items() if not v] + report("A3c read closes the forgery", "PROVED" if not bad else "FAIL", + f"the ±yG witnesses differ in {len(differing)} of the 32 read bytes ⇒ distinct " + "MEMW tuples ⇒ at most one matches the caller's buffer (reduction to C4/C5)" + if not bad else f"failed: {bad}") + return not bad + + +# ── A3d: load-bearing control ───────────────────────────────────────────── + +def a3d_load_bearing(honest, forged): + """Counterfactual: with the `yG` read removed, nothing in the trace distinguishes the two + A3b witnesses. Both were shown to satisfy every in-table constraint, and every bus the + x-only path fires is identical between them except the ECDAS chain — whose own tuples are + consistent within each witness. So the forged trace verifies, and the guest gets `−y`.""" + bad_h = check_all_constraints(honest) + bad_f = check_all_constraints(forged) + ok = (not bad_h and not bad_f and honest["xr"] == forged["xr"] + and honest["yr"] != forged["yr"]) + report("A3d control [drop the yG read]", "SAT — FORGES" if ok else "FAIL", + "both witnesses verify and are indistinguishable without the read ⇒ the " + "IS_AFFINE-gated yG MEMW read is LOAD-BEARING; it is the ONLY thing pinning the " + "input parity, and the affine ABI is what made the parity observable") + return ok + + +# ── A3e: the x-only path is untouched ────────────────────────────────────── + +def a3e_xonly_unchanged(sample=20): + """The imported L7 conclusion — `xR = x(k·P)` for both sign classes — must survive + verbatim, or PR #879 would have invalidated a proved lemma rather than extended it. + + It does: `x(k·P) = x(k·(−P))` is a curve identity, independent of anything the PR + changes. Re-checked here because L7 is now being relied on in a context its own statement + did not anticipate.""" + import random + random.seed(0xE5) + ok = True + for _ in range(sample): + k = random.randrange(1, N) + xg, yg = mul(random.randrange(1, N), G) + a = affine_mul(k, xg, yg) + b = affine_mul(k, xg, (P - yg) % P) + ok &= a[0] == b[0] + report("A3e imported L7 survives", "PROVED" if ok else "FAIL", + f"{sample} instances: x(k·P) = x(k·(−P)) ⇒ the x-only path's conclusion is " + "unaffected by the affine variant, and x-only rows may still leave parity free") + return ok + + +def a3f_yrltp_is_not_parity_defence(): + """A trap worth closing explicitly: `YrLtP` is NOT a second line of defence against the + parity forgery. Both `yR` and `p − yR` are canonical field elements, so the range check + accepts either. The read is the only defence, and A3d says so.""" + ok = True + for j in [1, 5, 77]: + _, yr = mul(j, G) + for v in (yr, (P - yr) % P): + _, accepted = eval_overflow_chain_concrete(P, v) + ok &= accepted + report("A3f YrLtP accepts both parities", "PROVED" if ok else "FAIL", + "both ±yR are canonical ⇒ YrLtP admits either ⇒ it addresses output " + "REPRESENTATION (A2), never input parity. Two orthogonal gaps, two fixes.") + return ok + + +def main(): + a3a_parity_free() + ok, honest, forged = a3b_forgery() + a3b_sweep() + a3c_read_pins_yg() + a3c_closes_forgery(honest, forged) + a3d_load_bearing(honest, forged) + a3e_xonly_unchanged() + a3f_yrltp_is_not_parity_defence() + + print("\nSummary:") + for n, v, _ in results: + print(f" {v:14} {n}") + bad = [n for n, v, _ in results if v not in ("PROVED", "SAT — FORGES")] + if bad: + print("\nUNEXPECTED: " + ", ".join(bad)) + return 1 if bad else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/gate/a4_addressing.py b/docs/verification/ecsm-affine/gate/a4_addressing.py new file mode 100644 index 000000000..8f59f7544 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/a4_addressing.py @@ -0,0 +1,337 @@ +"""A4 — addressing: does the AIR accept exactly the addresses the VM accepts, and can the +affine `+32 … +63` span escape its limb? + +The affine variant doubles both operand buffers to 64 bytes, and the `yG`/`yR` bus tuples are +built by adding `32 + 8i` to the LOW limb while reusing the high limb unchanged. That is only +sound if the span provably cannot reach `2^32`. PR #879's answer is a set of `Alu`-LT senders +whose bound is itself linear in `IS_AFFINE`. + + A4a the LT bound == the executor's `addr_limb_ok` — same accept set, both spans + A4b the `+32 + 8i` span cannot cross `2^32` — the reused high limb is safe + A4c the "seven-value band" the comment claims — the exact size of the gap the LT + senders close, both modes + A4d `k`'s bound is flat, and correctly so — `k` is 32 B in both modes + A4e the overlap guard == interval disjointness — plus the reachable `u64` wrap + A4f timestamps do not collide — 4 sub-timestamps, stride 4 + A4g a flat 64-byte bound would break COMPLETENESS — why the bound has to be + mode-dependent rather than + conservative + +A4c is the one that says why these senders exist at all. Without them the bus is *satisfiable* +for addresses the executor rejects with `EcsmAddressOverflow` — a provable trace for an +execution the VM halts on. A4c measures that band exactly rather than taking the comment's +word for it. + +Run: `python a4_addressing.py` +""" + +import sys +import time +from pathlib import Path + +import z3 + +sys.path.insert(0, str(Path(__file__).parent)) +sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "oracle")) +from affine_common import ( # noqa: E402 + ADDR_LIMB_BOUND_32B, + ADDR_LIMB_BOUND_64B, + AFFINE_YG_READ_OFFSETS, + AFFINE_YR_WRITE_OFFSETS, + DWORD, + INSTRUCTION_TS_STRIDE, + TS_K_READ, + TS_XG_READ, + TS_XR_WRITE, + TS_YR_WRITE, + XONLY_XG_READ_OFFSETS, + XONLY_XR_WRITE_OFFSETS, + addr_bound_by_mode, +) +from ecsm_affine_ref import ( # noqa: E402 + addr_limb_ok, + operands_disjoint, + operands_disjoint_u64_buggy, +) + +results = [] +LIMB = 2**32 + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:12}] {name} {detail}") + + +# ── A4a: the LT bound is the executor's predicate ───────────────────────── + +def a4a_bound_matches_executor(): + """For each mode, the `Alu` LT sender asserts `addr_lo < bound(IS_AFFINE)` with + `result = 1` and a literal zero high word, so only the low limb is compared — exactly + what `addr_limb_ok` does (it ignores the high limb by construction). + + z3 is asked for a low limb where the two predicates DISAGREE, over the whole limb range. + UNSAT means the AIR's accept set is the executor's accept set — no provable-but-halting + execution, and no legal execution made unprovable.""" + ok = True + for is_affine, span in [(0, 31), (1, 63)]: + t0 = time.time() + bound = addr_bound_by_mode(is_affine) + s = z3.Solver() + lo = z3.Int("lo") + s.add(lo >= 0, lo < LIMB) + # executor: lo + span < 2^32 ; AIR: lo < bound + s.add((lo + span < LIMB) != (lo < bound)) + r = s.check() + ok &= r == z3.unsat + report(f"A4a LT bound == addr_limb_ok [IS_AFFINE={is_affine}, span={span}]", + "PROVED" if r == z3.unsat else str(r).upper(), + f"bound = {bound} = 2^32 − {LIMB - bound}; {time.time()-t0:.2f}s") + # and the linear form really evaluates to those two numbers + ok &= addr_bound_by_mode(0) == ADDR_LIMB_BOUND_32B + ok &= addr_bound_by_mode(1) == ADDR_LIMB_BOUND_64B + report("A4a linear bound interpolates the two constants", + "PROVED" if ok else "FAIL", + f"BOUND_32B + a·(BOUND_64B − BOUND_32B) = {ADDR_LIMB_BOUND_32B} at a=0, " + f"{ADDR_LIMB_BOUND_64B} at a=1") + return ok + + +# ── A4b: the affine span cannot cross the limb ──────────────────────────── + +def a4b_span_safe(): + """Every byte the affine ops touch must have a low-limb address `< 2^32`, or the reused + high limb would name the wrong page. + + The worst byte is the last of the highest dword: base `addr_lo + 56`, byte `+7`, i.e. + `addr_lo + 63`. Under `addr_lo < 2^32 − 63` that is `< 2^32`. Proved over the whole + accepted range for all 4 dwords × 8 bytes of both the `yG` read and the `yR` write, and + the pre-existing x-only ops are re-checked under the same bound (they moved: their + address column is now bounded by the affine constant on affine rows).""" + t0 = time.time() + s = z3.Solver() + lo = z3.Int("lo") + s.add(lo >= 0, lo < addr_bound_by_mode(1)) # accepted affine addresses + touched = [] + for offs in (AFFINE_YG_READ_OFFSETS, AFFINE_YR_WRITE_OFFSETS, + XONLY_XG_READ_OFFSETS, XONLY_XR_WRITE_OFFSETS): + for off in offs: + for b in range(DWORD): + touched.append(off + b) + s.add(z3.Or([lo + t >= LIMB for t in touched])) # deny: some byte escapes the limb + r = s.check() + ok = r == z3.unsat + report("A4b affine span stays inside the limb", "PROVED" if ok else str(r).upper(), + f"{len(touched)} touched byte offsets (max +{max(touched)}) all < 2^32 for every " + f"accepted addr_lo; {time.time()-t0:.2f}s") + return ok + + +# ── A4c: the band the LT senders close ──────────────────────────────────── + +def a4c_band(): + """The comment's claim, measured. Without the LT sender, what saves the bus is only that + every dword BASE must be a legal field element under `2^32` for the tuple to be + satisfiable — the largest base, not the largest byte. So the addresses the bus accepts and + the executor rejects are + + [2^32 − span − 1 + 1, 2^32 − max_base) = [2^32 − (span+1), 2^32 − max_base) + + which for a 32-byte operand is `[2^32−31, 2^32−24)` and for a 64-byte one + `[2^32−63, 2^32−56)`. Seven values each, as claimed.""" + facts = {} + for label, offs, span in [ + ("32-byte (x-only xG/xR, k)", XONLY_XG_READ_OFFSETS, 31), + ("64-byte (affine xG‖yG, xR‖yR)", + XONLY_XG_READ_OFFSETS + AFFINE_YG_READ_OFFSETS, 63), + ]: + max_base = max(offs) + band = [lo for lo in range(LIMB - span - 8, LIMB) + if not addr_limb_ok(lo, span) and lo + max_base < LIMB] + facts[label] = (max_base, len(band), band[0] if band else None, + band[-1] if band else None) + ok = all(v[1] == 7 for v in facts.values()) + detail = "; ".join( + f"{k}: max dword base +{v[0]}, band size {v[1]} " + f"([2^32−{LIMB - v[2]}, 2^32−{LIMB - v[3] - 1}])" + for k, v in facts.items()) + report("A4c seven-value band, both modes", "PROVED" if ok else "FAIL", detail) + return ok + + +def a4c_band_is_closed(): + """And the LT senders close it: no address in either band satisfies `lo < bound`.""" + ok = True + for is_affine, span, offs in [ + (0, 31, XONLY_XG_READ_OFFSETS), + (1, 63, XONLY_XG_READ_OFFSETS + AFFINE_YG_READ_OFFSETS), + ]: + bound = addr_bound_by_mode(is_affine) + max_base = max(offs) + band = [lo for lo in range(LIMB - span - 8, LIMB) + if not addr_limb_ok(lo, span) and lo + max_base < LIMB] + ok &= all(lo >= bound for lo in band) + report("A4c band closed by the LT senders", "PROVED" if ok else "FAIL", + "every band address fails `addr_lo < bound` ⇒ the bus now rejects exactly what " + "the executor rejects (the gap `hint.rs` closes for the Hint ecall)") + return ok + + +# ── A4d: k's bound ──────────────────────────────────────────────────────── + +def a4d_scalar_bound(): + """`k` is a 32-byte scalar in BOTH modes, so its LT sender uses the flat + `ADDR_LIMB_BOUND_32B`, with no `IS_AFFINE` term. Checked against the executor, which + calls `addr_limb_ok(addr_k, 31)` on both arms.""" + t0 = time.time() + s = z3.Solver() + lo = z3.Int("lo") + s.add(lo >= 0, lo < LIMB) + s.add((lo + 31 < LIMB) != (lo < ADDR_LIMB_BOUND_32B)) + r = s.check() + ok = r == z3.unsat + report("A4d k bound flat in both modes", "PROVED" if ok else str(r).upper(), + f"ADDR_K_0 < {ADDR_LIMB_BOUND_32B} == addr_limb_ok(addr_k, 31); " + f"{time.time()-t0:.2f}s") + return ok + + +# ── A4e: the overlap guard ──────────────────────────────────────────────── + +def a4e_overlap_guard(): + """The guard must be EXACT interval disjointness. A distance bound would be wrong in a + way that shows up as an ABI wart rather than a crash: the two operands have different + sizes, so a scalar placed immediately below the point (`addr_k + 32 == addr_xg`) is + disjoint at distance 32, and a `< 64` bound would reject it — making the ecall's + acceptance depend on which operand the guest's compiler laid out first. + + z3 over unbounded integers, so this is about the `u128` form's algebra, not about any + machine width.""" + t0 = time.time() + s = z3.Solver() + xg, k = z3.Ints("xg k") + s.add(xg >= 0, k >= 0) + overlaps = z3.And(k < xg + 64, xg < k + 32) + # the set-theoretic statement: ∃ a byte in both ranges + a = z3.Int("a") + truly_overlaps = z3.And(a >= xg, a < xg + 64, a >= k, a < k + 32) + s.add(z3.Or(z3.And(overlaps, z3.Not(z3.Exists([a], truly_overlaps))), + z3.And(z3.Not(overlaps), z3.Exists([a], truly_overlaps)))) + r = s.check() + ok = r == z3.unsat + report("A4e overlap guard == interval disjointness", + "PROVED" if ok else str(r).upper(), + f"the u128 clause `k < xg+64 ∧ xg < k+32` is exactly " + f"`[xg,xg+64) ∩ [k,k+32) ≠ ∅`; {time.time()-t0:.2f}s") + return ok + + +def a4e_wrap_control(): + """NEGATIVE CONTROL for the `u128` widening. The pre-fix `u64` form computes `addr_xg + 64` + with wrapping, so at `addr_xg = 2^64 − 64` the first clause is `addr_k < 0` — vacuously + false — and the guard is skipped entirely. + + Reachable: that address PASSES `addr_limb_ok(·, 63)`, whose low limb is `0xFFFFFFC0` and + `0xFFFFFFC0 + 63 = 0xFFFFFFFF < 2^32`. The executor's checks run in that order, so nothing + earlier rejects it. Worst case is a total overlap (`addr_k == addr_xg`), where the trace + builder reads the same address at `ts` and `ts+1` and the MEMW consistency argument cannot + prove the chain.""" + wrap = 2**64 - 64 + facts = { + "wrap address passes addr_limb_ok(·, 63)": addr_limb_ok(wrap, 63), + "u64 form skips the guard (accepts)": operands_disjoint_u64_buggy(wrap, wrap), + "u128 form catches it (rejects)": not operands_disjoint(wrap, wrap), + "the overlap is total, not marginal": True, # addr_k == addr_xg + } + # and the whole wrapping band, not just one address + band = [a for a in range(2**64 - 64, 2**64) + if addr_limb_ok(a, 63) and operands_disjoint_u64_buggy(a, a) + and not operands_disjoint(a, a)] + facts["the band is non-empty"] = len(band) > 0 + bad = [k for k, v in facts.items() if not v] + report("A4e control [u64 wrap in the overlap guard]", + "SAT — FORGES" if not bad else "FAIL", + f"{len(band)} reachable addresses in [2^64−64, 2^64) pass addr_limb_ok, wrap the " + "pre-fix `+64`, and slip a TOTAL operand overlap past the guard ⇒ the u128 " + "widening is LOAD-BEARING" + if not bad else f"failed: {bad}") + return not bad + + +# ── A4f: timestamps ────────────────────────────────────────────────────── + +def a4f_timestamps(): + """The four sub-timestamps and their stride. `xG` and `yG` are both read at `ts` — legal, + because they sit at disjoint addresses inside the same buffer, and MEMW only forbids the + same address at two timestamps. `yR`'s write takes `ts + 3`, the last free slot before the + next instruction's `ts + 4`.""" + slots = {"xG read": TS_XG_READ, "yG read": TS_XG_READ, "k read": TS_K_READ, + "xR write": TS_XR_WRITE, "yR write": TS_YR_WRITE} + yg_addrs = set() + for off in AFFINE_YG_READ_OFFSETS: + yg_addrs |= {off + b for b in range(DWORD)} + xg_addrs = set() + for off in XONLY_XG_READ_OFFSETS: + xg_addrs |= {off + b for b in range(DWORD)} + facts = { + "all slots < the instruction stride": max(slots.values()) < INSTRUCTION_TS_STRIDE, + "yR takes the last free slot": TS_YR_WRITE == INSTRUCTION_TS_STRIDE - 1, + "xG and yG share ts but not an address": not (xg_addrs & yg_addrs), + "xG‖yG jointly cover [0, 64)": xg_addrs | yg_addrs == set(range(64)), + "the three distinct read/write times are distinct": + len({TS_XG_READ, TS_K_READ, TS_XR_WRITE, TS_YR_WRITE}) == 4, + } + bad = [k for k, v in facts.items() if not v] + report("A4f timestamp layout", "PROVED" if not bad else "FAIL", + f"slots {slots} within stride {INSTRUCTION_TS_STRIDE}; xG@ts and yG@ts are " + "address-disjoint so the same-timestamp reads are legal" + if not bad else f"failed: {bad}") + return not bad + + +# ── A4g: why the bound must be mode-dependent ──────────────────────────── + +def a4g_completeness(): + """The bound could have been a flat 64-byte one, which is *sound* — but it would reject + x-only addresses the executor accepts, i.e. break completeness on a path this PR is not + supposed to touch. Measured: 32 such addresses per operand. + + Conversely a flat 32-byte bound leaves the affine band open (A4c), so neither constant + works alone and the `IS_AFFINE` interpolation is doing real work.""" + flat64_rejects_legal_xonly = [ + lo for lo in range(LIMB - 64, LIMB) + if addr_limb_ok(lo, 31) and not (lo < ADDR_LIMB_BOUND_64B)] + flat32_leaves_affine_open = [ + lo for lo in range(LIMB - 64, LIMB) + if not addr_limb_ok(lo, 63) and lo < ADDR_LIMB_BOUND_32B] + ok = len(flat64_rejects_legal_xonly) > 0 and len(flat32_leaves_affine_open) > 0 + report("A4g mode-dependent bound is necessary", "PROVED" if ok else "FAIL", + f"a flat 64-byte bound would reject {len(flat64_rejects_legal_xonly)} legal " + f"x-only addresses (completeness); a flat 32-byte bound would admit " + f"{len(flat32_leaves_affine_open)} illegal affine ones (soundness) ⇒ the " + "IS_AFFINE interpolation is load-bearing in BOTH directions") + return ok + + +def main(): + a4a_bound_matches_executor() + a4b_span_safe() + a4c_band() + a4c_band_is_closed() + a4d_scalar_bound() + a4e_overlap_guard() + a4e_wrap_control() + a4f_timestamps() + a4g_completeness() + + print("\nSummary:") + for n, v, _ in results: + print(f" {v:14} {n}") + bad = [n for n, v, _ in results if v not in ("PROVED", "SAT — FORGES")] + if bad: + print("\nUNEXPECTED: " + ", ".join(bad)) + return 1 if bad else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/gate/a6_real_witness.py b/docs/verification/ecsm-affine/gate/a6_real_witness.py new file mode 100644 index 000000000..ec52321a1 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/a6_real_witness.py @@ -0,0 +1,280 @@ +"""A6 — the real-witness anchor: evaluate the transcribed model on witnesses produced by the +REPO's own generator. + +The earlier board's rule, and a good one: no UNSAT is trusted until the transcribed model has +been evaluated on real prover witnesses. A model that is *stronger* than the chip yields UNSAT +where the chip is forgeable, and no amount of solver work notices — but a real witness that +fails the model does. + +Two independent things are being anchored: + + * **the FUNCTION** — the Python oracle is a from-scratch reimplementation, so agreement + means the gate reasons about the right scalar multiplication; + * **the COLUMNS** — this file, which reads `ecsm::compute_witness{,_with_y}`'s actual output + and re-derives every witness field the model consumes. + +It also carries the campaign's most direct exhibit: the parity forgery, produced by the repo's +own witness generator rather than by the model. For every scalar, `compute_witness_with_y` +accepts BOTH roots of `xG³ + b` and returns two complete, internally consistent witnesses with +the same `x_r` and different `y_r`. Nothing in `crypto/ecsm` objects, and nothing in the AIR's +arithmetic objects either (A3b) — which is exactly why the `IS_AFFINE`-gated `yG` read has to +exist. + +Input: `logs/real_witnesses.jsonl`, produced by + + cd ../harness && cargo run --release -- > ../gate/logs/real_witnesses.jsonl + +Run: `python a6_real_witness.py` +""" + +import json +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).parent)) +sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "oracle")) +from affine_common import ( # noqa: E402 + CARRY_OFFSET_X2, + CARRY_OFFSET_YG, + CURVE_B, + N, + P, + eval_overflow_chain_concrete, + honest_conv_carries, + le_bytes, + s_ecsm_x2, + s_ecsm_yg, +) +from ecsm_affine_ref import affine_mul, is_on_curve, recover_y_canonical, x_only_mul # noqa: E402 + +WITNESSES = Path(__file__).parent / "logs" / "real_witnesses.jsonl" +results = [] + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:12}] {name} {detail}") + + +def le_hex(h): + """The harness emits little-endian byte hex; recover the integer.""" + return int.from_bytes(bytes.fromhex(h), "little") + + +def load(): + if not WITNESSES.exists(): + return None + out = [] + for line in WITNESSES.read_text().splitlines(): + line = line.strip() + if line: + out.append(json.loads(line)) + return out + + +# ── the per-witness check ────────────────────────────────────────────────── + +def check_witness(w): + """Re-derive every field the gate's model reads. Returns a list of failures.""" + k = le_hex(w["k"]) + xg, yg = le_hex(w["x_g"]), le_hex(w["y_g"]) + xr, yr = le_hex(w["x_r"]), le_hex(w["y_r"]) + x2, q0, q1 = le_hex(w["x2"]), le_hex(w["q0"]), le_hex(w["q1"]) + bad = [] + + # 1. the oracle agrees with the repo + if w["mode"] == "x-only": + if x_only_mul(k, xg) != xr: + bad.append("oracle x_only_mul disagrees with x_r") + if recover_y_canonical(xg) != yg: + bad.append("x-only y_g is not the canonical even lift") + else: + if affine_mul(k, xg, yg) != (xr, yr): + bad.append("oracle affine_mul disagrees with (x_r, y_r)") + if not is_on_curve((xg, yg)): + bad.append("input point not on curve") + if not is_on_curve((xr, yr)): + bad.append("output point not on curve") + + # 2. the three pre-existing overflow addends, plus the NEW y_r_sub_p + for field, const, value in [("x_g_sub_p", P, xg), ("k_sub_n", N, k), + ("x_r_sub_p", P, xr), ("y_r_sub_p", P, yr)]: + want = (2**256 + value - const) % 2**256 + if le_hex(w[field]) != want: + bad.append(f"{field} != (2^256 + value − const) mod 2^256") + _, ok = eval_overflow_chain_concrete(const, value, + sum_is_bits=(field == "k_sub_n")) + if not ok: + bad.append(f"overflow chain {field}: some c_i ∉ {{0,1}} or c_7 != 1") + + # 3. the two convolution relations and their carry windows + xg_b, yg_b, x2_b = le_bytes(xg), le_bytes(yg), le_bytes(x2) + q0_b = le_bytes(q0) + q1_b = [(q1 >> (8 * j)) & 0xFF for j in range(33)] + if x2 != xg * xg % P: + bad.append("x2 != xG² mod p") + if q0 != (xg * xg - x2) // P: + bad.append("q0 != (xG² − x2)/p") + if q1 != (yg * yg + P * P - x2 * xg - CURVE_B) // P: + bad.append("q1 != (yG² + p² − x2·xG − b)/p") + c0, exact0 = honest_conv_carries([s_ecsm_x2(xg_b, q0_b, x2_b, i) for i in range(64)]) + c1, exact1 = honest_conv_carries( + [s_ecsm_yg(yg_b, x2_b, xg_b, q1_b, i, 1) for i in range(64)]) + if not exact0: + bad.append("X2 relation: inexact carry or c_63 != 0") + if not exact1: + bad.append("Yg relation: inexact carry or c_63 != 0") + if not all(0 <= c + CARRY_OFFSET_X2 < 1 << 16 for c in c0[:63]): + bad.append("c0 escapes its IsHalfword window") + if not all(0 <= c + CARRY_OFFSET_YG < 1 << 16 for c in c1[:63]): + bad.append("c1 escapes its IsHalfword window") + if q1_b[32] not in (0, 1): + bad.append("q1[32] is not a bit") + + # 4. len_k + if w["len_k"] != k.bit_length() - 1: + bad.append("len_k != MSB(k)") + # 5. the ECDAS step count: one per double, plus one per set bit below the MSB + want_steps = 0 if k.bit_length() <= 1 else ( + k.bit_length() - 1 + bin(k)[3:].count("1")) + if w["steps"] != want_steps: + bad.append(f"steps {w['steps']} != expected {want_steps}") + return bad + + +def a6a_witnesses(rows): + accepted = [r for r in rows if "error" not in r] + rejected = [r for r in rows if "error" in r] + failures = {} + n_checks = 0 + for r in accepted: + bad = check_witness(r) + n_checks += 1 + if bad: + failures[f"{r['label']}/{r['mode']}"] = bad + report("A6a real-witness evaluation", "PROVED" if not failures else "FAIL", + f"{n_checks} witnesses from ecsm::compute_witness{{,_with_y}}: oracle agreement, " + "all four overflow chains, both convolution relations, carry windows, len_k and " + "the ECDAS step count all re-derived" + if not failures else f"failures: {dict(list(failures.items())[:3])}") + return not failures, accepted, rejected + + +def a6b_rejections(rejected): + """The executor's accept/reject set, from the repo's own generator.""" + want = { + "k=0": "non-zero", + "k=N": "< N", + "off-curve yG": "curve", + "yG=p": "< p", + } + got = {r["label"]: r["error"] for r in rejected} + ok = set(got) == set(want) + report("A6b rejections match the oracle", "PROVED" if ok else "FAIL", + f"{len(got)} rejected by crypto/ecsm: {got}" if ok + else f"expected {sorted(want)}, got {sorted(got)}") + return ok + + +def a6c_parity_forgery_from_the_repo(accepted): + """The campaign's central exhibit, sourced from the repo rather than the model: for every + scalar, `compute_witness_with_y` accepts BOTH roots and returns two valid witnesses with + the same `x_r` and a different `y_r`.""" + by_label = {} + for r in accepted: + by_label.setdefault(r["label"], {})[r["mode"]] = r + pairs = [(lab, v["affine/+y"], v["affine/-y"]) for lab, v in by_label.items() + if "affine/+y" in v and "affine/-y" in v] + facts = { + "at least one pair present": len(pairs) > 0, + "both roots always accepted": all( + "error" not in a and "error" not in b for _, a, b in pairs), + "same x_r in every pair": all(a["x_r"] == b["x_r"] for _, a, b in pairs), + "different y_r in every pair": all(a["y_r"] != b["y_r"] for _, a, b in pairs), + "y_r values are negatives mod p": all( + (le_hex(a["y_r"]) + le_hex(b["y_r"])) % P == 0 for _, a, b in pairs), + "different q1 in every pair": all(a["q1"] != b["q1"] for _, a, b in pairs), + "identical x2 / q0 (they depend on xG alone)": all( + a["x2"] == b["x2"] and a["q0"] == b["q0"] for _, a, b in pairs), + "both y_r canonical (YrLtP accepts either)": all( + le_hex(a["y_r"]) < P and le_hex(b["y_r"]) < P for _, a, b in pairs), + } + bad = [k for k, v in facts.items() if not v] + report("A6c parity forgery from the repo's generator", + "SAT — FORGES" if not bad else "FAIL", + f"{len(pairs)} ±yG witness pairs out of crypto/ecsm itself: every one is valid, " + f"agrees on x_r, and publishes a different y_r ⇒ the gap A3 proves is not a " + "modelling artefact" + if not bad else f"failed: {bad}") + return not bad + + +def a6d_xonly_equals_even_lift(accepted): + """`G`'s y is even, so the x-only witness and the `affine/+y` witness over `G` must be + IDENTICAL, field for field. If they diverged, the two paths would not be the same chip and + A3e's "x-only is untouched" would be false.""" + by_label = {} + for r in accepted: + by_label.setdefault(r["label"], {})[r["mode"]] = r + fields = ["x_g", "y_g", "x_r", "y_r", "x_g_sub_p", "k_sub_n", "x_r_sub_p", + "y_r_sub_p", "x2", "q0", "q1", "len_k", "steps"] + n = 0 + ok = True + for lab, v in by_label.items(): + if "x-only" in v and "affine/+y" in v: + if le_hex(v["x-only"]["x_g"]) != le_hex(v["affine/+y"]["x_g"]): + continue # different base point (the small-y instance) + ok &= all(v["x-only"][f] == v["affine/+y"][f] for f in fields) + n += 1 + report("A6d x-only == affine with the even lift", "PROVED" if ok and n else "FAIL", + f"{n} labels over G (whose y is even): all {len(fields)} witness fields identical " + "⇒ the affine variant is the same chip, not a parallel one") + return ok and n > 0 + + +def a6e_small_y_instance(accepted): + """The `y = 1` instance reached through the repo's generator: `y_r` really is 1, and its + `y_r_sub_p` sits at the extreme of the addend range — the exact witness A2's forgery + perturbs.""" + hit = [r for r in accepted if r["label"].startswith("small-y")] + if not hit: + report("A6e small-y instance", "FAIL", "instance missing from the dump") + return False + r = hit[0] + yr = le_hex(r["y_r"]) + addend = le_hex(r["y_r_sub_p"]) + ok = (yr == 1 and addend == (2**256 + 1 - P) % 2**256 + and yr + P < 2**256) + report("A6e small-y instance", "PROVED" if ok else "FAIL", + f"crypto/ecsm returns y_r = {yr} for the constructed point; y_r_sub_p = " + f"0x{addend:x} = 2^256 + 1 − p, and y_r + p < 2^256 ⇒ the A2 forgery's premise " + "holds against the real generator") + return ok + + +def main(): + rows = load() + if rows is None: + report("A6 real-witness anchor", "SKIP", + f"{WITNESSES.relative_to(Path(__file__).parent)} not found — run " + "`cd ../harness && cargo run --release -- > ../gate/logs/real_witnesses.jsonl`") + print("\nA6 SKIPPED: the anchor is NOT established without the harness dump.") + return 0 + + ok, accepted, rejected = a6a_witnesses(rows) + a6b_rejections(rejected) + a6c_parity_forgery_from_the_repo(accepted) + a6d_xonly_equals_even_lift(accepted) + a6e_small_y_instance(accepted) + + print("\nSummary:") + for n, v, _ in results: + print(f" {v:14} {n}") + bad = [n for n, v, _ in results if v not in ("PROVED", "SAT — FORGES", "SKIP")] + if bad: + print("\nUNEXPECTED: " + ", ".join(bad)) + return 1 if bad else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/gate/affine_common.py b/docs/verification/ecsm-affine/gate/affine_common.py new file mode 100644 index 000000000..ae142234b --- /dev/null +++ b/docs/verification/ecsm-affine/gate/affine_common.py @@ -0,0 +1,347 @@ +"""Shared model for the ECSM **affine-selector** z3 gate. + +Ground truth: `prover/src/tables/ecsm.rs` on branch `verify/ecsm-affine-selector` +(head of PR #879), plus `executor/src/vm/instruction/execution.rs` for the ABI predicates. +Every builder below carries the `file:line` it was transcribed from; the audit that checks +those citations still say what the builder assumes is `TRANSCRIPTION-AUDIT.md`. + +Scope. This board covers ONLY the surface PR #879 adds or changes: + + * the `IS_AFFINE` selector column and its two constraints (idx 421, 422), + * its `Ecall`-bus pinning (`syscall = xonly + IS_AFFINE·(affine − xonly)`), + * the `IS_AFFINE`-gated `yG` read and `yR` write, and their `+32 + 8i` offsets, + * the new `OverflowKind::YrLtP` carry chain (idx 413..420), + * the `Alu`-LT address-limb senders and their mode-dependent bound. + +The pre-existing chip — the curve relations, the ECDAS chain, the double-and-add +induction — is already proved by the earlier board, which this one deliberately does not +re-derive: + + thoughts/ec-recover-opt/gate/RESULTS.md on branch feat/ec-lincomb2, commit 1d2b4dd7 + (unmerged: that path exists on that branch only, never on main) + +Its lemmas L1–L7 and contracts C1–C7 are IMPORTED here as hypotheses and listed as such in +`RESULTS.md`. Two of them the affine change stresses in a new way, so they are re-examined +rather than imported blind: + + * L7 concluded `xR = x(k·P)` "for both yG sign classes", explicitly BECAUSE `yG`'s parity + was unobservable. Publishing `yR` breaks that premise — see a3_parity_binding.py. + * C4 (MEMW byte authority) listed `YR` as inheriting byte-ness "from tuple equality with + ECDAS's byte-checked yR (or YG for k=1)". `YrLtP` now *consumes* that byte contract, so + it is checked rather than assumed — see a2_yr_lt_p.py's C4-YR probe. + +The same builders serve three purposes, as in the earlier board: exact interval bounds, +z3 constraint models, and concrete evaluation of real witnesses — so a transcription error +shows up in the concrete evaluation before any UNSAT is trusted. +""" + +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).resolve().parents[1] / "oracle")) + +from ecsm_affine_ref import N, P # noqa: E402 (the oracle is the reference, not the repo) + +# ── field / template constants ─────────────────────────────────────────────── + +PG = 2**64 - 2**32 + 1 # Goldilocks; all AIR constraints are enforced mod PG +SHIFT_32 = 2**32 +# prover/src/constraints/templates.rs:26 +INV_SHIFT_32 = 18446744065119617026 +assert INV_SHIFT_32 * SHIFT_32 % PG == 1, "INV_SHIFT_32 is not 2^-32 mod p_g" + +P_BYTES = list(P.to_bytes(32, "little")) +N_BYTES = list(N.to_bytes(32, "little")) + +# ── syscall numbers (executor/src/vm/instruction/execution.rs:38, 47) ──────── + +ECSM_SYSCALL_NUMBER = 2**64 - 1 - 10 # u64::MAX - 10, x-only +ECSM_AFFINE_SYSCALL_NUMBER = 2**64 - 1 - 11 # u64::MAX - 11, affine + +# EVERY syscall number the CPU can put on the `Ecall` bus (execution.rs:29, 40, 48, 69). +# A1f needs the whole set, not just the ECSM pair: the receiver's syscall word is LINEAR in +# IS_AFFINE with low-word coefficient −1 and high-word coefficient 0, so as `IS_AFFINE` ranges +# over the field the received low word ranges over the WHOLE field while the high word stays +# fixed — which means every other syscall's tuple is reachable at some value of `IS_AFFINE`. +# `IS_BIT(IS_AFFINE)` is what confines it to {0, 1}. Audit premise P19 keeps this set in sync. +SYSCALL_NUMBERS = { + "KECCAK": 2**64 - 1 - 1, + "ECSM": ECSM_SYSCALL_NUMBER, + "ECSM_AFFINE": ECSM_AFFINE_SYSCALL_NUMBER, + "HINT": 2**64 - 1 - 30, +} + +# ── address-limb bounds (prover/src/tables/ecsm.rs:43, 47) ────────────────── + +ADDR_LIMB_BOUND_32B = (1 << 32) - 31 +ADDR_LIMB_BOUND_64B = (1 << 32) - 63 + +# ── the affine memory-op layout (ecsm.rs, the two `for i in 0..4` blocks) ─── +# +# yG read : 4 doublewords at ADDR_XG_0 + 32 + 8i, high limb ADDR_XG_1, ts (mult IS_AFFINE) +# yR write: 4 doublewords at ADDR_XR_0 + 32 + 8i, high limb ADDR_XR_1, ts + 3 (mult IS_AFFINE) +# +# The pre-existing x-only ops, for the offset-collision audit: +# xG read : 4 dwords at ADDR_XG_0 + 8i, ts ; k read : ADDR_K_0 + 8i, ts + 1 +# xR write: 4 dwords at ADDR_XR_0 + 8i, ts + 2 +AFFINE_YG_READ_OFFSETS = [32 + 8 * i for i in range(4)] +AFFINE_YR_WRITE_OFFSETS = [32 + 8 * i for i in range(4)] +XONLY_XG_READ_OFFSETS = [8 * i for i in range(4)] +XONLY_XR_WRITE_OFFSETS = [8 * i for i in range(4)] +DWORD = 8 + +TS_XG_READ, TS_K_READ, TS_XR_WRITE, TS_YR_WRITE = 0, 1, 2, 3 +INSTRUCTION_TS_STRIDE = 4 # cpu.rs: one instruction consumes 4 sub-timestamps + + +# ── the Ecall syscall-word model (ecsm.rs, `syscall_word` closure) ────────── + +def syscall_word_lo(is_affine): + """`xonly_lo + IS_AFFINE·(affine_lo − xonly_lo)`, the low 32-bit word the ECSM row + puts on the `Ecall` bus (ecsm.rs, ECALL receiver). Linear in IS_AFFINE by design so + one receiver serves both modes.""" + lo_x = ECSM_SYSCALL_NUMBER & 0xFFFF_FFFF + lo_a = ECSM_AFFINE_SYSCALL_NUMBER & 0xFFFF_FFFF + return lo_x + is_affine * (lo_a - lo_x) + + +def syscall_word_hi(is_affine): + """Same for the high word. Today both numbers share `0xFFFF_FFFF`, so the IS_AFFINE + coefficient is ZERO and this word carries no mode information — which is exactly what + the `const _: () = assert!` in execution.rs:53-58 exists to keep true-by-accident from + becoming true-by-nobody-noticing.""" + hi_x = ECSM_SYSCALL_NUMBER >> 32 + hi_a = ECSM_AFFINE_SYSCALL_NUMBER >> 32 + return hi_x + is_affine * (hi_a - hi_x) + + +def addr_bound_by_mode(is_affine): + """`ADDR_LIMB_BOUND_32B + IS_AFFINE·(BOUND_64B − BOUND_32B)`, the RHS of the `Alu` LT + senders for `ADDR_XG_0` and `ADDR_XR_0` (ecsm.rs, `addr_bound_by_mode`). `ADDR_K_0` + uses the flat 32-byte bound in both modes.""" + return ADDR_LIMB_BOUND_32B + is_affine * (ADDR_LIMB_BOUND_64B - ADDR_LIMB_BOUND_32B) + + +# ── the overflow carry chain (ecsm.rs, `EcsmConstraints::carry_chain`) ────── + +OVERFLOW_KINDS = { + # kind const addend sum stored as + "XgLtP": (P, "bytes"), + "KLtN": (N, "bits"), + "XrLtP": (P, "bytes"), + "YrLtP": (P, "bytes"), # NEW in PR #879 (idx 413..420) +} + + +def const_word(const_value, i): + """`OverflowKind::const_word(i)`: 32-bit word `i` of the constant addend, assembled + from its little-endian bytes (ecsm.rs, `const_word`).""" + return (const_value >> (32 * i)) & 0xFFFF_FFFF + + +def addend1_word(halfwords, i): + """`hl[2i] + 2^16·hl[2i+1]` — word `i` of the witnessed halfword addend + (`XG_SUB_P` / `K_SUB_N` / `XR_SUB_P` / `YR_SUB_P`).""" + return halfwords[2 * i] + halfwords[2 * i + 1] * (1 << 16) + + +def sum_word_bytes(byte_cols, i): + """Word `i` of a byte-stored sum (`XG` / `XR` / `YR`): bytes 4i..4i+3.""" + s = 0 + for byte in range(4): + s = s + byte_cols[4 * i + byte] * (1 << (8 * byte)) + return s + + +def sum_word_bits(bit_cols, i): + """Word `i` of the bit-stored sum (`K`): bits 32i..32i+31.""" + s = 0 + for bit in range(32): + s = s + bit_cols[32 * i + bit] * (1 << bit) + return s + + +def carry_chain(const_value, halfwords, sum_cols, sum_is_bits=False, inv=INV_SHIFT_32): + """The eight VIRTUAL carries, as expressions in the leaves: + + c_i = (const_word_i + addend1_i + c_{i−1} − sum_i) · 2^{−32} + + Returned in order; `c[7]` is the carry-out the `OverflowRequired` constraint pins to 1. + `inv` is a parameter only so a negative control can perturb it.""" + c = [] + prev = 0 + for i in range(8): + a1 = addend1_word(halfwords, i) + s = sum_word_bits(sum_cols, i) if sum_is_bits else sum_word_bytes(sum_cols, i) + ci = (const_word(const_value, i) + a1 + prev - s) * inv + c.append(ci) + prev = ci + return c + + +def overflow_constraints(mu, c): + """The nine emitted constraints per `OverflowKind`, as expressions that must vanish: + `µ·c_i·(1−c_i)` for i ∈ 0..6, then `µ·(1−c_7)` (ecsm.rs, the `for kind in [...]` loop). + + Note what is NOT here: there is no `µ·c_7·(1−c_7)`. `c_7` is pinned to the constant 1 + outright, which is stronger, so the missing bit constraint is not a gap.""" + out = [mu * c[i] * (1 - c[i]) for i in range(7)] + out.append(mu * (1 - c[7])) + return out + + +# ── the two new selector constraints (ecsm.rs idx 421, 422) ──────────────── + +def is_bit_is_affine(is_affine): + """idx 421 — `IS_AFFINE·(1 − IS_AFFINE)`.""" + return is_affine * (1 - is_affine) + + +def affine_zero_on_padding(is_affine, mu): + """idx 422 — `IS_AFFINE·(1 − µ)`.""" + return is_affine * (1 - mu) + + +# ── honest witness generation (mirrors crypto/ecsm/src/witness.rs) ────────── + +def y_sub_p_halfwords(value): + """`(value − p) mod 2^256` as 16 little-endian halfwords — the honest `YR_SUB_P` + witness (`witness.rs`: `to_le_32(&((&two_256 + &result.y) - p()))`).""" + v = (2**256 + value - P) % 2**256 + return [(v >> (16 * j)) & 0xFFFF for j in range(16)] + + +def le_bytes(value, n=32): + return [(value >> (8 * j)) & 0xFF for j in range(n)] + + +def le_bits(value, n=256): + return [(value >> j) & 1 for j in range(n)] + + +# ── the two pre-existing ECSM curve relations ─────────────────────────────── +# +# IMPORTED, not newly derived: these are the earlier board's `s_ecsm_x2` / `s_ecsm_yg` / +# `conv_carry` (thoughts/ec-recover-opt/gate/gate_common.py, branch feat/ec-lincomb2), and +# they were re-read against `prover/src/tables/ecsm.rs`'s `s_i` / `conv_carry` on THIS branch +# — where the bodies are byte-identical to main, since PR #879 does not touch them. +# +# They are here only because A3 needs to evaluate the FULL in-table constraint set on a +# forged witness. Establishing that these relations pin `yG² ≡ xG³ + b` is the earlier +# board's L3a/L4; this board consumes that. + +CARRY_OFFSET_X2 = 8160 # ecsm.rs:37 +CARRY_OFFSET_YG = 16319 # ecsm.rs:38 +CURVE_B = 7 + + +def _at(arr, length, j): + """`byte_at`: zero-padding past the operand's length (ecsm.rs, `byte_at`).""" + return arr[j] if 0 <= j < length else 0 + + +def s_ecsm_x2(xg, q0, x2, i): + """`Relation::X2` at limb i: `Σ xG_j·xG_{i−j} − x2_i − Σ q0_j·P_{i−j}`.""" + s = 0 + for j in range(i + 1): + s += _at(xg, 32, j) * _at(xg, 32, i - j) + s -= _at(q0, 32, j) * _at(P_BYTES, 32, i - j) + return s - _at(x2, 32, i) + + +def s_ecsm_yg(yg, x2, xg, q1, i, mu=1): + """`Relation::Yg` at limb i: + `Σ(yG_j·yG_{i−j} − x2_j·xG_{i−j} − q1_j·P_{i−j}) + µ·Σ P_j·P_{i−j} − µ·b·[i=0]`. + `q1` is 33 bytes; its top byte is IS_BIT-constrained.""" + s = 0 + p2 = 0 + for j in range(i + 1): + s += _at(yg, 32, j) * _at(yg, 32, i - j) + p2 += _at(P_BYTES, 32, j) * _at(P_BYTES, 32, i - j) + s -= _at(x2, 32, j) * _at(xg, 32, i - j) + s -= _at(q1, 33, j) * _at(P_BYTES, 32, i - j) + s += mu * p2 + if i == 0: + s -= mu * CURVE_B + return s + + +def honest_conv_carries(s_values): + """The honest carry array for a convolution relation: `c_i = (c_{i−1} + S_i)/256`, + the exact-division solution of `256·c_i − c_{i−1} − S_i = 0`. Returns + `(carries, exact)`; `exact` also requires the chain to close at `c_63 = 0`, which is the + `ColIsZero` constraint the earlier board's N3 found load-bearing.""" + c = [] + prev = 0 + exact = True + for s in s_values: + total = prev + s + if total % 256 != 0: + exact = False + prev = total // 256 + c.append(prev) + return c, exact and prev == 0 + + +# ── field-root machinery ──────────────────────────────────────────────────── +# +# The `IS_BIT`-shaped constraints (`x·(1−x) ≡ 0 mod p_g`) are statements about ROOTS OF A +# POLYNOMIAL OVER A FIELD, and that is how they are discharged here: sympy factors the +# polynomial over GF(p_g) and the factorisation is checked to be complete (total degree of +# the linear factors == degree of the polynomial), so no root is missed. +# +# Handing the lifted integer form `x(1−x) = m·p_g` to z3 instead does NOT terminate on +# constants this size — the query is nonlinear integer arithmetic with a free quotient. +# Recorded in RESULTS.md's method note so nobody re-attempts it. + +def certify_pg_prime(): + """p_g = 2^64 − 2^32 + 1 is prime. The one assumed-then-certified algebraic fact this + board needs (the analogue of the earlier board's A-PRIME).""" + import sympy + + return bool(sympy.isprime(PG)) + + +def field_roots(coeffs, modulus=None): + """Roots over GF(`modulus`) of the polynomial with the given coefficients, highest degree + first, together with a completeness flag. `modulus` defaults to the Goldilocks prime + `p_g`, the field the AIR is enforced over; the curve-side lemmas pass `p` instead. + + Returns `(roots, complete)`. `complete` is True when the linear factors account for the + full degree, i.e. the polynomial splits and the root list is exhaustive. A degree-`d` + polynomial over a field has at most `d` roots, so a complete split is a proof that the + returned set is ALL of them. + + sympy's `modulus=` uses the SYMMETRIC residue range, so factor coefficients come back + possibly negative; roots are normalised into `[0, modulus)` here.""" + import sympy + from sympy.abc import x + + q = PG if modulus is None else modulus + poly = sympy.Poly(sum(c * x**i for i, c in enumerate(reversed(coeffs))), x, modulus=q) + _, factors = poly.factor_list() + roots = {} + linear_degree = 0 + for f, mult in factors: + if f.degree() == 1: + a, b = (int(v) for v in f.all_coeffs()) # a·x + b + roots[(-b * pow(a, -1, q)) % q] = mult + linear_degree += mult + return roots, linear_degree == poly.degree() + + +def eval_overflow_chain_concrete(const_value, value, sum_is_bits=False, + addend_value=None): + """Evaluate the carry chain on a CONCRETE honest witness, over F_pg, and return + `(carries, ok)` where ok means: every c_i ∈ {0,1} and c_7 == 1. + + `addend_value` overrides the honest `(value − const) mod 2^256` addend, which is how + the negative controls inject a forged representation.""" + if addend_value is None: + addend_value = (2**256 + value - const_value) % 2**256 + hl = [(addend_value >> (16 * j)) & 0xFFFF for j in range(16)] + cols = le_bits(value) if sum_is_bits else le_bytes(value) + c = carry_chain(const_value, hl, cols, sum_is_bits) + c = [ci % PG for ci in c] + ok = all(ci in (0, 1) for ci in c) and c[7] == 1 + return c, ok diff --git a/docs/verification/ecsm-affine/gate/audit_transcription.py b/docs/verification/ecsm-affine/gate/audit_transcription.py new file mode 100644 index 000000000..25447a5d7 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/audit_transcription.py @@ -0,0 +1,488 @@ +"""A5 — the transcription audit: does the gate's model match the code it claims to model? + +This is the pass the BLAKE3 campaign identified as highest-value and the EC campaign proved +the point with — its equivalent audit +(`thoughts/ec-recover-opt/gate/TRANSCRIPTION-AUDIT.md`, branch feat/ec-lincomb2) "found three +premises the gate asserted about the chip and never read, one of them hiding a working +forgery". + +The dangerous direction is a model STRONGER than the object it models: it yields UNSAT where +the real chip is forgeable, and no positive anchor can catch it, because honest witnesses +satisfy a correct model and an over-strong one equally well. So every premise the lemma +scripts rely on is listed here as a `Premise` and CHECKED against the source text — not +re-derived, read. + +Two kinds of entry: + + * **assumed** — the model relies on this being true of the code. Failing one invalidates + a lemma. + * **negative-space** — the model relies on something being ABSENT (e.g. "nothing constrains + `yG`'s parity"). These are the ones a reader cannot verify by looking at what is written, + so they are the ones most worth mechanising. + +Each premise is also MUTATION-TESTED: the source is perturbed in memory and the premise must +then fail. A premise whose check passes on mutated source is checking nothing, which is the +failure mode this file exists to prevent. + +Run: `python audit_transcription.py` +""" + +import re +import sys +from dataclasses import dataclass, field +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).parent)) +from affine_common import ( # noqa: E402 + ADDR_LIMB_BOUND_32B, + ADDR_LIMB_BOUND_64B, + CARRY_OFFSET_X2, + CARRY_OFFSET_YG, + ECSM_AFFINE_SYSCALL_NUMBER, + ECSM_SYSCALL_NUMBER, + INSTRUCTION_TS_STRIDE, + SYSCALL_NUMBERS, +) + + +def find_repo_root(start=None): + """Walk up until a directory looks like the lambda_vm root (a workspace `Cargo.toml` + next to `prover/`). + + Deliberately NOT `parents[N]`. A hard-coded depth breaks silently when the campaign + moves — and this audit reads repo source by path, so a wrong root would report premises + against the wrong tree. (It happens to fail loudly here, because `load_sources` checks + existence and names every missing file, but a marker walk removes the hazard instead of + relying on the guard.)""" + here = (start or Path(__file__)).resolve() + for cand in here.parents: + if (cand / "Cargo.toml").is_file() and (cand / "prover").is_dir(): + if "[workspace]" in (cand / "Cargo.toml").read_text(): + return cand + raise RuntimeError(f"no lambda_vm repo root above {here}") + + +REPO = find_repo_root() +ECSM_RS = REPO / "prover" / "src" / "tables" / "ecsm.rs" +EXEC_RS = REPO / "executor" / "src" / "vm" / "instruction" / "execution.rs" +WITNESS_RS = REPO / "crypto" / "ecsm" / "src" / "witness.rs" +TEMPLATES_RS = REPO / "prover" / "src" / "constraints" / "templates.rs" +TRACE_BUILDER_RS = REPO / "prover" / "src" / "tables" / "trace_builder.rs" + +results = [] + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:10}] {name} {detail}") + + +@dataclass +class Premise: + """One thing the gate assumes about the code.""" + key: str + lemma: str # which lemma consumes it + what: str # the assumption, in words + check: object # (sources) -> (ok, detail) + kind: str = "assumed" # or "negative-space" + mutations: list = field(default_factory=list) # (file, pattern, replacement, why) + + +def _src(sources, path): + return sources[path] + + +# ── the premises ──────────────────────────────────────────────────────────── + +def p_columns(s): + src = _src(s, ECSM_RS) + got = {n: int(m) for n, m in re.findall( + r"pub const (IS_AFFINE|YR_SUB_P|NUM_COLUMNS|MU): usize = (\d+);", src)} + want = {"MU": 666, "IS_AFFINE": 667, "YR_SUB_P": 668, "NUM_COLUMNS": 684} + ok = got == want and got["YR_SUB_P"] + 16 == got["NUM_COLUMNS"] + return ok, (f"{got}; YR_SUB_P + 16 halfwords = {got.get('YR_SUB_P', 0) + 16} == " + f"NUM_COLUMNS {got.get('NUM_COLUMNS')}") + + +def p_constraint_count(s): + src = _src(s, ECSM_RS) + m = re.search(r"debug_assert_eq!\(idx, (\d+)\);", src) + ok = m is not None and int(m.group(1)) == 423 + # and the header index map mentions the new blocks + ok &= "// 413..420 : CarryBit(YrLtP, 0..7)" in src + ok &= "// 421 : IS_BIT(IS_AFFINE)" in src + ok &= "// 422 : AffineZeroOnPadding" in src + return ok, f"idx closes at {m.group(1) if m else '?'} == 423; header map lists 413..422" + + +def p_addr_bounds(s): + src = _src(s, ECSM_RS) + b32 = re.search(r"ADDR_LIMB_BOUND_32B: u64 = \(1 << 32\) - (\d+);", src) + b64 = re.search(r"ADDR_LIMB_BOUND_64B: u64 = \(1 << 32\) - (\d+);", src) + ok = (b32 and b64 + and (1 << 32) - int(b32.group(1)) == ADDR_LIMB_BOUND_32B + and (1 << 32) - int(b64.group(1)) == ADDR_LIMB_BOUND_64B) + return ok, (f"2^32−{b32.group(1) if b32 else '?'} / 2^32−{b64.group(1) if b64 else '?'} " + "match the model's constants") + + +def p_syscall_numbers(s): + src = _src(s, EXEC_RS) + x = re.search(r"ECSM_SYSCALL_NUMBER: u64 = u64::MAX - (\d+);", src) + a = re.search(r"ECSM_AFFINE_SYSCALL_NUMBER: u64 = u64::MAX - (\d+);", src) + ok = (x and a + and 2**64 - 1 - int(x.group(1)) == ECSM_SYSCALL_NUMBER + and 2**64 - 1 - int(a.group(1)) == ECSM_AFFINE_SYSCALL_NUMBER) + return ok, f"u64::MAX−{x.group(1) if x else '?'} / u64::MAX−{a.group(1) if a else '?'}" + + +def p_lowword_assert(s): + """A1c's premise: the low-word inequality is guarded at COMPILE time, so a future + variant cannot silently un-pin `IS_AFFINE`.""" + src = _src(s, EXEC_RS) + ok = bool(re.search( + r"const _: \(\) = assert!\(\s*ECSM_SYSCALL_NUMBER & 0xFFFF_FFFF" + r"\s*!=\s*ECSM_AFFINE_SYSCALL_NUMBER & 0xFFFF_FFFF", src)) + return ok, "the low-32-bit-word inequality is a compile-time assert" + + +def p_syscall_word_linear(s): + """A1c's other premise: the Ecall receiver's syscall words really are + `xonly + IS_AFFINE·(affine − xonly)`, per word.""" + src = _src(s, ECSM_RS) + ok = ("let syscall_word = |xonly: i64, affine: i64|" in src + and "LinearTerm::Constant(xonly)" in src + and "coefficient: affine - xonly," in src + and "column: cols::IS_AFFINE," in src + and "syscall_word(xonly_lo, affine_lo)" in src + and "syscall_word(xonly_hi, affine_hi)" in src) + return ok, "both received words are the IS_AFFINE interpolation of the two numbers" + + +def p_affine_gated_buses(s): + """A1/A3's premise: the yG read and yR write fire with multiplicity IS_AFFINE, four + doublewords each, at `+32 + 8i`, and the yR write at `ts + 3`.""" + src = _src(s, ECSM_RS) + ok = "let affine = || Multiplicity::Column(cols::IS_AFFINE);" in src + ok &= src.count(" affine(),") == 2 # one per for-loop body + ok &= len(re.findall(r"LinearTerm::Constant\(\(32 \+ 8 \* i\) as i64\)", src)) == 2 + ok &= "memw_read(\n dword_bytes(cols::YG, i)," in src + ok &= "memw_write(\n dword_bytes(cols::YR, i)," in src + ok &= "ts_lo_plus(3)," in src + return ok, ("2 affine-gated bus blocks (4 dwords each), offsets +32+8i, yG via " + "memw_read at ts and yR via memw_write at ts+3") + + +def p_yrltp_wiring(s): + """A2's premise: `OverflowKind::YrLtP` uses `P_BYTES` as the constant, `YR_SUB_P` as the + halfword addend, `YR` as the byte-stored sum.""" + src = _src(s, ECSM_RS) + ok = ("OverflowKind::YrLtP => &P_BYTES," in src + and "OverflowKind::YrLtP => cols::YR_SUB_P," in src + and "OverflowKind::YrLtP => cols::YR," in src + and "fn sum_is_bits(self) -> bool {\n matches!(self, OverflowKind::KLtN)" in src) + return ok, "YrLtP → (P_BYTES, YR_SUB_P, YR), byte-stored sum (not bits)" + + +def p_yrltp_mu_gated(s): + """A2d's premise, and the reason it is an OBSERVATION rather than a bug: `YrLtP` sits in + the same `for kind in [...]` loop as the other three, so its constraints are µ-gated — + NOT IS_AFFINE-gated. It therefore binds on x-only rows too.""" + src = _src(s, ECSM_RS) + m = re.search(r"for kind in \[\s*OverflowKind::XgLtP,\s*OverflowKind::KLtN,\s*" + r"OverflowKind::XrLtP,\s*OverflowKind::YrLtP,\s*\] \{(.*?)\n \}", + src, re.S) + ok = m is not None + if ok: + body = m.group(1) + ok = ("let mu = b.main(0, cols::MU);" in body + and "mu * ci.clone() * (one - ci.clone())" in body + and "mu * (one - c[7].clone())" in body + and "cols::IS_AFFINE" not in body) + return ok, ("all four chains share one µ-gated loop; IS_AFFINE does not appear in it ⇒ " + "YrLtP binds x-only rows too (strictly stronger; A2d)") + + +def p_yr_sub_p_halfword_checks(s): + """A2's C2 premise: the 16 `YR_SUB_P` halfwords are IsHalfword-checked, µ-gated.""" + src = _src(s, ECSM_RS) + ok = bool(re.search( + r"for i in 0\.\.16 \{\s*out\.push\(BusInteraction::sender\(\s*BusId::IsHalfword," + r"\s*mu\(\),\s*vec!\[packed\(cols::yr_sub_p\(i\)\)\],", src)) + return ok, "16 µ-gated IsHalfword sends on yr_sub_p(i)" + + +def p_alu_lt_senders(s): + """A4's premise: three µ-gated `Alu` LT senders, xG/xR against the mode-dependent bound + and k against the flat one, each asserting `result = 1` with a literal zero high word.""" + src = _src(s, ECSM_RS) + ok = src.count("out.push(alu_lt(") == 3 + ok &= "out.push(alu_lt(packed(cols::ADDR_XG_0), addr_bound_by_mode()));" in src + ok &= "out.push(alu_lt(packed(cols::ADDR_XR_0), addr_bound_by_mode()));" in src + ok &= re.search(r"out\.push\(alu_lt\(\s*packed\(cols::ADDR_K_0\),\s*" + r"BusValue::constant\(ADDR_LIMB_BOUND_32B\),", src) is not None + ok &= "BusValue::constant(alu_op::LT as u64)" in src + ok &= re.search(r"let alu_lt = \|lhs_lo: BusValue, rhs_lo: BusValue\|", src) is not None + return ok, "3 senders: xG/xR vs addr_bound_by_mode(), k vs the flat 32-byte bound, LT/1" + + +def p_executor_abi(s): + """A4's premise about the executor arm: both 64-byte spans checked at 63, k at 31, and + the overlap guard computed in u128.""" + src = _src(s, EXEC_RS) + ok = bool(re.search(r"if !addr_limb_ok\(addr_xg, 63\)\s*\|\|\s*!addr_limb_ok\(addr_xr, 63\)" + r"\s*\|\|\s*!addr_limb_ok\(addr_k, 31\)", src)) + ok &= bool(re.search(r"if \(addr_k as u128\) < addr_xg as u128 \+ 64\s*" + r"&& \(addr_xg as u128\) < addr_k as u128 \+ 32", src)) + ok &= "load_u256_le(memory, addr_xg.wrapping_add(32))?" in src + ok &= "store_u256_le(memory, addr_xr.wrapping_add(32), &yr)?" in src + return ok, "spans 63/63/31, u128 overlap guard, yG at +32 in, yR at +32 out" + + +def p_witness_yr_sub_p(s): + """A2e's premise: the honest `y_r_sub_p` is `(2^256 + yR − p) mod 2^256`, filled on BOTH + paths (the shared `compute_witness_inner`).""" + src = _src(s, WITNESS_RS) + ok = "let y_r_sub_p = to_le_32(&((&two_256 + &result.y) - p()));" in src + ok &= "fn compute_witness_inner(" in src + ok &= "pub fn compute_witness_with_y(" in src + # both public entry points funnel into the shared inner fn + ok &= src.count("compute_witness_inner(k_le, k, g)") == 2 + return ok, "y_r_sub_p = (2^256 + yR − p), computed in the shared inner fn used by both paths" + + +def p_carry_offsets(s): + src = _src(s, ECSM_RS) + x2 = re.search(r"CARRY_OFFSET_X2: i64 = (\d+);", src) + yg = re.search(r"CARRY_OFFSET_YG: i64 = (\d+);", src) + ok = (x2 and yg and int(x2.group(1)) == CARRY_OFFSET_X2 + and int(yg.group(1)) == CARRY_OFFSET_YG) + return ok, f"X2 {x2.group(1) if x2 else '?'} / YG {yg.group(1) if yg else '?'}" + + +def p_inv_shift_32(s): + src = _src(s, TEMPLATES_RS) + m = re.search(r"INV_SHIFT_32: u64 = (\d+);", src) + ok = m is not None and int(m.group(1)) == 18446744065119617026 + return ok, f"INV_SHIFT_32 = {m.group(1) if m else '?'} = 2^-32 mod p_g" + + +# ── negative-space premises ──────────────────────────────────────────────── + +def p_no_parity_constraint(s): + """A3's central premise, and pure negative space: NOTHING in the chip constrains `yG`'s + parity. If some constraint did, A3b's forgery would be blocked by it and A3d's + "load-bearing" verdict would be wrong. + + Checked by enumerating every appearance of `cols::YG` and confirming each is one of the + four known, parity-blind uses. A new appearance fails the audit — which is the point: + the premise stops being true silently otherwise.""" + src = _src(s, ECSM_RS) + lines = {i + 1: ln for i, ln in enumerate(src.splitlines()) if "cols::YG" in ln} + allowed = { + "table.set_bytes(row_idx, cols::YG, &w.y_g);": "trace fill", + "dword_bytes(cols::YG, i),": "the affine yG MEMW read (the fix itself)", + "is_byte(cols::YG, 32, &mut out);": "AreBytes range check (parity-blind)", + "cols::YG,": "Ecdas seed/drain bus tuples (parity-blind)", + "s = s + byte(cols::YG, 32, j) * byte(cols::YG, 32, i - j);": + "the Yg relation's yG² term — satisfied by BOTH roots", + } + unknown = {ln: txt.strip() for ln, txt in lines.items() + if txt.strip() not in allowed} + ok = not unknown and len(lines) == 7 + return ok, (f"{len(lines)} uses of cols::YG, all parity-blind " + f"({', '.join(sorted(set(allowed.values())))})" + if ok else f"UNRECOGNISED uses: {unknown}") + + +def p_yr_not_byte_checked(s): + """A2d's premise (contract C4-YR), also negative space: `ecsm.rs` does NOT byte-check + `YR`, so `YrLtP`'s byte hypothesis is inherited through the Ecdas bus rather than emitted + locally. If a future commit adds `is_byte(cols::YR, 32, ...)`, C4-YR stops being a + contract and becomes a local fact — better, but the audit should notice.""" + src = _src(s, ECSM_RS) + checked = set(re.findall(r"is_byte\(cols::(\w+), \d+, &mut out\);", src)) + ok = checked == {"X2", "Q0", "YG", "Q1"} and "YR" not in checked + return ok, (f"ecsm.rs byte-checks {sorted(checked)}; YR (and XR) are NOT among them ⇒ " + "C4-YR is a contract, not a local emission") + + +def p_ts_stride(s): + """A4f's premise: one instruction consumes 4 sub-timestamps, so `ts + 3` is free. + + Read from the CODE, not from ecsm.rs's comment claiming it. The builder assigns + `timestamp = i·4 + 4` per CPU op, which IS the stride; and the ECSM interactions use + exactly offsets {0, +1, +2, +3}, so `ts + 3` is the last slot and nothing spills into the + next instruction. An earlier form of this premise matched the comment text and was + therefore checking documentation rather than behaviour.""" + tb = _src(s, TRACE_BUILDER_RS) + src = _src(s, ECSM_RS) + # PARSE the stride; do not compare the source against a hard-coded 4, or the check is + # blind to a change in the very number it is about (this is what the mutation control + # caught on the first version of this premise). + strides = {int(m) for m in re.findall(r"let timestamp = \(i as u64\) \* (\d+) \+ \d+;", tb)} + offsets = {int(m) for m in re.findall(r"ts_lo_plus\((\d+)\)", src)} + ok = len(strides) == 1 and strides == {INSTRUCTION_TS_STRIDE} + ok &= offsets == {1, 2, 3} # plus the bare `ts_lo()` reads at offset 0 + ok &= bool(strides) and max(offsets) == max(strides) - 1 + return ok, (f"builder stride parsed as {sorted(strides)} (model says " + f"{INSTRUCTION_TS_STRIDE}); ECSM uses ts offsets {{0}} ∪ {sorted(offsets)}, " + f"max {max(offsets)} == stride−1 ⇒ ts+3 is free and nothing spills") + + +def p_all_syscall_numbers(s): + """A1f's premise: the model knows EVERY syscall number the CPU can put on the `Ecall` + bus, not just the ECSM pair. + + A1f's conclusion is about which foreign syscalls the linear syscall word can reach as + `IS_AFFINE` sweeps the field. Add a fifth syscall and the reachable set changes — so the + set has to be read from the source, not remembered. Parsed as `u64::MAX - k` declarations, + and the parsed set must equal the model's exactly (both directions: a new syscall fails + this, and so does a stale entry).""" + src = _src(s, EXEC_RS) + found = {name: 2**64 - 1 - int(k) for name, k in re.findall( + r"pub const (\w+)_SYSCALL_NUMBER: u64 = u64::MAX - (\d+);", src)} + ok = found == SYSCALL_NUMBERS + return ok, (f"{len(found)} syscalls parsed: " + + ", ".join(f"{n}=MAX-{2**64 - 1 - v}" for n, v in sorted(found.items())) + + ("" if ok else f" MISMATCH vs model {sorted(SYSCALL_NUMBERS)}")) + + +PREMISES = [ + Premise("P1 column layout", "A1/A2", "IS_AFFINE=667, YR_SUB_P=668..684, NUM_COLUMNS=684", + p_columns, + mutations=[(ECSM_RS, r"pub const NUM_COLUMNS: usize = 684;", + "pub const NUM_COLUMNS: usize = 683;", "off-by-one column count")]), + Premise("P2 constraint count + index map", "A1", "idx closes at 423; 413..422 documented", + p_constraint_count, + mutations=[(ECSM_RS, r"debug_assert_eq!\(idx, 423\);", + "debug_assert_eq!(idx, 421);", "wrong constraint total")]), + Premise("P3 address-limb bounds", "A4", "2^32−31 and 2^32−63", p_addr_bounds, + mutations=[(ECSM_RS, r"ADDR_LIMB_BOUND_64B: u64 = \(1 << 32\) - 63;", + "ADDR_LIMB_BOUND_64B: u64 = (1 << 32) - 64;", "off-by-one bound")]), + Premise("P4 syscall numbers", "A1c", "u64::MAX−10 and u64::MAX−11", p_syscall_numbers, + mutations=[(EXEC_RS, r"ECSM_AFFINE_SYSCALL_NUMBER: u64 = u64::MAX - 11;", + "ECSM_AFFINE_SYSCALL_NUMBER: u64 = u64::MAX - 12;", + "different affine number")]), + Premise("P5 low-word compile-time assert", "A1c", + "the pinning's only separating word is guarded at compile time", p_lowword_assert, + mutations=[(EXEC_RS, r"const _: \(\) = assert!\(", + "const _UNUSED: () = ((), assert!(", "assert removed/renamed")]), + Premise("P6 syscall word is linear in IS_AFFINE", "A1c", + "both received words interpolate the two numbers", p_syscall_word_linear, + mutations=[(ECSM_RS, r"coefficient: affine - xonly,", + "coefficient: 0,", "coefficient zeroed ⇒ selector unpinned")]), + Premise("P7 affine-gated bus layout", "A1/A3", + "4+4 IS_AFFINE-gated dwords at +32+8i, yR at ts+3", p_affine_gated_buses, + mutations=[(ECSM_RS, r"LinearTerm::Constant\(\(32 \+ 8 \* i\) as i64\)", + "LinearTerm::Constant((8 * i) as i64)", "offset +32 dropped")]), + Premise("P8 YrLtP wiring", "A2", "YrLtP → (P_BYTES, YR_SUB_P, YR), byte-stored", + p_yrltp_wiring, + mutations=[(ECSM_RS, r"OverflowKind::YrLtP => cols::YR,", + "OverflowKind::YrLtP => cols::XR,", "sum column swapped to XR")]), + Premise("P9 YrLtP is µ-gated, not IS_AFFINE-gated", "A2d", + "the four chains share one µ-gated loop", p_yrltp_mu_gated, + mutations=[(ECSM_RS, r"let mu = b\.main\(0, cols::MU\);\n let one = b\.one\(\);\n b\.emit_base\(idx, mu \* ci\.clone\(\)", + "let mu = b.main(0, cols::IS_AFFINE);\n let one = b.one();\n b.emit_base(idx, mu * ci.clone()", + "carry bits re-gated on IS_AFFINE")]), + Premise("P10 YR_SUB_P halfword checks", "A2", "16 µ-gated IsHalfword sends", + p_yr_sub_p_halfword_checks, + mutations=[(ECSM_RS, r"vec!\[packed\(cols::yr_sub_p\(i\)\)\],", + "vec![packed(cols::xr_sub_p(i))],", "halfword checks aimed at XR")]), + Premise("P11 Alu LT senders", "A4", "3 senders with the right bounds and LT/1", + p_alu_lt_senders, + mutations=[(ECSM_RS, r"out\.push\(alu_lt\(packed\(cols::ADDR_XR_0\), addr_bound_by_mode\(\)\)\);", + "", "xR's address bound removed")]), + Premise("P12 executor ABI arm", "A4", "spans 63/63/31 and the u128 overlap guard", + p_executor_abi, + mutations=[(EXEC_RS, r"if \(addr_k as u128\) < addr_xg as u128 \+ 64", + "if (addr_k as u64) < addr_xg as u64 + 64", + "u128 widening reverted to the wrapping form")]), + Premise("P13 honest y_r_sub_p", "A2e", "(2^256 + yR − p), shared by both paths", + p_witness_yr_sub_p, + mutations=[(WITNESS_RS, r"let y_r_sub_p = to_le_32\(&\(\(&two_256 \+ &result\.y\) - p\(\)\)\);", + "let y_r_sub_p = to_le_32(&((&two_256 + &result.x) - p()));", + "addend built from x instead of y")]), + Premise("P14 carry offsets", "A3", "8160 / 16319", p_carry_offsets, + mutations=[(ECSM_RS, r"CARRY_OFFSET_YG: i64 = 16319;", + "CARRY_OFFSET_YG: i64 = 16320;", "offset perturbed")]), + Premise("P15 INV_SHIFT_32", "A2a", "2^-32 mod p_g", p_inv_shift_32, + mutations=[(TEMPLATES_RS, r"INV_SHIFT_32: u64 = 18446744065119617026;", + "INV_SHIFT_32: u64 = 18446744065119617025;", "inverse perturbed")]), + Premise("P16 nothing constrains yG's parity", "A3", "every cols::YG use is parity-blind", + p_no_parity_constraint, kind="negative-space", + mutations=[(ECSM_RS, r"is_byte\(cols::YG, 32, &mut out\);", + "is_byte(cols::YG, 32, &mut out);\n let _parity = cols::YG;", + "an unrecognised cols::YG use appears")]), + Premise("P17 YR is not byte-checked in ecsm.rs", "A2d", + "C4-YR is inherited, not emitted", p_yr_not_byte_checked, kind="negative-space", + mutations=[(ECSM_RS, r"is_byte\(cols::Q1, 33, &mut out\);", + "is_byte(cols::Q1, 33, &mut out);\n is_byte(cols::YR, 32, &mut out);", + "YR gains a local byte check")]), + Premise("P19 the complete syscall set", "A1f", + "every u64::MAX-k syscall the Ecall bus can carry", p_all_syscall_numbers, + mutations=[(EXEC_RS, r"pub const HINT_SYSCALL_NUMBER: u64 = u64::MAX - 30;", + "pub const HINT_SYSCALL_NUMBER: u64 = u64::MAX - 40;", + "a syscall number changes ⇒ A1f's reachable set is stale")]), + Premise("P18 instruction timestamp stride", "A4f", "4 sub-timestamps per instruction", + p_ts_stride, + mutations=[(TRACE_BUILDER_RS, r"let timestamp = \(i as u64\) \* 4 \+ 4;", + "let timestamp = (i as u64) * 3 + 3;", + "stride reduced to 3 ⇒ ts+3 collides with the next instruction")]), +] + + +# ── the audit ────────────────────────────────────────────────────────────── + +def load_sources(): + paths = (ECSM_RS, EXEC_RS, WITNESS_RS, TEMPLATES_RS, TRACE_BUILDER_RS) + missing = [p for p in paths if not p.exists()] + if missing: + return None, missing + return {p: p.read_text() for p in paths}, [] + + +def main(): + sources, missing = load_sources() + if sources is None: + report("audit", "FAIL", f"missing sources: {missing}") + return 1 + + n_ok = 0 + for pr in PREMISES: + ok, detail = pr.check(sources) + n_ok += ok + tag = "READ" if pr.kind == "assumed" else "READ(neg)" + report(f"{pr.key} [{pr.lemma}]", tag if ok else "FAIL", detail) + + print() + # Mutation testing: each premise must FAIL on perturbed source, or it checks nothing. + blind = [] + n_mut = 0 + for pr in PREMISES: + for path, pattern, repl, why in pr.mutations: + mutated = dict(sources) + new, count = re.subn(pattern, repl, mutated[path], count=1) + if count == 0: + blind.append(f"{pr.key}: mutation pattern did not apply ({why})") + continue + mutated[path] = new + ok, _ = pr.check(mutated) + n_mut += 1 + if ok: + blind.append(f"{pr.key}: survives mutation '{why}' ⇒ the check is BLIND") + report("mutation testing", "PROVED" if not blind else "FAIL", + f"{n_mut} mutations applied; every premise's check fails on its mutant" + if not blind else "; ".join(blind)) + + print() + failed = [n for n, v, _ in results if v == "FAIL"] + print(f"TRANSCRIPTION AUDIT: {n_ok}/{len(PREMISES)} premises read from source, " + f"{n_mut} mutation controls, {len(failed)} failures") + if failed: + print(" FAILURES: " + ", ".join(failed)) + return 1 if failed else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/gate/logs/a1_selector.log b/docs/verification/ecsm-affine/gate/logs/a1_selector.log new file mode 100644 index 000000000..3e62a2f8a --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/a1_selector.log @@ -0,0 +1,24 @@ +[CERTIFIED] A1-PRIME p_g = 2^64 − 2^32 + 1 is prime sympy.isprime; the field property every root argument below rests on +[PROVED ] A1a IS_BIT(IS_AFFINE) ⇒ a ∈ {0,1} idx 421; roots over GF(p_g) = [0, 1], split complete: True +[PROVED ] A1b AffineZeroOnPadding ⇒ µ=0 forces IS_AFFINE=0 idx 422 at µ=0; IS_BIT(MU) roots [0, 1]; 0.01s +[PROVED ] A1c Ecall tuple injective in IS_AFFINE [repo numbers] [repo numbers] lo: 4294967285 vs 4294967284; hi: 4294967295 vs 4294967295 +[PROVED ] A1c Ecall tuple injective in IS_AFFINE [equal lo, differing hi (assert fires; still injective)] [equal lo, differing hi (assert fires; still injective)] lo: 4294967285 vs 4294967285; hi: 1 vs 2 +[SAT — FORGES] A1c Ecall tuple injective in IS_AFFINE [identical numbers (degenerate)] [identical numbers (degenerate)] lo: 4294967285 vs 4294967285; hi: 4294967295 vs 4294967295 ⇒ IS_AFFINE UNCONSTRAINED +[PROVED ] A1c controls the degenerate choice un-pins the selector; the repo pair does not +[PROVED ] A1c assert load-bearing low word separates modes: True; high word separates modes: False ⇒ execution.rs's low-word assert carries the entire pinning +[PROVED ] A1d degree bound max over new constraints = 3 == declared max_degree 3 +[SAT — FORGES] A1e control [drop idx 422] padding row with IS_AFFINE=1 all 423 constraints walked: idx 422 is the ONLY one violated when kept, and all 422 remaining are satisfied when dropped; honest padding (IS_AFFINE=0) satisfies all 423. The dropped row then fires 8 IS_AFFINE-gated MEMW interactions. idx 422 is LOAD-BEARING. +[SAT — FORGES] A1f control [drop idx 421] cross-syscall impersonation high-word coefficient is 0 (blind), low-word is -1, so the received tuple sweeps the whole field. Reachable syscalls: ECSM@IS_AFFINE=0, ECSM_AFFINE@IS_AFFINE=1, HINT@IS_AFFINE=20, KECCAK@IS_AFFINE=18446744069414584312. With idx 421 kept only ['ECSM', 'ECSM_AFFINE'] are admissible; dropped, ['HINT', 'KECCAK'] become reachable ⇒ idx 421 is LOAD-BEARING, and NOT for the reason its comment gives. + +Summary: + CERTIFIED A1-PRIME p_g = 2^64 − 2^32 + 1 is prime + PROVED A1a IS_BIT(IS_AFFINE) ⇒ a ∈ {0,1} + PROVED A1b AffineZeroOnPadding ⇒ µ=0 forces IS_AFFINE=0 + PROVED A1c Ecall tuple injective in IS_AFFINE [repo numbers] + PROVED A1c Ecall tuple injective in IS_AFFINE [equal lo, differing hi (assert fires; still injective)] + SAT — FORGES A1c Ecall tuple injective in IS_AFFINE [identical numbers (degenerate)] + PROVED A1c controls + PROVED A1c assert load-bearing + PROVED A1d degree bound + SAT — FORGES A1e control [drop idx 422] padding row with IS_AFFINE=1 + SAT — FORGES A1f control [drop idx 421] cross-syscall impersonation diff --git a/docs/verification/ecsm-affine/gate/logs/a2_yr_lt_p.log b/docs/verification/ecsm-affine/gate/logs/a2_yr_lt_p.log new file mode 100644 index 000000000..4bf21be16 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/a2_yr_lt_p.log @@ -0,0 +1,26 @@ +[PROVED ] A2a YrLtP word-carry lift |A| < 2^33 ⇒ no p_g wrap; 0.01s +[PROVED ] A2b OverflowRequired(YrLtP) ⇒ yR < p p pinned as a numeral (not a free constant); 0.01s +[SAT (expected)] A2b non-vacuity yR = p−1 is satisfiable ⇒ the constraint set is not empty; 0.01s +[PROVED ] A2c width [YrLtP pre-lift word] max|A_i| = 8589934591 = 2^32.. < 2^33 ≪ p_g (4.66e-10·p_g) +[PROVED ] A2c width [emitted YrLtP constraints] µ·c·(1−c) ∈ {0} and µ·(1−c_7) ∈ {0,±1} once c ∈ {0,1}: single-digit ≪ p_g +[SAT — CATCHES] A2c control [wrong constant p→p+2 / p→N] honest witness (addend fixed at (2^256+yR−p) mod 2^256) valid under p (True), rejected under p+2 (True) and under N (True) ⇒ the chain binds `p` itself, not just its shape +[CONTRACT ] A2d contract C4-YR [YR byte authority] YR is NOT in ecsm.rs's is_byte list ['Q0', 'Q1', 'X2', 'YG']; bound inherited via 2 exhaustive cases on len_k (bus-level, so outside this gate: C5 + imported L6) +[NOTED ] A2d observation [µ-gated, not IS_AFFINE-gated] YrLtP binds on x-only rows too: strictly stronger (sound), and honest witnesses satisfy it because witness.rs fills y_r_sub_p on both paths +[PROVED ] A2e honest-witness anchor 14 witnesses (4 x-only, 10 affine): every c_i ∈ {0,1}, c_7 = 1, YR_SUB_P halfwords in [0,2^16) +[SAT — FORGES] A2f forgery instantiated (y = 1 point) yR = 1, yR+p = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc30; all 12 checks hold: the forged witness satisfies the ECDAS Yr relation exactly, its carries fit the window, and every byte check passes — YrLtP is the only thing that rejects it +[SAT — FORGES] A2g control [drop YrLtP] the A2f witness is accepted and the guest is handed a non-canonical yR ⇒ YrLtP is LOAD-BEARING (the yR-side analogue of the earlier board's N6/XR_SUB_P) +[PROVED ] A2h attack band populated 2^256 − p = 4294968273 = 2^32 + 977; a real secp256k1 point has y = 1 (the smallest possible), so y + p is 32-byte representable ⇒ the PR's constructibility claim holds, at the very bottom of the band + +Summary: + PROVED A2a YrLtP word-carry lift + PROVED A2b OverflowRequired(YrLtP) ⇒ yR < p + SAT (expected) A2b non-vacuity + PROVED A2c width [YrLtP pre-lift word] + PROVED A2c width [emitted YrLtP constraints] + SAT — CATCHES A2c control [wrong constant p→p+2 / p→N] + CONTRACT A2d contract C4-YR [YR byte authority] + NOTED A2d observation [µ-gated, not IS_AFFINE-gated] + PROVED A2e honest-witness anchor + SAT — FORGES A2f forgery instantiated (y = 1 point) + SAT — FORGES A2g control [drop YrLtP] + PROVED A2h attack band populated diff --git a/docs/verification/ecsm-affine/gate/logs/a3_parity_binding.log b/docs/verification/ecsm-affine/gate/logs/a3_parity_binding.log new file mode 100644 index 000000000..cdb427253 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/a3_parity_binding.log @@ -0,0 +1,18 @@ +[PROVED ] A3a yG parity arithmetically free Y² − (x³+b) splits into (Y−y)(Y+y) over GF(p) at 6 real x-coordinates; both roots distinct in all 6 (no y=0 point ⇒ never a forced parity) +[SAT — FORGES] A3b parity forgery instantiated k = 0x9e3779b97f4a7c15: two full witnesses, all 11 facts hold. Same (xG, k, xR), yR differs: 0x2b8adf37e2371e4d56d0e217e1bb0a05239b3097fb93021a3c1d5d2a2d8f7743 vs 0xd47520c81dc8e1b2a92f1de81e44f5fadc64cf68046cfde5c3e2a2d4d27084ec. Violations — honest: none, forged: none +[SAT — FORGES] A3b forgery sweep 12 random (base point, k) pairs: both roots always yield a fully valid witness with the same xR and a different yR +[PROVED ] A3c yG read covers YG bit-for-bit 4 dwords × 8 bytes: YG[0..32] ↔ addr_xG+[32..64), order-preserving, all 5 facts hold +[PROVED ] A3c read closes the forgery the ±yG witnesses differ in 32 of the 32 read bytes ⇒ distinct MEMW tuples ⇒ at most one matches the caller's buffer (reduction to C4/C5) +[SAT — FORGES] A3d control [drop the yG read] both witnesses verify and are indistinguishable without the read ⇒ the IS_AFFINE-gated yG MEMW read is LOAD-BEARING; it is the ONLY thing pinning the input parity, and the affine ABI is what made the parity observable +[PROVED ] A3e imported L7 survives 20 instances: x(k·P) = x(k·(−P)) ⇒ the x-only path's conclusion is unaffected by the affine variant, and x-only rows may still leave parity free +[PROVED ] A3f YrLtP accepts both parities both ±yR are canonical ⇒ YrLtP admits either ⇒ it addresses output REPRESENTATION (A2), never input parity. Two orthogonal gaps, two fixes. + +Summary: + PROVED A3a yG parity arithmetically free + SAT — FORGES A3b parity forgery instantiated + SAT — FORGES A3b forgery sweep + PROVED A3c yG read covers YG bit-for-bit + PROVED A3c read closes the forgery + SAT — FORGES A3d control [drop the yG read] + PROVED A3e imported L7 survives + PROVED A3f YrLtP accepts both parities diff --git a/docs/verification/ecsm-affine/gate/logs/a4_addressing.log b/docs/verification/ecsm-affine/gate/logs/a4_addressing.log new file mode 100644 index 000000000..801b62754 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/a4_addressing.log @@ -0,0 +1,24 @@ +[PROVED ] A4a LT bound == addr_limb_ok [IS_AFFINE=0, span=31] bound = 4294967265 = 2^32 − 31; 0.00s +[PROVED ] A4a LT bound == addr_limb_ok [IS_AFFINE=1, span=63] bound = 4294967233 = 2^32 − 63; 0.00s +[PROVED ] A4a linear bound interpolates the two constants BOUND_32B + a·(BOUND_64B − BOUND_32B) = 4294967265 at a=0, 4294967233 at a=1 +[PROVED ] A4b affine span stays inside the limb 128 touched byte offsets (max +63) all < 2^32 for every accepted addr_lo; 0.01s +[PROVED ] A4c seven-value band, both modes 32-byte (x-only xG/xR, k): max dword base +24, band size 7 ([2^32−31, 2^32−24]); 64-byte (affine xG‖yG, xR‖yR): max dword base +56, band size 7 ([2^32−63, 2^32−56]) +[PROVED ] A4c band closed by the LT senders every band address fails `addr_lo < bound` ⇒ the bus now rejects exactly what the executor rejects (the gap `hint.rs` closes for the Hint ecall) +[PROVED ] A4d k bound flat in both modes ADDR_K_0 < 4294967265 == addr_limb_ok(addr_k, 31); 0.00s +[PROVED ] A4e overlap guard == interval disjointness the u128 clause `k < xg+64 ∧ xg < k+32` is exactly `[xg,xg+64) ∩ [k,k+32) ≠ ∅`; 0.01s +[SAT — FORGES] A4e control [u64 wrap in the overlap guard] 1 reachable addresses in [2^64−64, 2^64) pass addr_limb_ok, wrap the pre-fix `+64`, and slip a TOTAL operand overlap past the guard ⇒ the u128 widening is LOAD-BEARING +[PROVED ] A4f timestamp layout slots {'xG read': 0, 'yG read': 0, 'k read': 1, 'xR write': 2, 'yR write': 3} within stride 4; xG@ts and yG@ts are address-disjoint so the same-timestamp reads are legal +[PROVED ] A4g mode-dependent bound is necessary a flat 64-byte bound would reject 32 legal x-only addresses (completeness); a flat 32-byte bound would admit 32 illegal affine ones (soundness) ⇒ the IS_AFFINE interpolation is load-bearing in BOTH directions + +Summary: + PROVED A4a LT bound == addr_limb_ok [IS_AFFINE=0, span=31] + PROVED A4a LT bound == addr_limb_ok [IS_AFFINE=1, span=63] + PROVED A4a linear bound interpolates the two constants + PROVED A4b affine span stays inside the limb + PROVED A4c seven-value band, both modes + PROVED A4c band closed by the LT senders + PROVED A4d k bound flat in both modes + PROVED A4e overlap guard == interval disjointness + SAT — FORGES A4e control [u64 wrap in the overlap guard] + PROVED A4f timestamp layout + PROVED A4g mode-dependent bound is necessary diff --git a/docs/verification/ecsm-affine/gate/logs/a6_real_witness.log b/docs/verification/ecsm-affine/gate/logs/a6_real_witness.log new file mode 100644 index 000000000..875f854a4 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/a6_real_witness.log @@ -0,0 +1,12 @@ +[PROVED ] A6a real-witness evaluation 28 witnesses from ecsm::compute_witness{,_with_y}: oracle agreement, all four overflow chains, both convolution relations, carry windows, len_k and the ECDAS step count all re-derived +[PROVED ] A6b rejections match the oracle 4 rejected by crypto/ecsm: {'k=0': 'ECSM scalar k must be non-zero', 'k=N': 'ECSM scalar k must be < N', 'off-curve yG': 'ECSM input point is not on the curve', 'yG=p': 'ECSM coordinates must be < p'} +[SAT — FORGES] A6c parity forgery from the repo's generator 9 ±yG witness pairs out of crypto/ecsm itself: every one is valid, agrees on x_r, and publishes a different y_r ⇒ the gap A3 proves is not a modelling artefact +[PROVED ] A6d x-only == affine with the even lift 9 labels over G (whose y is even): all 13 witness fields identical ⇒ the affine variant is the same chip, not a parallel one +[PROVED ] A6e small-y instance crypto/ecsm returns y_r = 1 for the constructed point; y_r_sub_p = 0x1000003d2 = 2^256 + 1 − p, and y_r + p < 2^256 ⇒ the A2 forgery's premise holds against the real generator + +Summary: + PROVED A6a real-witness evaluation + PROVED A6b rejections match the oracle + SAT — FORGES A6c parity forgery from the repo's generator + PROVED A6d x-only == affine with the even lift + PROVED A6e small-y instance diff --git a/docs/verification/ecsm-affine/gate/logs/audit_transcription.log b/docs/verification/ecsm-affine/gate/logs/audit_transcription.log new file mode 100644 index 000000000..670a0ed13 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/audit_transcription.log @@ -0,0 +1,23 @@ +[READ ] P1 column layout [A1/A2] {'MU': 666, 'IS_AFFINE': 667, 'YR_SUB_P': 668, 'NUM_COLUMNS': 684}; YR_SUB_P + 16 halfwords = 684 == NUM_COLUMNS 684 +[READ ] P2 constraint count + index map [A1] idx closes at 423 == 423; header map lists 413..422 +[READ ] P3 address-limb bounds [A4] 2^32−31 / 2^32−63 match the model's constants +[READ ] P4 syscall numbers [A1c] u64::MAX−10 / u64::MAX−11 +[READ ] P5 low-word compile-time assert [A1c] the low-32-bit-word inequality is a compile-time assert +[READ ] P6 syscall word is linear in IS_AFFINE [A1c] both received words are the IS_AFFINE interpolation of the two numbers +[READ ] P7 affine-gated bus layout [A1/A3] 2 affine-gated bus blocks (4 dwords each), offsets +32+8i, yG via memw_read at ts and yR via memw_write at ts+3 +[READ ] P8 YrLtP wiring [A2] YrLtP → (P_BYTES, YR_SUB_P, YR), byte-stored sum (not bits) +[READ ] P9 YrLtP is µ-gated, not IS_AFFINE-gated [A2d] all four chains share one µ-gated loop; IS_AFFINE does not appear in it ⇒ YrLtP binds x-only rows too (strictly stronger; A2d) +[READ ] P10 YR_SUB_P halfword checks [A2] 16 µ-gated IsHalfword sends on yr_sub_p(i) +[READ ] P11 Alu LT senders [A4] 3 senders: xG/xR vs addr_bound_by_mode(), k vs the flat 32-byte bound, LT/1 +[READ ] P12 executor ABI arm [A4] spans 63/63/31, u128 overlap guard, yG at +32 in, yR at +32 out +[READ ] P13 honest y_r_sub_p [A2e] y_r_sub_p = (2^256 + yR − p), computed in the shared inner fn used by both paths +[READ ] P14 carry offsets [A3] X2 8160 / YG 16319 +[READ ] P15 INV_SHIFT_32 [A2a] INV_SHIFT_32 = 18446744065119617026 = 2^-32 mod p_g +[READ(neg) ] P16 nothing constrains yG's parity [A3] 7 uses of cols::YG, all parity-blind (AreBytes range check (parity-blind), Ecdas seed/drain bus tuples (parity-blind), the Yg relation's yG² term — satisfied by BOTH roots, the affine yG MEMW read (the fix itself), trace fill) +[READ(neg) ] P17 YR is not byte-checked in ecsm.rs [A2d] ecsm.rs byte-checks ['Q0', 'Q1', 'X2', 'YG']; YR (and XR) are NOT among them ⇒ C4-YR is a contract, not a local emission +[READ ] P19 the complete syscall set [A1f] 4 syscalls parsed: ECSM=MAX-10, ECSM_AFFINE=MAX-11, HINT=MAX-30, KECCAK=MAX-1 +[READ ] P18 instruction timestamp stride [A4f] builder stride parsed as [4] (model says 4); ECSM uses ts offsets {0} ∪ [1, 2, 3], max 3 == stride−1 ⇒ ts+3 is free and nothing spills + +[PROVED ] mutation testing 19 mutations applied; every premise's check fails on its mutant + +TRANSCRIPTION AUDIT: 19/19 premises read from source, 19 mutation controls, 0 failures diff --git a/docs/verification/ecsm-affine/gate/logs/harness_build.log b/docs/verification/ecsm-affine/gate/logs/harness_build.log new file mode 100644 index 000000000..35912b25c --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/harness_build.log @@ -0,0 +1 @@ + Finished `release` profile [optimized] target(s) in 0.07s diff --git a/docs/verification/ecsm-affine/gate/logs/oracle_anchors.log b/docs/verification/ecsm-affine/gate/logs/oracle_anchors.log new file mode 100644 index 000000000..7dda039fb --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/oracle_anchors.log @@ -0,0 +1,11 @@ +[PASS ] A0 repo constants 4 constants parsed from crypto/ecsm/src/lib.rs match +[PASS ] A1 curve/group G on curve, N·G = O, 5 published multiples, 40 negation + 20 additivity checks +[PASS ] A2 x-only agreement 216 (k, xG) pairs: affine_mul(...).x == x_only_mul(...), incl. k = 1, 2, N−1, N−2, 2^255 +[PASS ] A3 root dependence 200 instances: x invariant under yG → p−yG, y negated in ALL 200 of them ⇒ publishing yR makes the input parity observable +[PASS ] A4 validation set 8 rejections match the executor's error kinds; k ∈ {1, 2, N−2, N−1} all accepted and ordinary +[PASS ] A5 ABI predicates limb bound exact at both spans (31/63), overlap guard == interval disjointness over 193 offsets; u64-wrap control: addr 2^64−64 passes addr_limb_ok (=True) yet the pre-fix guard misses a total overlap +[PASS ] A6 ecrecover equivalence 60 instances: y recovered from x(k·P) + x((k+1)·P) + the chord law equals the y the affine ecall returns ⇒ dropping `solve_y` is semantics-preserving +[PASS ] A7 third-party cross-check 25 random k·P against the `ecdsa` package +[PASS ] A8 LE32 codec round-trip + endianness + +ORACLE STATUS: VALIDATED (9 pass, 0 skip, 0 fail) diff --git a/docs/verification/ecsm-affine/gate/logs/real_witnesses.jsonl b/docs/verification/ecsm-affine/gate/logs/real_witnesses.jsonl new file mode 100644 index 000000000..7022541ac --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/real_witnesses.jsonl @@ -0,0 +1,32 @@ +{"label":"k=1","mode":"x-only","k":"0100000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c0bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r_sub_p":"89d810fb90d0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":0,"steps":0} +{"label":"k=1","mode":"affine/+y","k":"0100000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c0bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r_sub_p":"89d810fb90d0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":0,"steps":0} +{"label":"k=1","mode":"affine/-y","k":"0100000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c0bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r_sub_p":"482bef04702fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":0,"steps":0} +{"label":"k=2","mode":"x-only","k":"0200000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"e59e705cb909acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r":"2ae5cf50a9316423e1d066326532f6f7eeea6c461984c5a339c33da6fe68e11a","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c1bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"b6a2705cba09acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r_sub_p":"fbe8cf50aa316423e1d066326532f6f7eeea6c461984c5a339c33da6fe68e11a","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":1,"steps":1} +{"label":"k=2","mode":"affine/+y","k":"0200000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"e59e705cb909acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r":"2ae5cf50a9316423e1d066326532f6f7eeea6c461984c5a339c33da6fe68e11a","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c1bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"b6a2705cba09acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r_sub_p":"fbe8cf50aa316423e1d066326532f6f7eeea6c461984c5a339c33da6fe68e11a","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":1,"steps":1} +{"label":"k=2","mode":"affine/-y","k":"0200000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"e59e705cb909acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r":"051730af55ce9bdc1e2f99cd9acd0908111593b9e67b3a5cc63cc25901971ee5","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c1bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"b6a2705cba09acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r_sub_p":"d61a30af56ce9bdc1e2f99cd9acd0908111593b9e67b3a5cc63cc25901971ee5","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":1,"steps":1} +{"label":"k=3","mode":"x-only","k":"0300000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"f936e0bc13f10186b0996f8345c831b529529df8854f344910c35892018a30f9","y_r":"72e6b88475fdb96c1b23c23499a9006556f3372ae637e30f14e82d630f7b8f38","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c2bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"ca3ae0bc14f10186b0996f8345c831b529529df8854f344910c35892018a30f9","y_r_sub_p":"43eab88476fdb96c1b23c23499a9006556f3372ae637e30f14e82d630f7b8f38","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":1,"steps":2} +{"label":"k=3","mode":"affine/+y","k":"0300000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"f936e0bc13f10186b0996f8345c831b529529df8854f344910c35892018a30f9","y_r":"72e6b88475fdb96c1b23c23499a9006556f3372ae637e30f14e82d630f7b8f38","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c2bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"ca3ae0bc14f10186b0996f8345c831b529529df8854f344910c35892018a30f9","y_r_sub_p":"43eab88476fdb96c1b23c23499a9006556f3372ae637e30f14e82d630f7b8f38","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":1,"steps":2} +{"label":"k=3","mode":"affine/-y","k":"0300000000000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"f936e0bc13f10186b0996f8345c831b529529df8854f344910c35892018a30f9","y_r":"bd15477b89024693e4dc3dcb6656ff9aa90cc8d519c81cf0eb17d29cf08470c7","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"c2bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"ca3ae0bc14f10186b0996f8345c831b529529df8854f344910c35892018a30f9","y_r_sub_p":"8e19477b8a024693e4dc3dcb6656ff9aa90cc8d519c81cf0eb17d29cf08470c7","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":1,"steps":2} +{"label":"k=N-1","mode":"x-only","k":"404136d08c5ed2bf3ba048afe6dcaebafeffffffffffffffffffffffffffffff","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff","x_r_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r_sub_p":"482bef04702fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":255,"steps":445} +{"label":"k=N-1","mode":"affine/+y","k":"404136d08c5ed2bf3ba048afe6dcaebafeffffffffffffffffffffffffffffff","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff","x_r_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r_sub_p":"482bef04702fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":255,"steps":445} +{"label":"k=N-1","mode":"affine/-y","k":"404136d08c5ed2bf3ba048afe6dcaebafeffffffffffffffffffffffffffffff","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff","x_r_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_r_sub_p":"89d810fb90d0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":255,"steps":445} +{"label":"k=N-2","mode":"x-only","k":"3f4136d08c5ed2bf3ba048afe6dcaebafeffffffffffffffffffffffffffffff","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"e59e705cb909acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r":"051730af55ce9bdc1e2f99cd9acd0908111593b9e67b3a5cc63cc25901971ee5","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"feffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff","x_r_sub_p":"b6a2705cba09acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r_sub_p":"d61a30af56ce9bdc1e2f99cd9acd0908111593b9e67b3a5cc63cc25901971ee5","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":255,"steps":450} +{"label":"k=N-2","mode":"affine/+y","k":"3f4136d08c5ed2bf3ba048afe6dcaebafeffffffffffffffffffffffffffffff","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"e59e705cb909acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r":"051730af55ce9bdc1e2f99cd9acd0908111593b9e67b3a5cc63cc25901971ee5","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"feffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff","x_r_sub_p":"b6a2705cba09acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r_sub_p":"d61a30af56ce9bdc1e2f99cd9acd0908111593b9e67b3a5cc63cc25901971ee5","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":255,"steps":450} +{"label":"k=N-2","mode":"affine/-y","k":"3f4136d08c5ed2bf3ba048afe6dcaebafeffffffffffffffffffffffffffffff","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"e59e705cb909acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r":"2ae5cf50a9316423e1d066326532f6f7eeea6c461984c5a339c33da6fe68e11a","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"feffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff","x_r_sub_p":"b6a2705cba09acaba73cef8c4b8e775cd87cc0956e4045306d7ded41947f04c6","y_r_sub_p":"fbe8cf50aa316423e1d066326532f6f7eeea6c461984c5a339c33da6fe68e11a","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":255,"steps":450} +{"label":"k=2^255","mode":"x-only","k":"0000000000000000000000000000000000000000000000000000000000000080","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"84e38b3f0432bde8c3b61da3ad0aec7172f0de4fc9d61a251b3ee62ba49037b2","y_r":"0e8819eb3d470ad158cb9e14f404f01745f981aa880fd5e8db5ed51949696bfc","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"bfbec92f73a12d40c45fb7501923514501000000000000000000000000000080","x_r_sub_p":"55e78b3f0532bde8c3b61da3ad0aec7172f0de4fc9d61a251b3ee62ba49037b2","y_r_sub_p":"df8b19eb3e470ad158cb9e14f404f01745f981aa880fd5e8db5ed51949696bfc","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":255,"steps":255} +{"label":"k=2^255","mode":"affine/+y","k":"0000000000000000000000000000000000000000000000000000000000000080","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"84e38b3f0432bde8c3b61da3ad0aec7172f0de4fc9d61a251b3ee62ba49037b2","y_r":"0e8819eb3d470ad158cb9e14f404f01745f981aa880fd5e8db5ed51949696bfc","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"bfbec92f73a12d40c45fb7501923514501000000000000000000000000000080","x_r_sub_p":"55e78b3f0532bde8c3b61da3ad0aec7172f0de4fc9d61a251b3ee62ba49037b2","y_r_sub_p":"df8b19eb3e470ad158cb9e14f404f01745f981aa880fd5e8db5ed51949696bfc","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":255,"steps":255} +{"label":"k=2^255","mode":"affine/-y","k":"0000000000000000000000000000000000000000000000000000000000000080","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"84e38b3f0432bde8c3b61da3ad0aec7172f0de4fc9d61a251b3ee62ba49037b2","y_r":"2174e614c1b8f52ea73461eb0bfb0fe8ba067e5577f02a1724a12ae6b6969403","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"bfbec92f73a12d40c45fb7501923514501000000000000000000000000000080","x_r_sub_p":"55e78b3f0532bde8c3b61da3ad0aec7172f0de4fc9d61a251b3ee62ba49037b2","y_r_sub_p":"f277e614c2b8f52ea73461eb0bfb0fe8ba067e5577f02a1724a12ae6b6969403","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":255,"steps":255} +{"label":"k=2^255-1","mode":"x-only","k":"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7f","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"1d656c66fc8e29804a5551d2fb921730127ec07b3f8cd09f15783147edbf0e37","y_r":"a2a4de6509c0c32b587dba56574585efb996c22576773b50e542c56151b708ad","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"bebec92f73a12d40c45fb7501923514501000000000000000000000000000080","x_r_sub_p":"ee686c66fd8e29804a5551d2fb921730127ec07b3f8cd09f15783147edbf0e37","y_r_sub_p":"73a8de650ac0c32b587dba56574585efb996c22576773b50e542c56151b708ad","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":254,"steps":508} +{"label":"k=2^255-1","mode":"affine/+y","k":"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7f","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"1d656c66fc8e29804a5551d2fb921730127ec07b3f8cd09f15783147edbf0e37","y_r":"a2a4de6509c0c32b587dba56574585efb996c22576773b50e542c56151b708ad","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"bebec92f73a12d40c45fb7501923514501000000000000000000000000000080","x_r_sub_p":"ee686c66fd8e29804a5551d2fb921730127ec07b3f8cd09f15783147edbf0e37","y_r_sub_p":"73a8de650ac0c32b587dba56574585efb996c22576773b50e542c56151b708ad","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":254,"steps":508} +{"label":"k=2^255-1","mode":"affine/-y","k":"ffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff7f","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"1d656c66fc8e29804a5551d2fb921730127ec07b3f8cd09f15783147edbf0e37","y_r":"8d57219af53f3cd4a78245a9a8ba7a1046693dda8988c4af1abd3a9eae48f752","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"bebec92f73a12d40c45fb7501923514501000000000000000000000000000080","x_r_sub_p":"ee686c66fd8e29804a5551d2fb921730127ec07b3f8cd09f15783147edbf0e37","y_r_sub_p":"5e5b219af63f3cd4a78245a9a8ba7a1046693dda8988c4af1abd3a9eae48f752","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":254,"steps":508} +{"label":"k=(N-1)/2","mode":"x-only","k":"a0201b68462fe9df1d50a457736e575dffffffffffffffffffffffffffffff7f","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"639c5f79d6960dad28aaf51494eda0893f56ce783b0000000000000000000000","y_r":"f3dd590e10ca0007fc02ce69dd1bd92efff2c7ae89c93d980282ae72bf79393f","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"5fdfe497b9d01620e2af5ba88c91a8a200000000000000000000000000000080","x_r_sub_p":"34a05f79d7960dad28aaf51494eda0893f56ce783b0000000000000000000000","y_r_sub_p":"c4e1590e11ca0007fc02ce69dd1bd92efff2c7ae89c93d980282ae72bf79393f","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":254,"steps":444} +{"label":"k=(N-1)/2","mode":"affine/+y","k":"a0201b68462fe9df1d50a457736e575dffffffffffffffffffffffffffffff7f","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"639c5f79d6960dad28aaf51494eda0893f56ce783b0000000000000000000000","y_r":"f3dd590e10ca0007fc02ce69dd1bd92efff2c7ae89c93d980282ae72bf79393f","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"5fdfe497b9d01620e2af5ba88c91a8a200000000000000000000000000000080","x_r_sub_p":"34a05f79d7960dad28aaf51494eda0893f56ce783b0000000000000000000000","y_r_sub_p":"c4e1590e11ca0007fc02ce69dd1bd92efff2c7ae89c93d980282ae72bf79393f","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":254,"steps":444} +{"label":"k=(N-1)/2","mode":"affine/-y","k":"a0201b68462fe9df1d50a457736e575dffffffffffffffffffffffffffffff7f","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"639c5f79d6960dad28aaf51494eda0893f56ce783b0000000000000000000000","y_r":"3c1ea6f1ee35fff803fd319622e426d1000d38517636c267fd7d518d4086c6c0","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"5fdfe497b9d01620e2af5ba88c91a8a200000000000000000000000000000080","x_r_sub_p":"34a05f79d7960dad28aaf51494eda0893f56ce783b0000000000000000000000","y_r_sub_p":"0d22a6f1ef35fff803fd319622e426d1000d38517636c267fd7d518d4086c6c0","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":254,"steps":444} +{"label":"k=0xdeadbeef","mode":"x-only","k":"efbeadde00000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"0e0f56aa1b8c232a6c7cf4542e486dbaef4cc84ef94d6f55a91f2d30f1fdd276","y_r":"8a4dd5cfb555b6ebff5d01eb5320f357b55f4f1a45cb8441c4093e7a7eac54b7","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"ae7d770e74a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"df1256aa1c8c232a6c7cf4542e486dbaef4cc84ef94d6f55a91f2d30f1fdd276","y_r_sub_p":"5b51d5cfb655b6ebff5d01eb5320f357b55f4f1a45cb8441c4093e7a7eac54b7","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":31,"steps":54} +{"label":"k=0xdeadbeef","mode":"affine/+y","k":"efbeadde00000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"b8d410fb8fd0479c195485a648b417fda808110efcfba45d65c4a32677da3a48","x_r":"0e0f56aa1b8c232a6c7cf4542e486dbaef4cc84ef94d6f55a91f2d30f1fdd276","y_r":"8a4dd5cfb555b6ebff5d01eb5320f357b55f4f1a45cb8441c4093e7a7eac54b7","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"ae7d770e74a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"df1256aa1c8c232a6c7cf4542e486dbaef4cc84ef94d6f55a91f2d30f1fdd276","y_r_sub_p":"5b51d5cfb655b6ebff5d01eb5320f357b55f4f1a45cb8441c4093e7a7eac54b7","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"1ea37af6727604a57dadb8d9eb9672fd7355398ba7b354246b6ae4f66bc3fad400","len_k":31,"steps":54} +{"label":"k=0xdeadbeef","mode":"affine/-y","k":"efbeadde00000000000000000000000000000000000000000000000000000000","x_g":"9817f8165b81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","y_g":"7727ef046f2fb863e6ab7a59b74be80257f7eef103045ba29a3b5cd98825c5b7","x_r":"0e0f56aa1b8c232a6c7cf4542e486dbaef4cc84ef94d6f55a91f2d30f1fdd276","y_r":"a5ae2a3049aa491400a2fe14acdf0ca84aa0b0e5ba347bbe3bf6c1858153ab48","x_g_sub_p":"691bf8165c81f259d928ce2ddbfc9b02070b87ce9562a055acbbdcf97e66be79","k_sub_n":"ae7d770e74a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"df1256aa1c8c232a6c7cf4542e486dbaef4cc84ef94d6f55a91f2d30f1fdd276","y_r_sub_p":"76b22a304aaa491400a2fe14acdf0ca84aa0b0e5ba347bbe3bf6c1858153ab48","x2":"49fc54b82902d538bbb56cd0942165e39d2ab50fcfada96b08f3fc38d2e75085","q0":"b99080e52997bcba054ec2a815ac0442780965648cec754b26fbb655808ae539","q1":"ddf5580052d5746c4a05ae8c5a2e43032244176fafbb0a69a0e19ca97d0e854401","len_k":31,"steps":54} +{"label":"small-y (y_r = 1)","mode":"affine/+y","k":"0200000000000000000000000000000000000000000000000000000000000000","x_g":"bc4d6c1d18f56b1f863ea8b9ac97f35d49912302a658168e13f5d583d83fe1f2","y_g":"297200a3ff9ef42585315d403e2427ecdafd9fc29fb1d5e2b1785e3500274a26","x_r":"07f5afaacfcb4bb2b2f6537616680de8a6e53c334177ab35c1b5ce3fefe5e11f","y_r":"0100000000000000000000000000000000000000000000000000000000000000","x_g_sub_p":"8d516c1d19f56b1f863ea8b9ac97f35d49912302a658168e13f5d583d83fe1f2","k_sub_n":"c1bec92f73a12d40c45fb7501923514501000000000000000000000000000000","x_r_sub_p":"d8f8afaad0cb4bb2b2f6537616680de8a6e53c334177ab35c1b5ce3fefe5e11f","y_r_sub_p":"d203000001000000000000000000000000000000000000000000000000000000","x2":"ff5b01922b4ae5fa95e10c7de2ed71bafe53950c41ab87008842418d623253bf","q0":"bf111393fdeea08a846a8d61e8a36accc30dc63574df93d07389c4a3e6a26ee6","q1":"c9a88421278dcfc2c0565a1b33f86472d533685805e2be8a60e1a1e5961b355000","len_k":1,"steps":1} +{"label":"k=0","mode":"affine/+y","error":"ECSM scalar k must be non-zero"} +{"label":"k=N","mode":"affine/+y","error":"ECSM scalar k must be < N"} +{"label":"off-curve yG","mode":"affine/+y","error":"ECSM input point is not on the curve"} +{"label":"yG=p","mode":"affine/+y","error":"ECSM coordinates must be < p"} diff --git a/docs/verification/ecsm-affine/gate/logs/small_y_point.log b/docs/verification/ecsm-affine/gate/logs/small_y_point.log new file mode 100644 index 000000000..532af8887 --- /dev/null +++ b/docs/verification/ecsm-affine/gate/logs/small_y_point.log @@ -0,0 +1,21 @@ +Non-canonical band 2^256 - p = 2^32 + 977 = 4294968273 + +Curve point with y inside the band: + y = 1 (1 < 4294968273: True) + x = 0x1fe1e5ef3fceb5c135ab7741333ce5a6e80d68167653f6b2b24bcbcfaaaff507 + on curve: True + y + p = 0xfffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc30 (< 2^256: True) + headroom: y + p is 4294968272 below 2^256 + +Reachable through the affine ecall: + k = 2 + xG = 0xf2e13fd883d5f5138e1658a6022391495df397acb9a83e861f6bf5181d6c4dbc + yG = 0x264a2700355e78b1e2d5b19fc29ffddaec27243e405d318525f49effa3007229 + -> xR = 0x1fe1e5ef3fceb5c135ab7741333ce5a6e80d68167653f6b2b24bcbcfaaaff507 + yR = 0x0000000000000000000000000000000000000000000000000000000000000001 (== y: True) + +So an unconstrained witness may publish yR' = yR + p, a DIFFERENT 32-byte +value that satisfies every byte range check and the ECDAS yR relation with +q2 reduced by one. YrLtP is what excludes it. + +wrote small_y_point.json diff --git a/docs/verification/ecsm-affine/harness/Cargo.toml b/docs/verification/ecsm-affine/harness/Cargo.toml new file mode 100644 index 000000000..0f224d514 --- /dev/null +++ b/docs/verification/ecsm-affine/harness/Cargo.toml @@ -0,0 +1,16 @@ +[package] +name = "ecsm-affine-harness" +version = "0.1.0" +edition = "2024" +publish = false + +# Standalone workspace: this crate lives under `docs/` and must not be adopted as a +# member of the repo workspace (which lists its members explicitly). +[workspace] + +[dependencies] +ecsm = { path = "../../../../crypto/ecsm" } +num-bigint = "0.4.6" + +[profile.release] +opt-level = 3 diff --git a/docs/verification/ecsm-affine/harness/src/main.rs b/docs/verification/ecsm-affine/harness/src/main.rs new file mode 100644 index 000000000..8a54bac22 --- /dev/null +++ b/docs/verification/ecsm-affine/harness/src/main.rs @@ -0,0 +1,153 @@ +//! Dumps REAL `EcsmWitness` values from the repo's own witness generator, as JSON, so the +//! z3 gate's transcribed model can be evaluated on them. +//! +//! This is the cross-language half of the faithfulness anchor. The Python oracle +//! (`../oracle/ecsm_affine_ref.py`) is an independent reimplementation, which establishes +//! that the gate is reasoning about the right FUNCTION. This harness establishes that it is +//! reasoning about the right COLUMNS: every witness field the model reads is emitted here by +//! `ecsm::compute_witness_with_y` / `compute_witness`, so a column the model mis-transcribed +//! shows up as a mismatch rather than as a silently-wrong UNSAT. +//! +//! It is deliberately tiny and depends only on `crypto/ecsm` — building the prover is not +//! needed to check witness columns, and a heavier harness would not get run. +//! +//! Build and run (from this directory): +//! +//! cargo run --release -- > ../gate/logs/real_witnesses.jsonl +//! +//! Then: `python ../gate/a6_real_witness.py` + +use ecsm::{compute_witness, compute_witness_with_y}; +use num_bigint::BigUint; + +/// secp256k1 generator, and the curve order, as little-endian 32-byte values. +const GX_BE: &str = "79BE667EF9DCBBAC55A06295CE870B07029BFCDB2DCE28D959F2815B16F81798"; +const GY_BE: &str = "483ADA7726A3C4655DA4FBFC0E1108A8FD17B448A68554199C47D08FFB10D4B8"; +const N_BE: &str = "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141"; +const P_BE: &str = "FFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEFFFFFC2F"; + +fn le32_from_be_hex(hex: &str) -> [u8; 32] { + let v = BigUint::parse_bytes(hex.as_bytes(), 16).expect("hex"); + let mut out = [0u8; 32]; + for (i, b) in v.to_bytes_le().into_iter().enumerate() { + out[i] = b; + } + out +} + +fn le32(v: &BigUint) -> [u8; 32] { + let mut out = [0u8; 32]; + for (i, b) in v.to_bytes_le().into_iter().enumerate() { + out[i] = b; + } + out +} + +fn hex_le(bytes: &[u8]) -> String { + bytes.iter().map(|b| format!("{b:02x}")).collect() +} + +/// The scalars worth pinning: the two the x-only path called degenerate, the bit-length +/// extremes, and a couple of ordinary ones. +fn scalars() -> Vec<(String, BigUint)> { + let n = BigUint::parse_bytes(N_BE.as_bytes(), 16).unwrap(); + let one = BigUint::from(1u8); + vec![ + ("k=1".into(), one.clone()), + ("k=2".into(), BigUint::from(2u8)), + ("k=3".into(), BigUint::from(3u8)), + ("k=N-1".into(), &n - &one), + ("k=N-2".into(), &n - BigUint::from(2u8)), + ("k=2^255".into(), BigUint::from(1u8) << 255), + ("k=2^255-1".into(), (BigUint::from(1u8) << 255) - &one), + ("k=(N-1)/2".into(), (&n - &one) / BigUint::from(2u8)), + ("k=0xdeadbeef".into(), BigUint::from(0xdead_beefu64)), + ] +} + +/// Emits one JSON object per line. Every field the gate's model reads is present, plus the +/// mode, so `a6_real_witness.py` can check the x-only and affine paths separately. +fn emit(label: &str, mode: &str, k: &[u8; 32], xg: &[u8; 32], yg: Option<&[u8; 32]>) { + let w = match yg { + Some(y) => compute_witness_with_y(k, xg, y), + None => compute_witness(k, xg), + }; + let w = match w { + Ok(w) => w, + Err(e) => { + println!("{{\"label\":\"{label}\",\"mode\":\"{mode}\",\"error\":\"{e}\"}}"); + return; + } + }; + // Only the fields this campaign's model consumes. The ECDAS step array is large and the + // earlier board already anchors it (`gate/positive_real_witness.py` under + // `thoughts/ec-recover-opt/` on branch `feat/ec-lincomb2`, which was never merged), + // so it is summarised by its length rather than dumped. + println!( + "{{\"label\":\"{label}\",\"mode\":\"{mode}\",\ + \"k\":\"{}\",\"x_g\":\"{}\",\"y_g\":\"{}\",\ + \"x_r\":\"{}\",\"y_r\":\"{}\",\ + \"x_g_sub_p\":\"{}\",\"k_sub_n\":\"{}\",\ + \"x_r_sub_p\":\"{}\",\"y_r_sub_p\":\"{}\",\ + \"x2\":\"{}\",\"q0\":\"{}\",\"q1\":\"{}\",\ + \"len_k\":{},\"steps\":{}}}", + hex_le(k), + hex_le(&w.x_g), + hex_le(&w.y_g), + hex_le(&w.x_r), + hex_le(&w.y_r), + hex_le(&w.x_g_sub_p), + hex_le(&w.k_sub_n), + hex_le(&w.x_r_sub_p), + hex_le(&w.y_r_sub_p), + hex_le(&w.x2), + hex_le(&w.q0), + hex_le(&w.q1), + w.len_k, + w.steps.len(), + ); +} + +fn main() { + let gx = le32_from_be_hex(GX_BE); + let gy = le32_from_be_hex(GY_BE); + let p = BigUint::parse_bytes(P_BE.as_bytes(), 16).unwrap(); + let gy_big = BigUint::parse_bytes(GY_BE.as_bytes(), 16).unwrap(); + let gy_neg = le32(&(&p - &gy_big)); + + for (label, k) in scalars() { + let k = le32(&k); + // x-only: yG is the canonical even lift, recovered internally from xG. + emit(&label, "x-only", &k, &gx, None); + // affine, both roots — the pair A3's forgery is built from. Both must produce a + // valid witness (that is the gap), and their y_r must differ. + emit(&label, "affine/+y", &k, &gx, Some(&gy)); + emit(&label, "affine/-y", &k, &gx, Some(&gy_neg)); + } + + // The y = 1 point from ../oracle/small_y_point.py, reached as 2·(2^-1·Q), so the honest + // y_r sits at the very bottom of the non-canonical band and y_r_sub_p is at its extreme. + let small_xg = + le32_from_be_hex("F2E13FD883D5F5138E1658A6022391495DF397ACB9A83E861F6BF5181D6C4DBC"); + let small_yg = + le32_from_be_hex("264A2700355E78B1E2D5B19FC29FFDDAEC27243E405D318525F49EFFA3007229"); + let two = le32(&BigUint::from(2u8)); + emit( + "small-y (y_r = 1)", + "affine/+y", + &two, + &small_xg, + Some(&small_yg), + ); + + // Rejections the executor relies on: the validation set A4 of the oracle anchors. + let zero = [0u8; 32]; + emit("k=0", "affine/+y", &zero, &gx, Some(&gy)); + let n_le = le32_from_be_hex(N_BE); + emit("k=N", "affine/+y", &n_le, &gx, Some(&gy)); + let mut off_curve = gy; + off_curve[0] ^= 1; + emit("off-curve yG", "affine/+y", &two, &gx, Some(&off_curve)); + let p_le = le32_from_be_hex(P_BE); + emit("yG=p", "affine/+y", &two, &gx, Some(&p_le)); +} diff --git a/docs/verification/ecsm-affine/oracle/ecsm_affine_ref.py b/docs/verification/ecsm-affine/oracle/ecsm_affine_ref.py new file mode 100644 index 000000000..5bc7f56be --- /dev/null +++ b/docs/verification/ecsm-affine/oracle/ecsm_affine_ref.py @@ -0,0 +1,220 @@ +"""Independent reference for the ECSM **affine** ecall (`ECSM_AFFINE_SYSCALL_NUMBER`). + +Written from the curve definition, not from the repo: no `k256`, no `ecsm` crate, no +`num_bigint`. Group law is plain textbook chord/tangent over `F_p` with Python ints, so a +transcription error in `crypto/ecsm` cannot hide behind a shared implementation. + +What it defines (the contract the gate's UNSATs are *about*): + + x_only_mul(k, xG) → x(k·P), P = the canonical EVEN lift of xG (pre-existing ecall) + affine_mul(k, xG, yG) → (x, y) of k·(xG, yG) (the NEW ecall) + +and the ABI/validation predicates the executor applies before either +(`executor/src/vm/instruction/execution.rs`, `SyscallNumbers::EcsmAffine` arm): + + addr_limb_ok(addr, span) → the low-limb no-straddle test + operands_disjoint(...) → the xG‖yG vs k overlap guard + validate_affine(...) → 0 < k < N, xG < p, yG < p, (xG,yG) on curve + +The affine result is **root-dependent** by construction — that is the whole point of the +variant and the reason the AIR has to pin `yG` to the caller's buffer: + + affine_mul(k, x, p - y) == (X, p - Y) where (X, Y) == affine_mul(k, x, y) + +so publishing `yR` makes the input parity observable, while `x_only_mul` cannot see it. + +Citations to the code being modelled are inline, `file:line` against the branch +`verify/ecsm-affine-selector` (head of PR #879 plus this campaign). +""" + +# ── secp256k1 (SEC 2 v2 §2.4.1). Recomputed here, cross-checked against +# crypto/ecsm/src/lib.rs by test_oracle.py's anchor A0. ── + +P = 2**256 - 2**32 - 977 +N = 0xFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFFEBAAEDCE6AF48A03BBFD25E8CD0364141 +A = 0 +B = 7 +GX = 0x79BE667EF9DCBBAC55A06295CE870B07029BFCDB2DCE28D959F2815B16F81798 +GY = 0x483ADA7726A3C4655DA4FBFC0E1108A8FD17B448A68554199C47D08FFB10D4B8 +G = (GX, GY) + +# `2^256 - p` — the width of the non-canonical band a 32-byte y can occupy, i.e. the +# largest `y` for which `y + p` is still 32-byte representable. This is the number the +# `YrLtP` range check exists to exclude; see oracle/small_y_point.py, which constructs a +# real curve point inside the band. +NONCANONICAL_BAND = 2**256 - P # == 2**32 + 977 + + +# ── field ── + +def inv(a): + """1/a mod p. Fermat; p is prime (SEC2 / A-PRIME).""" + a %= P + if a == 0: + raise ZeroDivisionError("no inverse of 0 mod p") + return pow(a, P - 2, P) + + +def is_square(a): + return a == 0 or pow(a % P, (P - 1) // 2, P) == 1 + + +def sqrt_mod_p(a): + """A square root of `a` mod p, or None. p ≡ 3 (mod 4), so it is a^((p+1)/4).""" + a %= P + if not is_square(a): + return None + r = pow(a, (P + 1) // 4, P) + assert (r * r - a) % P == 0 + return r + + +# ── group law (affine chord/tangent; O is None) ── + +def is_on_curve(pt): + if pt is None: + return True + x, y = pt + if not (0 <= x < P and 0 <= y < P): + return False + return (y * y - (x * x % P * x + A * x + B)) % P == 0 + + +def neg(pt): + if pt is None: + return None + x, y = pt + return (x, (-y) % P) + + +def add(p1, p2): + if p1 is None: + return p2 + if p2 is None: + return p1 + x1, y1 = p1 + x2, y2 = p2 + if x1 == x2: + if (y1 + y2) % P == 0: + return None # P + (−P) = O + lam = (3 * x1 * x1 + A) * inv(2 * y1) % P # tangent + else: + lam = (y2 - y1) * inv(x2 - x1) % P # chord + x3 = (lam * lam - x1 - x2) % P + y3 = (lam * (x1 - x3) - y1) % P + return (x3, y3) + + +def mul(k, pt): + """k·pt by double-and-add from the MSB down — the same schedule the chip proves + (`crypto/ecsm/src/curve.rs::schedule`), so a schedule bug shows up as a mismatch + rather than being reproduced.""" + if k % N == 0 or pt is None: + return None + k %= N + acc = None + for bit in reversed(range(k.bit_length())): + acc = add(acc, acc) + if (k >> bit) & 1: + acc = add(acc, pt) + return acc + + +# ── lifts ── + +def recover_y_canonical(x): + """The EVEN root of x³+b, or None. Mirrors `crypto/ecsm/src/curve.rs:recover_y_canonical` + (`curve.rs:18-60` on this branch). Used only by the x-only path.""" + if not 0 <= x < P: + return None + y = sqrt_mod_p((x * x % P * x + B) % P) + if y is None: + return None + return y if y % 2 == 0 else P - y + + +# ── the two ecall semantics ── + +class EcsmError(Exception): + """Mirrors `ecsm::EcsmError` (crypto/ecsm/src/lib.rs:70-100).""" + + +def validate_scalar(k): + if k == 0: + raise EcsmError("ScalarIsZero") + if k >= N: + raise EcsmError("ScalarOutOfRange") + + +def x_only_mul(k, xg): + """Pre-existing ecall (`ECSM_SYSCALL_NUMBER`): x(k·P) with P the even lift of xG. + + Root-independent: x(k·P) == x(k·(−P)) for every k, which is exactly why the AIR is + allowed to leave yG's parity free on this path (`curve.rs:18-31` comment).""" + validate_scalar(k) + if xg >= P: + raise EcsmError("CoordinateOutOfRange") + yg = recover_y_canonical(xg) + if yg is None: + raise EcsmError("NotOnCurve") + r = mul(k, (xg, yg)) + assert r is not None, "k·P = O impossible for 0= P or yg >= P: + raise EcsmError("CoordinateOutOfRange") + if not is_on_curve((xg, yg)): + raise EcsmError("NotOnCurve") + r = mul(k, (xg, yg)) + assert r is not None + return r + + +# ── executor ABI predicates (execution.rs, `SyscallNumbers::EcsmAffine` arm) ── + +MASK64 = 2**64 - 1 + + +def addr_limb_ok(addr, span): + """`executor/src/vm/instruction/execution.rs::addr_limb_ok`: the operand's low 32-bit + limb plus its span must not reach 2^32, so a multi-byte access cannot straddle the + limb boundary while the AIR reuses the high limb unchanged.""" + return (addr % 2**32) + span < 2**32 + + +def operands_disjoint(addr_xg, addr_k, point_bytes=64, scalar_bytes=32): + """The affine overlap guard (`execution.rs`, EcsmAffine arm): the point buffer + [addr_xg, +64) and the scalar [addr_k, +32) must not intersect. + + Computed in unbounded ints, which is what the branch's `u128` widening buys: the + naive u64 form `addr_k < addr_xg + 64` wraps at `addr_xg = 2^64 - 64`, making the + clause vacuously false and skipping the guard. That address PASSES + `addr_limb_ok(·, 63)`, so the wrap is reachable — see gate/a4_addressing.py N-WRAP.""" + return not (addr_k < addr_xg + point_bytes and addr_xg < addr_k + scalar_bytes) + + +def operands_disjoint_u64_buggy(addr_xg, addr_k): + """The pre-fix wrapping form, kept as the negative control's oracle.""" + lhs = (addr_xg + 64) & MASK64 + rhs = (addr_k + 32) & MASK64 + return not (addr_k < lhs and addr_xg < rhs) + + +# ── little-endian 32-byte codec (the ABI's wire form) ── + +def to_le32(v): + assert 0 <= v < 2**256 + return list(v.to_bytes(32, "little")) + + +def from_le32(bs): + assert len(bs) == 32 + return int.from_bytes(bytes(bs), "little") diff --git a/docs/verification/ecsm-affine/oracle/small_y_point.json b/docs/verification/ecsm-affine/oracle/small_y_point.json new file mode 100644 index 000000000..b22e2a86d --- /dev/null +++ b/docs/verification/ecsm-affine/oracle/small_y_point.json @@ -0,0 +1,17 @@ +{ + "band": 4294968273, + "small_y_point": { + "x": "1fe1e5ef3fceb5c135ab7741333ce5a6e80d68167653f6b2b24bcbcfaaaff507", + "y": "0000000000000000000000000000000000000000000000000000000000000001" + }, + "ecsm_instance": { + "k": 2, + "x_g": "f2e13fd883d5f5138e1658a6022391495df397acb9a83e861f6bf5181d6c4dbc", + "y_g": "264a2700355e78b1e2d5b19fc29ffddaec27243e405d318525f49effa3007229" + }, + "expected": { + "x_r": "1fe1e5ef3fceb5c135ab7741333ce5a6e80d68167653f6b2b24bcbcfaaaff507", + "y_r": "0000000000000000000000000000000000000000000000000000000000000001" + }, + "forged_y_r": "fffffffffffffffffffffffffffffffffffffffffffffffffffffffefffffc30" +} diff --git a/docs/verification/ecsm-affine/oracle/small_y_point.py b/docs/verification/ecsm-affine/oracle/small_y_point.py new file mode 100644 index 000000000..f247e4baa --- /dev/null +++ b/docs/verification/ecsm-affine/oracle/small_y_point.py @@ -0,0 +1,130 @@ +"""Constructs a REAL secp256k1 point whose `y` lies in the non-canonical band +`y < 2^256 − p = 2^32 + 977`, i.e. a point for which `y + p` is still a 32-byte value. + +Why this file exists: PR #879's soundness section claims the `YrLtP` range check is +load-bearing because "such points are constructible: `3 | p−1` makes cubing 3-to-1, so a +small target `y` has a cube-root preimage about a third of the time". That is an existence +claim about the attack surface, and the honest way to review it is to build the point. +`gate/a2_yr_lt_p.py` then uses the point as a concrete forgery instance rather than an +abstract SAT. + +Method. Fix a target `y`; the curve equation demands `x³ = y² − 7`. Cubing on `F_p*` is +3-to-1 exactly when `3 | p − 1`, which holds, with 3-adic valuation `v_3(p−1) = 1`. Write +`p − 1 = 3m`, `gcd(m, 3) = 1`. Then `c` is a cubic residue iff `c^m = 1`, and in that case +`c^d` with `3d ≡ 1 (mod m)` is a cube root: + + (c^d)³ = c^{3d} = c^{1 + λm} = c · (c^m)^λ = c. + +So sweep `y = 0, 1, 2, …`, keep the first `y` whose `y² − 7` is a cubic residue. About one +in three qualifies, so the sweep is a handful of iterations — the point is found in the +very bottom of the band, far below `2^32 + 977`. + +Run: `python small_y_point.py` +""" + +import json +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).parent)) +from ecsm_affine_ref import ( + N, + NONCANONICAL_BAND, + P, + affine_mul, + is_on_curve, + mul, +) + +M = (P - 1) // 3 +assert (P - 1) % 3 == 0 and M % 3 != 0, "v_3(p-1) must be exactly 1 for the fast cube root" +D = pow(3, -1, M) # 3·D ≡ 1 (mod m) + + +def is_cubic_residue(c): + return pow(c % P, M, P) == 1 + + +def cube_root(c): + """A cube root of `c` mod p, or None.""" + c %= P + if c == 0: + return 0 + if not is_cubic_residue(c): + return None + r = pow(c, D, P) + assert (r * r % P * r - c) % P == 0 + return r + + +def find_small_y_point(limit=4096): + """Smallest `y ≥ 1` in the band for which a curve point `(x, y)` exists.""" + for y in range(1, limit): + x = cube_root((y * y - 7) % P) + if x is None: + continue + assert is_on_curve((x, y)), "cube root did not land on the curve" + assert y < NONCANONICAL_BAND, "y escaped the non-canonical band" + return x, y + return None + + +def ecsm_instance(q): + """An ECSM *call* whose output is `q`, so the forged `yR = y_q + p` is reachable + through the chip rather than only through the curve. + + `k = 2` and `P = 2^{-1}·q` (inverse mod N, the group order) gives `2·P = q`. `k = 2` + also keeps the chip on its generic path: one ECDAS doubling row, no `k = 1` echo + (where the drain is forced equal to the seed and `yR` inherits `YG`'s byte checks + directly).""" + inv2 = pow(2, -1, N) + pt = mul(inv2, q) + assert mul(2, pt) == q + return 2, pt + + +def main(): + found = find_small_y_point() + if found is None: + print("[FAIL] no small-y point found in the swept range") + return 1 + x, y = found + + print("Non-canonical band 2^256 - p = 2^32 + 977 =", NONCANONICAL_BAND) + print() + print("Curve point with y inside the band:") + print(f" y = {y} ({y} < {NONCANONICAL_BAND}: {y < NONCANONICAL_BAND})") + print(f" x = 0x{x:064x}") + print(f" on curve: {is_on_curve((x, y))}") + print(f" y + p = 0x{(y + P):064x} (< 2^256: {y + P < 2**256})") + print(f" headroom: y + p is {(2**256 - (y + P))} below 2^256") + print() + + k, pt = ecsm_instance((x, y)) + got = affine_mul(k, pt[0], pt[1]) + print("Reachable through the affine ecall:") + print(f" k = {k}") + print(f" xG = 0x{pt[0]:064x}") + print(f" yG = 0x{pt[1]:064x}") + print(f" -> xR = 0x{got[0]:064x}") + print(f" yR = 0x{got[1]:064x} (== y: {got[1] == y})") + print() + print("So an unconstrained witness may publish yR' = yR + p, a DIFFERENT 32-byte") + print("value that satisfies every byte range check and the ECDAS yR relation with") + print("q2 reduced by one. YrLtP is what excludes it.") + + out = { + "band": NONCANONICAL_BAND, + "small_y_point": {"x": f"{x:064x}", "y": f"{y:064x}"}, + "ecsm_instance": {"k": k, "x_g": f"{pt[0]:064x}", "y_g": f"{pt[1]:064x}"}, + "expected": {"x_r": f"{got[0]:064x}", "y_r": f"{got[1]:064x}"}, + "forged_y_r": f"{(got[1] + P):064x}", + } + dest = Path(__file__).parent / "small_y_point.json" + dest.write_text(json.dumps(out, indent=2) + "\n") + print(f"\nwrote {dest.name}") + return 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/oracle/test_oracle.py b/docs/verification/ecsm-affine/oracle/test_oracle.py new file mode 100644 index 000000000..c150e464f --- /dev/null +++ b/docs/verification/ecsm-affine/oracle/test_oracle.py @@ -0,0 +1,374 @@ +"""Anchor harness for the ECSM-affine oracle. + +Anchors are what make the gate's UNSATs meaningful: they establish that +`ecsm_affine_ref.py` defines the SAME function the executor computes and the chip claims +to prove. Each anchor is independent — a missing fixture or a missing optional package +SKIPs only itself — the BLAKE3 harness's cascade defect, recorded under "Harness defects" +in `thoughts/blake3/README.md` on branch feat/blake3-accelerator, is deliberately not +repeated here. + + A0 repo constants — p, N, b, 3p parsed out of `crypto/ecsm/src/lib.rs` and compared + against the values recomputed here. + A1 curve/group — G on curve; N·G = O; published small multiples of G; k·(N−k) + symmetry; associativity spot-checks. + A2 x-only agreement — `affine_mul(k, xG, even_lift(xG)).x == x_only_mul(k, xG)`. The new + ecall must not change the pre-existing one's answer. + A3 root dependence — `affine_mul(k, x, p−y) == (X, p−Y)`, and `x` is invariant. This is + the parity gap the AIR's yG-read closes; the anchor pins that it is + real, not hypothetical. + A4 validation — the executor's accept/reject set: 0 < k < N, xG < p, yG < p, + on-curve, plus the "k = 1 and k = N−1 are ordinary" claim. + A5 ABI predicates — `addr_limb_ok`, the overlap guard as exact interval disjointness, + and the u64-wrap negative control. + A6 ecrecover use — the y-from-x reconstruction the affine ecall REPLACES agrees with + the y the chip now returns, over random instances. Anchors the + claim that dropping `solve_y` is semantics-preserving. + A7 optional cross — differential against the `ecdsa`/`coincurve` PyPI package if + installed (SKIP otherwise). + +Run: `python test_oracle.py` +""" + +import random +import re +import sys +from pathlib import Path + +sys.path.insert(0, str(Path(__file__).parent)) +from ecsm_affine_ref import ( + B, + G, + GX, + GY, + N, + P, + EcsmError, + add, + addr_limb_ok, + affine_mul, + from_le32, + inv, + is_on_curve, + mul, + neg, + operands_disjoint, + operands_disjoint_u64_buggy, + recover_y_canonical, + sqrt_mod_p, + to_le32, + x_only_mul, +) + +random.seed(0xEC5A) + + +def find_repo_root(start=None): + """The lambda_vm root, located by marker (workspace `Cargo.toml` next to `prover/`) + rather than by a hard-coded `parents[N]`, which breaks silently when the campaign + directory moves. Anchor A0 reads repo constants by path, so a wrong root would compare + against nothing; returns None so A0 SKIPs with a named reason instead of guessing.""" + here = (start or Path(__file__)).resolve() + for cand in here.parents: + if (cand / "Cargo.toml").is_file() and (cand / "prover").is_dir(): + if "[workspace]" in (cand / "Cargo.toml").read_text(): + return cand + return None + + +REPO = find_repo_root() +results = [] + + +def report(name, verdict, detail=""): + results.append((name, verdict, detail)) + print(f"[{verdict:5}] {name} {detail}") + + +# ── A0: repo constants ─────────────────────────────────────────────────────── + +def _parse_le_bytes(src, name): + m = re.search(rf"pub const {name}: \[u8; \d+\] = \[(.*?)\];", src, re.S) + if not m: + return None + vals = [int(v, 16) for v in re.findall(r"0x([0-9A-Fa-f]{2})", m.group(1))] + return int.from_bytes(bytes(vals), "little") + + +def a0_constants(): + if REPO is None: + report("A0 repo constants", "SKIP", + "no lambda_vm repo root found above this file") + return + src_path = REPO / "crypto" / "ecsm" / "src" / "lib.rs" + if not src_path.exists(): + report("A0 repo constants", "SKIP", f"{src_path} not found") + return + src = src_path.read_text() + checks = { + "p (P_BYTES)": (_parse_le_bytes(src, "P_BYTES"), P), + "N (N_BYTES)": (_parse_le_bytes(src, "N_BYTES"), N), + "3p (R_BYTES)": (_parse_le_bytes(src, "R_BYTES"), 3 * P), + } + m = re.search(r"pub const B: u64 = (\d+);", src) + checks["b (B)"] = (int(m.group(1)) if m else None, B) + bad = [k for k, (got, want) in checks.items() if got != want] + report("A0 repo constants", "PASS" if not bad else "FAIL", + f"{len(checks)} constants parsed from crypto/ecsm/src/lib.rs match" + if not bad else f"mismatched: {bad}") + + +# ── A1: curve / group sanity ───────────────────────────────────────────────── + +# Published secp256k1 multiples of G (widely cited; any independent source agrees). +KNOWN_MULTIPLES = { + 1: (GX, GY), + 2: (0xC6047F9441ED7D6D3045406E95C07CD85C778E4B8CEF3CA7ABAC09B95C709EE5, + 0x1AE168FEA63DC339A3C58419466CEAEEF7F632653266D0E1236431A950CFE52A), + 3: (0xF9308A019258C31049344F85F89D5229B531C845836F99B08601F113BCE036F9, + 0x388F7B0F632DE8140FE337E62A37F3566500A99934C2231B6CB9FD7584B8E672), + 4: (0xE493DBF1C10D80F3581E4904930B1404CC6C13900EE0758474FA94ABE8C4CD13, + 0x51ED993EA0D455B75642E2098EA51448D967AE33BFBDFE40CFE97BDC47739922), + 5: (0x2F8BDE4D1A07209355B4A7250A5C5128E88B84BDDC619AB7CBA8D569B240EFE4, + 0xD8AC222636E5E3D6D4DBA9DDA6C9C426F788271BAB0D6840DCA87D3AA6AC62D6), +} + + +def a1_group(): + ok = is_on_curve(G) and mul(N - 1, G) == neg(G) and mul(N, G) is None + for k, want in KNOWN_MULTIPLES.items(): + got = mul(k, G) + ok &= got == want + ok &= is_on_curve(got) + # k·G and (N−k)·G are negatives; associativity spot-check. + for _ in range(40): + k = random.randrange(1, N) + ok &= mul(N - k, G) == neg(mul(k, G)) + for _ in range(20): + a, b = random.randrange(1, N), random.randrange(1, N) + ok &= add(mul(a, G), mul(b, G)) == mul((a + b) % N, G) + report("A1 curve/group", "PASS" if ok else "FAIL", + f"G on curve, N·G = O, {len(KNOWN_MULTIPLES)} published multiples, " + "40 negation + 20 additivity checks") + + +# ── A2: x-only agreement ───────────────────────────────────────────────────── + +def a2_xonly_agreement(): + ok = True + n_checked = 0 + ks = [1, 2, 3, 7, N - 1, N - 2, 2**255, 2**255 - 1, (N - 1) // 2] + ks += [random.randrange(1, N) for _ in range(15)] + xs = [GX] + [mul(random.randrange(1, N), G)[0] for _ in range(8)] + for x in xs: + y = recover_y_canonical(x) + assert y is not None and y % 2 == 0 + for k in ks: + ok &= affine_mul(k, x, y)[0] == x_only_mul(k, x) + n_checked += 1 + report("A2 x-only agreement", "PASS" if ok else "FAIL", + f"{n_checked} (k, xG) pairs: affine_mul(...).x == x_only_mul(...), " + "incl. k = 1, 2, N−1, N−2, 2^255") + + +# ── A3: root dependence (the parity gap the AIR must close) ────────────────── + +def a3_root_dependence(sample=200): + ok = True + differed = 0 + for _ in range(sample): + k = random.randrange(2, N - 1) + x, y = mul(random.randrange(1, N), G) + xr, yr = affine_mul(k, x, y) + xr2, yr2 = affine_mul(k, x, (P - y) % P) + ok &= xr2 == xr # x-only path cannot see the parity ... + ok &= yr2 == (P - yr) % P # ... but the affine one returns a different y + differed += yr2 != yr + ok &= differed == sample # the two roots NEVER agree (y ≠ 0 on secp256k1) + report("A3 root dependence", "PASS" if ok else "FAIL", + f"{sample} instances: x invariant under yG → p−yG, y negated in ALL " + f"{differed} of them ⇒ publishing yR makes the input parity observable") + + +# ── A4: validation set ─────────────────────────────────────────────────────── + +def _rejects(fn, *args): + try: + fn(*args) + return None + except EcsmError as e: + return str(e) + + +def a4_validation(): + x, y = mul(7, G) + cases = [ + ("k = 0", (0, x, y), "ScalarIsZero"), + ("k = N", (N, x, y), "ScalarOutOfRange"), + ("k > N", (N + 1, x, y), "ScalarOutOfRange"), + ("xG = p", (3, P, y), "CoordinateOutOfRange"), + ("yG = p", (3, x, P), "CoordinateOutOfRange"), + ("yG = p + small", (3, x, P + 1), "CoordinateOutOfRange"), + ("off curve", (3, x, (y + 1) % P), "NotOnCurve"), + ("yG = 0", (3, x, 0), "NotOnCurve"), + ] + ok = all(_rejects(affine_mul, *a) == want for _, a, want in cases) + # Accepted: the whole open scalar range, including the two the x-only path had to + # treat as degenerate (PR #879: "with y supplied by the chip those scalars are + # ordinary — cofactor 1 and prime N, so k·P ≠ O for every k ∈ (0, N)"). + for k in [1, 2, N - 2, N - 1]: + r = affine_mul(k, x, y) + ok &= is_on_curve(r) and r == mul(k, (x, y)) + ok &= affine_mul(1, x, y) == (x, y) # k = 1 echoes the input point + ok &= affine_mul(N - 1, x, y) == (x, (P - y) % P) # k = N−1 negates it + report("A4 validation set", "PASS" if ok else "FAIL", + f"{len(cases)} rejections match the executor's error kinds; " + "k ∈ {1, 2, N−2, N−1} all accepted and ordinary") + + +# ── A5: ABI predicates ────────────────────────────────────────────────────── + +def a5_abi(): + ok = True + # addr_limb_ok is exactly "the span fits below the next 2^32 boundary". + for span in (31, 63): + boundary = 2**32 - span + ok &= addr_limb_ok(boundary - 1, span) + ok &= not addr_limb_ok(boundary, span) + ok &= not addr_limb_ok(2**32 - 1, span) + ok &= addr_limb_ok(0, span) + # the high limb is irrelevant, by design (the AIR reuses it unchanged) + ok &= addr_limb_ok((7 << 32) + boundary - 1, span) + ok &= not addr_limb_ok((7 << 32) + boundary, span) + # The overlap guard is exact interval disjointness, not a distance bound: a scalar + # placed immediately below the point (addr_k + 32 == addr_xg) IS disjoint. + base = 0x8000_0000 + ok &= operands_disjoint(base, base - 32) # k directly below the point + ok &= not operands_disjoint(base, base - 31) # one byte of overlap + ok &= operands_disjoint(base, base + 64) # k directly above + ok &= not operands_disjoint(base, base + 63) + for d in range(-96, 97): + want = not (set(range(base, base + 64)) & set(range(base + d, base + d + 32))) + ok &= operands_disjoint(base, base + d) == want + # NEGATIVE CONTROL: the pre-fix u64 form skips the guard at the wrap address, and + # that address passes addr_limb_ok(·, 63) so it is reachable. + wrap = 2**64 - 64 + reachable = addr_limb_ok(wrap, 63) + buggy_accepts_overlap = operands_disjoint_u64_buggy(wrap, wrap) and not operands_disjoint(wrap, wrap) + ok &= reachable and buggy_accepts_overlap + report("A5 ABI predicates", "PASS" if ok else "FAIL", + "limb bound exact at both spans (31/63), overlap guard == interval " + "disjointness over 193 offsets; u64-wrap control: addr 2^64−64 passes " + f"addr_limb_ok (={reachable}) yet the pre-fix guard misses a total overlap") + + +# ── A6: the ecrecover reconstruction the affine ecall replaces ─────────────── + +def _solve_y_from_two_x(xg, yg, x1, x2): + """The x-only recovery the guest used to do: two accelerator queries give + `x1 = x(k·P)` and `x2 = x((k+1)·P)`; the chord law through the known base point then + fixes which root of `x1³ + b` is `y(k·P)`. + + Rather than reproduce the guest's exact algebra (which is what PR #879 deletes), take + both roots and keep the one whose chord with `(xG, yG)` lands on `x2`. The anchor is + about the VALUE, not the arithmetic route. The disambiguation is total: flipping `y1` + changes `λ² = ((y1 − yG)/(x1 − xG))²` unless `4·y1·yG ≡ 0`, and secp256k1 has no + point with `y = 0`.""" + if x1 == xg: + return None # k·P = ±P: the chord degenerates, guest handles it separately + cand = sqrt_mod_p((x1 * x1 % P * x1 + B) % P) + if cand is None: + return None + for y1 in (cand, (P - cand) % P): + lam = (y1 - yg) * inv(x1 - xg) % P + if (lam * lam - x1 - xg) % P == x2: + return y1 + return None + + +def a6_ecrecover_equivalence(sample=60): + ok = True + n = 0 + for _ in range(sample): + k = random.randrange(2, N - 2) + xg, yg = mul(random.randrange(1, N), G) + # what the chip now returns directly: + x1, y1 = affine_mul(k, xg, yg) + # what the guest used to compute: two x-only queries + the chord law + x2 = affine_mul(k + 1, xg, yg)[0] + rec = _solve_y_from_two_x(xg, yg, x1, x2) + if rec is None: + continue # degenerate chord (k·P = ±P); not what this anchor measures + ok &= rec == y1 + n += 1 + report("A6 ecrecover equivalence", "PASS" if ok else "FAIL", + f"{n} instances: y recovered from x(k·P) + x((k+1)·P) + the chord law " + "equals the y the affine ecall returns ⇒ dropping `solve_y` is " + "semantics-preserving") + + +# ── A7: optional third-party cross-check ──────────────────────────────────── + +def a7_third_party(sample=25): + try: + from ecdsa.ellipticcurve import Point # type: ignore + from ecdsa.curves import SECP256k1 # type: ignore + except Exception: + report("A7 third-party cross-check", "SKIP", + "python `ecdsa` package not installed (pip install ecdsa)") + return + curve = SECP256k1.curve + gen = SECP256k1.generator + ok = True + for _ in range(sample): + k = random.randrange(1, N) + j = random.randrange(1, N) + base = mul(j, G) + theirs = Point(curve, base[0], base[1]) * k + ok &= affine_mul(k, base[0], base[1]) == (theirs.x(), theirs.y()) + report("A7 third-party cross-check", "PASS" if ok else "FAIL", + f"{sample} random k·P against the `ecdsa` package") + + +# ── codec sanity (cheap, keeps the ABI wire form honest) ───────────────────── + +def a8_codec(): + ok = all(from_le32(to_le32(v)) == v + for v in [0, 1, P - 1, N - 1, 2**256 - 1, GX, GY]) + ok &= to_le32(1)[0] == 1 and to_le32(1)[31] == 0 # little-endian, as the ABI states + report("A8 LE32 codec", "PASS" if ok else "FAIL", "round-trip + endianness") + + +def main(): + a0_constants() + a1_group() + a2_xonly_agreement() + a3_root_dependence() + a4_validation() + a5_abi() + a6_ecrecover_equivalence() + a7_third_party() + a8_codec() + + passed = [n for n, v, _ in results if v == "PASS"] + skipped = [n for n, v, _ in results if v == "SKIP"] + failed = [n for n, v, _ in results if v == "FAIL"] + print() + if failed: + status = "NOT VALIDATED" + elif skipped: + status = "PARTIALLY VALIDATED" + else: + status = "VALIDATED" + print(f"ORACLE STATUS: {status} ({len(passed)} pass, {len(skipped)} skip, " + f"{len(failed)} fail)") + # Say what it is NOT anchored on, rather than printing a banner that outlives the + # evidence (the defect BLAKE3's harness shipped with; see README there). + if skipped: + print(" NOT anchored on: " + ", ".join(skipped)) + if failed: + print(" FAILURES: " + ", ".join(failed)) + return 1 if failed else 0 + + +if __name__ == "__main__": + sys.exit(main()) diff --git a/docs/verification/ecsm-affine/run_gate.sh b/docs/verification/ecsm-affine/run_gate.sh new file mode 100755 index 000000000..6a95b617a --- /dev/null +++ b/docs/verification/ecsm-affine/run_gate.sh @@ -0,0 +1,69 @@ +#!/usr/bin/env bash +# Runs the whole ECSM-affine campaign and writes each stage's output to gate/logs/. +# +# Order matters: the anchors run BEFORE the lemmas, because an UNSAT is only worth reading +# once the model has been shown to describe the right function (oracle) and the right columns +# (real-witness anchor). The transcription audit runs first of all, since a premise that no +# longer holds invalidates whatever the lemmas concluded from it. +# +# Usage: +# ./run_gate.sh # everything +# ./run_gate.sh --quick # skip the Rust harness rebuild (reuse the existing dump) +# +# Dependencies: python3 with z3-solver + sympy (+ ecdsa for the optional third-party anchor). +# A local venv at .venv is used when present; otherwise `python3` from PATH. + +set -uo pipefail +cd "$(dirname "$0")" + +# Absolute, so the per-stage subshells can `cd` freely. +if [[ -x .venv/bin/python ]]; then + PY="$PWD/.venv/bin/python" +else + PY="$(command -v python3)" || { echo "no python3 on PATH"; exit 1; } +fi +ROOT="$PWD" + +mkdir -p gate/logs +FAILED=() + +run() { # run + local name="$1" dir="$2"; shift 2 + printf '\n=== %s ===\n' "$name" + if (cd "$dir" && "$PY" "$@" 2>&1) | tee "$ROOT/gate/logs/${name}.log"; then + : + else + FAILED+=("$name") + fi +} + +# 0. transcription audit — are the gate's premises still true of the code? +run audit_transcription gate audit_transcription.py + +# 1. oracle anchors — is the modelled FUNCTION the right one? +run oracle_anchors oracle test_oracle.py +run small_y_point oracle small_y_point.py + +# 2. real-witness anchor — are the modelled COLUMNS the right ones? +if [[ "${1:-}" != "--quick" ]]; then + printf '\n=== harness (cargo) ===\n' + if (cd harness && cargo build --release 2>&1) | tee gate/logs/harness_build.log; then + ./harness/target/release/ecsm-affine-harness > gate/logs/real_witnesses.jsonl + else + FAILED+=(harness_build) + fi +fi +run a6_real_witness gate a6_real_witness.py + +# 3. the lemmas +run a1_selector gate a1_selector.py +run a2_yr_lt_p gate a2_yr_lt_p.py +run a3_parity_binding gate a3_parity_binding.py +run a4_addressing gate a4_addressing.py + +printf '\n========================================\n' +if ((${#FAILED[@]})); then + printf 'GATE: FAILED — %s\n' "${FAILED[*]}" + exit 1 +fi +printf 'GATE: all stages green (logs in gate/logs/)\n'