diff --git a/arithmetization/src/main/riscv/instruction_processing/i_type.zkc b/arithmetization/src/main/riscv/instruction_processing/i_type.zkc index d63bbdcb20a..c27d5a5b6ee 100644 --- a/arithmetization/src/main/riscv/instruction_processing/i_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/i_type.zkc @@ -209,7 +209,7 @@ fn process_syscall(pc:Address) -> (new_pc:Address) { var call_num:DoubleWord = registers[17] // switch call_num { - case 93: { // exit + case 93: { // exit var exit_code:DoubleWord = registers[10] // check for non-zero exit code if exit_code != 0 { diff --git a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc index b1aafd3b56e..88cb0d2bc9d 100644 --- a/arithmetization/src/main/riscv/instruction_processing/r_type.zkc +++ b/arithmetization/src/main/riscv/instruction_processing/r_type.zkc @@ -69,6 +69,8 @@ fn process_R_type_instruction(opcode:Opcode, instruction_parameters:u funct7::rs2::rs1::funct3::rd = instruction_parameters + printf "funct3 ≡ %b, funct7 ≡ %b\n", funct3, funct7 + v1 = registers[rs1] v2 = registers[rs2] @@ -325,15 +327,21 @@ fn process_R_type_instruction(opcode:Opcode, instruction_parameters:u } else { registers[rd] = sgn_extension_u32_u64(v1_lower % v2_lower) } - } else { - printf "[ERROR] Unsupported R-type instruction with\n" - printf "\topcode ≡ OP_32 ≡ %x ≡ %b\n", opcode, opcode - printf "\tfunct3 ≡ %x ≡ %b\n", funct3, funct3 - printf "\tfunct7 ≡ %x ≡ %b\n", funct7, funct7 - fail } } + 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 + } + } default: { printf "[ERROR] Unsupported R-type instruction with\n" printf "\topcode ≡ %x ≡ %b\n", opcode, opcode diff --git a/arithmetization/src/main/riscv/utils/constants.zkc b/arithmetization/src/main/riscv/utils/constants.zkc index 9f2a325c94f..0f322914352 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 // ====================== 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/src/poseidon1.rs b/arithmetization/src/test/examples/rust/src/poseidon1.rs new file mode 100644 index 00000000000..d7efd8c68b8 --- /dev/null +++ b/arithmetization/src/test/examples/rust/src/poseidon1.rs @@ -0,0 +1,99 @@ +#![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 :&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 + +const FUNCT3_POSEIDON_1 :u8 = 0b111; +const FUNCT7_POSEIDON_1 :u8 = 0b1111111; + + +core::arch::global_asm!( + ".global _start", + "_start:", + "li sp, 0x087fffff", // set stack pointer to a known memory region + "call main", +); + + +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: 0x01 + // 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, 0b111, 0b1111111, {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); + + 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); +} + +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/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 +} 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/poseidon1.zkc b/arithmetization/src/test/poseidon/poseidon1.zkc new file mode 100644 index 00000000000..347a780edb7 --- /dev/null +++ b/arithmetization/src/test/poseidon/poseidon1.zkc @@ -0,0 +1,296 @@ +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 +// ============================================= +// +// 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. + +// 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) + +// // 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 + +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 + +const STATE_WIDTH:u8 = RATE + CAPACITY +const RATE:u8 = 15 +const CAPACITY:u8 = 1 + +// we will do +// - 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 = 4 + 4 full rounds +const PRTL_ROUNDS:u8 = 20 + +// 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 final_partial_round:u1 = 0 + + if final_size != 0 { + 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) { + zero_out_state() + + // taking the modulus is unnecessary in any reasonable application of the Poseidon hash function + write_to_state(RATE, size % KOALABEAR_PRIME) +} + +// 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<(2 * STATE_WIDTH); i = i + 1 { + write_to_state(i, 0) + } +} + +// update_state updates the current state σ to σ' defined by +// adding the next block of data carrying felts (blk) to the +// rate many first coordinates of σ: +// +// σ' ≡ σ + blk +// +// ←σ→ ←blk→ +// ┌ ┐ ┌ ┐ +// │ A │ │ a │ +// │ B │ │ b │ +// │ │ │ │ +// │ ⋮ │ │ ⋮ │ +// │ │ │ │ +// │ Q │ │ q │ +// ≡ │ R │ + │ r │ +// ├ ┤ ├ ┤ +// │ λ │ │ 0 │ +// │ μ │ │ 0 │ +// │ ⋮ │ │ ⋮ │ +// │ π │ │ 0 │ +// └ ┘ └ ┘ +fn update_state(input_address:Address, block_size:u32) { + + 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 + } + } + + 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 { + return + } + + if n_bytes>BYTES_PER_FELT { + fail + } + + for i:u8 = n_bytes - 1; i >= 0; i = i - 1 { + felt = (felt << 8) + (ram[offset + (i as u64)] as u32) + } +} + +fn permutation() { + + for r:u8 = 0; r (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 +} + +// 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 + var state_value:u32 + var overflow:u1 + + for i:u8 = 0; i(r:u8) { + add_round_constants(r) + for i:u8 = 0; i(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:u8 = 0 + for i:u8 = 0; i() { + + // 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 new file mode 100644 index 00000000000..2a7db1fe9d4 --- /dev/null +++ b/arithmetization/src/test/poseidon/utils.zkc @@ -0,0 +1,39 @@ +include "poseidon1.zkc" + +fn write_to_state(address:u8, value:u32) -> () { + state[address] = value +} + +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 +} + +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 +} +