Repository navigation
Field vm/3mi whir - #1026
Draft
jotabulacios wants to merge 11 commits into
Draft
Field vm/3mi whir#1026jotabulacios wants to merge 11 commits into
jotabulacios wants to merge 11 commits into
Conversation
AirWithBuses hardcoded its next-row openings at g·z to the LogUp accumulator, so any main-column constraint reading the next row was checked against zero and the proof failed to verify. Derive the set in AirWithBuses::new from the wrapped constraint set with a NextRowReads builder (every main(1, col) it evaluates), plus the accumulator when the AIR has interactions. Only single-row steps get the derived set: multi-row steps keep the accumulator alone, so the step-size ceiling guarded by the_prover_cannot_prove_a_step_size_two_air stays. The VM's tables read only the current row, so their openings do not change; the Field VM's transition constraints need the new columns. Soundness tests cover a next-row constraint that verifies honestly and rejects a tampered next row.
Two precompiles for option B of split recursion, where the hash half of a leaf verifier (v_bin) runs as a native RISC-V guest: - P1W16Permute (u64::MAX-5) applies the width-16 Poseidon1 permutation in place to a [u64; 16] state, rejecting non-canonical inputs. It is the same permutation the LFM's p1w16 chip constrains. - Fp3Mac (u64::MAX-7) computes acc*a + x over Fp[t]/(t^3-2) in place, one Horner step of the checksum that binds v_bin to the Field VM. Both have syscalls wrappers, executor unit tests (known answers, non-canonical rejection) and a guest program each. The CLI counts them as non-tracked accelerators.
Give the two new ecalls their own tables so the block WHIR prover proves v_bin with them: - P1W16: one row per permutation, 663 columns, the Compact rounds of lfm/p1w16_chip (its Affine/mds_affine helpers become pub(crate)). - FP3MAC: one row per Fp3 multiply-accumulate, 163 columns. CPU sends each ecall on its own bus; the trace builder, windowed and finish paths and the oracle collect the calls. TableCounts, VmAirs and the statement grow by two counts (NUM_TABLE_KINDS 21 -> 23, statement and continuation-epoch tags V5 -> V7), so the LFM statement replay and its registry are regenerated. NUM_PRODUCTION_AIRS goes to 31 and the constraint census records both tables' emitter counts. Block tests prove and verify each guest and refuse a proof claiming the table is absent.
A test-only fn_scope recorder marks where an emitted LFM program enters and leaves a named region (each table of the batched argue, each p1 grinding check). The Field VM translation uses the marks to find repeated verifier functions and outline them. Markers are cfg(test); production emission is unchanged.
The LFM verifier legs assumed the VM's tables: unit public inputs, no end-exempt transitions and only the LogUp accumulator read at g·z. The Field VM breaks all three: - emit_quotient multiplies each transition constraint by its end-exemption factor prod_j (zeta - g^(N-j)) before the shared division, from the artifact's constraints_meta. - TableVerifyShape takes the next-row columns from the AIR's own trace_ood_next_row_columns, as the STARK verifier's OodLayout does. - TableChallengeShape, TableVerifyShape and the harvest helpers are generic over the AIR's public inputs (DynVmAir<PI>). VM verification is unchanged: its tables have no exemptions and the same next-row set. The block-path scan follows the renamed generic try_child_arena_words.
The 3MI Field VM (#971 spec): one FMA instruction over Fp[t]/(t^3-2) with DECODE, MEM, PUBLIC and STATE buses (BusId 40-43), proved as a standalone STARK. Ported from field-vm/3mi-lfm onto the #1014 base, with a selector column, segment state on the FieldVmState bus and, in LFM mode, a second public sender at addr + 2^39 for lane 3 of each cell. lfm_translate turns an LFM verifier program into a Field VM program. On top of the port it outlines repeated verifier functions (found with fn_scope, grouped into shape classes) into CALL/RET bodies with frames, rerolls periodic blocks into loops (widened periods, FVM_REROLL_MIN; blocks that use the frame register are skipped) and decomposes bits with a Horner fold (FVM_BITDEC_HORNER). hash_side proves the hash half of a translated leaf with the LFM's chips. Features fvm-d3/d4/narrow/n1 select the AIR variant.
prove_whir/verify_whir prove Field VM traces with the block WHIR
prover (BlockWhirHash, Poseidon1), with the ADDR ramp as a preprocessed
column; prove_whir_block uses the block proof format. The _bound
variants add the FIELD_VM_CKSUM table: alpha = H(c_bin || c_fld), where
c_bin digests the crossing cells on the v_bin side and c_fld is a
Poseidon1 sponge ("CKRT") over the non-CKSUM table roots. CKSUM folds
the crossing values with Horner in Fp3 and exposes s, which must equal
v_bin's FP3MAC result. alpha lives in three CKSUM columns held constant
down the table and is published as a public cell, so the verifier
program does not depend on the witness; the last group must be exactly
[CKSUM], so alpha binds every other root.
generic_fold is one Field VM program that performs a WHIR fold for any round shape, reading the shape as data instead of unrolling it. It costs 1.06-1.26x the rows of the shape-specific code and is a step toward a constant program id (L102). Tests are off under fvm-narrow.
split cuts a translated leaf verifier into its field half (v_fld, Field VM) and its hash half (v_bin). native_vbin compiles v_bin to RV64 machine code (rv64 is the encoder) that runs on the Lambda VM: Hash16 through the P1W16 ecall, Walk4 fusion of 4-ary tree walks, unrolled loops (NATIVE_VBIN_UNROLL), and with NATIVE_VBIN_BIND an epilogue that digests the crossing cells and folds the checksum with FP3MAC (unrolled by eight). Packed hint streams and slot reuse are the default (NATIVE_VBIN_WIDE_HINTS / NATIVE_VBIN_NO_REUSE turn them off): -5.0% cycles and -10.6% cells on the mainnet leaf. Cut::both/FVM_SPLIT_INDEX cross indices instead of bits.
The native v_bin guest was generated per leaf from the cut, so its program id named the leaf. vbin_generic compiles the cut's hash-half program to a schedule the guest reads as data: every cell gets a home (a word hint where the stream holds it, a shared hint in its IN cell, a constant in the schedule, BACK in BACK, the rest in ring slots), and the ops become a fixed interpreter's, with macros for hash chains over runs, 4-ary Merkle paths, muxes and lane asserts. The guest hashes the schedule (width-16 Poseidon1) and publishes that digest where the per-leaf guest published keccak of its program, so a verifier pins the schedule instead of the ELF. BACK, the published words and the binding are unchanged. A hint lane is checked canonical only when a non-canonical value could change a result (VBG_CANON_ALL=1 checks as before). Mainnet leaf 0: 19.0 M cycles (from 34.2 M) and 2.81 G proof cells (from 4.65 G). The ELF is the same for every leaf.
Option A leaves are hybrid Field VM proofs. ChildKind::Hybrid lets an LFM node verify one: the Field VM statement and transcript domain, the PUBLIC-bus balance and the STATE-bus fingerprints in place of the LFM's, and block_node pairs each public cell with its lane-3 companion to rebuild the block words. derive_top_with derives a hybrid tree's top from the plan alone through a dry run of each leaf (single-segment leaves), with the same program id as the top built over the proofs. An option B leaf is two proofs: v_bin as a Lambda VM block WHIR proof and v_fld as a Field VM WHIR proof. block_whir's frame holds either the VM's AIRs or an owned set (FrameAirs), so the same emitters verify the Field VM. whir_block gains an FvmBinding leaf target: the verifier reads c_bin, alpha, s and the computed public cells from its arena, recomputes alpha from c_bin and the Field VM roots, checks the CKSUM s against v_bin's and closes the Field VM bus. The B node takes the leaf's bus sum from the v_fld verifier's published input (LeafWord::Field) and, for the generic guest, pins its schedule digest. fvm_node, fvm_whir_leaf and fvm_whir_node test both on the small block's full tree under the plan's top (top_claims accepts; tampered lane-3 cells, id cells, schedules and swapped v_fld proofs are refused) and build the bound mainnet leaf verifier. Debug hooks dump a failing verifier's memory.
|
Benchmark Results for modified programs 🚀
|
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Motivation
The 3MI recursion spec splits the recursive verifier into two halves:
The two halves can be proved together or separately, bound by a check. This PR implements both forms on top of the WHIR no-epoch (prove-and-retire) block prover of #1014 and plugs them into its recursion tree, to measure them against the LFM on the same blocks. It also follows the review on PR #1019, in particular lines 102/114: one verifier program with a constant program id.
This is experimental: it is meant for measurement and discussion, not for merging as is.
Description
Two variants, both verified by the block recursion tree of #1014:
FP3MACprecompile, the Field VM with aFIELD_VM_CKSUMtable.What it adds:
P1W16(Poseidon1 width-16 permutation, ecallu64::MAX−5) andFP3MAC(acc·α + xin Fp³, ecallu64::MAX−7).except_lasttransitions;BlockFamilywrap hash;AirWithBuses: opens at g·z every column a constraint reads at the next row (single-row steps only, so the step-size-2 guard still holds).Measured (CPU, 96 cores; mainnet block 25368371, leaf 0; LFM leaf = 149–193 M cells):