From dd2ec28a9f5976715ac9ba6a2e50221c22ec6f28 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 01:05:03 +0200 Subject: [PATCH 01/11] feat: wip Poseidon_1 hash function --- .../src/test/poseidon/poseidon_1.zkc | 197 ++++++++++++++++++ arithmetization/src/test/poseidon/utils.zkc | 9 + 2 files changed, 206 insertions(+) create mode 100644 arithmetization/src/test/poseidon/poseidon_1.zkc create mode 100644 arithmetization/src/test/poseidon/utils.zkc diff --git a/arithmetization/src/test/poseidon/poseidon_1.zkc b/arithmetization/src/test/poseidon/poseidon_1.zkc new file mode 100644 index 00000000000..8619f3a3dce --- /dev/null +++ b/arithmetization/src/test/poseidon/poseidon_1.zkc @@ -0,0 +1,197 @@ +include "../../main/riscv/utils/types.zkc" + +// ============================================= +// zkc implementation of Poseidon_1 permutation +// ============================================= +// +// source: https://github.com/khovratovich/poseidon-tools/tree/main + + +memory ram (address :Address) -> (byte :u8) +memory params (index :u8) -> (pa :u32) +memory state (index :u8) -> (st :u32) +memory state_copy (index :u8) -> (st :u32) + +// we require TOTAL_ROUNDS * STATE_WIDTH round constants +input round_constants (index :u16) -> (rc :u32) +input mds_matrix (index :u16) -> (mt :u32) + +// this implementation does not use the native field element type yet + +const KOALABEAR_PRIME :u32 = 0x7F000001 // 2^31 - 2^24 + 1 or 2130706433 +const ALPHA :u2 = 3 +const BYTES_PER_FELT :u2 = 3 + +const OUTPUT_LENGTH :u8 = RATE // OUTPUT_LENGTH ≤ RATE is required + +const STATE_WIDTH :u8 = RATE + CAPACITY +const RATE :u8 = 12 +const CAPACITY :u8 = 4 + +// we will do +// - FULL_ROUNDS_HALF full rounds +// - PRTL_ROUNDS partial rounds +// - FULL_ROUNDS_HALF full rounds +// whence +const TOTAL_ROUNDS :u8 = FULL_ROUNDS_HALF + PRTL_ROUNDS + FULL_ROUNDS_HALF +const FULL_ROUNDS_HALF :u8 = 12 +const PRTL_ROUNDS :u8 = 8 + +fn poseidon(start :Address, size :u32) { + initialize_state(start, size) +} + +// initialize_state initializes the state to contain +// +// ┌ ┐ +// │ a │ +// │ b │ +// │ │ +// │ ⋮ │ r ≡ rate many felts +// │ │ +// │ q │ +// σ ≡ │ r │ +// ├ ┤ +// │ L │ ← peculiar to https://github.com/khovratovich/poseidon-tools/tree/main +// │ 0 │ +// │ ⋮ │ +// │ 0 │ +// └ ┘ +// +// where L ≡ length in bytes of the inputs +fn initialize_state(input_offset :Address, input_size :u32) { + + var input_felt :u32 + + for i :u8 = 0; i < RATE; i = i + 1 { + input_felt = (ram[i as Address] :: ram[(i + 1) as Address] :: ram[(i + 2) as Address]) as u32 + write_to_state(i, input_felt) + } + + // Note: technically one should record 'input_size mod KOALABEAR_PRIME' rather than 'input_size' + write_to_state(RATE, input_size) + + for i :u8 = RATE; i < STATE_WIDTH; i = i + 1 { + write_to_state(i, 0) + } +} + +// update_state updates the current state σ to σ' defined by +// adding the next batch of data carrying felts (nxt) to the +// rate many first coordinates of σ. +// +// σ' ≡ σ + nxt +// +// ←σ→ ←nxt→ +// ┌ ┐ ┌ ┐ +// │ A │ │ a │ +// │ B │ │ b │ +// │ │ │ │ +// │ ⋮ │ │ ⋮ │ +// │ │ │ │ +// │ Q │ │ q │ +// ≡ │ R │ + │ r │ +// ├ ┤ ├ ┤ +// │ Λ │ │ 0 │ +// │ μ │ │ 0 │ +// │ ⋮ │ │ ⋮ │ +// │ π │ │ 0 │ +// └ ┘ └ ┘ +// +fn update_state(input_offset :Address) { + var input_felt :u32 + var curr_value :u32 + var updt_value :u32 + var overflow :u1 + + for i :u8 = 0; i < RATE; i = i + 1 { + input_felt = (ram[i as Address] :: ram[(i + 1) as Address] :: ram[(i + 2) as Address]) as u32 + curr_value = read_from_state(i) + overflow :: updt_value = (curr_value as u33) + (input_felt as u33) + write_to_state(i, updt_value) + } +} + +fn permutation(initial_round :Boolean) { + + for r :u8 = 0; r < FULL_ROUNDS_HALF; r = r + 1 { + full_round(r) + } + + for r :u8 = 0; r < PRTL_ROUNDS; r = r + 1 { + partial_round(r + FULL_ROUNDS_HALF) + } + + for r :u8 = 0; r < FULL_ROUNDS_HALF; r = r + 1 { + full_round(r + FULL_ROUNDS_HALF + PRTL_ROUNDS) + } +} + +// sbox computes the ALPHA-th power of its input +fn sbox(x :u32) -> (res :u32) { + var aux :u64 + + // square + aux = (x as u64) * (x as u64) + res = (aux % (KOALABEAR_PRIME as u64)) as u32 + + // cube + aux = (res as u64) * (x as u64) + res = (aux % (KOALABEAR_PRIME as u64)) as u32 + + return +} + +fn add_round_constants(r :u8) { + var start_index :u16 = (r as u16) * (STATE_WIDTH as u16) + var round_constant :u32 + var state_value :u32 + var overflow :u1 + + for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { + round_constant = round_constants[start_index] + state_value = state[i] + overflow :: state_value = (round_constant as u33) + (state_value as u33) + state[i] = state_value % KOALABEAR_PRIME + start_index = start_index + 1 + } +} + +fn full_round(r :u8) { + add_round_constants(r) + for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { + state[i] = sbox(state[i]) + } + apply_mds() +} + +fn partial_round(r :u8) { + add_round_constants(r) + state[0] = sbox(state[0]) + apply_mds() +} + +// apply_mds applies the STATE_WIDTH x STATE_WIDTH mds matrix to the +// state, viewed as a column vector w/ STATE_WIDTH many rows. +fn apply_mds() { + + // STATE_WIDTH < 2**8 + // mds[i,j] < 2**32 + // state[j] < 2**32 + // sum_j mds[i,j] ∙ state[j] < 2**(32 + 32 + 8) = 2**72 + var index :u16 = 0 + for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { + var unreduced_sum :u72 = 0 + for j :u8 = 0; j < STATE_WIDTH; j = j + 1 { + unreduced_sum = unreduced_sum + ((mds_matrix[index] as u72) * (state[j] as u72)) + index = index + 1 + } + state_copy[i] = (unreduced_sum % (KOALABEAR_PRIME as u72)) as u32 + } + + // we copy the updated state over to the state + for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { + state[i] = state_copy[i] + } +} + diff --git a/arithmetization/src/test/poseidon/utils.zkc b/arithmetization/src/test/poseidon/utils.zkc new file mode 100644 index 00000000000..f74f5830bc2 --- /dev/null +++ b/arithmetization/src/test/poseidon/utils.zkc @@ -0,0 +1,9 @@ + +fn write_to_state(address :u8, value:u32) -> () { + state[address] = value +} + +fn read_from_state(address :u8) -> (value :u32) { + value = state[address] + return +} From bd3e3fb89ca6865396c97e033864fc7982f1885d Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 17:27:30 +0200 Subject: [PATCH 02/11] wip --- .../src/test/examples/rust/poseidon1.rs | 106 ++++++++++++++++++ arithmetization/src/test/poseidon/README.md | 41 +++++++ arithmetization/src/test/poseidon/notes.md | 53 +++++++++ .../{poseidon_1.zkc => poseidon1.zkc} | 57 +++++++--- .../test/poseidon/test/poseidon1_01.accepts | 7 ++ .../src/test/poseidon/test/poseidon1_01.zkc | 11 ++ 6 files changed, 259 insertions(+), 16 deletions(-) create mode 100644 arithmetization/src/test/examples/rust/poseidon1.rs create mode 100644 arithmetization/src/test/poseidon/README.md create mode 100644 arithmetization/src/test/poseidon/notes.md rename arithmetization/src/test/poseidon/{poseidon_1.zkc => poseidon1.zkc} (73%) create mode 100644 arithmetization/src/test/poseidon/test/poseidon1_01.accepts create mode 100644 arithmetization/src/test/poseidon/test/poseidon1_01.zkc diff --git a/arithmetization/src/test/examples/rust/poseidon1.rs b/arithmetization/src/test/examples/rust/poseidon1.rs new file mode 100644 index 00000000000..342cf3f7b48 --- /dev/null +++ b/arithmetization/src/test/examples/rust/poseidon1.rs @@ -0,0 +1,106 @@ +#![no_std] +#![no_main] + +/// inputs: +/// - [×] KOALABEAR prime +/// - [φ] 8 = n_full_rounds +/// - [φ] 20 = n_partial_rounds +/// - [φ] 1 = output_size +/// - [φ] mds_matrix +/// - [φ] round_constants +/// - [✓] input vector +/// - [✓] output vector +/// +/// φ ≡ fixed +/// ✓ ≡ to be provided +/// × ≡ don't need it + +/// constants in the zkc file: +/// +/// mds_matrix ≡ 0x07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a5bf72c2447f777784dd6b5ae10eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a5bf72c2447f7777863c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a5bf72c243a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed58e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555560fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c8591489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd174669d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf333344286186232cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf333341fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af28754aaaaab1fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c723f80000054aaaaab1fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f17f0000003f80000054aaaaab1fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f00000 +/// roundconstants ≡ 0x7ee56a481136704512e419417ebbc12b1970b7d5662b60e83e4990c6679f91f5350813bb00874ad428a0081a18fa58725f25b0715e5d59985e6fd3e75b2e26606f1837bf3fe6182b1edd7ac557470d0043d486d51982c70f0ea53af961d6165b51639c002dec352c2950e5312d2cb94708256cef1a0109f61f51faf35cef1c623d65e50e33d91626133d5a1e0ff49b0d38900cd12c22cc3f28852bb206c65a027b2cf7bc68016e1a15e16bc05248149a6dd212a018d6830a5001be8264dac34e5902b287426583a00c9216323fe028a5245f8e4943bb297e7873dbd93cc987df286bb4ce640a8dcd512a8e3603a4cf55481837a203d6da8473726ac7760e7fdf54dfeb5d7d40afd6722cb316106a457345a7ccdb44061375154077a545744faa4eb5e5ee3794e83f47c7093c5694903c69cb6299373df84c46a0df5846b8758a3241ebcb0b09d2331af423571e66cec243e7dc24259a5d6127e85a3b1b9133fa343e5628485cd4c216e269f5165b60c625f683d9124f81f9174331f977344dc55a821dba5fc4177f54153bf55e3f11943bdbf191088c84a368256c9b3c90bbc66846166a03f4238d463335fb5e3d35516e59ae6f32d06cc0596293f36c87edb208fc60b534bcca8024f007f362731c6f1e1db6c60ca409bb585c1e7856e94edc16d2273418e114677b2c3730770075e435d1b18c22be3db54fb1fbb7477cb3ed7d5311c65b62ae7d559c5fa877f150483211570b490fef6a77ec311f2247171b4e0ac7112edf69c93b5a8850658094215619b4aa362019a76bf9d4ed5b413dff617e181e5e7ab57b33ad78333466c7ca6488dff471f068f4056e891f04f1eccc663257d5671e31b95871987c280c109e2a227761350a25e95b91b1c47a0735460182627053a677200ed4b07434cf0c4e6e751e8829bd5f5949ec32df7693452b3cf09e586ba0e2bf7ab93acf3ce597df536e3d42147a808d5e32eb565a203323509657666d44b7c56698636a57b84f9f554b61b96da0ab281585b6ac6705a2b4152872f60f4409fd23a9dd606f2b18d465ac9fd42f0efbea591e67fd217ca19b469c90ca03d60ef54ea7857e07c86a4f288ed4612fe51b227e2936142c4beb855b0b7d111e17dff6089beae10a5acf1a2fc33d8f60422dc66e1dc939635351b955522fc03eb94ef72a24a65c2e139c765139114478cc0742579538f944de9aae3c2f1e2e195747be2496339c650b2e39528996656cb355580f461c1c70f6b2703faaa36f62e3348a672167cb394c880b2a46ba8263ffb74a1cf875d653d12772036a45523bdd9f2b02f72c2402b6006c077fe1581f9d6ea420904d6f5d6534fa066d89746198f1f426301ab441f274c200eac15c28b54b472339739d48c6281c4ed935fc3f9187fa4a1930a63ad4d7360f3f1889635a388f2862c145277ed1e84db23cad1f1b11f51f3dba2b1c26eb4e0f7f55466cd024b067c47902793b89000e8a283c4590b7ea6f567a2b5dc9730015247bc650567fcb133eff84547dc2ef34eb3dbb1240231766c6ae49174338b6242510081b514927062d98d67af30bbc26af15e870d907a35dfc5cac731f27ec53aa7d3f63ab0ec6216053f418796b3919156afd5eea69736704c6a90dce002b331169c0714d71783ddaffaf7e46495720ca59ea679820c942ef21a1798ea08914a74fa30c06cf186a4c8d52620f6d812220901a5277bb90230bf95e0ad8847a5e96e8b677b4056e70a50d2c5f0eed593646c4df10eb9a8721eed6b7534add366e3e74212b25810e1d8f707b45318a1a677f8ff20258c9e04cd02a002e24ff15634a715d4ac01e59601511e126e9c01a4c165c6e57cd11403ac6543b6787d847037dfbf96dd9d0794d24b2812a6f407d0131df8e4b8a7896237008582cf5e53412aafc3f54568d031a2507355331686d4ce76d91799c1a8c2b7a8ac960aee67274f7421c3c42146d26d369c54ae54a127eea16d15ce3eae869f28994262b8642610d4cc45e1af21c1a8526d0316b127b3576fe5d02d968a04ba00f5140bed993377fb9077859216e1931d9d153b0934e71914ff74eabae6c7196468e164b3cc258cb66c04c1473076b3afccd4236518b4ad85605291382e11e89b6cf5e16c3a82e6759212430095405e555c378880a24763a31254f53b24018b7fa432bbe8a731c9a12f23f6fd40d0e1d4ec41361c64d09a8f47003d23a40109ad29028c2fb883b6498f274d8be576a4277d218c2b3d46252c30c07cc2560209fe15b52a55fac4df19eb7025211165e414ff13cd9a1f4005aad1527a53f0072bbe9cb71d8bd7d4194b79a48e87a723341553c63d34faa132a01e33833e2d949726e04054957f87b71bce473eec57d556e55331fa93fde346a8ca81162dfde5c30d028094a42943052dcda3798849851f06b97658487797599b0d4436fdabc66c5b77d40c86a9e27e7055b6d0dd9d87e5598b51a4d04f35e3b2bc7533b5b2f3e33a125664d71ce382e6c2a24c4eb6e13f246f707e2d7ef + +const INPUT_STRING = "000102030405060708090a0b0c0d0e0f"; +const OUPUT_STRING = "00"; // TODO + +/// Poseidon1 function call +/// +/// zkc-test poseidon1.rs + +// use core::convert::TryInto; +// use core::result::Result; +// use core::result::Result::Err; +// use core::result::Result::Ok; + +const INPUT_LENGTH = 16; // length in bytes of the input string +const OUTPUT_SIZE = 1; // number of output field elements, has to be ≤ rate + + +core::arch::global_asm!( + ".global _start", + "_start:", + "li sp, 0x087fffff", // set stack pointer to a known memory region + "call main", +); + + +fn poseidon_1(input_offset :u64, input_size :u64, output_offset :u64) { + unsafe { + core::arch::asm!( + // interpretation of ":insn r 0x0b, 0x42, 0x69, {2}, {0}, {1}", + // + // instruction type: r + // opcode: 0x0b ≡ custom-0 + // funct3: 0x42 + // funct7: 0x69 + // + // {0} = register address holding io + // {1} = register address holding is + // {2} = register address holding ro + // + // order is decided by the declaration order of the in(reg) XXX + ":insn r 0x0b, 0x42, 0x69, {2}, {0}, {1}", + in(reg) input_offset, + in(reg) input_size, + in(reg) output_offset, + ); + } +} + +/// Parse a hex string into a [u8; INPUT_LENGTH], for input. +pub fn hex_to_input(s: &str) -> [u8; INPUT_LENGTH] { + let mut out = [0u8; INPUT_LENGTH]; + for i in 0..INPUT_LENGTH { + out[i] = u8::from_str_radix(&s[i * 2..i * 2 + 2], 16).unwrap(); + } + out +} + +#[no_mangle] +fn main() -> ! { + + let input = hex_to_input(INPUT_STRING); + + poseidon_1(&input, len(input), 0); + + // Encode the 5 codes into a single exit code (e.g. 0000 for all pass, 1000 for 1st test failing, etc.) + exit(0); +} + +fn exit(code: i32) -> ! { + unsafe { + core::arch::asm!( + "mv a0, {0}", // exit code + "li a7, 93", // syscall number for exit + "ecall", + in(reg) code, + options(noreturn) + ); + } +} + +// required by the compiler +#[panic_handler] +fn panic(_: &core::panic::PanicInfo) -> ! { + exit(3); +} diff --git a/arithmetization/src/test/poseidon/README.md b/arithmetization/src/test/poseidon/README.md new file mode 100644 index 00000000000..423ff3c2c94 --- /dev/null +++ b/arithmetization/src/test/poseidon/README.md @@ -0,0 +1,41 @@ +# Generating data + +The Poseidon hash function requires two pieces of data besides the (nonempty) input byte slice: +- the mds matrix of size t×t +- the round constants a matrix of size r×t +where t ≡ state width t and r ≡ total rounds. + +This data can be generated using the [poseidon-tools](https://github.com/khovratovich/poseidon-tools) library. + +## Generatring an mds matrix + +The following generates the MDS matrix for the koalabear prime with state width 16. + +```bash + python3 +>>> from poseidon.mds_matrix import generate_mds_matrix +>>> KOALABEAR_P = 2130706433 +>>> STATE_WIDTH = 16 +>>> [[f"{k:08x}" for k in l] for l in generate_mds_matrix(STATE_WIDTH, KOALABEAR_P)] +``` + +## Getting round constants + +For the round constants I used `_KB_ROUND_CONSTANTS_16` from the tests of that repo. + +## Stuff + +```bash + python3 +>>> from poseidon.poseidon import Poseidon +>>> KOALABEAR_P = 2130706433 +>>> pos = Poseidon(prime=KOALABEAR_P, alpha=3, t=16, r_f=8, r_p=20) +# t is the state_width, no rate is specified (it defaults to t-1), r_f is the number of full rounds (which has to be +# even), r_p that of partial rounds +>>> pos.sponge_hash(list(range(16)), 1) +[584229223] +>>> pos.sponge_hash(list(range(16)), 15) +[584229223, 1225903167, 435734976, 745693090, 1580884015, 1393870516, 1514786559, 1416327482, 401740899, 305698337, 123847430, 1985271412, 660999169, 1953826170, 1390527262] +# 1 and 15 are the the respectve output_size's, which have to be ≤ rate +``` + diff --git a/arithmetization/src/test/poseidon/notes.md b/arithmetization/src/test/poseidon/notes.md new file mode 100644 index 00000000000..cb0667385c7 --- /dev/null +++ b/arithmetization/src/test/poseidon/notes.md @@ -0,0 +1,53 @@ +- Rust or Zig program `poseidon.rs` +- that populates memory with inputs, either as + - hardcoded (nonempty) inputs + - alternatively that takes (nonempty) inputs from a file +- example: in_bytes = [0x00, 0x01, ..., 0xff] +- add an in-line assembly custom-0 instruction to run poseidon with + - special opcode + - special type (maybe R-type) + - and funct3/funct7 coding for the Poseidon1 precompile + +Question: which registers will hold the pointer to the data + its size ? Also: where do you write the output ? + +All of these could be in rs1, rs2, rd [which is ok if we go with R-type] + +```rust +poseidon(io :u64, is: u64, ro: u64) { + unsafe { + core::arch::asm!( + // funct3 = 42, funct7 = 69 + // r-type isntruction, 0x0b ≡ custom-0, 42 = funct3, 69 = funct7, + // {0} = register address holding io + // {1} = register address holding is + // {2} = register address holding ro + // order is decided by the declaration order of the in(reg) XXX + ":insn r 0x0b, 42, 69, {2}, {0}, {1}", + in(reg) io, + in(reg) is, + in(reg) ro, + ); + } +} + +// à la +fn exit(code: i32) -> ! { + unsafe { + core::arch::asm!( + "mv a0, {0}", // exit code + "li a7, 93", // syscall number for exit + "ecall", + in(reg) code, + options(noreturn) + ); + } +} +``` + +According to Claude: + +``` +Custom-0 through custom-3 instructions in RISC-V don't have a fixed instruction type — the spec reserves the opcodes but leaves the encoding format up to the implementer. You can use any of the standard formats (R, I, S, etc.) or define your own, as long as bits [1:0] are 11 (indicating a 32-bit instruction). + +That said, R-type is the most common choice for custom instructions since it gives you two source registers and one destination register with no implicit memory semantics. +``` diff --git a/arithmetization/src/test/poseidon/poseidon_1.zkc b/arithmetization/src/test/poseidon/poseidon1.zkc similarity index 73% rename from arithmetization/src/test/poseidon/poseidon_1.zkc rename to arithmetization/src/test/poseidon/poseidon1.zkc index 8619f3a3dce..edbd697dd77 100644 --- a/arithmetization/src/test/poseidon/poseidon_1.zkc +++ b/arithmetization/src/test/poseidon/poseidon1.zkc @@ -1,32 +1,40 @@ +include "../../main/riscv/memory.zkc" include "../../main/riscv/utils/types.zkc" +include "../../main/riscv/main.zkc" +include "../../main/riscv/utils/type.zkc" +include "../../main/riscv/ram/write.zkc" // ============================================= // zkc implementation of Poseidon_1 permutation // ============================================= // -// source: https://github.com/khovratovich/poseidon-tools/tree/main +// we use as source the implementation found in +// +// https://github.com/khovratovich/poseidon-tools/tree/main +// +// One notable feature of this implementation is that the length +// of the message is included in the state at initialization time. -memory ram (address :Address) -> (byte :u8) -memory params (index :u8) -> (pa :u32) memory state (index :u8) -> (st :u32) memory state_copy (index :u8) -> (st :u32) -// we require TOTAL_ROUNDS * STATE_WIDTH round constants +// round_constants is a matrix with TOTAL_ROUNDS many rows and STATE_WIDTH many columns +// mds_matrix is a square matrix of format STATE_WIDTH × STATE_WIDTH input round_constants (index :u16) -> (rc :u32) -input mds_matrix (index :u16) -> (mt :u32) +input mds_matrix (index :u16) -> (md :u32) // this implementation does not use the native field element type yet const KOALABEAR_PRIME :u32 = 0x7F000001 // 2^31 - 2^24 + 1 or 2130706433 const ALPHA :u2 = 3 -const BYTES_PER_FELT :u2 = 3 +const BYTES_PER_FELT :u8 = 3 const OUTPUT_LENGTH :u8 = RATE // OUTPUT_LENGTH ≤ RATE is required const STATE_WIDTH :u8 = RATE + CAPACITY -const RATE :u8 = 12 -const CAPACITY :u8 = 4 +const RATE :u8 = 15 +const CAPACITY :u8 = 1 // we will do // - FULL_ROUNDS_HALF full rounds @@ -34,10 +42,10 @@ const CAPACITY :u8 = 4 // - FULL_ROUNDS_HALF full rounds // whence const TOTAL_ROUNDS :u8 = FULL_ROUNDS_HALF + PRTL_ROUNDS + FULL_ROUNDS_HALF -const FULL_ROUNDS_HALF :u8 = 12 -const PRTL_ROUNDS :u8 = 8 +const FULL_ROUNDS_HALF :u8 = 4 // 8 full rounds +const PRTL_ROUNDS :u8 = 20 -fn poseidon(start :Address, size :u32) { +fn poseidon(start :Address, size :u32) { initialize_state(start, size) } @@ -59,7 +67,7 @@ fn poseidon(start :Address, size :u32) { // └ ┘ // // where L ≡ length in bytes of the inputs -fn initialize_state(input_offset :Address, input_size :u32) { +fn initialize_state(input_offset :Address, input_size :u32) { var input_felt :u32 @@ -92,27 +100,44 @@ fn initialize_state(input_offset :Address, input_size :u32) // │ Q │ │ q │ // ≡ │ R │ + │ r │ // ├ ┤ ├ ┤ -// │ Λ │ │ 0 │ +// │ λ │ │ 0 │ // │ μ │ │ 0 │ // │ ⋮ │ │ ⋮ │ // │ π │ │ 0 │ // └ ┘ └ ┘ // -fn update_state(input_offset :Address) { +fn update_state(offset :Address, num_bytes :u8) { var input_felt :u32 var curr_value :u32 var updt_value :u32 var overflow :u1 + if num_bytes == 0 { fail } + if num_bytes > ((BYTES_PER_FELT as u8) * (RATE as u8)) { fail } + for i :u8 = 0; i < RATE; i = i + 1 { - input_felt = (ram[i as Address] :: ram[(i + 1) as Address] :: ram[(i + 2) as Address]) as u32 + input_felt = (ram[(i + 2) as Address] :: ram[(i + 1) as Address] :: ram[(i + 0) as Address]) as u32 curr_value = read_from_state(i) overflow :: updt_value = (curr_value as u33) + (input_felt as u33) write_to_state(i, updt_value) } } -fn permutation(initial_round :Boolean) { +fn get_full_felt(offset :Address) -> (felt :u32) { + felt = (ram[(offset + 2) as Address] :: ram[(offset + 1) as Address] :: ram[(offset + 0) as Address]) as u32 +} + +fn get_partial_felt(offset :Address, n_bytes :u8) -> (felt :u32) { + if n_bytes == 0 { fail } + if n_bytes > BYTES_PER_FELT { fail } + + felt = 0 + for i :u8 = n_bytes - 1; i >= 0; i = i - 1 { + felt = (felt << 8) + (ram[offset + (i as u64)] as u32) + } +} + +fn permutation(initial_round :Boolean) { for r :u8 = 0; r < FULL_ROUNDS_HALF; r = r + 1 { full_round(r) diff --git a/arithmetization/src/test/poseidon/test/poseidon1_01.accepts b/arithmetization/src/test/poseidon/test/poseidon1_01.accepts new file mode 100644 index 00000000000..212bc093c0d --- /dev/null +++ b/arithmetization/src/test/poseidon/test/poseidon1_01.accepts @@ -0,0 +1,7 @@ +{ + "mds_matrix": + "0x07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_5ccec4ed_41da12f7_7164924a_5bf72c24_47f77778_4dd6b5ae_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_5ccec4ed_41da12f7_7164924a_5bf72c24_47f77778_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_5ccec4ed_41da12f7_7164924a_5bf72c24_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_5ccec4ed_41da12f7_7164924a_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_5ccec4ed_41da12f7_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_5ccec4ed_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_6fc28f5d_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_59f55556_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_2c2c8591_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_1cdd1746_69d55556_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_42861862_32cccccd_69d55556_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_6bf33334_1fc00000_32cccccd_69d55556_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_281af287_54aaaaab_1fc00000_32cccccd_69d55556_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_23471c72_3f800000_54aaaaab_1fc00000_32cccccd_69d55556_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000_0ef0f0f1_7f000000_3f800000_54aaaaab_1fc00000_32cccccd_69d55556_48924925_0fe00000_468e38e4_58e66667_39ba2e8c_34eaaaab_3a9d89d9_63c92493_10eeeeef_07f00000", + "round_constants": + "0x7ee56a48_11367045_12e41941_7ebbc12b_1970b7d5_662b60e8_3e4990c6_679f91f5_350813bb_00874ad4_28a0081a_18fa5872_5f25b071_5e5d5998_5e6fd3e7_5b2e2660_6f1837bf_3fe6182b_1edd7ac5_57470d00_43d486d5_1982c70f_0ea53af9_61d6165b_51639c00_2dec352c_2950e531_2d2cb947_08256cef_1a0109f6_1f51faf3_5cef1c62_3d65e50e_33d91626_133d5a1e_0ff49b0d_38900cd1_2c22cc3f_28852bb2_06c65a02_7b2cf7bc_68016e1a_15e16bc0_5248149a_6dd212a0_18d6830a_5001be82_64dac34e_5902b287_426583a0_0c921632_3fe028a5_245f8e49_43bb297e_7873dbd9_3cc987df_286bb4ce_640a8dcd_512a8e36_03a4cf55_481837a2_03d6da84_73726ac7_760e7fdf_54dfeb5d_7d40afd6_722cb316_106a4573_45a7ccdb_44061375_154077a5_45744faa_4eb5e5ee_3794e83f_47c7093c_5694903c_69cb6299_373df84c_46a0df58_46b8758a_3241ebcb_0b09d233_1af42357_1e66cec2_43e7dc24_259a5d61_27e85a3b_1b9133fa_343e5628_485cd4c2_16e269f5_165b60c6_25f683d9_124f81f9_174331f9_77344dc5_5a821dba_5fc4177f_54153bf5_5e3f1194_3bdbf191_088c84a3_68256c9b_3c90bbc6_6846166a_03f4238d_463335fb_5e3d3551_6e59ae6f_32d06cc0_596293f3_6c87edb2_08fc60b5_34bcca80_24f007f3_62731c6f_1e1db6c6_0ca409bb_585c1e78_56e94edc_16d22734_18e11467_7b2c3730_770075e4_35d1b18c_22be3db5_4fb1fbb7_477cb3ed_7d5311c6_5b62ae7d_559c5fa8_77f15048_3211570b_490fef6a_77ec311f_2247171b_4e0ac711_2edf69c9_3b5a8850_65809421_5619b4aa_362019a7_6bf9d4ed_5b413dff_617e181e_5e7ab57b_33ad7833_3466c7ca_6488dff4_71f068f4_056e891f_04f1eccc_663257d5_671e31b9_5871987c_280c109e_2a227761_350a25e9_5b91b1c4_7a073546_01826270_53a67720_0ed4b074_34cf0c4e_6e751e88_29bd5f59_49ec32df_7693452b_3cf09e58_6ba0e2bf_7ab93acf_3ce597df_536e3d42_147a808d_5e32eb56_5a203323_50965766_6d44b7c5_6698636a_57b84f9f_554b61b9_6da0ab28_1585b6ac_6705a2b4_152872f6_0f4409fd_23a9dd60_6f2b18d4_65ac9fd4_2f0efbea_591e67fd_217ca19b_469c90ca_03d60ef5_4ea7857e_07c86a4f_288ed461_2fe51b22_7e293614_2c4beb85_5b0b7d11_1e17dff6_089beae1_0a5acf1a_2fc33d8f_60422dc6_6e1dc939_635351b9_55522fc0_3eb94ef7_2a24a65c_2e139c76_51391144_78cc0742_579538f9_44de9aae_3c2f1e2e_195747be_2496339c_650b2e39_52899665_6cb35558_0f461c1c_70f6b270_3faaa36f_62e3348a_672167cb_394c880b_2a46ba82_63ffb74a_1cf875d6_53d12772_036a4552_3bdd9f2b_02f72c24_02b6006c_077fe158_1f9d6ea4_20904d6f_5d6534fa_066d8974_6198f1f4_26301ab4_41f274c2_00eac15c_28b54b47_2339739d_48c6281c_4ed935fc_3f9187fa_4a1930a6_3ad4d736_0f3f1889_635a388f_2862c145_277ed1e8_4db23cad_1f1b11f5_1f3dba2b_1c26eb4e_0f7f5546_6cd024b0_67c47902_793b8900_0e8a283c_4590b7ea_6f567a2b_5dc97300_15247bc6_50567fcb_133eff84_547dc2ef_34eb3dbb_12402317_66c6ae49_174338b6_24251008_1b514927_062d98d6_7af30bbc_26af15e8_70d907a3_5dfc5cac_731f27ec_53aa7d3f_63ab0ec6_216053f4_18796b39_19156afd_5eea6973_6704c6a9_0dce002b_331169c0_714d7178_3ddaffaf_7e464957_20ca59ea_679820c9_42ef21a1_798ea089_14a74fa3_0c06cf18_6a4c8d52_620f6d81_2220901a_5277bb90_230bf95e_0ad8847a_5e96e8b6_77b4056e_70a50d2c_5f0eed59_3646c4df_10eb9a87_21eed6b7_534add36_6e3e7421_2b25810e_1d8f707b_45318a1a_677f8ff2_0258c9e0_4cd02a00_2e24ff15_634a715d_4ac01e59_601511e1_26e9c01a_4c165c6e_57cd1140_3ac6543b_6787d847_037dfbf9_6dd9d079_4d24b281_2a6f407d_0131df8e_4b8a7896_23700858_2cf5e534_12aafc3f_54568d03_1a250735_5331686d_4ce76d91_799c1a8c_2b7a8ac9_60aee672_74f7421c_3c42146d_26d369c5_4ae54a12_7eea16d1_5ce3eae8_69f28994_262b8642_610d4cc4_5e1af21c_1a8526d0_316b127b_3576fe5d_02d968a0_4ba00f51_40bed993_377fb907_7859216e_1931d9d1_53b0934e_71914ff7_4eabae6c_7196468e_164b3cc2_58cb66c0_4c147307_6b3afccd_4236518b_4ad85605_291382e1_1e89b6cf_5e16c3a8_2e675921_24300954_05e555c3_78880a24_763a3125_4f53b240_18b7fa43_2bbe8a73_1c9a12f2_3f6fd40d_0e1d4ec4_1361c64d_09a8f470_03d23a40_109ad290_28c2fb88_3b6498f2_74d8be57_6a4277d2_18c2b3d4_6252c30c_07cc2560_209fe15b_52a55fac_4df19eb7_02521116_5e414ff1_3cd9a1f4_005aad15_27a53f00_72bbe9cb_71d8bd7d_4194b79a_48e87a72_3341553c_63d34faa_132a01e3_3833e2d9_49726e04_054957f8_7b71bce4_73eec57d_556e5533_1fa93fde_346a8ca8_1162dfde_5c30d028_094a4294_3052dcda_37988498_51f06b97_65848779_7599b0d4_436fdabc_66c5b77d_40c86a9e_27e7055b_6d0dd9d8_7e5598b5_1a4d04f3_5e3b2bc7_533b5b2f_3e33a125_664d71ce_382e6c2a_24c4eb6e_13f246f7_07e2d7ef" +} + diff --git a/arithmetization/src/test/poseidon/test/poseidon1_01.zkc b/arithmetization/src/test/poseidon/test/poseidon1_01.zkc new file mode 100644 index 00000000000..0f6fdd1e933 --- /dev/null +++ b/arithmetization/src/test/poseidon/test/poseidon1_01.zkc @@ -0,0 +1,11 @@ +include "../../main/riscv/memory.zkc" +include "../../main/riscv/utils/types.zkc" +include "../../main/riscv/main.zkc" +include "../../main/riscv/utils/type.zkc" +include "../../main/riscv/ram/write.zkc" + +fn main() { + for i :Address = 0; i < 16; i = i + 1 { + write_8(i * 4, i as u8) + } +} From 5fa31c146f48c7cd1d152a01fb0736cfcda88484 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 22:28:22 +0200 Subject: [PATCH 03/11] fix: switch over opcode in process_R_type_instruction + CUSTOM inst This addresses issue #3018 + introduces switch statements in instrution processing --- .../riscv/instruction_processing/r_type.zkc | 464 ++++++++++-------- .../src/main/riscv/interpreter.zkc | 4 +- .../src/main/riscv/utils/constants.zkc | 8 +- 3 files changed, 280 insertions(+), 196 deletions(-) diff --git a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc index 8dde449fb79..4d2e33d84de 100644 --- a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc @@ -36,7 +36,7 @@ include "../utils/signed_comparisons.zkc" // treat register values as two's-complement integers. Division and remainder // follow RISC-V semantics: division by zero returns −1 (or the dividend for REM), // and signed overflow (INT_MIN / −1) returns INT_MIN (or 0 for REM). -fn process_R_type_instruction(instruction_parameters:u25) { +fn process_R_type_instruction(opcode:Opcode, instruction_parameters:u25) { var funct7:Funct7 var rs2:Register @@ -69,6 +69,8 @@ fn process_R_type_instruction(instruction_parameters:u25) { funct7::rs2::rs1::funct3::rd = instruction_parameters + printf "funct3 ≡ %b, funct7 ≡ %b\n", funct3, funct7 + v1 = registers[rs1] v2 = registers[rs2] @@ -82,221 +84,299 @@ fn process_R_type_instruction(instruction_parameters:u25) { // and you interpret them either as uintN or intN, then the underlying // bit string of their additions is the same in both interpretations. // This also holds for subtraction. - if (funct3 == FUNCT3_ADD) && (funct7 == FUNCT7_ADD) { - overflow::double_word_working_copy = (v1 as u65) + (v2 as u65) - registers[rd] = double_word_working_copy - } - if (funct3 == FUNCT3_SUB) && (funct7 == FUNCT7_SUB) { - // we prevent underflow by pre-pending v1 with a 1 - overflow::double_word_working_copy = ((1 as u1)::(v1 as u64)) - (v2 as u65) - registers[rd] = double_word_working_copy - } - if (funct3 == FUNCT3_SLL) && (funct7 == FUNCT7_SLL) { - shift_discard_6::shift_amount_6 = v2 - registers[rd] = v1 << shift_amount_6 - } - if (funct3 == FUNCT3_SLT) && (funct7 == FUNCT7_SLT) { - registers[rd] = signed_LT(v1, v2) as DoubleWord - } - if (funct3 == FUNCT3_SLTU) && (funct7 == FUNCT7_SLTU) { - if (v1> shift_amount_6 - } - if (funct3 == FUNCT3_SRA) && (funct7 == FUNCT7_SRA) { - shift_discard_6::shift_amount_6 = v2 - if (v1_sign == 1) { - double_word_working_copy = bit_flip_double_word(v1) - } else { - double_word_working_copy = v1 - } - double_word_working_copy = double_word_working_copy >> shift_amount_6 - if (v1_sign == 1) { - double_word_working_copy = bit_flip_double_word(double_word_working_copy) - } - registers[rd] = double_word_working_copy - } - if (funct3 == FUNCT3_OR) && (funct7 == FUNCT7_OR) { - registers[rd] = v1 | v2 - } - if (funct3 == FUNCT3_AND) && (funct7 == FUNCT7_AND) { - registers[rd] = v1 & v2 - } - // Support variables to do not make multiplication overflow - var v1_as_u128:u128 = registers[rs1] as u128 - var v2_as_u128:u128 = registers[rs2] as u128 + switch opcode { + case OP: { - var v1_abs_as_u128:u128 = v1_abs as u128 - var v2_abs_as_u128:u128 = v2_abs as u128 + // ============================================= + // RISCV-64-I base instruction set instructions + // ============================================= - if (funct3 == FUNCT3_MUL) && (funct7 == FUNCT7_MUL) { - registers[rd] = ((v1_as_u128 * v2_as_u128) & MAX_UINT_64_AS_U128) as u64 - } + if (funct3 == FUNCT3_ADD) && (funct7 == FUNCT7_ADD) { + printf "ADD\n" + overflow::double_word_working_copy = (v1 as u65) + (v2 as u65) + registers[rd] = double_word_working_copy + } - if (funct3 == FUNCT3_MULH) && (funct7 == FUNCT7_MULH) { - var v1_times_v2_as_u128:u128 = v1_abs_as_u128 * v2_abs_as_u128 - if (v1_sign ^ v2_sign) == 1 { - // compute the complement's two negative of the result - v1_times_v2_as_u128 = (~v1_times_v2_as_u128) + 1 - } - registers[rd] = ((v1_times_v2_as_u128 >> 64) & MAX_UINT_64_AS_U128) as u64 - } + if (funct3 == FUNCT3_SUB) && (funct7 == FUNCT7_SUB) { + // we prevent underflow by pre-pending v1 with a 1 + printf "SUB\n" + overflow::double_word_working_copy = ((1 as u1)::(v1 as u64)) - (v2 as u65) + registers[rd] = double_word_working_copy + } - if (funct3 == FUNCT3_MULHSU) && (funct7 == FUNCT7_MULHSU) { - var v1_times_v2_as_u128:u128 = v1_abs_as_u128 * v2_as_u128 - if v1_sign == 1 { - // compute the complement's two negative of the result - v1_times_v2_as_u128 = (~v1_times_v2_as_u128) + 1 - } - registers[rd] = ((v1_times_v2_as_u128 >> 64) & MAX_UINT_64_AS_U128) as u64 - } + if (funct3 == FUNCT3_SLL) && (funct7 == FUNCT7_SLL) { + printf "SLL\n" + shift_discard_6::shift_amount_6 = v2 + registers[rd] = v1 << shift_amount_6 + } - if (funct3 == FUNCT3_MULHU) && (funct7 == FUNCT7_MULHU) { - registers[rd] = (((v1_as_u128 * v2_as_u128) >> 64) & MAX_UINT_64_AS_U128) as u64 - } + if (funct3 == FUNCT3_SLT) && (funct7 == FUNCT7_SLT) { + printf "SLT\n" + registers[rd] = signed_LT(v1, v2) as DoubleWord + } - if (funct3 == FUNCT3_DIV) && (funct7 == FUNCT7_DIV) { - if v2 == 0 { - registers[rd] = NEGATIVE_ONE_AS_I64 - } else if (v1 == OVERFLOW_DIVIDEND) && (v2 == NEGATIVE_ONE_AS_I64) { - registers[rd] = OVERFLOW_DIVIDEND - } else { - registers[rd] = v1_abs / v2_abs - if (v1_sign ^ v2_sign) == 1 { - registers[rd] = negative_of_double_word(registers[rd]) + if (funct3 == FUNCT3_SLTU) && (funct7 == FUNCT7_SLTU) { + printf "SLTU\n" + if (v1> shift_amount_6 } - } - } - if (funct3 == FUNCT3_REMU) && (funct7 == FUNCT7_REMU) { - if v2 == 0 { - registers[rd] = v1 - } else { - registers[rd] = v1 % v2 - } - } + if (funct3 == FUNCT3_SRA) && (funct7 == FUNCT7_SRA) { + printf "SRA\n" + shift_discard_6::shift_amount_6 = v2 + if (v1_sign == 1) { + double_word_working_copy = bit_flip_double_word(v1) + } else { + double_word_working_copy = v1 + } + double_word_working_copy = double_word_working_copy >> shift_amount_6 + if (v1_sign == 1) { + double_word_working_copy = bit_flip_double_word(double_word_working_copy) + } + registers[rd] = double_word_working_copy + } - v1_upper::v1_lower = v1 - v2_upper::v2_lower = v2 - v1_lower_abs = absolute_value_word(v1_lower) - v2_lower_abs = absolute_value_word(v2_lower) - - if (funct3 == FUNCT3_MULW) && (funct7 == FUNCT7_MULW) { - product_upper::product_lower = (v1_lower as DoubleWord) * (v2_lower as DoubleWord) - sign_bit = sign_bit_of_word(product_lower) - if (sign_bit == 1) { - registers[rd] = MAX_UINT_32::product_lower - } else { - registers[rd] = product_lower as DoubleWord - } - } + if (funct3 == FUNCT3_OR) && (funct7 == FUNCT7_OR) { + printf "OR\n" + registers[rd] = v1 | v2 + } - // signed division satisfies - // a, b ∈ Z - // a = b∙q + r - // 0 ≤ |r| < |b| - // r and a have the same sign - if (funct3 == FUNCT3_DIVW) && (funct7 == FUNCT7_DIVW) { - if (v2_lower == 0) { - registers[rd] = NEGATIVE_ONE_AS_I64 - } else { - word_wip = v1_lower_abs / v2_lower_abs - if (sign_bit_of_word(v1_lower) == sign_bit_of_word(v2_lower)) { - registers[rd] = sgn_extension_u32_u64(word_wip) - } else { - registers[rd] = sgn_extension_u32_u64(negative_of_word(word_wip)) + if (funct3 == FUNCT3_AND) && (funct7 == FUNCT7_AND) { + printf "AND\n" + registers[rd] = v1 & v2 + } + + // ========================= + // M-extension instructions + // ========================= + + // Support variables to do not make multiplication overflow + var v1_as_u128:u128 = registers[rs1] as u128 + var v2_as_u128:u128 = registers[rs2] as u128 + + var v1_abs_as_u128:u128 = v1_abs as u128 + var v2_abs_as_u128:u128 = v2_abs as u128 + + if (funct3 == FUNCT3_MUL) && (funct7 == FUNCT7_MUL) { + printf "MUL\n" + registers[rd] = ((v1_as_u128 * v2_as_u128) & MAX_UINT_64_AS_U128) as u64 + } + + if (funct3 == FUNCT3_MULH) && (funct7 == FUNCT7_MULH) { + printf "MULH\n" + var v1_times_v2_as_u128:u128 = v1_abs_as_u128 * v2_abs_as_u128 + if (v1_sign ^ v2_sign) == 1 { + // compute the complement's two negative of the result + v1_times_v2_as_u128 = (~v1_times_v2_as_u128) + 1 + } + registers[rd] = ((v1_times_v2_as_u128 >> 64) & MAX_UINT_64_AS_U128) as u64 + } + + if (funct3 == FUNCT3_MULHSU) && (funct7 == FUNCT7_MULHSU) { + printf "MULHSU\n" + var v1_times_v2_as_u128:u128 = v1_abs_as_u128 * v2_as_u128 + if v1_sign == 1 { + // compute the complement's two negative of the result + v1_times_v2_as_u128 = (~v1_times_v2_as_u128) + 1 + } + registers[rd] = ((v1_times_v2_as_u128 >> 64) & MAX_UINT_64_AS_U128) as u64 + } + + if (funct3 == FUNCT3_MULHU) && (funct7 == FUNCT7_MULHU) { + printf "MULHU\n" + registers[rd] = (((v1_as_u128 * v2_as_u128) >> 64) & MAX_UINT_64_AS_U128) as u64 + } + + if (funct3 == FUNCT3_DIV) && (funct7 == FUNCT7_DIV) { + printf "DIV\n" + if v2 == 0 { + registers[rd] = NEGATIVE_ONE_AS_I64 + } else if (v1 == OVERFLOW_DIVIDEND) && (v2 == NEGATIVE_ONE_AS_I64) { + registers[rd] = OVERFLOW_DIVIDEND + } else { + registers[rd] = v1_abs / v2_abs + if (v1_sign ^ v2_sign) == 1 { + registers[rd] = negative_of_double_word(registers[rd]) + } + } + } + + if (funct3 == FUNCT3_DIVU) && (funct7 == FUNCT7_DIVU) { + printf "DIVU\n" + if v2 == 0 { + registers[rd] = NEGATIVE_ONE_AS_I64 + } else { + registers[rd] = v1 / v2 + } + } + + if (funct3 == FUNCT3_REM) && (funct7 == FUNCT7_REM) { + printf "REM\n" + if v2 == 0 { + registers[rd] = v1 + } else if (v1 == OVERFLOW_DIVIDEND) && (v2 == NEGATIVE_ONE_AS_I64) { + registers[rd] = 0 + } else { + registers[rd] = v1_abs % v2_abs + if v1_sign == 1 { + registers[rd] = negative_of_double_word(registers[rd]) + } + } + } + + if (funct3 == FUNCT3_REMU) && (funct7 == FUNCT7_REMU) { + printf "REMU\n" + if v2 == 0 { + registers[rd] = v1 + } else { + registers[rd] = v1 % v2 + } } } - } + case OP_32: { - if (funct3 == FUNCT3_REMW) && (funct7 == FUNCT7_REMW) { - if (v2_lower == 0) { - registers[rd] = sgn_extension_u32_u64(v1_lower) - } else { - word_wip = v1_lower_abs % v2_lower_abs - if (sign_bit_of_word(v1_lower) == 0) { + // ============================================= + // RISCV-64-I base instruction set instructions + // ============================================= + + v1_upper::v1_lower = v1 + v2_upper::v2_lower = v2 + v1_lower_abs = absolute_value_word(v1_lower) + v2_lower_abs = absolute_value_word(v2_lower) + + if (funct3 == FUNCT3_ADDW) && (funct7 == FUNCT7_ADDW) { + printf "ADDW\n" + overflow::word_wip = (v1_lower as u33) + (v2_lower as u33) registers[rd] = sgn_extension_u32_u64(word_wip) - } else { - registers[rd] = sgn_extension_u32_u64(negative_of_word(word_wip)) } - } - } + if (funct3 == FUNCT3_SUBW) && (funct7 == FUNCT7_SUBW) { + printf "SUBW\n" + // underflow prevention + overflow::word_wip = ((1 as u1)::v1_lower) - (v2_lower as u33) + registers[rd] = sgn_extension_u32_u64(word_wip) + } + if (funct3 == FUNCT3_SLLW) && (funct7 == FUNCT7_SLLW) { + printf "SLLW\n" + shift_discard_5::shift_amount_5 = v2_lower + registers[rd] = sgn_extension_u32_u64(v1_lower << shift_amount_5) + } + if (funct3 == FUNCT3_SRLW) && (funct7 == FUNCT7_SRLW) { + printf "SRLW\n" + shift_discard_5::shift_amount_5 = v2_lower + registers[rd] = sgn_extension_u32_u64(v1_lower >> shift_amount_5) + } + if (funct3 == FUNCT3_SRAW) && (funct7 == FUNCT7_SRAW) { + printf "SRAW\n" + shift_discard_5::shift_amount_5 = v2_lower + if (sign_bit_of_word(v1_lower) == 1) { + word_working_copy = bit_flip_word(v1_lower) + } else { + word_working_copy = v1_lower + } + word_working_copy = word_working_copy >> shift_amount_5 + if (sign_bit_of_word(v1_lower) == 1) { + word_working_copy = bit_flip_word(word_working_copy) + } + registers[rd] = sgn_extension_u32_u64(word_working_copy) + } - if (funct3 == FUNCT3_DIVUW) && (funct7 == FUNCT7_DIVUW) { - if (v2_lower == 0) { - registers[rd] = NEGATIVE_ONE_AS_I64 - } else { - registers[rd] = sgn_extension_u32_u64(v1_lower / v2_lower) - } - } - if (funct3 == FUNCT3_REMUW) && (funct7 == FUNCT7_REMUW) { - if (v2_lower == 0) { - registers[rd] = sgn_extension_u32_u64(v1_lower) - } else { - registers[rd] = sgn_extension_u32_u64(v1_lower % v2_lower) + // ============================================== + // RISCV-64 M-extension instruction instructions + // ============================================== + + if (funct3 == FUNCT3_MULW) && (funct7 == FUNCT7_MULW) { + printf "MULW\n" + product_upper::product_lower = (v1_lower as DoubleWord) * (v2_lower as DoubleWord) + sign_bit = sign_bit_of_word(product_lower) + if (sign_bit == 1) { + registers[rd] = MAX_UINT_32::product_lower + } else { + registers[rd] = product_lower as DoubleWord + } + } + + // signed division satisfies + // a, b ∈ Z + // a = b∙q + r + // 0 ≤ |r| < |b| + // r and a have the same sign + if (funct3 == FUNCT3_DIVW) && (funct7 == FUNCT7_DIVW) { + printf "DIVW\n" + if (v2_lower == 0) { + registers[rd] = NEGATIVE_ONE_AS_I64 + } else { + word_wip = v1_lower_abs / v2_lower_abs + if (sign_bit_of_word(v1_lower) == sign_bit_of_word(v2_lower)) { + registers[rd] = sgn_extension_u32_u64(word_wip) + } else { + registers[rd] = sgn_extension_u32_u64(negative_of_word(word_wip)) + } + } + } + + if (funct3 == FUNCT3_DIVUW) && (funct7 == FUNCT7_DIVUW) { + printf "DIVUW\n" + if (v2_lower == 0) { + registers[rd] = NEGATIVE_ONE_AS_I64 + } else { + registers[rd] = sgn_extension_u32_u64(v1_lower / v2_lower) + } + } + + if (funct3 == FUNCT3_REMW) && (funct7 == FUNCT7_REMW) { + printf "REMW\n" + if (v2_lower == 0) { + registers[rd] = sgn_extension_u32_u64(v1_lower) + } else { + word_wip = v1_lower_abs % v2_lower_abs + if (sign_bit_of_word(v1_lower) == 0) { + registers[rd] = sgn_extension_u32_u64(word_wip) + } else { + registers[rd] = sgn_extension_u32_u64(negative_of_word(word_wip)) + } + } + } + + if (funct3 == FUNCT3_REMUW) && (funct7 == FUNCT7_REMUW) { + printf "REMUW\n" + if (v2_lower == 0) { + registers[rd] = sgn_extension_u32_u64(v1_lower) + } else { + registers[rd] = sgn_extension_u32_u64(v1_lower % v2_lower) + } + } } - } - if (funct3 == FUNCT3_ADDW) && (funct7 == FUNCT7_ADDW) { - overflow::word_wip = (v1_lower as u33) + (v2_lower as u33) - registers[rd] = sgn_extension_u32_u64(word_wip) - } - if (funct3 == FUNCT3_SUBW) && (funct7 == FUNCT7_SUBW) { - // underflow prevention - overflow::word_wip = ((1 as u1)::v1_lower) - (v2_lower as u33) - registers[rd] = sgn_extension_u32_u64(word_wip) - } - if (funct3 == FUNCT3_SLLW) && (funct7 == FUNCT7_SLLW) { - shift_discard_5::shift_amount_5 = v2_lower - registers[rd] = sgn_extension_u32_u64(v1_lower << shift_amount_5) - } - if (funct3 == FUNCT3_SRLW) && (funct7 == FUNCT7_SRLW) { - shift_discard_5::shift_amount_5 = v2_lower - registers[rd] = sgn_extension_u32_u64(v1_lower >> shift_amount_5) - } - if (funct3 == FUNCT3_SRAW) && (funct7 == FUNCT7_SRAW) { - shift_discard_5::shift_amount_5 = v2_lower - if (sign_bit_of_word(v1_lower) == 1) { - word_working_copy = bit_flip_word(v1_lower) - } else { - word_working_copy = v1_lower + case CUSTOM_0: { + + // ========================================== + // custom instructions (precompiles etc ...) + // ========================================== + + if (funct3 == FUNCT3_POSEIDON_1) && (funct7 == FUNCT7_POSEIDON_1) { + printf "POSEIDON precompile\n" + fail + } } - word_working_copy = word_working_copy >> shift_amount_5 - if (sign_bit_of_word(v1_lower) == 1) { - word_working_copy = bit_flip_word(word_working_copy) + default: { + printf "unsupported R-type instruction with opcode %x", opcode + fail } - registers[rd] = sgn_extension_u32_u64(word_working_copy) } } diff --git a/arithmetization/src/main/riscv/interpreter.zkc b/arithmetization/src/main/riscv/interpreter.zkc index 5c8c49a695c..cb7311bf702 100644 --- a/arithmetization/src/main/riscv/interpreter.zkc +++ b/arithmetization/src/main/riscv/interpreter.zkc @@ -17,8 +17,8 @@ fn interpreter(instruction:u32, pc:Address) -> (new_pc:Address) printf "instruction %b\n", instruction printf "opcode: %b\n", opcode - printf "parameters: %b\n", instruction_parameters printf "type: %b\n", instruction_type + printf "parameters: %b\n", instruction_parameters // printf "[SP before execution] : %x\n", registers[2] @@ -28,7 +28,7 @@ fn interpreter(instruction:u32, pc:Address) -> (new_pc:Address) // TODO: switch if instruction_type == R_TYPE { printf "R-Type instruction\n" - process_R_type_instruction(instruction_parameters) + process_R_type_instruction(opcode, instruction_parameters) new_pc = pc + 4 as Address } else if instruction_type == I_TYPE { printf "I-Type instruction\n" diff --git a/arithmetization/src/main/riscv/utils/constants.zkc b/arithmetization/src/main/riscv/utils/constants.zkc index 0e72b7a4ca0..e7ea29f27ca 100644 --- a/arithmetization/src/main/riscv/utils/constants.zkc +++ b/arithmetization/src/main/riscv/utils/constants.zkc @@ -25,7 +25,7 @@ static instruction_type_from_opcode(opcode:Opcode) -> (instruction_type:Type) { UNDEFINED_TYPE, // 0b0001000 UNDEFINED_TYPE, // 0b0001001 UNDEFINED_TYPE, // 0b0001010 - UNDEFINED_TYPE, // 0b0001011 + R_TYPE, // 0b0001011 NOTE: this is the custom-0 instruction opcode (0x0b) UNDEFINED_TYPE, // 0b0001100 UNDEFINED_TYPE, // 0b0001101 UNDEFINED_TYPE, // 0b0001110 @@ -147,6 +147,7 @@ static instruction_type_from_opcode(opcode:Opcode) -> (instruction_type:Type) { // R_type const OP:Opcode = 0b0110011 // ADD, SUB, SLL, SLT, SLTU, XOR, SRL, SRA, OR, AND const OP_32:Opcode = 0b0111011 // ADDW, SUBW, SLLW, SRLW, SRAW (RV64 only) +const CUSTOM_0:Opcode = 0b0001011 // for precompiles // I_type const LOAD:Opcode = 0b0000011 // LB, LH, LW, LBU, LHU, LWU, LD @@ -215,6 +216,9 @@ const FUNCT3_DIVUW:Funct3 = 0b101, FUNCT7_DIVUW:Funct7 = 0b0000001 const FUNCT3_REMW:Funct3 = 0b110, FUNCT7_REMW:Funct7 = 0b0000001 const FUNCT3_REMUW:Funct3 = 0b111, FUNCT7_REMUW:Funct7 = 0b0000001 +// CUSTOM_0 (0001011) — R-type precompiles +const FUNCT3_POSEIDON_1:Funct3 = 0b111, FUNCT7_POSEIDON_1:Funct7 = 0b1111111 + // ====================== // I-type funct3 values // ====================== @@ -283,4 +287,4 @@ const U64_FIRST_BIT_MASK:u64 = 0x8000000000000000 const OVERFLOW_DIVIDEND:u64 = 0x8000000000000000 const NEGATIVE_ONE_AS_I64:u64 = 0xffffffffffffffff -const MASK_64_ERASE_LAST_BIT:u64 = 0xfffffffffffffffe \ No newline at end of file +const MASK_64_ERASE_LAST_BIT:u64 = 0xfffffffffffffffe From d601d28e91dc38a8f7d09913a876e905360bad90 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 22:30:11 +0200 Subject: [PATCH 04/11] feat: use switch statements in instrution processing --- .../riscv/instruction_processing/b_type.zkc | 77 ++++--- .../riscv/instruction_processing/i_type.zkc | 212 +++++++++++------- .../riscv/instruction_processing/j_type.zkc | 1 + .../riscv/instruction_processing/s_type.zkc | 4 + .../riscv/instruction_processing/u_type.zkc | 6 + arithmetization/src/main/riscv/main.zkc | 1 + 6 files changed, 181 insertions(+), 120 deletions(-) diff --git a/arithmetization/src/main/riscv/instruction_processing/b_type.zkc b/arithmetization/src/main/riscv/instruction_processing/b_type.zkc index c91912f16d6..6ae9e6b9a9e 100644 --- a/arithmetization/src/main/riscv/instruction_processing/b_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/b_type.zkc @@ -60,49 +60,54 @@ fn process_B_type_instruction(instruction_parameters:u25, pc:Address) imm = (imm_11::imm_10_5::imm_4_1::(0 as u1)) as DoubleWord } - // TODO: question @david: providing a default value to overwrite later on seems like it would - // trigger a second row just to overwrite the original value. Is that correct, and if so - // should it be avoided _a priori_ ? - // - // default case + // "no branching" value of pc_new; + // gets overwritten if branching occurs pc_new = pc + 4 - if funct3 == FUNCT3_BEQ { - if registers[rs1] == registers[rs2] { - // the branch case - pc_new = signed_sum_of_double_word(pc, imm) + switch funct3 { + case FUNCT3_BEQ: { + printf "BEQ\n" + if registers[rs1] == registers[rs2] { + // the branch case + pc_new = signed_sum_of_double_word(pc, imm) + } } - } - if funct3 == FUNCT3_BNE { - if registers[rs1] != registers[rs2] { - // the branch case - pc_new = signed_sum_of_double_word(pc, imm) + case FUNCT3_BNE: { + printf "BNE\n" + if registers[rs1] != registers[rs2] { + // the branch case + pc_new = signed_sum_of_double_word(pc, imm) + } } - } - if funct3 == FUNCT3_BLT { - comparison = signed_LT(registers[rs1], registers[rs2]) - if comparison == 1 { - // the branch case - pc_new = signed_sum_of_double_word(pc, imm) + case FUNCT3_BLT: { + printf "BLT\n" + comparison = signed_LT(registers[rs1], registers[rs2]) + if comparison == 1 { + // the branch case + pc_new = signed_sum_of_double_word(pc, imm) + } } - } - if funct3 == FUNCT3_BGE { - comparison = signed_LT(registers[rs1], registers[rs2]) - if comparison == 0 { - // the branch case - pc_new = signed_sum_of_double_word(pc, imm) + case FUNCT3_BGE: { + printf "BGE\n" + comparison = signed_LT(registers[rs1], registers[rs2]) + if comparison == 0 { + // the branch case + pc_new = signed_sum_of_double_word(pc, imm) + } } - } - if funct3 == FUNCT3_BLTU { - if registers[rs1]= registers[rs2] { - // the branch case - pc_new = signed_sum_of_double_word(pc, imm) + case FUNCT3_BGEU: { + printf "BGEU\n" + if registers[rs1] >= registers[rs2] { + // the branch case + pc_new = signed_sum_of_double_word(pc, imm) + } } } } diff --git a/arithmetization/src/main/riscv/instruction_processing/i_type.zkc b/arithmetization/src/main/riscv/instruction_processing/i_type.zkc index 6e69eb3a783..173fad26d3b 100644 --- a/arithmetization/src/main/riscv/instruction_processing/i_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/i_type.zkc @@ -54,105 +54,149 @@ fn process_I_type_instruction(opcode:Opcode, instruction_paramet var signext_imm12_64:DoubleWord = sgn_extension_u12_u64(imm12) var mem_address:Address = signed_sum_of_double_word(registers[rs1], signext_imm12_64) as Address - new_pc = (pc + 4) as Address //TODO: this is the default case, we will overwrite it for JALR. + //TODO: this is the default case, we will overwrite it for JALR. // We should handle this differently to avoid a potential second row just to overwrite the value of new_pc? + new_pc = (pc + 4) as Address - // ----- LOAD (opcode LOAD) ----- - if opcode == LOAD { - if funct3 == FUNCT3_LB { - registers[rd] = sgn_extension_u8_u64(ram[mem_address]) - } - if funct3 == FUNCT3_LH { - registers[rd] = sgn_extension_u16_u64(read_16(mem_address)) - } - if funct3 == FUNCT3_LW { - registers[rd] = sgn_extension_u32_u64(read_32(mem_address)) - } - if funct3 == FUNCT3_LBU { - registers[rd] = ram[mem_address] as DoubleWord - } - if funct3 == FUNCT3_LHU { - registers[rd] = read_16(mem_address) as DoubleWord - } - if funct3 == FUNCT3_LWU { - registers[rd] = read_32(mem_address) as DoubleWord - } - if funct3 == FUNCT3_LD { - registers[rd] = read_64(mem_address) as DoubleWord + switch opcode { + + // =============================== + // ----- LOAD (opcode LOAD) ----- + // =============================== + + case LOAD: { + switch funct3 { + case FUNCT3_LB: { + printf "LB\n" + registers[rd] = sgn_extension_u8_u64(ram[mem_address]) + } + case FUNCT3_LH: { + printf "LH\n" + registers[rd] = sgn_extension_u16_u64(read_16(mem_address)) + } + case FUNCT3_LW: { + printf "LW\n" + registers[rd] = sgn_extension_u32_u64(read_32(mem_address)) + } + case FUNCT3_LBU: { + printf "LBU\n" + registers[rd] = ram[mem_address] as DoubleWord + } + case FUNCT3_LHU: { + printf "LHU\n" + registers[rd] = read_16(mem_address) as DoubleWord + } + case FUNCT3_LWU: { + printf "LWU\n" + registers[rd] = read_32(mem_address) as DoubleWord + } + case FUNCT3_LD: { + printf "LD\n" + registers[rd] = read_64(mem_address) as DoubleWord + } + } } - } - // ----- OP-IMM (opcode OP_IMM) ----- - else if opcode == OP_IMM { + // =================================== + // ----- OP-IMM (opcode OP_IMM) ----- + // =================================== - if funct3 == FUNCT3_ADDI { - registers[rd] = signed_sum_of_double_word(registers[rs1], signext_imm12_64) as DoubleWord - } else if funct3 == FUNCT3_SLTI { - var is_lt:Boolean = signed_LT(registers[rs1], signext_imm12_64) - if is_lt == 1 { - registers[rd] = 1 - } else { - registers[rd] = 0 + case OP_IMM: { + if funct3 == FUNCT3_ADDI { + printf "ADDI\n" + registers[rd] = signed_sum_of_double_word(registers[rs1], signext_imm12_64) as DoubleWord + } else if funct3 == FUNCT3_SLTI { + printf "SLTI\n" + var is_lt:Boolean = signed_LT(registers[rs1], signext_imm12_64) + if is_lt == 1 { + registers[rd] = 1 + } else { + registers[rd] = 0 + } + } else if funct3 == FUNCT3_SLTIU { + printf "SLTIU\n" + // Warn: this is an unsigned comparison (even if imm12 is SGN_EXT) + if registers[rs1]> uimm6 + } else if (funct3 == FUNCT3_SRAI) && (funct6 == FUNCT6_SRAI) { + printf "SRAI\n" + registers[rd] = _ashr_u64(registers[rs1], uimm6) } - } else if funct3 == FUNCT3_SLTIU { - // Warn: this is an unsigned comparison (even if imm12 is SGN_EXT) - if registers[rs1]> uimm5) + } else if (funct3 == FUNCT3_SRAIW) && (funct7 == FUNCT7_SRAIW) { + printf "SRAIW\n" + registers[rd] = sgn_extension_u32_u64(_ashr_u32(registers[rs1], uimm5)) } - } else if funct3 == FUNCT3_XORI { - registers[rd] = registers[rs1] ^ signext_imm12_64 - } else if funct3 == FUNCT3_ORI { - registers[rd] = registers[rs1] | signext_imm12_64 - } else if funct3 == FUNCT3_ANDI { - registers[rd] = registers[rs1] & signext_imm12_64 - } else if (funct3 == FUNCT3_SLLI) && (funct6 == FUNCT6_SLLI) { - registers[rd] = registers[rs1] << uimm6 - } else if (funct3 == FUNCT3_SRLI) && (funct6 == FUNCT6_SRLI) { - registers[rd] = registers[rs1] >> uimm6 - } else if (funct3 == FUNCT3_SRAI) && (funct6 == FUNCT6_SRAI) { - registers[rd] = _ashr_u64(registers[rs1], uimm6) } - } - // ----- OP-IMM-32 (opcode OP_IMM_32) — RV64 *W ----- - else if opcode == OP_IMM_32 { - if funct3 == FUNCT3_ADDIW { - registers[rd] = sgn_extension_u32_u64((signed_sum_of_double_word(registers[rs1], signext_imm12_64) & MAX_UINT_32_AS_U64) as Word) - } else if (funct3 == FUNCT3_SLLIW) && (funct7 == FUNCT7_SLLIW) { - registers[rd] = sgn_extension_u32_u64(((registers[rs1] & MAX_UINT_32_AS_U64) as Word) << uimm5) - } else if (funct3 == FUNCT3_SRLIW) && (funct7 == FUNCT7_SRLIW) { - registers[rd] = sgn_extension_u32_u64(((registers[rs1] & MAX_UINT_32_AS_U64) as Word) >> uimm5) - } else if (funct3 == FUNCT3_SRAIW) && (funct7 == FUNCT7_SRAIW) { - registers[rd] = sgn_extension_u32_u64(_ashr_u32(registers[rs1], uimm5)) + // ================= + // ----- JALR ----- + // ================= + + case JALR: { + printf "JALR\n" + // only instruction is JALR, no need to switch over funct3 + new_pc = (signed_sum_of_double_word(registers[rs1], signext_imm12_64) & MASK_64_ERASE_LAST_BIT) as Address + registers[rd] = (pc + 4) as DoubleWord } - } - else if opcode == JALR { - // only instruction is JALR, no need to switch over funct3 - new_pc = (signed_sum_of_double_word(registers[rs1], signext_imm12_64) & MASK_64_ERASE_LAST_BIT) as Address - registers[rd] = (pc + 4) as DoubleWord - } + // =================== + // ----- SYSTEM ----- + // =================== - else if opcode == SYSTEM { - // note: same funct3 for ECALL and EBREAK - if funct3 == FUNCT3_ECALL { - // imm12 is interpreted as funct12 for SYSTEM opcode - if imm12 == FUNCT12_ECALL { - // Note: as we don't fully support CSR, we use ECALL as generic STOP instruction for now - new_pc = MAX_UINT_64 // set the stop signal to end the program execution - } else if imm12 == FUNCT12_EBREAK { - printf "[ERROR] EBREAK instruction triggered\n" + case SYSTEM: { + // note: same funct3 for ECALL and EBREAK + if funct3 == FUNCT3_ECALL { + printf "ECALL\n" + // imm12 is interpreted as funct12 for SYSTEM opcode + if imm12 == FUNCT12_ECALL { + // Note: as we don't fully support CSR, we use ECALL as generic STOP instruction for now + new_pc = MAX_UINT_64 // set the stop signal to end the program execution + } else if imm12 == FUNCT12_EBREAK { + printf "[ERROR] EBREAK instruction triggered\n" + } + } else { + printf "[ERROR] SYSTEM instruction with funct3 %b has been triggered, not implemented\n", funct3 } - } else { - printf "[ERROR] SYSTEM instruction with funct3 %b\n has been triggered, not implemented", funct3 } - } - // TODO: should never be reached - else { - fail + // TODO: should never be reached + default: { + fail + } } } diff --git a/arithmetization/src/main/riscv/instruction_processing/j_type.zkc b/arithmetization/src/main/riscv/instruction_processing/j_type.zkc index 641e5505f79..402a3082739 100644 --- a/arithmetization/src/main/riscv/instruction_processing/j_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/j_type.zkc @@ -43,6 +43,7 @@ fn process_J_type_instruction(instruction_parameters:u25, pc:Address) // restructure and 1 left shift the immediate to get imm21 var imm21:u21 = ((imm20::imm19_12::imm11::imm10_1) as u21) << 1 + printf "JAL\n" registers[rd] = signed_sum_of_double_word(pc, 4) pc_new = signed_sum_of_double_word(pc, sgn_extension_u21_u64(imm21)) as Address } diff --git a/arithmetization/src/main/riscv/instruction_processing/s_type.zkc b/arithmetization/src/main/riscv/instruction_processing/s_type.zkc index 1a6592b6360..3c5b130b5b5 100644 --- a/arithmetization/src/main/riscv/instruction_processing/s_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/s_type.zkc @@ -57,21 +57,25 @@ fn process_S_type_instruction(instruction_parameters:u25) { var mem_address:Address = signed_sum_of_double_word(registers[rs1], signext_imm12_64) as Address if funct3 == FUNCT3_SB { + printf "SB\n" // Store byte (u8) write_8(mem_address, (registers[rs2] & (0xFF as u64)) as u8) } if funct3 == FUNCT3_SH { + printf "SH\n" // Store halfword (u16) write_16(mem_address, (registers[rs2] & (0xFFFF as u64)) as u16) } if funct3 == FUNCT3_SW { + printf "SW\n" // Store word (u32) write_32(mem_address, (registers[rs2] & (0xFFFFFFFF as u64)) as u32) } if funct3 == FUNCT3_SD { + printf "SD\n" // Store doubleword (u64) write_64(mem_address, registers[rs2]) } diff --git a/arithmetization/src/main/riscv/instruction_processing/u_type.zkc b/arithmetization/src/main/riscv/instruction_processing/u_type.zkc index b70f8fa2b66..99d477f1188 100644 --- a/arithmetization/src/main/riscv/instruction_processing/u_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/u_type.zkc @@ -41,7 +41,13 @@ fn process_U_type_instruction(opcode:Opcode, instruction_parameters:u tmp = sgn_extension_u32_u64(((imm20 as u32) << 12) as u32) if opcode == AUIPC { + printf "AUIPC\n" tmp = signed_sum_of_double_word(tmp, pc) as DoubleWord + } else if opcode == LUI { + printf "LUI\n" + } else { + printf "Unsupported instruction of U-Type\n" + fail } // Note: the definition of tmp already works for the LUI opcode diff --git a/arithmetization/src/main/riscv/main.zkc b/arithmetization/src/main/riscv/main.zkc index e00e042bfe7..c3009ddd273 100644 --- a/arithmetization/src/main/riscv/main.zkc +++ b/arithmetization/src/main/riscv/main.zkc @@ -32,6 +32,7 @@ fn main() { } printf "program length=%d\n", program_len + printf "===========\n" // We interpret pc == MAX_UINT_64 as the stop signal, which is set by the ecall instruction while pc != MAX_UINT_64 { From 8bc8c5508f764ef36448475c647c70caa8448063 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 22:33:10 +0200 Subject: [PATCH 05/11] feat: use switch statement in interpreter --- .../src/main/riscv/interpreter.zkc | 60 ++++++++++--------- 1 file changed, 32 insertions(+), 28 deletions(-) diff --git a/arithmetization/src/main/riscv/interpreter.zkc b/arithmetization/src/main/riscv/interpreter.zkc index cb7311bf702..a6fb8f3e0d9 100644 --- a/arithmetization/src/main/riscv/interpreter.zkc +++ b/arithmetization/src/main/riscv/interpreter.zkc @@ -20,39 +20,43 @@ fn interpreter(instruction:u32, pc:Address) -> (new_pc:Address) printf "type: %b\n", instruction_type printf "parameters: %b\n", instruction_parameters - // printf "[SP before execution] : %x\n", registers[2] - // TODO: handle the case where rd = 0: we will handle this in RAM itself, likely by adding an extra read-write pair // to reset the value in registers[rd] to 0 - // TODO: switch - if instruction_type == R_TYPE { - printf "R-Type instruction\n" - process_R_type_instruction(opcode, instruction_parameters) - new_pc = pc + 4 as Address - } else if instruction_type == I_TYPE { - printf "I-Type instruction\n" - new_pc = process_I_type_instruction(opcode, instruction_parameters, pc) - } else if instruction_type == S_TYPE { - printf "S-Type instruction\n" - process_S_type_instruction(instruction_parameters) - new_pc = pc + 4 as Address - } else if instruction_type == B_TYPE { - printf "B-Type instruction\n" - new_pc = process_B_type_instruction(instruction_parameters, pc) - } else if instruction_type == U_TYPE { - printf "U-Type instruction\n" - process_U_type_instruction(opcode, instruction_parameters, pc) - new_pc = pc + 4 as Address - } else if instruction_type == J_TYPE { - printf "J-Type instruction\n" - new_pc = process_J_type_instruction(instruction_parameters, pc) - } else { - fail + switch instruction_type { + case R_TYPE: { + printf "R-Type instruction\n" + process_R_type_instruction(opcode, instruction_parameters) + new_pc = pc + 4 as Address + } + case I_TYPE: { + printf "I-Type instruction\n" + new_pc = process_I_type_instruction(opcode, instruction_parameters, pc) + } + case S_TYPE: { + printf "S-Type instruction\n" + process_S_type_instruction(instruction_parameters) + new_pc = pc + 4 as Address + } + case B_TYPE: { + printf "B-Type instruction\n" + new_pc = process_B_type_instruction(instruction_parameters, pc) + } + case U_TYPE: { + printf "U-Type instruction\n" + process_U_type_instruction(opcode, instruction_parameters, pc) + new_pc = pc + 4 as Address + } + case J_TYPE: { + printf "J-Type instruction\n" + new_pc = process_J_type_instruction(instruction_parameters, pc) + } + default: { + printf "Unsupported instrution type %d\n", instruction_type + fail + } } - // printf "[SP after execution] : %x\n", registers[2] - printf "-----------\n" } From a2dbbcba98cb0f44e39b9e40ae5542c7bca5b895 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 22:35:20 +0200 Subject: [PATCH 06/11] feat: poseidon wip --- .../src/test/examples/rust/Cargo.toml | 4 + .../test/examples/rust/{ => src}/poseidon1.rs | 27 +-- .../src/test/poseidon/poseidon1.zkc | 227 +++++++++--------- .../src/test/poseidon/test/poseidon1_01.zkc | 6 +- arithmetization/src/test/poseidon/utils.zkc | 10 +- 5 files changed, 139 insertions(+), 135 deletions(-) rename arithmetization/src/test/examples/rust/{ => src}/poseidon1.rs (92%) diff --git a/arithmetization/src/test/examples/rust/Cargo.toml b/arithmetization/src/test/examples/rust/Cargo.toml index d6bef6249b8..a3020cd064e 100644 --- a/arithmetization/src/test/examples/rust/Cargo.toml +++ b/arithmetization/src/test/examples/rust/Cargo.toml @@ -12,6 +12,10 @@ path = "src/blake.rs" name = "test" path = "src/test.rs" +[[bin]] +name = "poseidon1" +path = "src/poseidon1.rs" + [profile.release] opt-level = 2 debug = false diff --git a/arithmetization/src/test/examples/rust/poseidon1.rs b/arithmetization/src/test/examples/rust/src/poseidon1.rs similarity index 92% rename from arithmetization/src/test/examples/rust/poseidon1.rs rename to arithmetization/src/test/examples/rust/src/poseidon1.rs index 342cf3f7b48..d7efd8c68b8 100644 --- a/arithmetization/src/test/examples/rust/poseidon1.rs +++ b/arithmetization/src/test/examples/rust/src/poseidon1.rs @@ -20,20 +20,13 @@ /// mds_matrix ≡ 0x07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a5bf72c2447f777784dd6b5ae10eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a5bf72c2447f7777863c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a5bf72c243a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f77164924a34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed41da12f739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d5ccec4ed58e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555566fc28f5d468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c859159f555560fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd17462c2c8591489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf33334428618621cdd174669d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf333344286186232cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af2876bf333341fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c72281af28754aaaaab1fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f123471c723f80000054aaaaab1fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f000000ef0f0f17f0000003f80000054aaaaab1fc0000032cccccd69d55556489249250fe00000468e38e458e6666739ba2e8c34eaaaab3a9d89d963c9249310eeeeef07f00000 /// roundconstants ≡ 0x7ee56a481136704512e419417ebbc12b1970b7d5662b60e83e4990c6679f91f5350813bb00874ad428a0081a18fa58725f25b0715e5d59985e6fd3e75b2e26606f1837bf3fe6182b1edd7ac557470d0043d486d51982c70f0ea53af961d6165b51639c002dec352c2950e5312d2cb94708256cef1a0109f61f51faf35cef1c623d65e50e33d91626133d5a1e0ff49b0d38900cd12c22cc3f28852bb206c65a027b2cf7bc68016e1a15e16bc05248149a6dd212a018d6830a5001be8264dac34e5902b287426583a00c9216323fe028a5245f8e4943bb297e7873dbd93cc987df286bb4ce640a8dcd512a8e3603a4cf55481837a203d6da8473726ac7760e7fdf54dfeb5d7d40afd6722cb316106a457345a7ccdb44061375154077a545744faa4eb5e5ee3794e83f47c7093c5694903c69cb6299373df84c46a0df5846b8758a3241ebcb0b09d2331af423571e66cec243e7dc24259a5d6127e85a3b1b9133fa343e5628485cd4c216e269f5165b60c625f683d9124f81f9174331f977344dc55a821dba5fc4177f54153bf55e3f11943bdbf191088c84a368256c9b3c90bbc66846166a03f4238d463335fb5e3d35516e59ae6f32d06cc0596293f36c87edb208fc60b534bcca8024f007f362731c6f1e1db6c60ca409bb585c1e7856e94edc16d2273418e114677b2c3730770075e435d1b18c22be3db54fb1fbb7477cb3ed7d5311c65b62ae7d559c5fa877f150483211570b490fef6a77ec311f2247171b4e0ac7112edf69c93b5a8850658094215619b4aa362019a76bf9d4ed5b413dff617e181e5e7ab57b33ad78333466c7ca6488dff471f068f4056e891f04f1eccc663257d5671e31b95871987c280c109e2a227761350a25e95b91b1c47a0735460182627053a677200ed4b07434cf0c4e6e751e8829bd5f5949ec32df7693452b3cf09e586ba0e2bf7ab93acf3ce597df536e3d42147a808d5e32eb565a203323509657666d44b7c56698636a57b84f9f554b61b96da0ab281585b6ac6705a2b4152872f60f4409fd23a9dd606f2b18d465ac9fd42f0efbea591e67fd217ca19b469c90ca03d60ef54ea7857e07c86a4f288ed4612fe51b227e2936142c4beb855b0b7d111e17dff6089beae10a5acf1a2fc33d8f60422dc66e1dc939635351b955522fc03eb94ef72a24a65c2e139c765139114478cc0742579538f944de9aae3c2f1e2e195747be2496339c650b2e39528996656cb355580f461c1c70f6b2703faaa36f62e3348a672167cb394c880b2a46ba8263ffb74a1cf875d653d12772036a45523bdd9f2b02f72c2402b6006c077fe1581f9d6ea420904d6f5d6534fa066d89746198f1f426301ab441f274c200eac15c28b54b472339739d48c6281c4ed935fc3f9187fa4a1930a63ad4d7360f3f1889635a388f2862c145277ed1e84db23cad1f1b11f51f3dba2b1c26eb4e0f7f55466cd024b067c47902793b89000e8a283c4590b7ea6f567a2b5dc9730015247bc650567fcb133eff84547dc2ef34eb3dbb1240231766c6ae49174338b6242510081b514927062d98d67af30bbc26af15e870d907a35dfc5cac731f27ec53aa7d3f63ab0ec6216053f418796b3919156afd5eea69736704c6a90dce002b331169c0714d71783ddaffaf7e46495720ca59ea679820c942ef21a1798ea08914a74fa30c06cf186a4c8d52620f6d812220901a5277bb90230bf95e0ad8847a5e96e8b677b4056e70a50d2c5f0eed593646c4df10eb9a8721eed6b7534add366e3e74212b25810e1d8f707b45318a1a677f8ff20258c9e04cd02a002e24ff15634a715d4ac01e59601511e126e9c01a4c165c6e57cd11403ac6543b6787d847037dfbf96dd9d0794d24b2812a6f407d0131df8e4b8a7896237008582cf5e53412aafc3f54568d031a2507355331686d4ce76d91799c1a8c2b7a8ac960aee67274f7421c3c42146d26d369c54ae54a127eea16d15ce3eae869f28994262b8642610d4cc45e1af21c1a8526d0316b127b3576fe5d02d968a04ba00f5140bed993377fb9077859216e1931d9d153b0934e71914ff74eabae6c7196468e164b3cc258cb66c04c1473076b3afccd4236518b4ad85605291382e11e89b6cf5e16c3a82e6759212430095405e555c378880a24763a31254f53b24018b7fa432bbe8a731c9a12f23f6fd40d0e1d4ec41361c64d09a8f47003d23a40109ad29028c2fb883b6498f274d8be576a4277d218c2b3d46252c30c07cc2560209fe15b52a55fac4df19eb7025211165e414ff13cd9a1f4005aad1527a53f0072bbe9cb71d8bd7d4194b79a48e87a723341553c63d34faa132a01e33833e2d949726e04054957f87b71bce473eec57d556e55331fa93fde346a8ca81162dfde5c30d028094a42943052dcda3798849851f06b97658487797599b0d4436fdabc66c5b77d40c86a9e27e7055b6d0dd9d87e5598b51a4d04f35e3b2bc7533b5b2f3e33a125664d71ce382e6c2a24c4eb6e13f246f707e2d7ef -const INPUT_STRING = "000102030405060708090a0b0c0d0e0f"; -const OUPUT_STRING = "00"; // TODO +const INPUT_STRING :&str = "000102030405060708090a0b0c0d0e0f"; +const OUPUT_STRING :&str = "00"; // TODO +const INPUT_LENGTH :usize = 16; // length in bytes of the input string +const OUTPUT_SIZE :usize = 1; // number of output field elements, has to be ≤ rate -/// Poseidon1 function call -/// -/// zkc-test poseidon1.rs - -// use core::convert::TryInto; -// use core::result::Result; -// use core::result::Result::Err; -// use core::result::Result::Ok; - -const INPUT_LENGTH = 16; // length in bytes of the input string -const OUTPUT_SIZE = 1; // number of output field elements, has to be ≤ rate +const FUNCT3_POSEIDON_1 :u8 = 0b111; +const FUNCT7_POSEIDON_1 :u8 = 0b1111111; core::arch::global_asm!( @@ -44,14 +37,14 @@ core::arch::global_asm!( ); -fn poseidon_1(input_offset :u64, input_size :u64, output_offset :u64) { +fn some_crap(input_offset :usize, input_size :usize, output_offset :usize) { unsafe { core::arch::asm!( // interpretation of ":insn r 0x0b, 0x42, 0x69, {2}, {0}, {1}", // // instruction type: r // opcode: 0x0b ≡ custom-0 - // funct3: 0x42 + // funct3: 0x01 // funct7: 0x69 // // {0} = register address holding io @@ -59,7 +52,7 @@ fn poseidon_1(input_offset :u64, input_size :u64, output_offset :u64) { // {2} = register address holding ro // // order is decided by the declaration order of the in(reg) XXX - ":insn r 0x0b, 0x42, 0x69, {2}, {0}, {1}", + ".insn r 0x0b, 0b111, 0b1111111, {2}, {0}, {1}", in(reg) input_offset, in(reg) input_size, in(reg) output_offset, @@ -81,7 +74,7 @@ fn main() -> ! { let input = hex_to_input(INPUT_STRING); - poseidon_1(&input, len(input), 0); + some_crap(input.as_ptr() as usize, input.len(), 0); // Encode the 5 codes into a single exit code (e.g. 0000 for all pass, 1000 for 1st test failing, etc.) exit(0); diff --git a/arithmetization/src/test/poseidon/poseidon1.zkc b/arithmetization/src/test/poseidon/poseidon1.zkc index edbd697dd77..68abf258fa7 100644 --- a/arithmetization/src/test/poseidon/poseidon1.zkc +++ b/arithmetization/src/test/poseidon/poseidon1.zkc @@ -15,38 +15,37 @@ include "../../main/riscv/ram/write.zkc" // One notable feature of this implementation is that the length // of the message is included in the state at initialization time. - -memory state (index :u8) -> (st :u32) -memory state_copy (index :u8) -> (st :u32) +memory state(index:u8) -> (st:u32) +memory state_copy(index:u8) -> (st:u32) // round_constants is a matrix with TOTAL_ROUNDS many rows and STATE_WIDTH many columns // mds_matrix is a square matrix of format STATE_WIDTH × STATE_WIDTH -input round_constants (index :u16) -> (rc :u32) -input mds_matrix (index :u16) -> (md :u32) +input round_constants(index:u16) -> (rc:u32) +input mds_matrix(index:u16) -> (md:u32) // this implementation does not use the native field element type yet -const KOALABEAR_PRIME :u32 = 0x7F000001 // 2^31 - 2^24 + 1 or 2130706433 -const ALPHA :u2 = 3 -const BYTES_PER_FELT :u8 = 3 +const KOALABEAR_PRIME:u32 = 0x7F000001 // 2^31 - 2^24 + 1 or 2130706433 +const ALPHA:u2 = 3 +const BYTES_PER_FELT:u8 = 3 -const OUTPUT_LENGTH :u8 = RATE // OUTPUT_LENGTH ≤ RATE is required +const OUTPUT_LENGTH:u8 = RATE // OUTPUT_LENGTH ≤ RATE is required -const STATE_WIDTH :u8 = RATE + CAPACITY -const RATE :u8 = 15 -const CAPACITY :u8 = 1 +const STATE_WIDTH:u8 = RATE + CAPACITY +const RATE:u8 = 15 +const CAPACITY:u8 = 1 // we will do // - FULL_ROUNDS_HALF full rounds // - PRTL_ROUNDS partial rounds // - FULL_ROUNDS_HALF full rounds // whence -const TOTAL_ROUNDS :u8 = FULL_ROUNDS_HALF + PRTL_ROUNDS + FULL_ROUNDS_HALF -const FULL_ROUNDS_HALF :u8 = 4 // 8 full rounds -const PRTL_ROUNDS :u8 = 20 +const TOTAL_ROUNDS:u8 = FULL_ROUNDS_HALF + PRTL_ROUNDS + FULL_ROUNDS_HALF +const FULL_ROUNDS_HALF:u8 = 4 // 8 full rounds +const PRTL_ROUNDS:u8 = 20 -fn poseidon(start :Address, size :u32) { - initialize_state(start, size) +fn poseidon(start:Address, size:u32) { + initialize_state(start, size) } // initialize_state initializes the state to contain @@ -67,21 +66,21 @@ fn poseidon(start :Address, size :u32) { // └ ┘ // // where L ≡ length in bytes of the inputs -fn initialize_state(input_offset :Address, input_size :u32) { +fn initialize_state(input_offset:Address, input_size:u32) { - var input_felt :u32 + var input_felt:u32 - for i :u8 = 0; i < RATE; i = i + 1 { - input_felt = (ram[i as Address] :: ram[(i + 1) as Address] :: ram[(i + 2) as Address]) as u32 - write_to_state(i, input_felt) - } + for i:u8 = 0; i(input_offset :Address, input_size :u32) { // │ π │ │ 0 │ // └ ┘ └ ┘ // -fn update_state(offset :Address, num_bytes :u8) { - var input_felt :u32 - var curr_value :u32 - var updt_value :u32 - var overflow :u1 - - if num_bytes == 0 { fail } - if num_bytes > ((BYTES_PER_FELT as u8) * (RATE as u8)) { fail } - - for i :u8 = 0; i < RATE; i = i + 1 { - input_felt = (ram[(i + 2) as Address] :: ram[(i + 1) as Address] :: ram[(i + 0) as Address]) as u32 - curr_value = read_from_state(i) - overflow :: updt_value = (curr_value as u33) + (input_felt as u33) - write_to_state(i, updt_value) - } +fn update_state(offset:Address, num_bytes:u8) { + var input_felt:u32 + var curr_value:u32 + var updt_value:u32 + var overflow:u1 + + if num_bytes == 0 { + fail + } + if num_bytes>((BYTES_PER_FELT as u8) * (RATE as u8)) { + fail + } + + for i:u8 = 0; i(offset :Address) -> (felt :u32) { - felt = (ram[(offset + 2) as Address] :: ram[(offset + 1) as Address] :: ram[(offset + 0) as Address]) as u32 +fn get_full_felt(offset:Address) -> (felt:u32) { + felt = (ram[(offset + 2) as Address]::ram[(offset + 1) as Address]::ram[(offset + 0) as Address]) as u32 } -fn get_partial_felt(offset :Address, n_bytes :u8) -> (felt :u32) { - if n_bytes == 0 { fail } - if n_bytes > BYTES_PER_FELT { fail } +fn get_partial_felt(offset:Address, n_bytes:u8) -> (felt:u32) { + if n_bytes == 0 { + fail + } + if n_bytes>BYTES_PER_FELT { + fail + } - felt = 0 - for i :u8 = n_bytes - 1; i >= 0; i = i - 1 { - felt = (felt << 8) + (ram[offset + (i as u64)] as u32) - } + felt = 0 + for i:u8 = n_bytes - 1; i >= 0; i = i - 1 { + felt = (felt << 8) + (ram[offset + (i as u64)] as u32) + } } -fn permutation(initial_round :Boolean) { +fn permutation(initial_round:Boolean) { - for r :u8 = 0; r < FULL_ROUNDS_HALF; r = r + 1 { - full_round(r) - } + for r:u8 = 0; r (res :u32) { - var aux :u64 +fn sbox(x:u32) -> (res:u32) { + var aux:u64 - // square - aux = (x as u64) * (x as u64) - res = (aux % (KOALABEAR_PRIME as u64)) as u32 + // square + aux = (x as u64) * (x as u64) + res = (aux % (KOALABEAR_PRIME as u64)) as u32 - // cube - aux = (res as u64) * (x as u64) - res = (aux % (KOALABEAR_PRIME as u64)) as u32 + // cube + aux = (res as u64) * (x as u64) + res = (aux % (KOALABEAR_PRIME as u64)) as u32 - return + return } -fn add_round_constants(r :u8) { - var start_index :u16 = (r as u16) * (STATE_WIDTH as u16) - var round_constant :u32 - var state_value :u32 - var overflow :u1 - - for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { - round_constant = round_constants[start_index] - state_value = state[i] - overflow :: state_value = (round_constant as u33) + (state_value as u33) - state[i] = state_value % KOALABEAR_PRIME - start_index = start_index + 1 - } +fn add_round_constants(r:u8) { + var start_index:u16 = (r as u16) * (STATE_WIDTH as u16) + var round_constant:u32 + var state_value:u32 + var overflow:u1 + + for i:u8 = 0; i(r :u8) { - add_round_constants(r) - for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { - state[i] = sbox(state[i]) - } - apply_mds() +fn full_round(r:u8) { + add_round_constants(r) + for i:u8 = 0; i(r :u8) { - add_round_constants(r) - state[0] = sbox(state[0]) - apply_mds() +fn partial_round(r:u8) { + add_round_constants(r) + state[0] = sbox(state[0]) + apply_mds() } // apply_mds applies the STATE_WIDTH x STATE_WIDTH mds matrix to the // state, viewed as a column vector w/ STATE_WIDTH many rows. fn apply_mds() { - // STATE_WIDTH < 2**8 - // mds[i,j] < 2**32 - // state[j] < 2**32 - // sum_j mds[i,j] ∙ state[j] < 2**(32 + 32 + 8) = 2**72 - var index :u16 = 0 - for i :u8 = 0; i < STATE_WIDTH; i = i + 1 { - var unreduced_sum :u72 = 0 - for j :u8 = 0; j < STATE_WIDTH; j = j + 1 { - unreduced_sum = unreduced_sum + ((mds_matrix[index] as u72) * (state[j] as u72)) - index = index + 1 + // STATE_WIDTH < 2**8 + // mds[i,j] < 2**32 + // state[j] < 2**32 + // sum_j mds[i,j] ∙ state[j] < 2**(32 + 32 + 8) = 2**72 + var index:u16 = 0 + for i:u8 = 0; i() { - for i :Address = 0; i < 16; i = i + 1 { - write_8(i * 4, i as u8) - } + for i:Address = 0; i<16; i = i + 1 { + write_8(i * 4, i as u8) + } } diff --git a/arithmetization/src/test/poseidon/utils.zkc b/arithmetization/src/test/poseidon/utils.zkc index f74f5830bc2..9d0adf3a47b 100644 --- a/arithmetization/src/test/poseidon/utils.zkc +++ b/arithmetization/src/test/poseidon/utils.zkc @@ -1,9 +1,9 @@ -fn write_to_state(address :u8, value:u32) -> () { - state[address] = value +fn write_to_state(address:u8, value:u32) -> () { + state[address] = value } -fn read_from_state(address :u8) -> (value :u32) { - value = state[address] - return +fn read_from_state(address:u8) -> (value:u32) { + value = state[address] + return } From 2140afc0796eb477de2ea67248c46476d642f813 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Tue, 5 May 2026 23:50:46 +0200 Subject: [PATCH 07/11] ras --- .../src/main/riscv/instruction_processing/r_type.zkc | 3 ++- arithmetization/src/main/riscv/interpreter.zkc | 2 +- 2 files changed, 3 insertions(+), 2 deletions(-) diff --git a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc index 4d2e33d84de..6592ead53af 100644 --- a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc @@ -363,11 +363,12 @@ fn process_R_type_instruction(opcode:Opcode, instruction_parameters:u } case CUSTOM_0: { - // ========================================== // custom instructions (precompiles etc ...) // ========================================== + printf "custom-0 instruction\n" + if (funct3 == FUNCT3_POSEIDON_1) && (funct7 == FUNCT7_POSEIDON_1) { printf "POSEIDON precompile\n" fail diff --git a/arithmetization/src/main/riscv/interpreter.zkc b/arithmetization/src/main/riscv/interpreter.zkc index a6fb8f3e0d9..fd750a6bbcd 100644 --- a/arithmetization/src/main/riscv/interpreter.zkc +++ b/arithmetization/src/main/riscv/interpreter.zkc @@ -52,7 +52,7 @@ fn interpreter(instruction:u32, pc:Address) -> (new_pc:Address) new_pc = process_J_type_instruction(instruction_parameters, pc) } default: { - printf "Unsupported instrution type %d\n", instruction_type + printf "Unsupported instruction type %d\n", instruction_type fail } } From a92c656a1465c50f66ace8fa0f89bb8425fbedfb Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 7 May 2026 19:37:51 +0200 Subject: [PATCH 08/11] feat: some work in progress ... --- .../src/test/poseidon/poseidon1.zkc | 129 +++++++++++------- arithmetization/src/test/poseidon/utils.zkc | 11 ++ 2 files changed, 93 insertions(+), 47 deletions(-) diff --git a/arithmetization/src/test/poseidon/poseidon1.zkc b/arithmetization/src/test/poseidon/poseidon1.zkc index 68abf258fa7..184aca09024 100644 --- a/arithmetization/src/test/poseidon/poseidon1.zkc +++ b/arithmetization/src/test/poseidon/poseidon1.zkc @@ -15,8 +15,14 @@ include "../../main/riscv/ram/write.zkc" // One notable feature of this implementation is that the length // of the message is included in the state at initialization time. +// we make state an array of felts (emulated as u32's) +// of length STATE_WIDTH × 2 which looks like so: +// +// [ σ₀, σ₁, ..., σₙ │ τ₀, τ₁, ..., τₙ] +// +// where the τ-part of the state is meant as temporary storage for +// operations updating the full state and n ≡ STATE_WIDTH memory state(index:u8) -> (st:u32) -memory state_copy(index:u8) -> (st:u32) // round_constants is a matrix with TOTAL_ROUNDS many rows and STATE_WIDTH many columns // mds_matrix is a square matrix of format STATE_WIDTH × STATE_WIDTH @@ -28,6 +34,7 @@ input mds_matrix(index:u16) -> (md:u32) const KOALABEAR_PRIME:u32 = 0x7F000001 // 2^31 - 2^24 + 1 or 2130706433 const ALPHA:u2 = 3 const BYTES_PER_FELT:u8 = 3 +const BYTES_PER_BLOCK:u32 = (BYTES_PER_FELT * RATE) as u32 const OUTPUT_LENGTH:u8 = RATE // OUTPUT_LENGTH ≤ RATE is required @@ -44,20 +51,31 @@ const TOTAL_ROUNDS:u8 = FULL_ROUNDS_HALF + PRTL_ROUNDS + FULL_ROUNDS_HALF const FULL_ROUNDS_HALF:u8 = 4 // 8 full rounds const PRTL_ROUNDS:u8 = 20 -fn poseidon(start:Address, size:u32) { - initialize_state(start, size) +fn poseidon(address:Address, size:u32) { + var n_rounds:u32 = (size + (BYTES_PER_BLOCK - 1)) / BYTES_PER_BLOCK + var final_size:u32 = size % BYTES_PER_BLOCK + var partial_round:u1 = 0 + + if final_size != 0 { + partial_round = 1 + } + + initialize_state(size) + + for i:u32 = 0; i(start:Address, size:u32) { // │ 0 │ // └ ┘ // -// where L ≡ length in bytes of the inputs -fn initialize_state(input_offset:Address, input_size:u32) { - - var input_felt:u32 - - for i:u8 = 0; i(size:u32) { + zero_out_state() - // Note: technically one should record 'input_size mod KOALABEAR_PRIME' rather than 'input_size' - write_to_state(RATE, input_size) + // taking the modulus is unnecessary in any reasonable application of the Poseidon hash function + write_to_state(RATE, size % KOALABEAR_PRIME) +} - for i:u8 = RATE; i() { + for i:u8 = 0; i(input_offset:Address, input_size:u32) { // │ ⋮ │ │ ⋮ │ // │ π │ │ 0 │ // └ ┘ └ ┘ -// -fn update_state(offset:Address, num_bytes:u8) { - var input_felt:u32 - var curr_value:u32 - var updt_value:u32 - var overflow:u1 +fn update_state(input_address:Address, block_size:u32) { - if num_bytes == 0 { - fail + var quotient:u32 + var remainder:u8 + + quotient = block_size / (BYTES_PER_FELT as u32) + remainder = (block_size % (BYTES_PER_FELT as u32)) as u8 + + var n_full_felts:u8 = RATE + var with_partl:u1 = 0 + + if quotient<(RATE as u32) { + n_full_felts = quotient as u8 + if remainder != 0 { + with_partl = 1 + } } - if num_bytes>((BYTES_PER_FELT as u8) * (RATE as u8)) { - fail + + var input_felt:u32 + var state_felt:u32 + var overflow:u1 + var curr_address:Address = input_address + + for i:u8 = 0; i(offset:Address) -> (felt:u32) { felt = (ram[(offset + 2) as Address]::ram[(offset + 1) as Address]::ram[(offset + 0) as Address]) as u32 } fn get_partial_felt(offset:Address, n_bytes:u8) -> (felt:u32) { + felt = 0 + if n_bytes == 0 { - fail + return } + if n_bytes>BYTES_PER_FELT { fail } - felt = 0 for i:u8 = n_bytes - 1; i >= 0; i = i - 1 { felt = (felt << 8) + (ram[offset + (i as u64)] as u32) } } -fn permutation(initial_round:Boolean) { +fn permutation() { for r:u8 = 0; r(r:u8) { } } -fn full_round(r:u8) { +fn full_round(r:u8) { add_round_constants(r) for i:u8 = 0; i(r:u8) { apply_mds() } -fn partial_round(r:u8) { +fn partial_round(r:u8) { add_round_constants(r) state[0] = sbox(state[0]) apply_mds() @@ -205,7 +240,7 @@ fn partial_round(r:u8) { // apply_mds applies the STATE_WIDTH x STATE_WIDTH mds matrix to the // state, viewed as a column vector w/ STATE_WIDTH many rows. -fn apply_mds() { +fn apply_mds() { // STATE_WIDTH < 2**8 // mds[i,j] < 2**32 @@ -218,12 +253,12 @@ fn apply_mds() { unreduced_sum = unreduced_sum + ((mds_matrix[index] as u72) * (state[j] as u72)) index = index + 1 } - state_copy[i] = (unreduced_sum % (KOALABEAR_PRIME as u72)) as u32 + write_to_tmp(i, (unreduced_sum % (KOALABEAR_PRIME as u72)) as u32) } // we copy the updated state over to the state for i:u8 = 0; i(address:u8, value:u32) -> () { state[address] = value @@ -7,3 +8,13 @@ fn read_from_state(address:u8) -> (value:u32) { value = state[address] return } + +fn write_to_tmp(address:u8, value:u32) -> () { + state[address + STATE_WIDTH] = value +} + +fn read_from_tmp(address:u8) -> (value:u32) { + value = state[address + STATE_WIDTH] + return +} + From 2bebdca54b8b2f56b4e3a1b127cfa783c83a8bdc Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Thu, 7 May 2026 21:29:35 +0200 Subject: [PATCH 09/11] fix: merge main issue --- .../main/riscv/instruction_processing/r_type.zkc | 15 ++++++--------- 1 file changed, 6 insertions(+), 9 deletions(-) diff --git a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc index 23c041e68e0..88cb0d2bc9d 100644 --- a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc @@ -329,8 +329,8 @@ fn process_R_type_instruction(opcode:Opcode, instruction_parameters:u } } } - case CUSTOM_0: { + case CUSTOM_0: { // ========================================== // custom instructions (precompiles etc ...) // ========================================== @@ -343,14 +343,11 @@ fn process_R_type_instruction(opcode:Opcode, instruction_parameters:u } } default: { - printf "unsupported R-type instruction with opcode %x", opcode - } else { - printf "[ERROR] Unsupported R-type instruction with\n" - printf "\topcode ≡ %x ≡ %b\n", opcode, opcode - printf "\tfunct3 ≡ %x ≡ %b\n", funct3, funct3 - printf "\tfunct7 ≡ %x ≡ %b\n", funct7, funct7 - fail - } + printf "[ERROR] Unsupported R-type instruction with\n" + printf "\topcode ≡ %x ≡ %b\n", opcode, opcode + printf "\tfunct3 ≡ %x ≡ %b\n", funct3, funct3 + printf "\tfunct7 ≡ %x ≡ %b\n", funct7, funct7 + fail } } } From fc5c2845b6b6f4c04bdf044cb3b5e237bc43bc69 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 8 May 2026 18:25:49 +0200 Subject: [PATCH 10/11] ras --- .../test/poseidon/constants/mds_matrix.zkc | 20 +++++++++++ .../poseidon/constants/round_constants.zkc | 33 +++++++++++++++++++ 2 files changed, 53 insertions(+) create mode 100644 arithmetization/src/test/poseidon/constants/mds_matrix.zkc create mode 100644 arithmetization/src/test/poseidon/constants/round_constants.zkc diff --git a/arithmetization/src/test/poseidon/constants/mds_matrix.zkc b/arithmetization/src/test/poseidon/constants/mds_matrix.zkc new file mode 100644 index 00000000000..e6631ed88cb --- /dev/null +++ b/arithmetization/src/test/poseidon/constants/mds_matrix.zkc @@ -0,0 +1,20 @@ +// STATE_WIDTH × STATE_WIDTH matrix +// M_{a,b} = Mij with ij = 8 × a + b +static mds_matrix(ij:u8) -> (Mij:u32) { + 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, 0x5ccec4ed, 0x41da12f7, 0x7164924a, 0x5bf72c24, 0x47f77778, 0x4dd6b5ae, + 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, 0x5ccec4ed, 0x41da12f7, 0x7164924a, 0x5bf72c24, 0x47f77778, + 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, 0x5ccec4ed, 0x41da12f7, 0x7164924a, 0x5bf72c24, + 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, 0x5ccec4ed, 0x41da12f7, 0x7164924a, + 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, 0x5ccec4ed, 0x41da12f7, + 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, 0x5ccec4ed, + 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, 0x6fc28f5d, + 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, 0x59f55556, + 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, 0x2c2c8591, + 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, 0x1cdd1746, + 0x69d55556, 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, 0x42861862, + 0x32cccccd, 0x69d55556, 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, 0x6bf33334, + 0x1fc00000, 0x32cccccd, 0x69d55556, 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, 0x281af287, + 0x54aaaaab, 0x1fc00000, 0x32cccccd, 0x69d55556, 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, 0x23471c72, + 0x3f800000, 0x54aaaaab, 0x1fc00000, 0x32cccccd, 0x69d55556, 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000, 0x0ef0f0f1, + 0x7f000000, 0x3f800000, 0x54aaaaab, 0x1fc00000, 0x32cccccd, 0x69d55556, 0x48924925, 0x0fe00000, 0x468e38e4, 0x58e66667, 0x39ba2e8c, 0x34eaaaab, 0x3a9d89d9, 0x63c92493, 0x10eeeeef, 0x07f00000 +} diff --git a/arithmetization/src/test/poseidon/constants/round_constants.zkc b/arithmetization/src/test/poseidon/constants/round_constants.zkc new file mode 100644 index 00000000000..cd743c9d143 --- /dev/null +++ b/arithmetization/src/test/poseidon/constants/round_constants.zkc @@ -0,0 +1,33 @@ +// 28 rows ≡ 28 rounds +// ≡ 4 + 20 + 4 +// ≡ 4 (full) + 20 (prtl) + 4 (full) +static round_constants(ij:u16) -> (Rij:u32) { + 0x7ee56a48, 0x11367045, 0x12e41941, 0x7ebbc12b, 0x1970b7d5, 0x662b60e8, 0x3e4990c6, 0x679f91f5, 0x350813bb, 0x00874ad4, 0x28a0081a, 0x18fa5872, 0x5f25b071, 0x5e5d5998, 0x5e6fd3e7, 0x5b2e2660, + 0x6f1837bf, 0x3fe6182b, 0x1edd7ac5, 0x57470d00, 0x43d486d5, 0x1982c70f, 0x0ea53af9, 0x61d6165b, 0x51639c00, 0x2dec352c, 0x2950e531, 0x2d2cb947, 0x08256cef, 0x1a0109f6, 0x1f51faf3, 0x5cef1c62, + 0x3d65e50e, 0x33d91626, 0x133d5a1e, 0x0ff49b0d, 0x38900cd1, 0x2c22cc3f, 0x28852bb2, 0x06c65a02, 0x7b2cf7bc, 0x68016e1a, 0x15e16bc0, 0x5248149a, 0x6dd212a0, 0x18d6830a, 0x5001be82, 0x64dac34e, + 0x5902b287, 0x426583a0, 0x0c921632, 0x3fe028a5, 0x245f8e49, 0x43bb297e, 0x7873dbd9, 0x3cc987df, 0x286bb4ce, 0x640a8dcd, 0x512a8e36, 0x03a4cf55, 0x481837a2, 0x03d6da84, 0x73726ac7, 0x760e7fdf, + 0x54dfeb5d, 0x7d40afd6, 0x722cb316, 0x106a4573, 0x45a7ccdb, 0x44061375, 0x154077a5, 0x45744faa, 0x4eb5e5ee, 0x3794e83f, 0x47c7093c, 0x5694903c, 0x69cb6299, 0x373df84c, 0x46a0df58, 0x46b8758a, + 0x3241ebcb, 0x0b09d233, 0x1af42357, 0x1e66cec2, 0x43e7dc24, 0x259a5d61, 0x27e85a3b, 0x1b9133fa, 0x343e5628, 0x485cd4c2, 0x16e269f5, 0x165b60c6, 0x25f683d9, 0x124f81f9, 0x174331f9, 0x77344dc5, + 0x5a821dba, 0x5fc4177f, 0x54153bf5, 0x5e3f1194, 0x3bdbf191, 0x088c84a3, 0x68256c9b, 0x3c90bbc6, 0x6846166a, 0x03f4238d, 0x463335fb, 0x5e3d3551, 0x6e59ae6f, 0x32d06cc0, 0x596293f3, 0x6c87edb2, + 0x08fc60b5, 0x34bcca80, 0x24f007f3, 0x62731c6f, 0x1e1db6c6, 0x0ca409bb, 0x585c1e78, 0x56e94edc, 0x16d22734, 0x18e11467, 0x7b2c3730, 0x770075e4, 0x35d1b18c, 0x22be3db5, 0x4fb1fbb7, 0x477cb3ed, + 0x7d5311c6, 0x5b62ae7d, 0x559c5fa8, 0x77f15048, 0x3211570b, 0x490fef6a, 0x77ec311f, 0x2247171b, 0x4e0ac711, 0x2edf69c9, 0x3b5a8850, 0x65809421, 0x5619b4aa, 0x362019a7, 0x6bf9d4ed, 0x5b413dff, + 0x617e181e, 0x5e7ab57b, 0x33ad7833, 0x3466c7ca, 0x6488dff4, 0x71f068f4, 0x056e891f, 0x04f1eccc, 0x663257d5, 0x671e31b9, 0x5871987c, 0x280c109e, 0x2a227761, 0x350a25e9, 0x5b91b1c4, 0x7a073546, + 0x01826270, 0x53a67720, 0x0ed4b074, 0x34cf0c4e, 0x6e751e88, 0x29bd5f59, 0x49ec32df, 0x7693452b, 0x3cf09e58, 0x6ba0e2bf, 0x7ab93acf, 0x3ce597df, 0x536e3d42, 0x147a808d, 0x5e32eb56, 0x5a203323, + 0x50965766, 0x6d44b7c5, 0x6698636a, 0x57b84f9f, 0x554b61b9, 0x6da0ab28, 0x1585b6ac, 0x6705a2b4, 0x152872f6, 0x0f4409fd, 0x23a9dd60, 0x6f2b18d4, 0x65ac9fd4, 0x2f0efbea, 0x591e67fd, 0x217ca19b, + 0x469c90ca, 0x03d60ef5, 0x4ea7857e, 0x07c86a4f, 0x288ed461, 0x2fe51b22, 0x7e293614, 0x2c4beb85, 0x5b0b7d11, 0x1e17dff6, 0x089beae1, 0x0a5acf1a, 0x2fc33d8f, 0x60422dc6, 0x6e1dc939, 0x635351b9, + 0x55522fc0, 0x3eb94ef7, 0x2a24a65c, 0x2e139c76, 0x51391144, 0x78cc0742, 0x579538f9, 0x44de9aae, 0x3c2f1e2e, 0x195747be, 0x2496339c, 0x650b2e39, 0x52899665, 0x6cb35558, 0x0f461c1c, 0x70f6b270, + 0x3faaa36f, 0x62e3348a, 0x672167cb, 0x394c880b, 0x2a46ba82, 0x63ffb74a, 0x1cf875d6, 0x53d12772, 0x036a4552, 0x3bdd9f2b, 0x02f72c24, 0x02b6006c, 0x077fe158, 0x1f9d6ea4, 0x20904d6f, 0x5d6534fa, + 0x066d8974, 0x6198f1f4, 0x26301ab4, 0x41f274c2, 0x00eac15c, 0x28b54b47, 0x2339739d, 0x48c6281c, 0x4ed935fc, 0x3f9187fa, 0x4a1930a6, 0x3ad4d736, 0x0f3f1889, 0x635a388f, 0x2862c145, 0x277ed1e8, + 0x4db23cad, 0x1f1b11f5, 0x1f3dba2b, 0x1c26eb4e, 0x0f7f5546, 0x6cd024b0, 0x67c47902, 0x793b8900, 0x0e8a283c, 0x4590b7ea, 0x6f567a2b, 0x5dc97300, 0x15247bc6, 0x50567fcb, 0x133eff84, 0x547dc2ef, + 0x34eb3dbb, 0x12402317, 0x66c6ae49, 0x174338b6, 0x24251008, 0x1b514927, 0x062d98d6, 0x7af30bbc, 0x26af15e8, 0x70d907a3, 0x5dfc5cac, 0x731f27ec, 0x53aa7d3f, 0x63ab0ec6, 0x216053f4, 0x18796b39, + 0x19156afd, 0x5eea6973, 0x6704c6a9, 0x0dce002b, 0x331169c0, 0x714d7178, 0x3ddaffaf, 0x7e464957, 0x20ca59ea, 0x679820c9, 0x42ef21a1, 0x798ea089, 0x14a74fa3, 0x0c06cf18, 0x6a4c8d52, 0x620f6d81, + 0x2220901a, 0x5277bb90, 0x230bf95e, 0x0ad8847a, 0x5e96e8b6, 0x77b4056e, 0x70a50d2c, 0x5f0eed59, 0x3646c4df, 0x10eb9a87, 0x21eed6b7, 0x534add36, 0x6e3e7421, 0x2b25810e, 0x1d8f707b, 0x45318a1a, + 0x677f8ff2, 0x0258c9e0, 0x4cd02a00, 0x2e24ff15, 0x634a715d, 0x4ac01e59, 0x601511e1, 0x26e9c01a, 0x4c165c6e, 0x57cd1140, 0x3ac6543b, 0x6787d847, 0x037dfbf9, 0x6dd9d079, 0x4d24b281, 0x2a6f407d, + 0x0131df8e, 0x4b8a7896, 0x23700858, 0x2cf5e534, 0x12aafc3f, 0x54568d03, 0x1a250735, 0x5331686d, 0x4ce76d91, 0x799c1a8c, 0x2b7a8ac9, 0x60aee672, 0x74f7421c, 0x3c42146d, 0x26d369c5, 0x4ae54a12, + 0x7eea16d1, 0x5ce3eae8, 0x69f28994, 0x262b8642, 0x610d4cc4, 0x5e1af21c, 0x1a8526d0, 0x316b127b, 0x3576fe5d, 0x02d968a0, 0x4ba00f51, 0x40bed993, 0x377fb907, 0x7859216e, 0x1931d9d1, 0x53b0934e, + 0x71914ff7, 0x4eabae6c, 0x7196468e, 0x164b3cc2, 0x58cb66c0, 0x4c147307, 0x6b3afccd, 0x4236518b, 0x4ad85605, 0x291382e1, 0x1e89b6cf, 0x5e16c3a8, 0x2e675921, 0x24300954, 0x05e555c3, 0x78880a24, + 0x763a3125, 0x4f53b240, 0x18b7fa43, 0x2bbe8a73, 0x1c9a12f2, 0x3f6fd40d, 0x0e1d4ec4, 0x1361c64d, 0x09a8f470, 0x03d23a40, 0x109ad290, 0x28c2fb88, 0x3b6498f2, 0x74d8be57, 0x6a4277d2, 0x18c2b3d4, + 0x6252c30c, 0x07cc2560, 0x209fe15b, 0x52a55fac, 0x4df19eb7, 0x02521116, 0x5e414ff1, 0x3cd9a1f4, 0x005aad15, 0x27a53f00, 0x72bbe9cb, 0x71d8bd7d, 0x4194b79a, 0x48e87a72, 0x3341553c, 0x63d34faa, + 0x132a01e3, 0x3833e2d9, 0x49726e04, 0x054957f8, 0x7b71bce4, 0x73eec57d, 0x556e5533, 0x1fa93fde, 0x346a8ca8, 0x1162dfde, 0x5c30d028, 0x094a4294, 0x3052dcda, 0x37988498, 0x51f06b97, 0x65848779, + 0x7599b0d4, 0x436fdabc, 0x66c5b77d, 0x40c86a9e, 0x27e7055b, 0x6d0dd9d8, 0x7e5598b5, 0x1a4d04f3, 0x5e3b2bc7, 0x533b5b2f, 0x3e33a125, 0x664d71ce, 0x382e6c2a, 0x24c4eb6e, 0x13f246f7, 0x07e2d7ef +} From 8707345cfa04362db63d030d8fd84803714bd406 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Olivier=20B=C3=A9gassat?= Date: Fri, 8 May 2026 18:26:04 +0200 Subject: [PATCH 11/11] ras: minor poseidon stuff --- .../src/test/poseidon/poseidon1.zkc | 62 ++++++++++++++----- .../src/test/poseidon/test/poseidon1_01.zkc | 9 ++- arithmetization/src/test/poseidon/utils.zkc | 19 ++++++ 3 files changed, 74 insertions(+), 16 deletions(-) diff --git a/arithmetization/src/test/poseidon/poseidon1.zkc b/arithmetization/src/test/poseidon/poseidon1.zkc index 184aca09024..347a780edb7 100644 --- a/arithmetization/src/test/poseidon/poseidon1.zkc +++ b/arithmetization/src/test/poseidon/poseidon1.zkc @@ -24,10 +24,10 @@ include "../../main/riscv/ram/write.zkc" // operations updating the full state and n ≡ STATE_WIDTH memory state(index:u8) -> (st:u32) -// round_constants is a matrix with TOTAL_ROUNDS many rows and STATE_WIDTH many columns -// mds_matrix is a square matrix of format STATE_WIDTH × STATE_WIDTH -input round_constants(index:u16) -> (rc:u32) -input mds_matrix(index:u16) -> (md:u32) +// // round_constants is a matrix with TOTAL_ROUNDS many rows and STATE_WIDTH many columns +// // mds_matrix is a square matrix of format STATE_WIDTH × STATE_WIDTH +// input round_constants(index:u16) -> (rc:u32) +// input mds_matrix(index:u16) -> (md:u32) // this implementation does not use the native field element type yet @@ -43,26 +43,55 @@ const RATE:u8 = 15 const CAPACITY:u8 = 1 // we will do -// - FULL_ROUNDS_HALF full rounds -// - PRTL_ROUNDS partial rounds -// - FULL_ROUNDS_HALF full rounds +// - FULL_ROUNDS_HALF full rounds +// - PRTL_ROUNDS prtl rounds +// - FULL_ROUNDS_HALF full rounds // whence const TOTAL_ROUNDS:u8 = FULL_ROUNDS_HALF + PRTL_ROUNDS + FULL_ROUNDS_HALF -const FULL_ROUNDS_HALF:u8 = 4 // 8 full rounds +const FULL_ROUNDS_HALF:u8 = 4 // 8 = 4 + 4 full rounds const PRTL_ROUNDS:u8 = 20 -fn poseidon(address:Address, size:u32) { +// poseidon performs the Poseidon1 hash of the nonempty byte range +// +// sa..ea +// +// with sa := address, ea := address + size and copies the results over to +// destination +fn poseidon(address:Address, size:u32, destination:Address) { + + if size == 0 { + printf "poseidon called with empty inputs" + fail + } + var n_rounds:u32 = (size + (BYTES_PER_BLOCK - 1)) / BYTES_PER_BLOCK var final_size:u32 = size % BYTES_PER_BLOCK - var partial_round:u1 = 0 + var final_partial_round:u1 = 0 if final_size != 0 { - partial_round = 1 + final_partial_round = 1 } initialize_state(size) + var curr_address:Address = address + var curr_size:u32 = BYTES_PER_BLOCK + for i:u32 = 0; i(size:u32) { write_to_state(RATE, size % KOALABEAR_PRIME) } -// zero_out_state sets the state σ to all zeros. +// zero_out_state sets the state (σ, τ) to all zeros, +// which includes the "tmp" portion τ of the state fn zero_out_state() { - for i:u8 = 0; i (res:u32) { return } +// add_round_constants adds round constants to the state fn add_round_constants(r:u8) { var start_index:u16 = (r as u16) * (STATE_WIDTH as u16) var round_constant:u32 @@ -224,6 +255,7 @@ fn add_round_constants(r:u8) { } } +// full_round processes a full round: the s_box is applied to every entry of the state fn full_round(r:u8) { add_round_constants(r) for i:u8 = 0; i() { // mds[i,j] < 2**32 // state[j] < 2**32 // sum_j mds[i,j] ∙ state[j] < 2**(32 + 32 + 8) = 2**72 - var index:u16 = 0 + var index:u8 = 0 for i:u8 = 0; i() { // we copy the updated state over to the state for i:u8 = 0; i() { +fn main() { + + // we write the message 0x00 01 02 ... fe ff into memory for i:Address = 0; i<16; i = i + 1 { write_8(i * 4, i as u8) } + + var message_size:u32 = 16 + var message_offset:Address = 0 + + poseidon(message_offset, message_size, 256) } diff --git a/arithmetization/src/test/poseidon/utils.zkc b/arithmetization/src/test/poseidon/utils.zkc index 7adef7ee0fb..2a7db1fe9d4 100644 --- a/arithmetization/src/test/poseidon/utils.zkc +++ b/arithmetization/src/test/poseidon/utils.zkc @@ -18,3 +18,22 @@ fn read_from_tmp(address:u8) -> (value:u32) { return } +fn wipe_tmp() { + for i:u8 = 0; i(address:Address, index:u8) -> (address_updt:Address) { + var b3:u8 + var b2:u8 + var b1:u8 + var b0:u8 + b3::b2::b1::b0 = state[index] + ram[address + 3] = b3 + ram[address + 2] = b2 + ram[address + 1] = b1 + ram[address + 0] = b0 + address_updt = address + 4 +} +