diff --git a/AGENTS.md b/AGENTS.md index faa00f6c0..174c62850 100644 --- a/AGENTS.md +++ b/AGENTS.md @@ -41,7 +41,7 @@ The root `Cargo.toml` is workspace-only: the libraries are in `crates/`, the CLI - A hash chain, each step's digest the next step's value and a counter field its position, is `Template::chain` (both signature schemes' chains): on the VM its loop is written by hand in `precompile.rs`, eight instructions a step with the compression, which is what the compiler's own loop could not reach. A guest calls `Template::chain`, never the loop, so the loop can change under it. Everything else stays Rust, unrolled where a constant index makes a shift or an offset free (leanXMSS's 42 chain ends, its 32 Merkle levels). leanSPHINCS's tree paths go the other way, one loop that is never inlined (`fold`): its tweak's level is the high half of a word, which a loop keeps as a running sum, where an unrolled path builds each level's word as a constant with a shift. -- **A saved instruction pays only where it takes a table under a power of two** at the size proved: every class's table pads to a power of two, so read `bench --cycles-only`'s per-table heights, not the total. A rewrite that trades ALU rows for SHIFT or LOAD rows can double another table. +- **A saved instruction pays only where it takes a table under a power of two** at the size proved: every class's table pads to a power of two, so read `bench --cycles-only`'s per-table heights, not the total. A rewrite that trades ADD rows for SHIFT or LOAD rows can double another table. - rv64im has no carry-less multiply, so leanDA's membership check uses the extension-field precompile: one `extmack` per symbol, `sum += L_x * w_x` with `L_x` in `E` and `w_x` in `K` (`leanvm_guest::ext::mul_add_base`). An unrolled loop measured worse: LLVM strength-reduces it into more pointer updates than it saves. @@ -108,21 +108,21 @@ scripts/ab.sh --base HEAD~2 pcs-throughput # against another base The registers, RAM and the advice are read-write, by timestamped offline memory checking (`doc/leanvm` §sec:memchan). What to keep in mind before touching it: -- **A timestamp is an integer**, `2^40 | cycle << 5 | slot` read as the `K` word with those bits (`tables::SEED_CLOCK`, `CLOCK_START`, `LIVE_BIT`). **The clock rides the state tuple**, `(pc, ts)`, with slot zero, and a row's access in slot `k` carries `ts ^ k`, a column plus a constant, which is what lets one row touch the same cell twice (`add a0, a0, a0`). Slots are `rs1` at 0, `rs2` at 1, the RAM access at 2, `rd` at 3, and a row that skips an access leaves its slot unused (a load reads no `rs2`, a store and a hash write no `rd`); a hash row's sixteen block words take slots 2 to 17. Seeds are at cycle 0 (`2^40`), so the run starts at cycle 1: an access must be strictly later than the one before. -- **Each table has a second flock circuit, its clock circuit** (`tables::clock_circuit`, reference `tables::clock_step`): ports the row's clock `ts`, each access's previous timestamp `prev`, and `step`, all virtual columns of the table, packed in a witness of its own (`class_flock::N_FLOCKS` is 21: every class circuit, `tables::N_CIRCUITS` of them, then every table's clock circuit). An access pulls `(addr, prev, old)` and pushes `(addr, ts ^ k, new)`; the circuit checks `prev`'s bit 40 equals `ts`'s and, on a live row (bit 40 set), `prev < ts ^ k` over 40 bits; `ts`'s five slot bits are empty positions, forced zero, so the order check's `ts | k` is the `ts ^ k` the tuple carries. **Strictness is the soundness**: with `prev = ts ^ k` a read pulls the tuple it pushes and returns anything. The verdict goes to bit 41 of `step`, and the next clock is `ts ^ step`: one cycle on for a live row, `ts` itself otherwise, bit 41 set on a failure. Every timestamp port is 41 bits wide, so no row pulls a clock with bit 41, and the verifier requires the announced final clock to be live at slot zero with nothing above bit 40 (`CpuError::FinalClock`): a failed row leaves its next state unmatched, the exit row's included. A class with no circuit extends its table's clock circuit with ports of its own (`ClassSpec::clock_inputs`, `clock_outputs`, `ClassSpec::clock_circuit`, built on `tables::Clock::builder`). +- **A timestamp is an integer**, `2^40 | cycle << 5 | slot` read as the `K` word with those bits (`tables::SEED_CLOCK`, `CLOCK_START`, `LIVE_BIT`). **The clock rides the state tuple**, `(pc, ts)`, with slot zero, and a row's access in slot `k` carries `ts ^ k`, a column plus a constant, which is what lets one row touch the same cell twice (`add a0, a0, a0`). Slots are `rs1` at 0, `rs2` at 1, the RAM access at 2, `rd` at 3, and a row that skips an access leaves its slot unused (a load and a jump read no `rs2`, a store, a branch and a hash write no `rd`); a hash row's sixteen block words take slots 2 to 17. Seeds are at cycle 0 (`2^40`), so the run starts at cycle 1: an access must be strictly later than the one before. +- **Each table has a second flock circuit, its clock circuit** (`tables::clock_circuit`, reference `tables::clock_step`): ports the row's clock `ts`, each access's previous timestamp `prev`, and `step`, all virtual columns of the table, packed in a witness of its own (`class_flock::N_FLOCKS` is 27: every class circuit, `tables::N_CIRCUITS` of them, then every table's clock circuit). An access pulls `(addr, prev, old)` and pushes `(addr, ts ^ k, new)`; the circuit checks `prev`'s bit 40 equals `ts`'s and, on a live row (bit 40 set), `prev < ts ^ k` over 40 bits; `ts`'s five slot bits are empty positions, forced zero, so the order check's `ts | k` is the `ts ^ k` the tuple carries. **Strictness is the soundness**: with `prev = ts ^ k` a read pulls the tuple it pushes and returns anything. The verdict goes to bit 41 of `step`, and the next clock is `ts ^ step`: one cycle on for a live row, `ts` itself otherwise, bit 41 set on a failure. Every timestamp port is 41 bits wide, so no row pulls a clock with bit 41, and the verifier requires the announced final clock to be live at slot zero with nothing above bit 40 (`CpuError::FinalClock`): a failed row leaves its next state unmatched, the exit row's included. A class with no circuit extends its table's clock circuit with ports of its own (`ClassSpec::clock_inputs`, `clock_outputs`, `ClassSpec::clock_circuit`, built on `tables::Clock::builder`). - **Padding rows have clock zero**, which lacks the live bit: their clock does not advance, so their state tuples close around a fill block, and their access in slot `k` pulls and pushes timestamp `k`, cancelling itself. The live-bit equality is what keeps them away from the run: a padding row cannot pull a seed, and a live row cannot pull a padding row's tuple. They are written out by `cpu::Program::execute`, not executed, and touch no memory. **The verifier's notion of a padding row is a clock without the live bit and nothing else**, so a prover may close such rows around any cycle of the program's own control flow rather than a fill block; that is inert too, and the fill blocks exist to make the fill exact, not to make it safe. Any new table has to keep this true: every memory tuple's timestamp must be `ts ^ k` or a `prev` its clock circuit checks, nothing else. - **Two committed columns per array**: what it holds after the run, and each cell's last timestamp. What it holds before is public for the registers (zero) and RAM (`Coord::Sparse`: the image, then zeros, evaluated in time proportional to the image), and a third committed column for the advice (`ADV_INIT`), which is the prover's. RAM and the advice share `SEP_MEM`; they never share an address, every region's base being a multiple of its largest size (`rv::TEXT_BASE`, `rv::ADVICE_BASE`, `rv::RAM_BASE`), so word `z` of a region sits at `base ^ (z << 3)` and the seed block's address is the free `Coord::IntIndex`. - **A padding row rewrites what it writes**, its `old` column set to its `new` (the register write's `vd_old`, the hash's `out_old`), which is why a row can never update a cell in place: the hash reads `h` and writes `out` in different words, since no chaining value is a fixed point of the compression. - **A run is capped below `2^35 - 1` cycles** (`tables::MAX_CYCLES`): past that the cycle count would carry into the live bit. The executor refuses a longer run, and one commitment (`pcs::MAX_MU`) holds far fewer rows anyway. Soundness needs no row bound: a run whose clock wrapped could never reach a live final clock. -- `a_stale_read_unbalances_the_bus` is the soundness regression test (a forged run that serves an overwritten register), `a_forged_load_unbalances_the_bus` its RAM counterpart, `a_forged_store_unbalances_the_bus` the same for a store's `rs2` read (both for `ld`/`sd` and `lw`/`sw`), `a_doubleword_moves_its_value_unchanged` the binding of the word `LD` and `SD` move as a column, `a_misaligned_doubleword_names_no_cell` their bus address, `a_read_of_its_own_push_is_out_of_order`, `a_padding_row_cannot_pull_a_seed`, `a_live_row_cannot_pull_a_padding_tuple`, `the_final_clock_cannot_carry_a_failure` and `a_clock_with_slot_bits_cannot_read_its_own_push` (in `tables/clock.rs`) the clock circuit's checks, `a_write_to_x0_unbalances_the_bytecode_read` the zero in `x0` that a base-field operand's high limbs read, `a_forged_bytecode_read_unbalances_the_bus` and `a_wrong_multiplicity_unbalances_the_bus` (in `crates/leanvm_core/src/cpu/program.rs`) the bytecode lookup's, `a_forged_extension_product_is_refused` and `a_forged_extension_padding_row_is_refused` the extension-field identities' (a forged product whose bus balances, live and padding), `a_forged_extension_operand_unbalances_the_bus`, `a_misaligned_extension_operand_unbalances_the_bus` and `a_base_field_operand_has_no_high_limbs` its limbs' accesses, and `leaf::tests::unmatched_leaves` (test-only, taking the producer alongside the push and pull blocks) names the tuples a forged run leaves unmatched, which says more than a failing proof. `leanvm_core/tests/verifiers/programs.rs` holds the hand-assembled programs checked by both verifiers, `guests.rs` the Rust guests. +- `a_stale_read_unbalances_the_bus` is the soundness regression test (a forged run that serves an overwritten register), `a_forged_load_unbalances_the_bus` its RAM counterpart, `a_forged_store_unbalances_the_bus` the same for a store's `rs2` read (both for `ld`/`sd` and `lw`/`sw`), `a_forged_add_operand_unbalances_the_bus`, `a_forged_logic_operand_unbalances_the_bus` and `a_forged_jump_base_unbalances_the_bus` the same for ADD's `rs2`, LOGIC's `rs1` and JUMP's base (with the bit `jalr` clears, so the target forgets it), `a_doubleword_moves_its_value_unchanged` the binding of the word `LD` and `SD` move as a column, `a_misaligned_doubleword_names_no_cell` their bus address, `a_read_of_its_own_push_is_out_of_order`, `a_padding_row_cannot_pull_a_seed`, `a_live_row_cannot_pull_a_padding_tuple`, `the_final_clock_cannot_carry_a_failure` and `a_clock_with_slot_bits_cannot_read_its_own_push` (in `tables/clock.rs`) the clock circuit's checks, `a_write_to_x0_unbalances_the_bytecode_read` the zero in `x0` that a base-field operand's high limbs read, `a_forged_bytecode_read_unbalances_the_bus` and `a_wrong_multiplicity_unbalances_the_bus` (in `crates/leanvm_core/src/cpu/program.rs`) the bytecode lookup's, `a_forged_extension_product_is_refused` and `a_forged_extension_padding_row_is_refused` the extension-field identities' (a forged product whose bus balances, live and padding), `a_forged_extension_operand_unbalances_the_bus`, `a_misaligned_extension_operand_unbalances_the_bus` and `a_base_field_operand_has_no_high_limbs` its limbs' accesses, and `leaf::tests::unmatched_leaves` (test-only, taking the producer alongside the push and pull blocks) names the tuples a forged run leaves unmatched, which says more than a failing proof. `leanvm_core/tests/verifiers/programs.rs` holds the hand-assembled programs checked by both verifiers, `guests.rs` the Rust guests. ## The RISC-V machine `leanvm_core::rv` is the machine, `leanvm_core::tables` and `leanvm_core::cpu` prove it. What to keep in mind: -- **The program is public, so decoding is free.** `rv::Entry::decode` turns each word into an `Entry` once: an instruction class, a `flags` word selecting what the class's one function does, the three register cells the row touches, the immediate already sign-extended, and the branch or jump target. `LUI`, `AUIPC` and `JAL`'s link fold to constants added to `x0`, `JALR` is the ALU's flags `INDIRECT | ALWAYS`, `ECALL` is a jump to the halt slot, and everything rv64im does not define (reserved shift encodings, `EBREAK`, CSRs) is an illegal entry. The bytecode lookup returns those fields; no table ever decomposes an instruction word. An entry whose class has no table has tag zero, which no row can read. -- **The statement is about the decoded table**, so the rules that make it RISC-V are checked where a table enters, on both sides (`rv::Entry::is_well_formed` in `Program::new`, `check_bytecode` in Python): two registers below 32 are read, the cell written is in `1..=32`, the successor is `pc + 4`, the flags are ones the class defines, only a branch, a `jal` or the exit has a jump offset (`dt`), a `jal` reads `x0` twice and has `pc + 4` as its immediate, and a field a class's table holds at a constant has that value (a load's `rs2` is `x0`, a store's and a hash's `rd` is `SINK`, a hash's immediate is 0, an `ld`'s or an `sd`'s flags are 0). The proof system itself is sound for any table. -- **`x0` is hardwired by the decoder.** Every entry names two registers read and one cell written. An instruction with fewer reads `x0`; one with no destination, or with `rd = x0`, writes `RegisterFile::SINK` (cell 32), which nothing reads. So cell 0 is never written, and its seed is zero. A class whose `rs2` is always `x0` (LOAD, LD) or whose `rd` is always `SINK` (STORE, SD, HASH) makes no such access at all: its table reads the register number off the entry as a constant (`ClassSpec::reads_rs2`, `ClassSpec::writes_rd`), and the interpreter skips that write. +- **The program is public, so decoding is free.** `rv::Entry::decode` turns each word into an `Entry` once: an instruction class, a `flags` word selecting what the class's one function does, the three register cells the row touches, the immediate already sign-extended, and the branch or jump target. `LUI` and `AUIPC` fold to constants added to `x0`, `JAL` is a JUMP entry that reads `x0` and has immediate 0 (its link is the row's `pc4`), `JALR` is JUMP's flag `INDIRECT`, `ECALL` is a jump to the halt slot, and everything rv64im does not define (reserved shift encodings, `EBREAK`, CSRs) is an illegal entry. The bytecode lookup returns those fields; no table ever decomposes an instruction word. An entry whose class has no table has tag zero, which no row can read. +- **The statement is about the decoded table**, so the rules that make it RISC-V are checked where a table enters, on both sides (`rv::Entry::is_well_formed` in `Program::new`, `check_bytecode` in Python): two registers below 32 are read, the cell written is in `1..=32`, the successor is `pc + 4`, the flags are ones the class defines, the exit has one form, only a branch, a `jal` or the exit has a jump offset (`dt`), a `jal` reads `x0` and has immediate 0, and a field a class's table holds at a constant has that value (a load's and a jump's `rs2` is `x0`, a store's, a branch's and a hash's `rd` is `SINK`, a branch's and a hash's immediate is 0, an `ld`'s or an `sd`'s flags are 0). The proof system itself is sound for any table. +- **`x0` is hardwired by the decoder.** Every entry names two registers read and one cell written. An instruction with fewer reads `x0`; one with no destination, or with `rd = x0`, writes `RegisterFile::SINK` (cell 32), which nothing reads. So cell 0 is never written, and its seed is zero. A class whose `rs2` is always `x0` (LOAD, LD, JUMP) or whose `rd` is always `SINK` (STORE, SD, BRANCH, HASH) makes no such access at all: its table reads the register number off the entry as a constant (`ClassSpec::reads_rs2`, `ClassSpec::writes_rd`), and the interpreter skips that write. - **Registers are a read-write array of their own**, under their own separator `REG`, so that loads and stores cannot reach them: 64 cells, a public zero seed, committed final values and timestamps, the same clock and clock circuit as memory. A register's number comes straight from the bytecode, so an access needs no address arithmetic. - **No integer addition happens on the bus.** A load's or a store's address is its circuit's word, with the misalignment bits ORed back in (`rv::WordAccess::bus_address`), so a misaligned or out-of-range access names no seeded cell and the bus does not balance; a doubleword's misalignment bits are all three low ones, so `ld`'s and `sd`'s word is the sum itself (`rv::WordAccess::word_address`). A hash row's block words are at `v1 ^ 8k`, which is `Coord::Sum(Col(v1), Const(8k))`, the XOR being the sum in `K`. The `EXP` lookup of the leanISA days is gone. - **State is `(pc, ts)`**, `pc` the real byte address. Instruction `z` sits at `TEXT_BASE ^ (z << 2)` and the bytecode block's address coordinate is `Coord::IntIndex { base, shift }`, whose MLE is linear. Everything sits inside one 2 GiB window and below `0x7FFF_F800` for the code models' sake. A computed or misaligned jump target needs no check: the next row's bytecode read finds no entry. @@ -136,13 +136,13 @@ The registers, RAM and the advice are read-write, by timestamped offline memory Addition with carries, comparisons, shifts, AND/OR, multiplication and division are Boolean relations no degree-2 identity over `K` expresses, so each instruction class is a Boolean circuit proven by flock (`doc/leanvm` Annex C), and a table only does plumbing. The extension-field product is the exception: it is degree 2 over `K`, so its table states it as identities and has its clock circuit alone. -- **One generic table, specialized by a `tables::ClassSpec`**: the state step, the bytecode read, the `rs1` read, the `rs2` read and the `rd` write where `reads_rs2` and `writes_rd` say so (exactly when the table's circuits take `v2` and give `out`, or for `ClassSpec::copies` move the word, which `ClassTable::new` asserts), and the class's RAM accesses (`Ram::None`, one cell `Read` or `Write`n at the circuit's address, the hash's `Block`, or the extension-field `Limbs`), every successor linear: a row pushes `pc4`, or for the class with control flow (`ClassSpec::control`, the ALU: branches, `jal`, `jalr`, the exit) `pc4 + jump`, its circuit's output `jump = taken·(dt ^ indirect·(sum ^ pc4))` (bit 0 left out of the indirect part) gating the bytecode's offset bit by bit, and `rd` receives `out`, which a `jalr`'s circuit sets to `pc4`. **A table with a class circuit flushes only linear tuples** (`ClassTable::new` asserts it), so its columns but its register numbers are sent at the bus point `zeta[..tau]` and that share comes off the bus totals (`Layout::reduce_tables`): the table sumcheck runs EXT, the bytecode's producer and each such table's forms on its register numbers alone (`ClassTable::summed_columns`, `summed_form`). A new class is a spec, a circuit beside its reference function in `rv::semantics` returned by `Class::circuit`, its flag-word type and reference function in `rv::semantics` (`Alu`, `Div`, ...), a no-op word in `cpu::filler`, its decoding, and the same in Python (`Table(...)` in `TABLES`, its gate list, its flags in `check_bytecode`). A class with no circuit (`ClassSpec::circuit` is `None`) goes after the circuit tables (`N_CIRCUITS`, so packed witness `t` stays table `t`'s class circuit), states its function as `ClassTable::identities` (which `cpu::batch` weights at the powers of `xi` past the bus forms', in table order), and puts the Boolean checks it needs in its clock circuit through `clock_inputs`, `clock_outputs` and `ClassSpec::clock_circuit`; in Python its `Table` has `circuit=None`, the same clock ports and `clock_gates`, and its `identities`. -- **Every word the circuit reads or writes is a virtual column** of the table, living in the class's packed witness (`Q_BASE + t`, one committed column per table with a circuit, instance `j` being row `j`; the clock circuit's are at `Q_BASE + N_CIRCUITS + t`): `flags` and `imm` from the bytecode tuple, `v1` and `v2` from the register tuples, a load's `address` and `cell`, a hash's block words, `out`, an ALU's `dt`, `pc4` and `jump`. The bus is the whole binding. `FlockId::instance` asserts that what the circuit computed is what the interpreter did. A hint (`DIV`'s quotient and remainder) is a port in no column, and what a circuit asserts (`Word::Bad`) rides bytecode slot 10 (`tables::BAD_SLOT`), where the program is zero. **`LD` and `SD` (`ClassSpec::copies`) move a doubleword unchanged**, so their circuit is the address adder alone (`rv::Ld`'s, which `rv::Sd` shares, `k_log` 8) and the word moved is a committed column: `LD`'s `cell` is what its `rd` write pushes, `SD`'s `v2` what its RAM access pushes, one column on both tuples; their table has no flags column (the bytecode tuple holds 0). `LOAD` and `STORE` keep the narrower widths and make no gate for the 8-byte one: bit 2 of their bus address is empty, a load shifts only the cell's low half into place and a store only `v2`'s. -- **Circuits are gate lists over word ports** (`flock::circuit`): inputs, outputs, the constant, then products in the order they are made. A port bit with no gate is an empty row, hence zero, which is what makes a one-bit output such as EXT's flag bits a 0 or 1 field element: give such an output a word to itself and never put a free wire on its spare bits. What Rust and Python must agree on is the port layout and the ORDER PRODUCTS ARE MADE IN; XOR order is free. `alu_is_its_reference` pins a circuit to its reference function, and the end-to-end tests pin the Python mirror. -- **One batched reduction for all circuits, one opening for all**: one zerocheck and one lincheck over every packed witness under shared challenges (`flock::reduction::{prove, verify}`, `doc/leanvm` §flock:batch), every class circuit in table order then every clock circuit, after the exit claims, each circuit leaving a claim on its own witness. Both sumchecks are front-loaded like the table sumcheck: every circuit takes part from the first round and is done after its own rounds (the zerocheck binding each circuit's lowest variable first, lincheck its top inner coordinate, as for one circuit), and a done circuit adds only to the coefficient the round's claim fixes. Circuit `f`'s zerocheck takes `λ^f` and its lincheck `α^{4f}`; the zerocheck sends every circuit's `v_a, v_b, v_c` and checks their `λ`-combination. Lincheck sends each circuit's 64 slices, then the value of its matrices' form, and checks the batch's final claim against those values and each circuit's closed terms (pin and `C`); each value is left as that circuit's deferred matrix claim, so the verifier's core builds no circuit. A batch of one is how the recursion machine proves its hash rows. The zerocheck prover is a per-circuit state machine (`zerocheck::CircuitProver`) stepped one round at a time, so all twenty-one circuits' folded tables are alive at once. `pcs::stack_open` takes one ring-switched region per witness, then one for the bytecode's multiplicity column, then one per register word, and ring-switches all their claims as one family under one map challenge; claims whose points are prefixes of one another (the circuits of one block size) share one pass of the Frobenius products (`ring_switch::PrefixGroup`, also the rows' grouping, by wire), each region closing once. +- **One generic table, specialized by a `tables::ClassSpec`**: the state step, the bytecode read, the `rs1` read, the `rs2` read and the `rd` write where `reads_rs2` and `writes_rd` say so (exactly when the table's circuits take `v2` and give `out`, or for `ClassSpec::copies` move the word, or for a jump link `pc4`, which `ClassTable::new` asserts), and the class's RAM accesses (`Ram::None`, one cell `Read` or `Write`n at the circuit's address, the hash's `Block`, or the extension-field `Limbs`), every successor linear: a row pushes `pc4`, or for a class with control flow (`ClassSpec::control`, `Control::{None, Branch, Jump}`) `pc4 + jump`. `Control::Branch` (BRANCH) has the ports `dt` and `jump`, `jump = taken·dt` bit by bit, and no exit column: its bytecode tuple holds the sink, immediate 0 and exit selector 0. `Control::Jump` (JUMP: `jal`, `jalr`, the exit) has `dt`, `jump` and `pc4` as ports and the exit selector as a committed column, `jump = dt ^ indirect·((v1 + imm) ^ pc4)` (bit 0 left out of the indirect part), and its `rd` receives `pc4` itself, so it has no `out` (`ClassSpec::assert_valid`). What was the ALU is four classes, ADD, LOGIC, BRANCH and JUMP, so that a row pays only for the circuit it needs; their no-ops are `addi x0, x0, 0`, `andi x0, x0, 0`, `bne x0, x0, 0` (never taken) and `jal x0, 4` (a jump to the next instruction, so a block of them falls through), and every fill block's closing jump lands on JUMP (`cpu::filler::JUMP`), which is solved last. **A table with a class circuit flushes only linear tuples** (`ClassTable::new` asserts it), so its columns but its register numbers are sent at the bus point `zeta[..tau]` and that share comes off the bus totals (`Layout::reduce_tables`): the table sumcheck runs EXT, the bytecode's producer and each such table's forms on its register numbers alone (`ClassTable::summed_columns`, `summed_form`). A new class is a spec, a circuit beside its reference function in `rv::semantics` returned by `Class::circuit`, its flag-word type and reference function in `rv::semantics` (`Add`, `Div`, ...), a no-op word in `cpu::filler`, its decoding, and the same in Python (`Table(...)` in `TABLES`, its gate list, its flags in `check_bytecode`). A class with no circuit (`ClassSpec::circuit` is `None`) goes after the circuit tables (`N_CIRCUITS`, so packed witness `t` stays table `t`'s class circuit), states its function as `ClassTable::identities` (which `cpu::batch` weights at the powers of `xi` past the bus forms', in table order), and puts the Boolean checks it needs in its clock circuit through `clock_inputs`, `clock_outputs` and `ClassSpec::clock_circuit`; in Python its `Table` has `circuit=None`, the same clock ports and `clock_gates`, and its `identities`. +- **Every word the circuit reads or writes is a virtual column** of the table, living in the class's packed witness (`Q_BASE + t`, one committed column per table with a circuit, instance `j` being row `j`; the clock circuit's are at `Q_BASE + N_CIRCUITS + t`): `flags` and `imm` from the bytecode tuple, `v1` and `v2` from the register tuples, a load's `address` and `cell`, a hash's block words, `out`, a branch's or a jump's `dt` and `jump`, a jump's `pc4`. The bus is the whole binding. `FlockId::instance` asserts that what the circuit computed is what the interpreter did. A hint (`DIV`'s quotient and remainder) is a port in no column, and what a circuit asserts (`Word::Bad`) rides bytecode slot 10 (`tables::BAD_SLOT`), where the program is zero. **`LD` and `SD` (`ClassSpec::copies`) move a doubleword unchanged**, so their circuit is the address adder alone (`rv::Ld`'s, which `rv::Sd` shares, `k_log` 8) and the word moved is a committed column: `LD`'s `cell` is what its `rd` write pushes, `SD`'s `v2` what its RAM access pushes, one column on both tuples; their table has no flags column (the bytecode tuple holds 0). `LOAD` and `STORE` keep the narrower widths and make no gate for the 8-byte one: bit 2 of their bus address is empty, a load shifts only the cell's low half into place and a store only `v2`'s. +- **Circuits are gate lists over word ports** (`flock::circuit`): inputs, outputs, the constant, then products in the order they are made. A port bit with no gate is an empty row, hence zero, which is what makes a one-bit output such as EXT's flag bits a 0 or 1 field element: give such an output a word to itself and never put a free wire on its spare bits. What Rust and Python must agree on is the port layout and the ORDER PRODUCTS ARE MADE IN; XOR order is free. `every_alu_class_circuit_matches_its_reference` (`rv::semantics::alu`) pins ADD's, LOGIC's, BRANCH's and JUMP's circuits to their reference functions, and the end-to-end tests pin the Python mirror. +- **One batched reduction for all circuits, one opening for all**: one zerocheck and one lincheck over every packed witness under shared challenges (`flock::reduction::{prove, verify}`, `doc/leanvm` §flock:batch), every class circuit in table order then every clock circuit, after the exit claims, each circuit leaving a claim on its own witness. Both sumchecks are front-loaded like the table sumcheck: every circuit takes part from the first round and is done after its own rounds (the zerocheck binding each circuit's lowest variable first, lincheck its top inner coordinate, as for one circuit), and a done circuit adds only to the coefficient the round's claim fixes. Circuit `f`'s zerocheck takes `λ^f` and its lincheck `α^{4f}`; the zerocheck sends every circuit's `v_a, v_b, v_c` and checks their `λ`-combination. Lincheck sends each circuit's 64 slices, then the value of its matrices' form, and checks the batch's final claim against those values and each circuit's closed terms (pin and `C`); each value is left as that circuit's deferred matrix claim, so the verifier's core builds no circuit. A batch of one is how the recursion machine proves its hash rows. The zerocheck prover is a per-circuit state machine (`zerocheck::CircuitProver`) stepped one round at a time, so all twenty-seven circuits' folded tables are alive at once. `pcs::stack_open` takes one ring-switched region per witness, then one for the bytecode's multiplicity column, then one per register word, and ring-switches all their claims as one family under one map challenge; claims whose points are prefixes of one another (the circuits of one block size) share one pass of the Frobenius products (`ring_switch::PrefixGroup`, also the rows' grouping, by wire), each region closing once. - **A row's register numbers `a1`, `a2`, `ad` are not committed columns**: they are bit fields of a committed register word (`cpu::layout::RegisterWord`, in a register column after every table's span; `Source::Sliced`), five bits per register read and six for the cell written (the sink is 32), packed low first in that order, the fields the class has. Tables of one height share a word: in table order each joins the first word of its height with room, else opens one in its own register column (`RegisterWord::of`, `register_words` in Python), since they share their table-sumcheck point and so one ring-switched claim. The table sumcheck folds every table's numbers, a table the bus point settles keeping only those, so that all words sit at prefixes of its point: read at the bus point instead, they would be a second prefix group the opening and the rows pay for. It sends each number's bits' evaluations in place of its own (`constraints::BitColumns`), the verifier recombines `sum_b x^b s_b`, and each word's claim is its tables' slices in order, then zeros (`doc/leanvm` §sec:regpack). The bytecode lookup still binds the numbers; the opening binds the bits and zeroes the unused ones (`a_forged_register_number_unbalances_the_bus`, `a_packed_register_word_is_its_slices`). - **Batch floors.** Flock needs eight instances and a zerocheck cube of `2^13` bits for each of a table's circuits (`ClassSpec::n_blocks_log`); padding rows supply them, as honest instances on zero registers. -- **Witness generation is word arithmetic wherever a circuit has a generator, and the generic walk of the gate list, bit by bit, elsewhere**: ALU, LOAD, STORE, LD, SD, SHIFT, MULH and HASH fill by `Fill::Instance` (`ClassCircuit::fill`), MUL by `Fill::Batch8` on AVX2 only, and every clock circuit has one (`ClassSpec::clock_witness`: `Clock::witness`, and for EXT's, whose ports past the clock's split the flags and add 8 and 16 to the pointers, `Ext::clock_witness` on top of `Clock::witness_with`); DIV and MUL off AVX2 walk. Each generator computes the circuit's values natively and writes its rows in the order the circuit makes its products (all but the multipliers' through `rv::circuits::Products`), so a change to a circuit's gate list must change its generator too. Each is pinned to the walk by a test that covers edge words (zero, all ones, the sign bits, every shift amount, every misalignment) and random instances: `semantics::tests::word_witness_is_the_walk` for ALU, the memory classes and SHIFT, and their own for MUL, MULH, HASH and the clock circuits (`clock::tests::the_word_witness_is_the_gate_walk`, every table's, EXT's included). A new generator needs such a test. HASH's generator is unrolled, so every carry run's place is a constant. +- **Witness generation is word arithmetic wherever a circuit has a generator, and the generic walk of the gate list, bit by bit, elsewhere**: ADD, LOGIC, BRANCH, JUMP, LOAD, STORE, LD, SD, SHIFT, MULH and HASH fill by `Fill::Instance` (`ClassCircuit::fill`), MUL by `Fill::Batch8` on AVX2 only, and every clock circuit has one (`ClassSpec::clock_witness`: `Clock::witness`, and for EXT's, whose ports past the clock's split the flags and add 8 and 16 to the pointers, `Ext::clock_witness` on top of `Clock::witness_with`); DIV and MUL off AVX2 walk. Each generator computes the circuit's values natively and writes its rows in the order the circuit makes its products (all but the multipliers' through `rv::circuits::Products`), so a change to a circuit's gate list must change its generator too. Each is pinned to the walk by a test that covers edge words (zero, all ones, the sign bits, every shift amount, every misalignment) and random instances: `semantics::tests::word_witness_is_the_walk` for ADD, LOGIC, BRANCH and JUMP, the memory classes and SHIFT, and their own for MUL, MULH, HASH and the clock circuits (`clock::tests::the_word_witness_is_the_gate_walk`, every table's, EXT's included). A new generator needs such a test. HASH's generator is unrolled, so every carry run's place is a constant. - **Circuit sizes are structure, not measurements**: `k_log` (its `ClassCircuit`'s) and `clock_k_log` per class are pinned in its `ClassSpec` and asserted against the built circuits; product counts are in `doc/leanvm` Annex C. A product can be committed straight at an output port's position (`flock::circuit::Builder::and_output`), which saves the copy; the clock circuit's step uses it. CI compares every PR with its base, never with a history. The base is the merge commit's first parent; a workflow builds and runs both on one runner and saves both as an artifact, and a `workflow_run` workflow on the default branch (`main`, the only branch GitHub runs those from) posts them on the PR as one comment, edited on every run and deleted once nothing changed. The posting workflows never run the PR's code: they take only the PR number from a run's artifact, a fork's included, post nothing unless GitHub's API says that PR's head is the commit the run measured, and check every name and number before it reaches the comment. **Exact counts**: `counts.yml` runs `cargo leanvm bench --cycles-only`, every program at the sizes above without a proof (`cycles`, the program's own instructions; `proven-rows`, table heights after padding; `committed`, witness words) and the two aggregation trees above, one case per tree and kind of node (`aggregate-leanxmss-400-2to1-first` and `-node`, `aggregate-leanxmss-400-4to1-first` and `-node`, from `counted_trees()`: `rows`, the circuit's own; `proven-rows` and `committed` as for a program), puts the tables in each run's summary from the same pass (`--markdown-file "$GITHUB_STEP_SUMMARY"`, which appends what `--markdown` prints), saves the artifact `counts` and fails on any increase; `counts-comment.yml` posts the counts that changed. A tree's name says its shape, `Nto1` for N proofs combined into 1 at every node; `-first` is a first-level node (the RISC-V verifier in rows over N leaf proofs) and `-node` a higher node (the recursion verifier in rows over N child proofs). **Proving**: `bench.yml` runs one job per testbed and benchmark: each case of `proven()` in `bins/leanvm/src/tracked.rs` (at the sizes a 16 GB runner holds: leanXMSS, leanSPHINCS, Falcon, the state proofs and the shielded transfers at a quarter, no leanDA; leanXMSS also on one thread, `leanxmss-100-1thread`, which the CLI proves in a process of its own with `LEANVM_NUM_THREADS=1` since the pool is sized once per process), each of `proven_trees()` (the two aggregation trees above over leanXMSS at a quarter, `aggregate-leanxmss-100-2to1` and `aggregate-leanxmss-100-4to1`: the leaf proven once, then one first-level node and one node over copies of it, the two benchmarks `-first` and `-node`, each node's stages the children of a `Prove` span around it and the node's peak memory including the first-level node's; the 2-to-1 tree also on one thread, `aggregate-leanxmss-100-2to1-1thread`, proven whole, leaf included, in a process of its own like `leanxmss-100-1thread`), and each `benches/` target above with every benchmark it prints (flock's two at `FLOCK_N_LOG=18`, pcs's `throughput` at its default size). Each job builds both sides and runs them in turns, base, PR, PR, base, for `ROUNDS` rounds: `cargo leanvm bench --only ` gives the proving time, the proof's size in bytes (exact: the inputs are seeded and grinding takes the smallest nonce), the time of each of the proof's stages (`stage.`, the `Prove` span's direct children, `--tracing`'s first level, timed by a `tracing` layer that enables spans only), the process's peak resident memory (`peak-memory`, that case's alone since each job proves one), the proving passes' heap as the global allocator counts it (`heap-peak`, the most bytes live at once above those live when a pass began, and `allocations`, its allocations and reallocations, each the largest over the measured passes; host-side setup is outside them), and the verifying time, and a target's `--json` its own measures: `latency` for a whole operation (flock's proving times with the witness excluded, pcs's commit and open), `per-op` in nanoseconds per call for `kernels`, a hashed block of `hash_throughput` and one NTT encode. `bench-comment.yml` posts a size that changed and a time that moved the same way in every round with a median ratio at least 1% from one, every result collapsed beneath; it gates nothing. Run in turns on one runner, the comparison does not depend on which machine the job landed on, which a history across GitHub's runners does (one runner label spans CPU models of different speeds). The testbeds are GitHub-hosted: `x86-64` (built for `target-cpu=haswell`) and `arm64` (`ubuntu-24.04-arm`, `target-cpu=neoverse-n2` plus `+aes,+sha3`, since the NEON field kernels are chosen at compile time on those features and a generic aarch64 target enables neither; the job fails early if the CPU lacks them), each ISA pinned because a cached native build dies of SIGILL on an older CPU. A runner has 4 vCPUs, so a change to how the prover scales across many cores shows there only in part. A benchmark's name is what base and PR are matched by, so renaming one or changing its input shows it as new, as does one the base cannot run (it cannot build the target, or its first base run fails or prints no JSON, and the job carries on with the PR's runs alone). diff --git a/crates/leanvm_core/src/class_flock.rs b/crates/leanvm_core/src/class_flock.rs index 24dc43016..53dedaf9f 100644 --- a/crates/leanvm_core/src/class_flock.rs +++ b/crates/leanvm_core/src/class_flock.rs @@ -41,7 +41,7 @@ pub struct FlockId { impl FlockId { /// Every packed witness, in protocol order. pub const ALL: [Self; N_FLOCKS] = { - let mut all = [Self::clock(TableId::ALU); N_FLOCKS]; + let mut all = [Self::clock(TableId::ALL[0]); N_FLOCKS]; let mut t = 0; while t < N_TABLES { let table = TableId::ALL[t]; diff --git a/crates/leanvm_core/src/cpu/filler.rs b/crates/leanvm_core/src/cpu/filler.rs index 7062058da..aeb2b88ac 100644 --- a/crates/leanvm_core/src/cpu/filler.rs +++ b/crates/leanvm_core/src/cpu/filler.rs @@ -16,7 +16,7 @@ //! //! The rows therefore touch nothing, and the prover writes them out rather than executing them. //! -//! A traversal of the size-`s` block costs exactly `s + 1` rows: `s` of its table, and the jump, on the ALU. +//! A traversal of the size-`s` block costs exactly `s + 1` rows: `s` of its table, and the jump, on JUMP. //! //! That is what makes the solve exact, with no cost model and no residual to correct. @@ -27,15 +27,15 @@ use crate::tables::{N_TABLES, PerTable, TableId}; /// /// A fill of `f` rows takes `f / 128` traversals of the largest block, then one per set bit of the remainder. /// -/// The last, a lone jump, is the ALU's only: it makes a gap of a single row reachable. +/// The last, a lone jump, is JUMP's only: it makes a gap of a single row reachable. pub const SIZES: [usize; 9] = [128, 64, 32, 16, 8, 4, 2, 1, 0]; -/// The table of the closing jumps, the ALU. +/// The table of the closing jumps, JUMP. /// /// Every traversal of every block lands its closing jump there. /// /// So that table is solved last, absorbing the cost of the whole fill. -pub const JUMP: TableId = TableId::ALU; +pub const JUMP: TableId = TableId::JUMP; /// One block in the text: `size` no-ops of `table`'s class from entry `index`, then the jump back to `index`. #[derive(Clone, Debug, PartialEq, Eq)] @@ -72,7 +72,7 @@ impl FillBlocks { /// Append every table's blocks to `text`. /// - /// Each table gets a block per positive size, and the ALU the lone jump too. + /// Each table gets a block per positive size, and JUMP the lone jump too. pub fn append(text: &mut Vec) -> Self { let mut blocks = Vec::new(); for t in TableId::ALL { @@ -141,7 +141,7 @@ impl Traversals { fn delivering(fill: usize) -> Self { let mut left = fill; let out = SIZES.map(|size| { - // The lone jump supplies no rows to a non-ALU table. + // The lone jump supplies no rows to a table other than JUMP. if size == 0 { return 0; } @@ -153,15 +153,15 @@ impl Traversals { Self(out) } - /// The ALU's own traversals, landing exactly `gap` rows on it. + /// JUMP's own traversals, landing exactly `gap` rows on it. /// - /// A traversal of the size-`s` block gives the ALU `s + 1` rows: its no-ops and its own closing jump. + /// A traversal of the size-`s` block gives JUMP `s + 1` rows: its no-ops and its own closing jump. /// /// So the sizes to decompose over are `s + 1`, down to the lone jump's 1. fn landing_on_jump(gap: usize) -> Self { let mut left = gap; let out = SIZES.map(|size| { - // Each traversal contributes its closing jump to the ALU too. + // Each traversal contributes its closing jump to JUMP too. let count = left / (size + 1); left -= count * (size + 1); count @@ -187,9 +187,9 @@ pub struct Plan(PerTable); impl Plan { /// The plan taking every table from `base` rows to its provable height: the next power of two at or above its floor. /// - /// Every table but the ALU is independent: its fill is the distance to that height. + /// Every table but JUMP is independent: its fill is the distance to that height. /// - /// The ALU is not, since every traversal lands a row there, its own included. + /// JUMP is not, since every traversal lands a row there, its own included. /// /// Counting those first makes it one decomposition rather than a fixpoint. pub fn solve(base: PerTable) -> Self { @@ -199,7 +199,7 @@ impl Plan { plan.0[t] = Traversals::delivering(height(t, base[t]) - base[t]); } - // What the ALU already owes: its own rows, plus one per traversal so far. + // What JUMP already owes: its own rows, plus one per traversal so far. let owed = base[JUMP] + plan.traversals(); plan.0[JUMP] = Traversals::landing_on_jump(height(JUMP, owed) - owed); debug_assert!( @@ -236,13 +236,13 @@ mod tests { #[test] fn solve_reaches_each_tables_provable_height() { - // Fixture: empty, tiny, large and power-of-two runs, then ALU gaps of 3, 2 and 1 rows. + // Fixture: empty, tiny, large and power-of-two runs, then JUMP gaps of 3, 2 and 1 rows. // - // A gap of one row is what the other tables' closing jumps can leave the ALU with. + // A gap of one row is what the other tables' closing jumps can leave JUMP with. let mut cases: Vec<_> = [0, 1, 125_000, 1 << 17].map(|n| PerTable::new([n; N_TABLES])).into(); - for alu in [(1 << 17) - 3, (1 << 17) - 2, (1 << 17) - 1] { + for jumps in [(1 << 17) - 3, (1 << 17) - 2, (1 << 17) - 1] { let mut base = PerTable::new([1 << 10; N_TABLES]); - base[JUMP] = alu; + base[JUMP] = jumps; cases.push(base); } @@ -250,7 +250,7 @@ mod tests { let plan = Plan::solve(base); let got = plan.filled(base); - // Every table lands on the nearest provable height: what it owed, rounded up, the ALU owing the others' jumps too. + // Every table lands on the nearest provable height: what it owed, rounded up, JUMP owing the others' jumps too. for t in TableId::ALL { let spec = t.spec(); let jumps = if t == JUMP { diff --git a/crates/leanvm_core/src/cpu/layout.rs b/crates/leanvm_core/src/cpu/layout.rs index 46274bf94..d4a29d598 100644 --- a/crates/leanvm_core/src/cpu/layout.rs +++ b/crates/leanvm_core/src/cpu/layout.rs @@ -840,7 +840,7 @@ mod tests { fn multiplicity_bits_cover_every_read() { // Fixture: one table of 2^10 rows, the rest of 2^3. let mut taus = PerTable::new([3; N_TABLES]); - taus[TableId::ALU] = 10; + taus[TableId::ADD] = 10; let rows: u64 = taus.values().map(|&tau| 1u64 << tau).sum(); // The bits hold the most reads one entry can get, every row reading it, and no more. diff --git a/crates/leanvm_core/src/cpu/program.rs b/crates/leanvm_core/src/cpu/program.rs index 8a7c6cd52..578a8368b 100644 --- a/crates/leanvm_core/src/cpu/program.rs +++ b/crates/leanvm_core/src/cpu/program.rs @@ -42,7 +42,7 @@ const _: () = assert!(cfg!(target_endian = "little")); impl Program { /// The domain separator of the digest, versioned with the statement's format. - const DIGEST_DOMAIN: &'static [u8] = b"leanvm-rv64im-11"; + const DIGEST_DOMAIN: &'static [u8] = b"leanvm-rv64im-12"; /// The cycles between two checks of a running trace against one commitment. const SIZE_CHECK_PERIOD: u64 = 1 << 16; @@ -512,7 +512,7 @@ mod tests { use crate::pcs::Rate; use crate::rv::asm::*; use crate::rv::semantics::Outcome; - use crate::rv::{Alu, Class, Machine, ProgramError, Reg, RegisterFile, Trap}; + use crate::rv::{Class, Jump, Machine, ProgramError, Reg, RegisterFile, Trap}; use crate::tables::{ClassSpec, ClassTable, Clock, Separator}; use std::panic::AssertUnwindSafe; @@ -650,16 +650,27 @@ mod tests { ); } - /// Put `row` in place of a padding row of `ALU` that is the lone jump of its fill, a jump to itself. + /// Whether every tuple left unmatched is a state tuple of one of `tables`, or a framework block's in `framework`. + /// + /// A table's state tuples are its first block on each side. + fn only_states(w: &Witness, unmatched: &[(&str, usize, usize)], tables: &[TableId], framework: &[usize]) -> bool { + unmatched.iter().all(|&(side, block, _)| { + let blocks = if side == "push" { &w.layout.push } else { &w.layout.pull }; + framework.contains(&block) + || (tables.iter()).any(|&t| blocks.iter().position(|b| b.owner == Some(t.index())) == Some(block)) + }) + } + + /// Put `row` in place of a padding row of JUMP that is the lone jump of its fill, a jump to itself. /// /// Both are closed walks of one row at clock zero, so the state channel does not see the swap. fn replace_lone_jump(program: &Program, exec: &mut Execution, row: Row) { - let lone = program.filler.get(JUMP, 0).expect("ALU has a lone jump").index; - let at = exec.trace.rows[TableId::ALU] + let lone = program.filler.get(JUMP, 0).expect("JUMP has a lone jump").index; + let at = exec.trace.rows[JUMP] .iter() .position(|r| r.index as usize == lone) .expect("the fill traverses the lone jump"); - exec.trace.rows[TableId::ALU][at] = row; + exec.trace.rows[JUMP][at] = row; } /// The padding row a jump to itself makes, `jal rd, 0` at entry `index`, at clock zero. @@ -667,7 +678,7 @@ mod tests { let e = &program.rv.entries()[index]; let Outcome { out, taken, access } = e.evaluate(program.rv.pc_of(index), 0, 0, 0); let ram = access.unwrap_or_default(); - let slots: Vec = ClassSpec::ALU.slots().into_iter().map(u64::from).collect(); + let slots: Vec = ClassSpec::JUMP.slots().into_iter().map(u64::from).collect(); Row { index: index as u32, ts: 0, @@ -677,7 +688,7 @@ mod tests { taken, vd_old: program.rv.pc_of(index) + 4, ram, - prev: [slots[0], slots[1], slots[2], 0], + prev: [slots[0], slots[1], 0, 0], } } @@ -746,41 +757,40 @@ mod tests { let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid jump program"); assert!(matches!(program.execute(&[]), Err(ProveError::Trap(Trap::Illegal { pc })) if pc == halt)); - // Mutation: the exit's row becomes the jump's, bypassing the interpreter's trap; it writes its link to the sink. - let mut execution = honest_program.execute(&[]).unwrap(); - let row = execution.trace.rows[TableId::ALU] - .iter_mut() + // Mutation: the exit's row becomes the jump's, bypassing the interpreter's trap; each links `pc + 4` into the + // sink. + let execution = honest_program.execute(&[]).unwrap(); + let jump = TableId::JUMP; + let row = execution.trace.rows[jump] + .iter() .find(|r| r.index as usize == exit_index) .unwrap(); - row.out = pc + 4; - execution.trace.reg_fin[RegisterFile::SINK as usize] = F64(pc + 4); + assert_eq!(row.out, pc + 4); let witness = Witness::build(&program, &execution); let unmatched = unmatched(&witness); - // The final state on the pull side, and the ALU's state push, the push side's - // first block past its four framework blocks. + // The final state on the pull side, the first framework block, and the jump's state push. assert_eq!(unmatched.len(), 2, "{unmatched:?}"); - assert!(unmatched.iter().all(|(_, block, _)| *block == 0 || *block == 4)); + assert!(only_states(&witness, &unmatched, &[jump], &[0]), "{unmatched:?}"); assert_unbalanced(&program, witness, execution.output.into()); } - /// The jump's column on the ALU's state push, `pc + 4` plus the jump: a port of its class circuit. - fn jump_column() -> usize { - let alu = TableId::ALU; - let push = alu.class_table().flushes().push.swap_remove(0); + /// The jump's column on table `t`'s state push, `pc + 4` plus the jump: a port of its class circuit. + fn jump_column(t: TableId) -> usize { + let push = t.class_table().flushes().push.swap_remove(0); let Coord::Sum(terms) = &push[1] else { panic!("pc + 4 plus the jump") }; let [_, Coord::Col(jump)] = terms[..] else { panic!("pc + 4 plus the jump") }; - Schema::get().spans[alu].0 + jump + Schema::get().spans[t].0 + jump } - /// Prove a forged run of `program` whose ALU jump at `row` is `value` on the bus alone, the circuit's witness keeping - /// what its inputs give. + /// Prove a forged run of `program` whose jump at `row` of table `t` is `value` on the bus alone, the circuit's + /// witness keeping what its inputs give. /// /// The bus is unbalanced until that column is forged, and balanced after, so what refuses it is the verifier. - fn forged_jump(program: &Program, forged: &Execution, row: usize, value: u64) -> CpuError { + fn forged_jump(program: &Program, forged: &Execution, t: TableId, row: usize, value: u64) -> CpuError { let mut w = Witness::build(program, forged); // The row's state push, and the next row's pull. let left = unmatched(&w); @@ -789,7 +799,7 @@ mod tests { left.iter().all(|&(_, block, _)| block >= Framework::ALL.len()), "{left:?}" ); - column_mut(&mut w, jump_column())[row] = F64(value); + column_mut(&mut w, jump_column(t))[row] = F64(value); assert!(unmatched(&w).is_empty()); let proof = program.prove_witness(w, forged.output.into(), Rate::MIN); program @@ -818,10 +828,10 @@ mod tests { // // Its push names `pc + 4`, which the exit's pull does not meet, until the bus's jump is forged to the offset. let mut forged = taken.execute(&[]).unwrap(); - let alu = TableId::ALU; - let row = forged.trace.rows[alu].iter().position(|r| r.index == 0).unwrap(); - forged.trace.rows[alu][row].taken = false; - let error = forged_jump(&program, &forged, row, program.rv.dt_of(0)); + let branch = TableId::BRANCH; + let row = forged.trace.rows[branch].iter().position(|r| r.index == 0).unwrap(); + forged.trace.rows[branch][row].taken = false; + let error = forged_jump(&program, &forged, branch, row, program.rv.dt_of(0)); assert!(matches!(error, CpuError::Open(_)), "{error}"); } @@ -848,16 +858,16 @@ mod tests { // // Its push names `L`, which the exit's pull does not meet, until the bus's jump is forged to the exit's. let forged = skipping.execute(&[]).unwrap(); - let alu = TableId::ALU; + let jump = TableId::JUMP; let jalr = (0..) - .find(|&i| program.rv.entries()[i].flags == Alu::INDIRECT | Alu::ALWAYS) + .find(|&i| (program.rv.entries()[i].class, program.rv.entries()[i].flags) == (Class::Jump, Jump::INDIRECT)) .unwrap(); - let row = forged.trace.rows[alu] + let row = forged.trace.rows[jump] .iter() .position(|r| r.index as usize == jalr && r.ts != 0) .unwrap(); let pc4 = program.rv.pc_of(jalr) + 4; - let error = forged_jump(&program, &forged, row, (target + 4) ^ pc4); + let error = forged_jump(&program, &forged, jump, row, (target + 4) ^ pc4); assert!(matches!(error, CpuError::Open(_)), "{error}"); } @@ -963,10 +973,10 @@ mod tests { // // addi writes x0 after its own read of it in slot 1; t3 keeps its seed // ext reads b = (9, 1, 1), and c and RAM follow it - // ecall reads 1 twice, and writes 1 + 1 to the sink + // ecall reads 1, and links into the sink as before let mut forged = program.execute(&[]).unwrap(); - let alu = TableId::ALU; - let write = forged.trace.rows[alu].iter_mut().find(|r| r.index == addi).unwrap(); + let add = TableId::ADD; + let write = forged.trace.rows[add].iter_mut().find(|r| r.index == addi).unwrap(); let ts = write.ts; (write.prev[2], write.vd_old) = (ts | 1, 0); let t3 = Reg::T3.index(); @@ -980,24 +990,24 @@ mod tests { for (k, word) in x.c.into_iter().enumerate() { forged.trace.ram_fin[4 + k] = F64(word); } - let exit = forged.trace.rows[alu].iter_mut().find(|r| r.index == ecall).unwrap(); - (exit.v1, exit.v2, exit.out) = (1, 1, 2); + let jump = TableId::JUMP; + let exit = forged.trace.rows[jump].iter_mut().find(|r| r.index == ecall).unwrap(); + exit.v1 = 1; forged.trace.reg_fin[0] = F64(1); - forged.trace.reg_fin[RegisterFile::SINK as usize] = F64(2); let mut w = Witness::build(&program, &forged); - let bus = alu.class_table().flushes(); + let bus = add.class_table().flushes(); let Coord::Col(destination) = bus.pull[1][ClassTable::DESTINATION_SLOT] else { - panic!("the ALU binds its destination to a column"); + panic!("ADD binds its destination to a column"); }; - let row = forged.trace.rows[alu].iter().position(|r| r.index == addi).unwrap(); + let row = forged.trace.rows[add].iter().position(|r| r.index == addi).unwrap(); // The destination is a register number: its column and its field of the packed word both name `x0`. - virtual_mut(&mut w, Schema::get().spans[alu].0 + destination)[row] = F64::ZERO; - // The ALU's fields come first in its word, so its destination's sits after the reads'. - let fields = alu.class_table().register_bits().fields; + virtual_mut(&mut w, Schema::get().spans[add].0 + destination)[row] = F64::ZERO; + // ADD's fields come first in its word, so its destination's sits after the reads'. + let fields = add.class_table().register_bits().fields; let at = fields.iter().position(|f| f.col == destination).unwrap(); let shift: usize = fields[..at].iter().map(|f| f.width).sum(); let mask = (1 << fields[at].width) - 1; - column_mut(&mut w, Schema::get().registers[alu])[row].0 &= !(mask << shift); + column_mut(&mut w, Schema::get().registers[add])[row].0 &= !(mask << shift); column_mut(&mut w, Shared::BytecodeMult.col())[addi as usize].0 -= 1; // Registers, RAM and the multiplicities balance: only the read of an entry whose destination is 0 is left. @@ -1179,6 +1189,87 @@ mod tests { } } + /// The run's row of entry `index` in table `t`. + fn row_of(exec: &mut Execution, t: TableId, index: usize) -> &mut Row { + exec.trace.rows[t] + .iter_mut() + .find(|r| r.index as usize == index && r.ts != 0) + .expect("the entry ran in the table") + } + + #[test] + fn a_forged_add_operand_unbalances_the_bus() { + // Invariant: an `ADD` row cannot use a value its `rs2` does not hold. + // + // Fixture state: `t0 = 5` and `t1 = 3`, then `a0 = t0 + t1`. + // Mutation: the add reads 4 from `t1`, and its result, `a0` and the output follow it, so its circuit's instance + // is honest. Only the read of `t1` is left to refuse it: it meets neither `t1`'s write nor its final value. + let text = Asm::new() + .i(Addi, Reg::T0, Reg::ZERO, 5) + .i(Addi, Reg::T1, Reg::ZERO, 3) + .r(Add, Reg::A0, Reg::T0, Reg::T1) + .exit() + .finish(); + let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); + let mut forged = program.execute(&[]).unwrap(); + let row = row_of(&mut forged, TableId::ADD, 2); + assert_eq!((row.v2, row.out), (3, 8)); + (row.v2, row.out) = (4, 9); + forged.output[0] = 9; + forged.trace.reg_fin[Reg::A0.index()] = F64(9); + // Two tuples on each side: the read's pull and push. + let unmatched = unmatched_run(&program, &forged); + assert_eq!(unmatched.len(), 4, "{unmatched:?}"); + } + + #[test] + fn a_forged_logic_operand_unbalances_the_bus() { + // Invariant: a `LOGIC` row cannot use a value its `rs1` does not hold. + // + // Fixture state: `t0 = 5`, then `a0 = t0 ^ 3`. + // Mutation: the XOR reads 6 from `t0`, and its result, `a0` and the output follow it, so its circuit's instance + // is honest. Only the read of `t0` is left to refuse it: it meets neither `t0`'s write nor its final value. + let text = Asm::new() + .i(Addi, Reg::T0, Reg::ZERO, 5) + .i(Xori, Reg::A0, Reg::T0, 3) + .exit() + .finish(); + let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); + let mut forged = program.execute(&[]).unwrap(); + let row = row_of(&mut forged, TableId::LOGIC, 1); + assert_eq!((row.v1, row.out), (5, 6)); + (row.v1, row.out) = (6, 5); + forged.output[0] = 5; + forged.trace.reg_fin[Reg::A0.index()] = F64(5); + // Two tuples on each side: the read's pull and push. + let unmatched = unmatched_run(&program, &forged); + assert_eq!(unmatched.len(), 4, "{unmatched:?}"); + } + + #[test] + fn a_forged_jump_base_unbalances_the_bus() { + // Invariant: a `JUMP` row cannot read a value its `rs1` does not hold, even one the target it computes forgets. + // + // Fixture state: `t0` is the address of the exit, which `jalr x0, 0(t0)` jumps to. + // Mutation: the jump reads `t0` with bit 0 set, which `JALR` clears: its target, so every other tuple, and its + // circuit's instance are the honest ones. Only the read of `t0` is left to refuse it. + let text = Asm::new() + .auipc(Reg::T0, 0) + .i(Addi, Reg::T0, Reg::T0, 12) + .jalr(Reg::ZERO, Reg::T0, 0) + .exit() + .finish(); + let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); + let mut forged = program.execute(&[]).unwrap(); + let target = program.rv.pc_of(3); + let row = row_of(&mut forged, TableId::JUMP, 2); + assert_eq!(row.v1, target); + row.v1 = target | 1; + // Two tuples on each side: the read's pull and push. + let unmatched = unmatched_run(&program, &forged); + assert_eq!(unmatched.len(), 4, "{unmatched:?}"); + } + #[test] fn a_doubleword_moves_its_value_unchanged() { // Invariant: a doubleword load's `rd` receives the cell it reads, and a doubleword store's cell the `v2` it reads. @@ -1264,7 +1355,7 @@ mod tests { .expect("the honest run verifies"); let mut forged = program.execute(&[]).unwrap(); - let row = &mut forged.trace.rows[TableId::ALU][3]; + let row = &mut forged.trace.rows[TableId::ADD][3]; // The read happens at cycle 4; the first write happened at cycle 1, the second at 2, each in slot 3. let write = |cycle: u64| Clock::SEED_CLOCK | (cycle * Clock::CYCLE) | 3; assert_eq!((row.v1, row.prev[0]), (9, write(2))); @@ -1288,20 +1379,27 @@ mod tests { /// the multiplicities for what the rows now read leaves its bytecode read unmatched. #[test] fn a_forged_bytecode_read_unbalances_the_bus() { - let text = Asm::new().i(Addi, Reg::A0, Reg::ZERO, 5).exit().finish(); + // Fixture: `a0 = 5`, then `beq a0, x0`, not taken. + let text = Asm::new() + .i(Addi, Reg::A0, Reg::ZERO, 5) + .branch(Beq, Reg::A0, Reg::ZERO, "skip") + .i(Addi, Reg::A1, Reg::ZERO, 1) + .label("skip") + .exit() + .finish(); let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); let exec = program.execute(&[]).unwrap(); - let alu = TableId::ALU; - let row = exec.trace.rows[alu].iter().position(|r| r.index == 0).unwrap(); + let branch = TableId::BRANCH; + let row = exec.trace.rows[branch].iter().position(|r| r.index == 1).unwrap(); let mut w = Witness::build(&program, &exec); // Bytecode slot 9 binds the decoded branch target offset. - let bus = alu.class_table().flushes(); + let bus = branch.class_table().flushes(); let Coord::Col(branch_offset) = bus.pull[1][9] else { - panic!("the ALU binds its branch offset to a column"); + panic!("BRANCH binds its branch offset to a column"); }; - let offset = Schema::get().spans[alu].0 + branch_offset; + let offset = Schema::get().spans[branch].0 + branch_offset; column_mut(&mut w, offset)[row] = F64(8); - column_mut(&mut w, Shared::BytecodeMult.col())[0].0 -= 1; + column_mut(&mut w, Shared::BytecodeMult.col())[1].0 -= 1; let unmatched = unmatched(&w); assert_eq!(unmatched.len(), 1, "{unmatched:?}"); @@ -1353,17 +1451,17 @@ mod tests { 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 mut forged = program.execute(&[]).unwrap(); - let alu = TableId::ALU; - let row = forged.trace.rows[alu].iter().position(|r| r.index == 0).unwrap(); - let addi = &mut forged.trace.rows[alu][row]; + let add = TableId::ADD; + let row = forged.trace.rows[add].iter().position(|r| r.index == 0).unwrap(); + let addi = &mut forged.trace.rows[add][row]; assert_eq!(addi.prev[..2], [Clock::SEED_CLOCK, addi.ts]); addi.prev[1] = Clock::SEED_CLOCK; forged.trace.reg_ts[Reg::RA.index()] = F64(addi.ts); let mut w = Witness::build(&program, &forged); - let table = alu.class_table(); - let a1 = Schema::get().spans[alu].0 + table.register_bits().fields[0].col; + let fields = add.class_table().register_bits().fields; + let a1 = Schema::get().spans[add].0 + fields[0].col; virtual_mut(&mut w, a1)[row] = F64(Reg::RA.index() as u64); - column_mut(&mut w, Schema::get().registers[alu])[row].0 ^= Reg::RA.index() as u64; + column_mut(&mut w, Schema::get().registers[add])[row].0 ^= Reg::RA.index() as u64; // The entry's count follows the reads, which no longer include this one. column_mut(&mut w, Shared::BytecodeMult.col())[0].0 -= 1; @@ -1386,15 +1484,15 @@ mod tests { 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 exec = program.execute(&[]).unwrap(); - let alu = TableId::ALU; - let row = exec.trace.rows[alu].iter().position(|r| r.index == 0).unwrap(); - // The ALU opens its word, which the tables of its height share after it. + let add = TableId::ADD; + let row = exec.trace.rows[add].iter().position(|r| r.index == 0).unwrap(); + // ADD opens its word, which the tables of its height share after it. let word = Witness::build(&program, &exec).layout.registers.swap_remove(0); - assert_eq!(word.tables[0], alu); + assert_eq!(word.tables[0], add); assert!(word.tables.len() > 1, "the tables of one height share the word"); let bits = |t: TableId| t.class_table().register_bits().n_slices(); let used: usize = word.tables.iter().map(|&t| bits(t)).sum(); - for bit in [0, bits(alu), used, 63] { + for bit in [0, bits(add), used, 63] { let mut w = Witness::build(&program, &exec); column_mut(&mut w, word.col)[row].0 ^= 1 << bit; assert!( @@ -1426,15 +1524,17 @@ mod tests { .finish(); let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); let mut forged = program.execute(&[]).unwrap(); - let row = &mut forged.trace.rows[TableId::ALU][1]; + let (add, jump) = (TableId::ADD, TableId::JUMP); + let row = &mut forged.trace.rows[add][1]; (row.v1, row.out, row.prev[0]) = (9, 9, row.ts); forged.output[0] = 9; forged.trace.reg_fin[Reg::A0.index()] = F64(9); forged.trace.reg_ts[Reg::T0.index()] = F64(Clock::CLOCK_START | 3); - // The read's row pushes a failed clock, which the next row's pull does not meet. - let unmatched = unmatched_run(&program, &forged); + // The read's row pushes a failed clock, which the next row's pull, the exit's, does not meet. + let w = Witness::build(&program, &forged); + let unmatched = unmatched(&w); assert_eq!(unmatched.len(), 2, "{unmatched:?}"); - assert!(unmatched.iter().all(|&(_, block, _)| block == Framework::ALL.len())); + assert!(only_states(&w, &unmatched, &[add, jump], &[]), "{unmatched:?}"); } #[test] @@ -1443,7 +1543,7 @@ mod tests { // // Fixture state: the run sets `a0 = 42` and exits, never touching `a1`. // Past the exit sits `jal a1, 0`, a jump to itself, which the run never reaches. - // The two no-ops size ALU's fill so that it ends on the lone jump. + // The two no-ops size the other tables' fill so that JUMP's ends on the lone jump. // Mutation: a padding instance of it takes the place of the fill's lone jump, its write pulling `a1`'s seed. // `a1`'s final value is what it pushes, so the output claims `a1 = pc + 4`. let text = Asm::new() @@ -1458,16 +1558,17 @@ mod tests { let mut forged = program.execute(&[]).unwrap(); let spin = text.len() - 1; let mut row = padding_jump(&program, spin); - (row.prev[2], row.vd_old) = (Clock::SEED_CLOCK, 0); + (row.prev[1], row.vd_old) = (Clock::SEED_CLOCK, 0); replace_lone_jump(&program, &mut forged, row); let link = program.rv.pc_of(spin) + 4; forged.output[1] = link; forged.trace.reg_fin[Reg::A1.index()] = F64(link); forged.trace.reg_ts[Reg::A1.index()] = F64(3); // The row's failed clock leaves its own state tuples unmatched, and nothing else. - let unmatched = unmatched_run(&program, &forged); + let w = Witness::build(&program, &forged); + let unmatched = unmatched(&w); assert_eq!(unmatched.len(), 2, "{unmatched:?}"); - assert!(unmatched.iter().all(|&(_, block, _)| block == Framework::ALL.len())); + assert!(only_states(&w, &unmatched, &[JUMP], &[]), "{unmatched:?}"); } #[test] @@ -1475,15 +1576,13 @@ mod tests { // Invariant: a row of the run pulls only timestamps of the run, which have the live bit. // // Fixture state: `t0 = 5`, then `a0 = t0 + x0`; past the exit sits `jal t0, 0`, a jump to itself. - // The two no-ops size ALU's fill so that it ends on the lone jump. + // Its rows size the other tables' fill so that JUMP's ends on the lone jump. // Mutation: a padding instance of the jump pulls `t0`'s write and pushes `(t0, 3, pc + 4)`, which the run's read pulls. // The read's `prev` is 3, live bit clear, and the output claims `a0 = pc + 4`. let text = Asm::new() .i(Addi, Reg::T0, Reg::ZERO, 5) .r(Add, Reg::A0, Reg::T0, Reg::ZERO) .i(Addi, Reg::T1, Reg::ZERO, 0) - .i(Addi, Reg::ZERO, Reg::ZERO, 0) - .i(Addi, Reg::ZERO, Reg::ZERO, 0) .exit() .label("spin") .jal(Reg::T0, "spin") @@ -1492,19 +1591,21 @@ mod tests { let mut forged = program.execute(&[]).unwrap(); let spin = text.len() - 1; let link = program.rv.pc_of(spin) + 4; - let read = &mut forged.trace.rows[TableId::ALU][1]; + let add = TableId::ADD; + let read = &mut forged.trace.rows[add][1]; let write = read.prev[0]; (read.v1, read.out, read.prev[0]) = (link, link, 3); let mut row = padding_jump(&program, spin); - (row.prev[2], row.vd_old) = (write, 5); + (row.prev[1], row.vd_old) = (write, 5); replace_lone_jump(&program, &mut forged, row); forged.output[0] = link; forged.trace.reg_fin[Reg::A0.index()] = F64(link); forged.trace.reg_fin[Reg::T0.index()] = F64(link); // Both rows push failed clocks: the read's, and the padding row's, each a state tuple pushed and one not pulled. - let unmatched = unmatched_run(&program, &forged); + let w = Witness::build(&program, &forged); + let unmatched = unmatched(&w); assert_eq!(unmatched.len(), 4, "{unmatched:?}"); - assert!(unmatched.iter().all(|&(_, block, _)| block == Framework::ALL.len())); + assert!(only_states(&w, &unmatched, &[add, JUMP], &[]), "{unmatched:?}"); } #[test] @@ -1517,11 +1618,8 @@ mod tests { let text = Asm::new().i(Addi, Reg::A0, Reg::ZERO, 42).exit().finish(); let program = Program::new(&text, Region::TEXT.base(), vec![], 2, 0).expect("valid instruction program"); let mut forged = program.execute(&[]).unwrap(); - let exit = forged.trace.rows[TableId::ALU] - .iter_mut() - .find(|r| r.index == 2) - .unwrap(); - (exit.prev[2], exit.vd_old) = (exit.ts | 3, exit.out); + let exit = forged.trace.rows[JUMP].iter_mut().find(|r| r.index == 2).unwrap(); + (exit.prev[1], exit.vd_old) = (exit.ts | 3, exit.out); let sink = RegisterFile::SINK as usize; (forged.trace.reg_ts[sink], forged.trace.reg_fin[sink]) = (F64(Clock::SEED_CLOCK), F64::ZERO); forged.trace.ts_final |= 1 << Clock::FAIL_BIT; diff --git a/crates/leanvm_core/src/cpu/proof.rs b/crates/leanvm_core/src/cpu/proof.rs index 71b707502..3e4d339fa 100644 --- a/crates/leanvm_core/src/cpu/proof.rs +++ b/crates/leanvm_core/src/cpu/proof.rs @@ -17,7 +17,7 @@ impl Proof { /// The header of a proof's bytes: the magic `LVMP`, then the protocol version. /// /// The version is bumped by every change to what a proof says. - const ENVELOPE: Envelope = Envelope::new(*b"LVMP", 13); + const ENVELOPE: Envelope = Envelope::new(*b"LVMP", 14); /// The proof's bytes. #[must_use] diff --git a/crates/leanvm_core/src/lib.rs b/crates/leanvm_core/src/lib.rs index 0c56607a1..9c18fb069 100644 --- a/crates/leanvm_core/src/lib.rs +++ b/crates/leanvm_core/src/lib.rs @@ -57,7 +57,7 @@ pub use cpu::{CpuError, DeferredClaims, Lookup, MAX_LOG_ROWS, MalformedClaim, Q_ #[doc(hidden)] pub use leaf::{BusError, N_TUPLE_BITS}; #[doc(hidden)] -pub use rv::{Alu, Class, Guest, Hash, Machine, Reg, RegisterFile, Syscall}; +pub use rv::{Add, Branch, Class, Guest, Hash, Jump, Logic, Machine, Reg, RegisterFile, Syscall}; #[doc(hidden)] pub use tables::{BAD_SLOT, Clock, EXIT_SLOT, Fill, N_TABLES, PerTable, TableId}; diff --git a/crates/leanvm_core/src/rec/tree/design.rs b/crates/leanvm_core/src/rec/tree/design.rs index 81d308aad..540aa2053 100644 --- a/crates/leanvm_core/src/rec/tree/design.rs +++ b/crates/leanvm_core/src/rec/tree/design.rs @@ -27,7 +27,7 @@ use primitives::hash::Hasher; use primitives::multilinear::mle_eval_par; /// The domain of every tree proof's transcript. -const DOMAIN: &[u8] = b"leanvm-tree-6"; +const DOMAIN: &[u8] = b"leanvm-tree-9"; /// What fixes a tree's circuits: the leaves' shape, the arities, the rate, and the nodes' heights. pub(crate) struct Design<'p> { diff --git a/crates/leanvm_core/src/rec/tree/mod.rs b/crates/leanvm_core/src/rec/tree/mod.rs index da06e0caa..8e12792dc 100644 --- a/crates/leanvm_core/src/rec/tree/mod.rs +++ b/crates/leanvm_core/src/rec/tree/mod.rs @@ -306,7 +306,7 @@ impl TreeProof { /// The header of a tree proof's bytes: the magic `LVMT`, then the tree protocol's version. /// /// The version is bumped by every change to what a tree proof says. - const ENVELOPE: Envelope = Envelope::new(*b"LVMT", 10); + const ENVELOPE: Envelope = Envelope::new(*b"LVMT", 12); /// The kind of node that made the proof. #[must_use] diff --git a/crates/leanvm_core/src/rec/tree/tests.rs b/crates/leanvm_core/src/rec/tree/tests.rs index 79b453225..08813023b 100644 --- a/crates/leanvm_core/src/rec/tree/tests.rs +++ b/crates/leanvm_core/src/rec/tree/tests.rs @@ -495,7 +495,7 @@ fn forged_reduced_claims_are_refused() { ( Forge::Matrix, FalseClaim::Matrix { - table: TableId::ALU.name(), + table: TableId::ADD.name(), part: Part::Class, }, ), diff --git a/crates/leanvm_core/src/rv/asm.rs b/crates/leanvm_core/src/rv/asm.rs index f17e1bfe9..ab835efc4 100644 --- a/crates/leanvm_core/src/rv/asm.rs +++ b/crates/leanvm_core/src/rv/asm.rs @@ -247,7 +247,7 @@ mod tests { let entry = |i: usize| Entry::decode(text[i], Region::TEXT.base() + 4 * i as u64); assert_eq!(entry(0).target, Target::Abs(Region::TEXT.base())); assert_eq!(entry(1).target, Target::Abs(Region::TEXT.base() + 12)); - assert_eq!(entry(2).class, Class::Alu); + assert_eq!(entry(2).class, Class::Add); } #[test] diff --git a/crates/leanvm_core/src/rv/circuits.rs b/crates/leanvm_core/src/rv/circuits.rs index 81cb3219f..d8a763bbc 100644 --- a/crates/leanvm_core/src/rv/circuits.rs +++ b/crates/leanvm_core/src/rv/circuits.rs @@ -211,10 +211,10 @@ impl<'a> Products<'a> { } } - /// The next 192 rows, three per bit of three words: row `3i + k` has `A·z` bit `i` of `a[k]` and `B·z` bit `i` of `b[k]`. + /// The next 128 rows, two per bit of two words: row `2i + k` has `A·z` bit `i` of `a[k]` and `B·z` bit `i` of `b[k]`. #[inline(always)] - pub(crate) fn push_interleaved3(&mut self, a: [u64; 3], b: [u64; 3]) { - for (a, b) in interleave3(a).into_iter().zip(interleave3(b)) { + pub(crate) fn push_interleaved2(&mut self, a: [u64; 2], b: [u64; 2]) { + for (a, b) in interleave2(a).into_iter().zip(interleave2(b)) { self.push(a, b, 64); } } @@ -230,40 +230,34 @@ impl<'a> Products<'a> { } } -/// The 192 bits `x0_0, x1_0, x2_0, x0_1, ...` of three words, as three words. +/// The 128 bits `x0_0, x1_0, x0_1, ...` of two words, as two words. #[inline(always)] -fn interleave3([x, y, w]: [u64; 3]) -> [u64; 3] { - // Word `j` starts at bit 64j of the sequence, which is bit `64j / 3` of the word at `64j mod 3`. - [ - spread3(x) | spread3(y) << 1 | spread3(w) << 2, - spread3(y >> 21) | spread3(w >> 21) << 1 | spread3(x >> 22) << 2, - spread3(w >> 42) | spread3(x >> 43) << 1 | spread3(y >> 43) << 2, - ] +fn interleave2([x, y]: [u64; 2]) -> [u64; 2] { + // Word `j` holds bits `32j` to `32j + 31` of each. + [spread2(x) | spread2(y) << 1, spread2(x >> 32) | spread2(y >> 32) << 1] } -/// The low 22 bits of `x` at every third bit, from bit 0. +/// The low 32 bits of `x` at every other bit, from bit 0. #[cfg_attr( not(all(target_arch = "x86_64", target_feature = "bmi2")), expect(clippy::missing_const_for_fn, reason = "BMI2's bit deposit is a runtime intrinsic.") )] #[inline(always)] -fn spread3(x: u64) -> u64 { +fn spread2(x: u64) -> u64 { #[cfg(all(target_arch = "x86_64", target_feature = "bmi2"))] { // SAFETY: BMI2 is enabled at compile time. - unsafe { std::arch::x86_64::_pdep_u64(x, 0x9249_2492_4924_9249) } + unsafe { std::arch::x86_64::_pdep_u64(x, 0x5555_5555_5555_5555) } } - // Without it, bits 0 to 20 spread by halving strides, and bit 21 goes to bit 63. + // Without it, the bits spread by halving strides. #[cfg(not(all(target_arch = "x86_64", target_feature = "bmi2")))] { - let top = (x >> 21 & 1) << 63; - let mut x = x & 0x1f_ffff; - x = (x | x << 32) & 0x001f_0000_0000_ffff; - x = (x | x << 16) & 0x001f_0000_ff00_00ff; - x = (x | x << 8) & 0x100f_00f0_0f00_f00f; - x = (x | x << 4) & 0x10c3_0c30_c30c_30c3; - x = (x | x << 2) & 0x1249_2492_4924_9249; - x | top + let mut x = x & 0xffff_ffff; + 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 } } @@ -275,8 +269,11 @@ mod tests { use proptest::test_runner::TestRunner; /// Every class with a circuit. - const CLASSES: [Class; 10] = [ - Class::Alu, + const CLASSES: [Class; 13] = [ + Class::Add, + Class::Logic, + Class::Branch, + Class::Jump, Class::Shift, Class::Load, Class::Store, @@ -292,7 +289,7 @@ mod tests { fn instance_sizes_are_pinned() { // The log of each instance's bits, which the tables fix before any circuit is built. let sizes = CLASSES.map(|class| class.circuit().k_log()); - assert_eq!(sizes, [10, 10, 10, 10, 8, 8, 12, 13, 13, 14]); + assert_eq!(sizes, [9, 9, 9, 9, 10, 10, 10, 8, 8, 12, 13, 13, 14]); } #[test] diff --git a/crates/leanvm_core/src/rv/entry.rs b/crates/leanvm_core/src/rv/entry.rs index 4d266014b..404a4e919 100644 --- a/crates/leanvm_core/src/rv/entry.rs +++ b/crates/leanvm_core/src/rv/entry.rs @@ -7,10 +7,11 @@ //! The program is public, so each instruction word is decoded into an entry once, before any run. use super::circuits::ClassCircuit; -use super::instruction::{ExtOp, ImmOp, Instruction, LoadOp, Op, RegOp, ShiftOp, StoreOp}; +use super::instruction::{BranchOp, ExtOp, ImmOp, Instruction, LoadOp, Op, RegOp, ShiftOp, StoreOp}; use super::register::{Reg, RegisterFile}; use super::semantics::{ - Alu, Div, Ext, Hash, InstructionClass, Ld, Load, Mul, Mulh, Outcome, Sd, Shift, Store, WordAccess, + Add, Branch, Div, Ext, Hash, InstructionClass, Jump, Ld, Load, Logic, Mul, Mulh, Outcome, Sd, Shift, Store, + WordAccess, }; use flock::circuit::Circuit; @@ -19,8 +20,14 @@ use flock::circuit::Circuit; /// The classes with a table come in table order. #[derive(Clone, Copy, Debug, PartialEq, Eq, Hash)] pub enum Class { - /// Add, subtract, compare, bitwise logic, branches and jumps. - Alu, + /// Add, subtract and compare. + Add, + /// AND, OR and XOR. + Logic, + /// The conditional branches. + Branch, + /// `JAL`, `JALR` and the exit. + Jump, /// A byte, half word or word read from memory. Load, /// A byte, half word or word written to memory. @@ -53,7 +60,10 @@ impl Class { /// An illegal entry carries none at all. pub const fn legal_flags(self) -> &'static [u64] { match self { - Self::Alu => Alu::LEGAL, + Self::Add => Add::LEGAL, + Self::Logic => Logic::LEGAL, + Self::Branch => Branch::LEGAL, + Self::Jump => Jump::LEGAL, Self::Shift => Shift::LEGAL, Self::Load => Load::LEGAL, Self::Store => Store::LEGAL, @@ -70,6 +80,8 @@ impl Class { /// An instruction of the class that names no register but `x0`, or `ra` where `x0` is undefined. /// + /// A branch is never taken, and a jump goes to the next instruction, so that each falls through. + /// /// A load, a store, a hash and an extension-field product touch the memory at address zero. /// /// The extension-field product reads `c`'s address from `ra`, as an address in `x0` is undefined. @@ -78,12 +90,25 @@ impl Class { pub const fn nop(self) -> Option { let (rd, rs1, rs2) = (Reg::ZERO, Reg::ZERO, Reg::ZERO); Some(match self { - Self::Alu => Op::Imm { + Self::Add => Op::Imm { op: ImmOp::Addi, rd, rs1, imm: 0, }, + Self::Logic => Op::Imm { + op: ImmOp::Andi, + rd, + rs1, + imm: 0, + }, + Self::Branch => Op::Branch { + op: BranchOp::Bne, + rs1, + rs2, + offset: 0, + }, + Self::Jump => Op::Jal { rd, offset: 4 }, Self::Shift => Op::Shift { op: ShiftOp::Slli, rd, @@ -151,7 +176,10 @@ impl Class { /// proves by identities over `K` instead (`tables::ClassTable::identities`). pub fn circuit(self) -> Circuit { match self { - Self::Alu => Alu::circuit(), + Self::Add => Add::circuit(), + Self::Logic => Logic::circuit(), + Self::Branch => Branch::circuit(), + Self::Jump => Jump::circuit(), Self::Shift => Shift::circuit(), Self::Load => Load::circuit(), Self::Store => Store::circuit(), @@ -221,10 +249,10 @@ impl Entry { target: Target::Next, }; - /// `ECALL`: an unconditional jump to the halt slot. + /// `ECALL`: a jump to the halt slot. pub const EXIT: Self = Self { - class: Class::Alu, - flags: Alu::ALWAYS, + class: Class::Jump, + flags: 0, a1: 0, a2: 0, ad: RegisterFile::SINK, @@ -240,19 +268,11 @@ impl Entry { pub fn evaluate(&self, pc: u64, v1: u64, v2: u64, cell: u64) -> Outcome { let (flags, imm) = (self.flags, self.imm); let (out, taken, access) = match self.class { - // The decision reads no jump offset. - Class::Alu => { - let (out, taken) = Alu { - flags, - v1, - v2, - imm, - dt: 0, - pc4: pc.wrapping_add(4), - } - .eval(); - (out, taken, None) - } + // The decision reads no jump offset, and a jump's link is `pc + 4`. + Class::Add => (Add { flags, v1, v2, imm }.eval(), false, None), + Class::Logic => (Logic { flags, v1, v2, imm }.eval(), false, None), + Class::Branch => (0, Branch { flags, v1, v2, dt: 0 }.eval(), None), + Class::Jump => (pc.wrapping_add(4), true, None), Class::Shift => (Shift { flags, v1, v2, imm }.eval(), false, None), Class::Mul => (Mul { flags, v1, v2 }.eval(), false, None), Class::Mulh => (Mulh { flags, v1, v2 }.eval(), false, None), @@ -344,16 +364,16 @@ impl Entry { Op::Lui { rd, imm20 } => entry(zero, zero, rd, (imm20 << 12) as i32 as i64 as u64), Op::Auipc { rd, imm20 } => entry(zero, zero, rd, pc.wrapping_add((imm20 << 12) as i32 as i64 as u64)), - // A branch compares by subtraction, and jumps to a fixed target. + // A branch compares two registers, and jumps to a fixed target. Op::Branch { rs1, rs2, offset, .. } => Self { target: Target::Abs(pc.wrapping_add(offset as i64 as u64)), ..entry(rs1, rs2, zero, 0) }, - // JAL: an unconditional jump to a fixed target, linking pc + 4 as a constant added to x0. + // JAL: a jump to a fixed target, linking pc + 4, which the jump's table writes itself. Op::Jal { rd, offset } => Self { target: Target::Abs(pc.wrapping_add(offset as i64 as u64)), - ..entry(zero, zero, rd, pc.wrapping_add(4)) + ..entry(zero, zero, rd, 0) }, // JALR: a jump to rs1 + offset with bit 0 cleared, linking pc + 4. @@ -366,7 +386,7 @@ impl Entry { self.target == Target::Halt } - /// Whether the entry at `pc` obeys the rules that make the bytecode table RISC-V. + /// Whether the entry obeys the rules that make the bytecode table RISC-V. /// /// Both verifiers check these rules on every entry. /// @@ -377,9 +397,9 @@ impl Entry { /// - an illegal entry and an exit each have exactly one form; /// - the registers read are below 32, and the cell written is in `1..=32`; /// - the flags are legal for the class; - /// - the target matches what the flags select, and a `jal` links `pc + 4`; + /// - the target matches the class and its flags, and a `jal` reads `x0` and has no immediate; /// - a field the class's table holds at a constant has that constant. - pub fn is_well_formed(&self, pc: u64) -> bool { + pub fn is_well_formed(&self) -> bool { // An illegal entry has one inert form. if self.class == Class::Illegal { return *self == Self::ILLEGAL; @@ -393,7 +413,7 @@ impl Entry { // Register numbers, and flags the class's circuit is written for. let operands = self.a1 < 32 && self.a2 < 32 && (1..=RegisterFile::SINK).contains(&self.ad); let flags = self.class.legal_flags().contains(&self.flags); - operands && flags && self.has_consistent_control(pc) && self.has_table_constants() + operands && flags && self.has_consistent_control() && self.has_table_constants() } /// An entry with no control flow. @@ -415,39 +435,36 @@ impl Entry { } } - /// Whether the target matches the flags of the entry at `pc`. + /// Whether the target matches the class and the flags. /// - /// - A `jal` jumps to a fixed target, and its sum `x0 + x0 + imm` is the link `pc + 4`. + /// - A `jal` jumps to a fixed target, and reads nothing: `x0`, and no immediate. + /// - A `jalr` jumps to the address it computes. /// - A branch jumps to a fixed target. - /// - Anything else has none: it falls through, or jumps to the address it computes. - fn has_consistent_control(&self, pc: u64) -> bool { + /// - Anything else falls through. + fn has_consistent_control(&self) -> bool { let fixed = matches!(self.target, Target::Abs(_)); let next = self.target == Target::Next; - if self.class != Class::Alu { - return next; - } - - // The flags say which control shape the entry must have. - match self.flags { - Alu::ALWAYS => fixed && self.a1 == 0 && self.a2 == 0 && self.imm == pc.wrapping_add(4), - flags if flags & Alu::BRANCHES != 0 => fixed, + match (self.class, self.flags) { + (Class::Jump, Jump::INDIRECT) => next, + (Class::Jump, _) => fixed && self.a1 == 0 && self.imm == 0, + (Class::Branch, _) => fixed, _ => next, } } /// Whether the fields a class's table fixes hold their constants. /// - /// - A load reads no `rs2`, so its second register is `x0`. + /// - A load reads no `rs2`, and neither does a jump, so their second register is `x0`. /// - A store writes no `rd`, so its destination is the sink. - /// - A hash writes no `rd` and has no immediate. + /// - A branch and a hash write no `rd` and have no immediate. /// - An extension-field product reads `rd` as an address, so it names a register, and has no immediate. /// /// That a doubleword load or store has no flags is its legal flag word, zero. const fn has_table_constants(&self) -> bool { match self.class { - Class::Load | Class::Ld => self.a2 == 0, + Class::Load | Class::Ld | Class::Jump => self.a2 == 0, Class::Store | Class::Sd => self.ad == RegisterFile::SINK, - Class::Hash => self.ad == RegisterFile::SINK && self.imm == 0, + Class::Branch | Class::Hash => self.ad == RegisterFile::SINK && self.imm == 0, Class::Ext => self.ad < RegisterFile::SINK && self.imm == 0, _ => true, } @@ -458,7 +475,6 @@ impl Entry { mod tests { use super::*; use crate::rv::Region; - use crate::rv::instruction::BranchOp; use crate::rv::register::Reg; use proptest::prelude::*; use std::collections::HashSet; @@ -468,7 +484,7 @@ mod tests { // Fixture: the decoded ecall. let exit = Entry::decode(0x73, 0); assert_eq!(exit, Entry::EXIT); - assert!(exit.is_well_formed(0)); + assert!(exit.is_well_formed()); // Mutation: change any one field, the halt target kept. for malformed in [ @@ -476,19 +492,23 @@ mod tests { class: Class::Load, ..exit }, - Entry { flags: 0, ..exit }, + Entry { + flags: Jump::INDIRECT, + ..exit + }, Entry { a1: 1, ..exit }, Entry { a2: 1, ..exit }, Entry { ad: 1, ..exit }, Entry { imm: 1, ..exit }, ] { - assert!(!malformed.is_well_formed(0), "{malformed:?}"); + assert!(!malformed.is_well_formed(), "{malformed:?}"); } } #[test] fn a_skipped_register_access_names_its_constant() { - // Invariant: a load's rs2 is x0, a store's rd is the sink, and a double word's flags are zero. + // Invariant: a load's and a jump's rs2 is x0, a store's rd is the sink, a branch's rd is the sink and its + // immediate zero, and a double word's flags are zero. // // Fixture: `ld`, `sd`, `lw` and `sw` of `a0` at `0(a1)`. for (load, store, classes) in [ @@ -497,70 +517,90 @@ mod tests { ] { let (load, store) = (Entry::decode(load, 0), Entry::decode(store, 0)); assert_eq!((load.class, store.class), classes); - assert!(load.is_well_formed(0) && store.is_well_formed(0)); + assert!(load.is_well_formed() && store.is_well_formed()); // Mutation: the load reads x1 as rs2, the store writes x1, the double words carry a width. - assert!(!Entry { a2: 1, ..load }.is_well_formed(0)); - assert!(!Entry { ad: 1, ..store }.is_well_formed(0)); + assert!(!Entry { a2: 1, ..load }.is_well_formed()); + assert!(!Entry { ad: 1, ..store }.is_well_formed()); if classes.0 == Class::Ld { - assert!(!Entry { flags: 3, ..load }.is_well_formed(0)); - assert!(!Entry { flags: 3, ..store }.is_well_formed(0)); + assert!(!Entry { flags: 3, ..load }.is_well_formed()); + assert!(!Entry { flags: 3, ..store }.is_well_formed()); } } + + // Fixture: `jalr ra, 0(a1)` and `beq a0, a1, 0`. + let (jump, branch) = (Entry::decode(0x0005_80e7, 0), Entry::decode(0x00b5_0063, 0)); + assert_eq!((jump.class, branch.class), (Class::Jump, Class::Branch)); + assert!(jump.is_well_formed() && branch.is_well_formed()); + + // Mutation: the jump reads x1 as rs2, the branch writes x1 or adds 4. + assert!(!Entry { a2: 1, ..jump }.is_well_formed()); + assert!(!Entry { ad: 1, ..branch }.is_well_formed()); + assert!(!Entry { imm: 4, ..branch }.is_well_formed()); } #[test] - fn alu_control_shapes_match_their_flags() { - // Fixture: one instruction per legal ALU word, in the order of the legal list. + fn control_shapes_match_their_class_and_flags() { + // Fixture: one instruction per legal word of the four classes split from the ALU, in the order of each legal + // list. // - // addi, sub, addiw, subw, slt, sltu, and, or, xor, - // jalr, beq, bne, blt, bge, bltu, bgeu, jal - let witnesses = [ - 0x0000_0013, - 0x4000_0033, - 0x0000_001b, - 0x4000_003b, - 0x0000_2033, - 0x0000_3033, - 0x0000_7033, - 0x0000_6033, - 0x0000_4033, - 0x0000_0067, - 0x0000_0063, - 0x0000_1063, - 0x0000_4063, - 0x0000_5063, - 0x0000_6063, - 0x0000_7063, - 0x0000_006f, + // addi, sub, addiw, subw, slt, sltu + // and, or, xor + // beq, bne, blt, bge, bltu, bgeu + // jal, jalr + let witnesses: [(Class, &[u32]); 4] = [ + ( + Class::Add, + &[ + 0x0000_0013, + 0x4000_0033, + 0x0000_001b, + 0x4000_003b, + 0x0000_2033, + 0x0000_3033, + ], + ), + (Class::Logic, &[0x0000_7033, 0x0000_6033, 0x0000_4033]), + ( + Class::Branch, + &[ + 0x0000_0063, + 0x0000_1063, + 0x0000_4063, + 0x0000_5063, + 0x0000_6063, + 0x0000_7063, + ], + ), + (Class::Jump, &[0x0000_006f, 0x0000_0067]), ]; - assert_eq!(Alu::LEGAL.len(), witnesses.len()); - let pc = Region::TEXT.base(); - for (&flags, word) in Alu::LEGAL.iter().zip(witnesses) { - let decoded = Entry::decode(word, pc); - assert_eq!((decoded.class, decoded.flags), (Class::Alu, flags)); - - // Mutation: every target kind. - // - // Only the decoded shape is well formed, whatever the fixed address. - for target in [Target::Next, Target::Abs(pc), Target::Abs(pc + 4)] { - let candidate = Entry { target, ..decoded }; - let same_kind = matches!( - (target, decoded.target), - (Target::Next, Target::Next) | (Target::Abs(_), Target::Abs(_)) - ); - assert_eq!(candidate.is_well_formed(pc), same_kind, "{candidate:?}"); + for (class, words) in witnesses { + assert_eq!(class.legal_flags().len(), words.len()); + for (&flags, &word) in class.legal_flags().iter().zip(words) { + let decoded = Entry::decode(word, pc); + assert_eq!((decoded.class, decoded.flags), (class, flags)); + + // Mutation: every target kind. + // + // Only the decoded shape is well formed, whatever the fixed address. + for target in [Target::Next, Target::Abs(pc), Target::Abs(pc + 4)] { + let candidate = Entry { target, ..decoded }; + let same_kind = matches!( + (target, decoded.target), + (Target::Next, Target::Next) | (Target::Abs(_), Target::Abs(_)) + ); + assert_eq!(candidate.is_well_formed(), same_kind, "{candidate:?}"); + } } } - // A jal links pc + 4, a constant added to x0: at another address, or read off a register, it is not a jal. + // A jal's link is its table's `pc + 4`: reading a register or adding an immediate, it is not a jal. let jal = Entry::decode(0x0000_00ef, pc); - assert_eq!((jal.flags, jal.imm), (Alu::ALWAYS, pc + 4)); - assert!(jal.is_well_formed(pc)); - assert!(!jal.is_well_formed(pc + 4)); - assert!(!Entry { a1: 1, ..jal }.is_well_formed(pc)); - assert!(!Entry { a2: 1, ..jal }.is_well_formed(pc)); + assert_eq!((jal.class, jal.flags, jal.imm), (Class::Jump, 0, 0)); + assert!(jal.is_well_formed()); + assert!(!Entry { a1: 1, ..jal }.is_well_formed()); + assert!(!Entry { imm: 4, ..jal }.is_well_formed()); } #[test] @@ -602,10 +642,7 @@ mod tests { // Every operation's entry obeys the bytecode table's rules. for &op in &ops { - assert!( - Entry::new(op, Region::TEXT.base()).is_well_formed(Region::TEXT.base()), - "{op:?}" - ); + assert!(Entry::new(op, Region::TEXT.base()).is_well_formed(), "{op:?}"); } // Invariant: a class's legal words are the words its operations use, no more and no fewer. @@ -613,7 +650,10 @@ mod tests { // an unused legal word would be a function no program reaches // a used word outside the list would be refused by the verifiers for class in [ - Class::Alu, + Class::Add, + Class::Logic, + Class::Branch, + Class::Jump, Class::Shift, Class::Load, Class::Store, @@ -642,7 +682,7 @@ mod tests { // // ecall, blake2s, blake2s on the final block for word in [0x73, 0x0000_000b, 0x0000_100b] { - assert!(Entry::decode(word, Region::TEXT.base()).is_well_formed(Region::TEXT.base())); + assert!(Entry::decode(word, Region::TEXT.base()).is_well_formed()); } // Every opcode and function, every 12-bit top, with fixed registers. @@ -653,7 +693,7 @@ mod tests { for top in 0..(1u32 << 12) { let word = opcode | (f3 << 12) | (top << 20) | (0x15 << 7) | (0x0a << 15); let e = Entry::decode(word, Region::TEXT.base()); - assert!(e.is_well_formed(Region::TEXT.base()), "{word:#010x} decodes to {e:?}"); + assert!(e.is_well_formed(), "{word:#010x} decodes to {e:?}"); } } } @@ -663,7 +703,10 @@ mod tests { fn each_class_nop_is_of_its_class_and_names_only_x0() { // Fixture: every class but the illegal one, which has no instruction. let classes = [ - Class::Alu, + Class::Add, + Class::Logic, + Class::Branch, + Class::Jump, Class::Shift, Class::Load, Class::Store, @@ -684,7 +727,7 @@ mod tests { (class, 0, 0, RegisterFile::SINK, 0), "{class:?}" ); - assert!(e.is_well_formed(Region::TEXT.base())); + assert!(e.is_well_formed()); } } @@ -727,7 +770,7 @@ mod tests { let e = Entry::decode(op.encode(rd, rs1, rs2).bits(), Region::TEXT.base()); let ad = if rd.index() == 0 { RegisterFile::SINK } else { rd.index() as u8 }; prop_assert_eq!((e.a1, e.a2, e.ad, e.imm), (rs1.index() as u8, rs2.index() as u8, ad, 0)); - prop_assert!(e.is_well_formed(Region::TEXT.base())); + prop_assert!(e.is_well_formed()); } #[test] @@ -743,8 +786,8 @@ mod tests { let flags = ExtOp::ALL.iter().position(|&o| o == op).unwrap() as u64; prop_assert_eq!((e.class, e.flags), (Class::Ext, flags)); prop_assert_eq!((e.a1, e.a2, e.ad), (rs1.index() as u8, rs2.index() as u8, rd.index() as u8)); - prop_assert!(e.is_well_formed(Region::TEXT.base())); - prop_assert!(!Entry { ad: RegisterFile::SINK, ..e }.is_well_formed(Region::TEXT.base()), "an address in the sink"); + prop_assert!(e.is_well_formed()); + prop_assert!(!Entry { ad: RegisterFile::SINK, ..e }.is_well_formed(), "an address in the sink"); } } diff --git a/crates/leanvm_core/src/rv/instruction.rs b/crates/leanvm_core/src/rv/instruction.rs index 24b438f1e..3971d1bbe 100644 --- a/crates/leanvm_core/src/rv/instruction.rs +++ b/crates/leanvm_core/src/rv/instruction.rs @@ -29,7 +29,7 @@ use std::ops::Range; use super::entry::Class; use super::register::Reg; -use super::semantics::{Alu, Div, Ext, Hash, Load, Mul, Mulh, Shift}; +use super::semantics::{Add, Branch, Div, Ext, Hash, Jump, Load, Logic, Mul, Mulh, Shift}; /// Sign-extend the low bits of a 32-bit value to a 64-bit word. const fn sign_extend(value: u32, bits: u32) -> u64 { @@ -682,15 +682,15 @@ impl RegOp { /// The class running this operation, and its flag word. const fn function(self) -> (Class, u64) { match self { - Self::Add => (Class::Alu, 0), - Self::Sub => (Class::Alu, Alu::SUB), - Self::Slt => (Class::Alu, Alu::SUB | Alu::SEL_LT), - Self::Sltu => (Class::Alu, Alu::SUB | Alu::SEL_LTU), - Self::Xor => (Class::Alu, Alu::SEL_XOR), - Self::Or => (Class::Alu, Alu::SEL_OR), - Self::And => (Class::Alu, Alu::SEL_AND), - Self::Addw => (Class::Alu, Alu::WORD), - Self::Subw => (Class::Alu, Alu::SUB | Alu::WORD), + Self::Add => (Class::Add, 0), + Self::Sub => (Class::Add, Add::SUB), + Self::Slt => (Class::Add, Add::SUB | Add::SEL_LT), + Self::Sltu => (Class::Add, Add::SUB | Add::SEL_LTU), + Self::Xor => (Class::Logic, Logic::XOR), + Self::Or => (Class::Logic, Logic::OR), + Self::And => (Class::Logic, Logic::AND), + Self::Addw => (Class::Add, Add::WORD), + Self::Subw => (Class::Add, Add::SUB | Add::WORD), Self::Sll => (Class::Shift, 0), Self::Srl => (Class::Shift, Shift::RIGHT), Self::Sra => (Class::Shift, Shift::RIGHT | Shift::ARITH), @@ -721,16 +721,16 @@ impl ImmOp { Instruction::i(opcode, funct3, rd, rs1, imm) } - /// The ALU's flag word. - const fn flags(self) -> u64 { + /// The class running this operation, and its flag word. + const fn function(self) -> (Class, u64) { match self { - Self::Addi => 0, - Self::Slti => Alu::SUB | Alu::SEL_LT, - Self::Sltiu => Alu::SUB | Alu::SEL_LTU, - Self::Xori => Alu::SEL_XOR, - Self::Ori => Alu::SEL_OR, - Self::Andi => Alu::SEL_AND, - Self::Addiw => Alu::WORD, + Self::Addi => (Class::Add, 0), + Self::Slti => (Class::Add, Add::SUB | Add::SEL_LT), + Self::Sltiu => (Class::Add, Add::SUB | Add::SEL_LTU), + Self::Xori => (Class::Logic, Logic::XOR), + Self::Ori => (Class::Logic, Logic::OR), + Self::Andi => (Class::Logic, Logic::AND), + Self::Addiw => (Class::Add, Add::WORD), } } } @@ -848,15 +848,15 @@ impl BranchOp { Instruction::b(self.fields(), rs1, rs2, offset) } - /// The ALU's condition flag. + /// The branch's condition flag. const fn condition(self) -> u64 { match self { - Self::Beq => Alu::BR_EQ, - Self::Bne => Alu::BR_NE, - Self::Blt => Alu::BR_LT, - Self::Bge => Alu::BR_GE, - Self::Bltu => Alu::BR_LTU, - Self::Bgeu => Alu::BR_GEU, + Self::Beq => Branch::EQ, + Self::Bne => Branch::NE, + Self::Blt => Branch::LT, + Self::Bge => Branch::GE, + Self::Bltu => Branch::LTU, + Self::Bgeu => Branch::GEU, } } } @@ -940,14 +940,14 @@ impl Op { pub const fn function(self) -> (Class, u64) { match self { Self::Reg { op, .. } => op.function(), - Self::Imm { op, .. } => (Class::Alu, op.flags()), + Self::Imm { op, .. } => op.function(), Self::Shift { op, .. } => (Class::Shift, op.flags()), Self::Load { op, .. } => op.function(), Self::Store { op, .. } => op.function(), - Self::Branch { op, .. } => (Class::Alu, Alu::SUB | op.condition()), - Self::Lui { .. } | Self::Auipc { .. } | Self::Fence => (Class::Alu, 0), - Self::Jal { .. } | Self::Ecall => (Class::Alu, Alu::ALWAYS), - Self::Jalr { .. } => (Class::Alu, Alu::INDIRECT | Alu::ALWAYS), + Self::Branch { op, .. } => (Class::Branch, op.condition()), + Self::Lui { .. } | Self::Auipc { .. } | Self::Fence => (Class::Add, 0), + Self::Jal { .. } | Self::Ecall => (Class::Jump, 0), + Self::Jalr { .. } => (Class::Jump, Jump::INDIRECT), Self::Blake2s { last, .. } => (Class::Hash, if last { Hash::FINAL } else { 0 }), Self::Ext { op, .. } => (Class::Ext, op.flags()), } diff --git a/crates/leanvm_core/src/rv/machine.rs b/crates/leanvm_core/src/rv/machine.rs index 1e9520d33..b52d52ee3 100644 --- a/crates/leanvm_core/src/rv/machine.rs +++ b/crates/leanvm_core/src/rv/machine.rs @@ -291,14 +291,14 @@ impl<'a> Machine<'a> { /// Write `vd` to the entry's destination and return what it held. /// - /// A store and a hash always write the sink, which nothing reads. + /// A store, a branch and a hash always write the sink, which nothing reads. /// /// An extension-field product reads `rd` as an address, and writes no register. /// /// They make no write at all, so their tables have none to prove. const fn write_destination(&mut self, entry: &Entry, vd: u64) -> u64 { match entry.class { - Class::Store | Class::Sd | Class::Hash | Class::Ext => 0, + Class::Store | Class::Sd | Class::Branch | Class::Hash | Class::Ext => 0, _ => self.registers.replace(entry.ad, vd), } } @@ -332,7 +332,7 @@ pub struct Step { pub taken: bool, /// What the destination held before. /// - /// Zero for a store, a hash or an extension-field product, which write no register. + /// Zero for a store, a branch, a hash or an extension-field product, which write no register. pub vd_old: u64, /// What the destination holds now: the output. pub vd: u64, diff --git a/crates/leanvm_core/src/rv/mod.rs b/crates/leanvm_core/src/rv/mod.rs index 0a33a156a..2b7cf3d8c 100644 --- a/crates/leanvm_core/src/rv/mod.rs +++ b/crates/leanvm_core/src/rv/mod.rs @@ -41,5 +41,6 @@ pub use program::{Fetched, ProgramError, RiscvProgram}; pub use region::Region; pub use register::{Reg, RegisterFile, Syscall}; pub use semantics::{ - Alu, BlockAccess, Div, Ext, Hash, InstructionClass, Ld, Limb, Load, Mul, Mulh, Shift, Store, WordAccess, + Add, BlockAccess, Branch, Div, Ext, Hash, InstructionClass, Jump, Ld, Limb, Load, Logic, Mul, Mulh, Shift, Store, + WordAccess, }; diff --git a/crates/leanvm_core/src/rv/program.rs b/crates/leanvm_core/src/rv/program.rs index 4649bd720..f9926aa69 100644 --- a/crates/leanvm_core/src/rv/program.rs +++ b/crates/leanvm_core/src/rv/program.rs @@ -77,7 +77,7 @@ impl RiscvProgram { entries.resize((text.len() + 2).next_power_of_two(), Entry::ILLEGAL); // The decoder only makes well-formed entries, which the bytecode table's rules restate. - if !(entries.iter().enumerate()).all(|(i, e)| e.is_well_formed(Region::TEXT.address(i))) { + if !entries.iter().all(Entry::is_well_formed) { return Err(ProgramError::MalformedEntry); } Ok(Self { @@ -184,7 +184,8 @@ impl RiscvProgram { /// /// Zero for an entry with no fixed target. /// - /// The ALU's circuit gates it by its decision, and the table adds that to `pc + 4`, the sum in the field being XOR. + /// A branch's or a jump's circuit gates it by its decision, and the table adds that to `pc + 4`, the sum in the + /// field being XOR. pub fn dt_of(&self, index: usize) -> u64 { self.target_of(index) .map_or(0, |target| target ^ self.pc_of(index).wrapping_add(4)) @@ -279,7 +280,7 @@ mod tests { // A power of two of well-formed entries. let entries = program.entries(); prop_assert!(entries.len().is_power_of_two()); - prop_assert!((entries.iter().enumerate()).all(|(i, e)| e.is_well_formed(program.pc_of(i)))); + prop_assert!(entries.iter().all(Entry::is_well_formed)); // Each word decoded at its own address, then illegal padding to the end. for (i, &word) in text.iter().enumerate() { diff --git a/crates/leanvm_core/src/rv/semantics/alu.rs b/crates/leanvm_core/src/rv/semantics/alu.rs index fcc4cd386..08a71214b 100644 --- a/crates/leanvm_core/src/rv/semantics/alu.rs +++ b/crates/leanvm_core/src/rv/semantics/alu.rs @@ -1,17 +1,19 @@ -//! The ALU: sums, differences, comparisons, bitwise logic, branches and jumps. +//! The ALU's four classes: sums and comparisons, bitwise logic, branches, and jumps. +//! +//! Each is a table of its own, so that a row pays only for the circuit its instruction needs. use super::{InstructionClass, sext32}; use crate::rv::circuits::{ClassCircuit, Products, Word, WordGadgets}; use flock::circuit::{Builder, Circuit}; -/// One ALU instance: add, subtract, compare, bitwise logic, branches and jumps. +/// One adder instance: add, subtract, and the two comparisons. /// /// The second operand `b` is `v2 ^ imm`. /// /// One of the two is always zero. #[derive(Clone, Copy, Debug, PartialEq, Eq)] -pub struct Alu { - /// What the ALU computes: one of its legal words. +pub struct Add { + /// What the adder computes: one of its legal words. pub flags: u64, /// The first register's value. pub v1: u64, @@ -19,18 +21,12 @@ pub struct Alu { pub v2: u64, /// The immediate. pub imm: u64, - /// The jump's offset: the fixed target XOR `pc + 4`, zero for an entry with none. - /// - /// The decision does not read it; the circuit gates it by the decision. - pub dt: u64, - /// The fall-through address `pc + 4`: what an indirect jump links, and what its target is taken against. - pub pc4: u64, } -impl Alu { +impl Add { /// Compute `v1 - b` instead of `v1 + b`. /// - /// The comparisons and the branches need the difference. + /// The comparisons need the difference. pub const SUB: u64 = 1 << 0; /// Sign-extend the low 32 bits of the sum. pub const WORD: u64 = 1 << 1; @@ -38,53 +34,10 @@ impl Alu { pub const SEL_LT: u64 = 1 << 2; /// Output `v1 < b`, unsigned. pub const SEL_LTU: u64 = 1 << 3; - /// Output `v1 & b`. - pub const SEL_AND: u64 = 1 << 4; - /// Output `v1 | b`. - pub const SEL_OR: u64 = 1 << 5; - /// Output `v1 ^ b`. - pub const SEL_XOR: u64 = 1 << 6; - /// Jump to the sum with bit 0 cleared and output `pc + 4`, as `JALR` does; set with `ALWAYS`. - pub const INDIRECT: u64 = 1 << 7; - /// Branch when `v1 == b`. - pub const BR_EQ: u64 = 1 << 8; - /// Branch when `v1 != b`. - pub const BR_NE: u64 = 1 << 9; - /// Branch when `v1 < b`, signed. - pub const BR_LT: u64 = 1 << 10; - /// Branch when `v1 >= b`, signed. - pub const BR_GE: u64 = 1 << 11; - /// Branch when `v1 < b`, unsigned. - pub const BR_LTU: u64 = 1 << 12; - /// Branch when `v1 >= b`, unsigned. - pub const BR_GEU: u64 = 1 << 13; - /// Always take the jump. - pub const ALWAYS: u64 = 1 << 14; - - /// Every branch condition. - pub const BRANCHES: u64 = Self::BR_EQ | Self::BR_NE | Self::BR_LT | Self::BR_GE | Self::BR_LTU | Self::BR_GEU; - - const fn has_flag(&self, flag: u64) -> bool { - self.flags & flag != 0 - } - - /// What the successor adds to `pc + 4`, given the decision: zero when the jump is not taken. - /// - /// - A fixed jump adds its offset, the target XOR `pc + 4`. - /// - An indirect jump has offset zero and adds the sum XOR `pc + 4`, bit 0 left out. - /// - Its successor is then the sum with bit 0 cleared, since `pc + 4` is even. - pub const fn jump(&self, taken: bool) -> u64 { - let indirect = if self.has_flag(Self::INDIRECT) { - (self.v1.wrapping_add(self.v2 ^ self.imm) ^ self.pc4) & !1 - } else { - 0 - }; - if taken { self.dt ^ indirect } else { 0 } - } } -impl InstructionClass for Alu { - /// At most one output selector and at most one branch condition is set. +impl InstructionClass for Add { + /// A comparison subtracts, and has no word form. const LEGAL: &'static [u64] = &[ 0, Self::SUB, @@ -92,82 +45,38 @@ impl InstructionClass for Alu { Self::SUB | Self::WORD, Self::SUB | Self::SEL_LT, Self::SUB | Self::SEL_LTU, - Self::SEL_AND, - Self::SEL_OR, - Self::SEL_XOR, - Self::INDIRECT | Self::ALWAYS, - Self::SUB | Self::BR_EQ, - Self::SUB | Self::BR_NE, - Self::SUB | Self::BR_LT, - Self::SUB | Self::BR_GE, - Self::SUB | Self::BR_LTU, - Self::SUB | Self::BR_GEU, - Self::ALWAYS, ]; - /// The output, and whether the jump is taken. - /// - /// The output of an indirect jump is its link, `pc + 4`. - type Output = (u64, bool); + /// The sum, or the comparison's bit. + type Output = u64; - fn eval(&self) -> (u64, bool) { + fn eval(&self) -> u64 { + let on = |flag: u64| self.flags & flag != 0; let (v1, b) = (self.v1, self.v2 ^ self.imm); - - // One adder serves the sum and the difference. - let sum = if self.has_flag(Self::SUB) { - v1.wrapping_sub(b) + if on(Self::SEL_LT) { + ((v1 as i64) < (b as i64)) as u64 + } else if on(Self::SEL_LTU) { + (v1 < b) as u64 } else { - v1.wrapping_add(b) - }; - - // The comparisons every selector and branch picks from. - let (lt, ltu, eq) = ((v1 as i64) < (b as i64), v1 < b, v1 == b); - - // The output: one selector, or the sum when none is set. - let out = if self.has_flag(Self::SEL_LT) { - lt as u64 - } else if self.has_flag(Self::SEL_LTU) { - ltu as u64 - } else if self.has_flag(Self::SEL_AND) { - v1 & b - } else if self.has_flag(Self::SEL_OR) { - v1 | b - } else if self.has_flag(Self::SEL_XOR) { - v1 ^ b - } else if self.has_flag(Self::INDIRECT) { - self.pc4 - } else if self.has_flag(Self::WORD) { - sext32(sum) - } else { - sum - }; - - // The jump: unconditional, or the one branch condition set. - let taken = self.has_flag(Self::ALWAYS) - || (self.has_flag(Self::BR_EQ) && eq) - || (self.has_flag(Self::BR_NE) && !eq) - || (self.has_flag(Self::BR_LT) && lt) - || (self.has_flag(Self::BR_GE) && !lt) - || (self.has_flag(Self::BR_LTU) && ltu) - || (self.has_flag(Self::BR_GEU) && !ltu); - (out, taken) + let sum = if on(Self::SUB) { + v1.wrapping_sub(b) + } else { + v1.wrapping_add(b) + }; + if on(Self::WORD) { sext32(sum) } else { sum } + } } } -impl ClassCircuit for Alu { - /// The ALU: `(v1, v2, imm, flags, dt, pc4) -> (out, jump)`. - /// - /// It mirrors the reference function on every legal flag word. +impl ClassCircuit for Add { + /// The adder: `(v1, v2, imm, flags) -> out`. /// /// - The second operand is `b = v2 ^ imm`. /// - One adder gives `v1 + b`, or `v1 - b` for the comparisons. - /// - The output is that sum, unless a selector picks a comparison or a bitwise operation. - /// - An indirect jump outputs `pc + 4` instead, and adds to `dt` the sum XOR `pc + 4` but for bit 0. - /// - The jump is taken always, or when the one branch condition set holds. - /// - `jump` is that offset gated by the decision, so the successor `pc + 4 + jump` is linear in the row's columns. + /// - The output is that sum, unless a comparison replaces it by its bit. fn circuit() -> Circuit { - let mut c = Builder::new(&[64, 64, 64, 15, 64, 64], &[64, 64]); - let (v1, v2, imm, f, dt, pc4) = (c.input(0), c.input(1), c.input(2), c.input(3), c.input(4), c.input(5)); + let mut c = Builder::new(&[64, 64, 64, 4], &[64]); + let (v1, v2, imm, f) = (c.input(0), c.input(1), c.input(2), c.input(3)); let flag = |bit: u64| f[bit.trailing_zeros() as usize]; let b = c.xor_word(&v2, &imm); @@ -182,101 +91,41 @@ impl ClassCircuit for Alu { // // ltu = borrow // lt = borrow ^ sign(v1) ^ sign(b) - // eq = no bit of v1 ^ b set let ltu = c.not(carry_out); let signs = c.xor(v1[63], b[63]); let lt = c.xor(ltu, signs); - let diff = c.xor_word(&v1, &b); - let ne = c.any(&diff); - let eq = c.not(ne); - // The output: the sum unless a selector is set. - // - // and = v1 * b - // or = v1 * b ^ (v1 ^ b) - // xor = v1 ^ b + // The sum unless a comparison is selected, whose single bit is the output's bit 0. let sum = c.sext32_if(flag(Self::WORD), &sum); - let selectors = [Self::SEL_LT, Self::SEL_LTU, Self::SEL_AND, Self::SEL_OR, Self::SEL_XOR]; - let none = selectors.iter().fold(c.one(), |acc, &s| c.xor(acc, flag(s))); - let and_or = c.xor(flag(Self::SEL_AND), flag(Self::SEL_OR)); - let or_xor = c.xor(flag(Self::SEL_OR), flag(Self::SEL_XOR)); - let mut out = c.and_word(none, &sum); - for i in 0..64 { - let both = c.and(v1[i], b[i]); - let and_term = c.and(and_or, both); - let xor_term = c.and(or_xor, diff[i]); - let logic = c.xor(and_term, xor_term); - out[i] = c.xor(out[i], logic); - } - - // A comparison is a single bit, the output's bit 0. + let compares = c.xor(flag(Self::SEL_LT), flag(Self::SEL_LTU)); + let keeps = c.not(compares); + let mut out = c.and_word(keeps, &sum); let lt_term = c.and(flag(Self::SEL_LT), lt); let ltu_term = c.and(flag(Self::SEL_LTU), ltu); let compared = c.xor(lt_term, ltu_term); out[0] = c.xor(out[0], compared); - // An indirect jump outputs its link, and offsets the successor by the sum's difference from it. - // - // out = out ^ indirect * (out ^ pc4) = pc4 when indirect - // jump = dt ^ indirect * (out ^ pc4), bit 0 kept = the sum with bit 0 cleared, XOR pc4 - let indirect = flag(Self::INDIRECT); - let mut offset = dt; - for i in 0..64 { - let d = c.xor(out[i], pc4[i]); - let moved = c.and(indirect, d); - out[i] = c.xor(out[i], moved); - if i > 0 { - offset[i] = c.xor(offset[i], moved); - } - } - - // The jump: unconditional, or the one branch condition set. - let (ge, geu) = (c.not(lt), c.not(ltu)); - let taken = [ - (Self::BR_EQ, eq), - (Self::BR_NE, ne), - (Self::BR_LT, lt), - (Self::BR_GE, ge), - (Self::BR_LTU, ltu), - (Self::BR_GEU, geu), - ] - .into_iter() - .fold(flag(Self::ALWAYS), |acc, (when, holds)| { - let term = c.and(flag(when), holds); - c.xor(acc, term) - }); - - // Each bit of the jump is a product written at its output position, so it costs no copy. c.output_word(0, &out); - for (i, &bit) in offset.iter().enumerate() { - c.and_output(1, i, taken, bit); - } c.finish() } } -impl Alu { - /// One instance of the circuit's witness by word arithmetic: what the walk of [`Alu::circuit`] writes, into zeroed buffers. +impl Add { + /// One instance of the circuit's witness by word arithmetic: what the walk of [`Add::circuit`] writes, into zeroed buffers. /// - /// Inputs `v1`, `v2`, `imm`, the flags' 15 bits, `dt` and `pc4`, the outputs `out` and `jump` (each bit of `jump` the product `taken * offset`), the constant at bit 512, then the products: + /// Inputs `v1`, `v2`, `imm` and the flags' 4 bits, the output `out`, the constant at bit 320, then the products: /// /// ```text /// adder 64 A·z = v1 ^ c, B·z = (b ^ sub) ^ c, c the carries of v1 + (b ^ sub) + sub - /// any 63 A·z = the OR of diff's bits below, B·z = diff's bit /// sext32 32 A·z = word, B·z = sum_31 ^ sum_i - /// none 64 A·z = none, B·z = the sign-extended sum - /// logic 192 per bit: v1 * b, and_or * that, or_xor * diff + /// keeps 64 A·z = keeps, B·z = the sign-extended sum /// comparisons 2 SEL_LT * lt, SEL_LTU * ltu - /// indirect 64 INDIRECT * (out ^ pc4) - /// branches 6 each condition's flag * whether it holds /// ``` pub(crate) fn witness(inputs: &[u64], z: &mut [u64], az: &mut [u64], bz: &mut [u64]) { - const FLAG_BITS: u64 = (1 << 15) - 1; - let (v1, v2, imm, flags) = (inputs[0], inputs[1], inputs[2], inputs[3] & FLAG_BITS); - let (dt, pc4) = (inputs[4], inputs[5]); + const FLAG_BITS: u64 = (1 << 4) - 1; + let (v1, b, flags) = (inputs[0], inputs[1] ^ inputs[2], inputs[3] & FLAG_BITS); let flag = |bit: u64| u64::from(flags & bit != 0); let all = |bit: u64| u64::from(bit != 0).wrapping_neg(); - let b = v2 ^ imm; let sub = flag(Self::SUB); // The adder: the carry into each bit, and out of the top. @@ -286,63 +135,291 @@ impl Alu { let carries = sum ^ v1 ^ y; let ltu = u64::from(!(o1 | o2)); let lt = ltu ^ (v1 ^ b) >> 63; - let diff = v1 ^ b; - let ne = u64::from(diff != 0); + // The sum, sign-extended for a word form, unless a comparison replaces it by its bit. let word = all(flag(Self::WORD)); let sext_diff = ((sum >> 31 & 1).wrapping_neg() ^ sum) >> 32; let extended = sum ^ (word & sext_diff) << 32; - let none = 1 - ^ flag(Self::SEL_LT) - ^ flag(Self::SEL_LTU) - ^ flag(Self::SEL_AND) - ^ flag(Self::SEL_OR) - ^ flag(Self::SEL_XOR); - let and_or = all(flag(Self::SEL_AND) ^ flag(Self::SEL_OR)); - let or_xor = all(flag(Self::SEL_OR) ^ flag(Self::SEL_XOR)); - let both = v1 & b; + let keeps = 1 ^ flag(Self::SEL_LT) ^ flag(Self::SEL_LTU); let (lt_term, ltu_term) = (flag(Self::SEL_LT) & lt, flag(Self::SEL_LTU) & ltu); - let selected = all(none) & extended ^ and_or & both ^ or_xor & diff ^ lt_term ^ ltu_term; + let out = all(keeps) & extended ^ lt_term ^ ltu_term; - // An indirect jump moves the output to `pc4` and the offset by the same difference but for bit 0. - let indirect = all(flag(Self::INDIRECT)); - let link = selected ^ pc4; - let moved = indirect & link; - let out = selected ^ moved; - let offset = dt ^ moved & !1; + // The ports. + let bits = [u64::MAX, u64::MAX, u64::MAX, FLAG_BITS]; + for (i, bits) in bits.into_iter().enumerate() { + (z[i], az[i], bz[i]) = (inputs[i] & bits, inputs[i] & bits, bits); + } + (z[4], az[4], bz[4]) = (out, out, u64::MAX); + + // The constant, then the products in the order the circuit makes them. + let mut rows = Products::new([z, az, bz], 5); + rows.push(1, 1, 1); + rows.push(v1 ^ carries, y ^ carries, 64); + rows.push(word >> 32, sext_diff, 32); + rows.push(all(keeps), extended, 64); + rows.push(flag(Self::SEL_LT), lt, 1); + rows.push(flag(Self::SEL_LTU), ltu, 1); + rows.finish(); + } +} + +/// One instance of the bitwise logic: AND, OR or XOR of `v1` and `b = v2 ^ imm`. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Logic { + /// The operation: one of its legal words. + pub flags: u64, + /// The first register's value. + pub v1: u64, + /// The second register's value. + pub v2: u64, + /// The immediate. + pub imm: u64, +} + +impl Logic { + /// Output `v1 & b`. + pub const AND: u64 = 1 << 0; + /// Output `v1 | b`. + pub const OR: u64 = 1 << 1; + /// Output `v1 ^ b`. + pub const XOR: u64 = 1 << 2; +} + +impl InstructionClass for Logic { + /// Exactly one operation. + const LEGAL: &'static [u64] = &[Self::AND, Self::OR, Self::XOR]; + + /// The result. + type Output = u64; + + fn eval(&self) -> u64 { + let (v1, b) = (self.v1, self.v2 ^ self.imm); + match self.flags { + Self::AND => v1 & b, + Self::OR => v1 | b, + _ => v1 ^ b, + } + } +} + +impl ClassCircuit for Logic { + /// The bitwise logic: `(v1, v2, imm, flags) -> out`, two products per bit. + /// + /// With `b = v2 ^ imm` and the selectors `or` and `xor`, bit by bit: + /// + /// ```text + /// p = (v1 ^ or) * (b ^ or) v1 & b, or !(v1 | b) when or + /// out = p ^ or ^ xor * (p ^ v1 ^ b) + /// ``` + fn circuit() -> Circuit { + let mut c = Builder::new(&[64, 64, 64, 3], &[64]); + let (v1, v2, imm, f) = (c.input(0), c.input(1), c.input(2), c.input(3)); + let flag = |bit: u64| f[bit.trailing_zeros() as usize]; + let (or, xor) = (flag(Self::OR), flag(Self::XOR)); + let b = c.xor_word(&v2, &imm); + for i in 0..64 { + let (x, y) = (c.xor(v1[i], or), c.xor(b[i], or)); + let p = c.and(x, y); + let diff = c.xor(v1[i], b[i]); + let flip = c.xor(p, diff); + let xor_term = c.and(xor, flip); + let kept = c.xor(p, or); + let bit = c.xor(kept, xor_term); + c.output(0, i, bit); + } + c.finish() + } +} + +impl Logic { + /// One instance of the circuit's witness by word arithmetic: what the walk of [`Logic::circuit`] writes, into zeroed buffers. + /// + /// Inputs `v1`, `v2`, `imm` and the flags' 3 bits, the output `out`, the constant at bit 320, then two products per + /// bit, bit by bit: + /// + /// ```text + /// p A·z = v1 ^ or, B·z = b ^ or + /// xor term A·z = xor, B·z = p ^ v1 ^ b + /// ``` + pub(crate) fn witness(inputs: &[u64], z: &mut [u64], az: &mut [u64], bz: &mut [u64]) { + const FLAG_BITS: u64 = (1 << 3) - 1; + let (v1, b, flags) = (inputs[0], inputs[1] ^ inputs[2], inputs[3] & FLAG_BITS); + let all = |bit: u64| u64::from(flags & bit != 0).wrapping_neg(); + let (or, xor) = (all(Self::OR), all(Self::XOR)); + let (x, y) = (v1 ^ or, b ^ or); + let p = x & y; + let flip = p ^ v1 ^ b; + let out = p ^ or ^ xor & flip; + + // The ports. + let bits = [u64::MAX, u64::MAX, u64::MAX, FLAG_BITS]; + for (i, bits) in bits.into_iter().enumerate() { + (z[i], az[i], bz[i]) = (inputs[i] & bits, inputs[i] & bits, bits); + } + (z[4], az[4], bz[4]) = (out, out, u64::MAX); + + // The constant, then the products in the order the circuit makes them. + let mut rows = Products::new([z, az, bz], 5); + rows.push(1, 1, 1); + rows.push_interleaved2([x, xor], [y, flip]); + rows.finish(); + } +} + +/// One conditional branch: whether `v1` and `v2` meet its condition, and the offset that moves the successor. +/// +/// A branch writes no register and has no immediate: its target is the entry's. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Branch { + /// The condition: one of its legal words. + pub flags: u64, + /// The first register's value. + pub v1: u64, + /// The second register's value. + pub v2: u64, + /// The jump's offset: the fixed target XOR `pc + 4`. + /// + /// The decision does not read it; the circuit gates it by the decision. + pub dt: u64, +} + +impl Branch { + /// Branch when `v1 == v2`. + pub const EQ: u64 = 1 << 0; + /// Branch when `v1 != v2`. + pub const NE: u64 = 1 << 1; + /// Branch when `v1 < v2`, signed. + pub const LT: u64 = 1 << 2; + /// Branch when `v1 >= v2`, signed. + pub const GE: u64 = 1 << 3; + /// Branch when `v1 < v2`, unsigned. + pub const LTU: u64 = 1 << 4; + /// Branch when `v1 >= v2`, unsigned. + pub const GEU: u64 = 1 << 5; +} + +impl InstructionClass for Branch { + /// Exactly one condition. + const LEGAL: &'static [u64] = &[Self::EQ, Self::NE, Self::LT, Self::GE, Self::LTU, Self::GEU]; + + /// Whether the branch is taken. + type Output = bool; + + fn eval(&self) -> bool { + let (v1, v2) = (self.v1, self.v2); + let (lt, ltu) = ((v1 as i64) < (v2 as i64), v1 < v2); + match self.flags { + Self::EQ => v1 == v2, + Self::NE => v1 != v2, + Self::LT => lt, + Self::GE => !lt, + Self::LTU => ltu, + _ => !ltu, + } + } +} + +impl ClassCircuit for Branch { + /// The branch: `(v1, v2, flags, dt) -> jump`. + /// + /// - The difference `v1 + !v2 + 1` borrows exactly when it does not carry out, and only its carries are used. + /// - The branch is taken when the one condition set holds. + /// - `jump` is `dt` gated by that decision, so the successor `pc + 4 + jump` is linear in the row's columns. + fn circuit() -> Circuit { + let mut c = Builder::new(&[64, 64, 6, 64], &[64]); + let (v1, v2, f, dt) = (c.input(0), c.input(1), c.input(2), c.input(3)); + let flag = |bit: u64| f[bit.trailing_zeros() as usize]; + let one = c.one(); + + // The comparisons, from the borrow and the signs. + // + // ltu = borrow + // lt = borrow ^ sign(v1) ^ sign(v2) + // eq = no bit of v1 ^ v2 set + let not_v2: Word = v2.iter().map(|&bit| c.not(bit)).collect(); + let (_, carry_out) = c.add_with_carry(&v1, ¬_v2, one); + let ltu = c.not(carry_out); + let signs = c.xor(v1[63], v2[63]); + let lt = c.xor(ltu, signs); + let diff = c.xor_word(&v1, &v2); + let ne = c.any(&diff); + let eq = c.not(ne); + + // The decision: the one condition set. + let (ge, geu) = (c.not(lt), c.not(ltu)); + let taken = [ + (Self::EQ, eq), + (Self::NE, ne), + (Self::LT, lt), + (Self::GE, ge), + (Self::LTU, ltu), + (Self::GEU, geu), + ] + .into_iter() + .fold(None, |acc, (when, holds)| { + let term = c.and(flag(when), holds); + c.xor(acc, term) + }); + + // Each bit of the jump is a product written at its output position, so it costs no copy. + for (i, &bit) in dt.iter().enumerate() { + c.and_output(0, i, taken, bit); + } + c.finish() + } +} + +impl Branch { + /// One instance of the circuit's witness by word arithmetic: what the walk of [`Branch::circuit`] writes, into zeroed buffers. + /// + /// Inputs `v1`, `v2`, the flags' 6 bits and `dt`, the output `jump` (each bit the product `taken * dt`), the constant + /// at bit 320, then the products: + /// + /// ```text + /// adder 64 A·z = v1 ^ c, B·z = !v2 ^ c, c the carries of v1 + !v2 + 1 + /// any 63 A·z = the OR of diff's bits below, B·z = diff's bit + /// conditions 6 each condition's flag * whether it holds + /// ``` + pub(crate) fn witness(inputs: &[u64], z: &mut [u64], az: &mut [u64], bz: &mut [u64]) { + const FLAG_BITS: u64 = (1 << 6) - 1; + let (v1, v2, flags, dt) = (inputs[0], inputs[1], inputs[2] & FLAG_BITS, inputs[3]); + let flag = |bit: u64| u64::from(flags & bit != 0); + + // The difference's carries, and the borrow out of the top. + let y = !v2; + let (partial, o1) = v1.overflowing_add(y); + let (sum, o2) = partial.overflowing_add(1); + let carries = sum ^ v1 ^ y; + let ltu = u64::from(!(o1 | o2)); + let diff = v1 ^ v2; + let lt = ltu ^ diff >> 63; + let ne = u64::from(diff != 0); let conditions = [ - (Self::BR_EQ, ne ^ 1), - (Self::BR_NE, ne), - (Self::BR_LT, lt), - (Self::BR_GE, lt ^ 1), - (Self::BR_LTU, ltu), - (Self::BR_GEU, ltu ^ 1), + (Self::EQ, ne ^ 1), + (Self::NE, ne), + (Self::LT, lt), + (Self::GE, lt ^ 1), + (Self::LTU, ltu), + (Self::GEU, ltu ^ 1), ]; - let taken = all(conditions - .iter() - .fold(flag(Self::ALWAYS), |acc, &(when, holds)| acc ^ flag(when) & holds)); + let taken = (conditions.iter()) + .fold(0, |acc, &(when, holds)| acc ^ flag(when) & holds) + .wrapping_neg(); // The ports. - let bits = [u64::MAX, u64::MAX, u64::MAX, FLAG_BITS, u64::MAX, u64::MAX]; + let bits = [u64::MAX, u64::MAX, FLAG_BITS, u64::MAX]; for (i, bits) in bits.into_iter().enumerate() { (z[i], az[i], bz[i]) = (inputs[i] & bits, inputs[i] & bits, bits); } - (z[6], az[6], bz[6]) = (out, out, u64::MAX); - (z[7], az[7], bz[7]) = (taken & offset, taken, offset); + (z[4], az[4], bz[4]) = (taken & dt, taken, dt); // The constant, then the products in the order the circuit makes them. - let mut rows = Products::new([z, az, bz], 8); + let mut rows = Products::new([z, az, bz], 5); rows.push(1, 1, 1); rows.push(v1 ^ carries, y ^ carries, 64); let below = diff.isolate_lowest_one().wrapping_neg(); rows.push(below & (u64::MAX >> 1), diff >> 1, 63); - rows.push(word >> 32, sext_diff, 32); - rows.push(all(none), extended, 64); - rows.push_interleaved3([v1, and_or, or_xor], [b, both, diff]); - rows.push(flag(Self::SEL_LT), lt, 1); - rows.push(flag(Self::SEL_LTU), ltu, 1); - rows.push(indirect, link, 64); for (when, holds) in conditions { rows.push(flag(when), holds, 1); } @@ -350,6 +427,107 @@ impl Alu { } } +/// One jump: `JAL` and the exit to the entry's fixed target, `JALR` to `v1 + imm` with bit 0 cleared. +/// +/// Every jump is taken, and links `pc + 4`, which its table writes to `rd` itself. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub struct Jump { + /// Direct or indirect: one of its legal words. + pub flags: u64, + /// The first register's value. + pub v1: u64, + /// The immediate. + pub imm: u64, + /// The jump's offset: the fixed target XOR `pc + 4`, zero for an indirect jump. + pub dt: u64, + /// The fall-through address `pc + 4`, what an indirect target is taken against. + pub pc4: u64, +} + +impl Jump { + /// Jump to `v1 + imm` with bit 0 cleared, as `JALR` does, rather than to the entry's fixed target. + pub const INDIRECT: u64 = 1 << 0; +} + +impl InstructionClass for Jump { + /// `JAL` and the exit, then `JALR`. + const LEGAL: &'static [u64] = &[0, Self::INDIRECT]; + + /// What the successor adds to `pc + 4`. + /// + /// - A fixed jump adds its offset, the target XOR `pc + 4`. + /// - An indirect jump has offset zero and adds the sum XOR `pc + 4`, bit 0 left out. + /// - Its successor is then the sum with bit 0 cleared, since `pc + 4` is even. + type Output = u64; + + fn eval(&self) -> u64 { + if self.flags & Self::INDIRECT == 0 { + self.dt + } else { + self.dt ^ ((self.v1.wrapping_add(self.imm) ^ self.pc4) & !1) + } + } +} + +impl ClassCircuit for Jump { + /// The jump: `(v1, imm, flags, dt, pc4) -> jump`. + /// + /// - The computed target is `v1 + imm`; its bit 0 is never made, the target clearing it. + /// - `jump` is `dt`, plus the target XOR `pc + 4` for an indirect jump, bit 0 kept, so the successor + /// `pc + 4 + jump` is linear in the row's columns. + fn circuit() -> Circuit { + let mut c = Builder::new(&[64, 64, 1, 64, 64], &[64]); + let (v1, imm, f, dt, pc4) = (c.input(0), c.input(1), c.input(2), c.input(3), c.input(4)); + let indirect = f[Self::INDIRECT.trailing_zeros() as usize]; + let target = c.add_wrapping(&v1, &imm); + + // jump = dt ^ indirect * (target ^ pc4), bit 0 kept + c.output(0, 0, dt[0]); + for i in 1..64 { + let d = c.xor(target[i], pc4[i]); + let moved = c.and(indirect, d); + let bit = c.xor(dt[i], moved); + c.output(0, i, bit); + } + c.finish() + } +} + +impl Jump { + /// One instance of the circuit's witness by word arithmetic: what the walk of [`Jump::circuit`] writes, into zeroed buffers. + /// + /// Inputs `v1`, `imm`, the flag's bit, `dt` and `pc4`, the output `jump`, the constant at bit 384, then the products: + /// + /// ```text + /// adder 63 A·z = v1 ^ c, B·z = imm ^ c, c the carries of v1 + imm, none out of the top + /// indirect 63 A·z = INDIRECT, B·z = (v1 + imm) ^ pc4, bits 1 to 63 + /// ``` + pub(crate) fn witness(inputs: &[u64], z: &mut [u64], az: &mut [u64], bz: &mut [u64]) { + const FLAG_BITS: u64 = 1; + let (v1, imm, flags, dt, pc4) = (inputs[0], inputs[1], inputs[2] & FLAG_BITS, inputs[3], inputs[4]); + let indirect = u64::from(flags & Self::INDIRECT != 0).wrapping_neg(); + let target = v1.wrapping_add(imm); + let carries = target ^ v1 ^ imm; + let link = target ^ pc4; + let jump = dt ^ indirect & link & !1; + + // The ports. + let bits = [u64::MAX, u64::MAX, FLAG_BITS, u64::MAX, u64::MAX]; + for (i, bits) in bits.into_iter().enumerate() { + (z[i], az[i], bz[i]) = (inputs[i] & bits, inputs[i] & bits, bits); + } + (z[5], az[5], bz[5]) = (jump, jump, u64::MAX); + + // The constant, then the products in the order the circuit makes them. + let mut rows = Products::new([z, az, bz], 6); + rows.push(1, 1, 1); + let low = u64::MAX >> 1; + rows.push((v1 ^ carries) & low, (imm ^ carries) & low, 63); + rows.push(indirect >> 1, link >> 1, 63); + rows.finish(); + } +} + #[cfg(test)] mod tests { use super::*; @@ -364,74 +542,131 @@ mod tests { use proptest::strategy::BoxedStrategy; use std::sync::LazyLock; - /// Any ALU instance, as the decoder makes them: one of `v2` and `imm` is zero. - impl Arbitrary for Alu { + /// An operand pair as the decoder makes them: one of `v2` and `imm` is zero, and now and then the second operand + /// equals `v1`, which random words never do. + fn operands() -> impl Strategy { + (edge_word(), edge_word(), any::(), any::()).prop_map(|(v1, v2, equal, immediate)| { + let v2 = if equal { v1 } else { v2 }; + let (v2, imm) = if immediate { (0, v2) } else { (v2, 0) }; + (v1, v2, imm) + }) + } + + impl Arbitrary for Add { + type Parameters = (); + type Strategy = BoxedStrategy; + + fn arbitrary_with((): ()) -> Self::Strategy { + (select(Self::LEGAL), operands()) + .prop_map(|(flags, (v1, v2, imm))| Self { flags, v1, v2, imm }) + .boxed() + } + } + + impl Arbitrary for Logic { + type Parameters = (); + type Strategy = BoxedStrategy; + + fn arbitrary_with((): ()) -> Self::Strategy { + (select(Self::LEGAL), operands()) + .prop_map(|(flags, (v1, v2, imm))| Self { flags, v1, v2, imm }) + .boxed() + } + } + + impl Arbitrary for Branch { + type Parameters = (); + type Strategy = BoxedStrategy; + + fn arbitrary_with((): ()) -> Self::Strategy { + (select(Self::LEGAL), operands(), any::()) + .prop_map(|(flags, (v1, v2, imm), dt)| Self { + flags, + v1, + v2: v2 ^ imm, + dt, + }) + .boxed() + } + } + + impl Arbitrary for Jump { type Parameters = (); type Strategy = BoxedStrategy; fn arbitrary_with((): ()) -> Self::Strategy { - // Equal operands now and then, which random words never are. ( select(Self::LEGAL), edge_word(), edge_word(), - any::(), - any::(), any::(), any::(), ) - .prop_map(|(flags, v1, v2, equal, immediate, dt, pc4)| { - let v2 = if equal { v1 } else { v2 }; - let (v2, imm) = if immediate { (0, v2) } else { (v2, 0) }; - Self { - flags, - v1, - v2, - imm, - dt, - pc4, - } + .prop_map(|(flags, v1, imm, dt, pc4)| Self { + flags, + v1, + imm, + dt, + pc4, }) .boxed() } } - static ALU: LazyLock = LazyLock::new(Alu::circuit); + static BRANCH: LazyLock = LazyLock::new(Branch::circuit); #[test] - fn alu_circuit_matches_the_reference() { - // Legal flags and edge-biased operands pin the gate list to the reference function. - circuit_matches_reference::(4096); + fn every_alu_class_circuit_matches_its_reference() { + // Legal flags and edge-biased operands pin each gate list to its reference function. + circuit_matches_reference::(4096); + circuit_matches_reference::(4096); + circuit_matches_reference::(4096); + circuit_matches_reference::(4096); } #[test] - fn the_word_witness_is_the_gate_walk() { - // Every legal flag word on edge operands: `b` an edge word or its complement, equal to `v1` on the diagonal, `dt` and `pc4` each none or all of their bits. - let edges = grid(&[ - &EDGES, - &EDGES, - &[0, u64::MAX], - Alu::LEGAL, - &[0, u64::MAX], - &[0, u64::MAX], - ]); - word_witness_is_the_walk::(Alu::witness, edges); + fn every_alu_class_word_witness_is_the_gate_walk() { + // Every legal flag word on edge operands: the second operand an edge word or its complement, equal to `v1` on + // the diagonal, and `dt` and `pc4` each none or all of their bits. + let both = [0, u64::MAX]; + word_witness_is_the_walk::(Add::witness, grid(&[&EDGES, &EDGES, &both, Add::LEGAL])); + word_witness_is_the_walk::(Logic::witness, grid(&[&EDGES, &EDGES, &both, Logic::LEGAL])); + word_witness_is_the_walk::(Branch::witness, grid(&[&EDGES, &EDGES, Branch::LEGAL, &both])); + word_witness_is_the_walk::(Jump::witness, grid(&[&EDGES, &EDGES, Jump::LEGAL, &both, &both])); } #[test] - fn flock_proves_honest_alu_instances_and_refuses_a_flipped_bit() { + fn an_indirect_jump_lands_on_its_target_with_bit_0_cleared() { + // Invariant: `pc + 4 + jump` is `JALR`'s target, and a fixed jump's offset is the entry's. + let (v1, imm, pc4) = (0x1000_0001, 6, 0x2000_0004); + let indirect = Jump { + flags: Jump::INDIRECT, + v1, + imm, + dt: 0, + pc4, + }; + assert_eq!(pc4 ^ indirect.eval(), 0x1000_0006); + let direct = Jump { + flags: 0, + dt: 0x44, + ..indirect + }; + assert_eq!(direct.eval(), 0x44); + } + + #[test] + fn flock_proves_honest_branch_instances_and_refuses_a_flipped_bit() { // Fixture: 16 instances cycling through the legal words. - const LABEL: &[u8] = b"rv-alu-reduction-test"; - let block = ALU.block(); + const LABEL: &[u8] = b"rv-branch-reduction-test"; + let block = BRANCH.block(); let n_log = 4; - let rows: Vec<[u64; 6]> = (0..1u64 << n_log) + let rows: Vec<[u64; 4]> = (0..1u64 << n_log) .map(|i| { [ i.wrapping_mul(0x9e37_79b9_7f4a_7c15), !i, - 0, - Alu::LEGAL[i as usize % Alu::LEGAL.len()], - i << 2, + Branch::LEGAL[i as usize % Branch::LEGAL.len()], i << 3, ] }) @@ -439,7 +674,7 @@ mod tests { // Prove the batch, optionally flipping one witness bit first, and verify. let accepts = |tamper: Option| { - let mut witness = ALU.generate_witness(&rows, n_log); + let mut witness = BRANCH.generate_witness(&rows, n_log); if let Some(bit) = tamper { witness.z[bit / 64] ^= 1 << (bit % 64); witness.stripes[bit] ^= 1; @@ -455,26 +690,58 @@ mod tests { }; assert!(accepts(None)); - // Mutation: an output bit, a bit of the jump, the last product. - for bit in [ - 64 * ALU.n_input_words() + 5, - 64 * (ALU.n_input_words() + 1) + 3, - ALU.useful_bits() - 1, - ] { + // Mutation: a bit of the jump, a spare bit of the flags' word, the last product. + for bit in [64 * BRANCH.n_input_words() + 3, 64 * 2 + 7, BRANCH.useful_bits() - 1] { assert!(!accepts(Some(bit)), "flipping bit {bit} must reject"); } } - impl Ports for Alu { - const CLASS: Class = Class::Alu; + impl Ports for Add { + const CLASS: Class = Class::Add; + + fn input_words(&self) -> Vec { + vec![self.v1, self.v2, self.imm, self.flags] + } + + fn output_words(&self, &out: &u64) -> Vec { + vec![out] + } + } + + impl Ports for Logic { + const CLASS: Class = Class::Logic; + + fn input_words(&self) -> Vec { + vec![self.v1, self.v2, self.imm, self.flags] + } + + fn output_words(&self, &out: &u64) -> Vec { + vec![out] + } + } + + impl Ports for Branch { + const CLASS: Class = Class::Branch; + + fn input_words(&self) -> Vec { + vec![self.v1, self.v2, self.flags, self.dt] + } + + // The offset the successor adds to `pc + 4`: the entry's when the branch is taken, zero otherwise. + fn output_words(&self, &taken: &bool) -> Vec { + vec![if taken { self.dt } else { 0 }] + } + } + + impl Ports for Jump { + const CLASS: Class = Class::Jump; fn input_words(&self) -> Vec { - vec![self.v1, self.v2, self.imm, self.flags, self.dt, self.pc4] + vec![self.v1, self.imm, self.flags, self.dt, self.pc4] } - // The output, and the offset the successor adds to `pc + 4`. - fn output_words(&self, &(out, taken): &(u64, bool)) -> Vec { - vec![out, self.jump(taken)] + fn output_words(&self, &jump: &u64) -> Vec { + vec![jump] } } } diff --git a/crates/leanvm_core/src/rv/semantics/mod.rs b/crates/leanvm_core/src/rv/semantics/mod.rs index d71273be5..9ed820845 100644 --- a/crates/leanvm_core/src/rv/semantics/mod.rs +++ b/crates/leanvm_core/src/rv/semantics/mod.rs @@ -22,7 +22,7 @@ mod memory; mod multiply; mod shift; -pub use alu::Alu; +pub use alu::{Add, Branch, Jump, Logic}; pub use divide::Div; pub use ext::{Ext, Limb}; pub use hash::{BlockAccess, Hash, blake2s_witness}; @@ -109,7 +109,7 @@ pub(super) mod tests { let w = |x: u32| x as i32 as i64 as u64; let (a, b) = (v1 as u32, v2 as u32); let shift = |flags| Shift { flags, v1, v2, imm: 0 }.eval(); - prop_assert_eq!(Alu { flags: Alu::WORD, v1, v2, imm: 0, dt: 0, pc4: 0 }.eval().0, w(a.wrapping_add(b))); + prop_assert_eq!(Add { flags: Add::WORD, v1, v2, imm: 0 }.eval(), w(a.wrapping_add(b))); prop_assert_eq!(Mul { flags: Mul::WORD, v1, v2 }.eval(), w(a.wrapping_mul(b))); prop_assert_eq!(shift(Shift::WORD), w(a << (b & 31))); prop_assert_eq!(shift(Shift::WORD | Shift::RIGHT), w(a >> (b & 31))); diff --git a/crates/leanvm_core/src/tables/columns.rs b/crates/leanvm_core/src/tables/columns.rs index da60f8433..0a36a0ffe 100644 --- a/crates/leanvm_core/src/tables/columns.rs +++ b/crates/leanvm_core/src/tables/columns.rs @@ -1,6 +1,6 @@ //! Local column allocation and the aliases used by memory moves. -use super::{ClassSpec, Ram, Word}; +use super::{ClassSpec, Control, Ram, Word}; use crate::leaf::Coord::{self, Col}; use crate::rv::{Ext, Hash}; @@ -37,7 +37,7 @@ pub(super) struct DestinationColumns { pub(super) out: usize, } -/// Columns of a class with branches and jumps, the exit included. +/// Columns of a class with branches or jumps, a jump's exit included. #[derive(Clone, Copy)] pub(super) struct ControlColumns { /// Decoded jump offset, a circuit input. @@ -46,8 +46,8 @@ pub(super) struct ControlColumns { /// The offset when the jump is taken, zero otherwise: a circuit output. pub(super) jump: usize, - /// Selector for the exit instruction. - pub(super) exit: usize, + /// Selector for the exit instruction: a jump's column, a branch's constant zero. + pub(super) exit: Option, } impl ControlColumns { @@ -200,22 +200,22 @@ impl Columns { a2: allocator.allocate(1), v2: allocator.allocate(1), }); - // A doubleword load's `rd` receives its cell, which is a column further on. + // A doubleword load's `rd` receives its cell, which is a column further on, and a jump's its link, `pc + 4`. let rd = spec.writes_rd.then(|| { ( allocator.allocate(1), allocator.allocate(1), - (!spec.copies).then(|| allocator.allocate(1)), + (!spec.copies && spec.control != Control::Jump).then(|| allocator.allocate(1)), ) }); let pointer = spec.reads_rd.then(|| PointerColumns { ad: allocator.allocate(1), vd: allocator.allocate(1), }); - let control = spec.control.then(|| ControlColumns { + let control = (spec.control != Control::None).then(|| ControlColumns { dt: allocator.allocate(1), jump: allocator.allocate(1), - exit: allocator.allocate(1), + exit: (spec.control == Control::Jump).then(|| allocator.allocate(1)), }); let imm = spec.words().any(|w| w == Word::Imm).then(|| allocator.allocate(1)); let (ram, block) = match spec.ram { @@ -243,7 +243,7 @@ impl Columns { let rd = rd.map(|(ad, vd_old, out)| DestinationColumns { ad, vd_old, - out: out.unwrap_or_else(|| ram.expect("a doubleword load reads a cell").cell), + out: out.unwrap_or_else(|| ram.map_or(pc4, |ram| ram.cell)), }); let limbs = (spec.ram == Ram::Limbs).then(|| LimbColumns { limbs: allocator.allocate(Ext::LIMBS), diff --git a/crates/leanvm_core/src/tables/fill.rs b/crates/leanvm_core/src/tables/fill.rs index 948bdcad9..3c9e9e4c8 100644 --- a/crates/leanvm_core/src/tables/fill.rs +++ b/crates/leanvm_core/src/tables/fill.rs @@ -176,8 +176,8 @@ impl ClassTable { ctx.columns_at(out, rows, [rd.ad, rd.vd_old], move |r| { [F64(entry(r).ad as u64), F64(r.vd_old)] }); - // A doubleword load's result is its cell's column, written with the cell. - if c.ram.is_none_or(|ram| ram.cell != rd.out) { + // A doubleword load's result is its cell's column, written with the cell, and a jump's link is `pc + 4`. + if rd.out != c.pc4 && c.ram.is_none_or(|ram| ram.cell != rd.out) { ctx.column(out, rows, rd.out, move |r| F64(r.out)); } } @@ -187,14 +187,13 @@ impl ClassTable { ctx.column(out, ext, p.vd, |x| F64(x.instance.pointers[2])); } if let Some(k) = c.control { - ctx.columns_at(out, rows, [k.dt, k.jump, k.exit], move |r| { + ctx.columns_at(out, rows, [k.dt, k.jump], move |r| { let at = p.fetch(r.index as usize); - [ - F64(at.dt), - F64(Word::Jump.value(RowRef::plain(r), at, &[])), - F64(at.entry.is_exit() as u64), - ] + [F64(at.dt), F64(Word::Jump.value(RowRef::plain(r), at, &[]))] }); + if let Some(exit) = k.exit { + ctx.column(out, rows, exit, move |r| F64(entry(r).is_exit() as u64)); + } } if let Some(imm) = c.imm { ctx.column(out, rows, imm, move |r| F64(entry(r).imm)); diff --git a/crates/leanvm_core/src/tables/id.rs b/crates/leanvm_core/src/tables/id.rs index d9aeab649..ee3433a56 100644 --- a/crates/leanvm_core/src/tables/id.rs +++ b/crates/leanvm_core/src/tables/id.rs @@ -7,7 +7,7 @@ use std::ops::{Index, IndexMut}; use std::slice::Iter; /// Number of instruction tables in the proof layout. -pub const N_TABLES: usize = 11; +pub const N_TABLES: usize = 14; /// An instruction table, named by the class it proves. /// @@ -16,8 +16,14 @@ pub const N_TABLES: usize = 11; pub struct TableId(Class); impl TableId { - /// Arithmetic, comparisons, logic, branches and jumps. - pub const ALU: Self = Self(Class::Alu); + /// Sums, differences and comparisons. + pub const ADD: Self = Self(Class::Add); + /// AND, OR and XOR. + pub const LOGIC: Self = Self(Class::Logic); + /// The conditional branches. + pub const BRANCH: Self = Self(Class::Branch); + /// `jal`, `jalr` and the exit. + pub const JUMP: Self = Self(Class::Jump); /// Byte, halfword and word loads. pub const LOAD: Self = Self(Class::Load); /// Byte, halfword and word stores. @@ -41,7 +47,10 @@ impl TableId { /// Every table, in protocol order. pub const ALL: [Self; N_TABLES] = [ - Self::ALU, + Self::ADD, + Self::LOGIC, + Self::BRANCH, + Self::JUMP, Self::LOAD, Self::STORE, Self::LD, @@ -76,7 +85,10 @@ impl TableId { /// The table's specification. pub const fn spec(self) -> &'static ClassSpec { match self.0 { - Class::Alu => &ClassSpec::ALU, + Class::Add => &ClassSpec::ADD, + Class::Logic => &ClassSpec::LOGIC, + Class::Branch => &ClassSpec::BRANCH, + Class::Jump => &ClassSpec::JUMP, Class::Load => &ClassSpec::LOAD, Class::Store => &ClassSpec::STORE, Class::Ld => &ClassSpec::LD, diff --git a/crates/leanvm_core/src/tables/mod.rs b/crates/leanvm_core/src/tables/mod.rs index 787f7cb5e..8b460dc00 100644 --- a/crates/leanvm_core/src/tables/mod.rs +++ b/crates/leanvm_core/src/tables/mod.rs @@ -14,7 +14,7 @@ mod word; pub use clock::Clock; pub use id::{N_TABLES, PerTable, TableId, TableKey}; -pub use spec::{BAD_SLOT, ClassSpec, EXIT_SLOT, Fill, N_CIRCUITS, Ram}; +pub use spec::{BAD_SLOT, ClassSpec, Control, EXIT_SLOT, Fill, N_CIRCUITS, Ram}; pub use table::ClassTable; pub use word::Word; diff --git a/crates/leanvm_core/src/tables/spec.rs b/crates/leanvm_core/src/tables/spec.rs index e6e291b97..86f91b98a 100644 --- a/crates/leanvm_core/src/tables/spec.rs +++ b/crates/leanvm_core/src/tables/spec.rs @@ -2,7 +2,7 @@ use super::clock::Clock; use super::{N_TABLES, TableId, Word}; -use crate::rv::{Alu, Class, Ext, Hash, Ld, Load, Mul, Mulh, Shift, Store}; +use crate::rv::{Add, Branch, Class, Ext, Hash, Jump, Ld, Load, Logic, Mul, Mulh, Shift, Store}; use crate::{class_flock, rv}; use flock::circuit::Circuit; use std::ops::Range; @@ -34,6 +34,21 @@ impl Ram { } } +/// Where a class's rows send control. +#[derive(Clone, Copy, Debug, PartialEq, Eq)] +pub enum Control { + /// To `pc + 4`. + None, + /// A branch: to `pc + 4` plus the circuit's jump, the bytecode's offset gated by the decision. + /// + /// The bytecode's exit selector is the constant zero. + Branch, + /// A jump: to `pc + 4` plus the circuit's jump, which also takes `pc + 4` for an indirect target. + /// + /// It links: `rd` receives `pc + 4`, and the bytecode's exit selector is a column. + Jump, +} + /// One instance's `z`, `A·z` and `B·z` from its input words, into zeroed buffers. pub type InstanceWitness = fn(&[u64], &mut [u64], &mut [u64], &mut [u64]); @@ -74,8 +89,8 @@ pub struct ClassSpec { /// Table name used in diagnostics and reports. pub name: &'static str, - /// Whether branches and jumps move the successor by the circuit's jump. - pub control: bool, + /// How branches and jumps move the successor. + pub control: Control, /// Whether the second source register is read, in clock slot 1. pub reads_rs2: bool, @@ -106,21 +121,88 @@ pub struct ClassSpec { } impl ClassSpec { - /// Arithmetic, comparisons, logic, branches, and jumps. - pub const ALU: Self = Self { - class: Class::Alu, - name: "ALU", - control: true, + /// Addition, subtraction and comparisons, and the constants `lui` and `auipc` add to `x0`. + pub const ADD: Self = Self { + class: Class::Add, + name: "ADD", + control: Control::None, reads_rs2: true, writes_rd: true, reads_rd: false, ram: Ram::None, copies: false, circuit: Some(ClassCircuit { - k_log: 10, - inputs: &[Word::V1, Word::V2, Word::Imm, Word::Flags, Word::Dt, Word::Pc4], - outputs: &[Word::Out, Word::Jump], - fill: Fill::Instance(Alu::witness), + k_log: 9, + inputs: &[Word::V1, Word::V2, Word::Imm, Word::Flags], + outputs: &[Word::Out], + fill: Fill::Instance(Add::witness), + }), + clock_k_log: 9, + clock_inputs: &[], + clock_outputs: &[], + }; + + /// AND, OR and XOR. + pub const LOGIC: Self = Self { + class: Class::Logic, + name: "LOGIC", + control: Control::None, + reads_rs2: true, + writes_rd: true, + reads_rd: false, + ram: Ram::None, + copies: false, + circuit: Some(ClassCircuit { + k_log: 9, + inputs: &[Word::V1, Word::V2, Word::Imm, Word::Flags], + outputs: &[Word::Out], + fill: Fill::Instance(Logic::witness), + }), + clock_k_log: 9, + clock_inputs: &[], + clock_outputs: &[], + }; + + /// The conditional branches. + /// + /// A branch writes no `rd` and has no immediate: its bytecode tuple holds the sink and zero there. + pub const BRANCH: Self = Self { + class: Class::Branch, + name: "BRANCH", + control: Control::Branch, + reads_rs2: true, + writes_rd: false, + reads_rd: false, + ram: Ram::None, + copies: false, + circuit: Some(ClassCircuit { + k_log: 9, + inputs: &[Word::V1, Word::V2, Word::Flags, Word::Dt], + outputs: &[Word::Jump], + fill: Fill::Instance(Branch::witness), + }), + clock_k_log: 9, + clock_inputs: &[], + clock_outputs: &[], + }; + + /// `jal`, `jalr` and the exit. + /// + /// A jump reads no `rs2`: its bytecode tuple holds `x0` there. + pub const JUMP: Self = Self { + class: Class::Jump, + name: "JUMP", + control: Control::Jump, + reads_rs2: false, + writes_rd: true, + reads_rd: false, + ram: Ram::None, + copies: false, + circuit: Some(ClassCircuit { + k_log: 9, + inputs: &[Word::V1, Word::Imm, Word::Flags, Word::Dt, Word::Pc4], + outputs: &[Word::Jump], + fill: Fill::Instance(Jump::witness), }), clock_k_log: 9, clock_inputs: &[], @@ -131,7 +213,7 @@ impl ClassSpec { pub const LOAD: Self = Self { class: Class::Load, name: "LOAD", - control: false, + control: Control::None, reads_rs2: false, writes_rd: true, reads_rd: false, @@ -152,7 +234,7 @@ impl ClassSpec { pub const STORE: Self = Self { class: Class::Store, name: "STORE", - control: false, + control: Control::None, reads_rs2: true, writes_rd: false, reads_rd: false, @@ -173,7 +255,7 @@ impl ClassSpec { pub const LD: Self = Self { class: Class::Ld, name: "LD", - control: false, + control: Control::None, reads_rs2: false, writes_rd: true, reads_rd: false, @@ -194,7 +276,7 @@ impl ClassSpec { pub const SD: Self = Self { class: Class::Sd, name: "SD", - control: false, + control: Control::None, reads_rs2: true, writes_rd: false, reads_rd: false, @@ -215,7 +297,7 @@ impl ClassSpec { pub const SHIFT: Self = Self { class: Class::Shift, name: "SHIFT", - control: false, + control: Control::None, reads_rs2: true, writes_rd: true, reads_rd: false, @@ -236,7 +318,7 @@ impl ClassSpec { pub const MUL: Self = Self { class: Class::Mul, name: "MUL", - control: false, + control: Control::None, reads_rs2: true, writes_rd: true, reads_rd: false, @@ -261,7 +343,7 @@ impl ClassSpec { pub const MULH: Self = Self { class: Class::Mulh, name: "MULH", - control: false, + control: Control::None, reads_rs2: true, writes_rd: true, reads_rd: false, @@ -282,7 +364,7 @@ impl ClassSpec { pub const DIV: Self = Self { class: Class::Div, name: "DIV", - control: false, + control: Control::None, reads_rs2: true, writes_rd: true, reads_rd: false, @@ -303,7 +385,7 @@ impl ClassSpec { pub const HASH: Self = Self { class: Class::Hash, name: "HASH", - control: false, + control: Control::None, reads_rs2: true, writes_rd: false, reads_rd: false, @@ -343,7 +425,7 @@ impl ClassSpec { pub const EXT: Self = Self { class: Class::Ext, name: "EXT", - control: false, + control: Control::None, reads_rs2: true, writes_rd: false, reads_rd: true, @@ -366,11 +448,12 @@ impl ClassSpec { /// Check that register accesses and copy semantics match the circuit ports. pub(super) fn assert_valid(&self) { - // Invariant: a register access exists exactly when its value is a word of one of the table's circuits, or a column a doubleword load or store moves. + // Invariant: a register access exists exactly when its value is a word of one of the table's circuits, or a + // column a doubleword load or store moves, or the link a jump writes. let has = |word: Word| self.words().any(|w| w == word); assert_eq!(self.reads_rs2 && !self.copies, has(Word::V2), "{}: rs2 read", self.name); assert_eq!( - self.writes_rd && !self.copies, + self.writes_rd && !self.copies && self.control != Control::Jump, has(Word::Out), "{}: rd write", self.name @@ -381,9 +464,12 @@ impl ClassSpec { "{}: rd is read or written, not both", self.name ); - // A class with branches and jumps gates the bytecode's offset in its circuit, and reads `pc + 4` for its indirect jump. + // A class with branches or jumps gates the bytecode's offset in its circuit, and a jump links, and reads + // `pc + 4` for its indirect target. assert!( - self.control == (has(Word::Dt) && has(Word::Jump)) && self.control == has(Word::Pc4), + (self.control != Control::None) == (has(Word::Dt) && has(Word::Jump)) + && (self.control == Control::Jump) == has(Word::Pc4) + && (self.control != Control::Jump || self.writes_rd), "{}: control flow", self.name ); @@ -396,7 +482,7 @@ impl ClassSpec { }; let ports = [Word::V1, Word::Imm, Word::Address]; assert!( - moves && !self.control && !self.reads_rd && self.ports().eq(ports), + moves && self.control == Control::None && !self.reads_rd && self.ports().eq(ports), "{}: a copy", self.name ); diff --git a/crates/leanvm_core/src/tables/table.rs b/crates/leanvm_core/src/tables/table.rs index a816e01da..69065a1a3 100644 --- a/crates/leanvm_core/src/tables/table.rs +++ b/crates/leanvm_core/src/tables/table.rs @@ -188,11 +188,13 @@ impl ClassTable { /// Bind the next instruction and clock to the current state. /// - /// The successor is linear in the row's columns: `pc + 4`, plus the circuit's jump for a class with control flow. + /// The successor is linear in the row's columns: `pc + 4`, plus the circuit's jump for a branch or a jump. + /// + /// Only a jump has an exit selector; a branch's is the constant zero. fn flush_state(&self, bus: &mut FlushBuilder) { let c = &self.cols; let npc = c.control.map_or(Col(c.pc4), |control| control.next_pc(c.pc4)); - let exit = c.control.map_or(Const(F64::ZERO), |control| Col(control.exit)); + let exit = c.control.and_then(|k| k.exit).map_or(Const(F64::ZERO), Col); bus.state(c.pc, c.ts, c.step, npc, exit); } @@ -227,7 +229,7 @@ impl ClassTable { entry.push(Col(bad)); } entry.resize(EXIT_SLOT, Const(F64::ZERO)); - entry.push(c.control.map_or(Const(F64::ZERO), |k| Col(k.exit))); + entry.push(c.control.and_then(|k| k.exit).map_or(Const(F64::ZERO), Col)); entry } @@ -240,7 +242,7 @@ impl ClassTable { if let Some(r) = c.rs2 { accesses.read(Separator::Registers.coordinate(), Col(r.a2), Col(r.v2)); } - // The destination receives the circuit's output, which is the link of a jump that links. + // The destination receives the circuit's output, a jump's its link, `pc + 4`, or a doubleword load's cell. if let Some(rd) = c.rd { accesses.write( Separator::Registers.coordinate(), diff --git a/crates/leanvm_core/src/tables/word.rs b/crates/leanvm_core/src/tables/word.rs index 2f117945c..04c0497df 100644 --- a/crates/leanvm_core/src/tables/word.rs +++ b/crates/leanvm_core/src/tables/word.rs @@ -2,7 +2,7 @@ use super::Clock; use crate::cpu::{Payload, RowRef}; -use crate::rv::{Alu, Div, Ext, Fetched}; +use crate::rv::{Class, Div, Ext, Fetched, InstructionClass, Jump}; /// A circuit port word represented by a virtual table column or a prover hint. #[derive(Clone, Copy, Debug, PartialEq, Eq)] @@ -77,15 +77,25 @@ impl Word { Self::Out => row.out, Self::Dt => at.dt, Self::Pc4 => at.pc4, - Self::Jump => Alu { - flags: entry.flags, - v1: row.v1, - v2: row.v2, - imm: entry.imm, - dt: at.dt, - pc4: at.pc4, - } - .jump(row.taken), + // A branch's offset when it is taken; a jump's, which is always taken. + Self::Jump => match entry.class { + Class::Branch => { + if row.taken { + at.dt + } else { + 0 + } + } + Class::Jump => Jump { + flags: entry.flags, + v1: row.v1, + imm: entry.imm, + dt: at.dt, + pc4: at.pc4, + } + .eval(), + class => panic!("{class:?} has no jump"), + }, Self::Address => row.ram.address, Self::Cell(k) => r.cell(k as usize), Self::CellNew(k) => r.cell_new(k as usize), @@ -146,7 +156,7 @@ mod tests { fn entry() -> Entry { // A decoded instruction supplies metadata independently of the row's values. - Entry::new(Class::Alu.nop().expect("the ALU has a no-op"), Region::TEXT.base()) + Entry::new(Class::Add.nop().expect("ADD has a no-op"), Region::TEXT.base()) } fn at(entry: &Entry, dt: u64) -> Fetched<'_> { @@ -169,11 +179,14 @@ mod tests { for (port, expected) in ports.into_iter().zip(values) { prop_assert_eq!(port.value(RowRef::plain(&row), at(&entry, dt), &[]), expected); } - // The offset and the link are the bytecode's, and a fixed jump adds that offset only when the row takes it. - entry.flags = Alu::ALWAYS; + // The offset and the link are the bytecode's: a branch adds that offset only when the row takes it, and a + // fixed jump always. + entry.class = Class::Branch; prop_assert_eq!(Word::Dt.value(RowRef::plain(&row), at(&entry, dt), &[]), dt); prop_assert_eq!(Word::Pc4.value(RowRef::plain(&row), at(&entry, dt), &[]), Region::TEXT.base() + 4); prop_assert_eq!(Word::Jump.value(RowRef::plain(&row), at(&entry, dt), &[]), if taken { dt } else { 0 }); + (entry.class, entry.flags) = (Class::Jump, 0); + prop_assert_eq!(Word::Jump.value(RowRef::plain(&row), at(&entry, dt), &[]), dt); prop_assert_eq!(Word::Address.value(RowRef::plain(&row), at(&entry, 0), &[]), 16); prop_assert_eq!(Word::Bad.value(RowRef::plain(&row), at(&entry, 0), &[]), 0); } diff --git a/crates/leanvm_core/tests/verifiers/programs.rs b/crates/leanvm_core/tests/verifiers/programs.rs index f020b5735..918ab64f5 100644 --- a/crates/leanvm_core/tests/verifiers/programs.rs +++ b/crates/leanvm_core/tests/verifiers/programs.rs @@ -59,9 +59,9 @@ fn fibonacci_proves_and_verifies() { proves_and_verifies("fibonacci", &program, output); } -/// Every instruction of the `ALU` class at least once: the arithmetic and its 32-bit -/// forms, the comparisons, the logic, the constants, all six branches taken and not, -/// and a call and return. +/// Every instruction of the `ADD`, `LOGIC`, `BRANCH` and `JUMP` classes at least once: the +/// arithmetic and its 32-bit forms, the comparisons, the logic, the constants, all six +/// branches taken and not, and a call and return. #[test] fn alu_instructions_prove_and_verify() { let mut a = Asm::new(); diff --git a/crates/leanvm_core/tests/verifiers/python_verifier.rs b/crates/leanvm_core/tests/verifiers/python_verifier.rs index b82989973..ec82ecbf8 100644 --- a/crates/leanvm_core/tests/verifiers/python_verifier.rs +++ b/crates/leanvm_core/tests/verifiers/python_verifier.rs @@ -4,7 +4,8 @@ use fiat_shamir::transcript::RawProof; use leanvm_core::{ - Alu, Class, Clock, CpuError, EXIT_SLOT, Lookup, PerTable, Program, ProvenRun, Prover, Rate, Region, TableId, + Branch, Class, Clock, CpuError, EXIT_SLOT, Jump, Lookup, PerTable, Program, ProvenRun, Prover, Rate, Region, + TableId, }; use primitives::field::{F64, F192}; use std::path::{Path, PathBuf}; @@ -218,19 +219,28 @@ fn test_python_verifier() { String::from_utf8_lossy(&python.stderr).contains("misnames a register"), "Python refused a table that writes x0 for the wrong reason" ); - // A load reads no `rs2`, a store writes no `rd`, and a doubleword one has no flags: their tables hold those fields - // at constants, `x0`, the sink and zero, so an entry naming another register or a flag is refused. - for (class, slot, reason) in [ - (Class::Load, 5, "reads an rs2"), - (Class::Store, 6, "writes an rd"), - (Class::Ld, 5, "reads an rs2"), - (Class::Sd, 6, "writes an rd"), - (Class::Ld, 3, "flags are not its class's"), + // A load and a jump read no `rs2`, a store and a branch write no `rd`, a branch has no immediate, and a doubleword + // load or store has no flags: their tables hold those fields at constants, `x0`, the sink and zero, so an entry + // naming another register, an immediate or a flag is refused. The other fields are set to the class's legal + // values, so that this is the first rule broken. + // The class tag `g^t`, which is `2^t` since `g = x`. + let tag = |class| 1u64 << TableId::of(class).expect("the class has a table").index(); + for (class, fields, reason) in [ + (Class::Load, vec![(3, 0), (5, 1)], "reads an rs2"), + (Class::Store, vec![(3, 0), (6, 1)], "writes an rd"), + (Class::Ld, vec![(3, 0), (5, 1)], "reads an rs2"), + (Class::Sd, vec![(3, 0), (6, 1)], "writes an rd"), + (Class::Ld, vec![(3, 1)], "flags are not its class's"), + (Class::Jump, vec![(3, Jump::INDIRECT), (9, 0), (5, 1)], "reads an rs2"), + (Class::Branch, vec![(3, Branch::EQ), (7, 0), (6, 1)], "writes an rd"), + ( + Class::Branch, + vec![(3, Branch::EQ), (6, 32), (7, 4)], + "has an immediate", + ), ] { - // The class tag `g^t`, which is `2^t` since `g = x`. - let tag = 1u64 << TableId::of(class).expect("the class has a table").index(); let mut malformed = table.clone(); - for (slot, value) in [(2, tag), (3, 0), (slot, 1)] { + for (slot, value) in std::iter::once((2, tag(class))).chain(fields) { malformed[8 * slot * entries..][..8].copy_from_slice(&value.to_le_bytes()); } std::fs::write(&statement.bytecode, malformed).expect("write malformed register"); @@ -245,33 +255,26 @@ fn test_python_verifier() { let refused = statement.verify(&raw); PythonStatement::assert_rejects(&refused, "an ordinary instruction marked as an exit"); assert!(String::from_utf8_lossy(&refused.stderr).contains("an exit entry is not ECALL")); - // A jump's shape is its flags': only a branch or a `jal` has an offset, and a `jal` links `pc + 4` as a constant - // added to `x0`. Entry 0's fields are set in full, so each case breaks that rule alone. - let alu = 1u64 << TableId::ALU.index(); - let link = Region::TEXT.base() + 4; + // A jump's shape is its class's and its flags': only a branch, a `jal` or the exit has an offset, and a `jal` reads + // nothing, `x0` and no immediate, its link being `pc + 4`. Entry 0's fields are set in full, so each case breaks + // that rule alone. + let (add, jump, branch) = (tag(Class::Add), tag(Class::Jump), tag(Class::Branch)); for (what, fields) in [ ( "an addition with an offset", - [(2, alu), (3, 0), (4, 0), (5, 0), (7, 0), (9, 0x44)], + [(2, add), (3, 0), (4, 0), (5, 0), (7, 0), (9, 0x44)], ), ( "a jal reading a register", - [(2, alu), (3, Alu::ALWAYS), (4, 1), (5, 0), (7, link), (9, 0x44)], + [(2, jump), (3, 0), (4, 1), (5, 0), (7, 0), (9, 0x44)], ), ( - "a jal linking another address", - [(2, alu), (3, Alu::ALWAYS), (4, 0), (5, 0), (7, link + 4), (9, 0x44)], + "a jal with an immediate", + [(2, jump), (3, 0), (4, 0), (5, 0), (7, 4), (9, 0x44)], ), ( "a jalr with an offset", - [ - (2, alu), - (3, Alu::INDIRECT | Alu::ALWAYS), - (4, 0), - (5, 0), - (7, 0), - (9, 0x44), - ], + [(2, jump), (3, Jump::INDIRECT), (4, 0), (5, 0), (7, 0), (9, 0x44)], ), ] { let mut malformed = table.clone(); @@ -298,15 +301,14 @@ data = Path(sys.argv[2]).read_bytes() words = [v['K'](int.from_bytes(data[i:i+8], 'little')) for i in range(0, len(data), 8)] v['check_bytecode'](words) n = len(words) // 16 -for fields in [[(2, {alu}), (3, {always}), (4, 0), (5, 0), (7, {link}), (9, 0)], [(2, {alu}), (3, {branch}), (9, 0x44)], [(2, {alu}), (3, {indirect}), (5, 0), (9, 0)]]: +for fields in [[(2, {jump}), (3, 0), (4, 0), (5, 0), (7, 0), (9, 0)], [(2, {branch}), (3, {eq}), (6, 32), (7, 0), (9, 0x44)], [(2, {jump}), (3, {indirect}), (5, 0), (9, 0)]]: candidate = words.copy() for slot, value in fields: candidate[slot * n] = v['K'](value) v['check_bytecode'](candidate) "#, - always = Alu::ALWAYS, - branch = Alu::SUB | Alu::BR_EQ, - indirect = Alu::INDIRECT | Alu::ALWAYS, + eq = Branch::EQ, + indirect = Jump::INDIRECT, )) .arg(Path::new(env!("CARGO_MANIFEST_DIR")).join("../../python-verifier/verifier.py")) .arg(&statement.bytecode) @@ -369,9 +371,9 @@ fn the_python_verifier_refuses_what_rust_cannot_express() { "an illegal entry is not in its one form", ); } - // A halt slot tagged as an ALU entry is otherwise a well-formed `addi` to the sink. - let alu = 1u64 << TableId::ALU.index(); - write(2, entries - 1, alu); + // A halt slot tagged as an ADD entry is otherwise a well-formed `addi` to the sink. + let add = 1u64 << TableId::ADD.index(); + write(2, entries - 1, add); refuses("a readable halt slot", "the halt slot is not an illegal entry"); std::fs::write(&statement.bytecode, table).expect("restore bytecode"); diff --git a/doc/leanvm/body/04-committing-the-witness.tex b/doc/leanvm/body/04-committing-the-witness.tex index 63684b2e9..4ea5bf4f6 100644 --- a/doc/leanvm/body/04-committing-the-witness.tex +++ b/doc/leanvm/body/04-committing-the-witness.tex @@ -29,6 +29,6 @@ \subsection{Multilinear stacking}\label{sec:stacking} \subsection{Committing to booleans via Ring-Switching}\label{sec:ringswitch} -Flock's argument for an instruction class (\S\ref{sec:tab-class}) requires a commitment to a Boolean multilinear in $\nflock+\kskip$ variables. Ring switching~\cite{DP24} lets the prover pack its low $\kskip=6$ coordinates into the $\K$-valued multilinear $\qflock$ in $\nflock$ variables (Annex~\ref{annex:rs}), which occupies one region of the stack in \S\ref{sec:stacking}, one per circuit: a clock's per table (\S\ref{sec:clock}), and a class's per table but \texttt{EXT}'s, which has none (\S\ref{sec:tab-classes}). The bytecode's multiplicity column is bit-packed the same way, its bit slices being the producer's one-bit columns (\S\ref{sec:lookup}), and is one more ring-switched region. So is each register word, whose bit slices are the register numbers of the tables of one height (\S\ref{sec:regpack}): one more per word, at most eleven. +Flock's argument for an instruction class (\S\ref{sec:tab-class}) requires a commitment to a Boolean multilinear in $\nflock+\kskip$ variables. Ring switching~\cite{DP24} lets the prover pack its low $\kskip=6$ coordinates into the $\K$-valued multilinear $\qflock$ in $\nflock$ variables (Annex~\ref{annex:rs}), which occupies one region of the stack in \S\ref{sec:stacking}, one per circuit: a clock's per table (\S\ref{sec:clock}), and a class's per table but \texttt{EXT}'s, which has none (\S\ref{sec:tab-classes}). The bytecode's multiplicity column is bit-packed the same way, its bit slices being the producer's one-bit columns (\S\ref{sec:lookup}), and is one more ring-switched region. So is each register word, whose bit slices are the register numbers of the tables of one height (\S\ref{sec:regpack}): one more per word, at most fourteen. The opening ring-switches these claims as one family (\S\ref{rs:family}): a challenge $\rsgamma$ gives claim $j$ the scale $\rsgamma^{\,j}$, the family's $64$ slices are the claims' slices so weighted, and the map $\Phi$, drawn after them, makes one target $\sum_ix^i\Phi(\sfam{i})$ and one weight, which puts $\Phi\bigl(\rsgamma^{\,j}\eq(r_j,\cdot)\bigr)$ on claim $j$'s region. The claims' points need not be related. diff --git a/doc/leanvm/body/06-bus-interactions.tex b/doc/leanvm/body/06-bus-interactions.tex index 1352888c8..145de0a15 100644 --- a/doc/leanvm/body/06-bus-interactions.tex +++ b/doc/leanvm/body/06-bus-interactions.tex @@ -162,8 +162,9 @@ \subsection{Bytecode}\label{sec:bytecode} The bytecode is a lookup array (\S\ref{sec:lookup}) of $\nprog = 2^{\kbc}$ entries, entry $i$ at the address $\intk{\tbase+4i}$, the byte address of the instruction. Bus interaction uses domain separation $\sep=\dsep{BC} = \gen^{2}$. The program is public, and so is its decoding: an entry is not the instruction word but the fields a row needs of it, decoded once by both parties (\S\ref{sec:e2e-bc}). So $\ncomp=10$: the class tag, the flags, the three register numbers, the immediate, the successor $\intk{\tbase+4i+4}$, which every row pushes as its next $\pc$ unless it jumps, the jump offset of a branch, a \texttt{jal} or an \texttt{ecall}, a zero in slot $10$, where the row of a division puts its verdict (\S\ref{sec:tables}), and the exit selector. With the separator and the address ahead of them, this is the widest entry on the bus at $12$ coordinates, which is what forces the four index bits, hence the $m=16$ slots of \S\ref{sec:m3}. Its producer's multiplicity column $\mlt$ has height $2^{\kbc}$, entry $i$'s word counting the rows at $\pc=\intk{\tbase+4i}$. A jump's target needs no check of its own: the row it leads to reads the bytecode there, and Corollary~\ref{cor:addrrange} makes it an instruction. A row's three register numbers are not committed as words: they are bit fields of a committed word, one per row for the tables of one height, read through its bit slices as $\mlt$'s are (\S\ref{sec:regpack}). Coordinate $2$ is the tag, naming the instruction's class and its table: \begin{gather*} - \opc{ALU}=\gen^{0},\quad \opc{LOAD}=\gen^{1},\quad \opc{STORE}=\gen^{2},\quad \opc{LD}=\gen^{3},\quad \opc{SD}=\gen^{4},\quad \opc{SHIFT}=\gen^{5},\\ - \opc{MUL}=\gen^{6},\quad \opc{MULH}=\gen^{7},\quad \opc{DIV}=\gen^{8},\quad \opc{HASH}=\gen^{9},\quad \opc{EXT}=\gen^{10}. + \opc{ADD}=\gen^{0},\quad \opc{LOGIC}=\gen^{1},\quad \opc{BRANCH}=\gen^{2},\quad \opc{JUMP}=\gen^{3},\quad \opc{LOAD}=\gen^{4},\\ + \opc{STORE}=\gen^{5},\quad \opc{LD}=\gen^{6},\quad \opc{SD}=\gen^{7},\quad \opc{SHIFT}=\gen^{8},\quad \opc{MUL}=\gen^{9},\\ + \opc{MULH}=\gen^{10},\quad \opc{DIV}=\gen^{11},\quad \opc{HASH}=\gen^{12},\quad \opc{EXT}=\gen^{13}. \end{gather*} A slot of the text that holds no instruction the machine defines has the tag $0$, which is no table's: a run reaching it has no proof. diff --git a/doc/leanvm/body/07-instruction-tables.tex b/doc/leanvm/body/07-instruction-tables.tex index 93fa34103..a44ef0e3f 100644 --- a/doc/leanvm/body/07-instruction-tables.tex +++ b/doc/leanvm/body/07-instruction-tables.tex @@ -1,7 +1,7 @@ % !TeX root = ../drafts/07-instruction-tables.tex \section{The instruction tables}\label{sec:tables} -The instructions are grouped into eleven \emph{classes}, and each class has its own table (\S\ref{sec:bytecode}). All eleven tables are the same table: a row does the plumbing that every instruction needs, the state step, the bytecode read, the register accesses and the memory accesses, and what the class computes is a Boolean circuit proven by Flock (Annex~\ref{annex:flock}), one instance per row, whose words the row puts on the bus. The exception is \texttt{EXT}, the extension-field product, which is of degree two over $\K$: its table has no class circuit and states the product as identities instead. A second circuit per table, its clock circuit (\S\ref{sec:clock}), orders the row's accesses in time. The tables differ in which words their circuit has, where the class sends control, and how it touches memory. Every tuple a table with a class circuit flushes is linear in its columns, so that table settles at the bus's point, all but its register numbers, which the table sumcheck folds (\S\ref{sec:leafstack}, \S\ref{sec:regpack}). +The instructions are grouped into fourteen \emph{classes}, and each class has its own table (\S\ref{sec:bytecode}). All fourteen tables are the same table: a row does the plumbing that every instruction needs, the state step, the bytecode read, the register accesses and the memory accesses, and what the class computes is a Boolean circuit proven by Flock (Annex~\ref{annex:flock}), one instance per row, whose words the row puts on the bus. The exception is \texttt{EXT}, the extension-field product, which is of degree two over $\K$: its table has no class circuit and states the product as identities instead. A second circuit per table, its clock circuit (\S\ref{sec:clock}), orders the row's accesses in time. The tables differ in which words their circuit has, where the class sends control, and how it touches memory. Every tuple a table with a class circuit flushes is linear in its columns, so that table settles at the bus's point, all but its register numbers, which the table sumcheck folds (\S\ref{sec:leafstack}, \S\ref{sec:regpack}). A read of a lookup array (\S\ref{sec:lookup}) is the single flush \pull\ $\tup{\sep,\addr,\val_0,\val_1,\dots}$; the array's producer pushes the entry back as often as it is read. @@ -15,20 +15,20 @@ \subsection{The class table}\label{sec:tab-class} \paragraph{The circuit's words.} A class's circuit (\S\ref{flock:classes}) reads and writes whole $64$-bit words, its \emph{ports}: the register values $v_1,v_2$, the bytecode's flags and immediate, the result, a memory cell, and so on, as the class needs. Flock packs the circuit's witness $64$ bits to a $\K$-element, so a port IS one word of the class's packed witness $\qcls{j}$, committed once (\S\ref{sec:e2e-unrolled}). The table commits none of these words again: they are \emph{virtual} columns, and a claim the bus raises on one of them at a row is routed to the same word of that row's instance in $\qcls{j}$ (\S\ref{sec:stacking}). Putting a port in a bus tuple is therefore what binds the circuit to the machine: the value it reads from a register is what the register tuple carries, the flags it decodes on are what the bytecode tuple carries, the result it computes is what the register write pushes. No constraint ties the two, because they are one committed value. -\paragraph{Columns.} The state $\pc$ and the clock $\ts$, a port of the clock circuit; the bytecode entry's register number $a_1$ and successor $\pc^{+}$, $a_1$ like $a_2$ and $a_d$ below a field of the row's register word rather than a column of its own (\S\ref{sec:regpack}); the value read, $v_1$, a port; the flags, a port, for a class that has them; then, for a class that reads a second register, $a_2$ and the port $v_2$; for a class that writes a register, $a_d$, the old value $v_d^{\mathrm{old}}$ and the result $\mathit{out}$ (a port); for the class with control flow, the bytecode's jump offset $\Delta$, a port, the circuit's jump $\mathit{jump}$, a port, and the bytecode's exit selector $\exitflag$, the successor $\pc^{+}$ being a port of its circuit too; the immediate $\mathit{imm}$ (a port) if the circuit takes one; the memory words below; each access's previous timestamp $\tsprev_k$ and the clock circuit's $\mathit{step}$, ports of the clock circuit. A word is $64$ bits and a register holds one, so every port that reaches a tuple is a $\K$-element as it stands. The same holds of the clock circuit's ports, packed in $\qclk{j}$: the clock, the accesses' previous timestamps and the step are virtual columns too. +\paragraph{Columns.} The state $\pc$ and the clock $\ts$, a port of the clock circuit; the bytecode entry's register number $a_1$ and successor $\pc^{+}$, $a_1$ like $a_2$ and $a_d$ below a field of the row's register word rather than a column of its own (\S\ref{sec:regpack}); the value read, $v_1$, a port; the flags, a port, for a class that has them; then, for a class that reads a second register, $a_2$ and the port $v_2$; for a class that writes a register, $a_d$, the old value $v_d^{\mathrm{old}}$ and the result $\mathit{out}$ (a port), but for \texttt{JUMP}, whose register receives $\pc^{+}$; for a class with control flow, \texttt{BRANCH} or \texttt{JUMP}, the bytecode's jump offset $\Delta$, a port, and the circuit's jump $\mathit{jump}$, a port, then for \texttt{JUMP} the bytecode's exit selector $\exitflag$, the successor $\pc^{+}$ being a port of its circuit too; the immediate $\mathit{imm}$ (a port) if the circuit takes one; the memory words below; each access's previous timestamp $\tsprev_k$ and the clock circuit's $\mathit{step}$, ports of the clock circuit. A word is $64$ bits and a register holds one, so every port that reaches a tuple is a $\K$-element as it stands. The same holds of the clock circuit's ports, packed in $\qclk{j}$: the clock, the accesses' previous timestamps and the step are virtual columns too. \paragraph{Flushes.} \begin{itemize} - \item \textbf{State:} \pull\ $\tup{\dsep{ST},\pc,\ts,0}$, \push\ $\tup{\dsep{ST},\pc',\ts+\mathit{step},\exitflag}$, where the next $\pc$ is the class's (below), $\pc'=\pc^{+}$ unless said otherwise, and $\exitflag=0$ for a class with no control flow. - \item \textbf{Bytecode:} \pull\ $\tup{\dsep{BC},\pc,\opc{j},\mathit{flags},a_1,a_2,a_d,\mathit{imm},\pc^{+},\Delta,0,\exitflag}$, a constant in place of a column the row has not: $0$ for $\mathit{flags}$, $0$ for $a_2$, $\intk{\sink}$ for $a_d$, $0$ for $\mathit{imm}$, and $0$ for $\Delta$ and $\exitflag$ outside the class with control flow, which the entry then has to hold (\S\ref{sec:e2e-bc}). - \item \textbf{Registers:} $\acc{0}\tup{\dsep{REG},a_1;\,v_1}$, then $\acc{1}\tup{\dsep{REG},a_2;\,v_2}$ for a class that reads a second register, and $\acc{3}\tup{\dsep{REG},a_d;\,v_d^{\mathrm{old}}\to v_d}$ for a class that writes one, with $v_d=\mathit{out}$ unless said otherwise. A class makes a register access exactly when its circuit has the word, a second read when it takes $v_2$ and a write when it gives $\mathit{out}$, or when it moves the word between the register and its cell (\texttt{LD}, \texttt{SD}). The other accesses would prove nothing, a read of $\regs[0]$ or a write of the sink, and a row that skips one leaves its slot unused. + \item \textbf{State:} \pull\ $\tup{\dsep{ST},\pc,\ts,0}$, \push\ $\tup{\dsep{ST},\pc',\ts+\mathit{step},\exitflag}$, where the next $\pc$ is the class's (below), $\pc'=\pc^{+}$ unless said otherwise, and $\exitflag=0$ for every class but \texttt{JUMP}. + \item \textbf{Bytecode:} \pull\ $\tup{\dsep{BC},\pc,\opc{j},\mathit{flags},a_1,a_2,a_d,\mathit{imm},\pc^{+},\Delta,0,\exitflag}$, a constant in place of a column the row has not: $0$ for $\mathit{flags}$, $0$ for $a_2$, $\intk{\sink}$ for $a_d$, $0$ for $\mathit{imm}$, $0$ for $\Delta$ outside \texttt{BRANCH} and \texttt{JUMP}, and $0$ for $\exitflag$ outside \texttt{JUMP}, which the entry then has to hold (\S\ref{sec:e2e-bc}). + \item \textbf{Registers:} $\acc{0}\tup{\dsep{REG},a_1;\,v_1}$, then $\acc{1}\tup{\dsep{REG},a_2;\,v_2}$ for a class that reads a second register, and $\acc{3}\tup{\dsep{REG},a_d;\,v_d^{\mathrm{old}}\to v_d}$ for a class that writes one, with $v_d=\mathit{out}$ unless said otherwise. A class makes a register access exactly when its circuit has the word, a second read when it takes $v_2$ and a write when it gives $\mathit{out}$, or when it moves the word between the register and its cell (\texttt{LD}, \texttt{SD}), or links $\pc^{+}$ (\texttt{JUMP}). The other accesses would prove nothing, a read of $\regs[0]$ or a write of the sink, and a row that skips one leaves its slot unused. \item \textbf{Memory:} the class's accesses, in slot $2$ and up. \end{itemize} A padding row (\S\ref{sec:e2e-pad}) is a row of the class's no-op instruction on zero registers, its circuit instance an honest one. \subsection{The register words}\label{sec:regpack} -A row's register numbers, $a_1$, then $a_2$ and $a_d$ for a class that has them, $\nreg$ of them, are fields of its bytecode entry: the bytecode lookup reads them, and the register accesses name the cells they number. A register read is below $2^{5}$; a cell written may be the sink, $32$, below $2^{6}$ (\S\ref{sec:vm}). A word of its own would spend $64$ bits on five or six, so a table's numbers are packed, low first, into $\nregbit{j}$ bits, five per register read and six for a cell written: for an \texttt{ALU} row, +A row's register numbers, $a_1$, then $a_2$ and $a_d$ for a class that has them, $\nreg$ of them, are fields of its bytecode entry: the bytecode lookup reads them, and the register accesses name the cells they number. A register read is below $2^{5}$; a cell written may be the sink, $32$, below $2^{6}$ (\S\ref{sec:vm}). A word of its own would spend $64$ bits on five or six, so a table's numbers are packed, low first, into $\nregbit{j}$ bits, five per register read and six for a cell written: for an \texttt{ADD} row, \[ a_1+x^{5}a_2+x^{10}a_d,\qquad \nregbit{j}=16. \] @@ -49,13 +49,21 @@ \subsection{The register words}\label{sec:regpack} \subsection{The classes}\label{sec:tab-classes} -The instructions of rv64im and the custom ones are decoded into the eleven classes below, an entry's flags selecting one function of its class (\S\ref{sec:e2e-bc}); \texttt{lui}, \texttt{auipc} and \texttt{jal}'s link $\pc+4$ are constants added to $\regs[0]$, \texttt{fence} is an addition of zeros, and \texttt{ecall} a jump to the halt slot. The reference for every function is the specification~\cite{riscv}; \S\ref{flock:classes} gives the circuits. +The instructions of rv64im and the custom ones are decoded into the fourteen classes below, an entry's flags selecting one function of its class (\S\ref{sec:e2e-bc}); \texttt{lui} and \texttt{auipc} are constants added to $\regs[0]$, \texttt{fence} is an addition of zeros, and \texttt{ecall} a jump to the halt slot. Integer arithmetic, bitwise logic, branches and jumps are four classes, \texttt{ADD}, \texttt{LOGIC}, \texttt{BRANCH} and \texttt{JUMP}, so that a row pays only for the circuit its instruction needs. The reference for every function is the specification~\cite{riscv}; \S\ref{flock:classes} gives the circuits. -\paragraph{\texttt{ALU}} (arithmetic, comparisons, bitwise logic, branches and jumps). Ports $v_1,v_2,\mathit{imm},\mathit{flags},\Delta,\pc^{+}\to\mathit{out},\mathit{jump}$. The second operand is $v_2\oplus\mathit{imm}$, the decoder making one of the two zero. The bytecode's $\Delta$ is the fixed target XOR $\pc^{+}$, so that $\pc^{+}+\Delta$ is the target, and $0$ for an entry with none. With $b\in\{0,1\}$ whether the jump is taken, a wire of the circuit, the circuit gives $\mathit{jump}=b\,\Delta$, bit by bit. This is the one class with control flow, and its successor is linear in the row's columns: +\paragraph{\texttt{ADD}} (\texttt{add}, \texttt{sub}, \texttt{addw}, \texttt{subw}, \texttt{addi}, \texttt{addiw}, \texttt{slt}, \texttt{sltu}, \texttt{slti}, \texttt{sltiu}, \texttt{lui}, \texttt{auipc}, \texttt{fence}). Ports $v_1,v_2,\mathit{imm},\mathit{flags}\to\mathit{out}$. The second operand is $v_2\oplus\mathit{imm}$, the decoder making one of the two zero. The circuit adds it to $v_1$, or subtracts it for a subtraction or a comparison, sign-extends the low half of the result for a word form, and for a comparison outputs the one bit it gives in place of the sum. + +\paragraph{\texttt{LOGIC}} (\texttt{and}, \texttt{or}, \texttt{xor}, \texttt{andi}, \texttt{ori}, \texttt{xori}). Ports $v_1,v_2,\mathit{imm},\mathit{flags}\to\mathit{out}$: the function the flags select of $v_1$ and $v_2\oplus\mathit{imm}$, bit by bit. + +\paragraph{Control flow.} \texttt{BRANCH} and \texttt{JUMP} are the classes with control flow. The bytecode's $\Delta$ is the fixed target XOR $\pc^{+}$, so that $\pc^{+}+\Delta$ is the target, and $0$ for an entry with none. Each circuit gives a word $\mathit{jump}$, and the successor is linear in the row's columns: \[ - \pc'=\pc^{+}+\mathit{jump},\qquad v_d=\mathit{out}. + \pc'=\pc^{+}+\mathit{jump}. \] -A \texttt{jal} links $\pc^{+}$ as its immediate added to $\regs[0]$, so $\mathit{out}$ is the link; a branch writes the sink. A \texttt{jalr} is the flag $\mathit{indirect}$, set with the one that makes $b=1$, and has $\Delta=0$: with $s=v_1+\mathit{imm}$ the sum, its circuit outputs $\mathit{out}=\pc^{+}$, the link, and adds $s\oplus\pc^{+}$ to $\Delta$ but for bit $0$, so that $\pc'$ is $s$ with bit $0$ cleared, $\pc^{+}$ having none. A target that is no instruction's address, misaligned or outside the text, names no entry, so the next row reads none. +A target that is no instruction's address, misaligned or outside the text, names no entry, so the next row reads none. + +\paragraph{\texttt{BRANCH}} (\texttt{beq}, \texttt{bne}, \texttt{blt}, \texttt{bge}, \texttt{bltu}, \texttt{bgeu}). Ports $v_1,v_2,\mathit{flags},\Delta\to\mathit{jump}$. With $b\in\{0,1\}$ whether $v_1$ and $v_2$ meet the condition the flags select, a wire of the circuit, the circuit gives $\mathit{jump}=b\,\Delta$, bit by bit, so that a branch not taken falls through to $\pc^{+}$. A branch writes no register and has no immediate, so it has no $a_d,v_d^{\mathrm{old}},\mathit{out},\mathit{imm}$ columns and reads $\intk{\sink}$ and $0$ off the entry; it never exits, and reads $0$ off the entry for its exit selector too. + +\paragraph{\texttt{JUMP}} (\texttt{jal}, \texttt{jalr}, \texttt{ecall}). Ports $v_1,\mathit{imm},\mathit{flags},\Delta,\pc^{+}\to\mathit{jump}$. Every jump is taken. A jump reads one register, so it has no $a_2,v_2$ columns and reads $0$ off the entry. It links: $\regs[a_d]$ receives $\pc^{+}$ itself, the row's successor column, so the table has no $\mathit{out}$ column and $v_d=\pc^{+}$. Its exit selector $\exitflag$ is a column. A \texttt{jal} has flags $0$, reads $\regs[0]$ and has immediate $0$, its link being the row's $\pc^{+}$ rather than a constant, and its circuit gives $\mathit{jump}=\Delta$. A \texttt{jalr} is the flag $\mathit{indirect}$ and has $\Delta=0$: with $s=v_1+\mathit{imm}$ the sum, its circuit adds $s\oplus\pc^{+}$ to $\Delta$ but for bit $0$, so that $\pc'$ is $s$ with bit $0$ cleared, $\pc^{+}$ having none. \texttt{ecall} is a jump of flags $0$ to the halt slot that writes the sink and has $\exitflag=1$. \paragraph{\texttt{LOAD}} (\texttt{lb}, \texttt{lbu}, \texttt{lh}, \texttt{lhu}, \texttt{lw}, \texttt{lwu}). Ports $v_1,\mathit{imm},\mathit{flags},\mathit{cell}\to\mathit{address},\mathit{out}$: the circuit adds the address, extracts the bytes the width and the offset select from the cell and extends them, and hands the bus the word's address with the misalignment bits in it (\S\ref{sec:exp}). A load reads one register, so it has no $a_2,v_2$ columns and reads $0$ off the entry. One access, $\acc{2}\tup{\dsep{MEM},\mathit{address};\,\mathit{cell}}$. @@ -102,4 +110,4 @@ \subsection{The classes}\label{sec:tab-classes} A padding row multiplies zeros at the address $0$. It writes $0$ over $0$, so each of its accesses pulls the tuple it pushes, and its identities hold. -\paragraph{Sizes.} A circuit's instance occupies $2^{\kblock}$ bits: $8$ for \texttt{LD} and \texttt{SD}, $10$ for \texttt{ALU}, \texttt{LOAD}, \texttt{STORE} and \texttt{SHIFT}, $12$ for \texttt{MUL}, $13$ for \texttt{MULH} and \texttt{DIV}, and $14$ for \texttt{HASH}, \texttt{EXT} having none; $9$ for the clock circuit of a row with three accesses, every class's but \texttt{HASH}'s and \texttt{EXT}'s, $11$ for \texttt{HASH}'s eighteen, and $12$ for \texttt{EXT}'s twelve, which also computes the limbs' addresses (\S\ref{flock:classes}). Flock proves a batch of at least $2^{13}$ bits and at least eight instances, so a table has at least $2^{3}$ rows, and at least $2^{13-\kblock}$ for the smallest of its circuits: $2^{5}$ for \texttt{LD} and \texttt{SD}, $2^{3}$ for \texttt{HASH} and \texttt{EXT}, and $2^{4}$ for the others. Padding rows (\S\ref{sec:e2e-pad}) supply them. +\paragraph{Sizes.} A circuit's instance occupies $2^{\kblock}$ bits: $8$ for \texttt{LD} and \texttt{SD}, $9$ for \texttt{ADD}, \texttt{LOGIC}, \texttt{BRANCH} and \texttt{JUMP}, $10$ for \texttt{LOAD}, \texttt{STORE} and \texttt{SHIFT}, $12$ for \texttt{MUL}, $13$ for \texttt{MULH} and \texttt{DIV}, and $14$ for \texttt{HASH}, \texttt{EXT} having none; $9$ for the clock circuit of a row with three accesses, every class's but \texttt{BRANCH}'s, \texttt{JUMP}'s, \texttt{HASH}'s and \texttt{EXT}'s, and for that of a row with two, \texttt{BRANCH}'s and \texttt{JUMP}'s, $11$ for \texttt{HASH}'s eighteen, and $12$ for \texttt{EXT}'s twelve, which also computes the limbs' addresses (\S\ref{flock:classes}). Flock proves a batch of at least $2^{13}$ bits and at least eight instances, so a table has at least $2^{3}$ rows, and at least $2^{13-\kblock}$ for the smallest of its circuits: $2^{5}$ for \texttt{LD} and \texttt{SD}, $2^{3}$ for \texttt{HASH} and \texttt{EXT}, and $2^{4}$ for the others. Padding rows (\S\ref{sec:e2e-pad}) supply them. diff --git a/doc/leanvm/body/08-end-to-end-protocol.tex b/doc/leanvm/body/08-end-to-end-protocol.tex index 4d077079a..757a91b40 100644 --- a/doc/leanvm/body/08-end-to-end-protocol.tex +++ b/doc/leanvm/body/08-end-to-end-protocol.tex @@ -5,12 +5,12 @@ \subsection{Bytecode encoding}\label{sec:e2e-bc} The program is public, so nothing is decoded in a table: both parties decode each of the $\nprog=2^{\kbc}$ instruction words once, into the fields the rows read (\S\ref{sec:bytecode}), and encode the result as one $\K$-valued multilinear $P$ in $\kbc+4$ variables: \begin{enumerate}[itemsep=1pt,topsep=3pt] -\item lay instruction $z$ out as $16$ slots of $\K$: the class tag $\opc{j}$ in slot $2$ (\S\ref{sec:bytecode}); the flags in slot $3$, a word of selector bits naming the class's function, the finalization word for \texttt{HASH}, the accumulate and base-field bits for \texttt{EXT}; the register numbers $a_1,a_2,a_d$ in slots $4$ to $6$, $\intk{\sink}=\intk{32}$ for an instruction with no destination or with $\regs[0]$ as one; the immediate in slot $7$, sign-extended, folded with $\pc$ for \texttt{auipc}, and the link $\pc+4$ for \texttt{jal}; the successor $\intk{\tbase+4z+4}$ in slot $8$; the jump offset $\Delta$ in slot $9$, the fixed target of a branch, a \texttt{jal} or an \texttt{ecall} XOR the successor, and $0$ for an entry with none (\S\ref{sec:tab-classes}); the exit selector $\exitflag$ in slot $11$, $1$ only for \texttt{ecall}; and $0$ everywhere else: slot $10$, where a division's row puts its verdict (\S\ref{sec:tab-classes}), and slots $0$, $1$ and $12$ to $15$, which the separator, the address and nothing occupy in the bus tuple. A slot of the text holding no instruction the machine defines, the halt slot included, is all zeros: its tag is no table's. +\item lay instruction $z$ out as $16$ slots of $\K$: the class tag $\opc{j}$ in slot $2$ (\S\ref{sec:bytecode}); the flags in slot $3$, a word of selector bits naming the class's function, the finalization word for \texttt{HASH}, the accumulate and base-field bits for \texttt{EXT}; the register numbers $a_1,a_2,a_d$ in slots $4$ to $6$, $\intk{\sink}=\intk{32}$ for an instruction with no destination or with $\regs[0]$ as one; the immediate in slot $7$, sign-extended, folded with $\pc$ for \texttt{auipc}, and $0$ for \texttt{jal}, whose link is its row's successor; the successor $\intk{\tbase+4z+4}$ in slot $8$; the jump offset $\Delta$ in slot $9$, the fixed target of a branch, a \texttt{jal} or an \texttt{ecall} XOR the successor, and $0$ for an entry with none (\S\ref{sec:tab-classes}); the exit selector $\exitflag$ in slot $11$, $1$ only for \texttt{ecall}; and $0$ everywhere else: slot $10$, where a division's row puts its verdict (\S\ref{sec:tab-classes}), and slots $0$, $1$ and $12$ to $15$, which the separator, the address and nothing occupy in the bus tuple. A slot of the text holding no instruction the machine defines, the halt slot included, is all zeros: its tag is no table's. \item read the resulting $2^{\kbc}\times16$ table as $P$, the low $\kbc$ variables indexing the instruction and the high four its slot, bits low first. \end{enumerate} So $P(z,0,1,0,0)$ is instruction $z$'s tag, $P(z,0,0,1,0)$ its first register, $P(z,0,0,0,1)$ its successor, and $P(z,0,0,0,0)=P(z,1,1,1,1)=0$. -\paragraph{Well-formedness.} The proof system is sound for any table $P$, a malformed one included: it proves that the rows read $P$ and did what its fields say. What makes $P$ a RISC-V program is checked once, by both parties, where a program enters: every entry with a tag reads two registers below $32$ and writes a cell in $1..32$, its successor is its own address plus $4$, its flags are ones its class defines, its exit selector is a bit, $1$ only for the one form of \texttt{ecall}, only a branch, a \texttt{jal} or an \texttt{ecall} has a jump offset, a \texttt{jal} reads $\regs[0]$ twice and has its successor as immediate, a \texttt{LOAD} or \texttt{LD} entry reads $\regs[0]$ as its second register, a \texttt{STORE} or \texttt{SD} entry writes the sink, an \texttt{LD} or \texttt{SD} entry has flags $0$, a \texttt{HASH} entry writes the sink and has immediate $0$, and an \texttt{EXT} entry reads its address from a register, not the sink, and has immediate $0$. The two verifiers check the same rules, and the digest below is of the decoded table, so a verifier is never handed a program it did not check. A table of $\nprog=2^{\kbc}$ slots, the padding and the halt slot included, makes the bus grind $\max(0,\kbc-21)$ bits before its challenges (\S\ref{sec:e2e-ledger}); the text region caps it at $2^{26}$ slots. +\paragraph{Well-formedness.} The proof system is sound for any table $P$, a malformed one included: it proves that the rows read $P$ and did what its fields say. What makes $P$ a RISC-V program is checked once, by both parties, where a program enters: every entry with a tag reads two registers below $32$ and writes a cell in $1..32$, its successor is its own address plus $4$, its flags are ones its class defines, its exit selector is a bit, $1$ only for the one form of \texttt{ecall} (a \texttt{JUMP} entry with flags $0$ that reads $\regs[0]$, writes the sink and has immediate $0$), only a branch, a \texttt{jal} or an \texttt{ecall} has a jump offset, a \texttt{jal} reads $\regs[0]$ and has immediate $0$, a \texttt{LOAD}, \texttt{LD} or \texttt{JUMP} entry reads $\regs[0]$ as its second register, a \texttt{STORE} or \texttt{SD} entry writes the sink, an \texttt{LD} or \texttt{SD} entry has flags $0$, a \texttt{BRANCH} or \texttt{HASH} entry writes the sink and has immediate $0$, and an \texttt{EXT} entry reads its address from a register, not the sink, and has immediate $0$. The two verifiers check the same rules, and the digest below is of the decoded table, so a verifier is never handed a program it did not check. A table of $\nprog=2^{\kbc}$ slots, the padding and the halt slot included, makes the bus grind $\max(0,\kbc-21)$ bits before its challenges (\S\ref{sec:e2e-ledger}); the text region caps it at $2^{26}$ slots. \subsection{The statement}\label{sec:e2e-pi} @@ -24,7 +24,7 @@ \subsection{The statement}\label{sec:e2e-pi} \subsection{Filling the tables}\label{sec:e2e-pad} -A table is proven over a power-of-two number of rows. The prover reaches one with \emph{padding rows}, whose clock is $0$. The text carries, past the program and an illegal word that keeps a run from falling into them, for each table and each of a few sizes, a block of that many no-ops of the table's class followed by a \texttt{jal} back to the block's first instruction, which no program code jumps into. A padding row is a row at one of those instructions. A clock without the live bit does not advance, so the states pushed and pulled around a block cancel among themselves, for any number of traversals: these are the closed walks of Proposition~\ref{prop:walk}, and by Corollary~\ref{cor:clock} they are the only ones. A traversal of the block of size $n$ adds $n$ rows to its table and one to \texttt{ALU}'s, so every table can be brought to its next power of two exactly, \texttt{ALU}, where every closing jump lands, being solved last. +A table is proven over a power-of-two number of rows. The prover reaches one with \emph{padding rows}, whose clock is $0$. The text carries, past the program and an illegal word that keeps a run from falling into them, for each table and each of a few sizes, a block of that many no-ops of the table's class followed by a \texttt{jal} back to the block's first instruction, which no program code jumps into; \texttt{JUMP}'s no-op is a jump to the next instruction, so its block falls through like any other. A padding row is a row at one of those instructions. A clock without the live bit does not advance, so the states pushed and pulled around a block cancel among themselves, for any number of traversals: these are the closed walks of Proposition~\ref{prop:walk}, and by Corollary~\ref{cor:clock} they are the only ones. A traversal of the block of size $n$ adds $n$ rows to its table and one to \texttt{JUMP}'s, so every table can be brought to its next power of two exactly, \texttt{JUMP}, where every closing jump lands, being solved last. The verifier has no notion of a padding row, and needs none: a row is inert exactly when its clock lacks the live bit, and the filler blocks are only how an honest prover comes by such rows. A prover may close such rows around any cycle of the program's own control flow instead, and they are inert all the same, by the same two facts: their state tuples cancel because their clocks do not advance, and their accesses meet nothing of the run because the order check \eqref{eq:order} keeps the live bit off their previous timestamps (Theorem~\ref{thm:rwmem}). The filler blocks earn their place by making the fill exact, not by making it safe. @@ -42,12 +42,12 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled} \paragraph{Setup.} -The Fiat-Shamir state is seeded by the statement (\S\ref{sec:e2e-fiat-shamir}). The prover sends the eleven table log-heights $\tau_j$, the PCS rate and the final clock $\tsfinal\in\K$ (\S\ref{sec:state}); the verifier checks each $\tau_j$ against the cap $2^{32}$ and the batch floors (\S\ref{sec:tables}), and that $\tsfinal$ is a live clock at slot $0$, and derives the layout of every stack (PCS and GKR leaves) and the producer's bit count $\nbit$ (\S\ref{sec:lookup}) from those sizes and the program's. +The Fiat-Shamir state is seeded by the statement (\S\ref{sec:e2e-fiat-shamir}). The prover sends the fourteen table log-heights $\tau_j$, the PCS rate and the final clock $\tsfinal\in\K$ (\S\ref{sec:state}); the verifier checks each $\tau_j$ against the cap $2^{32}$ and the batch floors (\S\ref{sec:tables}), and that $\tsfinal$ is a live clock at slot $0$, and derives the layout of every stack (PCS and GKR leaves) and the producer's bit count $\nbit$ (\S\ref{sec:lookup}) from those sizes and the program's. \paragraph{Commitment.} \begin{enumerate} -\item \textbf{Prover.} Stack (\S\ref{sec:stacking}) every column: the read-write arrays' final columns and timestamps, $\regfin,\memfin,\advfin$ and their $\tsfin$, the advice's initial words $\advinit$ (\S\ref{sec:memchan}), the bytecode's multiplicity column $\mlt$ (\S\ref{sec:lookup}), the twenty-one packed witnesses, $\qcls{j}$ for the ten tables with a class circuit and $\qclk{j}$ for all eleven (\S\ref{sec:tab-class}, \S\ref{sec:clock}), every committed column of the eleven tables, and the register words $\regword{w}$ (\S\ref{sec:regpack}), into $q$, and send its commitment (Annex~\ref{annex:pcs}). +\item \textbf{Prover.} Stack (\S\ref{sec:stacking}) every column: the read-write arrays' final columns and timestamps, $\regfin,\memfin,\advfin$ and their $\tsfin$, the advice's initial words $\advinit$ (\S\ref{sec:memchan}), the bytecode's multiplicity column $\mlt$ (\S\ref{sec:lookup}), the twenty-seven packed witnesses, $\qcls{j}$ for the thirteen tables with a class circuit and $\qclk{j}$ for all fourteen (\S\ref{sec:tab-class}, \S\ref{sec:clock}), every committed column of the fourteen tables, and the register words $\regword{w}$ (\S\ref{sec:regpack}), into $q$, and send its commitment (Annex~\ref{annex:pcs}). \item \textbf{Verifier.} Receives the commitment to $q$. \end{enumerate} @@ -61,7 +61,7 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled} \item \textbf{Prover \& Verifier.} Decompose each leaf claim (\S\ref{sec:leafstack}). The verifier forms every public part itself: the block selectors, the constant entries, the index columns (\S\ref{sec:idxcol}) and RAM's seed column (\S\ref{sec:e2e-pi}). Four blocks per side belong to no table: the state boundary, plus the registers', RAM's and the advice's seed (push side) or finalization (pull side). For their committed columns the prover sends one evaluation each, entering the claim pool: on the push side the advice's initial column alone, on the pull side every final column and timestamp. Every other block belongs to a table or to a producer, and is discharged below. \end{enumerate} -\paragraph{Linear tables.} The ten tables with a class circuit flush only tuples linear in their columns (\S\ref{sec:tables}). +\paragraph{Linear tables.} The thirteen tables with a class circuit flush only tuples linear in their columns (\S\ref{sec:tables}). \begin{enumerate} \item \textbf{Prover.} Sends, table by table, the value of every column of $T_j$ at $\zeta_{<\tau_j}$ but its register numbers, which the table sumcheck folds (\S\ref{sec:regpack}); they enter the claim pool, a port's routed to its packed witness (\S\ref{sec:tab-class}). \item \textbf{Verifier.} Evaluates each such table's form $B^{s}_j$ at those values, its register numbers taken as zero, its share of side $s$ short of the numbers' part, and takes it off what the tables owe (\S\ref{sec:leafstack}). @@ -70,7 +70,7 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled} \paragraph{Table sumcheck.} One run proves what is left of the bus, \texttt{EXT}'s share, the linear tables' register numbers' part and the producer's (\S\ref{sec:air}), and \texttt{EXT}'s three identities, the only constraints a table has (\S\ref{sec:tab-classes}). \begin{enumerate} \item \textbf{Verifier.} Samples and sends the batch challenge $\xi\in\E$. Its first $\nside=2$ powers weight the bus forms, one per side and shared by every table and the producer, and the next three, $\xi^{2}$ to $\xi^{4}$, \texttt{EXT}'s identities, whose sums are zero, so the target is the bus's alone. It draws no point: the batch runs at the bus point, $T_j$ tested at $\zeta_{<\tau_j}$ and a producer of $2^{\kappa}$ entries at $\zeta_{<\kappa}$. -\item \textbf{Prover \& Verifier.} Run the sumcheck over the eleven tables, a linear table's forms restricted to its register numbers, and then the bytecode's producer, $\taumax$ rounds, $\taumax$ the largest of their log heights, each joining at round $\taumax$ minus its own, against the target the verifier derived from the two leaf claims. Its summand has individual degree three and the round check pins one of the four coefficients (\S\ref{sec:prelim}), so a round costs three $\E$-elements. +\item \textbf{Prover \& Verifier.} Run the sumcheck over the fourteen tables, a linear table's forms restricted to its register numbers, and then the bytecode's producer, $\taumax$ rounds, $\taumax$ the largest of their log heights, each joining at round $\taumax$ minus its own, against the target the verifier derived from the two leaf claims. Its summand has individual degree three and the round check pins one of the four coefficients (\S\ref{sec:prelim}), so a round costs three $\E$-elements. \item \textbf{Prover \& Verifier.} The prover sends one value per column of \texttt{EXT} and per register number of a linear table, but for a register number its bits' values (\S\ref{sec:regpack}), and each producer's bit values $\widetilde{\mbit{k}}(\fc_{<\kappa})$, $k<\nbit$; the verifier computes each producer's public columns $\widetilde{\pubp{k}}(\fc_{<\kappa})$ itself (\S\ref{sec:lookup}). It rebuilds each $B^{s}_j$ and \texttt{EXT}'s identities from them and checks that they reproduce the sumcheck's final value; \texttt{EXT}'s column values then enter the claim pool at $\fc_{<\tau_j}$. A circuit's ports are columns of its table but live in $\qcls{j}$ or $\qclk{j}$, so their claims route there (\S\ref{sec:tab-class}); a producer's bits are slices of its multiplicity column, and a table's register numbers' bits slices of the register word that packs them, so their claims go to ring switching (below). \end{enumerate} @@ -83,8 +83,8 @@ \subsection{The unrolled protocol}\label{sec:e2e-unrolled} \paragraph{Flock validity.} \begin{enumerate} -\item \textbf{Prover \& Verifier.} Run Flock's reduction (Annex~\ref{annex:flock}) once over the twenty-one circuits, batched under shared challenges (\S\ref{flock:batch}): every class circuit in table order, over $\qcls{j}$, \texttt{EXT} having none, then every clock circuit in table order, over $\qclk{j}$, each with $2^{\tau_j}$ instances. One zerocheck, its round-one message shared by all twenty-one, and one lincheck leave one evaluation claim on each packed witness, and one claim on each circuit's matrix form, which the verifier settles by one walk of the circuit once the proof is read. -\item \textbf{Verifier.} Sends $\rsgamma\in\E$, drawn after every ring-switched claim is bound. The claims are the twenty-one witnesses', then the bytecode's multiplicity column's, its suffix point being its $\fc_{<\kappa}$ and its $64$ slices the $\nbit$ bit values it sent, then zeros, which are not transmitted (\S\ref{sec:lookup}), then each register word's, its suffix point being its tables' shared $\fc_{<\tau_j}$ and its slices the bit values sent for its tables, in its order, then zeros (\S\ref{sec:regpack}); claim $j$, from zero, takes the scale $\rsgamma^{\,j}$, and both sides form the family's slices $\sfam{i}=\sum_j\rsgamma^{\,j}s_{j,i}$ (\S\ref{rs:family}). The prover sends nothing. +\item \textbf{Prover \& Verifier.} Run Flock's reduction (Annex~\ref{annex:flock}) once over the twenty-seven circuits, batched under shared challenges (\S\ref{flock:batch}): every class circuit in table order, over $\qcls{j}$, \texttt{EXT} having none, then every clock circuit in table order, over $\qclk{j}$, each with $2^{\tau_j}$ instances. One zerocheck, its round-one message shared by all twenty-seven, and one lincheck leave one evaluation claim on each packed witness, and one claim on each circuit's matrix form, which the verifier settles by one walk of the circuit once the proof is read. +\item \textbf{Verifier.} Sends $\rsgamma\in\E$, drawn after every ring-switched claim is bound. The claims are the twenty-seven witnesses', then the bytecode's multiplicity column's, its suffix point being its $\fc_{<\kappa}$ and its $64$ slices the $\nbit$ bit values it sent, then zeros, which are not transmitted (\S\ref{sec:lookup}), then each register word's, its suffix point being its tables' shared $\fc_{<\tau_j}$ and its slices the bit values sent for its tables, in its order, then zeros (\S\ref{sec:regpack}); claim $j$, from zero, takes the scale $\rsgamma^{\,j}$, and both sides form the family's slices $\sfam{i}=\sum_j\rsgamma^{\,j}s_{j,i}$ (\S\ref{rs:family}). The prover sends nothing. \item \textbf{Prover \& Verifier.} The ring switching of \S\ref{sec:ringswitch}, its map drawn after $\rsgamma$, reduces the family to one weighted-sum claim on the stack, target $\sum_ix^i\Phi(\sfam{i})$, with an MLE-friendly $\E$-valued weight (Definition~\ref{def:ipcs}) supported on the ring-switched regions, claim $j$'s being $\Phi\bigl(\rsgamma^{\,j}\eq(r_j,\cdot)\bigr)$; it joins the pool, ahead of every column claim. The circuits of one block size leave points that are prefixes of one another, so the verifier evaluates their weights in one pass (\S\ref{rs:weight}). \end{enumerate} diff --git a/doc/leanvm/body/c-flock-protocol.tex b/doc/leanvm/body/c-flock-protocol.tex index 4ced568ba..53f194508 100644 --- a/doc/leanvm/body/c-flock-protocol.tex +++ b/doc/leanvm/body/c-flock-protocol.tex @@ -1,7 +1,7 @@ % !TeX root = ../drafts/c-flock-protocol.tex \section{The Flock protocol}\label{annex:flock} -Flock~\cite{Flock26} proves many executions of one Boolean circuit at once. We use it for the instruction classes' circuits, ten of them, \texttt{EXT} having none, and the eleven tables' clock circuits (\S\ref{sec:tables}, \S\ref{sec:clock}, \S\ref{flock:classes}), each over its own witness, all twenty-one in one batched run of the protocol. Since we do not follow their protocol exactly, we describe our version here, first for one circuit of block size $\kblock$ with its constant wire at position $\jconst$, then how one run proves the twenty-one at once (\S\ref{flock:batch}); the twenty-one differ in those two numbers and their batch sizes alone, which \S\ref{flock:classes} gives, and the BLAKE2s compression, the largest at $\kblock=14$, is the running example. +Flock~\cite{Flock26} proves many executions of one Boolean circuit at once. We use it for the instruction classes' circuits, thirteen of them, \texttt{EXT} having none, and the fourteen tables' clock circuits (\S\ref{sec:tables}, \S\ref{sec:clock}, \S\ref{flock:classes}), each over its own witness, all twenty-seven in one batched run of the protocol. Since we do not follow their protocol exactly, we describe our version here, first for one circuit of block size $\kblock$ with its constant wire at position $\jconst$, then how one run proves the twenty-seven at once (\S\ref{flock:batch}); the twenty-seven differ in those two numbers and their batch sizes alone, which \S\ref{flock:classes} gives, and the BLAKE2s compression, the largest at $\kblock=14$, is the running example. \subsection{Statement and commitment}\label{flock:statement} @@ -172,7 +172,7 @@ \subsection{Protocol summary}\label{flock:summary} \subsection{Batching the circuits}\label{flock:batch} -One run of the protocol proves the twenty-one circuits. Index them by $f$, the class circuits in table order and then the clock circuits, from $f=0$, and write $\kblockf{f}$, $\kbatchf{f}$, $z_f$ and $\nflockf{f}=\kblockf{f}+\kbatchf{f}-\kskip$ for circuit $f$'s block size, batch size, witness and zerocheck rounds; its packed witness is the $\qcls{j}$ or $\qclk{j}$ of its table. The circuits share every challenge, and the batch adds one, $\zcbatch$, for the zerocheck; lincheck's $\lcalpha$ batches the circuits as well. Both sumchecks are front-loaded, as the table sumcheck is (\S\ref{sec:air}): round $j$ binds the same variable of every circuit still taking part, every circuit takes part from the first round, and a circuit is done after as many rounds as it has variables. +One run of the protocol proves the twenty-seven circuits. Index them by $f$, the class circuits in table order and then the clock circuits, from $f=0$, and write $\kblockf{f}$, $\kbatchf{f}$, $z_f$ and $\nflockf{f}=\kblockf{f}+\kbatchf{f}-\kskip$ for circuit $f$'s block size, batch size, witness and zerocheck rounds; its packed witness is the $\qcls{j}$ or $\qclk{j}$ of its table. The circuits share every challenge, and the batch adds one, $\zcbatch$, for the zerocheck; lincheck's $\lcalpha$ batches the circuits as well. Both sumchecks are front-loaded, as the table sumcheck is (\S\ref{sec:air}): round $j$ binds the same variable of every circuit still taking part, every circuit takes part from the first round, and a circuit is done after as many rounds as it has variables. \paragraph{Zerocheck.} Let $\nflockmax=\max_f\nflockf{f}$. The verifier forms one point $r\in\E^{\nflockmax}$, the seven fixed coordinates of \S\ref{flock:zerocheck} and then $\nflockmax-7$ sampled ones, circuit $f$ taking its first $\nflockf{f}$ coordinates; then it samples $\zcbatch$. Writing $P_f$ for \eqref{flock:eq:pskip} of circuit $f$ at $r_{<\nflockf{f}}$ and $G_f=\qext a_f\qext b_f+\qext c_f$ for its summand, the batch is \[ @@ -190,7 +190,7 @@ \subsection{Batching the circuits}\label{flock:batch} \end{equation} $\lcterm{f}$ the other two terms of the right side of \eqref{flock:eq:lincheck-terminal} for circuit $f$, its $\lcalpha^2$ and $\lcalpha^3$ ones, which need no circuit: the $\lcalpha^2$ term is $\eq(\fc_{\mathrm{in},f},\fc'_{\mathrm{in},f})\sum_i\lag_i(\zskip)s_{f,i}$, and the $\lcalpha^3$ term is the constant wire's slice times the equality weight of its index. Each $\lcmat{f}$ is left as circuit $f$'s deferred claim, that its matrix form at these challenges takes that value; the verifier settles it with one walk of the circuit (\S\ref{flock:native}), after the rest of the proof, and a recursive verifier carries it out of the proof instead (Annex~\ref{annex:rec}). Nothing is drawn after the forms' challenges, so settling them later is the same check. -\paragraph{What it leaves.} One family per witness, as for one circuit: $s_{f,i}\qeq\mle{z_f}(i,\fc'_{\mathrm{in},f},\fc_{\mathrm{out},f})$ for $i<64$, for ring switching (\S\ref{flock:ringswitch}), and one matrix claim per circuit. Two circuits of one block size share $\fc'_{\mathrm{in},f}$ and the first coordinates of $\fc$, so the shorter one's point is a prefix of the longer one's, and the verifier evaluates their weights in one pass (\S\ref{rs:weight}). The twenty-one make seven such groups, one per block size of \S\ref{flock:classes}: the nine clock circuits of $\kblock=9$, the four class circuits of $\kblock=10$, two each for $\kblock=8$, $\kblock=12$ and $\kblock=13$, and one each for $\kblock=11$ and $\kblock=14$. The matrix claims of one block size share their row point $(\zskip,\fc_{\mathrm{in},f})$ and their column point $\fc'_{\mathrm{in},f}$ too. +\paragraph{What it leaves.} One family per witness, as for one circuit: $s_{f,i}\qeq\mle{z_f}(i,\fc'_{\mathrm{in},f},\fc_{\mathrm{out},f})$ for $i<64$, for ring switching (\S\ref{flock:ringswitch}), and one matrix claim per circuit. Two circuits of one block size share $\fc'_{\mathrm{in},f}$ and the first coordinates of $\fc$, so the shorter one's point is a prefix of the longer one's, and the verifier evaluates their weights in one pass (\S\ref{rs:weight}). The twenty-seven make seven such groups, one per block size of \S\ref{flock:classes}: sixteen of $\kblock=9$, the twelve clock circuits of that size and the class circuits of \texttt{ADD}, \texttt{LOGIC}, \texttt{BRANCH} and \texttt{JUMP}, the three class circuits of $\kblock=10$, \texttt{LOAD}'s, \texttt{STORE}'s and \texttt{SHIFT}'s, two each for $\kblock=8$, $\kblock=12$ and $\kblock=13$, and one each for $\kblock=11$ and $\kblock=14$. The matrix claims of one block size share their row point $(\zskip,\fc_{\mathrm{in},f})$ and their column point $\fc'_{\mathrm{in},f}$ too. \subsection{Evaluating the matrices}\label{flock:matrices} @@ -274,13 +274,16 @@ \subsubsection{Transpose algorithm}\label{flock:backward} \subsection{The class circuits}\label{flock:classes} -Each instruction class's circuit (\S\ref{sec:tables}) and each table's clock circuit (\S\ref{sec:clock}) is a circuit in the sense of Definition~\ref{def:circuit}, built from a small vocabulary of gates over $64$-bit words: XOR, AND, the multiplexer $s\,(x\oplus y)\oplus y$, the ripple-carry adder, the incrementer and the carry-save multiplier below. One block layout serves all twenty-one: the ports first, $64$ positions per word, the inputs then the outputs, bit $i$ of a word at position $i$ of its range; the constant wire at $\jconst$, the position right after them; then the $\wedge$ wires in the order the circuit makes them. A port's bits are free wires when it is an input, and committed wires when it is an output, so that the result leaves the circuit: an $\oplus$ wire committed by a copy, or an $\wedge$ wire committed at the port's position rather than after $\jconst$, which saves the copy. A port bit with no wire, such as the $63$ high bits of a one-bit output, the $23$ high bits of a timestamp or the $5$ low bits of a row's clock, is an empty position, which \eqref{flock:eq:r1cs} forces to zero. Each port is therefore one packed $\K$-element, equal to the register, bytecode or memory word it stands for (\S\ref{sec:tab-class}). A hint (\texttt{DIV}'s quotient and remainder) is an input port that no tuple carries. +Each instruction class's circuit (\S\ref{sec:tables}) and each table's clock circuit (\S\ref{sec:clock}) is a circuit in the sense of Definition~\ref{def:circuit}, built from a small vocabulary of gates over $64$-bit words: XOR, AND, the multiplexer $s\,(x\oplus y)\oplus y$, the ripple-carry adder, the incrementer and the carry-save multiplier below. One block layout serves all twenty-seven: the ports first, $64$ positions per word, the inputs then the outputs, bit $i$ of a word at position $i$ of its range; the constant wire at $\jconst$, the position right after them; then the $\wedge$ wires in the order the circuit makes them. A port's bits are free wires when it is an input, and committed wires when it is an output, so that the result leaves the circuit: an $\oplus$ wire committed by a copy, or an $\wedge$ wire committed at the port's position rather than after $\jconst$, which saves the copy. A port bit with no wire, such as the $63$ high bits of a one-bit output, the $23$ high bits of a timestamp or the $5$ low bits of a row's clock, is an empty position, which \eqref{flock:eq:r1cs} forces to zero. Each port is therefore one packed $\K$-element, equal to the register, bytecode or memory word it stands for (\S\ref{sec:tab-class}). A hint (\texttt{DIV}'s quotient and remainder) is an input port that no tuple carries. \begin{center} \begin{tabular}{lrrrrr} \hline Circuit & ports (in $\to$ out) & $\kblock$ & $\jconst$ & $\wedge$ wires & positions used\\ \hline -\texttt{ALU} & $6\to2$ & $10$ & $512$ & $551$ & $1{,}000$\\ +\texttt{ADD} & $4\to1$ & $9$ & $320$ & $162$ & $483$\\ +\texttt{LOGIC} & $4\to1$ & $9$ & $320$ & $128$ & $449$\\ +\texttt{BRANCH} & $4\to1$ & $9$ & $320$ & $197$ & $454$\\ +\texttt{JUMP} & $5\to1$ & $9$ & $384$ & $126$ & $511$\\ \texttt{LOAD} & $4\to2$ & $10$ & $384$ & $253$ & $638$\\ \texttt{STORE} & $5\to2$ & $10$ & $448$ & $309$ & $758$\\ \texttt{LD}, \texttt{SD} & $2\to1$ & $8$ & $192$ & $63$ & $256$\\ @@ -291,12 +294,13 @@ \subsection{The class circuits}\label{flock:classes} \texttt{HASH} & $14\to4$ & $14$ & $1{,}152$ & $14{,}878$ & $16{,}031$\\ \hline clock, three accesses & $4\to1$ & $9$ & $320$ & $154$ & $440$\\ +clock, two accesses & $3\to1$ & $9$ & $256$ & $113$ & $335$\\ clock, \texttt{HASH}'s eighteen & $19\to1$ & $11$ & $1{,}280$ & $754$ & $2{,}000$\\ clock, \texttt{EXT}'s twelve & $17\to9$ & $12$ & $1{,}664$ & $993$ & $2{,}495$\\ \hline \end{tabular} \end{center} -A clock circuit's $\wedge$ wires include the $35$ carries placed at its output's positions (\S\ref{sec:clock}), which use none past $\jconst$, and \texttt{EXT}'s the $128$ that gate $b$'s addresses (below); the load tables' and the store tables' clock circuits make one fewer, their slots being $0,2,3$ and $0,1,2$ rather than $0,1,3$. \texttt{LD} and \texttt{SD} share one circuit, the adder of their address, whose $256$ positions fill $\kblock=8$ exactly. \texttt{ALU}'s indirect jump takes $64$ $\wedge$ wires, its flag times each bit of the sum XOR $\pc^{+}$, which make its output $\pc^{+}$ and are added to $\Delta$ but for bit $0$; its last $64$ are its jump, the decision times each bit of that offset, each placed at its output's position. \texttt{LOAD} and \texttt{STORE} make no gate for a width of $8$ bytes, which is \texttt{LD}'s and \texttt{SD}'s: their two width bits are never both set, so ``at least $2$ bytes'' is the XOR of the two; bit $2$ of their bus address is an empty position; a load shifts only the low half of the cell into place, and a store only the low half of $v_2$. +A clock circuit's $\wedge$ wires include the $35$ carries placed at its output's positions (\S\ref{sec:clock}), which use none past $\jconst$, and \texttt{EXT}'s the $128$ that gate $b$'s addresses (below); the load tables' and the store tables' clock circuits make one fewer, their slots being $0,2,3$ and $0,1,2$ rather than $0,1,3$. The clock circuit of two accesses makes the same wires for \texttt{BRANCH}, in slots $0,1$, and for \texttt{JUMP}, in slots $0,3$. \texttt{LD} and \texttt{SD} share one circuit, the adder of their address, whose $256$ positions fill $\kblock=8$ exactly. \texttt{LOAD} and \texttt{STORE} make no gate for a width of $8$ bytes, which is \texttt{LD}'s and \texttt{SD}'s: their two width bits are never both set, so ``at least $2$ bytes'' is the XOR of the two; bit $2$ of their bus address is an empty position; a load shifts only the low half of the cell into place, and a store only the low half of $v_2$. What the two verifiers and the prover have to agree on is this layout and the order the $\wedge$ wires are made in, which fixes every position; the order of the $\oplus$ wires is free, since they are substituted away. \paragraph{Addition.} A ripple-carry adder over $n$ bits ($n=64$, or $32$ in the compression). With $c_0=0$, the carry into position $i+1$ is the majority of $a_i,b_i,c_i$, @@ -313,6 +317,8 @@ \subsection{The class circuits}\label{flock:classes} Carry-save steps then compress the rows. A step replaces three rows by their sum row, the position-wise $\oplus$, and their carry row, the position-wise majority shifted up one place: a majority costs one product where at least two of the three rows have a bit, except that where exactly two do and the carry row is still free at that position, one of the two bits moves into it for nothing. Each step takes the three rows that end lowest. After $64$ steps two rows remain, and the adder above finishes. The low word of the product keeps $64$ positions of every row and drops the carry out of the top one, which is \texttt{MUL}'s $2{,}175$ products; the high word keeps all $128$, which is \texttt{MULH}'s, its signed forms correcting the product of the operands' magnitudes. \texttt{DIV} multiplies the divisor by the hinted quotient the same way and adds the remainder. +\paragraph{\texttt{ADD}, \texttt{LOGIC}, \texttt{BRANCH}, \texttt{JUMP}.} With $b=v_2\oplus\mathit{imm}$ the second operand, \texttt{ADD} is one adder of $v_1$ and $b$, or of $v_1$ and the complement of $b$ with a carry in of $1$, keeping its $64$th carry, the comparisons' borrow; then $32$ multiplexers that sign-extend the low half for a word form, one product per bit keeping the sum unless a comparison is selected, and two for the comparisons, each selector times its comparison, XORed into bit $0$. \texttt{LOGIC} makes two products per bit: with $o$ and $x$ the selectors of OR and XOR, $p=(v_1\oplus o)(b\oplus o)$, which is $v_1b$, or the complement of $v_1\vee b$ when $o$ is set, and the output bit is $p\oplus o\oplus x\,(p\oplus v_1\oplus b)$. \texttt{BRANCH} makes the $64$ carries of $v_1+\bar v_2+1$, whose carry out gives the unsigned comparison and, with the signs, the signed one; the $63$ products of the OR of the bits of $v_1\oplus v_2$, which is the inequality; one product per condition, its selector times whether it holds, their XOR being the decision; and last its jump, the decision times each bit of $\Delta$, $64$ products each placed at its output's position. \texttt{JUMP} makes the $63$ carries of the adder of $v_1$ and $\mathit{imm}$, then one product per bit $1$ to $63$, the flag $\mathit{indirect}$ times that bit of the sum XOR $\pc^{+}$, which is added to $\Delta$; bit $0$ of its jump is $\Delta$'s, so an indirect target has bit $0$ cleared. + \paragraph{The extension-field clock circuit.} \texttt{EXT} has no class circuit (\S\ref{sec:tab-classes}), so what its row needs that is Boolean its clock circuit computes, past the clock's own ports and products: four more input ports, $v_1,v_2,v_d,\mathit{flags}$, and eight more output ports, made in this order. \emph{The flags.} Their bits $0$ and $1$ are copied to two output ports, $\mathit{acc}$ and $\mathit{base}$, at no product. @@ -323,7 +329,7 @@ \subsection{The class circuits}\label{flock:classes} \paragraph{The compression.} \texttt{HASH} is the BLAKE2s compression itself: the ten rounds' $80$ G functions, each six $32$-bit additions on the halves of the ports' words, a three-operand addition being two of them chained, and XORs and rotations, which are free. Only the carries are products, $31$ per addition. -\paragraph{Batch size.} The zerocheck of \S\ref{flock:zerocheck} fixes seven coordinates of its point beyond the $\kskip$ skipped ones, so it needs $\kbool\ge13$, and lincheck works on batches of at least eight blocks, $\kbatch\ge3$. For the circuits of $\kblock\ge10$ the second bound is the binding one, and for the clock circuits of $\kblock=9$ and \texttt{LD}'s and \texttt{SD}'s circuit of $\kblock=8$ the first: a table's batches have one instance per row, so every table has at least $2^{4}$ rows, \texttt{LD} and \texttt{SD} at least $2^{5}$, \texttt{HASH} and \texttt{EXT} at least eight (\S\ref{sec:tables}). A circuit's lincheck has $\kblock-\kskip$ rounds, from $2$ to $8$, and the batch runs $\klcmax=8$. +\paragraph{Batch size.} The zerocheck of \S\ref{flock:zerocheck} fixes seven coordinates of its point beyond the $\kskip$ skipped ones, so it needs $\kbool\ge13$, and lincheck works on batches of at least eight blocks, $\kbatch\ge3$. For the circuits of $\kblock\ge10$ the second bound is the binding one, and for those of $\kblock=9$, the clock circuits and the class circuits of \texttt{ADD}, \texttt{LOGIC}, \texttt{BRANCH} and \texttt{JUMP}, and \texttt{LD}'s and \texttt{SD}'s circuit of $\kblock=8$ the first: a table's batches have one instance per row, so every table has at least $2^{4}$ rows, \texttt{LD} and \texttt{SD} at least $2^{5}$, \texttt{HASH} and \texttt{EXT} at least eight (\S\ref{sec:tables}). A circuit's lincheck has $\kblock-\kskip$ rounds, from $2$ to $8$, and the batch runs $\klcmax=8$. \subsection{Soundness analysis}\label{flock:soundness} diff --git a/python-verifier/verifier.py b/python-verifier/verifier.py index fbdde2161..fe1f40c14 100644 --- a/python-verifier/verifier.py +++ b/python-verifier/verifier.py @@ -980,7 +980,9 @@ def access(self, columns: Sequence[str], separator: Form, address: Form, access: # the product, and its clock circuit splits the flags into their bits and computes the addresses of the limbs at no # pointer. -CONTROL_COLUMNS = ("dt", "jump", "exit") # a class with jumps: the bytecode's offset, the circuit's gated jump, the exit +# A class's control columns: none; a branch's bytecode offset and the circuit's gated jump; or a jump's, then its exit +# selector. A branch's bytecode holds zero for the exit selector, so no branch row exits. +CONTROL_COLUMNS = {"none": (), "branch": ("dt", "jump"), "jump": ("dt", "jump", "exit")} HASH_COLUMNS = (*(f"cell_{k}" for k in range(HASH_WORDS)), *(f"cell_new_{HASH_OUT_WORD + j}" for j in range(4))) EXT_COLUMNS = ( *(f"limb_{k}" for k in range(EXT_LIMBS)), @@ -995,21 +997,21 @@ def access(self, columns: Sequence[str], separator: Form, address: Form, access: BYTECODE_PUBLIC_SLOT = 2 # an entry's first field, after the separator and the address -def _registers(ram: str, words: Sequence[str | None], copies: bool) -> tuple[bool, bool]: +def _registers(ram: str, words: Sequence[str | None], copies: bool, control: str) -> tuple[bool, bool]: """Whether a row reads rs2 and writes rd: when its circuits take v2 and give out, or when it is a doubleword store - reading the v2 it moves, or a doubleword load writing the cell it moves.""" - return "v2" in words or (copies and ram == "write"), "out" in words or (copies and ram == "read") + reading the v2 it moves, or a doubleword load writing the cell it moves, or a jump writing its link.""" + return "v2" in words or (copies and ram == "write"), "out" in words or (copies and ram == "read") or control == "jump" -def _class_columns(control: bool, ram: str, words: Sequence[str | None], copies: bool) -> tuple[str, ...]: - reads_rs2, writes_rd = _registers(ram, words, copies) +def _class_columns(control: str, ram: str, words: Sequence[str | None], copies: bool) -> tuple[str, ...]: + reads_rs2, writes_rd = _registers(ram, words, copies, control) # A doubleword store's new cell is its v2 column. ram_columns = RAM_COLUMNS[ram][:2] if copies else RAM_COLUMNS[ram] flag_bits = tuple(word for word in words if word and word.startswith("flag_bit_")) return ( "pc", "ts", "a1", "pc4", "v1", *(("flags",) if "flags" in words else ()), *(("a2", "v2") if reads_rs2 else ()), *(("ad", "vd_old") if writes_rd else ()), *(("out",) if "out" in words else ()), *(("ad", "vd") if "vd" in words else ()), - *(CONTROL_COLUMNS if control else ()), *(("imm",) if "imm" in words else ()), *ram_columns, *flag_bits, *(("bad",) if "bad" in words else ()), + *CONTROL_COLUMNS[control], *(("imm",) if "imm" in words else ()), *ram_columns, *flag_bits, *(("bad",) if "bad" in words else ()), *(f"prev_{i}" for i in range(len(_slots(ram, reads_rs2, writes_rd or "vd" in words)))), "step", ) # fmt: skip @@ -1024,8 +1026,8 @@ def _slots(ram: str, reads_rs2: bool, touches_rd: bool) -> tuple[int, ...]: return (*registers, RAM_SLOT) if RAM_COLUMNS[ram] else registers -def _class_flushes(opcode: int, columns: Sequence[str], control: bool, ram: str, words: Sequence[str | None], copies: bool) -> Flushes: - reads_rs2, writes_rd = _registers(ram, words, copies) +def _class_flushes(opcode: int, columns: Sequence[str], control: str, ram: str, words: Sequence[str | None], copies: bool) -> Flushes: + reads_rs2, writes_rd = _registers(ram, words, copies, control) a1, pc4, v1 = _cols(columns, "a1", "pc4", "v1") # A row without flags, an rs2 read, an rd write or an immediate reads their constants off the entry: zero, x0, the # sink, and zero. @@ -1036,18 +1038,21 @@ def _class_flushes(opcode: int, columns: Sequence[str], control: bool, ram: str, if reads_rs2: a2_form = _col(_cols(columns, "a2")[0]) if writes_rd: - # What rd receives: the circuit's result (a jump's link), or the cell a doubleword load moves. - ad, out = _cols(columns, "ad", "cell_0" if copies else "out") + # What rd receives: the circuit's result, the cell a doubleword load moves, or a jump's link, pc + 4. + ad, out = _cols(columns, "ad", "cell_0" if copies else "pc4" if control == "jump" else "out") ad_form, vd = _col(ad), _col(out) if "vd" in words: ad_form = _col(_cols(columns, "ad")[0]) if "imm" in words: imm_form = _col(_cols(columns, "imm")[0]) - if control: - # The next pc is pc + 4 plus the circuit's jump: the bytecode's offset when a fixed jump is taken, the sum XOR - # pc + 4 for an indirect one. Only an exit marks its next state, which only the final state meets. - dt, jump, exit = _cols(columns, *CONTROL_COLUMNS) - npc, fields, exit_selector = _col(pc4) + _col(jump), (_col(dt),), _col(exit) + if control != "none": + # The next pc is pc + 4 plus the circuit's jump: a branch's offset when it is taken, a jump's always, plus its + # sum XOR pc + 4 when it is indirect. + dt, jump = _cols(columns, "dt", "jump") + npc, fields = _col(pc4) + _col(jump), (_col(dt),) + if control == "jump": + # Only an exit marks its next state, which only the final state meets. + exit_selector = _col(_cols(columns, "exit")[0]) flushes = Flushes() flushes.state(columns, npc, exit_selector) entry = (_const(_gpow(opcode)), flags_form, _col(a1), a2_form, ad_form, imm_form, _col(pc4), *fields) @@ -1122,7 +1127,7 @@ class Table: name: str opcode: int # also its index in TABLES, so g^opcode is its bytecode tag - control: bool + control: str # how its rows send control: a key of CONTROL_COLUMNS ram: str # how the class uses RAM: a key of RAM_COLUMNS circuit: FlockCircuit | None # None for the class its table proves by identities ports: tuple[str | None, ...] # the circuit's port words in order: a column each, or None for a hint, which is no column @@ -1156,11 +1161,11 @@ def slots(self) -> tuple[int, ...]: @property def reads_rs2(self) -> bool: - return _registers(self.ram, self.words, self.copies)[0] + return _registers(self.ram, self.words, self.copies, self.control)[0] @property def writes_rd(self) -> bool: - return _registers(self.ram, self.words, self.copies)[1] + return _registers(self.ram, self.words, self.copies, self.control)[1] @property def reads_rd(self) -> bool: @@ -1676,64 +1681,91 @@ def circuit(self) -> FlockCircuit: return FlockCircuit(self.log_size, self.constant_column, self.bilinear) -# The ALU class's selector bits, one-hot where they select. `b` is `v2 ^ imm`, one of the two being zero. -ALU_SUB, ALU_WORD, ALU_LT, ALU_LTU, ALU_AND, ALU_OR, ALU_XOR, ALU_INDIRECT = range(8) -ALU_BRANCHES = ALU_EQ, ALU_NE, ALU_BLT, ALU_BGE, ALU_BLTU, ALU_BGEU = range(8, 14) -ALU_ALWAYS = 14 -ALU_LEGAL_FLAGS = frozenset( - sum(1 << bit for bit in bits) - for bits in [(), (ALU_SUB,), (ALU_WORD,), (ALU_SUB, ALU_WORD), (ALU_AND,), (ALU_OR,), (ALU_XOR,), (ALU_INDIRECT, ALU_ALWAYS), (ALU_ALWAYS,)] - + [(ALU_SUB, bit) for bit in (ALU_LT, ALU_LTU, *ALU_BRANCHES)] -) +# The four classes split from the ALU. Their selector bits are one-hot where they select, and `b` is `v2 ^ imm`, one of +# the two being zero. An adder's comparison subtracts; a jump's one flag says its target is the one it computes (jalr). +ADD_SUB, ADD_WORD, ADD_LT, ADD_LTU = range(4) +ADD_LEGAL_FLAGS = frozenset((0, 1 << ADD_SUB, 1 << ADD_WORD, 1 << ADD_SUB | 1 << ADD_WORD, 1 << ADD_SUB | 1 << ADD_LT, 1 << ADD_SUB | 1 << ADD_LTU)) +LOGIC_AND, LOGIC_OR, LOGIC_XOR = range(3) +LOGIC_LEGAL_FLAGS = frozenset(1 << bit for bit in (LOGIC_AND, LOGIC_OR, LOGIC_XOR)) +BRANCH_CONDITIONS = BRANCH_EQ, BRANCH_NE, BRANCH_LT, BRANCH_GE, BRANCH_LTU, BRANCH_GEU = range(6) +BRANCH_LEGAL_FLAGS = frozenset(1 << bit for bit in BRANCH_CONDITIONS) +JUMP_INDIRECT = 0 +JUMP_LEGAL_FLAGS = frozenset((0, 1 << JUMP_INDIRECT)) -def _alu() -> _GateList: - """(v1, v2, imm, flags, dt, pc4) -> (out, jump): add or subtract (and the 32-bit forms), the two comparisons, AND, OR, - XOR, the six branch conditions, the jumps. `v1 - b` is `v1 + not(b) + 1`, which borrows exactly when it does not carry - out. An indirect jump (jalr) outputs its link pc4 and offsets the successor by its sum XOR pc4, bit 0 left out, so - it lands on the sum with bit 0 cleared. `jump` is that offset added to `dt` when the jump is taken and zero - otherwise, each bit a product written at its output position.""" - c = _GateList((64, 64, 64, 15, 64, 64), (64, 64)) - v1, v2, imm, flags, dt, pc4 = c.inputs +def _adder() -> _GateList: + """(v1, v2, imm, flags) -> out: add or subtract (and the 32-bit forms), or one of the two comparisons. + `v1 - b` is `v1 + not(b) + 1`, which borrows exactly when it does not carry out.""" + c = _GateList((64, 64, 64, 4), (64,)) + v1, v2, imm, flags = c.inputs b = [c.xor(x, y) for x, y in zip(v2, imm)] - carry = flags[ALU_SUB] + carry = flags[ADD_SUB] total: list[Wire] = [] for x, y in zip(v1, b): - y = c.xor(y, flags[ALU_SUB]) + y = c.xor(y, flags[ADD_SUB]) xc, yc = c.xor(x, carry), c.xor(y, carry) total.append(c.xor(xc, y)) carry = c.xor(c.product(xc, yc), carry) ltu = c.invert(carry) lt = c.xor(ltu, c.xor(v1[63], b[63])) - diff = [c.xor(x, y) for x, y in zip(v1, b)] - ne = reduce(c.either, diff, None) - eq = c.invert(ne) + # `out`: the sum (its low 32 bits sign-extended if asked) unless a comparison replaces it by its bit. + total = total[:32] + [c.mux(flags[ADD_WORD], total[31], bit) for bit in total[32:]] + keeps = c.invert(c.xor(flags[ADD_LT], flags[ADD_LTU])) + out = [c.product(keeps, bit) for bit in total] + lt_term = c.product(flags[ADD_LT], lt) + out[0] = c.xor(out[0], c.xor(lt_term, c.product(flags[ADD_LTU], ltu))) + for i, wire in enumerate(out): + c.output(0, i, wire) + return c + + +def _logic() -> _GateList: + """(v1, v2, imm, flags) -> out: AND, OR or XOR, two products per bit. `p = (v1 ^ or)(b ^ or)` is `v1 & b`, or + `not(v1 | b)` when OR is selected, and `out = p ^ or ^ xor * (p ^ v1 ^ b)`.""" + c = _GateList((64, 64, 64, 3), (64,)) + v1, v2, imm, flags = c.inputs + either, exclusive = flags[LOGIC_OR], flags[LOGIC_XOR] + for i, (x, y) in enumerate(zip(v1, v2)): + b = c.xor(y, imm[i]) + p = c.product(c.xor(x, either), c.xor(b, either)) + xor_term = c.product(exclusive, c.xor(p, c.xor(x, b))) + c.output(0, i, c.xor(c.xor(p, either), xor_term)) + return c - # `out`: the sum (its low 32 bits sign-extended if asked) unless a selector is set. OR is AND plus XOR. - total = total[:32] + [c.mux(flags[ALU_WORD], total[31], bit) for bit in total[32:]] - none = reduce(c.xor, (flags[bit] for bit in (ALU_LT, ALU_LTU, ALU_AND, ALU_OR, ALU_XOR)), c.one) - and_or, or_xor = c.xor(flags[ALU_AND], flags[ALU_OR]), c.xor(flags[ALU_OR], flags[ALU_XOR]) - out = [c.product(none, bit) for bit in total] - for i in range(64): - both = c.product(v1[i], b[i]) - and_term = c.product(and_or, both) - out[i] = c.xor(out[i], c.xor(and_term, c.product(or_xor, diff[i]))) - lt_term = c.product(flags[ALU_LT], lt) - out[0] = c.xor(out[0], c.xor(lt_term, c.product(flags[ALU_LTU], ltu))) - offset = list(dt) - for i in range(64): - moved = c.product(flags[ALU_INDIRECT], c.xor(out[i], pc4[i])) - out[i] = c.xor(out[i], moved) - if i > 0: - offset[i] = c.xor(offset[i], moved) - taken = flags[ALU_ALWAYS] - for bit, holds in zip(ALU_BRANCHES, (eq, ne, lt, c.invert(lt), ltu, c.invert(ltu))): +def _branch() -> _GateList: + """(v1, v2, flags, dt) -> jump: `dt` when the one condition set holds, each bit a product written at its output + position, and zero otherwise. Only the carries of `v1 + not(v2) + 1` are made, which borrows exactly when it does + not carry out.""" + c = _GateList((64, 64, 6, 64), (64,)) + v1, v2, flags, dt = c.inputs + carry = c.one + for x, y in zip(v1, v2): + y = c.invert(y) + xc, yc = c.xor(x, carry), c.xor(y, carry) + carry = c.xor(c.product(xc, yc), carry) + ltu = c.invert(carry) + lt = c.xor(ltu, c.xor(v1[63], v2[63])) + ne = reduce(c.either, (c.xor(x, y) for x, y in zip(v1, v2)), None) + eq = c.invert(ne) + taken: Wire = None + for bit, holds in zip(BRANCH_CONDITIONS, (eq, ne, lt, c.invert(lt), ltu, c.invert(ltu)), strict=True): taken = c.xor(taken, c.product(flags[bit], holds)) - for i, wire in enumerate(out): - c.output(0, i, wire) - for i, bit in enumerate(offset): - c.and_output(1, i, taken, bit) + for i, bit in enumerate(dt): + c.and_output(0, i, taken, bit) + return c + + +def _jump() -> _GateList: + """(v1, imm, flags, dt, pc4) -> jump: `dt`, plus for an indirect jump (jalr) the target `v1 + imm` XOR pc4, bit 0 + left out, so that it lands on the target with bit 0 cleared. A jump's link is pc4 itself, which its table writes.""" + c = _GateList((64, 64, 1, 64, 64), (64,)) + v1, imm, flags, dt, pc4 = c.inputs + target = _add(c, v1, imm) + c.output(0, 0, dt[0]) + for i in range(1, 64): + moved = c.product(flags[JUMP_INDIRECT], c.xor(target[i], pc4[i])) + c.output(0, i, c.xor(dt[i], moved)) return c @@ -2105,27 +2137,31 @@ def _ext_clock(slots: Sequence[int]) -> _GateList: HASH_FINAL = 2**32 - 1 TABLES = ( - Table("alu", 0, True, "none", _alu().circuit(), ("v1", "v2", "imm", "flags", "dt", "pc4", "out", "jump"), ALU_LEGAL_FLAGS), + Table("add", 0, "none", "none", _adder().circuit(), ("v1", "v2", "imm", "flags", "out"), ADD_LEGAL_FLAGS), + Table("logic", 1, "none", "none", _logic().circuit(), ("v1", "v2", "imm", "flags", "out"), LOGIC_LEGAL_FLAGS), + # A branch writes no rd and has no immediate; a jump reads no rs2, and writes its link, pc + 4, to rd. + Table("branch", 2, "branch", "none", _branch().circuit(), ("v1", "v2", "flags", "dt", "jump"), BRANCH_LEGAL_FLAGS), + Table("jump", 3, "jump", "none", _jump().circuit(), ("v1", "imm", "flags", "dt", "pc4", "jump"), JUMP_LEGAL_FLAGS), # A load's flags are log2 of its width in bytes, then whether it sign-extends; a store's, log2 of its width. A # doubleword is LD's or SD's, which have no flags: their circuit is the address alone, the word moved a column. - Table("load", 1, False, "read", _load().circuit(), ("v1", "imm", "flags", "cell_0", "address", "out"), frozenset((0, 1, 2, 4, 5, 6))), - Table("store", 2, False, "write", _store().circuit(), ("v1", "v2", "imm", "flags", "cell_0", "address", "cell_new_0"), frozenset(range(3))), - Table("ld", 3, False, "read", _word_address().circuit(), ("v1", "imm", "address"), frozenset((0,)), copies=True), - Table("sd", 4, False, "write", _word_address().circuit(), ("v1", "imm", "address"), frozenset((0,)), copies=True), + Table("load", 4, "none", "read", _load().circuit(), ("v1", "imm", "flags", "cell_0", "address", "out"), frozenset((0, 1, 2, 4, 5, 6))), + Table("store", 5, "none", "write", _store().circuit(), ("v1", "v2", "imm", "flags", "cell_0", "address", "cell_new_0"), frozenset(range(3))), + Table("ld", 6, "none", "read", _word_address().circuit(), ("v1", "imm", "address"), frozenset((0,)), copies=True), + Table("sd", 7, "none", "write", _word_address().circuit(), ("v1", "imm", "address"), frozenset((0,)), copies=True), # A shift's flags: right, arithmetic (with right), 32-bit. A product's: 32-bit; its high word's: which operands are signed. - Table("shift", 5, False, "none", _shift().circuit(), ("v1", "v2", "imm", "flags", "out"), frozenset((0, 1, 3, 4, 5, 7))), - Table("mul", 6, False, "none", _mul().circuit(), ("v1", "v2", "flags", "out"), frozenset((0, 1))), - Table("mulh", 7, False, "none", _mulh().circuit(), ("v1", "v2", "flags", "out"), frozenset((0, 1, 3))), + Table("shift", 8, "none", "none", _shift().circuit(), ("v1", "v2", "imm", "flags", "out"), frozenset((0, 1, 3, 4, 5, 7))), + Table("mul", 9, "none", "none", _mul().circuit(), ("v1", "v2", "flags", "out"), frozenset((0, 1))), + Table("mulh", 10, "none", "none", _mulh().circuit(), ("v1", "v2", "flags", "out"), frozenset((0, 1, 3))), # A division's flags: signed, remainder, 32-bit. Its two hints are in its witness and in no column. - Table("div", 8, False, "none", _div().circuit(), ("v1", "v2", "flags", None, None, "out", "bad"), frozenset(range(8))), + Table("div", 11, "none", "none", _div().circuit(), ("v1", "v2", "flags", None, None, "out", "bad"), frozenset(range(8))), # The BLAKE2s precompile: the counter is v2 and the flags are the finalization word, all ones on the last block. - Table("hash", 9, False, "block", _blake2s().circuit(), HASH_PORTS, frozenset((0, HASH_FINAL))), + Table("hash", 12, "none", "block", _blake2s().circuit(), HASH_PORTS, frozenset((0, HASH_FINAL))), # The extension-field precompile, with no class circuit: a at v1, b at v2 and c at the address in rd. Its identities # say the product; its clock circuit splits the flags (accumulate, base field) and computes the limbs' addresses. Table( "ext", - 10, - False, + 13, + "none", "limbs", None, (), @@ -2172,9 +2208,9 @@ def register_words(table_log_heights: Sequence[int]) -> list[list[int]]: def check_bytecode(bytecode: Sequence[K]) -> None: """The proof system is sound for any decoded table, so what makes one RISC-V is checked here: an entry some table can read names two registers to read and a cell other than x0 to write, its successor is pc + 4, its flags are - ones its class defines, and only a branch or a jal has a jump offset, a jal linking pc + 4 as a constant added to - x0. An entry with no tag can be read by no table: a run reaching one has no proof. It has one form, the illegal - entry's, and the halt slot is one.""" + ones its class defines, only a branch, a jal or the exit has a jump offset, and a jal reads x0 and has no immediate, + its link being its table's pc + 4. An entry with no tag can be read by no table: a run reaching one has no proof. + It has one form, the illegal entry's, and the halt slot is one.""" size = len(bytecode) // 2**BUS_BITS fields = [[int(word) for word in bytecode[slot * size : (slot + 1) * size]] for slot in range(2**BUS_BITS)] tag, flags, a1, a2, ad, imm, pc4, dt = fields[BYTECODE_PUBLIC_SLOT:BAD_SLOT] @@ -2198,12 +2234,12 @@ def check_bytecode(bytecode: Sequence[K]) -> None: if exit[z]: halt_pc = TEXT_BASE + 4 * (size - 1) require( - table.control and flags[z] == 1 << ALU_ALWAYS and a1[z] == a2[z] == imm[z] == 0 and ad[z] == SINK and dt[z] == (halt_pc ^ pc4[z]), + table.control == "jump" and flags[z] == 0 and a1[z] == a2[z] == imm[z] == 0 and ad[z] == SINK and dt[z] == (halt_pc ^ pc4[z]), "an exit entry is not ECALL", ) - elif table.control and flags[z] == 1 << ALU_ALWAYS: - require(a1[z] == a2[z] == 0 and imm[z] == pc4[z], "a bytecode entry has invalid control flow") - elif not (table.control and any(flags[z] & (1 << bit) for bit in ALU_BRANCHES)): + elif table.control == "jump" and flags[z] == 0: + require(a1[z] == imm[z] == 0, "a bytecode entry has invalid control flow") + elif table.control != "branch": require(dt[z] == 0, "a bytecode entry has invalid control flow") # A field the class's table holds at a constant has to be that constant. require(table.reads_rs2 or a2[z] == 0, "a bytecode entry reads an rs2 its class does not") @@ -2481,7 +2517,7 @@ def verify_core( # Everything public and fixed is one digest, which seeds the transcript; every variable-length part is length-framed. halt_pc = TEXT_BASE + 4 * (len(bytecode) // 2**BUS_BITS - 1) require(entry_pc % 4 == 0 and TEXT_BASE <= entry_pc < halt_pc, "the entry pc is not an instruction of the text") - preimage = b"leanvm-rv64im-11" + pack("