diff --git a/AGENTS.md b/AGENTS.md
index 28d10576a..f6f35b8ff 100644
--- a/AGENTS.md
+++ b/AGENTS.md
@@ -5,7 +5,7 @@
 A RISC-V (rv64im) virtual machine and the SNARK that proves its execution. Proofs are not zero knowledge. Every rv64im instruction is proven, plus custom ones: the BLAKE2s compression (`blake2s rs1, rs2`) and the multiplication in the extension field `E = GF(2^192)` (`extmul`, `extmac`, `extmulk`, `extmack`, each `rd, rs1, rs2` with every register an address). A program is a guest's ELF file (`programs/<name>/guest`, Rust built for `riscv64im-unknown-none-elf`, loaded by `rv::Guest::from_elf`) or a text assembled by hand with `leanvm::asm`; a run is proven on an advice (a region of memory the prover fills), and its statement is the program's digest and the output (`a0..a3` at `exit`); there is no public input. One run is one proof: a run whose witness exceeds one commitment (`pcs::MAX_MU`) is refused up front with `ProveError::TooLong` (re-exported as `leanvm::ProveError::TooLong`), continuations being unimplemented.
 
 - `doc/leanvm/` is the LaTeX project describing the machine ISA and the snark that proves it. Its root is `doc/leanvm/main.tex`; build it with `cd doc/leanvm && latexmk -pdf main.tex`, which writes to the gitignored `doc/leanvm/.build/`. Sections live in `doc/leanvm/body/`, numbered `01`..`08` plus the lettered annexes `a` (ring switching), `b` (the PCS), `c` (Flock), `d` (novel basis and additive NTT), and `e` (recursion), and every symbol is defined once in `doc/leanvm/preamble/macros.tex`. If latexmk fails oddly (a bibtex error, or a missing `main.log`) right after inputs are renamed or `refs.bib` is edited, remove `doc/leanvm/.build` and rerun; it has not reproduced on unchanged inputs. **Drafting one section:** each section file carries a `% !TeX root` comment pointing at its generated driver in `doc/leanvm/drafts/`, so the LaTeX build key (`F5`, or the extension's `cmd+alt+b`) compiles only that section, numbered as in the full document and with cross-references and citations resolved against `.build/main.aux`; in `main.tex` the same key builds everything. Run `doc/leanvm/make-drafts.sh` after adding, renaming or renumbering a section.
-- The one hash function is BLAKE2s, in `primitives::hash`: scalar, streaming, and a lane-transposed batched form for the PCS Merkle tree. The VM's compression instruction is the generic gate-list circuit in `rv::semantics::hash` (`Class::Hash.circuit()`), proven like every other class; its witness is word arithmetic in `rv::semantics::hash` (exported as `rv::circuits::blake2s_witness`), pinned to the walk of the gate list by a test.
+- The one hash function is BLAKE2s, in `primitives::hash`: scalar, streaming, and a lane-transposed batched form for the PCS Merkle tree, with `hash::portable` the RFC's code alone, which the native verifier and the streaming `Hasher` (the program and tree digests) take. A transcript hashes by its `fiat_shamir::Hashing` backend, `Native` for the prover and `Portable` for the native verifier, the same bytes either way. The VM's compression instruction is the generic gate-list circuit in `rv::semantics::hash` (`Class::Hash.circuit()`), proven like every other class; its witness is word arithmetic in `rv::semantics::hash` (exported as `rv::circuits::blake2s_witness`), pinned to the walk of the gate list by a test.
 
 ## Layout
 
@@ -226,7 +226,7 @@ The opening's weight is never stored: the first WHIR pass fills it one chunk at
 
 No rayon. Every parallel site is "N independent items, each writing its own disjoint slice", so the pool is a claim counter, not a work-stealing deque: `NUM_THREADS-1` workers plus the dispatcher inline, and a dispatch allocates nothing (a reduction allocates its per-worker slots once per call, the slot type being the caller's). Primitives: `for_each{,_chunk}`, `chunks_mut{,2,_zip}`, `ChunkView`, `fill`, `map_collect`, `map_reduce`, `fold_reduce`, `map_reduce_with_state`, `find_first`, `SendPtr`.
 
-- **Nested dispatch panics**, because it would deadlock the dispatch lock.
+- **Nested dispatch panics**, because it would deadlock the dispatch lock. So does any dispatch while a `parallel::serial()` guard lives, whatever the pool's size: the native verifier holds one.
 - **Both core clusters share one queue** (P at `USER_INTERACTIVE`, E at `UTILITY`); guided self-scheduling means a slow core claims fewer batches. Do not add a second pool: that was `primitives::epool`, now deleted.
 - **The default holds back one performance worker when efficiency workers exist.**
 
@@ -238,6 +238,8 @@ Ring-switch claims' weights are built by `ring_switch::DeferredWeight::batch`, w
 
 The native verifier (`leanvm::cpu::Program::verify`) and the recursive verifier (`leanvm::rec::verifier`) run the same core over `fiat_shamir::arith`. `Arith` and `Verifier` execute natively over `VerifierState` or build rows over the circuit builder and the in-circuit transcript. The shared core covers GKR, bus decomposition, the table sumcheck, the program claim, flock reductions, and the opening over `pcs::verifier::OpeningVerifier`. `Verifier::scope` names a stage under which the rows report a failed check. `rec::verifier::tests` checks that the rows leave the native `DeferredClaims` value for value and that forged proofs fail at the expected stage.
 
+**The native verifier is portable and single-threaded, always.** It runs on the calling thread with no SIMD intrinsic, no inline assembly and no pool dispatch, so it computes the same way on every target; correctness and simplicity matter more than its speed. Its backend is `fiat_shamir::arith::Portable`: its arithmetic the `*_portable` field methods, its hashing (`fiat_shamir::Hashing`: the duplex and proof of work; `pcs::merkle::MerkleHashing`: Merkle openings) `primitives::hash::portable`. `VerifierState<'_, A>` computes and hashes by its backend; the public entry points fix it to `Portable`, and a prover replaying what it is handed (`Program::verify_recording` and `rec::proof::CircuitKey::verify`, over `pcs::verifier::Recording`) runs it on `Native`, which nothing trusts but the proof it feeds. Nothing the prover runs takes the portable code, apart from setup both sides compute once (session identifiers, the program and tree digests). A constant the verifier needs is a `const` computed by the portable products (`SkipDomain`, the zerocheck's medium challenges, the ring switch's roots of `x`), or is built by them (`pcs::ntt::NovelBasis`). Every public native entry point (`Program::verify`, `verify_core`, `check_deferred`, `Tree::verify`, `Tree::verify_claims`), a zero-knowledge leaf's (its recorder and `zk::KeyCommitment::verify_outer` included) and a tree's over zero-knowledge leaves alike, holds a `primitives::portable::Section`: a dispatch inside it panics always, and under `primitives`' `guard` feature, which the CLI's dev-dependencies turn on so that `cargo testall` arms it while no benchmark build pays for it, so does every SIMD or assembly kernel. So verifier code never calls a dispatching helper (`F192 * F192`, `mle_eval_par`, `multilinear::eq_table`, `hash::hash`): write it over `Arith` and `Hashing` and run it on `Portable`. The CLI's `verification_is_portable_and_single_threaded` checks the guard is armed, and `the_public_verifier_is_the_portable_one` that a `Native` replay is refused where the public verifier passes.
+
 Verification has two parts: `verify_core` checks the proof and returns claims on polynomials fixed by the program or the VM's circuits (`cpu::DeferredClaims`); `check_deferred` evaluates those claims. A recursive verifier carries them out of the proof instead of evaluating them. A caller of `verify_core` must never drop them. `check_deferred` refuses malformed claims with `CpuError::MalformedClaim`, never a panic. The recursion machine reads the very proof the native verifier accepted, with every Merkle opening that verifier authenticated (`rec::transcript::ProofSource::Proof(proof, openings)`): the prover verifies a leaf with `cpu::Program::verify_recording` and a child with `rec::proof::CircuitKey::verify`, both over `pcs::verifier::Recording`, so each hint is decoded and hashed once, natively, and the rows take its full paths (`pcs::merkle::Openings`, flat buffers) as free wires.
 
 Query positions are stratified (`pcs::whir::Stratum::batch`, Annex B's `def:strata`): each binary digit of the query count is a group whose `j`-th query has its top bits fixed to `j`. This keeps the i.i.d. query bound and lets the rows hash the top subtree once and each query's path only below it (`rec::verifier::Rows::authenticate`). Native and recursive verification share the WHIR configuration and its integer level ladder, so no floating point reaches a proof. The floating-point soundness derivation is test-only (`pcs::whir::config::tests`): `the_table_is_the_derivation` pins `WHIR_QUERIES` to it. Changing a constant the derivation reads (the security target, a folding factor, the grinding bits, the size window) fails that test, whose message holds the replacement rows for the Rust table. Moving the size window also changes the table's type: give each rate that many rows first (`&[]` will do) so that `pcs` compiles.
diff --git a/bins/leanvm/Cargo.toml b/bins/leanvm/Cargo.toml
index 655f33b21..b4fe6ddb1 100644
--- a/bins/leanvm/Cargo.toml
+++ b/bins/leanvm/Cargo.toml
@@ -37,3 +37,7 @@ tracing.workspace = true
 clap = { version = "4", features = ["derive"] }
 # The pinned cases' benchmarks, merged with this process's.
 serde_json = "1"
+
+[dev-dependencies]
+# Arms the portable verifier's guard in every workspace test build (`primitives::portable`), and in no benchmark's.
+primitives = { workspace = true, features = ["guard"] }
diff --git a/bins/leanvm/src/workload.rs b/bins/leanvm/src/workload.rs
index 7279d078f..444a08523 100644
--- a/bins/leanvm/src/workload.rs
+++ b/bins/leanvm/src/workload.rs
@@ -236,7 +236,9 @@ impl Workload {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use leanvm::Rate;
+    use leanvm::aggregate::{Capacity, ClaimGroup, ClaimLeaf, ClaimSet, ClaimShape, Leaf, LeafShape, Tree, TreeShape};
+    use leanvm::asm::Ld;
+    use leanvm::{Proof, Randomness, Rate};
 
     #[test]
     fn the_workloads_prove() {
@@ -263,4 +265,120 @@ mod tests {
             assert_eq!(stats.proven_rows, exec.proven_rows, "{}", workload.title);
         }
     }
+
+    /// Verification is portable and single-threaded: every native verifier holds a `primitives::portable::Section`, in
+    /// which this crate's tests (the `guard` feature) make a pool dispatch and every SIMD or assembly kernel panic.
+    /// A verifier that reached either fails here, and so does a guard that stopped refusing them.
+    #[test]
+    fn verification_is_portable_and_single_threaded() {
+        const { assert!(primitives::portable::GUARDED, "the CLI's tests arm the guard") };
+        let refused = |f: fn()| {
+            std::panic::catch_unwind(|| {
+                let _portable = primitives::portable::enter();
+                f();
+            })
+            .is_err()
+        };
+        assert!(refused(|| parallel::for_each(1, |_| {})));
+        #[cfg(any(
+            all(target_arch = "x86_64", target_feature = "pclmulqdq"),
+            all(target_arch = "aarch64", target_feature = "aes")
+        ))]
+        assert!(refused(|| {
+            let y = std::hint::black_box(primitives::field::F192::Y);
+            std::hint::black_box(y * y);
+        }));
+        #[cfg(target_arch = "x86_64")]
+        assert!(refused(|| _ = std::hint::black_box(hash(b"leanvm"))));
+
+        // A leaf proof, a tampered copy of it, a two-leaf tree over it, the same over a zero-knowledge leaf, and a claim-set
+        // root, each verified in the guard.
+        let leaf = Workload::fibonacci(1_000);
+        let prover = Prover::new(Rate::MIN);
+        let proved = leaf.prove(&prover);
+        leaf.program
+            .verify(proved.output, &proved.proof)
+            .expect("an honest proof");
+        let mut bytes = proved.proof.to_bytes();
+        let middle = bytes.len() / 2;
+        bytes[middle] ^= 1;
+        if let Ok(tampered) = Proof::from_bytes(&bytes) {
+            assert!(leaf.program.verify(proved.output, &tampered).is_err());
+        }
+        let shape = TreeShape {
+            leaf: LeafShape::measured(&leaf.measure(), Rate::MIN),
+            arity_0: 2,
+            arity: 2,
+            rate: Rate::MIN,
+            claims: None,
+        };
+        let tree = Tree::new(&leaf.program, shape).expect("a tree");
+        let root = tree
+            .prove(&[Leaf::new(&proved.proof, proved.output); 2])
+            .expect("honest leaves");
+        tree.verify(&root, &[proved.output; 2]).expect("the root");
+        assert!(tree.verify(&root, &[proved.output, Output::new([1, 2, 3, 4])]).is_err());
+
+        // A zero-knowledge leaf, its outer proof included, and a tree over two of them.
+        let hidden = leaf.prove(&prover.zero_knowledge(Randomness::Fixed([3; 32])));
+        leaf.program
+            .verify(hidden.output, &hidden.proof)
+            .expect("an honest zero-knowledge proof");
+        let mut bytes = hidden.proof.to_bytes();
+        let middle = bytes.len() / 2;
+        bytes[middle] ^= 1;
+        if let Ok(tampered) = Proof::from_bytes(&bytes) {
+            assert!(leaf.program.verify(hidden.output, &tampered).is_err());
+        }
+        let shape = TreeShape {
+            leaf: LeafShape::of(&hidden.proof).expect("a canonical announcement"),
+            arity_0: 2,
+            arity: 2,
+            rate: Rate::MIN,
+            claims: None,
+        };
+        let tree = Tree::new(&leaf.program, shape).expect("a tree");
+        let root = tree
+            .prove(&[Leaf::new(&hidden.proof, hidden.output); 2])
+            .expect("honest zero-knowledge leaves");
+        tree.verify(&root, &[hidden.output; 2]).expect("the root");
+
+        // A leaf that outputs its advice, the hash of its set's digest, after a loop that reads every framework block.
+        let text = Asm::new()
+            .li(Reg::T0, Region::ADVICE.base())
+            .load(Ld, Reg::A0, 0, Reg::T0)
+            .load(Ld, Reg::A1, 8, Reg::T0)
+            .load(Ld, Reg::A2, 16, Reg::T0)
+            .load(Ld, Reg::A3, 24, Reg::T0)
+            .li(Reg::T1, 9)
+            .label("loop")
+            .i(Addi, Reg::T1, Reg::T1, -1)
+            .branch(Bne, Reg::T1, Reg::ZERO, "loop")
+            .exit()
+            .finish();
+        let program = Program::new(&text, Region::TEXT.base(), vec![3, 5], 2, 2).expect("a valid program");
+        let set = ClaimSet {
+            groups: vec![ClaimGroup {
+                label: [1, 9, 0, 0, 0, 1],
+                members: vec![[1, 8, 1 << 9, 0x5eed ^ 1]],
+            }],
+        };
+        let words: Vec<u8> = set.digest().iter().flat_map(|w| w.to_le_bytes()).collect();
+        let run = (prover.prove(&program, &digest_words(&hash(&words)))).expect("the run halts");
+        let shape = TreeShape {
+            leaf: LeafShape::of(&run.proof).expect("a canonical announcement"),
+            arity_0: 1,
+            arity: 3,
+            rate: Rate::MIN,
+            claims: Some(ClaimShape {
+                capacity: Capacity { claims: 12, groups: 4 },
+                small: None,
+            }),
+        };
+        let tree = Tree::new(&program, shape).expect("a tree");
+        let first = (tree.aggregate_leaves(&[ClaimLeaf::new(Leaf::new(&run.proof, run.output), &set)], None))
+            .expect("an honest leaf");
+        tree.verify_claims(&first.proof, &first.claims).expect("the root");
+        assert!(tree.verify_claims(&first.proof, &ClaimSet { groups: vec![] }).is_err());
+    }
 }
diff --git a/crates/fiat_shamir/src/arith.rs b/crates/fiat_shamir/src/arith.rs
index 3c4852cfb..03ca755d3 100644
--- a/crates/fiat_shamir/src/arith.rs
+++ b/crates/fiat_shamir/src/arith.rs
@@ -5,6 +5,7 @@
 //! - Natively an element is an `F192`, a read comes off the proof, and a failed equality is an error.
 //! - In rows an element is a wire, a read is a free wire bound by a hash row, and an equality joins two wires.
 
+use crate::Hashing;
 use crate::verifier::{TranscriptError, VerifierState};
 use primitives::field::{F64, F192};
 use primitives::multilinear::mle_eval_par;
@@ -166,6 +167,13 @@ pub trait Arith {
         out
     }
 
+    /// `sum_i a_i b_i`, of two vectors of one length.
+    fn dot(&mut self, a: &[Self::E], b: &[Self::E]) -> Self::E {
+        assert_eq!(a.len(), b.len(), "two vectors of one length");
+        let zero = self.zero();
+        (a.iter().zip(b)).fold(zero, |acc, (&x, &y)| self.mul_add(x, y, acc))
+    }
+
     /// The integer index column `base ^ (z << shift)` at `point`: `base + sum_i point_i 2^(i + shift)`.
     fn int_index(&mut self, base: F64, shift: u32, point: &[Self::E]) -> Self::E {
         let base = self.constant(F192::from(base));
@@ -348,40 +356,141 @@ impl Arith for Native {
     }
 }
 
-/// The native verifier computes in the clear, as the prover does.
-impl Arith for VerifierState<'_> {
+/// Plain `F192` arithmetic with no SIMD intrinsic, no assembly and no pool dispatch: the native verifier's.
+///
+/// The verifier's transcript computes and hashes through it, and so does every check the native verifier makes off the
+/// transcript. See `primitives::portable`.
+#[derive(Clone, Copy, Debug, Default)]
+pub struct Portable;
+
+impl Arith for Portable {
+    type E = F192;
+
+    fn constant(&mut self, c: F192) -> F192 {
+        c
+    }
+
+    fn mul_add(&mut self, a: F192, b: F192, d: F192) -> F192 {
+        a.mul_portable(b) + d
+    }
+
+    fn add(&mut self, a: F192, d: F192) -> F192 {
+        a + d
+    }
+
+    /// A constant of `K`, as most are, takes the cheaper product by a word.
+    fn mul_const_add(&mut self, a: F192, c: F192, d: F192) -> F192 {
+        if c.c1 == 0 && c.c2 == 0 {
+            a.mul_base_portable(F64(c.c0)) + d
+        } else {
+            a.mul_portable(c) + d
+        }
+    }
+
+    fn inv(&mut self, a: F192) -> F192 {
+        a.inv_portable()
+    }
+
+    fn frobenius2(&mut self, a: F192) -> F192 {
+        a.frobenius().frobenius()
+    }
+
+    fn square(&mut self, a: F192) -> F192 {
+        a.square_portable()
+    }
+
+    /// One product an entry: a vertex's high child is it times `r`, and its low child `v (1 + r) = v + v r` reuses the
+    /// product.
+    fn eq_table_prefix(&mut self, point: &[F192], len: usize) -> Vec<F192> {
+        assert!(len <= 1 << point.len(), "a prefix of the cube");
+        let mut table = Vec::with_capacity(len);
+        table.push(F192::ONE);
+        for (i, &r) in point.iter().enumerate() {
+            let (old, need) = (table.len(), len.min(2 << i));
+            for j in 0..old {
+                let high = table[j].mul_portable(r);
+                table[j] += high;
+                if old + j < need {
+                    table.push(high);
+                }
+            }
+        }
+        table.truncate(len);
+        table
+    }
+
+    /// By the words' bits: `sum_x eq(point, x) v_x = sum_k x^k sum_x eq(point, x) bit_k(v_x)`.
+    ///
+    /// A row of `2^low` words sums its low eq weights into one slice per bit, by additions alone; a nonzero slice then
+    /// takes its row's high eq weight, and each bit's sum its power of `x`. `low` balances the low table's `2^low`
+    /// products against the rows' up to `64` each.
+    fn public_mle(&mut self, values: &[F64], point: &[F192]) -> F192 {
+        assert_eq!(values.len(), 1 << point.len(), "a column has a word per vertex");
+        let low = (point.len() + F64::DEGREE.ilog2() as usize).div_ceil(2);
+        let (low, high) = point.split_at(low.min(point.len()));
+        let (eq_low, eq_high) = (self.eq_table(low), self.eq_table(high));
+        let mut bits = [F192::ZERO; F64::DEGREE];
+        for (row, &weight) in values.chunks_exact(eq_low.len()).zip(&eq_high) {
+            let mut slices = [F192::ZERO; F64::DEGREE];
+            for (&e, v) in eq_low.iter().zip(row) {
+                let mut word = v.0;
+                while word != 0 {
+                    slices[word.trailing_zeros() as usize] += e;
+                    word &= word - 1;
+                }
+            }
+            for (bit, slice) in bits.iter_mut().zip(slices) {
+                if !slice.is_zero() {
+                    *bit += weight.mul_portable(slice);
+                }
+            }
+        }
+        (bits.iter().enumerate()).fold(F192::ZERO, |acc, (k, b)| acc + b.mul_base_portable(F64(1 << k)))
+    }
+}
+
+/// The transcript computes with its backend: [`Portable`] for the native verifier, [`Native`] for a prover's replay.
+impl<A: Arith<E = F192> + Hashing> Arith for VerifierState<'_, A> {
     type E = F192;
 
     fn constant(&mut self, c: F192) -> F192 {
-        Native.constant(c)
+        c
     }
 
     fn mul_add(&mut self, a: F192, b: F192, d: F192) -> F192 {
-        Native.mul_add(a, b, d)
+        self.arith.mul_add(a, b, d)
     }
 
     fn add(&mut self, a: F192, d: F192) -> F192 {
-        Native.add(a, d)
+        a + d
     }
 
     fn mul_const_add(&mut self, a: F192, c: F192, d: F192) -> F192 {
-        Native.mul_const_add(a, c, d)
+        self.arith.mul_const_add(a, c, d)
     }
 
     fn inv(&mut self, a: F192) -> F192 {
-        Native.inv(a)
+        self.arith.inv(a)
     }
 
     fn frobenius2(&mut self, a: F192) -> F192 {
-        Native.frobenius2(a)
+        self.arith.frobenius2(a)
+    }
+
+    fn square(&mut self, a: F192) -> F192 {
+        self.arith.square(a)
+    }
+
+    fn eq_table_prefix(&mut self, point: &[F192], len: usize) -> Vec<F192> {
+        self.arith.eq_table_prefix(point, len)
     }
 
     fn public_mle(&mut self, values: &[F64], point: &[F192]) -> F192 {
-        Native.public_mle(values, point)
+        self.arith.public_mle(values, point)
     }
 }
 
-impl Verifier for VerifierState<'_> {
+impl<A: Arith<E = F192> + Hashing> Verifier for VerifierState<'_, A> {
     fn prover_message(&mut self) -> Result<F192, TranscriptError> {
         Self::prover_message(self)
     }
@@ -410,3 +519,55 @@ impl Verifier for VerifierState<'_> {
         Self::is_hidden(self)
     }
 }
+
+#[cfg(test)]
+mod tests {
+    use super::*;
+    use primitives::multilinear::mle_eval;
+
+    #[test]
+    fn the_portable_public_mle_is_the_dispatched_one() {
+        // Below, at and past one row of the low eq table, words dense and sparse.
+        let mut state = 0x9e37_79b9_7f4a_7c15_u64;
+        let mut next = || {
+            state = state
+                .wrapping_mul(0x5851_f42d_4c95_7f2d)
+                .wrapping_add(0x1405_7b7e_f767_814f);
+            state
+        };
+        for n in [0, 1, 2, 3, 7, 8, 10, 12, 13, 15, 17] {
+            let point: Vec<F192> = (0..n).map(|_| F192::new(next(), next(), next())).collect();
+            for sparse in [false, true] {
+                let values: Vec<F64> = (0..1 << n)
+                    .map(|_| F64(if sparse { next() & 0x8001 } else { next() }))
+                    .collect();
+                assert_eq!(
+                    Portable.public_mle(&values, &point),
+                    mle_eval(&values, &point),
+                    "{n} variables"
+                );
+            }
+        }
+    }
+
+    #[test]
+    fn the_portable_eq_table_is_the_default_one() {
+        let mut state = 0x2545_f491_4f6c_dd1d_u64;
+        let mut next = || {
+            state ^= state << 13;
+            state ^= state >> 7;
+            state ^= state << 17;
+            state
+        };
+        for n in 0..8 {
+            let point: Vec<F192> = (0..n).map(|_| F192::new(next(), next(), next())).collect();
+            for len in 0..=1 << n {
+                assert_eq!(
+                    Portable.eq_table_prefix(&point, len),
+                    Native.eq_table_prefix(&point, len),
+                    "{n} variables, {len} vertices"
+                );
+            }
+        }
+    }
+}
diff --git a/crates/fiat_shamir/src/duplex.rs b/crates/fiat_shamir/src/duplex.rs
index 9193c71c3..475ffc2ce 100644
--- a/crates/fiat_shamir/src/duplex.rs
+++ b/crates/fiat_shamir/src/duplex.rs
@@ -34,9 +34,11 @@
 //!
 //! The loss is `q^2 / 2^257` for `q` compressions.
 
-use crate::SessionId;
+use crate::arith::Native;
 use crate::codec::{Encoding, FromUniform};
-use primitives::hash::{PARAM_IV, compress};
+use crate::{Hashing, SessionId};
+use primitives::hash::PARAM_IV;
+use std::marker::PhantomData;
 
 /// The role of a node, in the top byte of its compression counter.
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
@@ -89,8 +91,10 @@ impl Role {
 /// It holds at most one pending input block and one output block, and never allocates.
 ///
 /// It streams: splitting an absorb or a squeeze into several calls never changes the bytes squeezed.
+///
+/// `H` compresses: the prover's [`Native`] kernels, or the native verifier's [`crate::arith::Portable`] code.
 #[derive(Clone, Debug)]
-pub struct Blake2sDuplex {
+pub struct Blake2sDuplex<H = Native> {
     /// The chaining value: everything absorbed so far.
     cv: [u32; 8],
     /// Input not yet compressed, at most one block.
@@ -105,12 +109,16 @@ pub struct Blake2sDuplex {
     squeezed: u64,
     /// The output block the next squeezed bytes come from.
     output: [u8; 32],
+    /// How it compresses.
+    hashing: PhantomData<H>,
 }
 
 impl Blake2sDuplex {
-    /// Bytes one squeeze run may consume: a 49-bit count fits the framing word.
+    /// Bytes one squeeze run may consume, whatever compresses: a 49-bit count fits the framing word.
     pub const MAX_SQUEEZE: u64 = (1 << 49) - 1;
+}
 
+impl<H: Hashing> Blake2sDuplex<H> {
     /// The sponge a transcript starts from: seeded with the session, then the instance absorbed.
     ///
     /// The instance is public: both sides absorb it, and the proof does not carry it.
@@ -140,7 +148,7 @@ impl Blake2sDuplex {
         // Zero the unused tail: the framing word's length tells padding from data.
         self.pending[self.n_pending..].fill(0);
         let counter = Role::absorb(self.first, last).counter(self.n_pending, self.previous);
-        self.cv = node(self.cv, &self.pending, counter);
+        self.cv = node::<H>(self.cv, &self.pending, counter);
 
         // The run continues past a full block, and only its first block carries the previous count.
         self.n_pending = 0;
@@ -149,7 +157,7 @@ impl Blake2sDuplex {
     }
 }
 
-impl Blake2sDuplex {
+impl<H: Hashing> Blake2sDuplex<H> {
     /// The sponge started from a 32-byte initialization vector, such as a session identifier.
     #[must_use]
     pub fn new(iv: [u8; 32]) -> Self {
@@ -157,13 +165,14 @@ impl Blake2sDuplex {
         let mut block = [0; 64];
         block[..32].copy_from_slice(&iv);
         Self {
-            cv: node(PARAM_IV, &block, Role::Seed.counter(0, 0)),
+            cv: node::<H>(PARAM_IV, &block, Role::Seed.counter(0, 0)),
             pending: [0; 64],
             n_pending: 0,
             first: true,
             previous: 0,
             squeezed: 0,
             output: [0; 32],
+            hashing: PhantomData,
         }
     }
 
@@ -203,7 +212,10 @@ impl Blake2sDuplex {
             return;
         }
         let len = output.len() as u64;
-        assert!(len <= Self::MAX_SQUEEZE - self.squeezed, "squeeze run too long");
+        assert!(
+            len <= Blake2sDuplex::MAX_SQUEEZE - self.squeezed,
+            "squeeze run too long"
+        );
 
         // Close the absorb run: its pending block is its last.
         if self.n_pending != 0 {
@@ -218,7 +230,7 @@ impl Blake2sDuplex {
             if offset == 0 {
                 let mut block = [0; 64];
                 block[..8].copy_from_slice(&(self.squeezed / 32).to_le_bytes());
-                self.output = state_bytes(node(self.cv, &block, Role::Output.counter(0, 0)));
+                self.output = state_bytes(node::<H>(self.cv, &block, Role::Output.counter(0, 0)));
             }
 
             // Hand out the unused part of the block, keeping the rest for the next squeeze.
@@ -231,10 +243,10 @@ impl Blake2sDuplex {
 }
 
 /// One node: the final-flagged compression of `cv` and `block` at `counter`.
-fn node(mut cv: [u32; 8], block: &[u8; 64], counter: u64) -> [u32; 8] {
+fn node<H: Hashing>(mut cv: [u32; 8], block: &[u8; 64], counter: u64) -> [u32; 8] {
     let (chunks, _) = block.as_chunks::<4>();
     let words = std::array::from_fn(|i| u32::from_le_bytes(chunks[i]));
-    compress(&mut cv, &words, counter, true);
+    H::compress(&mut cv, &words, counter, true);
     cv
 }
 
@@ -250,6 +262,7 @@ fn state_bytes(cv: [u32; 8]) -> [u8; 32] {
 #[cfg(test)]
 mod tests {
     use super::*;
+    use crate::arith::Portable;
     use proptest::prelude::*;
 
     /// One run of a transcript: bytes absorbed, or a count of bytes squeezed.
@@ -259,13 +272,14 @@ mod tests {
         Squeeze(usize),
     }
 
-    // The mode written out node by node, with no buffering: what the streaming sponge must equal.
+    // The mode written out node by node, with no buffering, on the portable compression: what the streaming sponge on
+    // the native one must equal.
     //
     // Runs alternate, absorb runs non-empty, squeeze runs positive.
     fn reference(iv: [u8; 32], runs: &[Run]) -> Vec<u8> {
         let mut seed = [0; 64];
         seed[..32].copy_from_slice(&iv);
-        let mut cv = node(PARAM_IV, &seed, Role::Seed.counter(0, 0));
+        let mut cv = node::<Portable>(PARAM_IV, &seed, Role::Seed.counter(0, 0));
         let mut previous = 0;
         let mut out = Vec::new();
         for run in runs {
@@ -278,7 +292,7 @@ mod tests {
                         block[..chunk.len()].copy_from_slice(chunk);
                         let first = i == 0;
                         let role = Role::absorb(first, i + 1 == blocks.len());
-                        cv = node(cv, &block, role.counter(chunk.len(), if first { previous } else { 0 }));
+                        cv = node::<Portable>(cv, &block, role.counter(chunk.len(), if first { previous } else { 0 }));
                     }
                 }
                 Run::Squeeze(n) => {
@@ -287,7 +301,7 @@ mod tests {
                     for j in 0..n.div_ceil(32) as u64 {
                         let mut block = [0; 64];
                         block[..8].copy_from_slice(&j.to_le_bytes());
-                        stream.extend(state_bytes(node(cv, &block, Role::Output.counter(0, 0))));
+                        stream.extend(state_bytes(node::<Portable>(cv, &block, Role::Output.counter(0, 0))));
                     }
                     out.extend_from_slice(&stream[..*n]);
                     previous = *n as u64;
@@ -312,7 +326,7 @@ mod tests {
             //
             // Splitting and empty calls must change nothing.
             let iv = [9; 32];
-            let mut sponge = Blake2sDuplex::new(iv);
+            let mut sponge: Blake2sDuplex = Blake2sDuplex::new(iv);
             let mut out = Vec::new();
             for run in &runs {
                 match run {
@@ -340,7 +354,7 @@ mod tests {
     fn padding_and_squeeze_counts_are_bound() {
         // The framing tells apart transcripts a plain concatenation would merge.
         let challenge = |squeezed: usize, absorbed: &[u8]| {
-            let mut sponge = Blake2sDuplex::new([0; 32]);
+            let mut sponge: Blake2sDuplex = Blake2sDuplex::new([0; 32]);
             sponge.absorb(b"x");
             sponge.squeeze(&mut vec![0; squeezed]);
             sponge.absorb(absorbed);
@@ -368,7 +382,7 @@ mod tests {
     #[test]
     fn a_squeeze_run_past_the_limit_is_refused_before_any_change() {
         // Fixture: a sponge whose run already consumed all but one byte of the limit.
-        let mut sponge = Blake2sDuplex::new([0; 32]);
+        let mut sponge: Blake2sDuplex = Blake2sDuplex::new([0; 32]);
         sponge.squeeze(&mut [0; 1]);
         sponge.squeezed = Blake2sDuplex::MAX_SQUEEZE - 1;
         let before = sponge.clone();
@@ -384,18 +398,19 @@ mod tests {
     fn a_known_answer_pins_the_mode() {
         // Absorb 0..131, squeeze 40, absorb "ab", squeeze 8, from the iv 0..32.
         //
-        // Any change to the framing, the padding or the byte order moves these bytes.
-        let mut sponge = Blake2sDuplex::new(std::array::from_fn(|i| i as u8));
-        sponge.absorb(&(0..131).collect::<Vec<u8>>());
-        let mut first = [0; 40];
-        sponge.squeeze(&mut first);
-        sponge.absorb(b"ab");
-        let mut second = [0; 8];
-        sponge.squeeze(&mut second);
-        let hex: String = first.iter().chain(&second).map(|b| format!("{b:02x}")).collect();
-        assert_eq!(
-            hex,
-            "72d518bf9786c4060f03f3cb68a3ffc32dda36374ed40d4bb910659749d061d422f71eefc6691565f8a51fa46683db43"
-        );
+        // Any change to the framing, the padding or the byte order moves these bytes, on either compression.
+        fn run<H: Hashing>() -> String {
+            let mut sponge = Blake2sDuplex::<H>::new(std::array::from_fn(|i| i as u8));
+            sponge.absorb(&(0..131).collect::<Vec<u8>>());
+            let mut first = [0; 40];
+            sponge.squeeze(&mut first);
+            sponge.absorb(b"ab");
+            let mut second = [0; 8];
+            sponge.squeeze(&mut second);
+            first.iter().chain(&second).map(|b| format!("{b:02x}")).collect()
+        }
+        let want = "72d518bf9786c4060f03f3cb68a3ffc32dda36374ed40d4bb910659749d061d422f71eefc6691565f8a51fa46683db43";
+        assert_eq!(run::<Native>(), want);
+        assert_eq!(run::<Portable>(), want);
     }
 }
diff --git a/crates/fiat_shamir/src/lib.rs b/crates/fiat_shamir/src/lib.rs
index 5f03b45b1..d4f42209d 100644
--- a/crates/fiat_shamir/src/lib.rs
+++ b/crates/fiat_shamir/src/lib.rs
@@ -15,6 +15,9 @@
 //! - The proof's messages are exactly the bytes the sponge absorbed.
 //!
 //! The sponge is a duplex built from the BLAKE2s compression function, the one hash the VM proves.
+//!
+//! A transcript hashes by its [`Hashing`]: the prover's the build's fastest kernels ([`Native`]), the native
+//! verifier's the portable code ([`Portable`]). Both give the same bytes.
 
 pub mod arith;
 mod codec;
@@ -24,6 +27,9 @@ mod proof;
 mod prover;
 mod verifier;
 
+use arith::{Native, Portable};
+use primitives::hash::portable;
+
 pub use codec::{Encoding, FromNarg, FromUniform, LengthPrefixed};
 pub use duplex::{Blake2sDuplex, Role};
 pub use pow::ProofOfWork;
@@ -39,6 +45,37 @@ pub trait Challenger {
     fn verifier_message<T: FromUniform>(&mut self) -> T;
 }
 
+/// How a transcript hashes: its duplex's compressions and its proof of work's trials.
+pub trait Hashing: Copy {
+    /// The BLAKE2s compression of `m` into `h` at byte counter `t`, final if `last`.
+    fn compress(h: &mut [u32; 8], m: &[u32; 16], t: u64, last: bool);
+
+    /// One-shot BLAKE2s-256.
+    fn hash(data: &[u8]) -> [u8; 32];
+}
+
+/// The prover's: the build's kernels.
+impl Hashing for Native {
+    fn compress(h: &mut [u32; 8], m: &[u32; 16], t: u64, last: bool) {
+        primitives::hash::compress(h, m, t, last);
+    }
+
+    fn hash(data: &[u8]) -> [u8; 32] {
+        primitives::hash::hash(data)
+    }
+}
+
+/// The native verifier's: the portable code.
+impl Hashing for Portable {
+    fn compress(h: &mut [u32; 8], m: &[u32; 16], t: u64, last: bool) {
+        portable::compress(h, m, t, last);
+    }
+
+    fn hash(data: &[u8]) -> [u8; 32] {
+        portable::hash(data)
+    }
+}
+
 /// The 32 bytes that start a transcript.
 ///
 /// It identifies the protocol, the relation, and the context, as `draft-irtf-cfrg-fiat-shamir` requires.
@@ -58,6 +95,8 @@ const DERIVATION_IV: [u8; 32] = *b"irtf-cfrg-fiat-shamir/session-id";
 impl SessionId {
     /// The identifier of a tag.
     ///
+    /// Both sides derive it, the verifier included, so it compresses by the portable code.
+    ///
     /// The tag names the protocol, its version, its hash and codecs, and the relation.
     ///
     /// ```text
@@ -67,7 +106,7 @@ impl SessionId {
     /// ```
     #[must_use]
     pub fn new(tag: &[u8]) -> Self {
-        let mut sponge = Blake2sDuplex::new(DERIVATION_IV);
+        let mut sponge = Blake2sDuplex::<Portable>::new(DERIVATION_IV);
         sponge.absorb(tag);
         let mut id = [0; 32];
         sponge.squeeze(&mut id);
diff --git a/crates/fiat_shamir/src/pow.rs b/crates/fiat_shamir/src/pow.rs
index 16c81ba4b..0576efd7f 100644
--- a/crates/fiat_shamir/src/pow.rs
+++ b/crates/fiat_shamir/src/pow.rs
@@ -12,7 +12,9 @@
 //!
 //! So re-rolling that challenge costs `2^bits` hashes on average.
 
-use primitives::hash::{BATCH, hash, hash_many};
+use crate::Hashing;
+use crate::arith::Native;
+use primitives::hash::{BATCH, hash_many};
 use std::sync::atomic::{AtomicU64, Ordering};
 
 /// A proof-of-work difficulty: the number of leading zero bits a nonce's hash must have.
@@ -29,8 +31,8 @@ pub struct ProofOfWork {
 /// ```
 ///
 /// Nonce and tag are little-endian.
-fn trial(challenge: &[u8; 32], nonce: u64) -> [u8; 32] {
-    hash(&block(challenge, nonce))
+fn trial<H: Hashing>(challenge: &[u8; 32], nonce: u64) -> [u8; 32] {
+    H::hash(&block(challenge, nonce))
 }
 
 /// The 64-byte block a nonce is tried in.
@@ -68,10 +70,10 @@ impl ProofOfWork {
         self.bits
     }
 
-    /// Whether `nonce` is this much work on `challenge`.
+    /// Whether `nonce` is this much work on `challenge`, hashed by `H`.
     #[must_use]
-    pub fn verify(self, challenge: &[u8; 32], nonce: u64) -> bool {
-        self.accepts(&trial(challenge, nonce))
+    pub fn verify<H: Hashing>(self, challenge: &[u8; 32], nonce: u64) -> bool {
+        self.accepts(&trial::<H>(challenge, nonce))
     }
 
     /// Whether a trial's digest is this much work: its first eight bytes, little-endian, have their top bits zero.
@@ -95,7 +97,7 @@ impl ProofOfWork {
         const PARALLEL_MIN_TRIALS: u64 = 1 << 13;
         if (1u64 << bits) < PARALLEL_MIN_TRIALS {
             return (0..=u64::MAX)
-                .find(|&nonce| self.verify(challenge, nonce))
+                .find(|&nonce| self.verify::<Native>(challenge, nonce))
                 .expect("some nonce works");
         }
 
@@ -137,18 +139,22 @@ impl ProofOfWork {
 #[cfg(test)]
 mod tests {
     use super::*;
+    use crate::arith::Portable;
 
     #[test]
     fn grinding_finds_the_smallest_nonce() {
-        // For each difficulty, every nonce below the one found fails, and that one passes.
+        // For each difficulty, every nonce below the one found fails, and that one passes, on either backend.
         //
         // 14 bits crosses into the parallel search.
         let challenge = [7; 32];
         for bits in [1, 5, 9, 14] {
             let pow = ProofOfWork::new(bits);
             let nonce = pow.grind(&challenge);
-            assert!(pow.verify(&challenge, nonce));
-            assert!((0..nonce).all(|n| !pow.verify(&challenge, n)), "{bits} bits");
+            assert!(pow.verify::<Native>(&challenge, nonce) && pow.verify::<Portable>(&challenge, nonce));
+            assert!(
+                (0..nonce).all(|n| !pow.verify::<Portable>(&challenge, n)),
+                "{bits} bits"
+            );
         }
     }
 
@@ -157,7 +163,7 @@ mod tests {
         // No bit is required, so every nonce is work, the smallest being zero.
         let free = ProofOfWork::new(0);
         assert_eq!(free.grind(&[1; 32]), 0);
-        assert!(free.verify(&[1; 32], u64::MAX));
+        assert!(free.verify::<Portable>(&[1; 32], u64::MAX));
     }
 
     #[test]
diff --git a/crates/fiat_shamir/src/verifier.rs b/crates/fiat_shamir/src/verifier.rs
index 65af00662..c892cc299 100644
--- a/crates/fiat_shamir/src/verifier.rs
+++ b/crates/fiat_shamir/src/verifier.rs
@@ -1,10 +1,11 @@
 //! The verifier's side of a transcript, and why it refuses one.
 
+use crate::arith::{Native, Portable};
 use crate::codec::{Encoding, FromNarg, FromUniform};
 use crate::duplex::Blake2sDuplex;
 use crate::pow::ProofOfWork;
 use crate::proof::{Hints, ProofTranscript};
-use crate::{Challenger, SessionId};
+use crate::{Challenger, Hashing, SessionId};
 use thiserror::Error;
 
 /// Why a proof's transcript cannot be read.
@@ -51,9 +52,12 @@ pub enum TranscriptError {
 /// It mirrors the prover call for call.
 ///
 /// A failed read poisons it: every later read returns the same error.
-pub struct VerifierState<'a> {
+///
+/// Its backend `A` computes, hashes and checks proof of work: the native verifier's [`Portable`], or [`Native`] where
+/// a prover replays a proof it is handed, which feeds its own proof and nobody's trust.
+pub struct VerifierState<'a, A = Portable> {
     /// The duplex sponge.
-    sponge: Blake2sDuplex,
+    sponge: Blake2sDuplex<A>,
     /// The messages not yet read.
     narg: &'a [u8],
     /// The hints not yet read.
@@ -66,10 +70,12 @@ pub struct VerifierState<'a> {
     poison: Option<TranscriptError>,
     /// Whether the messages read next were sent under one-time-pad keys.
     hidden: bool,
+    /// The arithmetic it computes with.
+    pub(crate) arith: A,
 }
 
 impl<'a> VerifierState<'a> {
-    /// A transcript for one session, its first message the instance, reading `proof`.
+    /// A transcript for one session, its first message the instance, reading `proof`, on the portable backend.
     ///
     /// Session and instance must be the prover's, or every challenge differs.
     ///
@@ -77,6 +83,24 @@ impl<'a> VerifierState<'a> {
     ///
     /// Panics on an instance of no bytes, which would bind no statement.
     pub fn new(session: &SessionId, instance: &impl Encoding, proof: &'a ProofTranscript) -> Self {
+        Self::with_backend(session, instance, proof)
+    }
+}
+
+impl<'a> VerifierState<'a, Native> {
+    /// [`VerifierState::new`] on the prover's kernels, for a prover replaying a proof it is handed.
+    ///
+    /// # Panics
+    ///
+    /// Panics on an instance of no bytes, which would bind no statement.
+    pub fn native(session: &SessionId, instance: &impl Encoding, proof: &'a ProofTranscript) -> Self {
+        Self::with_backend(session, instance, proof)
+    }
+}
+
+impl<'a, A: Hashing + Default> VerifierState<'a, A> {
+    /// A transcript on the backend `A`.
+    fn with_backend(session: &SessionId, instance: &impl Encoding, proof: &'a ProofTranscript) -> Self {
         Self {
             sponge: Blake2sDuplex::transcript(session, instance),
             narg: &proof.narg,
@@ -85,9 +109,12 @@ impl<'a> VerifierState<'a> {
             hints_read: 0,
             poison: None,
             hidden: false,
+            arith: A::default(),
         }
     }
+}
 
+impl<'a, A: Hashing> VerifierState<'a, A> {
     /// Record `result`'s error, if any, so that every later read fails with it.
     fn guard<T>(&mut self, result: Result<T, TranscriptError>) -> Result<T, TranscriptError> {
         if let Err(e) = result {
@@ -177,7 +204,7 @@ impl<'a> VerifierState<'a> {
         (0..n).map(|_| self.verifier_message()).collect()
     }
 
-    /// Check `bits` of proof of work: draw the challenge, read the nonce, test it.
+    /// Check `bits` of proof of work: draw the challenge, read the nonce, test it by the backend's hash.
     ///
     /// Zero bits is no step at all, as on the prover's side.
     ///
@@ -195,7 +222,7 @@ impl<'a> VerifierState<'a> {
         }
         let challenge: [u8; 32] = self.verifier_message();
         let nonce: u64 = self.prover_message()?;
-        let worked = pow.verify(&challenge, nonce);
+        let worked = pow.verify::<A>(&challenge, nonce);
         self.guard(worked.then_some(()).ok_or(TranscriptError::PowFailed { bits }))
     }
 
@@ -233,7 +260,7 @@ impl<'a> VerifierState<'a> {
     }
 }
 
-impl Challenger for VerifierState<'_> {
+impl<A: Hashing> Challenger for VerifierState<'_, A> {
     fn verifier_message<T: FromUniform>(&mut self) -> T {
         Self::verifier_message(self)
     }
diff --git a/crates/flock/src/circuit.rs b/crates/flock/src/circuit.rs
index 94289c956..ed4069868 100644
--- a/crates/flock/src/circuit.rs
+++ b/crates/flock/src/circuit.rs
@@ -607,10 +607,9 @@ impl LincheckCircuit for Circuit {
         m
     }
 
-    /// The form by one forward walk, in time linear in the circuit.
-    fn bilinear_form(&self, alpha: F192, u: &[F192], w: &[F192]) -> F192 {
-        let (ra, rb) = self.row_values(w);
-        (u.iter().zip(ra.iter().zip(&rb))).fold(F192::ZERO, |acc, (&u, (&a, &b))| acc + u * (a + alpha * b))
+    /// One forward walk.
+    fn matrix_rows(&self, w: &[F192]) -> (Vec<F192>, Vec<F192>) {
+        self.row_values(w)
     }
 }
 
diff --git a/crates/flock/src/lincheck.rs b/crates/flock/src/lincheck.rs
index 455aea4cb..525c378a9 100644
--- a/crates/flock/src/lincheck.rs
+++ b/crates/flock/src/lincheck.rs
@@ -94,8 +94,8 @@ pub trait LincheckCircuit: Sync {
     /// That closes the all-zero witness, and requires the wire to be one in every instance, padding included.
     fn const_pin_col(&self) -> usize;
 
-    /// The batched bilinear form `u^T A_0 w + alpha u^T B_0 w`.
-    fn bilinear_form(&self, alpha: F192, u: &[F192], w: &[F192]) -> F192;
+    /// The matrix-vector products `(A_0 w, B_0 w)`, by additions alone: the verifier's form takes them.
+    fn matrix_rows(&self, w: &[F192]) -> (Vec<F192>, Vec<F192>);
 }
 
 /// A claim point with a univariate-skip coordinate.
@@ -162,11 +162,11 @@ pub enum LincheckError {
 }
 
 /// `out[i_lo + i_hi lo.len()] = lo[i_lo] * hi[i_hi]`: `lo` varies fastest.
-pub(crate) fn outer_product(hi: &[F192], lo: &[F192]) -> Vec<F192> {
+pub(crate) fn outer_product<A: Arith>(a: &mut A, hi: &[A::E], lo: &[A::E]) -> Vec<A::E> {
     // Sized up front: a flattened iterator cannot report its length.
     let mut out = Vec::with_capacity(hi.len() * lo.len());
     for &h in hi {
-        out.extend(lo.iter().map(|&l| l * h));
+        out.extend(lo.iter().map(|&l| a.mul(l, h)));
     }
     out
 }
@@ -567,11 +567,25 @@ impl MatrixForm {
         SkipDomain::new(self.s_hat_v.len().ilog2() as usize)
     }
 
-    /// The form against a circuit's matrices.
-    pub fn evaluate(&self, circuit: &dyn LincheckCircuit) -> F192 {
-        let eq_inner = self.domain().inner_eq_table(self.z_skip, &self.x_inner_rest);
-        let w_col = outer_product(&eq_table(&self.r_inner_rest), &self.s_hat_v);
-        circuit.bilinear_form(self.alpha, &eq_inner, &w_col)
+    /// The form against a circuit's matrices, on `a`: the native verifier's `Portable`, or a prover's replay.
+    ///
+    /// The row weights `u = eq_rows (x) lagrange` are never built: each block of `2^k_skip` rows takes the Lagrange
+    /// weights, and the blocks their eq weights.
+    pub fn evaluate<A: Arith<E = F192>>(&self, a: &mut A, circuit: &dyn LincheckCircuit) -> F192 {
+        let domain = self.domain();
+        let lagrange = domain.lagrange_weights(a, self.z_skip);
+        let eq_rows = a.eq_table(&self.x_inner_rest);
+        let eq_cols = a.eq_table(&self.r_inner_rest);
+        let w = outer_product(a, &eq_cols, &self.s_hat_v);
+        let (ra, rb) = circuit.matrix_rows(&w);
+        let n = ra.len().min(eq_rows.len() << domain.k_skip());
+        let rows: Vec<F192> = (ra[..n].iter().zip(&rb))
+            .map(|(&ra, &rb)| a.mul_add(self.alpha, rb, ra))
+            .collect();
+        let blocks: Vec<F192> = (rows.chunks(lagrange.len()))
+            .map(|block| a.dot(&lagrange[..block.len()], block))
+            .collect();
+        a.dot(&eq_rows[..blocks.len()], &blocks)
     }
 
     /// The form's weight on each bit slice, so that its value is `sum_i s_hat_v[i] * weights[i]`.
@@ -603,12 +617,12 @@ pub struct MatrixClaim<E = F192> {
 }
 
 impl MatrixClaim {
-    /// Settle the claim against a circuit's matrices.
+    /// Settle the claim against a circuit's matrices, on `a`.
     ///
     /// # Errors
     ///
     /// The circuit's width if it is not the form's, and a form mismatch when the form misses the value.
-    pub fn check(&self, circuit: &dyn LincheckCircuit) -> Result<(), LincheckError> {
+    pub fn check<A: Arith<E = F192>>(&self, a: &mut A, circuit: &dyn LincheckCircuit) -> Result<(), LincheckError> {
         // The form's column point and slices fix the circuit's width.
         let n_cols = self.form.s_hat_v.len() << self.form.r_inner_rest.len();
         if circuit.n_cols() != n_cols {
@@ -618,7 +632,7 @@ impl MatrixClaim {
             });
         }
         // The terminal identity holds exactly when the form takes the claimed value.
-        if self.form.evaluate(circuit) == self.value {
+        if self.form.evaluate(a, circuit) == self.value {
             Ok(())
         } else {
             Err(LincheckError::FormMismatch)
@@ -1144,6 +1158,7 @@ mod neon {
 mod tests {
     use std::collections::HashSet;
 
+    use fiat_shamir::arith::Portable;
     use fiat_shamir::{ProofTranscript, SessionId, VerifierState};
     use primitives::test_util::Rng;
 
@@ -1203,6 +1218,13 @@ mod tests {
             }
             out
         }
+
+        /// `M w`.
+        fn product(&self, w: &[F192]) -> Vec<F192> {
+            (self.rows.iter())
+                .map(|row| row.iter().fold(F192::ZERO, |acc, &c| acc + w[c]))
+                .collect()
+        }
     }
 
     /// A circuit over materialized matrices, by the naive row scatter.
@@ -1225,9 +1247,8 @@ mod tests {
             a.iter().zip(&b).map(|(&x, &y)| x + alpha * y).collect()
         }
 
-        fn bilinear_form(&self, alpha: F192, u: &[F192], w: &[F192]) -> F192 {
-            // The marginal's inner product with the column weights: the definition, through the materialized rows.
-            primitives::multilinear::inner_product(&self.fold_alpha_batched(alpha, u), w)
+        fn matrix_rows(&self, w: &[F192]) -> (Vec<F192>, Vec<F192>) {
+            (self.a_0.product(w), self.b_0.product(w))
         }
     }
 
@@ -1306,7 +1327,7 @@ mod tests {
             let matrices = verify_deferred(domain, &zc, &[shape], &mut vs)?
                 .pop()
                 .expect("one circuit");
-            matrices.check(&self.circuit)?;
+            matrices.check(&mut Portable, &self.circuit)?;
             Ok(LincheckClaim {
                 r_inner_rest: matrices.form.r_inner_rest,
                 s_hat_v: matrices.form.s_hat_v,
@@ -1316,7 +1337,7 @@ mod tests {
 
     /// A Boolean vector's extension at a quirky point: skip Lagrange weights, then eq on the other coordinates.
     fn skip_eval(f: &[bool], k_log: usize, k_skip: usize, point: &SkipPoint) -> F192 {
-        let lambda = SkipDomain::new(k_skip).lagrange_weights(point.z_skip);
+        let lambda = SkipDomain::new(k_skip).lagrange_weights(&mut Native, point.z_skip);
         let eq_rest = eq_table(&point.x_inner_rest);
         let eq_outer = eq_table(&point.x_outer);
         let mut acc = F192::ZERO;
@@ -1359,6 +1380,41 @@ mod tests {
         }
     }
 
+    #[test]
+    fn a_matrix_form_is_its_bilinear_form() {
+        // The form summed a skip block at a time is `sum_i u_i (A w + alpha B w)_i` with `u` and `w` built whole.
+        for (k_log, k_skip) in [(6, 0), (6, 3), (6, 6), (9, 4)] {
+            let mut rng = Rng::new(88 + (k_log * 10 + k_skip) as u64);
+            let k = 1 << k_log;
+            let circuit = SparseCircuit {
+                a_0: SparseMatrix::random(k, 3 * k, &mut rng),
+                b_0: SparseMatrix::random(k, 3 * k, &mut rng),
+            };
+            let form = MatrixForm {
+                alpha: rng.ext(),
+                z_skip: rng.ext(),
+                x_inner_rest: rng.ext_vec(k_log - k_skip),
+                r_inner_rest: rng.ext_vec(k_log - k_skip),
+                s_hat_v: rng.ext_vec(1 << k_skip),
+            };
+            let u = SkipDomain::new(k_skip).inner_eq_table(form.z_skip, &form.x_inner_rest);
+            let w = outer_product(&mut Native, &eq_table(&form.r_inner_rest), &form.s_hat_v);
+            let (ra, rb) = circuit.matrix_rows(&w);
+            let want = (u.iter().zip(ra.iter().zip(&rb)))
+                .fold(F192::ZERO, |acc, (&u, (&ra, &rb))| acc + u * (ra + form.alpha * rb));
+            assert_eq!(
+                form.evaluate(&mut Portable, &circuit),
+                want,
+                "k_log={k_log}, k_skip={k_skip}"
+            );
+            assert_eq!(
+                form.evaluate(&mut Native, &circuit),
+                want,
+                "k_log={k_log}, k_skip={k_skip}"
+            );
+        }
+    }
+
     #[test]
     fn a_form_is_its_slices_against_their_weights() {
         // Invariant: the form is linear in its slices, with weights fixed by its other coordinates.
@@ -1378,7 +1434,11 @@ mod tests {
             };
             let weights = form.slice_weights(&f.circuit);
             let linear = (form.s_hat_v.iter().zip(&weights)).fold(F192::ZERO, |acc, (&s, &w)| acc + s * w);
-            assert_eq!(form.evaluate(&f.circuit), linear, "k_log={k_log}, k_skip={k_skip}");
+            assert_eq!(
+                form.evaluate(&mut Portable, &f.circuit),
+                linear,
+                "k_log={k_log}, k_skip={k_skip}"
+            );
         }
     }
 
diff --git a/crates/flock/src/reduction.rs b/crates/flock/src/reduction.rs
index 5c53ddbba..ce4b2146b 100644
--- a/crates/flock/src/reduction.rs
+++ b/crates/flock/src/reduction.rs
@@ -274,6 +274,7 @@ mod tests {
     //! The circuits are built from the builder and the multiplier gadget, their witnesses by the generic walk.
     //! Only the commitment's opening is left out: it is generic in the claims.
 
+    use fiat_shamir::arith::Portable;
     use fiat_shamir::{ProofTranscript, ProverState, SessionId, VerifierState};
     use primitives::field::F192;
     use primitives::test_util::Rng;
@@ -368,7 +369,7 @@ mod tests {
         tamper(&mut proof);
         let mut vs = VerifierState::new(&SessionId::new(LABEL), &0u64, &proof);
         reduction::verify(&[(block.shape(), n_log)], &mut vs)
-            .is_ok_and(|r| r[0].claim == claims[0] && r[0].matrices.check(block.circuit).is_ok())
+            .is_ok_and(|r| r[0].claim == claims[0] && r[0].matrices.check(&mut Portable, block.circuit).is_ok())
             && vs.check_eof().is_ok()
     }
 
@@ -454,7 +455,8 @@ mod tests {
             let mut vs = VerifierState::new(&SessionId::new(LABEL), &0u64, proof);
             let shapes: Vec<_> = blocks.iter().map(|(block, n)| (block.shape(), *n)).collect();
             let replays = reduction::verify(&shapes, &mut vs).ok()?;
-            let settled = (replays.iter().zip(&blocks)).all(|(r, (block, _))| r.matrices.check(block.circuit).is_ok());
+            let settled = (replays.iter().zip(&blocks))
+                .all(|(r, (block, _))| r.matrices.check(&mut Portable, block.circuit).is_ok());
             (settled && vs.check_eof().is_ok()).then_some(replays)
         };
 
diff --git a/crates/flock/src/zerocheck/mod.rs b/crates/flock/src/zerocheck/mod.rs
index 55f311f5b..2e2153acb 100644
--- a/crates/flock/src/zerocheck/mod.rs
+++ b/crates/flock/src/zerocheck/mod.rs
@@ -29,7 +29,7 @@ use crate::lincheck::SkipPoint;
 use crate::round::RoundEvals;
 use lde::{AdditiveNttF8, LdeTable};
 use multilinear::{PackedWitness, RoundPair, bit_pass, bit_pass_storing, single_round, table_pass};
-use round1::{Round1, c_s, medium_challenges, small_challenges};
+use round1::{MEDIUM_CHALLENGES, Round1, c_s, small_challenges};
 
 mod lde;
 pub(crate) mod multilinear;
@@ -75,7 +75,7 @@ fn equality_tail(m: usize, sample: impl FnOnce(usize) -> Vec<F192>) -> Vec<F192>
     let outer = sample(m - MIN_CUBE_LOG);
     small_challenges()
         .into_iter()
-        .chain(medium_challenges())
+        .chain(MEDIUM_CHALLENGES)
         .chain(outer)
         .collect()
 }
@@ -245,7 +245,7 @@ impl<'a> CircuitProver<'a> {
 
     /// Take the skip challenge: the running claim becomes this circuit's `P(z)`.
     fn start(&mut self, z: F192, round1: &[F192]) {
-        self.lagrange = SkipDomain::FLOCK.lagrange_weights(z);
+        self.lagrange = SkipDomain::FLOCK.lagrange_weights(&mut Native, z);
         let vanishing = SkipDomain::FLOCK.vanishing(&mut Native, z);
         self.claim = SkipDomain::FLOCK.first_round_at(&mut Native, z, vanishing, round1);
     }
@@ -501,7 +501,7 @@ pub(crate) fn verify<V: Verifier>(log_ns: &[usize], v: &mut V) -> Result<Zeroche
     let outer = v.verifier_messages(m - MIN_CUBE_LOG);
     let lambda = v.verifier_message();
     let lambdas = v.powers(lambda, log_ns.len());
-    let fixed: Vec<V::E> = (small_challenges().into_iter().chain(medium_challenges()))
+    let fixed: Vec<V::E> = (small_challenges().into_iter().chain(MEDIUM_CHALLENGES))
         .map(|c| v.constant(c))
         .collect();
 
@@ -595,7 +595,7 @@ pub(crate) mod tests {
     /// Whether a claim holds the true evaluations of all three bit vectors.
     fn all_true(claim: &ZerocheckClaim, bits: &[Vec<bool>; 3]) -> bool {
         // The extension at `(z, chi)`: the bits folded over the skip at `z`, then weighted by `eq(chi, .)`.
-        let lagrange = SkipDomain::FLOCK.lagrange_weights(claim.z);
+        let lagrange = SkipDomain::FLOCK.lagrange_weights(&mut Native, claim.z);
         let eq = eq_table(&claim.mlv_challenges);
         (bits.iter().zip(claim.evals)).all(|(bits, eval)| inner_product(&fold_at_z(bits, &lagrange), &eq) == eval)
     }
@@ -776,7 +776,7 @@ pub(crate) mod tests {
         let lambdas = F192::powers(Verifier::verifier_message(&mut vs), circuits.len());
         let round1 = vs.prover_messages(1 << K_SKIP).unwrap();
         let z = Verifier::verifier_message(&mut vs);
-        let lagrange = SkipDomain::FLOCK.lagrange_weights(z);
+        let lagrange = SkipDomain::FLOCK.lagrange_weights(&mut Native, z);
         let mut tables: Vec<[Vec<F192>; 3]> = circuits
             .iter()
             .map(|c| c.dense.each_ref().map(|bits| fold_at_z(bits, &lagrange)))
diff --git a/crates/flock/src/zerocheck/multilinear.rs b/crates/flock/src/zerocheck/multilinear.rs
index 91ca7e12f..f7b497d74 100644
--- a/crates/flock/src/zerocheck/multilinear.rs
+++ b/crates/flock/src/zerocheck/multilinear.rs
@@ -826,6 +826,7 @@ mod tests {
     use crate::zerocheck::round1::tests::pack_bits;
     use crate::zerocheck::tests::{fold_at_z, honest};
     use crate::zerocheck::{K_SKIP, SkipDomain};
+    use fiat_shamir::arith::Native;
     use primitives::multilinear::fold_low_inplace;
     use primitives::test_util::Rng;
 
@@ -879,7 +880,7 @@ mod tests {
             let (bits, packed_bits) = honest(&mut rng, m);
             let r_rest = rng.ext_vec(m - K_SKIP);
             let rho = rng.ext_vec(m - K_SKIP);
-            let lagrange = SkipDomain::FLOCK.lagrange_weights(rng.ext());
+            let lagrange = SkipDomain::FLOCK.lagrange_weights(&mut Native, rng.ext());
             let full = dense(m);
 
             // Level 0 of the naive route.
@@ -919,7 +920,7 @@ mod tests {
                 useful_bits: useful,
                 live_blocks: usize::MAX,
             };
-            let lagrange = SkipDomain::FLOCK.lagrange_weights(rng.ext());
+            let lagrange = SkipDomain::FLOCK.lagrange_weights(&mut Native, rng.ext());
             let r_rest = rng.ext_vec(m - K_SKIP);
             let rho = rng.ext_vec(4);
             for t in 0..=4 {
diff --git a/crates/flock/src/zerocheck/round1.rs b/crates/flock/src/zerocheck/round1.rs
index f0ec3e795..c13fb739a 100644
--- a/crates/flock/src/zerocheck/round1.rs
+++ b/crates/flock/src/zerocheck/round1.rs
@@ -125,29 +125,41 @@ pub(crate) fn small_challenges() -> [F192; 3] {
 const MEDIUM_GENERATOR: F192 = F192::new(0x243f_6a88_85a3_08d3, 0x1319_8a2e_0370_7344, 0xa409_3822_299f_31d0);
 
 /// `gamma, gamma^2, gamma^4, gamma^8`.
-fn medium_squares() -> [F192; N_MEDIUM] {
+const MEDIUM_SQUARES: [F192; N_MEDIUM] = {
     let mut g = [MEDIUM_GENERATOR; N_MEDIUM];
-    for i in 1..N_MEDIUM {
-        g[i] = g[i - 1].square();
+    let mut i = 1;
+    while i < N_MEDIUM {
+        g[i] = g[i - 1].square_portable();
+        i += 1;
     }
     g
-}
+};
 
-/// The four medium challenges `gamma^(2^i) / (1 + gamma^(2^i))`.
-pub(crate) fn medium_challenges() -> [F192; N_MEDIUM] {
-    medium_squares().map(|g| g * (F192::ONE + g).inv())
+/// `1 + g`.
+const fn one_plus(g: F192) -> F192 {
+    F192::new(g.c0 ^ 1, g.c1, g.c2)
 }
 
+/// The four medium challenges `gamma^(2^i) / (1 + gamma^(2^i))`, at compile time.
+pub(crate) const MEDIUM_CHALLENGES: [F192; N_MEDIUM] = {
+    let mut out = MEDIUM_SQUARES;
+    let mut i = 0;
+    while i < N_MEDIUM {
+        out[i] = out[i].mul_portable(one_plus(out[i]).inv_portable());
+        i += 1;
+    }
+    out
+};
+
 /// `1 / D`, `D = prod_i (1 + gamma^(2^i))`: it cancels the medium eq's normalization.
-fn d_inv() -> F192 {
-    static D_INV: OnceLock<F192> = OnceLock::new();
-    *D_INV.get_or_init(|| {
-        let d = medium_squares()
-            .into_iter()
-            .fold(F192::ONE, |acc, g| acc * (F192::ONE + g));
-        d.inv()
-    })
-}
+const D_INV: F192 = {
+    let (mut d, mut i) = (F192::ONE, 0);
+    while i < N_MEDIUM {
+        d = d.mul_portable(one_plus(MEDIUM_SQUARES[i]));
+        i += 1;
+    }
+    d.inv_portable()
+};
 
 /// `gamma^b` for each medium position `b`.
 fn gamma_powers() -> &'static [F192; N_MEDIUM_VALUES] {
@@ -278,12 +290,11 @@ impl<'a> Round1<'a> {
         let tail = self.padding.tail(self.m, WINDOW_LOG, WINDOW_LOG, self.r);
         let n_windows = tail.map_or(1 << (self.m - WINDOW_LOG), |t| t.head >> WINDOW_LOG);
         let eq = SplitEq::with_high_vars(&self.r[N_INNER..], EQ_HIGH_VARS);
-        let d_inv = d_inv();
         let sweep = Sweep {
             bits: self.bits,
             lde: self.lde,
             // `1 / D` rides the low half once, cancelling the medium eq's normalization.
-            eq_lo: eq.low.iter().map(|&e| e * d_inv).collect(),
+            eq_lo: eq.low.iter().map(|&e| e * D_INV).collect(),
             n_lo: eq.low_log,
             n_windows,
             medium: MediumCounts::new(&self.padding),
@@ -1130,7 +1141,7 @@ pub(crate) mod tests {
 
     /// The eq coordinates: the seven fixed ones, then random outer ones.
     fn protocol_r(rng: &mut Rng, m: usize) -> Vec<F192> {
-        (small_challenges().into_iter().chain(medium_challenges()))
+        (small_challenges().into_iter().chain(MEDIUM_CHALLENGES))
             .chain(rng.ext_vec(m - WINDOW_LOG))
             .collect()
     }
@@ -1247,7 +1258,7 @@ pub(crate) mod tests {
         // Invariant: the 2^7 eq weights of the seven fixed coordinates have rank 128 over GF(2) (lem:fixed-zerocheck).
         //
         // Rank 7 of the coordinates alone would pass while a relation among their products broke the lemma.
-        let a: Vec<F192> = small_challenges().into_iter().chain(medium_challenges()).collect();
+        let a: Vec<F192> = small_challenges().into_iter().chain(MEDIUM_CHALLENGES).collect();
         assert_eq!(a.len(), N_INNER);
 
         // One row per corner `b`: `eq(a, b) = prod_i (b_i ? a_i : 1 + a_i)`.
diff --git a/crates/flock/src/zerocheck/skip_domain.rs b/crates/flock/src/zerocheck/skip_domain.rs
index b1bc8599a..9dce6d156 100644
--- a/crates/flock/src/zerocheck/skip_domain.rs
+++ b/crates/flock/src/zerocheck/skip_domain.rs
@@ -1,8 +1,8 @@
 // CREDIT: https://github.com/succinctlabs/flock (the skip domain's Lagrange weights), MIT OR Apache-2.0.
 //! The univariate skip's domain, and the interpolations at the skip challenge its verifiers and its prover share.
 
-use fiat_shamir::arith::Arith;
-use primitives::field::gf2_64::{reduce, software::clmul};
+use fiat_shamir::arith::{Arith, Native};
+use primitives::field::gf2_64::{portable::clmul, reduce};
 use primitives::field::{F192, PHI8_TABLE};
 use primitives::multilinear::eq_table;
 
@@ -16,20 +16,59 @@ use crate::lincheck::outer_product;
 #[derive(Clone, Copy, Debug, PartialEq, Eq)]
 pub struct SkipDomain {
     k_skip: usize,
+    /// The coefficients `c_j` of `V_S(X) = prod_{s in S} (X + s) = sum_j c_j X^(2^j)`, lowest first, zero past `k_skip`.
+    vanishing: [F192; 8],
+    /// `V_S(phi_8(2^k_skip))`, by which the coset's vanishing polynomial `V_Lambda` exceeds `V_S`, `V_S` being linear.
+    offset: F192,
 }
 
 impl SkipDomain {
     /// The domain the zerocheck skips and the lincheck interpolates over.
-    pub const FLOCK: Self = Self { k_skip: K_SKIP };
+    pub const FLOCK: Self = Self::new(K_SKIP);
 
-    /// The domain of `2^k_skip` nodes.
+    /// The domain of `2^k_skip` nodes, its constants computed at compile time.
     ///
     /// # Panics
     ///
     /// If `S` and `Lambda` do not fit the phi_8 table.
     pub(crate) const fn new(k_skip: usize) -> Self {
+        const ALL: [SkipDomain; 8] = {
+            let mut all = [SkipDomain::compute(0); 8];
+            let mut k = 1;
+            while k < 8 {
+                all[k] = SkipDomain::compute(k);
+                k += 1;
+            }
+            all
+        };
         assert!(k_skip < 8, "the window fits the phi_8 table");
-        Self { k_skip }
+        ALL[k_skip]
+    }
+
+    /// The domain of `2^k_skip` nodes, by the portable products.
+    const fn compute(k_skip: usize) -> Self {
+        // Adding a basis element `a` to a subspace takes `V` to `V(X)^2 + V(a) V(X)`, since `V(X + a) = V(X) + V(a)`.
+        // The zero subspace's polynomial is `X`; the basis elements are `phi_8(2^j)`.
+        let mut vanishing = [F192::ZERO; 8];
+        vanishing[0] = F192::ONE;
+        let mut j = 0;
+        while j < k_skip {
+            let at_a = linearized(&vanishing, PHI8_TABLE[1 << j]);
+            // `V(X)^2` shifts every coefficient up a power; `V(a) V(X)` scales them in place.
+            let mut k = j + 1;
+            while k > 0 {
+                vanishing[k] = plus(vanishing[k - 1].square_portable(), at_a.mul_portable(vanishing[k]));
+                k -= 1;
+            }
+            vanishing[0] = at_a.mul_portable(vanishing[0]);
+            j += 1;
+        }
+        let offset = linearized(&vanishing, PHI8_TABLE[1 << k_skip]);
+        Self {
+            k_skip,
+            vanishing,
+            offset,
+        }
     }
 
     /// The base-two logarithm of its size.
@@ -42,29 +81,9 @@ impl SkipDomain {
         1 << self.k_skip
     }
 
-    /// The coefficients `c_j` of `V_S(X) = prod_{s in S} (X + s) = sum_j c_j X^(2^j)`, lowest first.
-    ///
-    /// Adding a basis element `a` to a subspace takes `V` to `V(X)^2 + V(a) V(X)`, since `V(X + a) = V(X) + V(a)`.
-    fn vanishing_coefficients(self) -> Vec<F192> {
-        // The zero subspace's polynomial is `X`.
-        let mut c = vec![F192::ZERO; self.k_skip + 1];
-        c[0] = F192::ONE;
-        // Add the basis elements `phi_8(2^j)` one at a time.
-        for j in 0..self.k_skip {
-            let a = PHI8_TABLE[1 << j];
-            let at_a = linearized(&c, a);
-            // `V(X)^2` shifts every coefficient up a power; `V(a) V(X)` scales them in place.
-            for k in (0..=j + 1).rev() {
-                let squared = if k == 0 { F192::ZERO } else { c[k - 1].square() };
-                c[k] = squared + at_a * c[k];
-            }
-        }
-        c
-    }
-
     /// `V_S(z)`: `k_skip` squarings and as many products by constants of `K`.
     pub fn vanishing<A: Arith>(self, a: &mut A, z: A::E) -> A::E {
-        let c = self.vanishing_coefficients();
+        let c = &self.vanishing;
         // `z^(2^j)` for every `j`, by squaring.
         let mut powers = vec![z];
         for j in 0..self.k_skip {
@@ -90,8 +109,7 @@ impl SkipDomain {
         let size = self.size();
         // The coset's vanishing polynomial is the domain's shifted by a constant, `V_S` being linear.
         let lambda = &PHI8_TABLE[size..2 * size];
-        let offset = linearized(&self.vanishing_coefficients(), lambda[0]);
-        let on_lambda = a.add_const(vanishing, offset);
+        let on_lambda = a.add_const(vanishing, self.offset);
         let both = a.mul(vanishing, on_lambda);
         let scaled = a.mul_const(both, window_denominator(2 * size));
         let inverses = inverses_at(a, z, lambda);
@@ -110,9 +128,9 @@ impl SkipDomain {
         lagrange_sum(a, scaled, &inverses, values)
     }
 
-    /// The Lagrange basis of `S` at `z`, the prover's form: `L_i(z) = D_l * prod_{k != i} (z + s_k)`.
-    pub(crate) fn lagrange_weights(self, z: F192) -> Vec<F192> {
-        window_lagrange_weights(self.k_skip, z)
+    /// The Lagrange basis of `S` at `z`, `L_i(z) = D_l * prod_{k != i} (z + s_k)`, on `a`.
+    pub(crate) fn lagrange_weights<A: Arith>(self, a: &mut A, z: A::E) -> Vec<A::E> {
+        window_lagrange_weights(a, self.k_skip, z)
     }
 
     /// The eq table of a skip point's inner half: the Lagrange basis at `z_skip` on the low index bits.
@@ -121,20 +139,30 @@ impl SkipDomain {
     ///     out[i_skip + i_rest 2^k_skip] = L_(i_skip)(z_skip) * eq(x_inner_rest, i_rest)
     /// ```
     pub fn inner_eq_table(self, z_skip: F192, x_inner_rest: &[F192]) -> Vec<F192> {
-        outer_product(&eq_table(x_inner_rest), &self.lagrange_weights(z_skip))
+        outer_product(
+            &mut Native,
+            &eq_table(x_inner_rest),
+            &self.lagrange_weights(&mut Native, z_skip),
+        )
     }
 }
 
-/// A linearized polynomial `sum_j c_j x^(2^j)` at `x`.
-fn linearized(c: &[F192], x: F192) -> F192 {
-    let (mut power, mut acc) = (x, F192::ZERO);
-    for &cj in c {
-        acc += cj * power;
-        power = power.square();
+/// A linearized polynomial `sum_j c_j x^(2^j)` at `x`, by the portable products.
+const fn linearized(c: &[F192; 8], x: F192) -> F192 {
+    let (mut power, mut acc, mut j) = (x, F192::ZERO, 0);
+    while j < c.len() {
+        acc = plus(acc, c[j].mul_portable(power));
+        power = power.square_portable();
+        j += 1;
     }
     acc
 }
 
+/// `a + b`, in a `const` context.
+const fn plus(a: F192, b: F192) -> F192 {
+    F192::new(a.c0 ^ b.c0, a.c1 ^ b.c1, a.c2 ^ b.c2)
+}
+
 /// `1 / (z + node)` for each node.
 fn inverses_at<A: Arith>(a: &mut A, z: A::E, nodes: &[F192]) -> Vec<A::E> {
     (nodes.iter())
@@ -158,22 +186,25 @@ pub(crate) fn lagrange_sum<A: Arith>(a: &mut A, scale: A::E, inverses: &[A::E],
 /// Prefix and suffix products of the differences give every weight.
 ///
 /// No inverse is taken, so the weights are exact at a node too.
-fn window_lagrange_weights(log_size: usize, z: F192) -> Vec<F192> {
+fn window_lagrange_weights<A: Arith>(a: &mut A, log_size: usize, z: A::E) -> Vec<A::E> {
     let n = 1 << log_size;
     let nodes = &PHI8_TABLE[..n];
     // Prefix products: weight `i` holds `prod_{k < i} (z + s_k)`.
-    let mut weights = vec![window_denominator(n); n];
+    let denominator = a.constant(window_denominator(n));
+    let mut weights = vec![denominator; n];
     for i in 1..n {
-        weights[i] = weights[i - 1] * (z + nodes[i - 1]);
+        let difference = a.add_const(z, nodes[i - 1]);
+        weights[i] = a.mul(weights[i - 1], difference);
     }
     // Suffix products: weight `i` takes `prod_{k > i} (z + s_k)`.
-    let mut suffix = z + nodes[n - 1];
+    let mut suffix = a.add_const(z, nodes[n - 1]);
     for i in (1..n - 1).rev() {
-        weights[i] *= suffix;
-        suffix *= z + nodes[i];
+        weights[i] = a.mul(weights[i], suffix);
+        let difference = a.add_const(z, nodes[i]);
+        suffix = a.mul(suffix, difference);
     }
     if n > 1 {
-        weights[0] *= suffix;
+        weights[0] = a.mul(weights[0], suffix);
     }
     weights
 }
@@ -226,7 +257,7 @@ const DENOMINATORS: [F192; 9] = {
 #[cfg(test)]
 mod tests {
     use super::*;
-    use fiat_shamir::arith::Native;
+    use fiat_shamir::arith::Portable;
     use primitives::test_util::Rng;
 
     /// `1 / prod_{k != i} (s_i + s_k)` over a window's nodes, by its definition.
@@ -269,7 +300,16 @@ mod tests {
                         others.fold(per_node_denominator(nodes, i), |acc, (_, &node)| acc * (z + node))
                     })
                     .collect();
-                assert_eq!(window_lagrange_weights(log_size, z), want, "log_size {log_size}");
+                assert_eq!(
+                    window_lagrange_weights(&mut Native, log_size, z),
+                    want,
+                    "log_size {log_size}"
+                );
+                assert_eq!(
+                    window_lagrange_weights(&mut Portable, log_size, z),
+                    want,
+                    "log_size {log_size}"
+                );
             }
         }
     }
@@ -285,7 +325,7 @@ mod tests {
             let values = rng.ext_vec(domain.size());
             for z in rng.ext_vec(4) {
                 // The window's Lagrange weights at `z`, zero on S, so only Lambda's half counts.
-                let window = window_lagrange_weights(k_skip + 1, z)[domain.size()..]
+                let window = window_lagrange_weights(&mut Native, k_skip + 1, z)[domain.size()..]
                     .iter()
                     .zip(&values)
                     .fold(F192::ZERO, |acc, (&w, &v)| acc + w * v);
@@ -312,8 +352,8 @@ mod tests {
                 // `V_S(z)` as the product over the nodes.
                 let vanishing = (PHI8_TABLE[..domain.size()].iter()).fold(F192::ONE, |acc, &s| acc * (z + s));
                 assert_eq!(domain.vanishing(&mut Native, z), vanishing, "k_skip {k_skip}");
-                let lagrange =
-                    (domain.lagrange_weights(z).iter().zip(&values)).fold(F192::ZERO, |acc, (&w, &v)| acc + w * v);
+                let lagrange = (domain.lagrange_weights(&mut Native, z).iter().zip(&values))
+                    .fold(F192::ZERO, |acc, (&w, &v)| acc + w * v);
                 assert_eq!(
                     domain.lagrange_at(&mut Native, z, vanishing, &values),
                     lagrange,
diff --git a/crates/leanvm_core/benches/class_batch.rs b/crates/leanvm_core/benches/class_batch.rs
index 5a962e266..ac6798931 100644
--- a/crates/leanvm_core/benches/class_batch.rs
+++ b/crates/leanvm_core/benches/class_batch.rs
@@ -201,7 +201,10 @@ impl ClassBatch {
         let replay = reduction::verify(&[(block.shape(), self.n_log)], &mut vs)
             .expect("the reduction verifies")
             .remove(0);
-        replay.matrices.check(block.circuit).expect("the matrices settle");
+        replay
+            .matrices
+            .check(&mut vs, block.circuit)
+            .expect("the matrices settle");
         let ring = RingSwitch {
             offset: 0,
             qflock_vars: self.mu,
diff --git a/crates/leanvm_core/src/bus/coord.rs b/crates/leanvm_core/src/bus/coord.rs
index 59ad44cbb..04326fbd7 100644
--- a/crates/leanvm_core/src/bus/coord.rs
+++ b/crates/leanvm_core/src/bus/coord.rs
@@ -1,8 +1,8 @@
 //! A tuple coordinate as a function of its block's row, and the public columns a coordinate reads.
 
 use crate::rec::FixedColumn;
-use fiat_shamir::VerifierState;
 use fiat_shamir::arith::{Arith, Native};
+use fiat_shamir::{Hashing, VerifierState};
 use pcs::verifier::Recording;
 use primitives::field::{F64, F192};
 use std::sync::{Arc, OnceLock};
@@ -80,7 +80,7 @@ pub(crate) trait PublicColumns: Arith {
 
 impl PublicColumns for Native {}
 
-impl PublicColumns for VerifierState<'_> {}
+impl<A: Arith<E = F192> + Hashing> PublicColumns for VerifierState<'_, A> {}
 
 impl PublicColumns for Recording<'_> {}
 
@@ -152,14 +152,13 @@ impl SparseColumn {
     }
 
     /// The column's multilinear extension at `point`.
-    pub(crate) fn eval(&self, point: &[F192]) -> F192 {
+    pub(crate) fn eval<A: Arith<E = F192>>(&self, a: &mut A, point: &[F192]) -> F192 {
         assert_eq!(point.len(), self.log_len);
         self.blocks.iter().fold(F192::ZERO, |acc, (at, words)| {
             let k = words.len().ilog2() as usize;
-            let selector = point[k..].iter().enumerate().fold(F192::ONE, |s, (j, &z)| {
-                s * if (at >> (k + j)) & 1 == 1 { z } else { z + F192::ONE }
-            });
-            acc + selector * primitives::multilinear::mle_eval(words, &point[..k])
+            let selector = a.eq_bits(at >> k, &point[k..]);
+            let block = a.public_mle(words, &point[..k]);
+            a.mul_add(selector, block, acc)
         })
     }
 }
diff --git a/crates/leanvm_core/src/bus/decompose.rs b/crates/leanvm_core/src/bus/decompose.rs
index 52da59ecf..10522c91c 100644
--- a/crates/leanvm_core/src/bus/decompose.rs
+++ b/crates/leanvm_core/src/bus/decompose.rs
@@ -50,7 +50,7 @@ pub fn producer_affine_evals<A: Arith>(a: &mut A, p: &Producer, w: &[A::E], beta
             constant = a.square(constant);
             for (weight, monomials) in &mut affine {
                 *weight = a.square(*weight);
-                monomials.iter_mut().for_each(|m| *m = *m * *m);
+                monomials.iter_mut().for_each(|m| *m = m.square_portable());
             }
         }
     }
@@ -71,14 +71,26 @@ pub fn producer_affine_evals<A: Arith>(a: &mut A, p: &Producer, w: &[A::E], beta
 /// ```
 ///
 /// That is one pass over the columns, then a fixed cost per coordinate, bit and power.
-pub(crate) fn producer_public_twist(coords: &[Coord], w: &[F192], chi: &[F192], twist: &[F192]) -> F192 {
-    (producer_twist_terms(coords, w, chi, twist.len()).iter().zip(twist))
-        .fold(F192::ZERO, |acc, (&d, &mu)| acc + mu * d)
+pub(crate) fn producer_public_twist<A: Arith<E = F192>>(
+    a: &mut A,
+    coords: &[Coord],
+    w: &[F192],
+    chi: &[F192],
+    twist: &[F192],
+) -> F192 {
+    let terms = producer_twist_terms(a, coords, w, chi, twist.len());
+    a.dot(twist, &terms)
 }
 
 /// The terms `D_i` of the public half above, for `i < n_terms`, so that it is `sum_i mu_i D_i`.
-pub(crate) fn producer_twist_terms(coords: &[Coord], w: &[F192], chi: &[F192], n_terms: usize) -> Vec<F192> {
-    let eq = primitives::multilinear::eq_table(chi);
+pub(crate) fn producer_twist_terms<A: Arith<E = F192>>(
+    a: &mut A,
+    coords: &[Coord],
+    w: &[F192],
+    chi: &[F192],
+    n_terms: usize,
+) -> Vec<F192> {
+    let eq = a.eq_table(chi);
     let mut terms = vec![F192::ZERO; n_terms];
     for (c, &weight) in coords.iter().zip(w) {
         let Coord::Public(PublicColumn { values: vals, .. }) = c else {
@@ -97,10 +109,10 @@ pub(crate) fn producer_twist_terms(coords: &[Coord], w: &[F192], chi: &[F192], n
         let mut weight = weight;
         let mut basis: [F64; 64] = std::array::from_fn(|k| F64(1 << k));
         for term in &mut terms {
-            let sum = (slices.iter().zip(&basis)).fold(F192::ZERO, |s, (b, &g)| s + b.mul_base(g));
-            *term += weight * sum;
-            weight = weight.square();
-            basis.iter_mut().for_each(|g| *g = *g * *g);
+            let sum = (slices.iter().zip(&basis)).fold(F192::ZERO, |s, (&b, &g)| a.mul_const_add(b, F192::from(g), s));
+            *term = a.mul_add(weight, sum, *term);
+            weight = a.square(weight);
+            basis.iter_mut().for_each(|g| *g = g.square_portable());
         }
     }
     terms
@@ -528,6 +540,8 @@ impl Side<'_> {
             Ok::<_, Infallible>(v)
         });
         let Ok(framework) = framework;
-        (open.sparse.drain(..)).fold(framework, |acc, s| acc + s.weight * s.column.eval(&s.point))
+        (open.sparse.drain(..)).fold(framework, |acc, s| {
+            acc + s.weight * s.column.eval(&mut Native, &s.point)
+        })
     }
 }
diff --git a/crates/leanvm_core/src/bus/mod.rs b/crates/leanvm_core/src/bus/mod.rs
index 0cf59a937..80e0e2e69 100644
--- a/crates/leanvm_core/src/bus/mod.rs
+++ b/crates/leanvm_core/src/bus/mod.rs
@@ -504,6 +504,7 @@ pub(crate) mod tests {
     use crate::cpu::{Layout, Lookup, Program, UNGROUND_LOG_BYTECODE};
     use crate::rv::Region;
     use crate::tables::PerTable;
+    use fiat_shamir::arith::Portable;
     use fiat_shamir::{ProverState, SessionId, VerifierState};
     use std::collections::HashMap;
     use std::sync::Arc;
@@ -606,7 +607,7 @@ pub(crate) mod tests {
         assert_eq!(column.dense().iter().filter(|w| !w.is_zero()).count(), words.len());
         let point: Vec<F192> = (0..9).map(|i| F192::new(3 + i, 5 * i + 1, 7)).collect();
         assert_eq!(
-            column.eval(&point),
+            column.eval(&mut Portable, &point),
             primitives::multilinear::mle_eval(column.dense(), &point)
         );
     }
diff --git a/crates/leanvm_core/src/constraints.rs b/crates/leanvm_core/src/constraints.rs
index fe6fdae61..8229eed85 100644
--- a/crates/leanvm_core/src/constraints.rs
+++ b/crates/leanvm_core/src/constraints.rs
@@ -35,7 +35,7 @@
 use crate::PAR_THRESHOLD;
 use fiat_shamir::arith::RoundWeight;
 use fiat_shamir::arith::{Arith, Verifier};
-use fiat_shamir::{ProverState, TranscriptError, VerifierState};
+use fiat_shamir::{Hashing, ProverState, TranscriptError, VerifierState};
 use parallel::ChunkView;
 use primitives::field::{F64, F192, F192Unreduced, Subfield, padded_width};
 use primitives::multilinear::{SplitEq, eq_table, poly_eval, shrink_eq_high};
@@ -96,12 +96,12 @@ pub trait Residual<A: Arith> {
     }
 }
 
-impl<S: Summand> Residual<VerifierState<'_>> for S {
-    fn value_at(&self, _: &mut VerifierState<'_>, cols: &[F192]) -> F192 {
+impl<S: Summand, A: Arith<E = F192> + Hashing> Residual<VerifierState<'_, A>> for S {
+    fn value_at(&self, _: &mut VerifierState<'_, A>, cols: &[F192]) -> F192 {
         Summand::eval(self, cols, false)
     }
 
-    fn public_at(&self, _: &mut VerifierState<'_>, chi: &[F192]) -> Vec<F192> {
+    fn public_at(&self, _: &mut VerifierState<'_, A>, chi: &[F192]) -> Vec<F192> {
         Summand::public(self, chi)
     }
 }
diff --git a/crates/leanvm_core/src/cpu/deferred.rs b/crates/leanvm_core/src/cpu/deferred.rs
index 8315ef398..cf0dbf6e5 100644
--- a/crates/leanvm_core/src/cpu/deferred.rs
+++ b/crates/leanvm_core/src/cpu/deferred.rs
@@ -19,7 +19,7 @@ use crate::bus::{BusVerify, N_TUPLE_BITS, SparseColumn};
 use crate::constraints::{ConstraintError, Final};
 use crate::rv::RiscvProgram;
 use crate::tables::{CircuitId, N_CIRCUITS, N_TABLES, Part};
-use fiat_shamir::arith::Arith;
+use fiat_shamir::arith::{Arith, Portable};
 use flock::FlockError;
 use flock::lincheck::{LincheckError, MatrixClaim, MatrixForm};
 use primitives::field::F192;
@@ -127,7 +127,7 @@ pub enum MalformedClaim {
 
 impl ProgramPoint {
     /// The value of the program's fixed polynomials at this point, if the point has the program's shape.
-    fn evaluate(&self, rv: &RiscvProgram) -> Option<F192> {
+    fn evaluate<A: Arith<E = F192>>(&self, a: &mut A, rv: &RiscvProgram) -> Option<F192> {
         let kbc = crate::log2_strict_usize(rv.entries().len());
         // A multiplicity is one word, so it has at most 64 bits.
         if self.bytecode.len() != kbc + N_TUPLE_BITS || self.image_point.len() != rv.log_ram() || self.twist.len() > 64
@@ -135,10 +135,11 @@ impl ProgramPoint {
             return None;
         }
         let (chi, alphas) = self.bytecode.split_at(kbc);
-        let weights = bus::fingerprint_weights(alphas);
-        let bytecode = bus::producer_public_twist(&Lookup::Bytecode.tuple(rv), &weights, chi, &self.twist);
-        let image = SparseColumn::new(rv.log_ram(), &[(0, rv.image())]);
-        Some(bytecode + self.image_weight * image.eval(&self.image_point))
+        // The fingerprint weights are the eq weights of the slots at `alphas`.
+        let weights = a.eq_table(alphas);
+        let bytecode = bus::producer_public_twist(a, &Lookup::Bytecode.tuple(rv), &weights, chi, &self.twist);
+        let image = SparseColumn::new(rv.log_ram(), &[(0, rv.image())]).eval(a, &self.image_point);
+        Some(a.mul_add(self.image_weight, image, bytecode))
     }
 }
 
@@ -199,9 +200,15 @@ impl Program {
     ///
     /// - A malformed claim: one whose shape no proof of this program gives.
     /// - A false claim: the stage whose identity it completes, the table constraints or the circuit's lincheck.
-    #[tracing::instrument(name = "Check deferred", skip_all)]
     #[doc(hidden)]
     pub fn check_deferred(&self, claims: &DeferredClaims) -> Result<(), CpuError> {
+        let _portable = primitives::portable::enter();
+        self.settle(&mut Portable, claims)
+    }
+
+    /// [`Self::check_deferred`] on `a`.
+    #[tracing::instrument(name = "Check deferred", skip_all)]
+    pub(super) fn settle<A: Arith<E = F192>>(&self, a: &mut A, claims: &DeferredClaims) -> Result<(), CpuError> {
         if claims.circuits.len() != N_CIRCUITS {
             return Err(CpuError::MalformedClaim(MalformedClaim::CircuitCount {
                 expected: N_CIRCUITS,
@@ -210,7 +217,7 @@ impl Program {
         }
 
         let program = (claims.program.point)
-            .evaluate(self.rv())
+            .evaluate(a, self.rv())
             .ok_or(CpuError::MalformedClaim(MalformedClaim::ProgramPoint))?;
         if program != claims.program.value {
             return Err(CpuError::Constraint(ConstraintError::FinalMismatch));
@@ -221,7 +228,7 @@ impl Program {
             if !f.shape().fits(&claim.point) {
                 return Err(CpuError::MalformedClaim(MalformedClaim::MatrixForm { table, part }));
             }
-            if claim.point.evaluate(f.circuit()) != claim.value {
+            if claim.point.evaluate(a, f.circuit()) != claim.value {
                 return Err(CpuError::Flock {
                     table,
                     part,
@@ -273,7 +280,11 @@ mod tests {
         for i in 0..bits {
             let d = eq.iter().zip(&c).fold(F192::ZERO, |acc, (&e, &v)| acc + e * v);
             let unit: Vec<F192> = (0..=i).map(|j| if j == i { F192::ONE } else { F192::ZERO }).collect();
-            assert_eq!(bus::producer_public_twist(&tuple, &weights, &chi, &unit), d, "bit {i}");
+            assert_eq!(
+                bus::producer_public_twist(&mut Portable, &tuple, &weights, &chi, &unit),
+                d,
+                "bit {i}"
+            );
             let twisted: Vec<F192> = chi
                 .iter()
                 .map(|&z| frobenius(z, 192 - i))
@@ -285,6 +296,9 @@ mod tests {
         }
         let twist = rng.ext_vec(bits);
         let batched = (twist.iter().zip(&per_bit)).fold(F192::ZERO, |acc, (&mu, &d)| acc + mu * d);
-        assert_eq!(bus::producer_public_twist(&tuple, &weights, &chi, &twist), batched);
+        assert_eq!(
+            bus::producer_public_twist(&mut Portable, &tuple, &weights, &chi, &twist),
+            batched
+        );
     }
 }
diff --git a/crates/leanvm_core/src/cpu/layout.rs b/crates/leanvm_core/src/cpu/layout.rs
index d19bffc33..7f7e553b8 100644
--- a/crates/leanvm_core/src/cpu/layout.rs
+++ b/crates/leanvm_core/src/cpu/layout.rs
@@ -214,19 +214,19 @@ impl Lookup {
     }
 
     /// The array's public columns over its entries, in tuple order after the address.
+    ///
+    /// On the calling thread: the verifier builds them too.
     pub fn columns(self, p: &RiscvProgram) -> Vec<Vec<F64>> {
         match self {
             // The program's columns, in bytecode slot order.
             Self::Bytecode => {
                 let entries = p.entries();
-                let column = |f: &(dyn Fn(usize, &Entry) -> u64 + Sync)| {
-                    parallel::map_collect(entries.len(), |i| F64(f(i, &entries[i])))
+                let column = |f: &dyn Fn(usize, &Entry) -> u64| -> Vec<F64> {
+                    (entries.iter().enumerate()).map(|(i, e)| F64(f(i, e))).collect()
                 };
                 vec![
                     // An illegal entry's tag is zero, which is no table's: nothing can read it.
-                    parallel::map_collect(entries.len(), |i| {
-                        TableId::of(entries[i].class).map_or(F64::ZERO, TableId::tag)
-                    }),
+                    column(&|_, e| TableId::of(e.class).map_or(0, |t| t.tag().0)),
                     column(&|_, e| e.flags),
                     column(&|_, e| e.a1 as u64),
                     column(&|_, e| e.a2 as u64),
diff --git a/crates/leanvm_core/src/cpu/program.rs b/crates/leanvm_core/src/cpu/program.rs
index 90ea0929f..3d00b5311 100644
--- a/crates/leanvm_core/src/cpu/program.rs
+++ b/crates/leanvm_core/src/cpu/program.rs
@@ -377,6 +377,7 @@ impl Program {
     #[doc(hidden)]
     #[tracing::instrument(name = "Verify core", skip_all)]
     pub fn verify_core(&self, output: Output, proof: &Proof) -> Result<DeferredClaims, CpuError> {
+        let _portable = primitives::portable::enter();
         if proof.is_zero_knowledge() {
             let vs = VerifierState::new(&self.zk_session(), output.words(), &proof.0);
             return zero_knowledge::verify_core(self, output, vs).map(|(_, claims)| claims);
@@ -390,6 +391,9 @@ impl Program {
     ///
     /// A recursive verifier of the proof hashes those openings rather than decoding the hints again.
     ///
+    /// It is an aggregator's replay of a leaf it is handed: it feeds the aggregator's proof, which its own verifier
+    /// checks, and nobody's trust, so it runs on the prover's kernels.
+    ///
     /// # Errors
     ///
     /// Returns the first stage that refuses the proof.
@@ -397,14 +401,14 @@ impl Program {
     #[doc(hidden)]
     pub fn verify_recording(&self, output: Output, proof: &Proof) -> Result<Vec<Openings>, VerifyError> {
         if proof.is_zero_knowledge() {
-            let recording = Recording::new(VerifierState::new(&self.zk_session(), output.words(), &proof.0));
+            let recording = Recording::new(VerifierState::native(&self.zk_session(), output.words(), &proof.0));
             let (recording, claims) = zero_knowledge::verify_core(self, output, recording)?;
-            self.check_deferred(&claims)?;
+            self.settle(&mut Native, &claims)?;
             return Ok(recording.into_openings());
         }
-        let mut recording = Recording::new(VerifierState::new(&self.session(), output.words(), &proof.0));
+        let mut recording = Recording::new(VerifierState::native(&self.session(), output.words(), &proof.0));
         let claims = self.core(output, &mut recording)?;
-        self.check_deferred(&claims)?;
+        self.settle(&mut Native, &claims)?;
         Ok(recording.into_openings())
     }
 
@@ -483,7 +487,9 @@ impl Program {
     /// The digest of `rv`'s public statement.
     ///
     /// Every variable-length part is length-framed, so the preimage parses one way.
+    /// The verifier checks a proof against it, so it is computed as the verifier computes (`primitives::portable`).
     fn digest_of(rv: &RiscvProgram) -> [u8; 32] {
+        let _portable = primitives::portable::enter();
         let bytes = |words: &[u64]| -> Vec<u8> { words.iter().flat_map(|w| w.to_le_bytes()).collect() };
         let table = Lookup::Bytecode.table(rv);
         let table_bytes: Vec<u8> = table.iter().flat_map(|w| w.0.to_le_bytes()).collect();
@@ -570,6 +576,7 @@ mod tests {
     use crate::bus::Coord;
     use crate::bus::tests::unmatched_leaves;
     use crate::commitment::Rate;
+    use crate::cpu::Prover;
     use crate::cpu::execute::Row;
     use crate::cpu::filler::JUMP;
     use crate::cpu::layout::{Framework, Shared};
@@ -764,6 +771,22 @@ mod tests {
         );
     }
 
+    /// The public verifier is the portable one: in a portable section it verifies, where the prover's replay on
+    /// `Native` reaches a kernel the guard refuses (when the build arms it, as the workspace's tests do).
+    #[test]
+    fn the_public_verifier_is_the_portable_one() {
+        let text = Asm::new().i(Addi, Reg::A0, Reg::ZERO, 5).exit().finish();
+        let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program");
+        let run = Prover::new(Rate::MIN).prove(&program, &[]).expect("the run halts");
+        let _portable = primitives::portable::enter();
+        program.verify(run.output, &run.proof).expect("an honest proof");
+        if primitives::portable::GUARDED {
+            let replay =
+                std::panic::catch_unwind(AssertUnwindSafe(|| program.verify_recording(run.output, &run.proof)));
+            assert!(replay.is_err(), "the prover's replay ran in a portable section");
+        }
+    }
+
     #[test]
     fn a_run_too_long_for_one_proof_is_refused_while_it_runs() {
         // Fibonacci for 2^63 steps: only the cycle cap would stop it, after 2^35 rows.
diff --git a/crates/leanvm_core/src/cpu/zero_knowledge.rs b/crates/leanvm_core/src/cpu/zero_knowledge.rs
index e1c1f8ca3..53fc98412 100644
--- a/crates/leanvm_core/src/cpu/zero_knowledge.rs
+++ b/crates/leanvm_core/src/cpu/zero_knowledge.rs
@@ -37,7 +37,7 @@ use crate::bus::{self, N_TUPLE_BITS, PublicColumns, SparseColumn};
 use crate::commitment::{Commitment, Committed, Rate};
 use crate::constraints::ConstraintError;
 use crate::tables::{CircuitId, Clock, N_CIRCUITS};
-use fiat_shamir::arith::{Arith, Verifier};
+use fiat_shamir::arith::{Arith, Native, Verifier};
 use fiat_shamir::{ProofTranscript, ProverState, VerifierState};
 use flock::FlockError;
 use flock::lincheck::{LincheckError, MatrixForm};
@@ -109,6 +109,8 @@ pub(super) fn prove(program: &Program, mut w: Witness, output: Output, rate: Rat
 
 /// The prover's replay of its own proof so far, through the verifier's recorder: the recorder, and the core it recorded.
 ///
+/// It feeds the prover's own proof and nobody's trust, so it runs on the prover's kernels.
+///
 /// # Panics
 ///
 /// Panics if the prover's own proof is refused.
@@ -116,8 +118,8 @@ fn replay<'p>(
     program: &Program,
     output: Output,
     proof: &'p ProofTranscript,
-) -> (Recorder<VerifierState<'p>>, RecordedCore<Hash, F192>) {
-    let mut rec = Recorder::new(VerifierState::new(&program.zk_session(), output.words(), proof));
+) -> (Recorder<VerifierState<'p, Native>>, RecordedCore<Hash, F192>) {
+    let mut rec = Recorder::new(VerifierState::native(&program.zk_session(), output.words(), proof));
     let core = record_proof(program, &mut rec, output).expect("the prover's own proof verifies");
     (rec, core)
 }
@@ -218,8 +220,14 @@ impl PublicEvaluations {
         let kbc = crate::log2_strict_usize(rv.entries().len());
         let (chi, alphas) = bytecode.split_at(kbc);
         let weights = bus::fingerprint_weights(alphas);
-        let twist_terms = bus::producer_twist_terms(&Lookup::Bytecode.tuple(rv), &weights, chi, point.twist.len());
-        let image = SparseColumn::new(rv.log_ram(), &[(0, rv.image())]).eval(&image_point);
+        let twist_terms = bus::producer_twist_terms(
+            &mut Native,
+            &Lookup::Bytecode.tuple(rv),
+            &weights,
+            chi,
+            point.twist.len(),
+        );
+        let image = SparseColumn::new(rv.log_ram(), &[(0, rv.image())]).eval(&mut Native, &image_point);
         let slice_weights = (CircuitId::ALL.into_iter().zip(&claims.circuits))
             .map(|(f, c)| {
                 // The weights depend on the slices' count, not their values.
diff --git a/crates/leanvm_core/src/rec/circuit.rs b/crates/leanvm_core/src/rec/circuit.rs
index 84386c9f2..d64d69a78 100644
--- a/crates/leanvm_core/src/rec/circuit.rs
+++ b/crates/leanvm_core/src/rec/circuit.rs
@@ -18,7 +18,7 @@ use super::table::{PerRecTable, Table};
 use crate::rv::{Hash, InstructionClass};
 use fiat_shamir::arith::Arith;
 use primitives::field::{F64, F192};
-use primitives::hash::ChainingValue;
+use primitives::hash::{ChainingValue, portable};
 use std::collections::HashMap;
 use std::hash::{BuildHasherDefault, Hasher};
 use thiserror::Error;
@@ -349,6 +349,16 @@ impl Compression {
         }
         .eval()
     }
+
+    /// The output chaining value by the portable compression, which the native verifier runs.
+    pub(crate) fn output_portable(&self) -> Limbs {
+        let i = &self.0;
+        // Each word of `h` and `m` as its two 32-bit halves, low first.
+        let mut h: [u32; 8] = std::array::from_fn(|k| (i[2 + k / 2] >> (32 * (k % 2))) as u32);
+        let m: [u32; 16] = std::array::from_fn(|k| (i[6 + k / 2] >> (32 * (k % 2))) as u32);
+        portable::compress(&mut h, &m, i[0], i[1] == Hash::FINAL);
+        words(h)
+    }
 }
 
 /// The chaining value after `n` zero blocks from the parameter IV, as four words.
@@ -356,7 +366,8 @@ pub fn zero_prefix(n: usize) -> Limbs {
     words(ChainingValue::zero_prefix(n).state())
 }
 
-/// The BLAKE2s hash of the little-endian bytes of `words`, eight words a block.
+/// The BLAKE2s hash of the little-endian bytes of `words`, eight words a block, by the portable compression: both
+/// sides compute it, the native verifier included.
 ///
 /// The last block is zero padded and its counter is the message's length in bytes.
 /// So the length is hashed: appending zero words changes the digest.
@@ -366,7 +377,7 @@ pub fn chain(words: &[u64]) -> Limbs {
     (0..n_blocks).fold(PARAM_IV, |h, j| {
         // The final block retains the message's words and zero-pads its unused slots.
         let m = std::array::from_fn(|k| words.get(8 * j + k).copied().unwrap_or(0));
-        Compression::new(h, m, (64 * (j as u64 + 1)).min(bytes), j + 1 == n_blocks).output()
+        Compression::new(h, m, (64 * (j as u64 + 1)).min(bytes), j + 1 == n_blocks).output_portable()
     })
 }
 
diff --git a/crates/leanvm_core/src/rec/proof.rs b/crates/leanvm_core/src/rec/proof.rs
index 5e3e1a3ca..c1f2814b6 100644
--- a/crates/leanvm_core/src/rec/proof.rs
+++ b/crates/leanvm_core/src/rec/proof.rs
@@ -236,10 +236,29 @@ impl CircuitKey {
         ps.into_proof()
     }
 
+    /// Verify a proof of the circuit on the native verifier: portable and single-threaded, as a tree's root is checked.
+    ///
+    /// # Errors
+    ///
+    /// Returns the first check that refuses the proof.
+    pub(crate) fn verify_public(
+        &self,
+        statement: &[Limbs],
+        session: &SessionId,
+        rate: Rate,
+        proof: &ProofTranscript,
+    ) -> Result<(), RecError> {
+        let instance = LengthPrefixed(statement.as_flattened());
+        self.verify_after(statement, &mut VerifierState::new(session, &instance, proof), rate)
+    }
+
     /// Verify a proof of the circuit, returning every opening it authenticated.
     ///
     /// A recursive verifier of the proof hashes those openings rather than decoding the hints again.
     ///
+    /// It is a prover's replay of a child it is handed, which feeds its own proof and nobody's trust, so it runs on
+    /// the prover's kernels.
+    ///
     /// # Errors
     ///
     /// Returns the first check that refuses the proof.
@@ -251,26 +270,29 @@ impl CircuitKey {
         proof: &ProofTranscript,
     ) -> Result<Vec<Openings>, RecError> {
         let instance = LengthPrefixed(statement.as_flattened());
-        self.verify_after(statement, VerifierState::new(session, &instance, proof), rate)
+        let mut v = Recording::new(VerifierState::native(session, &instance, proof));
+        self.verify_after(statement, &mut v, rate)?;
+        Ok(v.into_openings())
     }
 
-    /// Verify a proof over a transcript that has absorbed its instance.
-    fn verify_after(
+    /// Verify a proof read by `v`, whose transcript has absorbed its instance, against `statement`.
+    fn verify_after<V: OpeningVerifier<E = F192> + PublicColumns>(
         &self,
         statement: &[Limbs],
-        transcript: VerifierState<'_>,
+        v: &mut V,
         rate: Rate,
-    ) -> Result<Vec<Openings>, RecError> {
+    ) -> Result<(), RecError> {
         if statement.len() != self.circuit.statement_len {
             return Err(RecError::StatementLength {
                 expected: self.circuit.statement_len,
                 got: statement.len(),
             });
         }
-        let mut v = Recording::new(transcript);
-        let matrices = TableArgument::of(&self.fixed, statement, &self.layout).verify_core(&mut v, rate)?;
-        matrices.check(hash::CIRCUIT.circuit()).map_err(FlockError::Lincheck)?;
-        Ok(v.into_openings())
+        let matrices = TableArgument::of(&self.fixed, statement, &self.layout).verify_core(v, rate)?;
+        matrices
+            .check(v, hash::CIRCUIT.circuit())
+            .map_err(FlockError::Lincheck)?;
+        Ok(())
     }
 }
 
@@ -295,8 +317,10 @@ mod tests {
         key(circuit).prove(a, &session(), Rate::MIN)
     }
 
+    /// The native verifier's run: portable, in a portable section.
     fn verify_run(circuit: &Circuit, statement: &[Limbs], proof: &ProofTranscript) -> Result<(), RecError> {
-        key(circuit).verify(statement, &session(), Rate::MIN, proof).map(drop)
+        let _portable = primitives::portable::enter();
+        key(circuit).verify_public(statement, &session(), Rate::MIN, proof)
     }
 
     // Verify a proof whose transcript absorbed `absorbed` as its instance, in place of the statement.
@@ -307,8 +331,8 @@ mod tests {
         proof: &ProofTranscript,
     ) -> Result<(), RecError> {
         let instance = LengthPrefixed(absorbed.as_flattened());
-        let transcript = VerifierState::new(&session(), &instance, proof);
-        key(circuit).verify_after(statement, transcript, Rate::MIN).map(drop)
+        let mut transcript = VerifierState::new(&session(), &instance, proof);
+        key(circuit).verify_after(statement, &mut transcript, Rate::MIN)
     }
 
     // Wires of the every-kind circuit a test forges.
diff --git a/crates/leanvm_core/src/rec/tree/mod.rs b/crates/leanvm_core/src/rec/tree/mod.rs
index 783caab7c..02b538e5d 100644
--- a/crates/leanvm_core/src/rec/tree/mod.rs
+++ b/crates/leanvm_core/src/rec/tree/mod.rs
@@ -37,9 +37,9 @@ use crate::rec::table::{PerRecTable, Table};
 use crate::rec::transcript::ProofSource;
 use crate::tables::CircuitId;
 use design::{ChildWitness, Design, LARGE, LeafWitness, Level, NodeInputs, NodeRows, SMALL};
+use fiat_shamir::arith::{Arith, Portable};
 use pcs::merkle::Openings;
-use primitives::field::{F64, F192};
-use primitives::multilinear::{eq_table, mle_eval_par};
+use primitives::field::F64;
 use reduce::DenseTables;
 use statement::TreeStatement;
 use thiserror::Error;
@@ -729,6 +729,7 @@ impl<'p> Tree<'p> {
     /// A tree of outputs only. Returns the first check that refuses.
     #[tracing::instrument(name = "Verify tree", skip_all)]
     pub fn verify(&self, root: &TreeProof, outputs: &[Output]) -> Result<(), TreeError> {
+        let _portable = primitives::portable::enter();
         self.outputs()?;
         let d = &self.design;
         self.check_rate(root)?;
@@ -741,7 +742,7 @@ impl<'p> Tree<'p> {
             });
         }
         let position = self.known(root)?;
-        self.read(root, position).map_err(TreeError::Root)?;
+        self.check(root, position).map_err(TreeError::Root)?;
         let statement = root.statement(d.statement);
         if statement.digest_words() != self.digest(outputs) {
             return Err(TreeError::Outputs);
@@ -760,12 +761,13 @@ impl<'p> Tree<'p> {
     /// A tree of outputs. Otherwise the first check that refuses.
     #[tracing::instrument(name = "Verify claim-set tree", skip_all)]
     pub fn verify_claims(&self, root: &TreeProof, claims: &ClaimSet) -> Result<(), TreeError> {
+        let _portable = primitives::portable::enter();
         let capacity = self.capacity()?;
         let d = &self.design;
         self.check_rate(root)?;
         let position = self.known(root)?;
         claims.check(capacity).map_err(TreeError::ClaimSet)?;
-        self.read(root, position).map_err(TreeError::Root)?;
+        self.check(root, position).map_err(TreeError::Root)?;
         let statement = root.statement(d.statement);
         if statement.digest_words() != claims.digest() {
             return Err(TreeError::Claims);
@@ -784,9 +786,18 @@ impl<'p> Tree<'p> {
         level[0]
     }
 
+    /// Verify a tree proof's recursion proof on the native verifier, short of its claims; the proof is of the tree's
+    /// circuit at `position`.
+    fn check(&self, p: &TreeProof, position: usize) -> Result<(), VerifyError> {
+        self.keys[position]
+            .verify_public(&p.limbs(), &self.design.session(), self.design.rate, &p.proof)
+            .map_err(Into::into)
+    }
+
     /// Verify a tree proof's recursion proof, short of its claims, returning every opening it authenticated.
     ///
-    /// The proof is of the tree's circuit at `position`.
+    /// The proof is of the tree's circuit at `position`. It is a node's prover's replay of a child, so it runs on the
+    /// prover's kernels.
     fn read(&self, p: &TreeProof, position: usize) -> Result<Vec<Openings>, VerifyError> {
         self.keys[position]
             .verify(&p.limbs(), &self.design.session(), self.design.rate, &p.proof)
@@ -811,6 +822,7 @@ impl<'p> Tree<'p> {
     /// Evaluate every claim a root's statement carries.
     #[tracing::instrument(name = "Settle claims", skip_all)]
     fn settle(&self, s: &TreeStatement, position: usize) -> Result<(), TreeError> {
+        let a = &mut Portable;
         let vars = &self.design.vars.0;
         for &poly in self.design.statement.polys() {
             // A first-level node reduces no claim on a fixed polynomial.
@@ -818,27 +830,24 @@ impl<'p> Tree<'p> {
                 continue;
             }
             let point = &s.dense_point()[..vars[poly as usize]];
-            if mle_eval_par(&self.tables.0[poly as usize], point) != s.dense_value(poly) {
+            if a.public_mle(&self.tables.0[poly as usize], point) != s.dense_value(poly) {
                 return Err(TreeError::Claim(FalseClaim::Dense(poly)));
             }
         }
-        let held = parallel::map_collect(CircuitId::ALL.len(), |f| {
-            let f = CircuitId::ALL[f];
+        for f in CircuitId::ALL {
             let circuit = f.circuit();
             let k = circuit.k_log();
-            let (ra, rb) = circuit.row_values(&eq_table(&s.cols()[..k]));
-            let u = eq_table(&s.rows()[..k]);
-            let dot = |r: &[F192]| u.iter().zip(r).fold(F192::ZERO, |acc, (&x, &y)| acc + x * y);
-            [dot(&ra), dot(&rb)] == s.matrices(f)
-        });
-        (CircuitId::ALL.into_iter().zip(held))
-            .find(|&(_, h)| !h)
-            .map_or(Ok(()), |(f, _)| {
-                Err(TreeError::Claim(FalseClaim::Matrix {
+            let cols = a.eq_table(&s.cols()[..k]);
+            let (ra, rb) = circuit.row_values(&cols);
+            let u = a.eq_table(&s.rows()[..k]);
+            if [a.dot(&u, &ra), a.dot(&u, &rb)] != s.matrices(f) {
+                return Err(TreeError::Claim(FalseClaim::Matrix {
                     table: f.table().name(),
                     part: f.part(),
-                }))
-            })
+                }));
+            }
+        }
+        Ok(())
     }
 
     /// What the circuit of one kind of node costs: of a claim-set tree's nodes, the one of the largest arity.
@@ -883,6 +892,7 @@ mod tests {
     use crate::rv::asm::*;
     use crate::tables::TableId;
     use fiat_shamir::ProofTranscript;
+    use primitives::field::F192;
     use std::sync::OnceLock;
     use zk::Randomness;
 
@@ -1197,7 +1207,7 @@ mod tests {
             rate: d.rate,
         };
         assert!(
-            f.tree.read(&child, 0).is_err(),
+            f.tree.check(&child, 0).is_err(),
             "natively, the fake is no first-level node"
         );
         let limbs = child.limbs();
@@ -1250,7 +1260,7 @@ mod tests {
             f.tree.keys[1].prove(&assignment, &d.session(), d.rate),
             d.rate,
         );
-        f.tree.read(&root, 1).expect("the root's recursion proof verifies");
+        f.tree.check(&root, 1).expect("the root's recursion proof verifies");
         assert_eq!(
             f.tree.verify(&root, &outputs),
             Err(TreeError::Claim(FalseClaim::Dense(DensePoly::Fixed)))
@@ -1446,6 +1456,8 @@ mod tests {
         use crate::rec::tree::*;
         use crate::rv::Region;
         use crate::rv::asm::*;
+        use primitives::field::F192;
+        use primitives::multilinear::mle_eval_par;
         use std::sync::LazyLock;
 
         // A program whose output is its four advice words, after a loop of `rounds` that reads every framework block: a leaf
@@ -2304,7 +2316,7 @@ mod tests {
                 d.rate,
             );
             assert!(
-                t.tree.read(&child, large).is_err(),
+                t.tree.check(&child, large).is_err(),
                 "natively, the fake is no large node"
             );
             let limbs = child.limbs();
@@ -2343,7 +2355,7 @@ mod tests {
                 t.tree.keys[wrap].prove(&assignment, &d.session(), d.rate),
                 d.rate,
             );
-            t.tree.read(&root, wrap).expect("the wrap's recursion proof verifies");
+            t.tree.check(&root, wrap).expect("the wrap's recursion proof verifies");
             assert_eq!(
                 t.tree.verify_claims(&root, &forged_set),
                 Err(TreeError::Claim(FalseClaim::Dense(DensePoly::Wide)))
diff --git a/crates/leanvm_core/src/rec/tree/multiset.rs b/crates/leanvm_core/src/rec/tree/multiset.rs
index b23a2c16f..64bfaadb6 100644
--- a/crates/leanvm_core/src/rec/tree/multiset.rs
+++ b/crates/leanvm_core/src/rec/tree/multiset.rs
@@ -204,14 +204,15 @@ impl ClaimSet {
         items
     }
 
-    /// Its digest: the chain of its blocks' compressions.
+    /// Its digest: the chain of its blocks' compressions, by the portable compression: both sides compute it, the
+    /// native verifier included.
     #[must_use]
     pub fn digest(&self) -> [u64; 4] {
         let items = self.items();
         let last = items.len() - 1;
         (items.iter().enumerate()).fold(PARAM_IV, |h: Limbs, (i, item)| {
             let t = item.code | if i == 0 { code::START } else { 0 };
-            Compression::new(h, item.block, t, i == last).output()
+            Compression::new(h, item.block, t, i == last).output_portable()
         })
     }
 
diff --git a/crates/leanvm_core/src/rec/tree/reduce/matrix.rs b/crates/leanvm_core/src/rec/tree/reduce/matrix.rs
index faecda579..7d9105b3b 100644
--- a/crates/leanvm_core/src/rec/tree/reduce/matrix.rs
+++ b/crates/leanvm_core/src/rec/tree/reduce/matrix.rs
@@ -477,6 +477,7 @@ mod tests {
     use crate::rec::hash;
     use crate::rec::tree::reduce;
 
+    use fiat_shamir::arith::Portable;
     use fiat_shamir::{ProverState, SessionId, VerifierState};
     use primitives::test_util::Rng;
 
@@ -500,7 +501,7 @@ mod tests {
                 r_inner_rest: r[..k - k_skip].to_vec(),
                 s_hat_v: rng.ext_vec(1 << k_skip),
             };
-            let value = form.evaluate(circuit);
+            let value = form.evaluate(&mut Portable, circuit);
             claims.push(MatrixClaim::fresh(f, &Claim { point: form, value }));
             if i == 0 {
                 continue;
diff --git a/crates/leanvm_core/src/rec/verifier/mod.rs b/crates/leanvm_core/src/rec/verifier/mod.rs
index 71edc3b93..3f95eb4d3 100644
--- a/crates/leanvm_core/src/rec/verifier/mod.rs
+++ b/crates/leanvm_core/src/rec/verifier/mod.rs
@@ -252,6 +252,7 @@ mod tests {
     use crate::rec::transcript::{ProofSource, Transcript};
 
     use crate::stacking::StackShape;
+    use fiat_shamir::arith::Portable;
     use fiat_shamir::{Encoding, FromNarg, ProofTranscript, ProverState, SessionId, VerifierState};
     use flock::BatchRows;
     use flock::FlockError;
@@ -431,7 +432,7 @@ mod tests {
         let replays = native(&proof).expect("an honest batch");
         for (batch, replay) in batches.iter().zip(&replays) {
             assert_eq!(
-                replay.matrices.form.evaluate(batch.block.circuit),
+                replay.matrices.form.evaluate(&mut Portable, batch.block.circuit),
                 replay.matrices.value
             );
         }
@@ -503,7 +504,7 @@ mod tests {
             let moved = native(&forged).expect("the batch's identity holds");
             for (f, replay) in moved.iter().enumerate() {
                 let matrices = &replay.matrices;
-                let settles = matrices.form.evaluate(batches[f].block.circuit) == matrices.value;
+                let settles = matrices.form.evaluate(&mut Portable, batches[f].block.circuit) == matrices.value;
                 assert_eq!(settles, f > 1, "circuit {f}'s moved claim");
             }
         }
@@ -667,7 +668,7 @@ mod tests {
             .expect("the committed witness");
         let proof = ps.into_proof();
         let native = |slots: &[StackClaim], rings: &[RingSwitch], proof: &ProofTranscript| {
-            let mut v = Recording::new(VerifierState::new(&SessionId::new(LABEL), &0u64, proof));
+            let mut v = Recording::new(VerifierState::native(&SessionId::new(LABEL), &0u64, proof));
             let commitment = Commitment::read(&mut v, shape, rate).expect("a root");
             commitment.verify(&mut v, slots, rings)?;
             v.transcript()
diff --git a/crates/leanvm_core/src/rec/verifier/recursion.rs b/crates/leanvm_core/src/rec/verifier/recursion.rs
index b2e1e2349..82274d2f5 100644
--- a/crates/leanvm_core/src/rec/verifier/recursion.rs
+++ b/crates/leanvm_core/src/rec/verifier/recursion.rs
@@ -192,6 +192,7 @@ mod tests {
     use crate::rec::transcript::ProofSource;
 
     use fiat_shamir::SessionId;
+    use fiat_shamir::arith::Portable;
 
     use primitives::field::F192;
 
@@ -243,7 +244,7 @@ mod tests {
         let (b, rows) = recursion_rows(&circuit, a.statement(), columns, ProofSource::Proof(&proof, &openings));
         let form = rows.matrix.point.map(|w| b.e(w));
         assert_eq!(
-            form.evaluate(hash::CIRCUIT.circuit()),
+            form.evaluate(&mut Portable, hash::CIRCUIT.circuit()),
             b.e(rows.matrix.value),
             "the hash rows' matrix claim settles"
         );
diff --git a/crates/leanvm_core/src/rv/semantics/alu.rs b/crates/leanvm_core/src/rv/semantics/alu.rs
index ceb63f87e..855efba8e 100644
--- a/crates/leanvm_core/src/rv/semantics/alu.rs
+++ b/crates/leanvm_core/src/rv/semantics/alu.rs
@@ -359,6 +359,7 @@ mod tests {
     use crate::rv::semantics::tests::{
         EDGES, Ports, circuit_matches_reference, edge_word, grid, word_witness_is_the_walk,
     };
+    use fiat_shamir::arith::Portable;
     use fiat_shamir::{ProverState, SessionId, VerifierState};
     use flock::BatchRows;
     use flock::reduction;
@@ -455,7 +456,7 @@ mod tests {
             let proof = ps.into_proof();
             let mut vs = VerifierState::new(&SessionId::new(LABEL), &0u64, &proof);
             reduction::verify(&[(block.shape(), n_log)], &mut vs)
-                .is_ok_and(|r| r[0].claim == claims[0] && r[0].matrices.check(block.circuit).is_ok())
+                .is_ok_and(|r| r[0].claim == claims[0] && r[0].matrices.check(&mut Portable, block.circuit).is_ok())
                 && vs.check_eof().is_ok()
         };
         assert!(accepts(None));
diff --git a/crates/leanvm_core/src/tables/id.rs b/crates/leanvm_core/src/tables/id.rs
index 1fe66750b..c20713a2c 100644
--- a/crates/leanvm_core/src/tables/id.rs
+++ b/crates/leanvm_core/src/tables/id.rs
@@ -79,8 +79,10 @@ impl TableId {
     /// The tags are distinct: `g` has order `2^64 - 1`, far above the table count.
     ///
     /// An illegal entry's tag is zero, which is no table's.
-    pub fn tag(self) -> F64 {
-        F64::G.pow(self.index() as u64)
+    ///
+    /// Computed by the portable products, since the verifier's layout computes it too.
+    pub const fn tag(self) -> F64 {
+        F64::G.pow_portable(self.index() as u64)
     }
 
     /// The table's specification.
diff --git a/crates/parallel/src/lib.rs b/crates/parallel/src/lib.rs
index bac0f6533..50e712a09 100644
--- a/crates/parallel/src/lib.rs
+++ b/crates/parallel/src/lib.rs
@@ -1,7 +1,7 @@
 //! A fixed-size thread pool for flat data-parallel kernels.
 //!
 //! - Workers claim ranges from one shared counter, which also balances cores of different speeds.
-//! - Dispatches cannot nest.
+//! - Dispatches cannot nest, and a [`serial`] section refuses them.
 //! - A task panic is resumed on the dispatcher after every worker stops.
 
 use std::sync::atomic::{AtomicUsize, Ordering};
@@ -9,7 +9,7 @@ use std::sync::atomic::{AtomicUsize, Ordering};
 mod pool;
 mod topology;
 
-pub use pool::{AlreadyConfigured, for_each_chunk, init, init_with_threads};
+pub use pool::{AlreadyConfigured, Serial, for_each_chunk, init, init_with_threads, serial};
 pub use topology::{Topology, num_threads, topology};
 
 /// Claims per worker that a recommended chunk size aims for.
diff --git a/crates/parallel/src/pool.rs b/crates/parallel/src/pool.rs
index f257729ec..c50e3c901 100644
--- a/crates/parallel/src/pool.rs
+++ b/crates/parallel/src/pool.rs
@@ -8,6 +8,7 @@ use crate::topology::{self, Qos, set_qos};
 use crate::{Topology, for_each, num_threads};
 use std::any::Any;
 use std::cell::{Cell, UnsafeCell};
+use std::marker::PhantomData;
 use std::num::NonZeroUsize;
 use std::ops::Deref;
 use std::panic::{AssertUnwindSafe, catch_unwind, resume_unwind};
@@ -32,8 +33,8 @@ const MAX_CLAIM_BATCH: usize = 1 << 12;
 thread_local! {
     /// The running thread's worker index: 0 for the dispatcher, `1..` for the pool's threads.
     static WORKER_ID: Cell<usize> = const { Cell::new(0) };
-    /// Whether the running thread is inside a pool task, where a dispatch would deadlock.
-    static IN_TASK: Cell<bool> = const { Cell::new(false) };
+    /// Why a dispatch from this thread would be a bug, if it would: set inside a pool task and inside [`serial`].
+    static REFUSED: Cell<Option<&'static str>> = const { Cell::new(None) };
 }
 
 /// The running thread's worker index, below the thread count and unique among live workers.
@@ -41,6 +42,33 @@ pub(crate) fn worker_id() -> usize {
     WORKER_ID.get()
 }
 
+/// Refuse every dispatch from this thread while the returned guard lives: one panics, whatever the pool's size.
+///
+/// The native verifier holds one, so that a dispatch it reaches fails every test that verifies a proof, rather than
+/// only those whose sizes cross a kernel's threshold or whose pool has more than one worker.
+#[must_use = "dispatch is refused only while the guard lives"]
+pub fn serial() -> Serial {
+    let previous = REFUSED.get();
+    REFUSED.set(Some(previous.unwrap_or("parallel dispatch inside a serial section")));
+    Serial {
+        previous,
+        _thread: PhantomData,
+    }
+}
+
+/// A [`serial`] section: dropping it restores the previous refusal, on return and on unwinding alike.
+pub struct Serial {
+    previous: Option<&'static str>,
+    /// The refusal is this thread's, so the guard stays on it.
+    _thread: PhantomData<*const ()>,
+}
+
+impl Drop for Serial {
+    fn drop(&mut self) {
+        REFUSED.set(self.previous);
+    }
+}
+
 /// A type-erased work unit. The `&dyn Fn`'s lifetime is erased to `'static`; it
 /// is dereferenced only inside a dispatch window during which the dispatcher
 /// blocks, so the borrow outlives every call. Range-based (`f(start, end)`) so a
@@ -233,7 +261,7 @@ fn drain(pool: &Pool) {
     let f = unsafe { job.f.as_ref() };
     let task_count = job.n_tasks;
     let worker_count = num_threads();
-    IN_TASK.set(true); // catches nested dispatch; see `for_each_chunk`
+    REFUSED.set(Some("nested parallel dispatch from inside a pool task")); // see `for_each_chunk`
     // Catch a task panic so it cannot unwind across `worker_main` (skipping the
     // `entered` decrement and hanging the join) or poison the dispatch lock.
     let result = catch_unwind(AssertUnwindSafe(|| {
@@ -252,7 +280,7 @@ fn drain(pool: &Pool) {
             f(start, (start + batch).min(task_count));
         }
     }));
-    IN_TASK.set(false);
+    REFUSED.set(None);
     if let Err(payload) = result {
         pool.panic.lock().unwrap().get_or_insert(payload); // keep the first
     }
@@ -268,9 +296,11 @@ fn drain(pool: &Pool) {
 /// # Panics
 /// If called from inside a pool task: that would deadlock on the dispatch lock, so
 /// it panics rather than silently serializing. Fan out over the outermost
-/// independent unit and keep the levels below it sequential.
+/// independent unit and keep the levels below it sequential. Also if called inside [`serial`].
 pub fn for_each_chunk<F: Fn(usize, usize) + Sync>(n_tasks: usize, f: F) {
-    assert!(!IN_TASK.get(), "nested parallel dispatch from inside a pool task");
+    if let Some(why) = REFUSED.get() {
+        panic!("{why}");
+    }
 
     let worker_count = num_threads();
     if worker_count <= 1 || n_tasks <= 1 {
diff --git a/crates/parallel/tests/pool.rs b/crates/parallel/tests/pool.rs
index 573a4c443..33bb42832 100644
--- a/crates/parallel/tests/pool.rs
+++ b/crates/parallel/tests/pool.rs
@@ -205,6 +205,26 @@ fn nested_dispatch_panics_rather_than_deadlocking() {
     });
 }
 
+/// A serial section refuses even a dispatch the pool would run inline, so a stray one fails on any pool and size.
+#[test]
+#[should_panic = "parallel dispatch inside a serial section"]
+fn a_serial_section_refuses_every_dispatch() {
+    let _serial = parallel::serial();
+    parallel::for_each(1, |_| {});
+}
+
+#[test]
+fn a_serial_section_ends_with_its_guard() {
+    assert!(
+        std::panic::catch_unwind(|| {
+            let _serial = parallel::serial();
+            panic!("inside");
+        })
+        .is_err()
+    );
+    assert_eq!(parallel::map_collect(scaled(1_000), |i| i).len(), scaled(1_000));
+}
+
 #[test]
 fn find_first_returns_the_global_minimum() {
     for n in SIZES {
diff --git a/crates/pcs/src/merkle.rs b/crates/pcs/src/merkle.rs
index 53a343a42..ce9d5c6e3 100644
--- a/crates/pcs/src/merkle.rs
+++ b/crates/pcs/src/merkle.rs
@@ -23,9 +23,11 @@
 //! - The encoder hands blocks over as it finishes them, so leaves are hashed while the rows are in L2.
 //! - Above the blocks, the last block to finish a unit of nodes climbs it, so no pass waits on a barrier.
 
+use fiat_shamir::Hashing;
+use fiat_shamir::arith::{Native, Portable};
 use parallel::SendPtr;
 use primitives::field::F64;
-use primitives::hash::{BATCH, BLOCK_LEN, ChainingValue, OUT_LEN, hash_many};
+use primitives::hash::{BATCH, BLOCK_LEN, ChainingValue, OUT_LEN, hash_many, portable};
 use std::mem::MaybeUninit;
 use std::sync::OnceLock;
 use std::sync::atomic::{AtomicBool, AtomicUsize, Ordering};
@@ -48,6 +50,63 @@ pub fn hash_pair(left: &Hash, right: &Hash) -> Hash {
     primitives::hash::hash(&buf)
 }
 
+/// How an opening hashes: its rows' leaf digests and its pairs' parents, beside its transcript's [`Hashing`].
+///
+/// The committer's batched kernels ([`Native`]), for a prover replaying a proof it is handed, or the native verifier's
+/// portable code ([`Portable`]), one hash at a time. Both give the same digests.
+pub trait MerkleHashing: Hashing {
+    /// The leaf digest of each `row_bytes` row of `rows` in a `leaf_bytes` image, as the committer hashed it.
+    fn hash_leaves(rows: &[u8], row_bytes: usize, leaf_bytes: usize) -> Vec<Hash>;
+
+    /// Each pair of children's parent, into `parents`.
+    fn hash_pairs(pairs: &[[Hash; 2]], parents: &mut Vec<Hash>);
+}
+
+impl MerkleHashing for Native {
+    fn hash_leaves(rows: &[u8], row_bytes: usize, leaf_bytes: usize) -> Vec<Hash> {
+        let mut hashes = Box::new_uninit_slice(rows.len() / row_bytes);
+        LeafHasher::new(row_bytes, leaf_bytes).hash(rows, &mut hashes);
+        // SAFETY: the hasher wrote one digest per row.
+        unsafe { hashes.assume_init() }.into_vec()
+    }
+
+    fn hash_pairs(pairs: &[[Hash; 2]], parents: &mut Vec<Hash>) {
+        parents.clear();
+        parents.resize(pairs.len(), [0; 32]);
+        hash_many::<{ 2 * OUT_LEN }>(pairs.as_flattened().as_flattened(), parents.as_flattened_mut());
+    }
+}
+
+impl MerkleHashing for Portable {
+    /// The digests `LeafHasher` gives, the image's whole zero blocks again one chaining value.
+    fn hash_leaves(rows: &[u8], row_bytes: usize, leaf_bytes: usize) -> Vec<Hash> {
+        if !leaf_bytes.is_multiple_of(BLOCK_LEN) {
+            let mut image = vec![0u8; leaf_bytes];
+            return (rows.chunks_exact(row_bytes))
+                .map(|row| {
+                    image[leaf_bytes - row_bytes..].copy_from_slice(row);
+                    portable::hash(&image)
+                })
+                .collect();
+        }
+        let zero_blocks = (leaf_bytes - row_bytes) / BLOCK_LEN;
+        let start = ChainingValue::zero_prefix_portable(zero_blocks);
+        let mut image = vec![0u8; leaf_bytes - zero_blocks * BLOCK_LEN];
+        let at = image.len() - row_bytes;
+        (rows.chunks_exact(row_bytes))
+            .map(|row| {
+                image[at..].copy_from_slice(row);
+                start.hash_portable(&image)
+            })
+            .collect()
+    }
+
+    fn hash_pairs(pairs: &[[Hash; 2]], parents: &mut Vec<Hash>) {
+        parents.clear();
+        parents.extend(pairs.iter().map(|pair| portable::hash(pair.as_flattened())));
+    }
+}
+
 /// Bytes of the staging tile for leaves whose zero padding does not end on a hash block boundary.
 const STAGE_TILE_BYTES: usize = 16 << 10;
 
@@ -55,7 +114,8 @@ const STAGE_TILE_BYTES: usize = 16 << 10;
 ///
 /// The image's whole hash blocks of leading zeros are one chaining value, computed once for every leaf.
 ///
-/// The committer and the native verifier hash leaves through it alike.
+/// The committer and a prover's replay hash leaves through it; the native verifier takes the same digests one at a
+/// time (the [`MerkleHashing`] of [`Portable`]).
 pub(crate) struct LeafHasher(LeafShape);
 
 /// The hashing plan for one leaf shape, chosen once.
@@ -490,13 +550,6 @@ const fn digests_as_bytes(out: &mut [MaybeUninit<Hash>]) -> &mut [u8] {
     unsafe { std::slice::from_raw_parts_mut(out.as_mut_ptr().cast(), out.len() * OUT_LEN) }
 }
 
-/// Hash each pair of children into its parent, all pairs together, into `parents`.
-fn hash_pairs(pairs: &[[Hash; 2]], parents: &mut Vec<Hash>) {
-    parents.clear();
-    parents.resize(pairs.len(), [0; 32]);
-    hash_many::<{ 2 * OUT_LEN }>(pairs.as_flattened().as_flattened(), parents.as_flattened_mut());
-}
-
 /// Query positions with duplicates removed, ascending.
 ///
 /// It is the order a phase stores its rows in, and the order its octopus is built and checked against.
@@ -565,7 +618,9 @@ impl PrunedMerklePaths {
     /// # Returns
     ///
     /// Nothing on a wrong row count or width, an out-of-range query, a wrong sibling count, or another root.
-    pub(crate) fn open(
+    ///
+    /// `H` hashes: the native verifier's [`Portable`], or a prover's replay's [`Native`].
+    pub(crate) fn open<H: MerkleHashing>(
         &self,
         root: &Hash,
         num_leaves: usize,
@@ -582,12 +637,9 @@ impl PrunedMerklePaths {
             return None;
         }
 
-        // The rows, one after another, hashed as the committer hashed them: zero prefix shared, leaves batched.
+        // The rows, one after another, hashed as the committer hashed them.
         let bytes: Vec<u8> = self.rows.iter().flat_map(|word| word.0.to_le_bytes()).collect();
-        let mut leaf_hashes = Box::new_uninit_slice(sorted.len());
-        LeafHasher::new(8 * row_words, 8 * leaf_words).hash(&bytes, &mut leaf_hashes);
-        // SAFETY: the hasher wrote one digest per row.
-        let leaf_hashes = unsafe { leaf_hashes.assume_init() };
+        let leaf_hashes = H::hash_leaves(&bytes, 8 * row_words, 8 * leaf_words);
 
         // Rebuild every node on the queried paths bottom-up.
         // A stored sibling is pulled only where it is not itself a queried subtree.
@@ -620,7 +672,7 @@ impl PrunedMerklePaths {
                 known.push((idx | 1, right));
                 i += if paired { 2 } else { 1 };
             }
-            hash_pairs(&pairs, &mut digests);
+            H::hash_pairs(&pairs, &mut digests);
             nodes.clear();
             nodes.extend(parents.iter().copied().zip(digests.iter().copied()));
         }
@@ -887,7 +939,11 @@ mod tests {
         let paths = tree.prune(&queries, |q| rows[q].clone());
         assert_eq!(paths.rows.len(), 3 * width, "one row per distinct query");
 
-        let openings = paths.open(&root, num_leaves, &queries, width, width).expect("open");
+        let openings = paths
+            .open::<Portable>(&root, num_leaves, &queries, width, width)
+            .expect("open");
+        let native = paths.open::<Native>(&root, num_leaves, &queries, width, width);
+        assert_eq!(native.as_ref(), Some(&openings), "both backends open alike");
         assert_eq!(openings.len(), queries.len());
         for (i, &q) in queries.iter().enumerate() {
             assert_eq!(openings.image(i), rows[q], "row must follow query order");
@@ -900,6 +956,19 @@ mod tests {
         }
     }
 
+    #[test]
+    fn the_portable_leaf_digests_are_the_committers() {
+        // Zero prefixes of whole blocks, of none, and of a part of one, rows narrower than a block and wider.
+        for (row_words, leaf_words) in [(4, 4), (3, 8), (8, 16), (5, 13), (20, 24), (1, 64)] {
+            let rows: Vec<u8> = (0..7 * 8 * row_words).map(|i| (i * 37 % 251) as u8).collect();
+            assert_eq!(
+                Portable::hash_leaves(&rows, 8 * row_words, 8 * leaf_words),
+                Native::hash_leaves(&rows, 8 * row_words, 8 * leaf_words),
+                "{row_words} of {leaf_words} words"
+            );
+        }
+    }
+
     #[test]
     fn malformed_phases_are_rejected() {
         let (num_leaves, width) = (8usize, 4usize);
@@ -910,7 +979,7 @@ mod tests {
         let root = tree.root();
         let queries = [5usize, 1, 3];
         let good = tree.prune(&queries, |q| rows[q].clone());
-        let open = |p: &PrunedMerklePaths, qs: &[usize], w: usize, n: usize| p.open(&root, n, qs, w, w);
+        let open = |p: &PrunedMerklePaths, qs: &[usize], w: usize, n: usize| p.open::<Portable>(&root, n, qs, w, w);
         assert!(open(&good, &queries, width, num_leaves).is_some(), "honest phase");
 
         let mut extra = good.clone();
diff --git a/crates/pcs/src/ntt/basis.rs b/crates/pcs/src/ntt/basis.rs
index dfd3b18ff..06f392db8 100644
--- a/crates/pcs/src/ntt/basis.rs
+++ b/crates/pcs/src/ntt/basis.rs
@@ -32,6 +32,8 @@ impl NovelBasis {
     ///
     /// Each normalizer is nonzero: `v_k` lies outside the span of `v_0, ..., v_{k-1}`, where `s_k` vanishes.
     ///
+    /// Computed by the portable products, since the native verifier builds it too.
+    ///
     /// # Panics
     ///
     /// Panics if `log_n > 63`, past the degree of `K`.
@@ -42,7 +44,7 @@ impl NovelBasis {
         let mut rows = Vec::with_capacity(log_n + 1);
         loop {
             // The recurrence on every later basis vector: s_{k+1}(v_j) = s_k(v_j) (s_k(v_j) + s_k(v_k)).
-            let next: Vec<F64> = row[1..].iter().map(|&s| s * (s + row[0])).collect();
+            let next: Vec<F64> = row[1..].iter().map(|&s| s.mul_portable(s + row[0])).collect();
             rows.push(row);
             if next.is_empty() {
                 break;
@@ -51,9 +53,9 @@ impl NovelBasis {
         }
         // Row k's first entry is s_k(v_k): dividing by it normalizes the row.
         let normalizers: Vec<F64> = rows.iter().map(|row| row[0]).collect();
-        let inverses: Vec<F64> = normalizers.iter().map(|s| s.inv()).collect();
+        let inverses: Vec<F64> = normalizers.iter().map(|s| s.inv_portable()).collect();
         for (row, &inverse) in rows.iter_mut().zip(&inverses) {
-            row.iter_mut().for_each(|s| *s *= inverse);
+            row.iter_mut().for_each(|s| *s = s.mul_portable(inverse));
         }
         Self {
             rows,
@@ -95,6 +97,12 @@ impl NovelBasis {
         }
     }
 
+    /// `s'_k(x)` alone, by the recurrence on the portable products, as the native verifier computes it.
+    pub(crate) fn normalized_portable(&self, x: F64, k: usize) -> F64 {
+        let s = (0..k).fold(x, |s, j| s.mul_portable(s + self.normalizers[j]));
+        s.mul_portable(self.inverses[k])
+    }
+
     /// `s_{k+1}(x)` from `s = s_k(x)`, as `s^2 + s_k(v_k) s`.
     ///
     /// The prover, the native verifier and the recursion machine's rows all step through it.
@@ -140,7 +148,7 @@ mod tests {
         // Invariant: every way of reaching `s'_k` gives the same value.
         //
         //     table:       subset sums of the values at the basis vectors
-        //     recurrence:  s_{k+1} = s_k (s_k + s_k(v_k)), natively and through the arithmetic
+        //     recurrence:  s_{k+1} = s_k (s_k + s_k(v_k)), natively, portably and through the arithmetic
         //
         // Fixture state: a 12-variable domain, at points spread over it.
         let basis = NovelBasis::new(12);
@@ -150,6 +158,11 @@ mod tests {
             let mut s = F192::from(F64(point as u64));
             for (k, &want) in normalized.iter().enumerate() {
                 assert_eq!(basis.at_point(k, point), want, "point {point}, k {k}");
+                assert_eq!(
+                    basis.normalized_portable(F64(point as u64), k),
+                    want,
+                    "point {point}, k {k}"
+                );
                 assert_eq!(
                     s.mul_base(basis.inverses()[k]),
                     F192::from(want),
diff --git a/crates/pcs/src/ring_switch.rs b/crates/pcs/src/ring_switch.rs
index a653fbfdd..08c8691e6 100644
--- a/crates/pcs/src/ring_switch.rs
+++ b/crates/pcs/src/ring_switch.rs
@@ -218,6 +218,19 @@ pub(crate) struct RingMap<E> {
     coefficients: Vec<E>,
 }
 
+/// `x^(2^-k)` for each `k < 64`, at compile time: `x^(2^(64 - k))`, since 64 squarings are the identity on `K`.
+static X_ROOTS: [F64; F64::DEGREE] = {
+    let mut roots = [F64::G; F64::DEGREE];
+    let (mut power, mut i) = (F64::G, 1);
+    while i < F64::DEGREE {
+        // `x^(2^i)`, which is `x^(2^-(64 - i))`.
+        power = power.square_portable();
+        roots[F64::DEGREE - i] = power;
+        i += 1;
+    }
+    roots
+};
+
 impl<E: Copy> RingMap<E> {
     /// The map of the six challenges `f_0..f_5`, in drawing order.
     ///
@@ -261,11 +274,9 @@ impl<E: Copy> RingMap<E> {
         assert_eq!(slices.len(), F64::DEGREE, "a family has 64 slices");
         let terms: Vec<E> = (0..F64::DEGREE)
             .map(|k| {
-                // `x^(2^-k) = x^(2^(64 - k))`, since 64 squarings are the identity on `K`.
-                let xk = (0..(F64::DEGREE - k) % F64::DEGREE).fold(F64(2), |x, _| x.square());
                 // `S(x^(2^-k))` by Horner's rule, from the last slice down.
                 let (&last, rest) = slices.split_last().expect("64 slices");
-                let s = (rest.iter().rev()).fold(last, |acc, &sj| a.mul_const_add(acc, F192::from(xk), sj));
+                let s = (rest.iter().rev()).fold(last, |acc, &sj| a.mul_const_add(acc, F192::from(X_ROOTS[k]), sj));
                 a.mul(self.coefficients[k], s)
             })
             .collect();
diff --git a/crates/pcs/src/verifier.rs b/crates/pcs/src/verifier.rs
index 3fabf6e1f..8d37a5010 100644
--- a/crates/pcs/src/verifier.rs
+++ b/crates/pcs/src/verifier.rs
@@ -5,9 +5,9 @@
 //! - Natively a root is a digest, a query an index, and a committed word a `K` value.
 //! - In rows they are the wires holding them, and an opened row is authenticated by hash rows.
 
-use crate::merkle::{Hash, Openings, PrunedMerklePaths, sorted_unique};
+use crate::merkle::{Hash, MerkleHashing, Openings, PrunedMerklePaths, sorted_unique};
 use crate::whir::sample_queries;
-use fiat_shamir::arith::{Arith, Verifier};
+use fiat_shamir::arith::{Arith, Native, Verifier};
 use fiat_shamir::{TranscriptError, VerifierState};
 use primitives::field::{F64, F192};
 
@@ -63,7 +63,7 @@ pub trait OpeningVerifier: Verifier {
     fn query_point(&mut self, query: &Self::Query) -> Self::E;
 }
 
-impl OpeningVerifier for VerifierState<'_> {
+impl<A: Arith<E = F192> + MerkleHashing> OpeningVerifier for VerifierState<'_, A> {
     type Root = Hash;
     type K = F64;
     type Query = usize;
@@ -89,7 +89,7 @@ impl OpeningVerifier for VerifierState<'_> {
     }
 
     fn mul_k_add(&mut self, a: F192, k: F64, d: F192) -> F192 {
-        a.mul_base(k) + d
+        self.mul_const_add(a, F192::from(k), d)
     }
 
     fn e_of_limbs(&mut self, limbs: [F64; 3]) -> F192 {
@@ -102,8 +102,8 @@ impl OpeningVerifier for VerifierState<'_> {
 }
 
 /// Read the next hint as Merkle paths and authenticate them against `root`: each query's opening, in query order.
-fn authenticate(
-    vs: &mut VerifierState<'_>,
+fn authenticate<A: MerkleHashing>(
+    vs: &mut VerifierState<'_, A>,
     root: &Hash,
     depth: usize,
     queries: &[usize],
@@ -114,16 +114,18 @@ fn authenticate(
     let distinct = sorted_unique(queries).len();
     vs.prover_hint_with(|hint| {
         let paths = PrunedMerklePaths::from_hint(hint, distinct, row_words)?;
-        paths.open(root, 1 << depth, queries, row_words, leaf_words)
+        paths.open::<A>(root, 1 << depth, queries, row_words, leaf_words)
     })
 }
 
 /// A native verifier that keeps every opening it authenticates, for a recursive verifier to hash.
 ///
 /// The recursive verifier then reads the openings rather than decoding and hashing the hints again.
+///
+/// Only a prover replays a proof this way, to prove it in turn, so it runs on the prover's kernels.
 pub struct Recording<'a> {
     /// The transcript the proof is read from.
-    vs: VerifierState<'a>,
+    vs: VerifierState<'a, Native>,
     /// Every phase's openings, in transcript order.
     openings: Vec<Openings>,
 }
@@ -131,7 +133,7 @@ pub struct Recording<'a> {
 impl<'a> Recording<'a> {
     /// A recording verifier over a transcript.
     #[must_use]
-    pub const fn new(vs: VerifierState<'a>) -> Self {
+    pub const fn new(vs: VerifierState<'a, Native>) -> Self {
         Self {
             vs,
             openings: Vec::new(),
@@ -139,7 +141,7 @@ impl<'a> Recording<'a> {
     }
 
     /// The transcript the proof is read from.
-    pub const fn transcript(&mut self) -> &mut VerifierState<'a> {
+    pub const fn transcript(&mut self) -> &mut VerifierState<'a, Native> {
         &mut self.vs
     }
 
diff --git a/crates/pcs/src/whir/query.rs b/crates/pcs/src/whir/query.rs
index d62189631..47aae61f8 100644
--- a/crates/pcs/src/whir/query.rs
+++ b/crates/pcs/src/whir/query.rs
@@ -129,11 +129,9 @@ impl Padding {
     /// The padding of lanes of `2^log_msg_cols` words at rate `2^-log_inv_rate`.
     pub(crate) fn new(log_msg_cols: usize, log_inv_rate: usize) -> Self {
         let basis = NovelBasis::new(log_msg_cols);
-        let mut normalized = vec![F64::ZERO; log_msg_cols + 1];
-        basis.normalized_at(F64(1 << (log_msg_cols + log_inv_rate)), &mut normalized);
         Self {
             log_msg_cols,
-            shift: normalized[log_msg_cols],
+            shift: basis.normalized_portable(F64(1 << (log_msg_cols + log_inv_rate)), log_msg_cols),
             basis,
         }
     }
diff --git a/crates/primitives/Cargo.toml b/crates/primitives/Cargo.toml
index 9d3510809..c7ba44ac5 100644
--- a/crates/primitives/Cargo.toml
+++ b/crates/primitives/Cargo.toml
@@ -18,6 +18,9 @@ serde.workspace = true
 # Shared test fixtures (`test_util`) used by this and other crates' tests.
 # Kept off the default build so `rand` stays out of the production graph.
 test-util = ["dep:rand"]
+# The portable verifier's guard: every SIMD or assembly kernel panics inside a `portable::Section`.
+# Enabled by the CLI's tests, so `cargo testall` runs it while no benchmark build pays for its check.
+guard = []
 
 [dev-dependencies]
 primitives = { path = ".", features = ["test-util"] }
diff --git a/crates/primitives/src/field/gf2_64.rs b/crates/primitives/src/field/gf2_64.rs
index c56b9d57f..cafb55fa7 100644
--- a/crates/primitives/src/field/gf2_64.rs
+++ b/crates/primitives/src/field/gf2_64.rs
@@ -19,6 +19,42 @@ pub const R64: u64 = 0x1B;
 #[repr(transparent)]
 pub struct F64(pub u64);
 
+/// `$v` squared `$n` times by `$square`: a macro, so that it is `const` when the square is.
+macro_rules! squarings {
+    ($square:expr, $v:expr, $n:expr) => {{
+        let mut v = $v;
+        let mut i = 0;
+        while i < $n {
+            v = $square(v);
+            i += 1;
+        }
+        v
+    }};
+}
+
+/// `$x^(2^64 - 2)` by Itoh-Tsujii, with the product `$mul` and the square `$square`: a macro, so that it is `const`
+/// when they are.
+///
+/// With `t_k = x^(2^k - 1)`, the inverse is `t_63^2`.
+/// Step `t_(a+b) = t_a^(2^b) * t_b` costs `b` squarings and one multiply.
+/// The addition chain 1, 2, 3, 6, 12, 24, 48, 60, 63 spends 63 squarings and 8 multiplies.
+macro_rules! itoh_tsujii {
+    ($x:expr, $mul:expr, $square:expr) => {{
+        // Each step reads t_k = x^(2^k - 1).
+        let t1 = $x;
+        let t2 = $mul(squarings!($square, t1, 1), t1);
+        let t3 = $mul(squarings!($square, t2, 1), t1);
+        let t6 = $mul(squarings!($square, t3, 3), t3);
+        let t12 = $mul(squarings!($square, t6, 6), t6);
+        let t24 = $mul(squarings!($square, t12, 12), t12);
+        let t48 = $mul(squarings!($square, t24, 24), t24);
+        let t60 = $mul(squarings!($square, t48, 12), t12);
+        let t63 = $mul(squarings!($square, t60, 3), t3);
+        // (x^(2^63 - 1))^2 = x^(2^64 - 2).
+        squarings!($square, t63, 1)
+    }};
+}
+
 impl F64 {
     /// Degree over GF(2), the number of binary coefficients in one element.
     pub const DEGREE: usize = 64;
@@ -78,30 +114,38 @@ impl F64 {
     }
 
     /// Multiplicative inverse `x^(2^64 - 2)`, mapping zero to zero.
-    ///
-    /// Itoh-Tsujii: with `t_k = x^(2^k - 1)`, the inverse is `t_63^2`.
-    /// Step `t_(a+b) = t_a^(2^b) * t_b` costs `b` squarings and one multiply.
-    /// The addition chain 1, 2, 3, 6, 12, 24, 48, 60, 63 spends 63 squarings and 8 multiplies.
     pub fn inv(self) -> Self {
-        // Square `v` a total of `n` times.
-        let sq = |mut v: Self, n: u32| {
-            for _ in 0..n {
-                v = v.square();
+        itoh_tsujii!(self, Mul::mul, Self::square)
+    }
+
+    /// The product, with no SIMD intrinsic or assembly: the verifier's (see [`crate::portable`]).
+    #[inline]
+    pub const fn mul_portable(self, rhs: Self) -> Self {
+        Self(reduce(portable::clmul(self.0, rhs.0)))
+    }
+
+    /// The square, with no SIMD intrinsic or assembly.
+    #[inline]
+    pub const fn square_portable(self) -> Self {
+        Self(reduce(portable::spread(self.0)))
+    }
+
+    /// The inverse, zero for zero, with no SIMD intrinsic or assembly.
+    pub const fn inv_portable(self) -> Self {
+        itoh_tsujii!(self, Self::mul_portable, Self::square_portable)
+    }
+
+    /// `self^exp` by square-and-multiply, with no SIMD intrinsic or assembly.
+    pub const fn pow_portable(self, mut exp: u64) -> Self {
+        let (mut base, mut acc) = (self, Self::ONE);
+        while exp > 0 {
+            if exp & 1 == 1 {
+                acc = acc.mul_portable(base);
             }
-            v
-        };
-        // Each step reads t_k = x^(2^k - 1).
-        let t1 = self;
-        let t2 = sq(t1, 1) * t1;
-        let t3 = sq(t2, 1) * t1;
-        let t6 = sq(t3, 3) * t3;
-        let t12 = sq(t6, 6) * t6;
-        let t24 = sq(t12, 12) * t12;
-        let t48 = sq(t24, 24) * t24;
-        let t60 = sq(t48, 12) * t12;
-        let t63 = sq(t60, 3) * t3;
-        // (x^(2^63 - 1))^2 = x^(2^64 - 2).
-        sq(t63, 1)
+            base = base.square_portable();
+            exp >>= 1;
+        }
+        acc
     }
 }
 
@@ -135,11 +179,13 @@ impl Mul for F64 {
     fn mul(self, rhs: Self) -> Self {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             // SAFETY: aes target feature is enabled at compile time.
             unsafe { aarch64::mul_pmull(self, rhs) }
         }
         #[cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq"))]
         {
+            crate::portable::kernel();
             // SAFETY: pclmulqdq is enabled at compile time.
             unsafe { Self(x86_64::mul(self.0, rhs.0)) }
         }
@@ -148,7 +194,7 @@ impl Mul for F64 {
             all(target_arch = "x86_64", target_feature = "pclmulqdq")
         )))]
         {
-            Self(reduce(mul_wide(self.0, rhs.0)))
+            self.mul_portable(rhs)
         }
     }
 }
@@ -175,11 +221,13 @@ impl MulAssign for F64 {
 pub fn mul_wide(a: u64, b: u64) -> u128 {
     #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
     {
+        crate::portable::kernel();
         // SAFETY: aes is enabled at compile time; the reinterpret is between 128-bit values.
         unsafe { core::mem::transmute::<core::arch::aarch64::uint64x2_t, u128>(aarch64::pmull(a, b)) }
     }
     #[cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq"))]
     {
+        crate::portable::kernel();
         // SAFETY: pclmulqdq is enabled at compile time.
         unsafe { x86_64::clmul(a, b) }
     }
@@ -188,7 +236,7 @@ pub fn mul_wide(a: u64, b: u64) -> u128 {
         all(target_arch = "x86_64", target_feature = "pclmulqdq")
     )))]
     {
-        software::clmul(a, b)
+        portable::clmul(a, b)
     }
 }
 
@@ -200,6 +248,7 @@ pub fn mul_wide(a: u64, b: u64) -> u128 {
 pub(crate) fn square_wide(a: u64) -> u128 {
     #[cfg(all(target_arch = "x86_64", target_feature = "bmi2"))]
     {
+        crate::portable::kernel();
         // SAFETY: bmi2 is enabled at compile time.
         unsafe { x86_64::spread(a) }
     }
@@ -392,19 +441,55 @@ mod x86_64 {
     }
 }
 
-pub mod software {
-    /// Portable 64x64 carry-less product, used by fallback paths and as the reference.
+/// The portable products: integer code with no SIMD intrinsic or assembly, the same on every target.
+pub mod portable {
+    /// The bits `i < 128` with `i % 5 == class`.
+    const fn class(class: u32) -> u128 {
+        let (mut mask, mut bit) = (0, class);
+        while bit < 128 {
+            mask |= 1 << bit;
+            bit += 5;
+        }
+        mask
+    }
+
+    const CLASSES: [u128; 5] = [class(0), class(1), class(2), class(3), class(4)];
+
+    /// The 64x64 carry-less product, by integer products of operands with holes.
+    ///
+    /// Each operand splits into five parts, part `i` its bits at positions `i` modulo 5, at most 13 of them.
+    /// A column of the integer product of two parts then sums at most 13 ones, so its carries stay in the four columns
+    /// above it and never reach the next column of its class: that column's low bit is the XOR of its terms, the
+    /// carry-less product's bit. The products of parts whose classes add to `k` modulo 5 give class `k`.
+    #[inline]
     pub const fn clmul(a: u64, b: u64) -> u128 {
-        let mut acc = 0u128;
-        let mut i = 0;
-        // Schoolbook: XOR in `b * x^i` for every set bit `i` of `a`.
-        while i < 64 {
-            if (a >> i) & 1 != 0 {
-                acc ^= (b as u128) << i;
+        let mut product = 0;
+        let mut k = 0;
+        while k < 5 {
+            let mut sum = 0;
+            let mut i = 0;
+            while i < 5 {
+                sum ^= (a as u128 & CLASSES[i]) * (b as u128 & CLASSES[(k + 5 - i) % 5]);
+                i += 1;
             }
-            i += 1;
+            product |= sum & CLASSES[k];
+            k += 1;
         }
-        acc
+        product
+    }
+
+    /// The carry-less square: bit `i` moves to bit `2i`.
+    pub const fn spread(a: u64) -> u128 {
+        // A 32-bit half's bits onto the even bits of a word, by halving shifts.
+        const fn half(x: u32) -> u64 {
+            let mut x = x as u64;
+            x = (x | x << 16) & 0x0000_FFFF_0000_FFFF;
+            x = (x | x << 8) & 0x00FF_00FF_00FF_00FF;
+            x = (x | x << 4) & 0x0F0F_0F0F_0F0F_0F0F;
+            x = (x | x << 2) & 0x3333_3333_3333_3333;
+            (x | x << 1) & 0x5555_5555_5555_5555
+        }
+        half(a as u32) as u128 | (half((a >> 32) as u32) as u128) << 64
     }
 }
 
@@ -425,9 +510,14 @@ mod tests {
     /// Operands that exercise the reduction's spill: the top bits set, all bits set, and the identities.
     const CORNERS: [u64; 6] = [0, 1, u64::MAX, 1 << 63, 0xF000_0000_0000_0000, R64];
 
+    /// The carry-less product bit by bit, the reference every other is checked against.
+    fn schoolbook(a: u64, b: u64) -> u128 {
+        (0..64).filter(|i| a >> i & 1 == 1).fold(0, |p, i| p ^ (b as u128) << i)
+    }
+
     /// Reference product: schoolbook multiply, then bit-by-bit long division by the modulus.
     fn reference_mul(a: u64, b: u64) -> u64 {
-        let mut p = software::clmul(a, b);
+        let mut p = schoolbook(a, b);
         // Clear bits 127..64 from the top, each with one shifted copy of x^64 + 0x1B.
         for bit in (64..128).rev() {
             if (p >> bit) & 1 != 0 {
@@ -441,6 +531,7 @@ mod tests {
     fn python_vectors() {
         for (a, b, c) in VECTORS {
             assert_eq!(F64(a) * F64(b), F64(c));
+            assert_eq!(F64(a).mul_portable(F64(b)), F64(c));
             assert_eq!(reference_mul(a, b), c);
         }
     }
@@ -453,20 +544,22 @@ mod tests {
         let corners = CORNERS.iter().flat_map(|&a| CORNERS.iter().map(move |&b| (a, b)));
         for (a, b) in random.chain(corners) {
             let want = reference_mul(a, b);
-            // The dispatched product and the portable composition agree with the reference.
+            // The dispatched and the portable products agree with the reference.
             assert_eq!((F64(a) * F64(b)).0, want);
-            assert_eq!(reduce(software::clmul(a, b)), want);
-            // The widening product is the carry-less product on every backend.
-            assert_eq!(mul_wide(a, b), software::clmul(a, b));
-            // The bit spread is the carry-less square, where a square uses it.
+            assert_eq!(F64(a).mul_portable(F64(b)).0, want);
+            // The widening products are the carry-less product on every backend.
+            assert_eq!(portable::clmul(a, b), schoolbook(a, b));
+            assert_eq!(mul_wide(a, b), schoolbook(a, b));
+            // The bit spreads are the carry-less square, where a square uses one, and squaring is the self-product.
+            assert_eq!(portable::spread(a), schoolbook(a, a));
             #[cfg(not(all(target_arch = "aarch64", target_feature = "aes")))]
-            assert_eq!(square_wide(a), software::clmul(a, a));
-            // Squaring is the self-product.
+            assert_eq!(square_wide(a), schoolbook(a, a));
             assert_eq!(F64(a).square(), F64(reference_mul(a, a)));
+            assert_eq!(F64(a).square_portable(), F64(reference_mul(a, a)));
         }
     }
 
-    /// Every NEON mul variant agrees with the software reference.
+    /// Every NEON mul variant agrees with the reference.
     #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
     #[test]
     fn neon_variants_match_software() {
@@ -496,9 +589,11 @@ mod tests {
         let elements = (0..200).map(|_| rng.next_u64()).chain(CORNERS.into_iter().skip(1));
         for a in elements.map(F64) {
             assert_eq!(a * a.inv(), F64::ONE);
+            assert_eq!(a.inv_portable(), a.inv());
         }
         // Zero has no inverse and maps to zero by convention.
         assert_eq!(F64::ZERO.inv(), F64::ZERO);
+        assert_eq!(F64::ZERO.inv_portable(), F64::ZERO);
     }
 
     /// x is primitive: x^((2^64−1)/q) ≠ 1 for every prime q | 2^64 − 1.
@@ -507,6 +602,7 @@ mod tests {
         let n = u64::MAX;
         for q in [3, 5, 17, 257, 641, 65537, 6700417] {
             assert_ne!(F64::G.pow(n / q), F64::ONE, "x^((2^64-1)/{q}) == 1");
+            assert_eq!(F64::G.pow_portable(n / q), F64::G.pow(n / q));
         }
     }
 }
diff --git a/crates/primitives/src/field/gf2_64x3/aarch64.rs b/crates/primitives/src/field/gf2_64x3/aarch64.rs
index aa2d7c715..2fdb8dffa 100644
--- a/crates/primitives/src/field/gf2_64x3/aarch64.rs
+++ b/crates/primitives/src/field/gf2_64x3/aarch64.rs
@@ -194,6 +194,7 @@ pub struct F192x1Unreduced([uint64x2_t; 3]);
 impl From<F192> for F192x1 {
     #[inline(always)]
     fn from(e: F192) -> Self {
+        crate::portable::kernel();
         let (c01, c22) = split(e);
         Self { c01, c22 }
     }
@@ -203,6 +204,7 @@ impl F192x1 {
     /// The element at `e`, loaded into its registers.
     #[inline(always)]
     pub fn load(e: &F192) -> Self {
+        crate::portable::kernel();
         let words = (e as *const F192).cast::<u64>();
         // SAFETY: `e` is three words, `c0` and `c1` adjacent under `repr(C)`.
         unsafe {
diff --git a/crates/primitives/src/field/gf2_64x3/mod.rs b/crates/primitives/src/field/gf2_64x3/mod.rs
index 90bb81f86..c271e4a68 100644
--- a/crates/primitives/src/field/gf2_64x3/mod.rs
+++ b/crates/primitives/src/field/gf2_64x3/mod.rs
@@ -22,7 +22,7 @@ use super::gf2_64::F64;
 )))]
 use super::gf2_64::mul_wide;
 #[cfg(not(all(target_arch = "aarch64", target_feature = "aes")))]
-use super::gf2_64::{reduce, square_wide};
+use super::gf2_64::square_wide;
 use core::iter::Sum;
 #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx2"))]
 use core::mem::MaybeUninit;
@@ -109,10 +109,12 @@ impl F192 {
     pub fn mul_unreduced(self, rhs: Self) -> F192Unreduced {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             aarch64::mul_unreduced(self, rhs)
         }
         #[cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq"))]
         {
+            crate::portable::kernel();
             // SAFETY: pclmulqdq is enabled at compile time.
             unsafe { x86_64::mul_unreduced(self, rhs) }
         }
@@ -121,7 +123,7 @@ impl F192 {
             all(target_arch = "x86_64", target_feature = "pclmulqdq")
         )))]
         {
-            software::mul_unreduced(self, rhs)
+            portable::mul_unreduced(self, rhs)
         }
     }
 
@@ -132,6 +134,7 @@ impl F192 {
     pub fn mul_base(self, k: F64) -> Self {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             aarch64::mul_base(self, k)
         }
         #[cfg(not(all(target_arch = "aarch64", target_feature = "aes")))]
@@ -145,10 +148,12 @@ impl F192 {
     pub fn mul_base_unreduced(self, k: F64) -> F192Unreduced {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             aarch64::mul_base_unreduced(self, k)
         }
         #[cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq"))]
         {
+            crate::portable::kernel();
             // SAFETY: pclmulqdq is enabled at compile time.
             unsafe { x86_64::mul_base_unreduced(self, k) }
         }
@@ -173,6 +178,7 @@ impl F192 {
     pub fn square(self) -> Self {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             aarch64::square(self)
         }
         #[cfg(not(all(target_arch = "aarch64", target_feature = "aes")))]
@@ -213,6 +219,29 @@ impl F192 {
         );
         m.mul_base(F64(norm.c0).inv())
     }
+
+    /// The product, with no SIMD intrinsic or assembly: the verifier's (see [`crate::portable`]).
+    #[inline]
+    pub const fn mul_portable(self, rhs: Self) -> Self {
+        portable::mul(self, rhs)
+    }
+
+    /// The square, with no SIMD intrinsic or assembly.
+    #[inline]
+    pub const fn square_portable(self) -> Self {
+        portable::square(self)
+    }
+
+    /// The product by a base-field scalar, with no SIMD intrinsic or assembly.
+    #[inline]
+    pub const fn mul_base_portable(self, k: F64) -> Self {
+        portable::mul_base(self, k)
+    }
+
+    /// The inverse, zero for zero, with no SIMD intrinsic or assembly.
+    pub const fn inv_portable(self) -> Self {
+        portable::inv(self)
+    }
 }
 
 impl F192 {
@@ -220,8 +249,11 @@ impl F192 {
     #[inline(always)]
     pub fn mul2(a: [Self; 2], b: [Self; 2]) -> [Self; 2] {
         #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx2"))]
-        // SAFETY: both features are enabled at compile time.
-        return unsafe { x86_64::mul_vec2(a, b) };
+        {
+            crate::portable::kernel();
+            // SAFETY: both features are enabled at compile time.
+            unsafe { x86_64::mul_vec2(a, b) }
+        }
         #[cfg(not(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx2")))]
         [a[0] * b[0], a[1] * b[1]]
     }
@@ -229,6 +261,8 @@ impl F192 {
     /// Four independent products.
     #[inline(always)]
     pub fn mul4(a: [Self; 4], b: [Self; 4]) -> [Self; 4] {
+        #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
+        crate::portable::kernel();
         #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
         // SAFETY: both features are enabled at compile time.
         return unsafe { x86_64::mul_vec4(a, b) };
@@ -243,6 +277,8 @@ impl F192 {
     /// Four independent products without the reduction, for a caller XOR-accumulating many products.
     #[inline(always)]
     pub fn mul_unreduced4(a: [Self; 4], b: [Self; 4]) -> [F192Unreduced; 4] {
+        #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx2"))]
+        crate::portable::kernel();
         #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
         // SAFETY: both features are enabled at compile time.
         return unsafe { x86_64::mul_unreduced_vec4(a, b) };
@@ -267,6 +303,8 @@ impl F192 {
     /// On AVX-512 this is six CLMULs for all eight, against twenty-four one at a time.
     #[inline(always)]
     pub fn mul_base8(t: Self, k: [F64; 8]) -> [Self; 8] {
+        #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
+        crate::portable::kernel();
         #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
         // SAFETY: both features are enabled at compile time.
         return unsafe { x86_64::mul_base8(t, k) };
@@ -316,6 +354,7 @@ impl Mul for F192 {
     fn mul(self, rhs: Self) -> Self {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             aarch64::mul(self, rhs)
         }
         #[cfg(not(all(target_arch = "aarch64", target_feature = "aes")))]
@@ -365,6 +404,7 @@ impl MixedSums8 {
     /// Add `t * k[i]` to sum `i`.
     #[inline(always)]
     pub fn add(&mut self, t: F192, k: [F64; 8]) {
+        crate::portable::kernel();
         // SAFETY: both features are enabled at compile time.
         unsafe { x86_64::mul_base8_add(&mut self.acc, t, k) }
     }
@@ -403,6 +443,7 @@ pub struct F192x4Unreduced {
 impl From<[F192; 4]> for F192x4 {
     #[inline(always)]
     fn from(v: [F192; 4]) -> Self {
+        crate::portable::kernel();
         Self {
             // SAFETY: both features are enabled at compile time.
             lanes: unsafe { x86_64::lanes4(v) },
@@ -435,6 +476,7 @@ impl F192x4 {
     /// From memory: two loads and two permutes, where building from values inserts twelve words one at a time.
     #[inline(always)]
     pub fn load(v: &[F192; 4]) -> Self {
+        crate::portable::kernel();
         Self {
             // SAFETY: both features are enabled at compile time; `v` is twelve words.
             lanes: unsafe { x86_64::load_lanes4(v) },
@@ -585,6 +627,8 @@ impl Weights8 {
 pub fn dot_base(w: &[Weights8], k: &[F64]) -> F192Unreduced {
     assert_eq!(k.len(), 8 * w.len());
     #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
+    crate::portable::kernel();
+    #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f"))]
     // SAFETY: both features are enabled at compile time; the lengths match.
     return unsafe { x86_64::dot_base(w, k) };
     #[cfg(not(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx512f")))]
@@ -614,25 +658,34 @@ impl F192Unreduced {
         allow(dead_code, reason = "the portable product's, kept as the tests' reference")
     )]
     #[inline]
-    fn from_wide(coeffs: [u128; 3]) -> Self {
+    const fn from_wide([c0, c1, c2]: [u128; 3]) -> Self {
         Self {
-            coeffs: coeffs.map(|c| [c as u64, (c >> 64) as u64]),
+            coeffs: [
+                [c0 as u64, (c0 >> 64) as u64],
+                [c1 as u64, (c1 >> 64) as u64],
+                [c2 as u64, (c2 >> 64) as u64],
+            ],
         }
     }
 
     /// Reduce each coefficient modulo the base polynomial.
+    #[cfg_attr(
+        not(all(target_arch = "aarch64", target_feature = "aes")),
+        expect(
+            clippy::missing_const_for_fn,
+            reason = "The aarch64 implementation requires runtime intrinsics."
+        )
+    )]
     #[inline]
     pub fn reduce(self) -> F192 {
         #[cfg(all(target_arch = "aarch64", target_feature = "aes"))]
         {
+            crate::portable::kernel();
             aarch64::reduce(self)
         }
         #[cfg(not(all(target_arch = "aarch64", target_feature = "aes")))]
         {
-            let [c0, c1, c2] = self
-                .coeffs
-                .map(|[lo, hi]| reduce(u128::from(hi) << 64 | u128::from(lo)));
-            F192 { c0, c1, c2 }
+            portable::reduce(self)
         }
     }
 }
@@ -709,39 +762,12 @@ pub mod aarch64;
 #[cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq"))]
 pub mod x86_64;
 
-/// Portable fallback, and the reference every accelerated path is tested against.
-mod software {
-    use super::{F192, F192Unreduced};
-    use crate::field::gf2_64::software::clmul;
-
-    /// Schoolbook: nine base products into the five coefficients of `y^0..y^4`, then the `y`-fold.
-    #[cfg_attr(
-        any(
-            all(target_arch = "aarch64", target_feature = "aes"),
-            all(target_arch = "x86_64", target_feature = "pclmulqdq")
-        ),
-        allow(
-            dead_code,
-            reason = "the portable product, kept as the tests' reference where a CLMUL backend serves"
-        )
-    )]
-    pub(super) fn mul_unreduced(a: F192, b: F192) -> F192Unreduced {
-        let (a, b) = ([a.c0, a.c1, a.c2], [b.c0, b.c1, b.c2]);
-        let mut e = [0u128; 5];
-        // a_i * b_j lands on y^(i + j).
-        for i in 0..3 {
-            for j in 0..3 {
-                e[i + j] ^= clmul(a[i], b[j]);
-            }
-        }
-        // y^3 = y + 1 and y^4 = y^2 + y.
-        F192Unreduced::from_wide([e[0] ^ e[3], e[1] ^ e[3] ^ e[4], e[2] ^ e[4]])
-    }
-}
+/// The portable products, behind the `*_portable` methods and every fallback.
+mod portable;
 
 #[cfg(test)]
 mod tests {
-    // Every backend against the software reference, independent vectors, the field axioms, and both moduli's irreducibility.
+    // Every backend against a schoolbook reference, independent vectors, the field axioms, and both moduli's irreducibility.
 
     use super::*;
     use crate::field::gf2_64::R64;
@@ -756,11 +782,6 @@ mod tests {
     #[cfg(all(target_arch = "x86_64", target_feature = "pclmulqdq"))]
     use x86_64::{F192x1, F192x1Unreduced};
 
-    /// The portable product, the reference every backend is checked against.
-    fn software_mul(a: F192, b: F192) -> F192 {
-        software::mul_unreduced(a, b).reduce()
-    }
-
     /// Vectors generated by an independent Python implementation
     /// (scratchpad/fieldref.py): (a, b, a·b, a·a).
     type ReferenceVector = ([u64; 3], [u64; 3], [u64; 3], [u64; 3]);
@@ -808,41 +829,58 @@ mod tests {
         random.chain(corners).collect()
     }
 
+    /// The schoolbook product over bit-by-bit carry-less products, the reference every other is checked against.
+    fn reference(a: F192, b: F192) -> F192 {
+        let clmul = |a: u64, b: u64| (0..64).filter(|i| a >> i & 1 == 1).fold(0, |p, i| p ^ (b as u128) << i);
+        let (a, b) = ([a.c0, a.c1, a.c2], [b.c0, b.c1, b.c2]);
+        let mut e = [0u128; 5];
+        for i in 0..3 {
+            for j in 0..3 {
+                e[i + j] ^= clmul(a[i], b[j]);
+            }
+        }
+        // y^3 = y + 1 and y^4 = y^2 + y.
+        portable::reduce(F192Unreduced::from_wide([e[0] ^ e[3], e[1] ^ e[3] ^ e[4], e[2] ^ e[4]]))
+    }
+
     #[test]
     fn python_vectors_and_modulus() {
         for (a, b, c, s) in VECTORS {
             let (a, b) = (F192::new(a[0], a[1], a[2]), F192::new(b[0], b[1], b[2]));
             assert_eq!(a * b, F192::new(c[0], c[1], c[2]));
             assert_eq!(a.square(), F192::new(s[0], s[1], s[2]));
-            assert_eq!(software_mul(a, b), F192::new(c[0], c[1], c[2]));
+            assert_eq!(reference(a, b), F192::new(c[0], c[1], c[2]));
         }
         assert_eq!(F192::Y * F192::Y * F192::Y, F192::Y + F192::ONE);
     }
 
     #[test]
-    fn products_match_software() {
+    fn products_match_the_reference() {
         for (a, b) in operand_pairs(2) {
-            let want = software_mul(a, b);
-            // Dispatched product, its unreduced form, and squaring.
+            let want = reference(a, b);
+            // Dispatched and portable products, the unreduced form, and squaring.
             assert_eq!(a * b, want);
+            assert_eq!(a.mul_portable(b), want);
             assert_eq!(a.mul_unreduced(b).reduce(), want);
-            assert_eq!(a.square(), software_mul(a, a));
+            assert_eq!(a.square(), reference(a, a));
+            assert_eq!(a.square_portable(), reference(a, a));
             // A mixed product is a full product by an element with no y part.
             let k = F64(b.c1);
-            let want = software_mul(a, F192::from(k));
+            let want = reference(a, F192::from(k));
             assert_eq!(a.mul_base(k), want);
+            assert_eq!(a.mul_base_portable(k), want);
             assert_eq!(a.mul_base_unreduced(k).reduce(), want);
         }
     }
 
     #[test]
-    fn batched_products_match_software() {
+    fn batched_products_match_the_reference() {
         // Four consecutive pairs per batch.
         let pairs = operand_pairs(6);
         for batch in pairs.as_chunks::<4>().0 {
             let a = batch.map(|(a, _)| a);
             let b = batch.map(|(_, b)| b);
-            let want: [F192; 4] = std::array::from_fn(|i| software_mul(a[i], b[i]));
+            let want: [F192; 4] = std::array::from_fn(|i| reference(a[i], b[i]));
             assert_eq!(F192::mul4(a, b), want);
             assert_eq!(F192::mul_unreduced4(a, b).map(F192Unreduced::reduce), want);
             assert_eq!(F192::mul2([a[0], a[1]], [b[0], b[1]]), [want[0], want[1]]);
@@ -851,7 +889,7 @@ mod tests {
 
     #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx2"))]
     #[test]
-    fn lane_products_match_software() {
+    fn lane_products_match_the_reference() {
         let pairs = operand_pairs(11);
         // Padded to whole batches, so the last corner pair is tested too.
         let pairs = [
@@ -862,7 +900,7 @@ mod tests {
         for batch in pairs.as_chunks::<4>().0 {
             let a = batch.map(|(a, _)| a);
             let b = batch.map(|(_, b)| b);
-            let want: [F192; 4] = std::array::from_fn(|i| software_mul(a[i], b[i]));
+            let want: [F192; 4] = std::array::from_fn(|i| reference(a[i], b[i]));
             let (a4, b4) = (F192x4::from(a), F192x4::from(b));
             assert_eq!(<[F192; 4]>::from(a4), a);
             assert_eq!(<[F192; 4]>::from(F192x4::load(&a)), a);
@@ -875,7 +913,7 @@ mod tests {
             let mut acc = F192x4Unreduced::zero();
             acc ^= a4.mul_unreduced(b4);
             acc ^= F192x4::splat(a[0]).mul_unreduced(b4);
-            let sum = (0..4).fold(F192::ZERO, |s, i| s + want[i] + software_mul(a[0], b[i]));
+            let sum = (0..4).fold(F192::ZERO, |s, i| s + want[i] + reference(a[0], b[i]));
             assert_eq!(acc.sum().reduce(), sum);
         }
     }
@@ -887,15 +925,15 @@ mod tests {
         all(target_arch = "x86_64", target_feature = "pclmulqdq")
     ))]
     #[test]
-    fn register_products_match_software() {
+    fn register_products_match_the_reference() {
         for (a, b) in operand_pairs(12) {
             let (a1, b1) = (F192x1::load(&a), F192x1::from(b));
-            assert_eq!(F192::from(a1 * b1), software_mul(a, b));
+            assert_eq!(F192::from(a1 * b1), reference(a, b));
             assert_eq!(F192::from(a1 + b1), a + b);
             let mut acc = F192x1Unreduced::zero();
             acc ^= a1.mul_unreduced(b1);
             acc ^= b1.mul_base_unreduced(F64(a.c2));
-            let want = software_mul(a, b) + software_mul(b, F192::from(F64(a.c2)));
+            let want = reference(a, b) + reference(b, F192::from(F64(a.c2)));
             assert_eq!(F192::from(acc.reduce()), want);
             assert_eq!(F192Unreduced::from(acc).reduce(), want);
             let mut out = MaybeUninit::uninit();
@@ -914,6 +952,7 @@ mod tests {
             if !a.is_zero() {
                 assert_eq!(a * a.inv(), F192::ONE);
             }
+            assert_eq!(a.inv_portable(), a.inv());
             // K-valued and y-free elements are the cases `inv`'s norm path is
             // most likely to get wrong, and the interpreter's MUL back-solve
             // inverts K-valued words exclusively.
@@ -922,8 +961,10 @@ mod tests {
                 assert_eq!(k * k.inv(), F192::ONE);
                 assert_eq!(k.inv(), F192::from(F64(k.c0).inv()));
             }
+            assert_eq!(k.inv_portable(), k.inv());
         }
         assert_eq!(F192::ZERO.inv(), F192::ZERO);
+        assert_eq!(F192::ZERO.inv_portable(), F192::ZERO);
     }
 
     #[test]
@@ -951,7 +992,7 @@ mod tests {
 
     #[cfg(all(target_arch = "x86_64", target_feature = "vpclmulqdq", target_feature = "avx2"))]
     #[test]
-    fn mixed_sums_match_software() {
+    fn mixed_sums_match_the_reference() {
         let mut rng = Rng::new(10);
         for _ in 0..200 {
             // A zero and an all-ones word in every term, a corner coefficient in the first.
@@ -973,7 +1014,7 @@ mod tests {
             let want: [F192; 8] = std::array::from_fn(|i| {
                 terms
                     .iter()
-                    .fold(F192::ZERO, |acc, (t, k)| acc + software_mul(*t, F192::from(k[i])))
+                    .fold(F192::ZERO, |acc, (t, k)| acc + reference(*t, F192::from(k[i])))
             });
             assert_eq!(sums.reduce(), want);
         }
diff --git a/crates/primitives/src/field/gf2_64x3/portable.rs b/crates/primitives/src/field/gf2_64x3/portable.rs
new file mode 100644
index 000000000..93159e19e
--- /dev/null
+++ b/crates/primitives/src/field/gf2_64x3/portable.rs
@@ -0,0 +1,57 @@
+//! The portable products: integer code with no SIMD intrinsic or assembly, the same on every target.
+
+use super::{F192, F192Unreduced};
+use crate::field::gf2_64::portable::{clmul, spread};
+use crate::field::gf2_64::{F64, reduce as reduce_wide};
+
+/// Karatsuba: six base products into the five coefficients of `y^0..y^4`, then the `y`-fold.
+#[inline]
+pub const fn mul_unreduced(a: F192, b: F192) -> F192Unreduced {
+    let (p0, p1, p2) = (clmul(a.c0, b.c0), clmul(a.c1, b.c1), clmul(a.c2, b.c2));
+    let p01 = clmul(a.c0 ^ a.c1, b.c0 ^ b.c1);
+    let p02 = clmul(a.c0 ^ a.c2, b.c0 ^ b.c2);
+    let p12 = clmul(a.c1 ^ a.c2, b.c1 ^ b.c2);
+    // `a_i b_j + a_j b_i = p_ij + p_i + p_j` lands on `y^(i + j)`.
+    let (e1, e2, e3) = (p01 ^ p0 ^ p1, p02 ^ p0 ^ p2 ^ p1, p12 ^ p1 ^ p2);
+    // `y^3 = y + 1` and `y^4 = y^2 + y`.
+    F192Unreduced::from_wide([p0 ^ e3, e1 ^ e3 ^ p2, e2 ^ p2])
+}
+
+/// Each coefficient reduced modulo the base polynomial.
+#[inline]
+pub const fn reduce(u: F192Unreduced) -> F192 {
+    const fn wide([lo, hi]: [u64; 2]) -> u64 {
+        reduce_wide((hi as u128) << 64 | lo as u128)
+    }
+    let [c0, c1, c2] = u.coeffs;
+    F192::new(wide(c0), wide(c1), wide(c2))
+}
+
+#[inline]
+pub const fn mul(a: F192, b: F192) -> F192 {
+    reduce(mul_unreduced(a, b))
+}
+
+/// Three base-field squares: `(c0 + c1 y + c2 y^2)^2 = c0^2 + c2^2 y + (c1^2 + c2^2) y^2`.
+#[inline]
+pub const fn square(a: F192) -> F192 {
+    let (s0, s1, s2) = (spread(a.c0), spread(a.c1), spread(a.c2));
+    reduce(F192Unreduced::from_wide([s0, s2, s1 ^ s2]))
+}
+
+/// The three coefficients times one base-field scalar.
+#[inline]
+pub const fn mul_base(a: F192, k: F64) -> F192 {
+    F192::new(
+        F64(a.c0).mul_portable(k).0,
+        F64(a.c1).mul_portable(k).0,
+        F64(a.c2).mul_portable(k).0,
+    )
+}
+
+/// Through the norm, as [`F192::inv`].
+pub const fn inv(a: F192) -> F192 {
+    let m = mul(a.frobenius(), a.frobenius().frobenius());
+    let norm = mul(a, m);
+    mul_base(m, F64(norm.c0).inv_portable())
+}
diff --git a/crates/primitives/src/field/gf2_64x3/x86_64.rs b/crates/primitives/src/field/gf2_64x3/x86_64.rs
index 638445658..2928acc51 100644
--- a/crates/primitives/src/field/gf2_64x3/x86_64.rs
+++ b/crates/primitives/src/field/gf2_64x3/x86_64.rs
@@ -142,6 +142,7 @@ pub struct F192x1Unreduced([__m128i; 3]);
 impl From<F192> for F192x1 {
     #[inline(always)]
     fn from(e: F192) -> Self {
+        crate::portable::kernel();
         // SAFETY: SSE2 is part of the x86-64 baseline.
         Self {
             c01: pair(e.c0, e.c1),
@@ -154,6 +155,7 @@ impl F192x1 {
     /// The element at `e`, loaded into its registers.
     #[inline(always)]
     pub fn load(e: &F192) -> Self {
+        crate::portable::kernel();
         let words = (e as *const F192).cast::<u64>();
         // SAFETY: `e` is three words, `c0` and `c1` adjacent under `repr(C)`.
         unsafe {
@@ -1137,6 +1139,7 @@ impl F192x8 {
     #[inline]
     #[target_feature(enable = "vpclmulqdq", enable = "avx512f")]
     pub fn mul(self, rhs: Self) -> Self {
+        crate::portable::kernel();
         let (even, odd) = (self.karatsuba::<0x00>(rhs), self.karatsuba::<0x11>(rhs));
         // Lane j of `even` is element 2j's product and of `odd` element 2j + 1's: unpacking restores qword order.
         // SAFETY: the function carries both features.
@@ -1159,6 +1162,7 @@ impl F192x8Sum {
     #[inline]
     #[target_feature(enable = "avx512f")]
     pub fn zero() -> Self {
+        crate::portable::kernel();
         Self([_mm512_setzero_si512(); 3])
     }
 
diff --git a/crates/primitives/src/hash/mod.rs b/crates/primitives/src/hash/mod.rs
index 0154a691b..21bee1472 100644
--- a/crates/primitives/src/hash/mod.rs
+++ b/crates/primitives/src/hash/mod.rs
@@ -100,37 +100,51 @@ pub const PARAM_IV: [u32; 8] = {
 #[inline]
 pub fn compress(h: &mut [u32; 8], m: &[u32; 16], t: u64, last: bool) {
     #[cfg(target_arch = "x86_64")]
-    x86::compress(h, m, t, last);
+    {
+        crate::portable::kernel();
+        x86::compress(h, m, t, last);
+    }
     #[cfg(not(target_arch = "x86_64"))]
-    compress_portable(h, m, t, last);
+    portable::compress(h, m, t, last);
 }
 
-/// The compression as written in RFC 7693, and the reference the x86-64 kernel is checked against.
-#[cfg_attr(target_arch = "x86_64", allow(dead_code))]
-fn compress_portable(h: &mut [u32; 8], m: &[u32; 16], t: u64, last: bool) {
-    let mut v = [0u32; 16];
-    v[..8].copy_from_slice(h);
-    v[8..].copy_from_slice(&IV);
-    v[12] ^= t as u32;
-    v[13] ^= (t >> 32) as u32;
-    if last {
-        v[14] = !v[14];
-    }
-    for round in &SIGMA {
-        for (g, &[a, b, c, d]) in G_LANES.iter().enumerate() {
-            let (mx, my) = (m[round[2 * g]], m[round[2 * g + 1]]);
-            v[a] = v[a].wrapping_add(v[b]).wrapping_add(mx);
-            v[d] = (v[d] ^ v[a]).rotate_right(16);
-            v[c] = v[c].wrapping_add(v[d]);
-            v[b] = (v[b] ^ v[c]).rotate_right(12);
-            v[a] = v[a].wrapping_add(v[b]).wrapping_add(my);
-            v[d] = (v[d] ^ v[a]).rotate_right(8);
-            v[c] = v[c].wrapping_add(v[d]);
-            v[b] = (v[b] ^ v[c]).rotate_right(7);
+/// The hashes the verifier takes: the compression as RFC 7693 writes it, with no SIMD intrinsic or assembly.
+pub mod portable {
+    use super::{G_LANES, IV, OUT_LEN, SIGMA};
+
+    /// The compression as written in RFC 7693, and the reference the x86-64 kernel is checked against.
+    pub fn compress(h: &mut [u32; 8], m: &[u32; 16], t: u64, last: bool) {
+        let mut v = [0u32; 16];
+        v[..8].copy_from_slice(h);
+        v[8..].copy_from_slice(&IV);
+        v[12] ^= t as u32;
+        v[13] ^= (t >> 32) as u32;
+        if last {
+            v[14] = !v[14];
+        }
+        for round in &SIGMA {
+            for (g, &[a, b, c, d]) in G_LANES.iter().enumerate() {
+                let (mx, my) = (m[round[2 * g]], m[round[2 * g + 1]]);
+                v[a] = v[a].wrapping_add(v[b]).wrapping_add(mx);
+                v[d] = (v[d] ^ v[a]).rotate_right(16);
+                v[c] = v[c].wrapping_add(v[d]);
+                v[b] = (v[b] ^ v[c]).rotate_right(12);
+                v[a] = v[a].wrapping_add(v[b]).wrapping_add(my);
+                v[d] = (v[d] ^ v[a]).rotate_right(8);
+                v[c] = v[c].wrapping_add(v[d]);
+                v[b] = (v[b] ^ v[c]).rotate_right(7);
+            }
+        }
+        for i in 0..8 {
+            h[i] ^= v[i] ^ v[i + 8];
         }
     }
-    for i in 0..8 {
-        h[i] ^= v[i] ^ v[i + 8];
+
+    /// [`super::hash`], by [`compress`].
+    ///
+    /// A continued hash is [`super::ChainingValue::hash_portable`].
+    pub fn hash(data: &[u8]) -> [u8; OUT_LEN] {
+        super::hash_with(compress, data)
     }
 }
 
@@ -150,7 +164,8 @@ fn state_bytes(h: &[u32; 8]) -> [u8; OUT_LEN] {
     out
 }
 
-/// Streaming BLAKE2s-256.
+/// Streaming BLAKE2s-256, by the portable compression: the program's and the tree's digests, which the verifier
+/// recomputes, take it.
 ///
 /// The final block carries the final flag, so a full buffer is held back until more input arrives.
 #[derive(Clone)]
@@ -182,7 +197,7 @@ impl Hasher {
             if self.buf_len == BLOCK_LEN {
                 // More input follows, so this buffered block is not the last.
                 self.counter += BLOCK_LEN as u64;
-                compress(&mut self.h, &block_words(&self.buf), self.counter, false);
+                portable::compress(&mut self.h, &block_words(&self.buf), self.counter, false);
                 self.buf_len = 0;
             }
             let take = (BLOCK_LEN - self.buf_len).min(data.len());
@@ -199,7 +214,7 @@ impl Hasher {
         let mut block = self.buf;
         block[self.buf_len..].fill(0);
         let t = self.counter + self.buf_len as u64;
-        compress(&mut h, &block_words(&block), t, true);
+        portable::compress(&mut h, &block_words(&block), t, true);
         state_bytes(&h)
     }
 }
@@ -212,13 +227,33 @@ impl Default for Hasher {
 
 /// One-shot unkeyed BLAKE2s-256.
 pub fn hash(data: &[u8]) -> [u8; OUT_LEN] {
-    // Whole blocks, the shape hashed in bulk, need no buffering.
-    if !data.is_empty() && data.len().is_multiple_of(BLOCK_LEN) {
-        return ChainingValue::START.hash(data);
+    hash_with(compress, data)
+}
+
+/// [`hash`] by `compress`.
+#[inline]
+fn hash_with(compress: impl Fn(&mut [u32; 8], &[u32; 16], u64, bool), data: &[u8]) -> [u8; OUT_LEN] {
+    let (blocks, tail) = data.as_chunks::<BLOCK_LEN>();
+    // The last block is the zero-padded tail, or the last whole block if there is no tail: an empty message is one zero block.
+    let (whole, last, last_len) = match blocks.split_last() {
+        Some((last, whole)) if tail.is_empty() => (whole, *last, BLOCK_LEN),
+        _ => {
+            let mut last = [0; BLOCK_LEN];
+            last[..tail.len()].copy_from_slice(tail);
+            (blocks, last, tail.len())
+        }
+    };
+    let mut h = PARAM_IV;
+    for (b, block) in whole.iter().enumerate() {
+        compress(&mut h, &block_words(block), ((b + 1) * BLOCK_LEN) as u64, false);
     }
-    let mut hasher = Hasher::new();
-    hasher.update(data);
-    hasher.finalize()
+    compress(
+        &mut h,
+        &block_words(&last),
+        (whole.len() * BLOCK_LEN + last_len) as u64,
+        true,
+    );
+    state_bytes(&h)
 }
 
 /// A digest as the four little-endian words it packs.
@@ -273,6 +308,17 @@ impl ChainingValue {
     ///
     /// PCS leaves share such a prefix: their absent interleaving lanes.
     pub fn zero_prefix(n_blocks: usize) -> Self {
+        Self::zero_prefix_with(compress, n_blocks)
+    }
+
+    /// [`Self::zero_prefix`] by the portable compression.
+    pub fn zero_prefix_portable(n_blocks: usize) -> Self {
+        Self::zero_prefix_with(portable::compress, n_blocks)
+    }
+
+    /// [`Self::zero_prefix`] by `compress`.
+    #[inline]
+    fn zero_prefix_with(compress: impl Fn(&mut [u32; 8], &[u32; 16], u64, bool), n_blocks: usize) -> Self {
         let mut h = PARAM_IV;
         for b in 0..n_blocks {
             compress(&mut h, &[0u32; 16], ((b + 1) * BLOCK_LEN) as u64, false);
@@ -290,6 +336,17 @@ impl ChainingValue {
 
     /// The digest of the image continued by `rest`, a nonzero whole number of blocks.
     pub fn hash(&self, rest: &[u8]) -> [u8; OUT_LEN] {
+        self.hash_with(compress, rest)
+    }
+
+    /// [`Self::hash`] by the portable compression.
+    pub fn hash_portable(&self, rest: &[u8]) -> [u8; OUT_LEN] {
+        self.hash_with(portable::compress, rest)
+    }
+
+    /// [`Self::hash`] by `compress`.
+    #[inline]
+    fn hash_with(&self, compress: impl Fn(&mut [u32; 8], &[u32; 16], u64, bool), rest: &[u8]) -> [u8; OUT_LEN] {
         assert!(
             !rest.is_empty() && rest.len().is_multiple_of(BLOCK_LEN),
             "a continued image is whole blocks"
@@ -308,6 +365,7 @@ impl ChainingValue {
     ///
     /// `len` is a nonzero whole number of blocks.
     pub fn hash_many(&self, data: &[u8], len: usize, out: &mut [u8]) {
+        crate::portable::kernel();
         assert!(
             len > 0 && len.is_multiple_of(BLOCK_LEN),
             "batched inputs are whole blocks"
@@ -379,6 +437,12 @@ mod tests {
                             want,
                             "scalar, zero_blocks={zero_blocks} rest_blocks={rest_blocks}"
                         );
+                        assert_eq!(
+                            ChainingValue::zero_prefix_portable(zero_blocks)
+                                .hash_portable(&rest[i * rlen..(i + 1) * rlen]),
+                            want,
+                            "portable, zero_blocks={zero_blocks} rest_blocks={rest_blocks}"
+                        );
                     }
                 }
             }
@@ -398,7 +462,7 @@ mod tests {
                 let m: [u32; 16] = std::array::from_fn(|_| rng.next_u32());
                 let (mut got, mut want) = (h, h);
                 compress(&mut got, &m, t, last);
-                compress_portable(&mut want, &m, t, last);
+                portable::compress(&mut want, &m, t, last);
                 assert_eq!(got, want, "t={t} last={last}");
             }
         }
@@ -420,9 +484,10 @@ mod tests {
 
     #[test]
     fn matches_official_vectors() {
-        // Whole blocks take the fast path, and 65 bytes pins the held-back buffer.
+        // Whole blocks, a padded tail, and 65 bytes, one byte past a block.
         for (input, digest) in test_vectors() {
             assert_eq!(hash(&input), digest, "{} bytes", input.len());
+            assert_eq!(portable::hash(&input), digest, "portable, {} bytes", input.len());
         }
     }
 
diff --git a/crates/primitives/src/lib.rs b/crates/primitives/src/lib.rs
index f90d2a756..7b2108d2e 100644
--- a/crates/primitives/src/lib.rs
+++ b/crates/primitives/src/lib.rs
@@ -5,6 +5,7 @@ pub mod bits;
 pub mod field;
 pub mod hash;
 pub mod multilinear;
+pub mod portable;
 pub mod stream;
 
 use std::mem::MaybeUninit;
diff --git a/crates/primitives/src/portable.rs b/crates/primitives/src/portable.rs
new file mode 100644
index 000000000..e7df6619d
--- /dev/null
+++ b/crates/primitives/src/portable.rs
@@ -0,0 +1,61 @@
+//! The native verifier is portable and single-threaded: it runs on the calling thread, with no SIMD intrinsic, no
+//! inline assembly and no pool dispatch, so that it computes the same way on every target.
+//!
+//! Its arithmetic is the `*_portable` field methods and its hashing [`crate::hash::portable`].
+//! Each of its entry points holds a [`Section`] while it runs, which refuses what it must not reach:
+//!
+//! - a pool dispatch panics, always ([`parallel::serial`]);
+//! - with the `guard` feature, which the workspace's tests enable, so does every SIMD or assembly kernel of this crate.
+
+use std::marker::PhantomData;
+
+#[cfg(feature = "guard")]
+use std::cell::Cell;
+
+#[cfg(feature = "guard")]
+thread_local! {
+    /// Whether this thread holds a [`Section`].
+    static INSIDE: Cell<bool> = const { Cell::new(false) };
+}
+
+/// Whether this build refuses kernels inside a [`Section`]: the `guard` feature, which tests check is on.
+pub const GUARDED: bool = cfg!(feature = "guard");
+
+/// Run as the verifier runs until the returned guard drops: on this thread, refusing pool dispatch, and under `guard`
+/// every kernel.
+#[must_use = "the section lasts only while the guard lives"]
+pub fn enter() -> Section {
+    Section {
+        _serial: parallel::serial(),
+        #[cfg(feature = "guard")]
+        previous: INSIDE.replace(true),
+        _thread: PhantomData,
+    }
+}
+
+/// A portable section: dropping it restores what was refused before, on return and on unwinding alike.
+pub struct Section {
+    _serial: parallel::Serial,
+    #[cfg(feature = "guard")]
+    previous: bool,
+    /// The section is this thread's, so the guard stays on it.
+    _thread: PhantomData<*const ()>,
+}
+
+#[cfg(feature = "guard")]
+impl Drop for Section {
+    fn drop(&mut self) {
+        INSIDE.set(self.previous);
+    }
+}
+
+/// A SIMD or assembly kernel is about to run: under `guard`, a panic inside a [`Section`].
+#[cfg_attr(
+    not(feature = "guard"),
+    expect(clippy::missing_const_for_fn, reason = "the guard reads a thread-local")
+)]
+#[inline(always)]
+pub(crate) fn kernel() {
+    #[cfg(feature = "guard")]
+    assert!(!INSIDE.get(), "a SIMD or assembly kernel inside the portable verifier");
+}