From 9588ecae8fe18a4d369641fca346f2a344819981 Mon Sep 17 00:00:00 2001 From: jacobdweightman Date: Thu, 20 Feb 2025 11:12:45 -0600 Subject: [PATCH] Delete unused keccak circuit; rename keccak2 to keccak --- zirgen/bootstrap/src/main.rs | 2 +- zirgen/circuit/BUILD.bazel | 1 - zirgen/circuit/keccak/BUILD.bazel | 105 +- zirgen/circuit/keccak/README.md | 45 - zirgen/circuit/{keccak2 => keccak}/arr.zir | 0 zirgen/circuit/keccak/bits.zir | 75 +- .../{keccak2 => keccak}/cpp/BUILD.bazel | 2 +- .../circuit/{keccak2 => keccak}/cpp/main.cpp | 10 +- .../{keccak2 => keccak}/cpp/preflight.cpp | 14 +- .../{keccak2 => keccak}/cpp/preflight.h | 8 +- .../circuit/{keccak2 => keccak}/cpp/trace.cpp | 8 +- .../circuit/{keccak2 => keccak}/cpp/trace.h | 6 +- .../{keccak2 => keccak}/cpp/wrap_dsl.cpp | 8 +- .../{keccak2 => keccak}/cpp/wrap_dsl.h | 8 +- .../circuit/{keccak2 => keccak}/is_zero.zir | 0 zirgen/circuit/keccak/keccak.zir | 1894 ++--------------- .../circuit/keccak/methods/guest/Cargo.lock | 1414 ------------ zirgen/circuit/keccak/one_hot.zir | 2 +- zirgen/circuit/{keccak2 => keccak}/pack.zir | 0 .../{keccak2 => keccak}/predicates.cpp | 2 +- zirgen/circuit/{keccak2 => keccak}/sha2.zir | 0 zirgen/circuit/keccak/sha256_for_keccak.zir | 417 ---- zirgen/circuit/keccak/test0k.nop | 11 - zirgen/circuit/keccak/test0s.nop | 11 - zirgen/circuit/keccak/test1k.zir | 11 - zirgen/circuit/keccak/test1s.nop | 11 - zirgen/circuit/keccak/test2k.zir | 11 - zirgen/circuit/keccak/test2s.nop | 11 - zirgen/circuit/keccak/test_keccak_01.txt | 3 - zirgen/circuit/keccak/test_keccak_02.txt | 5 - zirgen/circuit/{keccak2 => keccak}/top.zir | 0 zirgen/circuit/{keccak2 => keccak}/xor5.zir | 0 zirgen/circuit/keccak2/BUILD.bazel | 95 - zirgen/circuit/keccak2/bits.zir | 70 - zirgen/circuit/keccak2/keccak.zir | 206 -- zirgen/circuit/keccak2/one_hot.zir | 33 - 36 files changed, 305 insertions(+), 4194 deletions(-) delete mode 100644 zirgen/circuit/keccak/README.md rename zirgen/circuit/{keccak2 => keccak}/arr.zir (100%) rename zirgen/circuit/{keccak2 => keccak}/cpp/BUILD.bazel (92%) rename zirgen/circuit/{keccak2 => keccak}/cpp/main.cpp (94%) rename zirgen/circuit/{keccak2 => keccak}/cpp/preflight.cpp (97%) rename zirgen/circuit/{keccak2 => keccak}/cpp/preflight.h (90%) rename zirgen/circuit/{keccak2 => keccak}/cpp/trace.cpp (94%) rename zirgen/circuit/{keccak2 => keccak}/cpp/trace.h (94%) rename zirgen/circuit/{keccak2 => keccak}/cpp/wrap_dsl.cpp (98%) rename zirgen/circuit/{keccak2 => keccak}/cpp/wrap_dsl.h (89%) rename zirgen/circuit/{keccak2 => keccak}/is_zero.zir (100%) delete mode 100644 zirgen/circuit/keccak/methods/guest/Cargo.lock rename zirgen/circuit/{keccak2 => keccak}/pack.zir (100%) rename zirgen/circuit/{keccak2 => keccak}/predicates.cpp (98%) rename zirgen/circuit/{keccak2 => keccak}/sha2.zir (100%) delete mode 100644 zirgen/circuit/keccak/sha256_for_keccak.zir delete mode 100644 zirgen/circuit/keccak/test0k.nop delete mode 100644 zirgen/circuit/keccak/test0s.nop delete mode 100644 zirgen/circuit/keccak/test1k.zir delete mode 100644 zirgen/circuit/keccak/test1s.nop delete mode 100644 zirgen/circuit/keccak/test2k.zir delete mode 100644 zirgen/circuit/keccak/test2s.nop delete mode 100644 zirgen/circuit/keccak/test_keccak_01.txt delete mode 100644 zirgen/circuit/keccak/test_keccak_02.txt rename zirgen/circuit/{keccak2 => keccak}/top.zir (100%) rename zirgen/circuit/{keccak2 => keccak}/xor5.zir (100%) delete mode 100644 zirgen/circuit/keccak2/BUILD.bazel delete mode 100644 zirgen/circuit/keccak2/bits.zir delete mode 100644 zirgen/circuit/keccak2/keccak.zir delete mode 100644 zirgen/circuit/keccak2/one_hot.zir diff --git a/zirgen/bootstrap/src/main.rs b/zirgen/bootstrap/src/main.rs index 99eb9604..27dd7d01 100644 --- a/zirgen/bootstrap/src/main.rs +++ b/zirgen/bootstrap/src/main.rs @@ -584,7 +584,7 @@ impl Bootstrap { fn keccak(&'static self) { self.install_from_bazel( - "//zirgen/circuit/keccak2:bootstrap", + "//zirgen/circuit/keccak:bootstrap", self.output_and("risc0/circuit/keccak"), &[ Rule::copy("*.cpp", "kernels/cxx").base_suffix("-sys"), diff --git a/zirgen/circuit/BUILD.bazel b/zirgen/circuit/BUILD.bazel index 7b4334e8..15c106ec 100644 --- a/zirgen/circuit/BUILD.bazel +++ b/zirgen/circuit/BUILD.bazel @@ -7,7 +7,6 @@ filegroup( srcs = [ "//zirgen/circuit/bigint:bigint_blob", "//zirgen/circuit/fib", - "//zirgen/circuit/keccak", "//zirgen/circuit/predicates:recursion_zkr", "//zirgen/circuit/recursion", "//zirgen/circuit/rv32im/v1/edsl:rv32im", diff --git a/zirgen/circuit/keccak/BUILD.bazel b/zirgen/circuit/keccak/BUILD.bazel index 75b52add..cf7a71be 100644 --- a/zirgen/circuit/keccak/BUILD.bazel +++ b/zirgen/circuit/keccak/BUILD.bazel @@ -1,48 +1,95 @@ +load("@rules_pkg//pkg:zip.bzl", "pkg_zip") load("//bazel/rules/lit:defs.bzl", "glob_lit_tests") +load("//bazel/rules/zirgen:dsl-defs.bzl", "zirgen_build") load("//bazel/rules/zirgen:edsl-defs.bzl", "ZIRGEN_OUTS", "build_circuit") -package( - default_visibility = ["//visibility:public"], -) +package(default_visibility = ["//visibility:public"]) -KECCAK_ZIR_FILES = [ - "bits.zir", - "keccak.zir", - "one_hot.zir", - "sha256_for_keccak.zir", -] +filegroup( + name = "imports", + srcs = glob(["*.zir"]), +) glob_lit_tests( - # TODO: shorten timeout once zirgen is faster - timeout = "long", - data = KECCAK_ZIR_FILES, - exclude = KECCAK_ZIR_FILES, + data = [":imports"], + size_override = { + "top.zir": "medium", + "sha2.zir": "medium", + }, test_file_exts = ["zir"], ) -KECCAK_OUTS = ZIRGEN_OUTS + [ - "rust_poly_fp_0.cpp", - "rust_poly_fp_1.cpp", - "rust_poly_fp_2.cpp", - "rust_poly_fp_3.cpp", - "rust_poly_fp_4.cpp", - "eval_check_0.cu", - "eval_check_1.cu", - "eval_check_2.cu", - "eval_check_3.cu", - "eval_check_4.cu", +zirgen_build( + name = "cppinc", + out = "keccak.cpp.inc", + data = [":imports"], + opts = [ + "--emit=cpp", + "--validity=false", + ], + zir_file = ":top.zir", +) + +SPLIT_VALIDITY = 5 + +SPLIT_STEP = 16 + +OUTS = ZIRGEN_OUTS + [ + fn + for i in range(SPLIT_VALIDITY) + for fn in [ + "rust_poly_fp_" + str(i) + ".cpp", + "eval_check_" + str(i) + ".cu", + ] +] + [ + fn + for i in range(SPLIT_STEP) + for fn in [ + "steps_" + str(i) + ".cpp", + "steps_" + str(i) + ".cu", + ] +] + [ "eval_check.cuh", + "steps.h", + "steps.cuh", + "layout.h.inc", + "layout.cuh.inc", ] build_circuit( - name = "keccak", - outs = KECCAK_OUTS, + name = "codegen", + outs = OUTS, bin = "//zirgen/Main:gen_zirgen", - data = KECCAK_ZIR_FILES, + data = [":imports"], extra_args = [ - "zirgen/circuit/keccak/keccak.zir", + "zirgen/circuit/keccak/top.zir", "-I", "zirgen/circuit/keccak", - "--validity-split-count=5", + "--circuit-name=keccak", + "--validity-split-count=" + str(SPLIT_VALIDITY), + "--step-split-count=" + str(SPLIT_STEP), + "--parallel-witgen", + "--protocol-info=KECCAK:v1_______" + ], +) + +ZKRS = [("keccak_lift_" + str(po2)) for po2 in range(14, 19)] + +build_circuit( + name = "predicates", + srcs = ["predicates.cpp"], + outs = [fn for zkr in ZKRS for fn in [ + zkr + ".zkr", + ]], + data = ["@zirgen//zirgen/circuit/keccak:validity.ir"], + extra_args = ["--keccak-ir=$(location :validity.ir)"], + deps = ["//zirgen/circuit/predicates:lib"], +) + +filegroup( + name = "bootstrap", + srcs = [ + ":codegen", + ":predicates", ], ) diff --git a/zirgen/circuit/keccak/README.md b/zirgen/circuit/keccak/README.md deleted file mode 100644 index cad73830..00000000 --- a/zirgen/circuit/keccak/README.md +++ /dev/null @@ -1,45 +0,0 @@ -# The Keccak Accelerator - -This directory contains the implementation of the keccak accelerator. - -## Input transcript format - -The expected format of the keccak input is a list of one or more of `data blocks` ending with a `final padding` consisting of 8 bytes of zeros (`0x0000000000000000`) - -### Keccak Input Transcript - -| Name | Byte Length | Description | -|---------------|-------------|----------------------------------------------------------------------| -| data blocks | arbitrary | raw data blocks containing the block count followed by the raw data. | -| final padding | 8 | Padding used to indicate the end of the keccak input transcript. | - -### Data Blocks - -Data blocks represent the raw data being hashed. This contains an 2-byte value that represents the block size followed by a sequence of bytes representing the raw data, ending with the output digest generated by running keccak. - -| Name | Byte Length | Description | -|------------------|-------------|---------------------------------------------------------------------------------------------| -| block count (BC) | 2 | the amount of blocks that the raw data spans. Each block is 136 bytes. | -| padding | 6 | Padding containing all 0 values. This is used to align the length along an 8-byte boundary. | -| raw data | BC * 136 | Represents the raw data. | -| output digest | 32 | the keccak hash of the raw data. | - -### Example: using the accelerator in Rust crates - -Most rust cryptographic hashing crates use an API similar to the following code snippet: -``` -let mut hasher = Keccak256::new(); - -// write input message -hasher.update(&input); - -// read hash digest -let result = hasher.finalize(); -``` - -In this code snippet, `hasher` carries an internal state which is modified the input using the `update(input)` function. `finalize` will generate a resulting hash. In order to use the accelerator we need to generate an input transcript. To keep the proof under 2 million cycles the maximum amount of data we can hash in the accelerator is approximately 95 kilobytes. - -The following assumes a situation where a single call to finalize is compressing less than 95 KB of input data and only one instance of hasher is present. - -* Every time update is called, the input is split up to fit inside the 136 byte block. Once the block fills up, it is compressed using keccak. In our design, we send each of the blocks to the host in order to record the raw data of the input transcript. -* Once the hasher's `finalize` function is called we can communicate with the termination so that the block count can be computed and for the keccak hash to be generated. diff --git a/zirgen/circuit/keccak2/arr.zir b/zirgen/circuit/keccak/arr.zir similarity index 100% rename from zirgen/circuit/keccak2/arr.zir rename to zirgen/circuit/keccak/arr.zir diff --git a/zirgen/circuit/keccak/bits.zir b/zirgen/circuit/keccak/bits.zir index 93f4089e..200d1cb2 100644 --- a/zirgen/circuit/keccak/bits.zir +++ b/zirgen/circuit/keccak/bits.zir @@ -2,6 +2,7 @@ // RUN: zirgen --test %s // Assert that a given value is a bit +#[picus_inline] function AssertBit(val: Val) { val * (1 - val) = 0; } @@ -20,66 +21,50 @@ component BitReg(val: Val) { reg } -// Check that valid bits are valid -test BitInRange { - AssertBit(0); - AssertBit(1); -} - -// Check that 2 is not a bit -test_fails BitOutOfRange { - AssertBit(2); -} - -// Assert the a given value is a 2-bit number (i.e. 0-3) -function AssertTwit(val: Val) { - val * (1 - val) * (2 - val) * (3 - val) = 0; -} - +// Simple bit ops component BitAnd(a: Val, b: Val) { - Reg(a * b) + a * b } component BitOr(a: Val, b: Val) { - Reg(1 - (1 - a) * (1 - b)) + a + b - a * b } -// Set a register nodeterministically, and then verify it is a twit -component NondetTwitReg(val: Val) { - reg := NondetReg(val); - AssertTwit(reg); - reg +component BitXor(a: Val, b: Val) { + a + b - 2 * a * b } -// Set a register nodeterministically, and then verify it is a twit -component NondetFakeTwitReg(val: Val) { - reg0 := NondetBitReg(val & 1); - reg1 := NondetBitReg((val & 2) / 2); - reg1 * 2 + reg0 +// Tests.... + +// Check that valid bits are valid +test BitInRange { + AssertBit(0); + AssertBit(1); } -component TwitReg(val: Val) { - reg := NondetTwitReg(val); - val = reg; - reg +// Check that 2 is not a bit +test_fails BitOutOfRange { + AssertBit(2); } -component FakeTwitReg(val: Val) { - reg := NondetFakeTwitReg(val); - val = reg; - reg +test TestAnd { + BitAnd(0, 0) = 0; + BitAnd(0, 1) = 0; + BitAnd(1, 0) = 0; + BitAnd(1, 1) = 1; } -// Check that all valid twit values are OK -test TwitInRange{ - AssertTwit(0); - AssertTwit(1); - AssertTwit(2); - AssertTwit(3); +test TestOr { + BitOr(0, 0) = 0; + BitOr(0, 1) = 1; + BitOr(1, 0) = 1; + BitOr(1, 1) = 1; } -// Check that 4 is not a twit -test_fails TwitOutOfRange { - AssertTwit(4); +test TestXor { + BitXor(0, 0) = 0; + BitXor(0, 1) = 1; + BitXor(1, 0) = 1; + BitXor(1, 1) = 0; } diff --git a/zirgen/circuit/keccak2/cpp/BUILD.bazel b/zirgen/circuit/keccak/cpp/BUILD.bazel similarity index 92% rename from zirgen/circuit/keccak2/cpp/BUILD.bazel rename to zirgen/circuit/keccak/cpp/BUILD.bazel index 3f20553f..17345293 100644 --- a/zirgen/circuit/keccak2/cpp/BUILD.bazel +++ b/zirgen/circuit/keccak/cpp/BUILD.bazel @@ -11,7 +11,7 @@ cc_library( # "run.cpp", "trace.cpp", "wrap_dsl.cpp", - "//zirgen/circuit/keccak2:cppinc", + "//zirgen/circuit/keccak:cppinc", ], hdrs = [ "preflight.h", diff --git a/zirgen/circuit/keccak2/cpp/main.cpp b/zirgen/circuit/keccak/cpp/main.cpp similarity index 94% rename from zirgen/circuit/keccak2/cpp/main.cpp rename to zirgen/circuit/keccak/cpp/main.cpp index 334b5bb8..091305fe 100644 --- a/zirgen/circuit/keccak2/cpp/main.cpp +++ b/zirgen/circuit/keccak/cpp/main.cpp @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -12,7 +12,7 @@ // See the License for the specific language governing permissions and // limitations under the License. -#include "zirgen/circuit/keccak2/cpp/wrap_dsl.h" +#include "zirgen/circuit/keccak/cpp/wrap_dsl.h" #include "zirgen/compiler/zkp/sha256.h" /* The below implementation (up till the end of keccackf) is taken from: @@ -84,7 +84,7 @@ static void keccakf(uint64_t s[25]) { std::cout << "Final: " << round << ", s[0] = " << std::hex << s[0] << std::dec << "\n"; } -void ShaSingleKeccak(zirgen::Digest& digest, zirgen::keccak2::KeccakState state) { +void ShaSingleKeccak(zirgen::Digest& digest, zirgen::keccak::KeccakState state) { std::vector toHash(64); uint32_t* viewState = (uint32_t*)&state; for (size_t i = 0; i < 50; i++) { @@ -95,7 +95,7 @@ void ShaSingleKeccak(zirgen::Digest& digest, zirgen::keccak2::KeccakState state) } } -void DoTransaction(zirgen::Digest& digest, zirgen::keccak2::KeccakState state) { +void DoTransaction(zirgen::Digest& digest, zirgen::keccak::KeccakState state) { ShaSingleKeccak(digest, state); std::cout << "After compressing input: " << digest << "\n"; keccakf(state.data()); @@ -105,7 +105,7 @@ void DoTransaction(zirgen::Digest& digest, zirgen::keccak2::KeccakState state) { int main() { // Make an example - using namespace zirgen::keccak2; + using namespace zirgen::keccak; KeccakState state; uint64_t pows = 987654321; for (size_t i = 0; i < state.size(); i++) { diff --git a/zirgen/circuit/keccak2/cpp/preflight.cpp b/zirgen/circuit/keccak/cpp/preflight.cpp similarity index 97% rename from zirgen/circuit/keccak2/cpp/preflight.cpp rename to zirgen/circuit/keccak/cpp/preflight.cpp index 6a6b839e..28177634 100644 --- a/zirgen/circuit/keccak2/cpp/preflight.cpp +++ b/zirgen/circuit/keccak/cpp/preflight.cpp @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -12,15 +12,15 @@ // See the License for the specific language governing permissions and // limitations under the License. -#include "zirgen/circuit/keccak2/cpp/preflight.h" -#include "zirgen/circuit/keccak2/cpp/wrap_dsl.h" +#include "zirgen/circuit/keccak/cpp/preflight.h" +#include "zirgen/circuit/keccak/cpp/wrap_dsl.h" #include #include #include #include -namespace zirgen::keccak2 { +namespace zirgen::keccak { namespace { @@ -192,7 +192,7 @@ struct ControlState { static ControlState Write() { return ControlState{3, 0, 0, 0}; } static ControlState Keccak0(uint8_t round) { return ControlState{4, 0, 0, round}; } static ControlState Keccak1(uint8_t round) { return ControlState{5, 0, 0, round}; } - static ControlState Keccak2(uint8_t round) { return ControlState{6, 0, 0, round}; } + static ControlState keccak(uint8_t round) { return ControlState{6, 0, 0, round}; } static ControlState Keccak3(uint8_t round) { return ControlState{7, 0, 0, round}; } static ControlState Keccak4(uint8_t round) { return ControlState{8, 0, 0, round}; } static ControlState ShaIn(uint8_t block, uint8_t round) { @@ -329,7 +329,7 @@ PreflightTrace preflightSegment(const std::vector& inputs, size_t c addCycle(ControlState::Keccak0(round), writeTheta(theta), kflatOffset, sflatOffset); theta_p2_rho_pi(kstate, theta); addCycle(ControlState::Keccak1(round), writeKeccak(kstate, false), kflatOffset, sflatOffset); - addCycle(ControlState::Keccak2(round), writeKeccak(kstate, true), kflatOffset, sflatOffset); + addCycle(ControlState::keccak(round), writeKeccak(kstate, true), kflatOffset, sflatOffset); chi_iota(kstate, round); addCycle(ControlState::Keccak3(round), writeKeccak(kstate, false), kflatOffset, sflatOffset); addCycle(ControlState::Keccak4(round), writeKeccak(kstate, true), kflatOffset, sflatOffset); @@ -371,4 +371,4 @@ void applyPreflight(ExecutionTrace& exec, const PreflightTrace& preflight) { } } -} // namespace zirgen::keccak2 +} // namespace zirgen::keccak diff --git a/zirgen/circuit/keccak2/cpp/preflight.h b/zirgen/circuit/keccak/cpp/preflight.h similarity index 90% rename from zirgen/circuit/keccak2/cpp/preflight.h rename to zirgen/circuit/keccak/cpp/preflight.h index e1164a2f..c4b8bdbf 100644 --- a/zirgen/circuit/keccak2/cpp/preflight.h +++ b/zirgen/circuit/keccak/cpp/preflight.h @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -14,9 +14,9 @@ #pragma once -#include "zirgen/circuit/keccak2/cpp/trace.h" +#include "zirgen/circuit/keccak/cpp/trace.h" -namespace zirgen::keccak2 { +namespace zirgen::keccak { struct ScatterInfo { uint32_t dataOffset; // Place to get the data from (as u32 words) @@ -40,4 +40,4 @@ struct PreflightTrace { PreflightTrace preflightSegment(const std::vector& inputs, size_t cycles); void applyPreflight(ExecutionTrace& exec, const PreflightTrace& preflight); -} // namespace zirgen::keccak2 +} // namespace zirgen::keccak diff --git a/zirgen/circuit/keccak2/cpp/trace.cpp b/zirgen/circuit/keccak/cpp/trace.cpp similarity index 94% rename from zirgen/circuit/keccak2/cpp/trace.cpp rename to zirgen/circuit/keccak/cpp/trace.cpp index dbea9d8f..ae3ebea2 100644 --- a/zirgen/circuit/keccak2/cpp/trace.cpp +++ b/zirgen/circuit/keccak/cpp/trace.cpp @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -12,11 +12,11 @@ // See the License for the specific language governing permissions and // limitations under the License. -#include "zirgen/circuit/keccak2/cpp/trace.h" +#include "zirgen/circuit/keccak/cpp/trace.h" #include -namespace zirgen::keccak2 { +namespace zirgen::keccak { TraceGroup::TraceGroup(size_t rows, size_t cols) : rows(rows), cols(cols), vec(rows * cols, Fp::invalid()), unsafeReads(false) {} @@ -84,4 +84,4 @@ void GlobalTraceGroup::setUnsafe(bool val) { ExecutionTrace::ExecutionTrace(size_t rows, const CircuitParams& params) : data(rows, params.dataCols), global(params.globalCols) {} -} // namespace zirgen::keccak2 +} // namespace zirgen::keccak diff --git a/zirgen/circuit/keccak2/cpp/trace.h b/zirgen/circuit/keccak/cpp/trace.h similarity index 94% rename from zirgen/circuit/keccak2/cpp/trace.h rename to zirgen/circuit/keccak/cpp/trace.h index f87abff8..960f06d9 100644 --- a/zirgen/circuit/keccak2/cpp/trace.h +++ b/zirgen/circuit/keccak/cpp/trace.h @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -20,7 +20,7 @@ #include "risc0/fp/fp.h" #include "risc0/fp/fpext.h" -namespace zirgen::keccak2 { +namespace zirgen::keccak { using Fp = risc0::Fp; using FpExt = risc0::FpExt; @@ -72,4 +72,4 @@ struct ExecutionTrace { GlobalTraceGroup global; }; -} // namespace zirgen::keccak2 +} // namespace zirgen::keccak diff --git a/zirgen/circuit/keccak2/cpp/wrap_dsl.cpp b/zirgen/circuit/keccak/cpp/wrap_dsl.cpp similarity index 98% rename from zirgen/circuit/keccak2/cpp/wrap_dsl.cpp rename to zirgen/circuit/keccak/cpp/wrap_dsl.cpp index 6d0134e6..47ad600f 100644 --- a/zirgen/circuit/keccak2/cpp/wrap_dsl.cpp +++ b/zirgen/circuit/keccak/cpp/wrap_dsl.cpp @@ -12,7 +12,7 @@ // See the License for the specific language governing permissions and // limitations under the License. -#include "zirgen/circuit/keccak2/cpp/wrap_dsl.h" +#include "zirgen/circuit/keccak/cpp/wrap_dsl.h" #include #include @@ -26,7 +26,7 @@ #include "risc0/core/util.h" -namespace zirgen::keccak2 { +namespace zirgen::keccak { namespace impl { @@ -270,7 +270,7 @@ Val extern_nextPreimage(ExecContext& ctx) { #pragma GCC diagnostic ignored "-Wunused-variable" #pragma GCC diagnostic ignored "-Wunused-but-set-variable" #endif -#include "zirgen/circuit/keccak2/keccak.cpp.inc" +#include "zirgen/circuit/keccak/keccak.cpp.inc" } // namespace impl @@ -298,4 +298,4 @@ void DslStep(StepHandler& stepHandler, ExecutionTrace& trace, size_t cycle) { step_Top(ctx, &data, &global); } -} // namespace zirgen::keccak2 +} // namespace zirgen::keccak diff --git a/zirgen/circuit/keccak2/cpp/wrap_dsl.h b/zirgen/circuit/keccak/cpp/wrap_dsl.h similarity index 89% rename from zirgen/circuit/keccak2/cpp/wrap_dsl.h rename to zirgen/circuit/keccak/cpp/wrap_dsl.h index 20713bb1..8d386554 100644 --- a/zirgen/circuit/keccak2/cpp/wrap_dsl.h +++ b/zirgen/circuit/keccak/cpp/wrap_dsl.h @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. @@ -15,11 +15,11 @@ #pragma once #include "risc0/core/util.h" -#include "zirgen/circuit/keccak2/cpp/preflight.h" +#include "zirgen/circuit/keccak/cpp/preflight.h" #include -namespace zirgen::keccak2 { +namespace zirgen::keccak { struct StepHandler { StepHandler(const PreflightTrace& trace, size_t cycle) : trace(trace), cycle(cycle) {} @@ -46,4 +46,4 @@ LayoutInfo getLayoutInfo(); CircuitParams getDslParams(); void DslStep(StepHandler& stepHandler, ExecutionTrace& trace, size_t cycle); -} // namespace zirgen::keccak2 +} // namespace zirgen::keccak diff --git a/zirgen/circuit/keccak2/is_zero.zir b/zirgen/circuit/keccak/is_zero.zir similarity index 100% rename from zirgen/circuit/keccak2/is_zero.zir rename to zirgen/circuit/keccak/is_zero.zir diff --git a/zirgen/circuit/keccak/keccak.zir b/zirgen/circuit/keccak/keccak.zir index 60d55858..0ea88141 100644 --- a/zirgen/circuit/keccak/keccak.zir +++ b/zirgen/circuit/keccak/keccak.zir @@ -1,1772 +1,206 @@ -// RUN: zirgen -I %S --test %s --input-data-hex 010000000000000054686520717569636B2062726F776E20666F78206A756D7073206F76657220746865206C617A7920646F672E0100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080578951e24efd62a3d63a86f7cd19aaa53c898fe287d2Q552133220370240b572d0000000000000000 +// RUN: zirgen -I %S --test %s -import sha256_for_keccak; +import bits; import one_hot; -extern GetCycle() : Val; -extern configureInput(bytesPerElem: Val); -extern readInput() : Val; - -// use_once_mem_arg.zir -extern SimpleMemoryPoke(index: Val, data: Val); -extern SimpleMemoryPeek(index: Val) : Val; -component MEM_DIGEST_LEN() { 4 } -argument UseOnceMemoryElement(_count: Val, _index: Val, - arw: Array) { - public count := NondetReg(_count); - public index := NondetReg(_index); - public digest0 := NondetReg(arw[0]); - public digest1 := NondetReg(arw[1]); - public digest2 := NondetReg(arw[2]); - public digest3 := NondetReg(arw[3]); - //digest := [d1,d2,d3,d4]; // error: does not own the layout of member -} -component ReadMemory(i: Val, ar: Array) { - digest := for elemIdx : 0..MEM_DIGEST_LEN() { - SimpleMemoryPeek(i * MEM_DIGEST_LEN() + elemIdx) - }; - elem := UseOnceMemoryElement(-1, i, digest); - AliasLayout!(elem.digest0, ar[0]); - AliasLayout!(elem.digest1, ar[1]); - AliasLayout!(elem.digest2, ar[2]); - AliasLayout!(elem.digest3, ar[3]); - AliasLayout!(elem.index, ar[4]); -} -component WriteMemory(idx: Reg, aw: Array) { - for elemIdx : 0..MEM_DIGEST_LEN() { - SimpleMemoryPoke(idx * MEM_DIGEST_LEN() + elemIdx, aw[elemIdx]); - }; - elem := UseOnceMemoryElement(1, idx, aw); - elem.count = 1; - AliasLayout!(idx, elem.index); - AliasLayout!(elem.digest0, aw[0]); - AliasLayout!(elem.digest1, aw[1]); - AliasLayout!(elem.digest2, aw[2]); - AliasLayout!(elem.digest3, aw[3]); -} -// EOF use_once_mem_arg.zir - -// po2.zir unpacking up to 31 bits -component Po2(n: Val) { - arr := [ - 0x1, - 0x2, - 0x4, - 0x8, - 0x10, - 0x20, - 0x40, - 0x80, - 0x100, - 0x200, - 0x400, - 0x800, - 0x1000, - 0x2000, - 0x4000, - 0x8000, - 0x10000, - 0x20000, - 0x40000, - 0x80000, - 0x100000, - 0x200000, - 0x400000, - 0x800000, - 0x1000000, - 0x2000000, - 0x4000000, - 0x8000000, - 0x10000000, - 0x20000000, - 0x40000000 - ]; - arr[n] -} -component ToBitsU(x: Val) { - for i : 0..n { NondetReg((x & Po2(i)) / Po2(i)) } -} -component ToBits(x: Val) { - for i : 0..n { NondetBitReg((x & Po2(i)) / Po2(i)) } -} -component FromBits(bits: Array) { - reduce for i : 0..n { Po2(i) * bits[i] } init 0 with Add -} -component OneHotU(v: Val) { - // Make N bit registers, with bit v set and all others 0 - public bits := for i : 0..N { NondetReg(Isz(i - v)) }; - // Verify exactly one bit is set - reduce bits init 0 with Add = 1; - // Verify the right bit is set - reduce for i : 0..N { bits[i] * i } init 0 with Add = v; - bits -} -// EOF po2.zir - -// concatenate.zir -component vConcatenate(a: Array, b: Array) { - for i : 0..(N + M) { - low := InRange(0, i, N); - [low, 1-low] -> (a[i], b[i-N]) +import xor5; +import arr; +import pack; + +// Computes the xor5 part of Theta, results are 'bits' and can be aliased +component ThetaP1(a: Array, 5>, 5>) { + for j : 0..5 { + for k : 0..64 { + Xor5(for i : 0..5 { a[i][j][k] } ) + } } } -component Concatenate(a: Array, b: Array) { - result := for i : 0..(N + M) { - low := InRange(0, i, N); - NondetReg([low, 1-low] -> (a[i], b[i-N])) - }; - for i : 0..N { AliasLayout!(a[i], result[i]); }; - for i : N..M+N { AliasLayout!(b[i-N], result[i]); }; - result -} -component ConcatZeros(a: Array) { - result := for i : 0..(N + M) { - low := InRange(0, i, N); - NondetReg([low, 1-low] -> (low*a[i], 0) ) - }; - for i : 0..N { AliasLayout!(a[i], result[i]); }; - result -} -component ConcatElem(a: Array, b: NondetReg) { - result := for i : 0..(N + 1) { - low := InRange(0, i, N); - NondetReg([low, 1-low] -> (a[i], b)) - }; - for i : 0..N { AliasLayout!(a[i], result[i]); }; - AliasLayout!(b, result[N]); - result -} -// EOF concatenate.zir - -component MAJOR_EXTRA() { 17 } -component MINOR_1STCYC() { 5 } -component S2MAJOR_SETUP() { 16 } -component S2MAJOR_LOAD() { 18 } -component S2MAJOR_MIX() { 19 } -component S2MINOR_SKIP() { 1 } -component S2MINOR_INIT() { 0 } -component S2MINOR_FINI() { 4 } -component S2MINOR_OUTPUT() { 8 } - -component AUXLEN() { 16 } -component AUXBIN() { 11 } -component BLEN() { 22 } -component SLEN() { 21 } -component INPLEN() { 75 } -component EREGLEN() { 15 } -component RLEN() { INPLEN()+EREGLEN()-3*BLEN() } -component dummyB() { for i : 0.. BLEN() { NondetReg(0) } } -component dummyS() { for i : 0.. SLEN() { NondetReg(0) } } -component dummyE() { for i : 0.. RLEN() { NondetReg(0) } } -component WORDLEN() { 16 } -component BABYMAX() { 30 } - -component RetTuple(a: Array, - b: Array, - c: Array, - d: Array, - e: Array, - f: Array, - minor_count: Val, - major_count: Val, - round: Val, - block: Val, - memIdx: Val, - auxregs: Array) { - public arr_a := for elem : a { NondetReg(elem) }; AliasLayout!(a, arr_a); - public arr_b := for elem : b { NondetReg(elem) }; AliasLayout!(b, arr_b); - public arr_c := for elem : c { NondetReg(elem) }; AliasLayout!(c, arr_c); - public arr_d := for elem : d { NondetReg(elem) }; AliasLayout!(d, arr_d); - public arr_e := for elem : e { NondetReg(elem) }; AliasLayout!(e, arr_e); - public arr_f := for elem : f { NondetReg(elem) }; AliasLayout!(f, arr_f); - public minor := Reg(minor_count); - public major := Reg(major_count); - public rnd := Reg(round); - public blk := Reg(block); - public midx := Reg(memIdx); - public auxr := for elem : auxregs { NondetReg(elem) }; AliasLayout!(auxregs, auxr); -} - -component RGZ(arr: Array) { - for i : 0..N { Reg(arr[i]) } -} - -component rctable(idx: Val) { - arr := [ [[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[0,1,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[1,1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[1,0,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[0,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[0,0,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[1,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[1,1,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[1,1,0,1,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[1,0,0,1,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[1,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[0,1,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[1,0,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]], - [[1,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0]], - [[0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0], - [0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0]] ]; - arr[idx] -} - -component rot_table() { - arr := [ [0,0,0], [1,0,0], [21,21,20], [21,7,0], [21,6,0], - [21,15,0], [21,21,2], [6,0,0], [21,21,13], [20,0,0], - [3,0,0], [10,0,0], [21,21,1], [21,4,0], [21,18,0], - [21,20,0], [21,21,3], [15,0,0], [21,0,0], [8,0,0], - [18,0,0], [2,0,0], [21,21,19], [21,21,14], [14,0,0]]; - arr[5*y + x] -} - -component xor3(x: Val, y: Val, z: Val) { - ((x*y + (1-x)*(1-y)) * z) + ((1-(x*y + (1-x)*(1-y))) * (1-z)) -} - -component xor2(x: Val, y: Val) { - x + y - 2*x*y -} - -component andnxor(x: Val, y: Val, z: Val) { - t := (1-y)*z; // (not y) and z - x + t - 2*x*t // x xor t -} - -component IncMod5(v: Val) { - d := Isz(4-v); - [1-d, d] -> (v+1, 0) -} -component DecMod5(v: Val) { - d := Isz(v); - [1-d, d] -> (v-1, 4) -} - -component WordTriple(_a: Array, - _b: Array, - _c: Array) { - a := for elem : _a { NondetReg(elem) }; AliasLayout!(a, _a); - b := for elem : _b { NondetReg(elem) }; AliasLayout!(b, _b); - c := for elem : _c { NondetReg(elem) }; AliasLayout!(c, _c); -} -component RotLeft3impl - (a: Array, b: Array, c: Array) { - public ra := for i : 0..A { - wraparound := InRange(0,i,S); - NondetReg([wraparound,1-wraparound] -> (c[C-S+i],a[i-S]))}; - for i : 0..S { AliasLayout!(c[C-S+i], ra[i]); }; - for i : S..A { AliasLayout!(a[i-S], ra[i]); }; - public rb := for i : 0..B { - wraparound := InRange(0,i,S); - NondetReg([wraparound,1-wraparound] -> (a[A-S+i],b[i-S]))}; - for i : 0..S { AliasLayout!(a[A-S+i], rb[i]); }; - for i : S..B { AliasLayout!(b[i-S], rb[i]); }; - public rc := for i : 0..C { - wraparound := InRange(0,i,S); - NondetReg([wraparound,1-wraparound] -> (b[B-S+i],c[i-S]))}; - for i : 0..S { AliasLayout!(b[B-S+i], rc[i]); }; - for i : S..C { AliasLayout!(c[i-S], rc[i]); }; -} -component RotLeft3 - (a: Array, b: Array, c: Array) { - za := Isz(S1); - rot := [za, 1-za] -> ( WordTriple(a,b,c), - { arr1 := RotLeft3impl(a, b, c); - zb := Isz(S2); - [zb, 1-zb] -> ( WordTriple(arr1.ra, arr1.rb, arr1.rc), - { arr2 := RotLeft3impl(arr1.ra, arr1.rb, arr1.rc); - zc := Isz(S3); - [zc, 1-zc] -> ( WordTriple(arr2.ra, arr2.rb, arr2.rc), - { arr3 := RotLeft3impl(arr2.ra, arr2.rb, arr2.rc); - WordTriple(arr3.ra, arr3.rb, arr3.rc) - })})}); -} -component vRotLeft3impl - (a: Array, b: Array, c: Array) { - public ra := for i : 0..A { - wraparound := InRange(0,i,S); - [wraparound,1-wraparound] -> (c[C-S+i],a[i-S])}; - public rb := for i : 0..B { - wraparound := InRange(0,i,S); - [wraparound,1-wraparound] -> (a[A-S+i],b[i-S])}; - public rc := for i : 0..C { - wraparound := InRange(0,i,S); - [wraparound,1-wraparound] -> (b[B-S+i],c[i-S])}; -} -component vRotLeft3 - (a: Array, b: Array, c: Array) { - za := Isz(S1); - public packed := [za, 1-za] -> ( - [FromBits(a),FromBits(b),FromBits(c)], - { arr1 := vRotLeft3impl(a, b, c); - zb := Isz(S2); - [zb, 1-zb] -> ( - [FromBits(arr1.ra),FromBits(arr1.rb),FromBits(arr1.rc)], - { arr2 := vRotLeft3impl(arr1.ra, arr1.rb, arr1.rc); - zc := Isz(S3); - [zc, 1-zc] -> ( - [FromBits(arr2.ra),FromBits(arr2.rb),FromBits(arr2.rc)], - { arr3 := vRotLeft3impl(arr2.ra, arr2.rb, arr2.rc); - [FromBits(arr3.ra),FromBits(arr3.rb),FromBits(arr3.rc)] - })})}); -} - -component xor5words_resvals(rvpst: RetTuple) { - val_a := rvpst.arr_a[Sidx+3*Xidx+15*0]; - nxt_b := Isz(Xidx)+Isz(Xidx-1)+Isz(Xidx-2)*Isz(Sidx); - val_b := [nxt_b, 1-nxt_b] -> - (rvpst.arr_a[Sidx+3*Xidx+15*1], - rvpst.arr_b[Sidx+3*Xidx+15*1 - 22*1]); - nxt_c := Isz(4-Xidx)*Isz(2-Sidx); - val_c := [1-nxt_c, nxt_c] -> - (rvpst.arr_b[Sidx+3*Xidx+15*2 - 22*1], - rvpst.arr_c[Sidx+3*Xidx+15*2 - 22*2]); - val_d := rvpst.arr_c[Sidx+3*Xidx+15*3 - 22*2]; - nxt_e := Isz(Xidx)+Isz(Xidx-1); - val_e := [nxt_e, 1-nxt_e] -> - (rvpst.arr_c[Sidx+3*Xidx+15*4 - 22*2], - rvpst.arr_d[Sidx+3*Xidx+15*4 - 22*3]); - [val_a, val_b, val_c, val_d, val_e] -} - -component xor5words_result(rvpst: RetTuple) { - CURRLEN := [Isz(Sidx), 1-Isz(Sidx)] -> (BLEN(), SLEN()); - public minor_onehot := OneHotU<5>(rvpst.minor); - vals := minor_onehot -> ( xor5words_resvals<0,Sidx>(rvpst), - xor5words_resvals<1,Sidx>(rvpst), - xor5words_resvals<2,Sidx>(rvpst), - xor5words_resvals<3,Sidx>(rvpst), - xor5words_resvals<4,Sidx>(rvpst)); - val_a := vals[0]; - public unpack_a := ToBits(val_a); - FromBits(unpack_a) = val_a; - - val_b := vals[1]; - public unpack_b := ToBits(val_b); - FromBits(unpack_b) = val_b; - - val_c := vals[2]; - public unpack_c := ToBits(val_c); - FromBits(unpack_c) = val_c; - - val_d := vals[3]; - public unpack_d := ToBits(val_d); - FromBits(unpack_d) = val_d; - - val_e := vals[4]; - public unpack_e := ToBitsU(val_e); - FromBits(unpack_e) = val_e; - - public resbits := for i : 0..CURRLEN { - NondetReg(1 & (unpack_a[i] + unpack_b[i] + unpack_c[i] + - unpack_d[i] + unpack_e[i])) }; - - diff := for i : 0..CURRLEN { - unpack_a[i] + unpack_b[i] + unpack_c[i] + - unpack_d[i] + unpack_e[i] - resbits[i] }; - - for i : 0 .. CURRLEN { - 0 = diff[i] * (diff[i]-2) * (diff[i]-4); }; - - FromBits(resbits) -} - -component xor5words_minor0(rvprev: RetTuple) { - r := xor5words_result<0>(rvprev); - result := Reg(r); - withr_d := Concatenate(r.unpack_d, [result, NondetReg(0)]); - aux_regs := ConcatZeros<5,AUXLEN()-5>(r.minor_onehot); - RetTuple(r.unpack_a, r.unpack_b, r.unpack_c, withr_d, r.unpack_e, r.resbits, - rvprev.minor, 1, rvprev.rnd, rvprev.blk, rvprev.midx, aux_regs) -} - -component xor5words_minor1(rvals: RetTuple) { - rvp01 := rvals@1; - rvpst := rvals@2; - r := xor5words_result<1>(rvpst); - result := Reg(r); - withr_a := ConcatElem(r.unpack_a, Reg(rvp01.arr_d[0+BLEN()])); - withr_b := ConcatElem(r.unpack_b, result); - zc := ConcatZeros(r.unpack_c); - zd := ConcatZeros(r.unpack_d); - ze := ConcatZeros(r.unpack_e); - zx := ConcatZeros(r.resbits); - aux_regs := ConcatZeros<5,AUXLEN()-5>(r.minor_onehot); - RetTuple(withr_a, withr_b, zc, zd, ze, zx, - rvp01.minor, 2, rvp01.rnd, rvp01.blk, rvp01.midx, aux_regs) -} - -component xor5words_minor2(rvals: RetTuple) { - rvp01 := rvals@1; - rvpst := rvals@3; - r := xor5words_result<2>(rvpst); - result := Reg(r); - withr_a := ConcatElem(r.unpack_a, Reg(rvp01.arr_a[0+SLEN()])); - withr_b := ConcatElem(r.unpack_b, Reg(rvp01.arr_b[0+SLEN()])); - withr_c := ConcatElem(r.unpack_c, result); - zd := ConcatZeros(r.unpack_d); - ze := ConcatZeros(r.unpack_e); - zx := ConcatZeros(r.resbits); - aux_regs := ConcatZeros<5,AUXLEN()-5>(r.minor_onehot); - RetTuple(withr_a, withr_b, withr_c, zd, ze, zx, - rvp01.minor, 3, rvp01.rnd, rvp01.blk, rvp01.midx, aux_regs) -} - -component xor5words_m3impl(rvals: RetTuple, - auxr: Array) { - rvprev01 := rvals@1; - rvprev04 := rvals@4; - inp_a := RGZ(rvprev04.arr_a); - inp_b := RGZ(rvprev04.arr_b); - inp_c := RGZ(rvprev04.arr_c); - rs := [Reg(rvprev01.arr_a[BLEN()-1]), - Reg(rvprev01.arr_b[BLEN()-1]), - Reg(rvprev01.arr_c[BLEN()-1])]; - L := INPLEN()-BLEN()*3+3*Xidx; - tmp_1 := for i : 0..L { Reg(rvprev04.arr_d[i]) }; - tmp_2 := Concatenate(tmp_1, rs); - inp_d := ConcatZeros(tmp_2); - Z := Isz(Xidx-4); - [1-Z, Z] -> ( - RetTuple(inp_a, inp_b, inp_c, inp_d, dummyB(), dummyB(), - Xidx+1, 0, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr), - RetTuple(inp_a, inp_b, inp_c, inp_d, dummyB(), dummyB(), - 0, 4, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr)) -} - -component xor5words_minor3(rvals: RetTuple) { - minor_onehot := OneHotU<5>(rvals@1.minor); - aux_regs := ConcatZeros<5,AUXLEN()-5>(minor_onehot); - minor_onehot -> ( - xor5words_m3impl<0>(rvals, aux_regs), - xor5words_m3impl<1>(rvals, aux_regs), - xor5words_m3impl<2>(rvals, aux_regs), - xor5words_m3impl<3>(rvals, aux_regs), - xor5words_m3impl<4>(rvals, aux_regs)) -} - -component rho_minor0(rvals: RetTuple, - auxr: Array) { - rvpstate := rvals@(1+3*(X/2)); //X=0,pstate=1 X=2,pstate=4, X=4,pstate=7 - rvprev01 := rvals@1; - - v_dec1 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*DecMod5(X)+0]; - unpack_m1 := ToBitsU(v_dec1); - FromBits(unpack_m1) = v_dec1; - last_m1 := unpack_m1[BLEN()-1]; - last_m1 * (1-last_m1) = 0; - - v_dec2 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*DecMod5(X)+1]; - unpack_m2 := ToBitsU(v_dec2); - FromBits(unpack_m2) = v_dec2; - padded_m2 := ConcatZeros(unpack_m2); - - v_dec3 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*DecMod5(X)+2]; - unpack_m3 := ToBitsU(v_dec3); - FromBits(unpack_m3) = v_dec3; - padded_m3 := ConcatZeros(unpack_m3); - - v_inc1 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*IncMod5(X)+0]; - unpack_p1 := ToBitsU(v_inc1); - FromBits(unpack_p1) = v_inc1; - last_p1 := unpack_p1[BLEN()-1]; - last_p1 * (1-last_p1) = 0; - - v_inc2 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*IncMod5(X)+1]; - unpack_p2 := ToBitsU(v_inc2); - FromBits(unpack_p2) = v_inc2; - - v_inc3 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*IncMod5(X)+2]; - unpack_p3 := ToBitsU(v_inc3); - FromBits(unpack_p3) = v_inc3; - - rotp := RotLeft3impl( - unpack_p1, unpack_p2, unpack_p3); - pad_rb := ConcatZeros(rotp.rb); - pad_rc := ConcatZeros(rotp.rc); - - padded_m1 := ConcatZeros(unpack_m1); - RetTuple(rotp.ra, pad_rb, pad_rc, padded_m1, padded_m2, padded_m3, - 3*(X/2)+1, Y+4, rvpstate.rnd, rvpstate.blk, rvpstate.midx, auxr) -} - -component rho_minor1(rvals: RetTuple, - auxr: Array) { - rvpstate := rvals@(2+3*(X/2)); //X=0,pstate=2 X=2,pstate=5, X=4,pstate=8 - rvprev01 := rvals@1; - - idx1 := (X+5*Y)*3 + 0; - in_a := InRange(0,idx1,BLEN()); - v_xy1 := [in_a, 1-in_a] -> (rvpstate.arr_a[idx1], - { idx2 := idx1 - BLEN(); - in_b := InRange(0,idx2,BLEN()); - [in_b, 1-in_b] -> (rvpstate.arr_b[idx2], - { idx3 := idx2 - BLEN(); - in_c := InRange(0,idx3,BLEN()); - [in_c, 1-in_c] -> (rvpstate.arr_c[idx3], - rvpstate.arr_d[idx3-BLEN()]) })}); - unpack_xy1 := ToBitsU(v_xy1); - FromBits(unpack_xy1) = v_xy1; - last_xy1 := unpack_xy1[BLEN()-1]; - last_xy1 * (1-last_xy1) = 0; - - idx12 := idx1 + 1; - in_a2 := InRange(0,idx12,BLEN()); - v_xy2 := [in_a2, 1-in_a2] -> (rvpstate.arr_a[idx12], - { idx22 := idx12 - BLEN(); - in_b2 := InRange(0,idx22,BLEN()); - [in_b2, 1-in_b2] -> (rvpstate.arr_b[idx22], - { idx32 := idx22 - BLEN(); - in_c2 := InRange(0,idx32,BLEN()); - [in_c2, 1-in_c2] -> (rvpstate.arr_c[idx32], - rvpstate.arr_d[idx32-BLEN()]) })}); - unpack_xy2 := ToBitsU(v_xy2); - FromBits(unpack_xy2) = v_xy2; - - idx13 := idx12 + 1; - in_a3 := InRange(0,idx13,BLEN()); - v_xy3 := [in_a3, 1-in_a3] -> (rvpstate.arr_a[idx13], - { idx23 := idx13 - BLEN(); - in_b3 := InRange(0,idx23,BLEN()); - [in_b3, 1-in_b3] -> (rvpstate.arr_b[idx23], - { idx33 := idx23 - BLEN(); - in_c3 := InRange(0,idx33,BLEN()); - [in_c3, 1-in_c3] -> (rvpstate.arr_c[idx33], - rvpstate.arr_d[idx33-BLEN()]) })}); - unpack_xy3 := ToBitsU(v_xy3); - FromBits(unpack_xy3) = v_xy3; - - xor_1 := for i : 0..BLEN() { - xor3(unpack_xy1[i], rvprev01.arr_a[i], rvprev01.arr_d[i]) }; - xor_2 := for i : 0..SLEN() { - xor3(unpack_xy2[i], rvprev01.arr_b[i], rvprev01.arr_e[i]) }; - xor_3 := for i : 0..SLEN() { - xor3(unpack_xy3[i], rvprev01.arr_c[i], rvprev01.arr_f[i]) }; - t := rot_table(); - rotxor := vRotLeft3( - xor_1, xor_2, xor_3); - - result := [Reg(rotxor.packed[0]), - Reg(rotxor.packed[1]), - Reg(rotxor.packed[2])]; - withrs_d := Concatenate(unpack_xy3, result); - padded_xy2 := ConcatZeros(unpack_xy2); - - [Isz(X-4), 1-Isz(X-4)] -> ( - RetTuple(dummyB(), dummyB(), dummyB(), withrs_d, padded_xy2, unpack_xy1, - 3*(4/2)+2, Y+4, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr), - { v_dec1 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*DecMod5(X+1)+0]; - unpack_m1 := ToBitsU(v_dec1); - FromBits(unpack_m1) = v_dec1; - last_m1 := unpack_m1[BLEN()-1]; - last_m1 * (1-last_m1) = 0; - - v_dec2 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*DecMod5(X+1)+1]; - unpack_m2 := ToBitsU(v_dec2); - FromBits(unpack_m2) = v_dec2; - padded_m2 := ConcatZeros(unpack_m2); - - v_dec3 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*DecMod5(X+1)+2]; - unpack_m3 := ToBitsU(v_dec3); - FromBits(unpack_m3) = v_dec3; - padded_m3 := ConcatZeros(unpack_m3); - - RetTuple(unpack_m1, padded_m2, padded_m3, withrs_d, - padded_xy2, unpack_xy1, 3*(X/2)+2, Y+4, - rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - }) -} -component rho_minor2(rvals: RetTuple, - auxr: Array) { - rvpstate := rvals@(3+3*(X/2)); //X=0,pstate=3 X=2,pstate=6 - rvprev01 := rvals@1; - - v_inc1 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*IncMod5(X+1)+0]; - unpack_p1 := ToBitsU(v_inc1); - FromBits(unpack_p1) = v_inc1; - last_p1 := unpack_p1[BLEN()-1]; - last_p1 * (1-last_p1) = 0; - - v_inc2 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*IncMod5(X+1)+1]; - unpack_p2 := ToBitsU(v_inc2); - FromBits(unpack_p2) = v_inc2; - - v_inc3 := rvpstate.arr_d[INPLEN()-3*BLEN()+3*IncMod5(X+1)+2]; - unpack_p3 := ToBitsU(v_inc3); - FromBits(unpack_p3) = v_inc3; - - rotp := RotLeft3impl( - unpack_p1, unpack_p2, unpack_p3); - - idx1 := (X+1+5*Y)*3 + 0; - in_a := InRange(0,idx1,BLEN()); - v_xy1 := [in_a, 1-in_a] -> (rvpstate.arr_a[idx1], - { idx2 := idx1 - BLEN(); - in_b := InRange(0,idx2,BLEN()); - [in_b, 1-in_b] -> (rvpstate.arr_b[idx2], - { idx3 := idx2 - BLEN(); - in_c := InRange(0,idx3,BLEN()); - [in_c, 1-in_c] -> (rvpstate.arr_c[idx3], - rvpstate.arr_d[idx3-BLEN()]) })}); - unpack_xy1 := ToBitsU(v_xy1); - FromBits(unpack_xy1) = v_xy1; - last_xy1 := unpack_xy1[BLEN()-1]; - last_xy1 * (1-last_xy1) = 0; - - idx12 := idx1 + 1; - in_a2 := InRange(0,idx12,BLEN()); - v_xy2 := [in_a2, 1-in_a2] -> (rvpstate.arr_a[idx12], - { idx22 := idx12 - BLEN(); - in_b2 := InRange(0,idx22,BLEN()); - [in_b2, 1-in_b2] -> (rvpstate.arr_b[idx22], - { idx32 := idx22 - BLEN(); - in_c2 := InRange(0,idx32,BLEN()); - [in_c2, 1-in_c2] -> (rvpstate.arr_c[idx32], - rvpstate.arr_d[idx32-BLEN()]) })}); - unpack_xy2 := ToBitsU(v_xy2); - FromBits(unpack_xy2) = v_xy2; - - idx13 := idx12 + 1; - in_a3 := InRange(0,idx13,BLEN()); - v_xy3 := [in_a3, 1-in_a3] -> (rvpstate.arr_a[idx13], - { idx23 := idx13 - BLEN(); - in_b3 := InRange(0,idx23,BLEN()); - [in_b3, 1-in_b3] -> (rvpstate.arr_b[idx23], - { idx33 := idx23 - BLEN(); - in_c3 := InRange(0,idx33,BLEN()); - [in_c3, 1-in_c3] -> (rvpstate.arr_c[idx33], - rvpstate.arr_d[idx33-BLEN()]) })}); - unpack_xy3 := ToBitsU(v_xy3); - FromBits(unpack_xy3) = v_xy3; - - xor_1 := for i : 0..BLEN() { - xor3(unpack_xy1[i], rvprev01.arr_a[i], rotp.ra[i]) }; - xor_2 := for i : 0..SLEN() { - xor3(unpack_xy2[i], rvprev01.arr_b[i], rotp.rb[i]) }; - xor_3 := for i : 0..SLEN() { - xor3(unpack_xy3[i], rvprev01.arr_c[i], rotp.rc[i]) }; - t := rot_table(); - rotxor := vRotLeft3( - xor_1, xor_2, xor_3); - - result := [Reg(rotxor.packed[0]), - Reg(rotxor.packed[1]), - Reg(rotxor.packed[2])]; - withrs_d := Concatenate(unpack_xy3, result); - padded_xy2 := ConcatZeros(unpack_xy2); - padded_p2 := ConcatZeros(unpack_p2); - padded_p3 := ConcatZeros(unpack_p3); - - RetTuple(unpack_p1, padded_p2, padded_p3, withrs_d, padded_xy2, unpack_xy1, - 3*(X/2)+3, Y+4, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) +// Computes part 2 of theta, results are not by register +component ThetaP2(a: Array, 5>, 5>, c: Array, 5>) { + d := for j : 0..5 { + for k : 0..64 { + jm1 := if (Isz(j)) { 4 } else { j - 1 }; + jp1 := if (Isz(j-4)) { 0 } else { j + 1 }; + kp1 := if (Isz(k)) { 63 } else { k - 1 }; + BitXor(c[jm1][k], c[jp1][kp1]) + } + }; + for i : 0..5 { + for j : 0..5 { + for k : 0..64 { + BitXor(a[i][j][k], d[j][k]) + } + } + } } -component rho_minor3(rvals: RetTuple, - auxr: Array) { - rvp01 := rvals@1; - rvp03 := rvals@3; - rvp04 := rvals@4; - rvp06 := rvals@6; - rvp07 := rvals@7; - rvpst := rvals@9; - - A := SLEN() + 0; - B := SLEN() + 1; - C := SLEN() + 2; - D := SLEN() + 3; - [Isz(Y), 1-Isz(Y)] -> ( - { rs1 := Concatenate<12,3>( - Concatenate<9,3>( - Concatenate<6,3>( - Concatenate<3,3>( - for i : A..D { Reg(rvp07.arr_d[i]) }, - for i : A..D { Reg(rvp06.arr_d[i]) }), - for i : A..D { Reg(rvp04.arr_d[i]) }), - for i : A..D { Reg(rvp03.arr_d[i]) }), - for i : A..D { Reg(rvp01.arr_d[i]) }); - a := Concatenate<15, 7>(rs1, for i : 15..22 { Reg(rvpst.arr_a[i]) }); - RetTuple(a, RGZ(rvpst.arr_b), RGZ(rvpst.arr_c), - RGZ(rvpst.arr_d), dummyB(), dummyB(), - 0, 5, rvp01.rnd, rvp01.blk, rvp01.midx, auxr) - }, - [Isz(Y-1), 1-Isz(Y-1)] -> ( - { rs1 := [Reg(rvp07.arr_d[A]), Reg(rvp07.arr_d[B]), Reg(rvp07.arr_d[C]), - Reg(rvp06.arr_d[A]), Reg(rvp06.arr_d[B]), Reg(rvp06.arr_d[C]), - Reg(rvp04.arr_d[A])]; - a := Concatenate<15, 7>(for i : 0..15 { Reg(rvpst.arr_a[i]) }, rs1); - rs2 := [Reg(rvp04.arr_d[B]), Reg(rvp04.arr_d[C]), - Reg(rvp03.arr_d[A]), Reg(rvp03.arr_d[B]), Reg(rvp03.arr_d[C]), - Reg(rvp01.arr_d[A]), Reg(rvp01.arr_d[B]), Reg(rvp01.arr_d[C])]; - b := Concatenate<8, 14>(rs2, for i : 8..22 { Reg(rvpst.arr_b[i]) }); - RetTuple(a, b, RGZ(rvpst.arr_c), RGZ(rvpst.arr_d), - dummyB(), dummyB(), - 0, 6, rvp01.rnd, rvp01.blk, rvp01.midx, auxr) - }, - [Isz(Y-2), 1-Isz(Y-2)] -> ( - { rs1 := [ - Reg(rvp07.arr_d[A]),Reg(rvp07.arr_d[B]), Reg(rvp07.arr_d[C]), - Reg(rvp06.arr_d[A]),Reg(rvp06.arr_d[B]), Reg(rvp06.arr_d[C]), - Reg(rvp04.arr_d[A]),Reg(rvp04.arr_d[B]), Reg(rvp04.arr_d[C]), - Reg(rvp03.arr_d[A]),Reg(rvp03.arr_d[B]), Reg(rvp03.arr_d[C]), - Reg(rvp01.arr_d[A]),Reg(rvp01.arr_d[B])]; - b := Concatenate<8, 14>(for i : 0..8 { Reg(rvpst.arr_b[i]) }, rs1); - rs2 := for i : 2..3 { Reg(rvp01.arr_d[SLEN()+i]) }; - c := Concatenate<1, 21>(rs2, for i : 1..22 { Reg(rvpst.arr_c[i]) }); - RetTuple(RGZ(rvpst.arr_a), b, c, RGZ(rvpst.arr_d), - dummyB(), dummyB(), 0, 7, rvp01.rnd, rvp01.blk, rvp01.midx, auxr) - }, - [Isz(Y-3), 1-Isz(Y-3)] -> ( - { rs1 := [//Reg(rvpst.arr_c[0]), TODO - Reg(rvp07.arr_d[A]),Reg(rvp07.arr_d[B]), Reg(rvp07.arr_d[C]), - Reg(rvp06.arr_d[A]),Reg(rvp06.arr_d[B]), Reg(rvp06.arr_d[C]), - Reg(rvp04.arr_d[A]),Reg(rvp04.arr_d[B]), Reg(rvp04.arr_d[C]), - Reg(rvp03.arr_d[A]),Reg(rvp03.arr_d[B]), Reg(rvp03.arr_d[C]), - Reg(rvp01.arr_d[A]),Reg(rvp01.arr_d[B]), Reg(rvp01.arr_d[C])]; - c1 := Concatenate<1, 15>([Reg(rvpst.arr_c[0])], rs1); - c := Concatenate<16, 6>( - c1, for i : 16..22 { Reg(rvpst.arr_c[i]) }); - RetTuple(RGZ(rvpst.arr_a), RGZ(rvpst.arr_b), - c, RGZ(rvpst.arr_d), dummyB(), dummyB(), - 0, 8, rvp01.rnd, rvp01.blk, rvp01.midx, auxr) - }, - { // Keccak pi permuation: -//c': arr_c[0,1,2,3,...,15],p07d[0],p07d[1],p07d[2],p06d[0],p06d[1],p06d[2] -//d': p04d[0],p04d[1],p04d[2],p03d[0],p03d[1],p03d[2],p01d[0],p01d[1],p01d[2] - a := [ - //B(0,0)=A(0,0) - Reg(rvpst.arr_a[0]),Reg(rvpst.arr_a[1]),Reg(rvpst.arr_a[2]), - //B(1,0)=A(1,1) - Reg(rvpst.arr_a[18]),Reg(rvpst.arr_a[19]),Reg(rvpst.arr_a[20]), - //B(2,0)=A(2,2) - Reg(rvpst.arr_b[14]),Reg(rvpst.arr_b[15]),Reg(rvpst.arr_b[16]), - //B(3,0)=A(3,3) - Reg(rvpst.arr_c[10]),Reg(rvpst.arr_c[11]),Reg(rvpst.arr_c[12]), - //B(4,0)=A(4,4) - Reg(rvp01.arr_d[A]),Reg(rvp01.arr_d[B]),Reg(rvp01.arr_d[C]), - //B(0,1)=A(3,0) - Reg(rvpst.arr_a[9]),Reg(rvpst.arr_a[10]),Reg(rvpst.arr_a[11]), - //B(1,1)=A(4,1) - Reg(rvpst.arr_b[5]),Reg(rvpst.arr_b[6]),Reg(rvpst.arr_b[7]), - //B(2,1)=A(0,2) - Reg(rvpst.arr_b[8]) ]; - b := [ - //B(2,1)=A(0,2) - Reg(rvpst.arr_b[9]), Reg(rvpst.arr_b[10]), - //B(3,1)=A(1,3) - Reg(rvpst.arr_c[4]),Reg(rvpst.arr_c[5]),Reg(rvpst.arr_c[6]), - //B(4,1)=A(2,4) - Reg(rvp04.arr_d[A]),Reg(rvp04.arr_d[B]),Reg(rvp04.arr_d[C]), - //B(0,2)=A(1,0) - Reg(rvpst.arr_a[3]),Reg(rvpst.arr_a[4]),Reg(rvpst.arr_a[5]), - //B(1,2)=A(2,1) - Reg(rvpst.arr_a[21]),Reg(rvpst.arr_b[0]),Reg(rvpst.arr_b[1]), - //B(2,2)=A(3,2) - Reg(rvpst.arr_b[17]),Reg(rvpst.arr_b[18]),Reg(rvpst.arr_b[19]), - //B(3,2)=A(4,3) - Reg(rvpst.arr_c[13]),Reg(rvpst.arr_c[14]),Reg(rvpst.arr_c[15]), - //B(4,2)=A(0,4) - Reg(rvp07.arr_d[A]),Reg(rvp07.arr_d[B]) ]; - c := [ - //B(4,2)=A(0,4) - Reg(rvp07.arr_d[C]), - //B(0,3)=A(4,0) - Reg(rvpst.arr_a[12]),Reg(rvpst.arr_a[13]),Reg(rvpst.arr_a[14]), - //B(1,3)=A(0,1) - Reg(rvpst.arr_a[15]),Reg(rvpst.arr_a[16]),Reg(rvpst.arr_a[17]), - //B(2,3)=A(1,2) - Reg(rvpst.arr_b[11]),Reg(rvpst.arr_b[12]),Reg(rvpst.arr_b[13]), - //B(3,3)=A(2,3) - Reg(rvpst.arr_c[7]),Reg(rvpst.arr_c[8]),Reg(rvpst.arr_c[9]), - //B(4,3)=A(3,4) - Reg(rvp03.arr_d[A]),Reg(rvp03.arr_d[B]),Reg(rvp03.arr_d[C]), - //B(0,4)=A(2,0) - Reg(rvpst.arr_a[6]),Reg(rvpst.arr_a[7]),Reg(rvpst.arr_a[8]), - //B(1,4)=A(3,1) - Reg(rvpst.arr_b[2]),Reg(rvpst.arr_b[3]),Reg(rvpst.arr_b[4]) ]; - d := [ - //B(2,4)=A(4,2) - Reg(rvpst.arr_b[20]),Reg(rvpst.arr_b[21]),Reg(rvpst.arr_c[0]), - //B(3,4)=A(0,3) - Reg(rvpst.arr_c[1]),Reg(rvpst.arr_c[2]),Reg(rvpst.arr_c[3]), - //B(4,4)=A(1,4) - Reg(rvp06.arr_d[A]),Reg(rvp06.arr_d[B]),Reg(rvp06.arr_d[C]), - NondetReg(0),NondetReg(0),NondetReg(0), - NondetReg(0),NondetReg(0),NondetReg(0), - NondetReg(0),NondetReg(0),NondetReg(0), - NondetReg(0),NondetReg(0),NondetReg(0), - NondetReg(0),NondetReg(0),NondetReg(0)]; - RetTuple(a, b, c, d, dummyB(), dummyB(), - 0, 9, rvp01.rnd, rvp01.blk, rvp01.midx, auxr) - })))) +// One-shot version of theta +component Theta(a: Array, 5>, 5>) { + ThetaP2(a, ThetaP1(a)) } -component rho_major(rvals: RetTuple) { - m := rvals@1.minor; - minor_onehot := OneHotU<9>(m); - aux_regs := ConcatZeros<9,AUXLEN()-9>(minor_onehot); - r := minor_onehot -> ( - rho_minor0<0,Y>(rvals, aux_regs), - rho_minor1<0,Y>(rvals, aux_regs), - rho_minor2<0,Y>(rvals, aux_regs), - rho_minor0<2,Y>(rvals, aux_regs), - rho_minor1<2,Y>(rvals, aux_regs), - rho_minor2<2,Y>(rvals, aux_regs), - rho_minor0<4,Y>(rvals, aux_regs), - rho_minor1<4,Y>(rvals, aux_regs), - rho_minor3(rvals, aux_regs) - ); - for i : 0..SLEN() { 0 = (m-8) * r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..SLEN() { 0 = (m-8) * r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..SLEN() { 0 = (m-8) * r.arr_c[i] * (1-r.arr_c[i]); }; - for i : 0..SLEN() { 0 = (m-8) * r.arr_d[i] * (1-r.arr_d[i]); }; - r +component RhoMatrix() { + [[0,36,3,41,18],[1,44,10,45,2],[62,6,43,15,61],[28,55,25,21,56],[27,20,39,8,14]] } -component chi_minor0(rvpstate: RetTuple, - auxr: Array) { - XP1 := IncMod5(X); - idx0xp1 := (XP1+5*Y)*3 + 0; - in_a0xp1 := InRange(0,idx0xp1,BLEN()); - v_0xp1 := [in_a0xp1, 1-in_a0xp1] -> (rvpstate.arr_a[idx0xp1], - { idx0xp1b := idx0xp1 - BLEN(); - in_b0xp1 := InRange(0,idx0xp1b,BLEN()); - [in_b0xp1, 1-in_b0xp1] -> (rvpstate.arr_b[idx0xp1b], - { idx0xp1c := idx0xp1b - BLEN(); - in_c0xp1 := InRange(0,idx0xp1c,BLEN()); - [in_c0xp1, 1-in_c0xp1] -> - (rvpstate.arr_c[idx0xp1c], rvpstate.arr_d[idx0xp1c-BLEN()]) })}); - unpack_0xp1 := ToBitsU(v_0xp1); - FromBits(unpack_0xp1) = v_0xp1; - last0xp1 := unpack_0xp1[BLEN()-1]; - last0xp1 * (1-last0xp1) = 0; - - idx1xp1 := idx0xp1 + 1; - in_a1xp1 := InRange(0,idx1xp1,BLEN()); - v_1xp1 := [in_a1xp1, 1-in_a1xp1] -> (rvpstate.arr_a[idx1xp1], - { idx1xp1b := idx1xp1 - BLEN(); - in_b1xp1 := InRange(0,idx1xp1b,BLEN()); - [in_b1xp1, 1-in_b1xp1] -> (rvpstate.arr_b[idx1xp1b], - { idx1xp1c := idx1xp1b - BLEN(); - in_c1xp1 := InRange(0,idx1xp1c,BLEN()); - [in_c1xp1, 1-in_c1xp1] -> - (rvpstate.arr_c[idx1xp1c], rvpstate.arr_d[idx1xp1c-BLEN()]) })}); - unpack_1xp1 := ToBitsU(v_1xp1); - FromBits(unpack_1xp1) = v_1xp1; - - idx0xp2 := (IncMod5(XP1)+5*Y)*3 + 0; - in_a0xp2 := InRange(0,idx0xp2,BLEN()); - v_0xp2 := [in_a0xp2, 1-in_a0xp2] -> (rvpstate.arr_a[idx0xp2], - { idx0xp2b := idx0xp2 - BLEN(); - in_b0xp2 := InRange(0,idx0xp2b,BLEN()); - [in_b0xp2, 1-in_b0xp2] -> (rvpstate.arr_b[idx0xp2b], - { idx0xp2c := idx0xp2b - BLEN(); - in_c0xp2 := InRange(0,idx0xp2c,BLEN()); - [in_c0xp2, 1-in_c0xp2] -> - (rvpstate.arr_c[idx0xp2c], rvpstate.arr_d[idx0xp2c-BLEN()]) })}); - unpack_0xp2 := ToBitsU(v_0xp2); - FromBits(unpack_0xp2) = v_0xp2; - last0xp2 := unpack_0xp2[BLEN()-1]; - last0xp2 * (1-last0xp2) = 0; - - idx1xp2 := idx0xp2 + 1; - in_a1xp2 := InRange(0,idx1xp2,BLEN()); - v_1xp2 := [in_a1xp2, 1-in_a1xp2] -> (rvpstate.arr_a[idx1xp2], - { idx1xp2b := idx1xp2 - BLEN(); - in_b1xp2 := InRange(0,idx1xp2b,BLEN()); - [in_b1xp2, 1-in_b1xp2] -> (rvpstate.arr_b[idx1xp2b], - { idx1xp2c := idx1xp2b - BLEN(); - in_c1xp2 := InRange(0,idx1xp2c,BLEN()); - [in_c1xp2, 1-in_c1xp2] -> - (rvpstate.arr_c[idx1xp2c], rvpstate.arr_d[idx1xp2c-BLEN()]) })}); - unpack_1xp2 := ToBitsU(v_1xp2); - FromBits(unpack_1xp2) = v_1xp2; - - idx0x := (X+5*Y)*3 + 0; - in_a0x := InRange(0,idx0x,BLEN()); - v_0x := [in_a0x, 1-in_a0x] -> (rvpstate.arr_a[idx0x], - { idx0xb := idx0x - BLEN(); - in_b0x := InRange(0,idx0xb,BLEN()); - [in_b0x, 1-in_b0x] -> (rvpstate.arr_b[idx0xb], - { idx0xc := idx0xb - BLEN(); - in_c0x := InRange(0,idx0xc,BLEN()); - [in_c0x, 1-in_c0x] -> - (rvpstate.arr_c[idx0xc], rvpstate.arr_d[idx0xc-BLEN()]) })}); - unpack_0x := ToBitsU(v_0x); - FromBits(unpack_0x) = v_0x; - last0x := unpack_0x[BLEN()-1]; - last0x * (1-last0x) = 0; - - idx1x := idx0x + 1; - in_a1x := InRange(0,idx1x,BLEN()); - v_1x := [in_a1x, 1-in_a1x] -> (rvpstate.arr_a[idx1x], - { idx1xb := idx1x - BLEN(); - in_b1x := InRange(0,idx1xb,BLEN()); - [in_b1x, 1-in_b1x] -> (rvpstate.arr_b[idx1xb], - { idx1xc := idx1xb - BLEN(); - in_c1x := InRange(0,idx1xc,BLEN()); - [in_c1x, 1-in_c1x] -> - (rvpstate.arr_c[idx1xc], rvpstate.arr_d[idx1xc-BLEN()]) })}); - unpack_1x := ToBitsU(v_1x); - FromBits(unpack_1x) = v_1x; - - anx1 := for i : 0..BLEN() { andnxor(unpack_0x[i], unpack_0xp1[i], unpack_0xp2[i])}; - anx2 := for i : 0..SLEN() { andnxor(unpack_1x[i], unpack_1xp1[i], unpack_1xp2[i])}; - result := [Reg(FromBits(anx1)), Reg(FromBits(anx2))]; - - withrs_d := Concatenate(unpack_0xp1, result); - Z := (X-1)*(X-3); - minor_new := [Isz(Z), 1-Isz(Z)] -> (3*(1+(X-1)/2), 1+3*(X/2)); - a := ConcatZeros(unpack_1xp1); - c := ConcatZeros(unpack_1xp2); - f := ConcatZeros(unpack_1x); - RetTuple(a, unpack_0xp2, c, withrs_d, unpack_0x, f, - minor_new, Y+9, rvpstate.rnd, rvpstate.blk, rvpstate.midx, auxr) +component Rho(a: Array, 5>, 5>) { + for i : 0..5 { + for j : 0..5 { + RotateLeft<64>(a[i][j], RhoMatrix()[j][i]) + } + } } -component chi_minor1(rvals: RetTuple, - auxr: Array) { - rvpstate := rvals@(2+3*(X/2)); //X=0,pstate=2 X=2,pstate=5 X=4,pstate=8 - rvprev01 := rvals@1; - - idx2x := (X+5*Y)*3 + 2; - in_a2x := InRange(0,idx2x,BLEN()); - v_2x := [in_a2x, 1-in_a2x] -> (rvpstate.arr_a[idx2x], - { idx2xb := idx2x - BLEN(); - in_b2x := InRange(0,idx2xb,BLEN()); - [in_b2x, 1-in_b2x] -> (rvpstate.arr_b[idx2xb], - { idx2xc := idx2xb - BLEN(); - in_c2x := InRange(0,idx2xc,BLEN()); - [in_c2x, 1-in_c2x] -> - (rvpstate.arr_c[idx2xc], rvpstate.arr_d[idx2xc-BLEN()]) })}); - unpack_2x := ToBitsU(v_2x); - FromBits(unpack_2x) = v_2x; - - XP1 := IncMod5(X); - idx2xp1 := (XP1+5*Y)*3 + 2; - in_a2xp1 := InRange(0,idx2xp1,BLEN()); - v_2xp1 := [in_a2xp1, 1-in_a2xp1] -> (rvpstate.arr_a[idx2xp1], - { idx2xp1b := idx2xp1 - BLEN(); - in_b2xp1 := InRange(0,idx2xp1b,BLEN()); - [in_b2xp1, 1-in_b2xp1] -> (rvpstate.arr_b[idx2xp1b], - { idx2xp1c := idx2xp1b - BLEN(); - in_c2xp1 := InRange(0,idx2xp1c,BLEN()); - [in_c2xp1, 1-in_c2xp1] -> - (rvpstate.arr_c[idx2xp1c], rvpstate.arr_d[idx2xp1c-BLEN()]) })}); - unpack_2xp1 := ToBitsU(v_2xp1); - FromBits(unpack_2xp1) = v_2xp1; - - idx2xp2 := (IncMod5(XP1)+5*Y)*3 + 2; - in_a2xp2 := InRange(0,idx2xp2,BLEN()); - v_2xp2 := [in_a2xp2, 1-in_a2xp2] -> (rvpstate.arr_a[idx2xp2], - { idx2xp2b := idx2xp2 - BLEN(); - in_b2xp2 := InRange(0,idx2xp2b,BLEN()); - [in_b2xp2, 1-in_b2xp2] -> (rvpstate.arr_b[idx2xp2b], - { idx2xp2c := idx2xp2b - BLEN(); - in_c2xp2 := InRange(0,idx2xp2c,BLEN()); - [in_c2xp2, 1-in_c2xp2] -> - (rvpstate.arr_c[idx2xp2c], rvpstate.arr_d[idx2xp2c-BLEN()]) })}); - unpack_2xp2 := ToBitsU(v_2xp2); - FromBits(unpack_2xp2) = v_2xp2; - - anx3 := for i : 0..SLEN() { andnxor(unpack_2x[i], unpack_2xp1[i], unpack_2xp2[i])}; - res3 := Reg(FromBits(anx3)); - withr_a := ConcatElem(unpack_2x, Reg(rvprev01.arr_d[0+BLEN()])); - withr_b := ConcatElem(unpack_2xp1, Reg(rvprev01.arr_d[1+BLEN()])); - withr_c := ConcatElem(unpack_2xp2, res3); - minor_new := 2 + 3*(X/2); - - [Isz(X-4), 1-Isz(X-4)] -> ( - RetTuple(withr_a, withr_b, withr_c, dummyE(), dummyB(), dummyB(), - minor_new, Y+9, - rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr), - { NXTX := IncMod5(X); //TODO - idx2nx := (NXTX+5*Y)*3 + 2; - in_a2nx := InRange(0,idx2nx,BLEN()); - v_2nx := [in_a2nx, 1-in_a2nx] -> (rvpstate.arr_a[idx2nx], - { idx2nxb := idx2nx - BLEN(); - in_b2nx := InRange(0,idx2nxb,BLEN()); - [in_b2nx, 1-in_b2nx] -> (rvpstate.arr_b[idx2nxb], - { idx2nxc := idx2nxb - BLEN(); - in_c2nx := InRange(0,idx2nxc,BLEN()); - [in_c2nx, 1-in_c2nx] -> - (rvpstate.arr_c[idx2nxc], - rvpstate.arr_d[idx2nxc-BLEN()]) })}); - unpack_2nx := ToBitsU(v_2nx); - FromBits(unpack_2nx) = v_2nx; - - NXP1 := IncMod5(NXTX); - idx2nxp1 := (NXP1+5*Y)*3 + 2; - in_a2nxp1 := InRange(0,idx2nxp1,BLEN()); - v_2nxp1 := [in_a2nxp1, 1-in_a2nxp1] -> (rvpstate.arr_a[idx2nxp1], - { idx2nxp1b := idx2nxp1 - BLEN(); - in_b2nxp1 := InRange(0,idx2nxp1b,BLEN()); - [in_b2nxp1, 1-in_b2nxp1] -> (rvpstate.arr_b[idx2nxp1b], - { idx2nxp1c := idx2nxp1b - BLEN(); - in_c2nxp1 := InRange(0,idx2nxp1c,BLEN()); - [in_c2nxp1, 1-in_c2nxp1] -> - (rvpstate.arr_c[idx2nxp1c], - rvpstate.arr_d[idx2nxp1c-BLEN()]) })}); - unpack_2nxp1 := ToBitsU(v_2nxp1); - FromBits(unpack_2nxp1) = v_2nxp1; - - idx2nxp2 := (IncMod5(NXP1)+5*Y)*3 + 2; - in_a2nxp2 := InRange(0,idx2nxp2,BLEN()); - v_2nxp2 := [in_a2nxp2, 1-in_a2nxp2] -> (rvpstate.arr_a[idx2nxp2], - { idx2nxp2b := idx2nxp2 - BLEN(); - in_b2nxp2 := InRange(0,idx2nxp2b,BLEN()); - [in_b2nxp2, 1-in_b2nxp2] -> (rvpstate.arr_b[idx2nxp2b], - { idx2nxp2c := idx2nxp2b - BLEN(); - in_c2nxp2 := InRange(0,idx2nxp2c,BLEN()); - [in_c2nxp2, 1-in_c2nxp2] -> - (rvpstate.arr_c[idx2nxp2c], - rvpstate.arr_d[idx2nxp2c-BLEN()]) })}); - unpack_2nxp2 := ToBitsU(v_2nxp2); - FromBits(unpack_2nxp2) = v_2nxp2; - - anx3n := for i : 0..SLEN() { - andnxor(unpack_2nx[i], unpack_2nxp1[i], unpack_2nxp2[i]) }; - res3n := Reg(FromBits(anx3n)); - - withr_d := Concatenate( - unpack_2nxp1, [res3n,NondetReg(0),NondetReg(0)]); - e := ConcatZeros(unpack_2nxp2); - f := ConcatZeros(unpack_2nx); - RetTuple(withr_a, withr_b, withr_c, withr_d, e, f, - minor_new, Y+9, - rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - }) +component PiMatrix() { + [[0,3,1,4,2],[1,4,2,0,3],[2,0,3,1,4],[3,1,4,2,0],[4,2,0,3,1]] } -component chi_minor2(rvals: RetTuple, - auxr: Array) { - rvprev01 := rvals@1; - rvprev03 := rvals@3; - rvprev04 := rvals@4; - rvprev06 := rvals@6; - rvprev07 := rvals@7; - rvpstate := rvals@9; - - [Isz(Y), 1-Isz(Y)] -> ( - { a := [Reg(rvprev07.arr_a[0+SLEN()]),Reg(rvprev07.arr_b[0+SLEN()]), - Reg(rvprev07.arr_c[0+SLEN()]),Reg(rvprev06.arr_d[0+BLEN()]), - Reg(rvprev06.arr_d[1+BLEN()]),Reg(rvprev07.arr_d[0+SLEN()]), - Reg(rvprev04.arr_a[0+SLEN()]),Reg(rvprev04.arr_b[0+SLEN()]), - Reg(rvprev04.arr_c[0+SLEN()]),Reg(rvprev03.arr_d[0+BLEN()]), - Reg(rvprev03.arr_d[1+BLEN()]),Reg(rvprev04.arr_d[0+SLEN()]), - Reg(rvprev01.arr_a[0+SLEN()]),Reg(rvprev01.arr_b[0+SLEN()]), - Reg(rvprev01.arr_c[0+SLEN()]),Reg(rvpstate.arr_a[15]), - Reg(rvpstate.arr_a[16]),Reg(rvpstate.arr_a[17]), - Reg(rvpstate.arr_a[18]),Reg(rvpstate.arr_a[19]), - Reg(rvpstate.arr_a[20]),Reg(rvpstate.arr_a[21])]; - RetTuple(a, RGZ(rvpstate.arr_b), RGZ(rvpstate.arr_c), - RGZ(rvpstate.arr_d), dummyB(), dummyB(), - 0, 10, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - }, - [Isz(Y-1), 1-Isz(Y-1)] -> ( - { rs1 := [Reg(rvprev07.arr_a[0+SLEN()]),Reg(rvprev07.arr_b[0+SLEN()]), - Reg(rvprev07.arr_c[0+SLEN()]),Reg(rvprev06.arr_d[0+BLEN()]), - Reg(rvprev06.arr_d[1+BLEN()]),Reg(rvprev07.arr_d[0+SLEN()]), - Reg(rvprev04.arr_a[0+SLEN()])]; - a := Concatenate<15, 7>(for i : 0..15 {Reg(rvpstate.arr_a[i])}, rs1); - rs2 := [Reg(rvprev04.arr_b[0+SLEN()]),Reg(rvprev04.arr_c[0+SLEN()]), - Reg(rvprev03.arr_d[0+BLEN()]),Reg(rvprev03.arr_d[1+BLEN()]), - Reg(rvprev04.arr_d[0+SLEN()]),Reg(rvprev01.arr_a[0+SLEN()]), - Reg(rvprev01.arr_b[0+SLEN()]),Reg(rvprev01.arr_c[0+SLEN()])]; - b := Concatenate<8, 14>(rs2, for i : 8..22 {Reg(rvpstate.arr_b[i])}); - RetTuple(a, b, RGZ(rvpstate.arr_c), - RGZ(rvpstate.arr_d), dummyB(), dummyB(), - 0, 11, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - }, - [Isz(Y-2), 1-Isz(Y-2)] -> ( - { rs1 := [ - Reg(rvprev07.arr_a[0+SLEN()]),Reg(rvprev07.arr_b[0+SLEN()]), - Reg(rvprev07.arr_c[0+SLEN()]),Reg(rvprev06.arr_d[0+BLEN()]), - Reg(rvprev06.arr_d[1+BLEN()]),Reg(rvprev07.arr_d[0+SLEN()]), - Reg(rvprev04.arr_a[0+SLEN()]),Reg(rvprev04.arr_b[0+SLEN()]), - Reg(rvprev04.arr_c[0+SLEN()]),Reg(rvprev03.arr_d[0+BLEN()]), - Reg(rvprev03.arr_d[1+BLEN()]),Reg(rvprev04.arr_d[0+SLEN()]), - Reg(rvprev01.arr_a[0+SLEN()]),Reg(rvprev01.arr_b[0+SLEN()])]; - b := Concatenate<8, 14>(for i : 0..8 {Reg(rvpstate.arr_b[i])}, rs1); - rs2 := [Reg(rvprev01.arr_c[0+SLEN()])]; - c := Concatenate<1, 21>( - rs2, for i : 1..22 { Reg(rvpstate.arr_c[i]) }); - RetTuple(RGZ(rvpstate.arr_a), b, c, - RGZ(rvpstate.arr_d), dummyB(), dummyB(), - 0, 12, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - }, - [Isz(Y-3), 1-Isz(Y-3)] -> ( - { rs1 := [ - Reg(rvprev07.arr_a[0+SLEN()]),Reg(rvprev07.arr_b[0+SLEN()]), - Reg(rvprev07.arr_c[0+SLEN()]),Reg(rvprev06.arr_d[0+BLEN()]), - Reg(rvprev06.arr_d[1+BLEN()]),Reg(rvprev07.arr_d[0+SLEN()]), - Reg(rvprev04.arr_a[0+SLEN()]),Reg(rvprev04.arr_b[0+SLEN()]), - Reg(rvprev04.arr_c[0+SLEN()]),Reg(rvprev03.arr_d[0+BLEN()]), - Reg(rvprev03.arr_d[1+BLEN()]),Reg(rvprev04.arr_d[0+SLEN()]), - Reg(rvprev01.arr_a[0+SLEN()]),Reg(rvprev01.arr_b[0+SLEN()]), - Reg(rvprev01.arr_c[0+SLEN()])]; - c1 := Concatenate<1, 15>([rvpstate.arr_c[0]], rs1); - c := Concatenate<16, 6>( - c1, for i : 16..22 { Reg(rvpstate.arr_c[i]) }); - RetTuple(RGZ(rvpstate.arr_a), RGZ(rvpstate.arr_b), - c, RGZ(rvpstate.arr_d), dummyB(), dummyB(), - 0, 13, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - }, - { rs1 := [ - Reg(rvprev07.arr_a[0+SLEN()]),Reg(rvprev07.arr_b[0+SLEN()]), - Reg(rvprev07.arr_c[0+SLEN()]),Reg(rvprev06.arr_d[0+BLEN()]), - Reg(rvprev06.arr_d[1+BLEN()]),Reg(rvprev07.arr_d[0+SLEN()])]; - c := Concatenate<16, 6>( - for i : 0..16 { Reg(rvpstate.arr_c[i]) }, rs1); - rs2 := [ - Reg(rvprev04.arr_a[0+SLEN()]),Reg(rvprev04.arr_b[0+SLEN()]), - Reg(rvprev04.arr_c[0+SLEN()]),Reg(rvprev03.arr_d[0+BLEN()]), - Reg(rvprev03.arr_d[1+BLEN()]),Reg(rvprev04.arr_d[0+SLEN()]), - Reg(rvprev01.arr_a[0+SLEN()]),Reg(rvprev01.arr_b[0+SLEN()]), - Reg(rvprev01.arr_c[0+SLEN()])]; - - unpack_round := OneHotU<24>(rvprev01.rnd); - rnd_1 := for i : 0..2 { NondetReg(unpack_round[i]) }; - for i : 0..2 { AliasLayout!(rnd_1[i], unpack_round[i]); }; - rnd_2 := for i : 0..BLEN() { NondetReg(unpack_round[i+2]) }; - for i : 0..22 { AliasLayout!(rnd_2[i], unpack_round[i+2]); }; - - tmp_d := ConcatZeros<9,RLEN()-9-2>(rs2); - d := Concatenate(tmp_d, rnd_1); - 0 = d[BLEN()+0] * 1-d[BLEN()+0]; - 0 = d[BLEN()+1] * 1-d[BLEN()+1]; - - unpack_a002 := ToBitsU(rvpstate.arr_a[2]); - FromBits(unpack_a002) = rvpstate.arr_a[2]; - - RetTuple(RGZ(rvpstate.arr_a), - RGZ(rvpstate.arr_b), c, d, rnd_2, unpack_a002, - 9, 13, rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr) - })))) +component Pi(a: Array, 5>, 5>) { + for i : 0..5 { + for j : 0..5 { + newi := PiMatrix()[j][i]; + a[j][newi] + } + } } -component iota_xor_rc(rvprev01: RetTuple, - auxr: Array) { - b := rvprev01.blk; - unpack_a000 := ToBitsU(rvprev01.arr_a[0]); - unpack_a001 := ToBitsU(rvprev01.arr_a[1]); - - unpack_rnd := vConcatenate<2,22>( - for i : 0..2 {rvprev01.arr_d[22+i]}, for i : 0..22 {rvprev01.arr_e[i]}); - rc := unpack_rnd -> (rctable(0),rctable(1),rctable(2),rctable(3), - rctable(4), rctable(5),rctable(6),rctable(7),rctable(8),rctable(9), - rctable(10),rctable(11),rctable(12),rctable(13),rctable(14),rctable(15), - rctable(16),rctable(17),rctable(18),rctable(19),rctable(20),rctable(21), - rctable(22),rctable(23)); - - // TODO: merge rc & nxt muxes - - newBlk := b-1; - invNewBlk := NondetReg(Inv(newBlk)); - prod := Reg(newBlk*invNewBlk); - newBlk*(1-prod) = 0; - - nxt := unpack_rnd -> ( - [0,1,b],[0,2,b],[0,3,b],[0,4,b],[0,5,b],[0,6,b],[0,7,b],[0,8,b],[0,9,b], - [0,10,b],[0,11,b],[0,12,b],[0,13,b],[0,14,b],[0,15,b],[0,16,b],[0,17,b], - [0,18,b],[0,19,b],[0,20,b],[0,21,b],[0,22,b],[0,23,b], - [prod, 1-prod] -> ([14,0,newBlk], [MAJOR_EXTRA(),0,0]) ); - - a00 := [ - Reg(FromBits(for i : 0..BLEN() { - xor2(rc[0][i],unpack_a000[i])})), - Reg(FromBits(for i : 0..SLEN() { - xor2(rc[1][i],unpack_a001[i])})), - Reg(FromBits(for i : 0..SLEN() { - xor2(rc[2][i],rvprev01.arr_f[i])}))]; - a := Concatenate<3,BLEN()-3>(a00, for i : 3..BLEN() { - Reg(rvprev01.arr_a[i])}); - d_suffix := [invNewBlk, prod]; - d_tmp := ConcatZeros<9,RLEN()-2-9>( - for i : 0..9 {Reg(rvprev01.arr_d[i])}); - d := Concatenate(d_tmp, d_suffix); - - RetTuple(a, RGZ(rvprev01.arr_b), RGZ(rvprev01.arr_c), d, - unpack_a000, unpack_a001, - 0, nxt[0], nxt[1], nxt[2], rvprev01.midx, auxr) +component Chi(a: Array, 5>, 5>) { + for i : 0..5 { + for j : 0..5 { + for k : 0..64 { + jp1 := if (Isz(4-j)) { 0 } else { j + 1 }; + jp2 := if (Isz(4-jp1)) { 0 } else { jp1 + 1 }; + BitXor(a[i][j][k], (1 - a[i][jp1][k]) * a[i][jp2][k]) + } + } + } } -component chi_major(rvals: RetTuple) { - m := rvals@1.minor; - minor_onehot := OneHotU<10>(m); - aux_regs := ConcatZeros<10,AUXLEN()-10>(minor_onehot); - r := minor_onehot -> ( - chi_minor0<0,Y>(rvals@1, aux_regs), - chi_minor1<0,Y>(rvals, aux_regs), - chi_minor0<1,Y>(rvals@3, aux_regs), - chi_minor0<2,Y>(rvals@4, aux_regs), - chi_minor1<2,Y>(rvals, aux_regs), - chi_minor0<3,Y>(rvals@6, aux_regs), - chi_minor0<4,Y>(rvals@7, aux_regs), - chi_minor1<4,Y>(rvals, aux_regs), - chi_minor2(rvals, aux_regs), - iota_xor_rc(rvals@1, aux_regs) - ); - z := (m-8)*(m-9); - for i : 0..SLEN() { 0 = z * r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..SLEN() { 0 = z * r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..SLEN() { 0 = z * r.arr_c[i] * (1-r.arr_c[i]); }; - for i : 0..SLEN() { 0 = z * r.arr_d[i] * (1-r.arr_d[i]); }; - r +component IotaTable() { + [ + [0x0001, 0x0000, 0x0000, 0x0000], + [0x8082, 0x0000, 0x0000, 0x0000], + [0x808a, 0x0000, 0x0000, 0x8000], + [0x8000, 0x8000, 0x0000, 0x8000], + [0x808b, 0x0000, 0x0000, 0x0000], + [0x0001, 0x8000, 0x0000, 0x0000], + [0x8081, 0x8000, 0x0000, 0x8000], + [0x8009, 0x0000, 0x0000, 0x8000], + [0x008a, 0x0000, 0x0000, 0x0000], + [0x0088, 0x0000, 0x0000, 0x0000], + [0x8009, 0x8000, 0x0000, 0x0000], + [0x000a, 0x8000, 0x0000, 0x0000], + [0x808b, 0x8000, 0x0000, 0x0000], + [0x008b, 0x0000, 0x0000, 0x8000], + [0x8089, 0x0000, 0x0000, 0x8000], + [0x8003, 0x0000, 0x0000, 0x8000], + [0x8002, 0x0000, 0x0000, 0x8000], + [0x0080, 0x0000, 0x0000, 0x8000], + [0x800a, 0x0000, 0x0000, 0x0000], + [0x000a, 0x8000, 0x0000, 0x8000], + [0x8081, 0x8000, 0x0000, 0x8000], + [0x8080, 0x0000, 0x0000, 0x8000], + [0x0001, 0x8000, 0x0000, 0x0000], + [0x8008, 0x8000, 0x0000, 0x8000] + ] +} + +component ExpandedIotaTable() { + for i : 0..24 { UnpackNondet<64, 16>(IotaTable()[i]) } +} + +component RoundToArray(idx: Val) { + table := ExpandedIotaTable(); + split := OneHot<24>(idx); + for k : 0..64 { + reduce for i : 0..24 { split[i] * table[i][k] } init 0 with Add + } } -component absorb_word(rvprev: RetTuple, - auxregs: Array) { - idx1 := 3*X + 15*Y + 0; - idx2 := 3*X + 15*Y + 1; - idx3 := 3*X + 15*Y + 2; - in_a1 := InRange(0,idx1,BLEN()); - in_a2 := InRange(0,idx2,BLEN()); - in_a3 := InRange(0,idx3,BLEN()); - v1 := [in_a1, 1-in_a1] -> (rvprev.arr_a[idx1], - { idx1b := idx1 - BLEN(); - in_b1 := InRange(0,idx1b,BLEN()); - [in_b1, 1-in_b1] -> (rvprev.arr_b[idx1b], - rvprev.arr_c[idx1b-BLEN()])}); - v2 := [in_a2, 1-in_a2] -> (rvprev.arr_a[idx2], - { idx2b := idx2 - BLEN(); - in_b2 := InRange(0,idx2b,BLEN()); - [in_b2, 1-in_b2] -> (rvprev.arr_b[idx2b], - rvprev.arr_c[idx2b-BLEN()])}); - v3 := [in_a3, 1-in_a3] -> (rvprev.arr_a[idx3], - { idx3b := idx3 - BLEN(); - in_b3 := InRange(0,idx3b,BLEN()); - [in_b3, 1-in_b3] -> (rvprev.arr_b[idx3b], - rvprev.arr_c[idx3b-BLEN()])}); - unpack_a := ToBitsU(v1); - FromBits(unpack_a) = v1; - unpack_e := ToBitsU(v2); - FromBits(unpack_e) = v2; - unpack_f := ToBitsU(v3); - FromBits(unpack_f) = v3; - - inp1 := readInput(); - unpack_1 := ToBitsU(inp1); - inp2 := readInput(); - unpack_2 := ToBitsU(inp2); - inp3 := readInput(); - unpack_3 := ToBitsU(inp3); - inp4 := readInput(); - unpack_4 := ToBitsU(inp4); - memidx := Reg(rvprev.midx + 1 + X+5*Y); - invmidx := NondetReg(Inv(memidx)); - invmidx*memidx = 1; - - digest := - [Reg(FromBits(unpack_1)), Reg(FromBits(unpack_2)), - Reg(FromBits(unpack_3)), Reg(FromBits(unpack_4))]; - auxtmp1 := ConcatElem(auxregs, memidx); - auxr := Concatenate(auxtmp1, digest); - WriteMemory(memidx, digest); - - arr12 := for i : 0..BLEN() { - in_first12 := InRange(0,i,WORDLEN()); - NondetReg([in_first12, 1-in_first12] -> (unpack_1[i], - unpack_2[i-WORDLEN()]))}; - for i : 0..WORDLEN() { AliasLayout!(arr12[i], unpack_1[i]); }; - for i : WORDLEN()..BLEN() { - AliasLayout!(arr12[i], unpack_2[i-WORDLEN()]); }; - vals12 := for i : 0..BLEN() { xor2(unpack_a[i], arr12[i]) }; - - arr23 := for i : 0..SLEN() { - in_first23 := InRange(0,i,2*WORDLEN()-BLEN()); - NondetReg([in_first23, 1-in_first23] -> ( - unpack_2[i+BLEN()-WORDLEN()], unpack_3[i-(2*WORDLEN()-BLEN())]))}; - for i : 0..2*WORDLEN()-BLEN() - { AliasLayout!(arr23[i], unpack_2[i+BLEN()-WORDLEN()]); }; - for i : 2*WORDLEN()-BLEN()..SLEN() - { AliasLayout!(arr23[i], unpack_3[i-(2*WORDLEN()-BLEN())]); }; - vals23 := for i : 0..SLEN() { xor2(unpack_e[i], arr23[i]) }; - - arr34 := for i : 0..SLEN() { - in_first34 := InRange(0,i,3*WORDLEN()-BLEN()-SLEN()); - NondetReg([in_first34, 1-in_first34] -> ( - unpack_3[i+SLEN()+BLEN()-2*WORDLEN()], - unpack_4[i-(3*WORDLEN()-BLEN()-SLEN())]))}; - for i : 0..3*WORDLEN()-BLEN()-SLEN() - { AliasLayout!(arr34[i], unpack_3[i+SLEN()+BLEN()-2*WORDLEN()]); }; - for i : 3*WORDLEN()-BLEN()-SLEN()..SLEN() - { AliasLayout!(arr34[i], unpack_4[i-(3*WORDLEN()-BLEN()-SLEN())]); }; - vals34 := for i : 0..SLEN() { xor2(unpack_f[i], arr34[i]) }; - - padded23 := ConcatElem(arr23,invmidx); - results := [ - Reg(FromBits(for i : 0..BLEN() { vals12[i] })), - Reg(FromBits(for i : 0..SLEN() { vals23[i] })), - Reg(FromBits(for i : 0..SLEN() { vals34[i] }))]; - withr34 := Concatenate(arr34, results); - padded_e := ConcatZeros(unpack_e); - padded_f := ConcatZeros(unpack_f); - - last_a := unpack_a[BLEN()-1]; - 0 = last_a * (1-last_a); - last_12 := arr12[BLEN()-1]; - 0 = last_12 * (1-last_12); - - inc_idx := X+5*Y+1; - in_first := InRange(0,inc_idx,10); - nxt_major := 1 - in_first; - nxt_in := [in_first, nxt_major] -> (inc_idx, inc_idx-9); - - RetTuple(unpack_a, arr12, padded23, withr34, padded_e, padded_f, - nxt_in, 14+nxt_major, 0, rvprev.blk, rvprev.midx, auxr) +component Iota(a: Array, 5>, 5>, round: Val) { + iotaArray := RoundToArray(round); + for i : 0..5 { + for j : 0..5 { + if (Isz(i) * Isz(j)) { + for k: 0..64 { BitXor(iotaArray[k], a[i][j][k]) } + } else { + a[i][j] + } + } + } } +/* Testing only components */ -component absorb_copy1(rvals: RetTuple, - auxregs: Array) { - rvprev01 := rvals@1; - rvprev02 := rvals@2; - rvprev03 := rvals@3; - rvprev04 := rvals@4; - rvprev05 := rvals@5; - rvprev06 := rvals@6; - rvprev07 := rvals@7; - rvprev08 := rvals@8; - rvprev09 := rvals@9; - rvprev10 := rvals@10; - auxr := ConcatZeros(auxregs); - a := [Reg(rvprev09.arr_d[SLEN()+0]), Reg(rvprev09.arr_d[SLEN()+1]), - Reg(rvprev09.arr_d[SLEN()+2]), Reg(rvprev08.arr_d[SLEN()+0]), - Reg(rvprev08.arr_d[SLEN()+1]), Reg(rvprev08.arr_d[SLEN()+2]), - Reg(rvprev07.arr_d[SLEN()+0]), Reg(rvprev07.arr_d[SLEN()+1]), - Reg(rvprev07.arr_d[SLEN()+2]), Reg(rvprev06.arr_d[SLEN()+0]), - Reg(rvprev06.arr_d[SLEN()+1]), Reg(rvprev06.arr_d[SLEN()+2]), - Reg(rvprev05.arr_d[SLEN()+0]), Reg(rvprev05.arr_d[SLEN()+1]), - Reg(rvprev05.arr_d[SLEN()+2]), Reg(rvprev04.arr_d[SLEN()+0]), - Reg(rvprev04.arr_d[SLEN()+1]), Reg(rvprev04.arr_d[SLEN()+2]), - Reg(rvprev03.arr_d[SLEN()+0]), Reg(rvprev03.arr_d[SLEN()+1]), - Reg(rvprev03.arr_d[SLEN()+2]), Reg(rvprev02.arr_d[SLEN()+0])]; - b := [Reg(rvprev02.arr_d[SLEN()+1]), Reg(rvprev02.arr_d[SLEN()+2]), - Reg(rvprev01.arr_d[SLEN()+0]), Reg(rvprev01.arr_d[SLEN()+1]), - Reg(rvprev01.arr_d[SLEN()+2]), Reg(rvprev10.arr_b[5]), - Reg(rvprev10.arr_b[6]), Reg(rvprev10.arr_b[7]), - Reg(rvprev10.arr_b[8]), Reg(rvprev10.arr_b[9]), - Reg(rvprev10.arr_b[10]), Reg(rvprev10.arr_b[11]), - Reg(rvprev10.arr_b[12]), Reg(rvprev10.arr_b[13]), - Reg(rvprev10.arr_b[14]), Reg(rvprev10.arr_b[15]), - Reg(rvprev10.arr_b[16]), Reg(rvprev10.arr_b[17]), - Reg(rvprev10.arr_b[18]), Reg(rvprev10.arr_b[19]), - Reg(rvprev10.arr_b[20]), Reg(rvprev10.arr_b[21])]; - RetTuple(a, b, RGZ(rvprev10.arr_c), RGZ(rvprev10.arr_d), - dummyB(), dummyB(), 0, 15, 0, rvprev01.blk, rvprev01.midx, auxr) +component RegisterizeKeccak(a: Array, 5>, 5>) { + for i : 0..5 { + for j : 0..5 { + for k : 0..64 { + Reg(a[i][j][k]) + } + } + } } -component absorb_major1(rvals: RetTuple) { - m := rvals@1.minor; - minor_onehot := OneHotU<10>(m); - aux_regs := ConcatZeros<10, AUXBIN()-10>(minor_onehot); - r := minor_onehot -> ( - absorb_word<0,0>(rvals@1, aux_regs), - absorb_word<1,0>(rvals@2, aux_regs), - absorb_word<2,0>(rvals@3, aux_regs), - absorb_word<3,0>(rvals@4, aux_regs), - absorb_word<4,0>(rvals@5, aux_regs), - absorb_word<0,1>(rvals@6, aux_regs), - absorb_word<1,1>(rvals@7, aux_regs), - absorb_word<2,1>(rvals@8, aux_regs), - absorb_word<3,1>(rvals@9, aux_regs), - absorb_copy1(rvals, aux_regs) - ); - for i : 0..SLEN() { 0 = (m-9) * r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..SLEN() { 0 = (m-9) * r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..SLEN() { 0 = (m-9) * r.arr_c[i] * (1-r.arr_c[i]); }; - for i : 0..SLEN() { 0 = (m-9) * r.arr_d[i] * (1-r.arr_d[i]); }; - r +component TestDoRound(a: Array, 5>, 5>, round: Val) { + a := RegisterizeKeccak(Pi(Rho(Theta(a)))); + RegisterizeKeccak(Iota(Chi(a), round)) } -component absorb_copy2(rvals: RetTuple, - auxregs: Array) { - rvprev01 := rvals@1; - rvprev02 := rvals@2; - rvprev03 := rvals@3; - rvprev04 := rvals@4; - rvprev05 := rvals@5; - rvprev06 := rvals@6; - rvprev07 := rvals@7; - rvprev08 := rvals@8; - rvprev09 := rvals@9; - auxr := ConcatZeros(auxregs); - b := [Reg(rvprev09.arr_b[0]), Reg(rvprev09.arr_b[1]), - Reg(rvprev09.arr_b[2]), Reg(rvprev09.arr_b[3]), - Reg(rvprev09.arr_b[4]), Reg(rvprev08.arr_d[SLEN()+0]), - Reg(rvprev08.arr_d[SLEN()+1]), Reg(rvprev08.arr_d[SLEN()+2]), - Reg(rvprev07.arr_d[SLEN()+0]), Reg(rvprev07.arr_d[SLEN()+1]), - Reg(rvprev07.arr_d[SLEN()+2]), Reg(rvprev06.arr_d[SLEN()+0]), - Reg(rvprev06.arr_d[SLEN()+1]), Reg(rvprev06.arr_d[SLEN()+2]), - Reg(rvprev05.arr_d[SLEN()+0]), Reg(rvprev05.arr_d[SLEN()+1]), - Reg(rvprev05.arr_d[SLEN()+2]), Reg(rvprev04.arr_d[SLEN()+0]), - Reg(rvprev04.arr_d[SLEN()+1]), Reg(rvprev04.arr_d[SLEN()+2]), - Reg(rvprev03.arr_d[SLEN()+0]), Reg(rvprev03.arr_d[SLEN()+1])]; - c := [Reg(rvprev03.arr_d[SLEN()+2]), Reg(rvprev02.arr_d[SLEN()+0]), - Reg(rvprev02.arr_d[SLEN()+1]), Reg(rvprev02.arr_d[SLEN()+2]), - Reg(rvprev01.arr_d[SLEN()+0]), Reg(rvprev01.arr_d[SLEN()+1]), - Reg(rvprev01.arr_d[SLEN()+2]), Reg(rvprev09.arr_c[7]), - Reg(rvprev09.arr_c[8]), Reg(rvprev09.arr_c[9]), - Reg(rvprev09.arr_c[10]), Reg(rvprev09.arr_c[11]), - Reg(rvprev09.arr_c[12]), Reg(rvprev09.arr_c[13]), - Reg(rvprev09.arr_c[14]), Reg(rvprev09.arr_c[15]), - Reg(rvprev09.arr_c[16]), Reg(rvprev09.arr_c[17]), - Reg(rvprev09.arr_c[18]), Reg(rvprev09.arr_c[19]), - Reg(rvprev09.arr_c[20]), Reg(rvprev09.arr_c[21])]; - RetTuple(RGZ(rvprev09.arr_a), b, c, RGZ(rvprev09.arr_d), - dummyB(), dummyB(), - 0, 0, 0, rvprev01.blk, rvprev01.midx+17, auxr) +component PrintState(in: Array, 5>, 5>) { + for i : 0..5 { + for j : 0..5 { + p := Pack<64, 16>(in[i][j]); + Log("%x, %x, %x, %x", p[0], p[1], p[2], p[3]) + } + } } -component absorb_major2(rvals: RetTuple) { - m := rvals@1.minor; - minor_onehot := OneHotU<9>(m); - aux_regs := ConcatZeros<9, AUXBIN()-9>(minor_onehot); - r := minor_onehot -> ( - absorb_word<4,1>(rvals@1, aux_regs), - absorb_word<0,2>(rvals@2, aux_regs), - absorb_word<1,2>(rvals@3, aux_regs), - absorb_word<2,2>(rvals@4, aux_regs), - absorb_word<3,2>(rvals@5, aux_regs), - absorb_word<4,2>(rvals@6, aux_regs), - absorb_word<0,3>(rvals@7, aux_regs), - absorb_word<1,3>(rvals@8, aux_regs), - absorb_copy2(rvals, aux_regs) - ); - for i : 0..SLEN() { 0 = (m-8) * r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..SLEN() { 0 = (m-8) * r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..SLEN() { 0 = (m-8) * r.arr_c[i] * (1-r.arr_c[i]); }; - for i : 0..SLEN() { 0 = (m-8) * r.arr_d[i] * (1-r.arr_d[i]); }; - r +/* +test TestTheta { + input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); + PrintState(input); + Log("-----"); + output := Theta(input); + PrintState(output); } -component equal_word(rvprev: RetTuple, - auxregs: Array) { - v1 := rvprev.arr_a[3*X + 0]; - v2 := rvprev.arr_a[3*X + 1]; - v3 := rvprev.arr_a[3*X + 2]; - unpack_a := ToBitsU(v1); - FromBits(unpack_a) = v1; - unpack_e := ToBitsU(v2); - FromBits(unpack_e) = v2; - unpack_f := ToBitsU(v3); - FromBits(unpack_f) = v3; - - inp1 := readInput(); - unpack_1 := ToBitsU(inp1); - inp2 := readInput(); - unpack_2 := ToBitsU(inp2); - inp3 := readInput(); - unpack_3 := ToBitsU(inp3); - inp4 := readInput(); - unpack_4 := ToBitsU(inp4); - memidx := Reg(rvprev.midx + 1 + X); - invmidx := NondetReg(Inv(memidx)); - invmidx*memidx = 1; - - digest := - [Reg(FromBits(unpack_1)), Reg(FromBits(unpack_2)), - Reg(FromBits(unpack_3)), Reg(FromBits(unpack_4))]; - auxtmp1 := ConcatElem(auxregs, memidx); - auxr := Concatenate(auxtmp1, digest); - WriteMemory(memidx, digest); - - arr12 := for i : 0..BLEN() { - in_first12 := InRange(0,i,WORDLEN()); - NondetReg([in_first12, 1-in_first12] -> ( - unpack_1[i], unpack_2[i-WORDLEN()]))}; - for i : 0..WORDLEN() { AliasLayout!(arr12[i],unpack_1[i]); }; - for i : WORDLEN()..BLEN() { - AliasLayout!(arr12[i], unpack_2[i-WORDLEN()]); }; - arr23 := for i : 0..SLEN() { - in_first23 := InRange(0,i,2*WORDLEN()-BLEN()); - NondetReg([in_first23, 1-in_first23] -> ( - unpack_2[i+BLEN()-WORDLEN()], unpack_3[i-(2*WORDLEN()-BLEN())]))}; - for i : 0..2*WORDLEN()-BLEN() { - AliasLayout!(arr23[i], unpack_2[i+BLEN()-WORDLEN()]); }; - for i : 2*WORDLEN()-BLEN()..SLEN() { - AliasLayout!(arr23[i], unpack_3[i-(2*WORDLEN()-BLEN())]); }; - arr34 := for i : 0..SLEN() { - in_first34 := InRange(0,i,3*WORDLEN()-BLEN()-SLEN()); - NondetReg([in_first34, 1-in_first34] -> ( - unpack_3[i+SLEN()+BLEN()-2*WORDLEN()], - unpack_4[i-(3*WORDLEN()-BLEN()-SLEN())]))}; - for i : 0..3*WORDLEN()-BLEN()-SLEN() { - AliasLayout!(arr34[i], unpack_3[i+SLEN()+BLEN()-2*WORDLEN()]); }; - for i : 3*WORDLEN()-BLEN()-SLEN()..SLEN() { - AliasLayout!(arr34[i], unpack_4[i-(3*WORDLEN()-BLEN()-SLEN())]); }; - - for i : 0..BLEN() { unpack_a[i] = arr12[i]; }; - for i : 0..SLEN() { unpack_e[i] = arr23[i]; }; - for i : 0..SLEN() { unpack_f[i] = arr34[i]; }; - - c := ConcatElem(arr23, invmidx); - e := ConcatZeros(unpack_e); - f := ConcatZeros(unpack_f); - last_a := unpack_a[BLEN()-1]; - 0 = last_a * (1-last_a); - last12 := arr12[BLEN()-1]; - 0 = last12 * (1-last12); - - RetTuple(unpack_a, arr12, c, - ConcatZeros(arr34), - e, f, X+1, MAJOR_EXTRA(), 0, 0, memidx, auxr) +test TestRho { + input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); + PrintState(input); + Log("-----"); + output := Rho(input); + PrintState(output); } - -component parse_next_block(rvprev: RetTuple, - auxregs: Array) { - memidxNxt := Reg(rvprev.midx + 1); - invmidxNxt := NondetReg(Inv(memidxNxt)); - midxNN := memidxNxt + 1; - invmidxNN := NondetReg(Inv(midxNN)); - - blk := NondetReg(readInput()); - readInput(); readInput(); readInput(); - invBlk := NondetReg(Inv(blk)); - prod := Reg(blk*invBlk); - blk*(1-prod) = 0; - - invmidxNxt*memidxNxt = 1; - digest := [blk, NondetReg(0), NondetReg(0), NondetReg(0)]; - auxtmp1 := ConcatElem(auxregs, memidxNxt); - auxr := Concatenate(auxtmp1, digest); - WriteMemory(memidxNxt, digest); - - idx2 := Reg(midxNN); - digest2 := [Reg(0x0080), Reg(0), Reg(0), Reg(0)]; - - nskip := NondetReg(7 - ((midxNN+1)&7)); // 7 - num_of_writes%8 - unpack_nskip := ToBitsU<3>(nskip); - FromBits<3>(unpack_nskip) = nskip; // 0 <= nskip <= 7 - - dz := for i : 0..11 { NondetReg(0) }; - d1 := Concatenate<11,3>(dz, unpack_nskip); - d2 := Concatenate<14,6>(d1, - [nskip,invBlk,prod,invmidxNxt,invmidxNN,idx2]); - d := Concatenate<20,4>(d2, digest2); - - [prod, 1-prod] -> ( - RetTuple(dummyB(), dummyB(), dummyB(), d, dummyB(), dummyB(), - 0, 14, 0, blk, memidxNxt, auxr), - { invmidxNN*midxNN = 1; - WriteMemory(idx2, digest2); - bitlen := 64*midxNN; // TODO: overflow - RetTuple(dummyB(), dummyB(), dummyB(), d, dummyB(), dummyB(), - S2MINOR_SKIP()-1, S2MAJOR_SETUP(), bitlen, nskip, midxNN, auxr) - }) +test TestPi { + input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); + PrintState(input); + Log("-----"); + output := Pi(input); + PrintState(output); } -component mem_padding_sha256(rvprev01: RetTuple, - auxr: Array) { - bitlen := rvprev01.rnd; - Q := WORDLEN()/2; - E := 256; // Po2(Q); - H := WORDLEN(); - F := BABYMAX(); - unpack_bitlen := ToBitsU(bitlen); - FromBits(unpack_bitlen) = bitlen; - b12low := FromBits(for i : 0..Q {unpack_bitlen[i]}); - b12high := FromBits(for i : Q..H {unpack_bitlen[i]}); - b12 := Reg(b12low*E + b12high); - b34low := FromBits(for i : H..(H+Q) {unpack_bitlen[i]}); - b34high := FromBits(for i : (H+Q)..F {unpack_bitlen[i]}); - b34 := Reg(b34low*E + b34high); - - memidx := Reg(rvprev01.midx + 1); - nskip := rvprev01.blk; - invn := NondetReg(Inv(nskip)); - prod := Reg(nskip*invn); - nskip*(1-prod) = 0; - - a_tmp := for i : 0 .. SLEN() { NondetReg(unpack_bitlen[i]) }; - for i : 0 .. SLEN() { AliasLayout!(a_tmp[i], unpack_bitlen[i]); }; - a := ConcatElem(a_tmp, b12); - - b_tmp := for i : SLEN() .. F { NondetReg(unpack_bitlen[i]) }; - for i : SLEN() .. F { - AliasLayout!(b_tmp[i-SLEN()], unpack_bitlen[i]); }; - zdigest := for i : 0..4 { NondetReg(0) }; //TODO: slice? dom bug - vdigest := [NondetReg(0), NondetReg(0), b34, b12]; - b_tmp2 := Concatenate(b_tmp, zdigest); - b_tmp3 := ConcatZeros(b_tmp2); - b := Concatenate(b_tmp3, for i : 0..3 { vdigest[i] }); - - d := ConcatZeros<3, RLEN()-3>( - [invn, prod, memidx]); - - // anti-hoisting workaround - [1-prod, prod] -> ( - { WriteMemory(memidx, vdigest); }, - { } ); - [1-prod, prod] -> ( - { }, - { WriteMemory(memidx, zdigest); } ); - - [1-prod, prod] -> ( - RetTuple(a, b, dummyB(), d, dummyB(), dummyB(), - S2MINOR_SKIP(), S2MAJOR_SETUP(), 0, 0, memidx, auxr), - RetTuple(a, b, dummyB(), d, dummyB(), dummyB(), - S2MINOR_SKIP()-1, S2MAJOR_SETUP(), - rvprev01.rnd, nskip-1, memidx, auxr)) +test TestChi { + input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); + PrintState(input); + Log("-----"); + output := Chi(input); + PrintState(output); } -component sha256setup_major(rvals: RetTuple) { - m := rvals@1.minor; - minor_onehot := OneHotU<10>(m); - aux_regs := ConcatZeros<10, AUXLEN()-10>(minor_onehot); - r := minor_onehot -> ( - mem_padding_sha256(rvals@1, aux_regs), - sha256init<1>(rvals@1, aux_regs), - sha256init<2>(rvals@1, aux_regs), - sha256init<3>(rvals@1, aux_regs), - sha256init<4>(rvals@1, aux_regs), - sha256fini<5>(rvals@0, aux_regs), - sha256fini<6>(rvals@0, aux_regs), - sha256fini<7>(rvals@0, aux_regs), - sha256fini<8>(rvals@0, aux_regs), - RetTuple(dummyB(), dummyB(), dummyB(), dummyE(), dummyB(), dummyB(), - S2MINOR_SKIP()+S2MINOR_OUTPUT(), S2MAJOR_SETUP(), - 0, 0, 0, aux_regs) - ); - for i : 0..SLEN() { 0 = r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..SLEN() { 0 = r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..SLEN() { 0 = r.arr_c[i] * (1-r.arr_c[i]); }; - //TODO - //for i : 0..SLEN() { 0 = (m-8) * (m-9) * r.arr_d[i] * (1-r.arr_d[i]); }; - r +test TestIota { + input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); + PrintState(input); + Log("-----"); + output := Iota(input, 3); + PrintState(output); } -component extra_major(rvals: RetTuple, pc: NondetReg, inv_pc: NondetReg) { - m := rvals@1.minor; - - first_cycle := 1 - pc*inv_pc; - minor_idx := [first_cycle, 1-first_cycle] -> ( - MINOR_1STCYC(), rvals@1.minor); - minor_onehot := OneHotU<6>(minor_idx); - auxregs := ConcatZeros<6, AUXBIN()-6>(minor_onehot); - r := minor_onehot -> ( - equal_word<0>(rvals@1, auxregs), - equal_word<1>(rvals@2, auxregs), - equal_word<2>(rvals@3, auxregs), - equal_word<3>(rvals@4, auxregs), - parse_next_block(rvals@1, auxregs), - { blk := NondetReg(readInput()); - //invBlk := NondetReg(Inv(Blk)); Blk*InvBlk = 1; //maybe unneeded - readInput(); readInput(); readInput(); - - idx := Reg(0); - digest := [blk, NondetReg(0), NondetReg(0), NondetReg(0)]; - auxtmp1 := ConcatElem(auxregs, idx); - auxr := Concatenate(auxtmp1, digest); - WriteMemory(idx, digest); - - RetTuple(dummyB(), dummyB(), dummyB(), dummyE(), - dummyB(), dummyB(), 0, 14, 0, blk, 0, auxr) - } - ); - r +test Permute { + input := for i : 0..5 { for j : 0..5 { for k : 0..64 { 0 } } }; + output := reduce 0..4 init input with TestDoRound; + PrintState(output); } +*/ -component Top() { - configureInput(2); - retvals : RetTuple; - - PC := NondetReg(GetCycle()); - invPC := NondetReg(Inv(PC)); - is_first_cycle := 1 - PC*invPC; - is_first_cycle * PC = 0; - major_idx := [is_first_cycle, 1-is_first_cycle] -> ( - { - // PC@1 = total_cycles - 1; - MAJOR_EXTRA() - }, - { - PC = PC@1 + 1; - retvals@1.major - }); - major_onehot := OneHot<22>(major_idx); - retvals := major_onehot ->! ( - xor5words_minor0(retvals@1), - xor5words_minor1(retvals@0), - xor5words_minor2(retvals@0), - xor5words_minor3(retvals@0), - rho_major<0>(retvals@0), - rho_major<1>(retvals@0), - rho_major<2>(retvals@0), - rho_major<3>(retvals@0), - rho_major<4>(retvals@0), - chi_major<0>(retvals@0), - chi_major<1>(retvals@0), - chi_major<2>(retvals@0), - chi_major<3>(retvals@0), - chi_major<4>(retvals@0), - absorb_major1(retvals@0), - absorb_major2(retvals@0), - sha256setup_major(retvals@0), - extra_major(retvals@0, PC, invPC), - sha256load_all(retvals@0), - sha256mix_all<0>(retvals@0), - sha256mix_all<1>(retvals@0), - sha256mix_all<2>(retvals@0) - ); - for i : 0..BLEN() { 0 = retvals.arr_e[i] * (1-retvals.arr_e[i]); }; - for i : 0..BLEN() { 0 = retvals.arr_f[i] * (1-retvals.arr_f[i]); }; - for i : 0..AUXBIN() { 0 = retvals.auxr[i] * (1-retvals.auxr[i]); }; -} diff --git a/zirgen/circuit/keccak/methods/guest/Cargo.lock b/zirgen/circuit/keccak/methods/guest/Cargo.lock deleted file mode 100644 index cc91d4fc..00000000 --- a/zirgen/circuit/keccak/methods/guest/Cargo.lock +++ /dev/null @@ -1,1414 +0,0 @@ -# This file is automatically @generated by Cargo. -# It is not intended for manual editing. -version = 3 - -[[package]] -name = "adler2" -version = "2.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "512761e0bb2578dd7380c6baaa0f4ce03e84f95e960231d1dec8bf4d7d6e2627" - -[[package]] -name = "ahash" -version = "0.8.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e89da841a80418a9b391ebaea17f5c112ffaaa96f621d2c285b5174da76b9011" -dependencies = [ - "cfg-if", - "once_cell", - "version_check", - "zerocopy", -] - -[[package]] -name = "anstream" -version = "0.6.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8acc5369981196006228e28809f761875c0327210a891e941f4c683b3a99529b" -dependencies = [ - "anstyle", - "anstyle-parse", - "anstyle-query", - "anstyle-wincon", - "colorchoice", - "is_terminal_polyfill", - "utf8parse", -] - -[[package]] -name = "anstyle" -version = "1.0.10" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "55cc3b69f167a1ef2e161439aa98aed94e6028e5f9a59be9a6ffb47aef1651f9" - -[[package]] -name = "anstyle-parse" -version = "0.2.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3b2d16507662817a6a20a9ea92df6652ee4f94f914589377d69f3b21bc5798a9" -dependencies = [ - "utf8parse", -] - -[[package]] -name = "anstyle-query" -version = "1.1.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "79947af37f4177cfead1110013d678905c37501914fba0efea834c3fe9a8d60c" -dependencies = [ - "windows-sys", -] - -[[package]] -name = "anstyle-wincon" -version = "3.0.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2109dbce0e72be3ec00bed26e6a7479ca384ad226efdd66db8fa2e3a38c83125" -dependencies = [ - "anstyle", - "windows-sys", -] - -[[package]] -name = "anyhow" -version = "1.0.93" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4c95c10ba0b00a02636238b814946408b1322d5ac4760326e6fb8ec956d85775" - -[[package]] -name = "arbitrary" -version = "1.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dde20b3d026af13f561bdd0f15edf01fc734f0dafcedbaf42bba506a9517f223" -dependencies = [ - "derive_arbitrary", -] - -[[package]] -name = "ark-bn254" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a22f4561524cd949590d78d7d4c5df8f592430d221f7f3c9497bbafd8972120f" -dependencies = [ - "ark-ec", - "ark-ff", - "ark-std", -] - -[[package]] -name = "ark-crypto-primitives" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1f3a13b34da09176a8baba701233fdffbaa7c1b1192ce031a3da4e55ce1f1a56" -dependencies = [ - "ark-ec", - "ark-ff", - "ark-relations", - "ark-serialize", - "ark-snark", - "ark-std", - "blake2", - "derivative", - "digest", - "sha2", -] - -[[package]] -name = "ark-ec" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "defd9a439d56ac24968cca0571f598a61bc8c55f71d50a89cda591cb750670ba" -dependencies = [ - "ark-ff", - "ark-poly", - "ark-serialize", - "ark-std", - "derivative", - "hashbrown 0.13.2", - "itertools", - "num-traits", - "zeroize", -] - -[[package]] -name = "ark-ff" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ec847af850f44ad29048935519032c33da8aa03340876d351dfab5660d2966ba" -dependencies = [ - "ark-ff-asm", - "ark-ff-macros", - "ark-serialize", - "ark-std", - "derivative", - "digest", - "itertools", - "num-bigint", - "num-traits", - "paste", - "rustc_version", - "zeroize", -] - -[[package]] -name = "ark-ff-asm" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3ed4aa4fe255d0bc6d79373f7e31d2ea147bcf486cba1be5ba7ea85abdb92348" -dependencies = [ - "quote", - "syn 1.0.109", -] - -[[package]] -name = "ark-ff-macros" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7abe79b0e4288889c4574159ab790824d0033b9fdcb2a112a3182fac2e514565" -dependencies = [ - "num-bigint", - "num-traits", - "proc-macro2", - "quote", - "syn 1.0.109", -] - -[[package]] -name = "ark-groth16" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "20ceafa83848c3e390f1cbf124bc3193b3e639b3f02009e0e290809a501b95fc" -dependencies = [ - "ark-crypto-primitives", - "ark-ec", - "ark-ff", - "ark-poly", - "ark-relations", - "ark-serialize", - "ark-std", -] - -[[package]] -name = "ark-poly" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d320bfc44ee185d899ccbadfa8bc31aab923ce1558716e1997a1e74057fe86bf" -dependencies = [ - "ark-ff", - "ark-serialize", - "ark-std", - "derivative", - "hashbrown 0.13.2", -] - -[[package]] -name = "ark-relations" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "00796b6efc05a3f48225e59cb6a2cda78881e7c390872d5786aaf112f31fb4f0" -dependencies = [ - "ark-ff", - "ark-std", - "tracing", - "tracing-subscriber", -] - -[[package]] -name = "ark-serialize" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "adb7b85a02b83d2f22f89bd5cac66c9c89474240cb6207cb1efc16d098e822a5" -dependencies = [ - "ark-serialize-derive", - "ark-std", - "digest", - "num-bigint", -] - -[[package]] -name = "ark-serialize-derive" -version = "0.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ae3281bc6d0fd7e549af32b52511e1302185bd688fd3359fa36423346ff682ea" -dependencies = [ - "proc-macro2", - "quote", - "syn 1.0.109", -] - -[[package]] -name = "ark-snark" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "84d3cc6833a335bb8a600241889ead68ee89a3cf8448081fb7694c0fe503da63" -dependencies = [ - "ark-ff", - "ark-relations", - "ark-serialize", - "ark-std", -] - -[[package]] -name = "ark-std" -version = "0.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "94893f1e0c6eeab764ade8dc4c0db24caf4fe7cbbaafc0eba0a9030f447b5185" -dependencies = [ - "num-traits", - "rand", -] - -[[package]] -name = "autocfg" -version = "1.4.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ace50bade8e6234aa140d9a2f552bbee1db4d353f69b8217bc503490fc1a9f26" - -[[package]] -name = "bitflags" -version = "1.3.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bef38d45163c2f1dde094a7dfd33ccf595c92905c8f8f4fdc18d06fb1037718a" - -[[package]] -name = "bitflags" -version = "2.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b048fb63fd8b5923fc5aa7b340d8e156aec7ec02f0c78fa8a6ddc2613f6f71de" - -[[package]] -name = "blake2" -version = "0.10.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "46502ad458c9a52b69d4d4d32775c788b7a1b85e8bc9d482d92250fc0e3f8efe" -dependencies = [ - "digest", -] - -[[package]] -name = "block" -version = "0.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0d8c1fef690941d3e7788d328517591fecc684c084084702d6ff1641e993699a" - -[[package]] -name = "block-buffer" -version = "0.10.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3078c7629b62d3f0439517fa394996acacc5cbc91c5a20d8c658e77abd503a71" -dependencies = [ - "generic-array", -] - -[[package]] -name = "borsh" -version = "1.5.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "2506947f73ad44e344215ccd6403ac2ae18cd8e046e581a441bf8d199f257f03" -dependencies = [ - "borsh-derive", - "cfg_aliases", -] - -[[package]] -name = "borsh-derive" -version = "1.5.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2593a3b8b938bd68373196c9832f516be11fa487ef4ae745eb282e6a56a7244" -dependencies = [ - "once_cell", - "proc-macro-crate", - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "bumpalo" -version = "3.16.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "79296716171880943b8470b5f8d03aa55eb2e645a4874bdbb28adb49162e012c" - -[[package]] -name = "bytemuck" -version = "1.20.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8b37c88a63ffd85d15b406896cc343916d7cf57838a847b3a6f2ca5d39a5695a" -dependencies = [ - "bytemuck_derive", -] - -[[package]] -name = "bytemuck_derive" -version = "1.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bcfcc3cd946cb52f0bbfdbbcfa2f4e24f75ebb6c0e1002f7c25904fada18b9ec" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "byteorder" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1fd0f2584146f6f2ef48085050886acf353beff7305ebd1ae69500e27c67f64b" - -[[package]] -name = "cfg-if" -version = "1.0.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "baf1de4339761588bc0619e3cbc0120ee582ebb74b53b4efbf79117bd2da40fd" - -[[package]] -name = "cfg_aliases" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "613afe47fcd5fac7ccf1db93babcb082c5994d996f20b8b159f2ad1658eb5724" - -[[package]] -name = "clap" -version = "4.5.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fb3b4b9e5a7c7514dfa52869339ee98b3156b0bfb4e8a77c4ff4babb64b1604f" -dependencies = [ - "clap_builder", -] - -[[package]] -name = "clap_builder" -version = "4.5.21" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b17a95aa67cc7b5ebd32aa5370189aa0d79069ef1c64ce893bd30fb24bff20ec" -dependencies = [ - "anstream", - "anstyle", - "clap_lex", - "strsim", -] - -[[package]] -name = "clap_lex" -version = "0.7.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "afb84c814227b90d6895e01398aee0d8033c00e7466aca416fb6a8e0eb19d8a7" - -[[package]] -name = "colorchoice" -version = "1.0.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b63caa9aa9397e2d9480a9b13673856c78d8ac123288526c37d7839f2a86990" - -[[package]] -name = "const-oid" -version = "0.9.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c2459377285ad874054d797f3ccebf984978aa39129f6eafde5cdc8315b612f8" - -[[package]] -name = "core-foundation" -version = "0.9.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "91e195e091a93c46f7102ec7818a2aa394e1e1771c3ab4825963fa03e45afb8f" -dependencies = [ - "core-foundation-sys", - "libc", -] - -[[package]] -name = "core-foundation-sys" -version = "0.8.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "773648b94d0e5d620f64f280777445740e61fe701025087ec8b57f45c791888b" - -[[package]] -name = "core-graphics-types" -version = "0.1.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "45390e6114f68f718cc7a830514a96f903cccd70d02a8f6d9f643ac4ba45afaf" -dependencies = [ - "bitflags 1.3.2", - "core-foundation", - "libc", -] - -[[package]] -name = "cpufeatures" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0ca741a962e1b0bff6d724a1a0958b686406e853bb14061f218562e1896f95e6" -dependencies = [ - "libc", -] - -[[package]] -name = "crc32fast" -version = "1.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a97769d94ddab943e4510d138150169a2758b5ef3eb191a9ee688de3e23ef7b3" -dependencies = [ - "cfg-if", -] - -[[package]] -name = "crossbeam-deque" -version = "0.8.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "613f8cc01fe9cf1a3eb3d7f488fd2fa8388403e97039e2f73692932e291a770d" -dependencies = [ - "crossbeam-epoch", - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-epoch" -version = "0.9.18" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5b82ac4a3c2ca9c3460964f020e1402edd5753411d7737aa39c3714ad1b5420e" -dependencies = [ - "crossbeam-utils", -] - -[[package]] -name = "crossbeam-utils" -version = "0.8.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "22ec99545bb0ed0ea7bb9b8e1e9122ea386ff8a48c0922e43f36d45ab09e0e80" - -[[package]] -name = "crypto-common" -version = "0.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1bfb12502f3fc46cca1bb51ac28df9d618d813cdc3d2f25b9fe775a34af26bb3" -dependencies = [ - "generic-array", - "typenum", -] - -[[package]] -name = "derivative" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fcc3dd5e9e9c0b295d6e1e4d811fb6f157d5ffd784b8d202fc62eac8035a770b" -dependencies = [ - "proc-macro2", - "quote", - "syn 1.0.109", -] - -[[package]] -name = "derive_arbitrary" -version = "1.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "30542c1ad912e0e3d22a1935c290e12e8a29d704a420177a31faad4a601a0800" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "digest" -version = "0.10.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9ed9a281f7bc9b7576e61468ba615a66a5c8cfdff42420a70aa82701a3b1e292" -dependencies = [ - "block-buffer", - "const-oid", - "crypto-common", - "subtle", -] - -[[package]] -name = "displaydoc" -version = "0.2.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "97369cbbc041bc366949bc74d34658d6cda5621039731c6310521892a3a20ae0" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "downcast-rs" -version = "1.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "75b325c5dbd37f80359721ad39aca5a29fb04c89279657cffdda8736d0c0b9d2" - -[[package]] -name = "either" -version = "1.13.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "60b1af1c220855b6ceac025d3f6ecdd2b7c4894bfe9cd9bda4fbb4bc7c0d4cf0" - -[[package]] -name = "elf" -version = "0.7.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4445909572dbd556c457c849c4ca58623d84b27c8fff1e74b0b4227d8b90d17b" - -[[package]] -name = "equivalent" -version = "1.0.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "5443807d6dff69373d433ab9ef5378ad8df50ca6298caf15de6e52e24aaf54d5" - -[[package]] -name = "flate2" -version = "1.0.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c936bfdafb507ebbf50b8074c54fa31c5be9a1e7e5f467dd659697041407d07c" -dependencies = [ - "crc32fast", - "miniz_oxide", -] - -[[package]] -name = "foreign-types" -version = "0.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d737d9aa519fb7b749cbc3b962edcf310a8dd1f4b67c91c4f83975dbdd17d965" -dependencies = [ - "foreign-types-macros", - "foreign-types-shared", -] - -[[package]] -name = "foreign-types-macros" -version = "0.2.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1a5c6c585bc94aaf2c7b51dd4c2ba22680844aba4c687be581871a6f518c5742" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "foreign-types-shared" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "aa9a19cbb55df58761df49b23516a86d432839add4af60fc256da840f66ed35b" - -[[package]] -name = "generic-array" -version = "0.14.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "85649ca51fd72272d7821adaf274ad91c288277713d9c18820d8499a7ff69e9a" -dependencies = [ - "typenum", - "version_check", -] - -[[package]] -name = "getrandom" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c4567c8db10ae91089c99af84c68c38da3ec2f087c3f82960bcdbf3656b6f4d7" -dependencies = [ - "cfg-if", - "libc", - "wasi", -] - -[[package]] -name = "hashbrown" -version = "0.13.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "43a3c133739dddd0d2990f9a4bdf8eb4b21ef50e4851ca85ab661199821d510e" -dependencies = [ - "ahash", -] - -[[package]] -name = "hashbrown" -version = "0.15.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "3a9bfc1af68b1726ea47d3d5109de126281def866b33970e10fbab11b5dafab3" - -[[package]] -name = "hex" -version = "0.4.3" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7f24254aa9a54b5c858eaee2f5bccdb46aaf0e486a595ed5fd8f86ba55232a70" - -[[package]] -name = "hex-literal" -version = "0.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6fe2267d4ed49bc07b63801559be28c718ea06c4738b7a03c94df7386d2cde46" - -[[package]] -name = "indexmap" -version = "2.6.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "707907fe3c25f5424cce2cb7e1cbcafee6bdbe735ca90ef77c29e84591e5b9da" -dependencies = [ - "equivalent", - "hashbrown 0.15.1", -] - -[[package]] -name = "is_terminal_polyfill" -version = "1.70.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7943c866cc5cd64cbc25b2e01621d07fa8eb2a1a23160ee81ce38704e97b8ecf" - -[[package]] -name = "itertools" -version = "0.10.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b0fd2260e829bddf4cb6ea802289de2f86d6a7a690192fbe91b3f46e0f2c8473" -dependencies = [ - "either", -] - -[[package]] -name = "lazy_static" -version = "1.5.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "bbd2bcb4c963f2ddae06a2efc7e9f3591312473c50c6685e1f298068316e66fe" - -[[package]] -name = "libc" -version = "0.2.162" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "18d287de67fe55fd7e1581fe933d965a5a9477b38e949cfa9f8574ef01506398" - -[[package]] -name = "libm" -version = "0.2.11" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8355be11b20d696c8f18f6cc018c4e372165b1fa8126cef092399c9951984ffa" - -[[package]] -name = "lockfree-object-pool" -version = "0.1.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9374ef4228402d4b7e403e5838cb880d9ee663314b0a900d5a6aabf0c213552e" - -[[package]] -name = "log" -version = "0.4.22" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a7a70ba024b9dc04c27ea2f0c0548feb474ec5c54bba33a7f72f873a39d07b24" - -[[package]] -name = "malloc_buf" -version = "0.0.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "62bb907fe88d54d8d9ce32a3cceab4218ed2f6b7d35617cafe9adf84e43919cb" -dependencies = [ - "libc", -] - -[[package]] -name = "memchr" -version = "2.7.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "78ca9ab1a0babb1e7d5695e3530886289c18cf2f87ec19a575a0abdce112e3a3" - -[[package]] -name = "metal" -version = "0.29.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7ecfd3296f8c56b7c1f6fbac3c71cefa9d78ce009850c45000015f206dc7fa21" -dependencies = [ - "bitflags 2.6.0", - "block", - "core-graphics-types", - "foreign-types", - "log", - "objc", - "paste", -] - -[[package]] -name = "miniz_oxide" -version = "0.8.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e2d80299ef12ff69b16a84bb182e3b9df68b5a91574d3d4fa6e41b65deec4df1" -dependencies = [ - "adler2", -] - -[[package]] -name = "num-bigint" -version = "0.4.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "a5e44f723f1133c9deac646763579fdb3ac745e418f2a7af9cd0c431da1f20b9" -dependencies = [ - "num-integer", - "num-traits", -] - -[[package]] -name = "num-integer" -version = "0.1.46" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7969661fd2958a5cb096e56c8e1ad0444ac2bbcd0061bd28660485a44879858f" -dependencies = [ - "num-traits", -] - -[[package]] -name = "num-traits" -version = "0.2.19" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "071dfc062690e90b734c0b2273ce72ad0ffa95f0c74596bc250dcfd960262841" -dependencies = [ - "autocfg", -] - -[[package]] -name = "objc" -version = "0.2.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "915b1b472bc21c53464d6c8461c9d3af805ba1ef837e1cac254428f4a77177b1" -dependencies = [ - "malloc_buf", -] - -[[package]] -name = "once_cell" -version = "1.20.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1261fe7e33c73b354eab43b1273a57c8f967d0391e80353e51f764ac02cf6775" - -[[package]] -name = "paste" -version = "1.0.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "57c0d7b74b563b49d38dae00a0c37d4d6de9b432382b2892f0574ddcae73fd0a" - -[[package]] -name = "pin-project-lite" -version = "0.2.15" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "915a1e146535de9163f3987b8944ed8cf49a18bb0056bcebcdcece385cece4ff" - -[[package]] -name = "ppv-lite86" -version = "0.2.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "77957b295656769bb8ad2b6a6b09d897d94f05c41b069aede1fcdaa675eaea04" -dependencies = [ - "zerocopy", -] - -[[package]] -name = "proc-macro-crate" -version = "3.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8ecf48c7ca261d60b74ab1a7b20da18bede46776b2e55535cb958eb595c5fa7b" -dependencies = [ - "toml_edit", -] - -[[package]] -name = "proc-macro2" -version = "1.0.89" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "f139b0662de085916d1fb67d2b4169d1addddda1919e696f3252b740b629986e" -dependencies = [ - "unicode-ident", -] - -[[package]] -name = "quote" -version = "1.0.37" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b5b9d34b8991d19d98081b46eacdd8eb58c6f2b201139f7c5f643cc155a633af" -dependencies = [ - "proc-macro2", -] - -[[package]] -name = "rand" -version = "0.8.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34af8d1a0e25924bc5b7c43c079c942339d8f0a8b57c39049bef581b46327404" -dependencies = [ - "libc", - "rand_chacha", - "rand_core", -] - -[[package]] -name = "rand_chacha" -version = "0.3.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e6c10a63a0fa32252be49d21e7709d4d4baf8d231c2dbce1eaa8141b9b127d88" -dependencies = [ - "ppv-lite86", - "rand_core", -] - -[[package]] -name = "rand_core" -version = "0.6.4" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ec0be4795e2f6a28069bec0b5ff3e2ac9bafc99e6a9a7dc3547996c5c816922c" -dependencies = [ - "getrandom", -] - -[[package]] -name = "rayon" -version = "1.10.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b418a60154510ca1a002a752ca9714984e21e4241e804d32555251faf8b78ffa" -dependencies = [ - "either", - "rayon-core", -] - -[[package]] -name = "rayon-core" -version = "1.12.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1465873a3dfdaa8ae7cb14b4383657caab0b3e8a0aa9ae8e04b044854c8dfce2" -dependencies = [ - "crossbeam-deque", - "crossbeam-utils", -] - -[[package]] -name = "risc0-binfmt" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "anyhow", - "borsh", - "elf", - "risc0-zkp", - "risc0-zkvm-platform", - "serde", - "syn 2.0.87", - "tracing", -] - -[[package]] -name = "risc0-circuit-keccak" -version = "0.1.0" -dependencies = [ - "anyhow", - "bytemuck", - "clap", - "hex", - "hex-literal", - "lazy_static", - "paste", - "rand", - "rayon", - "risc0-binfmt", - "risc0-circuit-recursion", - "risc0-core", - "risc0-zkp", - "risc0-zkvm", - "risc0-zkvm-platform", - "tracing", - "zip", -] - -[[package]] -name = "risc0-circuit-keccak-test-methods" -version = "0.1.0" -dependencies = [ - "risc0-circuit-keccak", - "risc0-zkvm", -] - -[[package]] -name = "risc0-circuit-recursion" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "anyhow", - "bytemuck", - "hex", - "metal", - "risc0-core", - "risc0-zkp", - "tracing", -] - -[[package]] -name = "risc0-circuit-rv32im" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "anyhow", - "metal", - "risc0-binfmt", - "risc0-core", - "risc0-zkp", - "risc0-zkvm-platform", - "serde", - "tracing", -] - -[[package]] -name = "risc0-core" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "bytemuck", - "rand_core", -] - -[[package]] -name = "risc0-groth16" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "anyhow", - "ark-bn254", - "ark-ec", - "ark-groth16", - "ark-serialize", - "bytemuck", - "hex", - "num-bigint", - "num-traits", - "risc0-binfmt", - "risc0-zkp", - "serde", - "stability", -] - -[[package]] -name = "risc0-zkp" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "anyhow", - "blake2", - "borsh", - "bytemuck", - "cfg-if", - "digest", - "hex", - "hex-literal", - "metal", - "paste", - "rand_core", - "risc0-core", - "risc0-zkvm-platform", - "serde", - "sha2", - "tracing", -] - -[[package]] -name = "risc0-zkvm" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "anyhow", - "borsh", - "bytemuck", - "getrandom", - "hex", - "risc0-binfmt", - "risc0-circuit-recursion", - "risc0-circuit-rv32im", - "risc0-core", - "risc0-groth16", - "risc0-zkp", - "risc0-zkvm-platform", - "rrs-lib", - "semver", - "serde", - "sha2", - "stability", - "tracing", -] - -[[package]] -name = "risc0-zkvm-platform" -version = "1.2.0-alpha.1" -source = "git+https://github.com/risc0/risc0.git?rev=3c20ddcb2f5a707115d1cea896fb375818d798cf#3c20ddcb2f5a707115d1cea896fb375818d798cf" -dependencies = [ - "bytemuck", - "getrandom", - "libm", - "stability", -] - -[[package]] -name = "rrs-lib" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b4382d3af3a4ebdae7f64ba6edd9114fff92c89808004c4943b393377a25d001" -dependencies = [ - "downcast-rs", - "paste", -] - -[[package]] -name = "rustc_version" -version = "0.4.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "cfcb3a22ef46e85b45de6ee7e79d063319ebb6594faafcf1c225ea92ab6e9b92" -dependencies = [ - "semver", -] - -[[package]] -name = "semver" -version = "1.0.23" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "61697e0a1c7e512e84a621326239844a24d8207b4669b41bc18b32ea5cbf988b" - -[[package]] -name = "serde" -version = "1.0.215" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "6513c1ad0b11a9376da888e3e0baa0077f1aed55c17f50e7b2397136129fb88f" -dependencies = [ - "serde_derive", -] - -[[package]] -name = "serde_derive" -version = "1.0.215" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ad1e866f866923f252f05c889987993144fb74e722403468a4ebd70c3cd756c0" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "sha2" -version = "0.10.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "793db75ad2bcafc3ffa7c68b215fee268f537982cd901d132f89c6343f3a3dc8" -dependencies = [ - "cfg-if", - "cpufeatures", - "digest", -] - -[[package]] -name = "simd-adler32" -version = "0.3.7" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d66dc143e6b11c1eddc06d5c423cfc97062865baf299914ab64caa38182078fe" - -[[package]] -name = "stability" -version = "0.2.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "d904e7009df136af5297832a3ace3370cd14ff1546a232f4f185036c2736fcac" -dependencies = [ - "quote", - "syn 2.0.87", -] - -[[package]] -name = "strsim" -version = "0.11.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "7da8b5736845d9f2fcb837ea5d9e2628564b3b043a70948a3f0b778838c5fb4f" - -[[package]] -name = "subtle" -version = "2.6.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "13c2bddecc57b384dee18652358fb23172facb8a2c51ccc10d74c157bdea3292" - -[[package]] -name = "syn" -version = "1.0.109" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "72b64191b275b66ffe2469e8af2c1cfe3bafa67b529ead792a6d0160888b4237" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "syn" -version = "2.0.87" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "25aa4ce346d03a6dcd68dd8b4010bcb74e54e62c90c573f394c46eae99aba32d" -dependencies = [ - "proc-macro2", - "quote", - "unicode-ident", -] - -[[package]] -name = "thiserror" -version = "1.0.69" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "b6aaf5339b578ea85b50e080feb250a3e8ae8cfcdff9a461c9ec2904bc923f52" -dependencies = [ - "thiserror-impl", -] - -[[package]] -name = "thiserror-impl" -version = "1.0.69" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4fee6c4efc90059e10f81e6d42c60a18f76588c3d74cb83a0b242a2b6c7504c1" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "toml_datetime" -version = "0.6.8" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0dd7358ecb8fc2f8d014bf86f6f638ce72ba252a2c3a2572f2a795f1d23efb41" - -[[package]] -name = "toml_edit" -version = "0.22.22" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "4ae48d6208a266e853d946088ed816055e556cc6028c5e8e2b84d9fa5dd7c7f5" -dependencies = [ - "indexmap", - "toml_datetime", - "winnow", -] - -[[package]] -name = "tracing" -version = "0.1.40" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c3523ab5a71916ccf420eebdf5521fcef02141234bbc0b8a49f2fdc4544364ef" -dependencies = [ - "log", - "pin-project-lite", - "tracing-attributes", - "tracing-core", -] - -[[package]] -name = "tracing-attributes" -version = "0.1.27" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "34704c8d6ebcbc939824180af020566b01a7c01f80641264eba0999f6c2b6be7" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "tracing-core" -version = "0.1.32" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "c06d3da6113f116aaee68e4d601191614c9053067f9ab7f6edbcb161237daa54" -dependencies = [ - "once_cell", - "valuable", -] - -[[package]] -name = "tracing-subscriber" -version = "0.2.25" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0e0d2eaa99c3c2e41547cfa109e910a68ea03823cccad4a0525dcbc9b01e8c71" -dependencies = [ - "tracing-core", -] - -[[package]] -name = "typenum" -version = "1.17.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "42ff0bf0c66b8238c6f3b578df37d0b7848e55df8577b3f74f92a69acceeb825" - -[[package]] -name = "unicode-ident" -version = "1.0.13" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e91b56cd4cadaeb79bbf1a5645f6b4f8dc5bde8834ad5894a8db35fda9efa1fe" - -[[package]] -name = "utf8parse" -version = "0.2.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "06abde3611657adf66d383f00b093d7faecc7fa57071cce2578660c9f1010821" - -[[package]] -name = "valuable" -version = "0.1.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "830b7e5d4d90034032940e4ace0d9a9a057e7a45cd94e6c007832e39edb82f6d" - -[[package]] -name = "version_check" -version = "0.9.5" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0b928f33d975fc6ad9f86c8f283853ad26bdd5b10b7f1542aa2fa15e2289105a" - -[[package]] -name = "wasi" -version = "0.11.0+wasi-snapshot-preview1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9c8d87e72b64a3b4db28d11ce29237c246188f4f51057d65a7eab63b7987e423" - -[[package]] -name = "windows-sys" -version = "0.59.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1e38bc4d79ed67fd075bcc251a1c39b32a1776bbe92e5bef1f0bf1f8c531853b" -dependencies = [ - "windows-targets", -] - -[[package]] -name = "windows-targets" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "9b724f72796e036ab90c1021d4780d4d3d648aca59e491e6b98e725b84e99973" -dependencies = [ - "windows_aarch64_gnullvm", - "windows_aarch64_msvc", - "windows_i686_gnu", - "windows_i686_gnullvm", - "windows_i686_msvc", - "windows_x86_64_gnu", - "windows_x86_64_gnullvm", - "windows_x86_64_msvc", -] - -[[package]] -name = "windows_aarch64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "32a4622180e7a0ec044bb555404c800bc9fd9ec262ec147edd5989ccd0c02cd3" - -[[package]] -name = "windows_aarch64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "09ec2a7bb152e2252b53fa7803150007879548bc709c039df7627cabbd05d469" - -[[package]] -name = "windows_i686_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "8e9b5ad5ab802e97eb8e295ac6720e509ee4c243f69d781394014ebfe8bbfa0b" - -[[package]] -name = "windows_i686_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "0eee52d38c090b3caa76c563b86c3a4bd71ef1a819287c19d586d7334ae8ed66" - -[[package]] -name = "windows_i686_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "240948bc05c5e7c6dabba28bf89d89ffce3e303022809e73deaefe4f6ec56c66" - -[[package]] -name = "windows_x86_64_gnu" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "147a5c80aabfbf0c7d901cb5895d1de30ef2907eb21fbbab29ca94c5b08b1a78" - -[[package]] -name = "windows_x86_64_gnullvm" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "24d5b23dc417412679681396f2b49f3de8c1473deb516bd34410872eff51ed0d" - -[[package]] -name = "windows_x86_64_msvc" -version = "0.52.6" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "589f6da84c646204747d1270a2a5661ea66ed1cced2631d546fdfb155959f9ec" - -[[package]] -name = "winnow" -version = "0.6.20" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "36c1fec1a2bb5866f07c25f68c26e565c4c200aebb96d7e55710c19d3e8ac49b" -dependencies = [ - "memchr", -] - -[[package]] -name = "zerocopy" -version = "0.7.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "1b9b4fd18abc82b8136838da5d50bae7bdea537c574d8dc1a34ed098d6c166f0" -dependencies = [ - "byteorder", - "zerocopy-derive", -] - -[[package]] -name = "zerocopy-derive" -version = "0.7.35" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "fa4f8080344d4671fb4e831a13ad1e68092748387dfc4f55e356242fae12ce3e" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "zeroize" -version = "1.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ced3678a2879b30306d323f4542626697a464a97c0a07c9aebf7ebca65cd4dde" -dependencies = [ - "zeroize_derive", -] - -[[package]] -name = "zeroize_derive" -version = "1.4.2" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "ce36e65b0d2999d2aafac989fb249189a141aee1f53c612c1f37d72631959f69" -dependencies = [ - "proc-macro2", - "quote", - "syn 2.0.87", -] - -[[package]] -name = "zip" -version = "2.2.0" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "dc5e4288ea4057ae23afc69a4472434a87a2495cafce6632fd1c4ec9f5cf3494" -dependencies = [ - "arbitrary", - "crc32fast", - "crossbeam-utils", - "displaydoc", - "flate2", - "indexmap", - "memchr", - "thiserror", - "zopfli", -] - -[[package]] -name = "zopfli" -version = "0.8.1" -source = "registry+https://github.com/rust-lang/crates.io-index" -checksum = "e5019f391bac5cf252e93bbcc53d039ffd62c7bfb7c150414d61369afe57e946" -dependencies = [ - "bumpalo", - "crc32fast", - "lockfree-object-pool", - "log", - "once_cell", - "simd-adler32", -] diff --git a/zirgen/circuit/keccak/one_hot.zir b/zirgen/circuit/keccak/one_hot.zir index 34a12878..438dbc04 100644 --- a/zirgen/circuit/keccak/one_hot.zir +++ b/zirgen/circuit/keccak/one_hot.zir @@ -1,4 +1,4 @@ -// RUN: zirgen -I zirgen/%S --test %s +// RUN: zirgen -I %S --test %s import bits; diff --git a/zirgen/circuit/keccak2/pack.zir b/zirgen/circuit/keccak/pack.zir similarity index 100% rename from zirgen/circuit/keccak2/pack.zir rename to zirgen/circuit/keccak/pack.zir diff --git a/zirgen/circuit/keccak2/predicates.cpp b/zirgen/circuit/keccak/predicates.cpp similarity index 98% rename from zirgen/circuit/keccak2/predicates.cpp rename to zirgen/circuit/keccak/predicates.cpp index b7d85f0c..5d76c94e 100644 --- a/zirgen/circuit/keccak2/predicates.cpp +++ b/zirgen/circuit/keccak/predicates.cpp @@ -1,4 +1,4 @@ -// Copyright 2024 RISC Zero, Inc. +// Copyright 2025 RISC Zero, Inc. // // Licensed under the Apache License, Version 2.0 (the "License"); // you may not use this file except in compliance with the License. diff --git a/zirgen/circuit/keccak2/sha2.zir b/zirgen/circuit/keccak/sha2.zir similarity index 100% rename from zirgen/circuit/keccak2/sha2.zir rename to zirgen/circuit/keccak/sha2.zir diff --git a/zirgen/circuit/keccak/sha256_for_keccak.zir b/zirgen/circuit/keccak/sha256_for_keccak.zir deleted file mode 100644 index 9e41cb30..00000000 --- a/zirgen/circuit/keccak/sha256_for_keccak.zir +++ /dev/null @@ -1,417 +0,0 @@ -//import one_hot; - -component s2a(rtuple: RetTuple) { - a1 := rtuple.arr_e; - a2 := for i : 0..10 { rtuple.arr_f[i] }; - vConcatenate<22,10>(a1, a2) -} -component s2e(rtuple: RetTuple) { - e1 := for i : 10..22 { rtuple.arr_f[i] }; - e2 := for i : 0..20 { rtuple.arr_c[i] }; - vConcatenate<12,20>(e1, e2) -} -component s2w(rtuple: RetTuple) { - w1 := rtuple.arr_a; - w2 := for i : 0..10 { rtuple.arr_b[i] }; - vConcatenate<22,10>(w1, w2) -} - -component w2s(w_: Array) { - public a := for i : 0..22 { NondetReg(w_[i]) }; - for i : 0..22 { AliasLayout!(a[i], w_[i]); }; - - public b := for i : 22..32 { NondetReg(w_[i]) }; - for i : 22..32 { AliasLayout!(b[i-22], w_[i]); }; -} - -component ae2s(a_: Array, e_: Array) { - public e := for i : 0..22 { NondetReg(a_[i]) }; - for i : 0..22 { AliasLayout!(e[i], a_[i]); }; - - f1 := for i : 22..32 { NondetReg(a_[i]) }; - for i : 22..32 { AliasLayout!(f1[i-22], a_[i]); }; - f2 := for i : 0..12 { NondetReg(e_[i]) }; - for i : 0..12 { AliasLayout!(f2[i], e_[i]); }; - public f := Concatenate<10,12>(f1, f2); - - public c := for i : 12..32 { NondetReg(e_[i]) }; - for i : 12..32 { AliasLayout!(c[i-12], e_[i]); }; -} - -component IVvals(i: Val) { - arr := [[0x6a09, 0xe667], - [0xbb67, 0xae85], - [0x3c6e, 0xf372], - [0xa54f, 0xf53a], - [0x510e, 0x527f], - [0x9b05, 0x688c], - [0x1f83, 0xd9ab], - [0x5be0, 0xcd19]]; - TwoShorts(arr[i][1],arr[i][0]) -} - -component sha256rc_table() { - arr := [[0x428a,0x2f98],[0x7137,0x4491],[0xb5c0,0xfbcf],[0xe9b5,0xdba5], - [0x3956,0xc25b],[0x59f1,0x11f1],[0x923f,0x82a4],[0xab1c,0x5ed5], - [0xd807,0xaa98],[0x1283,0x5b01],[0x2431,0x85be],[0x550c,0x7dc3], - [0x72be,0x5d74],[0x80de,0xb1fe],[0x9bdc,0x06a7],[0xc19b,0xf174], - [0xe49b,0x69c1],[0xefbe,0x4786],[0x0fc1,0x9dc6],[0x240c,0xa1cc], - [0x2de9,0x2c6f],[0x4a74,0x84aa],[0x5cb0,0xa9dc],[0x76f9,0x88da], - [0x983e,0x5152],[0xa831,0xc66d],[0xb003,0x27c8],[0xbf59,0x7fc7], - [0xc6e0,0x0bf3],[0xd5a7,0x9147],[0x06ca,0x6351],[0x1429,0x2967], - [0x27b7,0x0a85],[0x2e1b,0x2138],[0x4d2c,0x6dfc],[0x5338,0x0d13], - [0x650a,0x7354],[0x766a,0x0abb],[0x81c2,0xc92e],[0x9272,0x2c85], - [0xa2bf,0xe8a1],[0xa81a,0x664b],[0xc24b,0x8b70],[0xc76c,0x51a3], - [0xd192,0xe819],[0xd699,0x0624],[0xf40e,0x3585],[0x106a,0xa070], - [0x19a4,0xc116],[0x1e37,0x6c08],[0x2748,0x774c],[0x34b0,0xbcb5], - [0x391c,0x0cb3],[0x4ed8,0xaa4a],[0x5b9c,0xca4f],[0x682e,0x6ff3], - [0x748f,0x82ee],[0x78a5,0x636f],[0x84c8,0x7814],[0x8cc7,0x0208], - [0x90be,0xfffa],[0xa450,0x6ceb],[0xbef9,0xa3f7],[0xc671,0x78f2]]; - TwoShorts(arr[i][1],arr[i][0]) -} - -component TwoShorts(lsbs: Val, msbs: Val) { - public low := lsbs; - public high := msbs; -} - -component rightRotate(a: Array) { - for i : 0..A { - wraparound := InRange(0,i,A-N); - //[wraparound, 1-wraparound] -> (a[i+N], a[i+N-A]) - wraparound*a[i+N] + (1-wraparound)*a[i+N-A] - } -} - -component rightShift(a: Array) { - for i : 0..A { - wraparound := InRange(0,i,A-N); - //[wraparound, 1-wraparound] -> (wraparound*a[i+N], 0) - wraparound*a[i+N] + 0 - } - //for i : 0..A-N { AliasLayout!( r[i], a[i+N]); }; -} - -component xor3a(x: Array, - y: Array, z: Array) { - for i : 0..N { - ( (x[i]*y[i] + (1-x[i])*(1-y[i])) * z[i] ) + - ( (1-(x[i]*y[i] + (1-x[i])*(1-y[i]))) * (1-z[i]) ) } -} - -component maj3(x: Array, - y: Array, z: Array) { - for i : 0..N - { x[i]*y[i]*(1-z[i]) + - x[i]*(1-y[i])*z[i] + - (1-x[i])*y[i]*z[i] + x[i]*y[i]*z[i] } -} - -component ch(x: Array, - y: Array, z: Array) { - for i : 0..N { x[i]*y[i] + (1-x[i])*z[i] } -} - -component pack2(arr: Array) { - low := FromBits<16>(for i : 0..16 { arr[i] }); - high := FromBits<16>(for i : 16..32 { arr[i] }); - TwoShorts(low, high) -} - -component pack2rev(arr: Array) { - lowest := FromBits<8>(for i : 0..8 { arr[i] }); - midlow := FromBits<8>(for i : 8..16 { arr[i] }); - midhigh := FromBits<8>(for i : 16..24 { arr[i] }); - highest := FromBits<8>(for i : 24..32 { arr[i] }); - TwoShorts(lowest*256+midlow, midhigh*256+highest) -} - -component add(a: TwoShorts, b: TwoShorts) { - TwoShorts(a.low + b.low, a.high + b.high) -} - -component computeW(w_2: Array, w_7: Array, - w_15: Array, w_16: Array) { - s0 := xor3a<32>(rightRotate<32,7>(w_15), - rightRotate<32,18>(w_15), rightShift<32,3>(w_15)); - s1 := xor3a<32>(rightRotate<32,17>(w_2), - rightRotate<32,19>(w_2), rightShift<32,10>(w_2)); - pack_s0 := pack2(s0); - pack_s1 := pack2(s1); - add(pack2(w_16), add(pack_s0, add(pack2(w_7), pack_s1))) -} - -component computeAE(a_: Array, b_: Array, - c_: Array, d_: Array, - e_: Array, f_: Array, - g_: Array, h_: Array, - w_: Array, k_rc: TwoShorts) { - s0 := xor3a<32>(rightRotate<32,2>(a_), - rightRotate<32,13>(a_), rightRotate<32,22>(a_)); - s1 := xor3a<32>(rightRotate<32,6>(e_), - rightRotate<32,11>(e_), rightRotate<32,25>(e_)); - pack_ch := pack2(ch<32>(e_, f_, g_)); - stage1 := - add(pack2(w_), add(k_rc, add(pack2(h_), add(pack_ch, pack2(s1))))); - pack_maj := pack2(maj3<32>(a_, b_, c_)); - public aOut := add(stage1, add(pack_maj, pack2(s0))); - public eOut := add(stage1, pack2(d_)); -} - -component unpack_with_carry(low: Val, high: Val) { - low_bits := ToBitsU<19>(low); - FromBits<19>(low_bits) = low; - carry := low_bits[16] + 2*low_bits[17] + 4*low_bits[18]; - high_plus_carry := high + carry; - high_bits := ToBitsU<20>(high_plus_carry); - FromBits<20>(high_bits) = high_plus_carry; - low16 := for i : 0..16 { low_bits[i] }; - high16 := for i : 0..16 { high_bits[i] }; - public carrybits := Concatenate<3,4>( - for i : 16..19 { low_bits[i] }, - for i : 16..20 { high_bits[i] }); - Concatenate<16,16>(low16, high16) -} - -component sha256load(rvals: RetTuple, - aux_regs: Array) { - rvprev01 := rvals@1; - rvprev02 := rvals@2; - rvprev03 := rvals@3; - rvprev04 := rvals@4; - - idx := rvprev01.blk; - within := rvprev01.midx + 1 - idx; - invWithin := NondetReg(Inv(within)); - within*invWithin = 1; - - flag := rvprev01.rnd; - rs : Array; - [1-flag, flag] -> ( - { ReadMemory(idx, rs@0); }, - { AliasLayout!(Reg(rvprev01.arr_d[RLEN()-3]), rs@0[0]); - AliasLayout!(Reg(rvprev01.arr_d[RLEN()-2]), rs@0[1]); - AliasLayout!(NondetReg(0), rs@0[2]); - AliasLayout!(NondetReg(0), rs@0[3]); - AliasLayout!(NondetReg(0), rs@0[4]); - }); - vals := rs@0; - - nxt := [1-flag, flag] -> ([1,idx], [0,idx+1]); - - inp1 := vals[0]; - high_w := ToBitsU<16>(inp1); //big endian - FromBits<16>(high_w) = inp1; - inp2 := vals[1]; - low_w := ToBitsU<16>(inp2); - FromBits<16>(low_w) = inp2; - unpacked_w := [low_w[8],low_w[9],low_w[10],low_w[11], - low_w[12],low_w[13],low_w[14],low_w[15], - low_w[0],low_w[1],low_w[2],low_w[3], - low_w[4],low_w[5],low_w[6],low_w[7], - high_w[8],high_w[9],high_w[10],high_w[11], - high_w[12],high_w[13],high_w[14],high_w[15], - high_w[0],high_w[1],high_w[2],high_w[3], - high_w[4],high_w[5],high_w[6],high_w[7]]; - - compae := computeAE( - s2a(rvprev01), s2a(rvprev02), s2a(rvprev03), s2a(rvprev04), - s2e(rvprev01), s2e(rvprev02), s2e(rvprev03), s2e(rvprev04), - unpacked_w, sha256rc_table()); - new_a := unpack_with_carry(compae.aOut.low, compae.aOut.high); - new_e := unpack_with_carry(compae.eOut.low, compae.eOut.high); - Z := Isz(I-15); - stae := ae2s(new_a, new_e); - stw := w2s(unpacked_w); - tmpb := Concatenate<7,5>( - new_a.carrybits, for i : 0..5 { new_e.carrybits[i]} ); - padb := Concatenate<10,12>(stw.b, tmpb); - padc := Concatenate<20,2>(stae.c, for i : 5..7 {new_e.carrybits[i]}); - d := Concatenate(for i : 0..RLEN()-6 { NondetReg(0) }, - [invWithin,vals[0],vals[1],vals[2],vals[3],vals[4]]); - [1-Z, Z] -> ( - RetTuple(stw.a, padb, padc, d, stae.e, stae.f, - I+1, S2MAJOR_LOAD(), nxt[0], nxt[1], rvprev01.midx, aux_regs), - RetTuple(stw.a, padb, padc, d, stae.e, stae.f, - 0, S2MAJOR_MIX(), nxt[0], nxt[1], rvprev01.midx, aux_regs)) -} - -component sha256load_all(rvals: RetTuple) { - m := OneHotU(rvals@1.minor); - for i : AUXLEN()-AUXBIN()..AUXLEN() { 0 = m[i] * (1-m[i]); }; - r := m -> (sha256load<0>(rvals, m), - sha256load<1>(rvals, m), - sha256load<2>(rvals, m), - sha256load<3>(rvals, m), - sha256load<4>(rvals, m), - sha256load<5>(rvals, m), - sha256load<6>(rvals, m), - sha256load<7>(rvals, m), - sha256load<8>(rvals, m), - sha256load<9>(rvals, m), - sha256load<10>(rvals, m), - sha256load<11>(rvals, m), - sha256load<12>(rvals, m), - sha256load<13>(rvals, m), - sha256load<14>(rvals, m), - sha256load<15>(rvals, m)); - for i : 0..BLEN() { 0 = r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..BLEN() { 0 = r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..BLEN() { 0 = r.arr_c[i] * (1-r.arr_c[i]); }; - r -} - -component sha256mix(rvals: RetTuple, - aux_regs: Array) { - rvprev01 := rvals@1; - rvprev02 := rvals@2; - rvprev03 := rvals@3; - rvprev04 := rvals@4; - rvprev07 := rvals@7; - rvprev15 := rvals@15; - rvprev16 := rvals@16; - - packed_w := computeW(s2w(rvprev02), s2w(rvprev07), s2w(rvprev15), s2w(rvprev16)); - new_w := unpack_with_carry(packed_w.low, packed_w.high); - compae := computeAE(s2a(rvprev01), s2a(rvprev02), s2a(rvprev03), s2a(rvprev04), - s2e(rvprev01), s2e(rvprev02), s2e(rvprev03), s2e(rvprev04), - new_w, sha256rc_table<(S+1)*16+I>()); - new_a := unpack_with_carry(compae.aOut.low, compae.aOut.high); - new_e := unpack_with_carry(compae.eOut.low, compae.eOut.high); - stae := ae2s(new_a, new_e); - stw := w2s(new_w); - tmpb := Concatenate<7,5>( - new_a.carrybits, for i : 0..5 {new_e.carrybits[i]}); - padb := Concatenate<10,12>(stw.b, tmpb); - padc := Concatenate<20,2>(stae.c, for i : 5..7 {new_e.carrybits[i]}); - tmpd := ConcatZeros<7,15>(new_w.carrybits); - d := Concatenate<22,2>( - tmpd, [Reg(rvprev01.arr_d[RLEN()-2]),Reg(rvprev01.arr_d[RLEN()-1])]); - - Z := Isz(I-15); - [1-Z, Z] -> ( - RetTuple(stw.a, padb, padc, d, stae.e, stae.f, - I+1, S2MAJOR_MIX()+S, 0, rvprev01.blk, rvprev01.midx, aux_regs), - { F := Isz(S-2); - [1-F, F] -> ( - RetTuple(stw.a, padb, padc, d, stae.e, stae.f, - 0, S2MAJOR_MIX()+S+1, - rvprev01.rnd, rvprev01.blk, rvprev01.midx, aux_regs), - RetTuple(stw.a, padb, padc, d, stae.e, stae.f, - S2MINOR_SKIP()+S2MINOR_FINI(), S2MAJOR_SETUP(), - rvprev01.rnd, rvprev01.blk, rvprev01.midx, aux_regs)) - }) -} - -component sha256mix_all(rvals: RetTuple) { - m := OneHotU(rvals@1.minor); - for i : AUXLEN()-AUXBIN()..AUXLEN() { 0 = m[i] * (1-m[i]); }; - r := m -> (sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m), - sha256mix(rvals, m)); - for i : 0..BLEN() { 0 = r.arr_a[i] * (1-r.arr_a[i]); }; - for i : 0..BLEN() { 0 = r.arr_b[i] * (1-r.arr_b[i]); }; - for i : 0..BLEN() { 0 = r.arr_c[i] * (1-r.arr_c[i]); }; - for i : 0..7 { 0 = r.arr_d[i] * (1-r.arr_d[i]); }; - r -} - -component sha256init(rvprev01: RetTuple, - auxr: Array) { - packed_a := IVvals(4-I); - low_a := ToBitsU<16>(packed_a.low); - FromBits<16>(low_a) = packed_a.low; - high_a := ToBitsU<16>(packed_a.high); - FromBits<16>(high_a) = packed_a.high; - unpacked_a := Concatenate<16,16>(low_a, high_a); - packed_e := IVvals(8-I); - low_e := ToBitsU<16>(packed_e.low); - FromBits<16>(low_e) = packed_e.low; - high_e := ToBitsU<16>(packed_e.high); - FromBits<16>(high_e) = packed_e.high; - unpacked_e := Concatenate<16,16>(low_e, high_e); - - stae := ae2s(unpacked_a, unpacked_e); - padc := ConcatZeros<20,2>(stae.c); - Z := Isz(4-I); - [1-Z, Z] -> ( - RetTuple(dummyB(), dummyB(), padc, dummyE(), stae.e, stae.f, - S2MINOR_SKIP()+I, S2MAJOR_SETUP(), 0, 0, rvprev01.midx, auxr), - RetTuple(dummyB(), dummyB(), padc, dummyE(), stae.e, stae.f, - 0, S2MAJOR_LOAD(), 0, 0, rvprev01.midx, auxr)) -} - -component ShaOutput(vals: Array) { - vals := for v : vals { Reg(v) }; -} - -component sha256fini(rvals: RetTuple, - auxr: Array) { - rvprev01 := rvals@1; - rvprev02 := rvals@2; - rvprev03 := rvals@3; - rvprev04 := rvals@4; - rvprev68 := rvals@68; - - packed_a := add(pack2(s2a(rvprev04)), pack2(s2a(rvprev68))); - new_a := unpack_with_carry(packed_a.low, packed_a.high); - packed_e := add(pack2(s2e(rvprev04)), pack2(s2e(rvprev68))); - new_e := unpack_with_carry(packed_e.low, packed_e.high); - stae := ae2s(new_a, new_e); - tmp14 := Concatenate<7,7>(new_a.carrybits, new_e.carrybits); - pada := ConcatZeros<14,8>(tmp14); - padc := ConcatZeros<20,2>(stae.c); - - Z := Isz(8-I); - moreInput := rvprev01.midx + 1 - rvprev01.blk; - invMoreInput := NondetReg(Inv(moreInput)); - prod := Reg(moreInput*invMoreInput); - moreInput*(1-prod) = 0; - d_suffix := [prod, Reg(rvprev01.arr_d[22]), Reg(rvprev01.arr_d[23])]; - d := Concatenate<21,3>(dummyS(), d_suffix); - zb := ConcatElem(dummyS(), invMoreInput); - [1-Z, Z] -> ( - RetTuple(pada, zb, padc, d, stae.e, stae.f, - S2MINOR_SKIP()+I, S2MAJOR_SETUP(), - rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr), - { - [prod, 1-prod] -> ( - RetTuple(pada, zb, padc, d, stae.e, stae.f, - 0, S2MAJOR_LOAD(), - rvprev01.rnd, rvprev01.blk, rvprev01.midx, auxr), - { fa := pack2rev(new_a); - fb := pack2rev(s2a(rvprev01)); - fc := pack2rev(s2a(rvprev02)); - fd := pack2rev(s2a(rvprev03)); - fe := pack2rev(new_e); - ff := pack2rev(s2e(rvprev01)); - fg := pack2rev(s2e(rvprev02)); - fh := pack2rev(s2e(rvprev03)); - res := [fa.high, fa.low, fb.high, fb.low, - fc.high, fc.low, fd.high, fd.low, - fe.high, fe.low, ff.high, ff.low, - fg.high, fg.low, fh.high, fh.low]; - Log("sha256output: %x,%x %x,%x %x,%x %x,%x %x,%x %x,%x %x,%x %x,%x", - res[0], res[1], res[2], res[3], - res[4], res[5], res[6], res[7], - res[8], res[9], res[10], res[11], - res[12], res[13], res[14], res[15]); - global output := ShaOutput(res); - RetTuple(pada, zb, padc, d, stae.e, stae.f, - S2MINOR_SKIP()+S2MINOR_OUTPUT(), S2MAJOR_SETUP(), - 0, 0, 0, auxr) - })}) -} diff --git a/zirgen/circuit/keccak/test0k.nop b/zirgen/circuit/keccak/test0k.nop deleted file mode 100644 index 08509856..00000000 --- a/zirgen/circuit/keccak/test0k.nop +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: zirgen -I %S --test %s --test-cycles 3000 --input-data-hex 010000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080c5d2460186f7233c927e7db2dcc703c0e500b653ca82273b7bfad8045d85a4700000000000000000 2>&1 | FileCheck %s - -import keccak; - -test TestKeccak00k { // test_cycles >= 2974 -// CHECK-LABEL: Running TestKeccak00k -// CHECK: sha256output: 0xc376,0xd218 0xa46f,0x1750 0xd163,0xea2 0xf9dc,0xb7a 0xc1ca,0xe1a6 0xa6a,0x259b 0x1023,0x7c1a 0xa863,0x32a8 -// CHECK: final accum: [0, 0, 0, 0] - Top () -} - diff --git a/zirgen/circuit/keccak/test0s.nop b/zirgen/circuit/keccak/test0s.nop deleted file mode 100644 index 16908b20..00000000 --- a/zirgen/circuit/keccak/test0s.nop +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: zirgen -I %S --test %s --test-cycles 3000 --input-data-hex 010000000000000006000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080a7ffc6f8bf1ed76651c14756a061d662f580ff4de43b49fa82d80a4b80f8434a0000000000000000 2>&1 | FileCheck %s - -import keccak; - -test TestKeccak00s { // test_cycles >= 2974 -// CHECK-LABEL: Running TestKeccak00s -// CHECK: sha256output: 0xd7da,0x872c 0x1921,0x7174 0x4dcf,0x92da 0xa191,0xf653 0x4c9f,0x10be 0xac8,0x7e90 0xf316,0x6b75 0x97c5,0xcca0 -// CHECK: final accum: [0, 0, 0, 0] - Top () -} - diff --git a/zirgen/circuit/keccak/test1k.zir b/zirgen/circuit/keccak/test1k.zir deleted file mode 100644 index 3816c0e6..00000000 --- a/zirgen/circuit/keccak/test1k.zir +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: zirgen -I %S --test %s --test-cycles 3000 --input-data-hex 010000000000000054686520717569636B2062726F776E20666F78206A756D7073206F76657220746865206C617A7920646F672E0100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080578951e24efd62a3d63a86f7cd19aaa53c898fe287d2552133220370240b572d0000000000000000 2>&1 | FileCheck %s - -import keccak; - -test TestKeccak01k { // test_cycles >= 2974 -// CHECK-LABEL: Running TestKeccak01k -// CHECK: sha256output: 0x95b3,0x6374 0x988e,0x6e0a 0xec7c,0xb317 0x54fd,0x4847 0xb009,0x9392 0xdafc,0x4759 0x3f57,0x7866 0x8a26,0xc723 -// CHECK: final accum: [0, 0, 0, 0] - Top () -} - diff --git a/zirgen/circuit/keccak/test1s.nop b/zirgen/circuit/keccak/test1s.nop deleted file mode 100644 index fc60dece..00000000 --- a/zirgen/circuit/keccak/test1s.nop +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: zirgen -I %S --test %s --test-cycles 3000 --input-data-hex 010000000000000054686520717569636B2062726F776E20666F78206A756D7073206F76657220746865206C617A7920646F672E0600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080a80f839cd4f83f6c3dafc87feae470045e4eb0d366397d5c6ce34ba1739f734d0000000000000000 2>&1 | FileCheck %s - -import keccak; - -test TestKeccak01s { // test_cycles >= 2974 -// CHECK-LABEL: Running TestKeccak01s -// CHECK: sha256output: 0xe656,0x6db2 0xbe09,0x4313 0x98b6,0xe5eb 0xdd04,0x85b1 0xdd60,0x6831 0x18a,0x5515 0xab3b,0xfffd 0xa2f3,0xdbe0 -// CHECK: final accum: [0, 0, 0, 0] - Top () -} - diff --git a/zirgen/circuit/keccak/test2k.zir b/zirgen/circuit/keccak/test2k.zir deleted file mode 100644 index b6619ccb..00000000 --- a/zirgen/circuit/keccak/test2k.zir +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: zirgen -I %S --test %s --test-cycles 23000 --input-data-hex 0600000000000000436F6D6D616E64657220526F64657269636B20426C61696E65206C6F6F6B6564206672616E746963616C6C792061726F756E6420746865206272696467652E20776865726520686973206F66666963657273207765726520646972656374696E6720726570616972732077697468206C6F7720616E6420757267656E7420766F696365732C2073757267656F6E7320617373697374696E67206174206120646966666963756C74206F7065726174696F6E2E20546865206772617920737465656C20636F6D706172746D656E7420776173206120636F6E667573696F6E206F6620616374697669746965732C2065616368206F726465726C7920627920697473656C662062757420746865206F766572616C6C20696D7072657373696F6E20776173206F66206368616F732E2053637265656E732061626F7665206F6E652068656C6D736D616E27732073746174696F6E2073686F7765642074686520706C616E65742062656C6F7720616E6420746865206F746865722C20736869707320696E206F72626974206E656172204D61634172746875722C20627574206576657279776865726520656C7365207468652070616E656C20636F7665727320686164206265656E2072656D6F7665642066726F6D20636F6E736F6C65732C207465737420696E737472756D656E7473207765726520636C697070656420696E746F20746865697220696E73696465732C20616E6420746563686E696369616E732073746F6F64206279207769746820636F6C6F722D636F64656420656C656374726F6E696320617373656D626C69657320746F207265706C6163652065766572797468696E672074686174207365656D656420646F75627466756C2E205468756D707320616E64207768696E657320736F756E646564207468726F75676820746865207368697020383920736F6D657768657265206166742074686520656E67696E656572696E67206372657720776F726B6564206F6E207468652068756C6C2E01000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008028c3f5c69c21be780e5508d355ebf7d5e060f203ca8717447b71cb44544df5c70200000000000000546865736520776F7264732077657265207574746572656420696E204A756C79203138303520627920416E6E61205061766C6F766E6120536368657265722C20612064697374696E67756973686564206C616479206F662074686520636F7572742C20616E6420636F6E666964656E7469616C206D6169642D6F662D686F6E6F757220746F2074686520456D7072657373204D617279612046796F646F726F766E612E2049742077617320686572206772656574696E6720746F205072696E63652056617373696C792C2061206D616E206869676820696E2072616E6B20616E64206F66666963652C2077686F207761732074686520666972737420746F2061727269766520617401000000000000804bdc1874a3125f1f911fe8c76ac8443a6ec623ef91bc58eabf54c5762097894d0000000000000000 2>&1 | FileCheck %s - -import keccak; - -test TestKeccak02k { // test_cycles >= 22776 -// CHECK-LABEL: Running TestKeccak02k -// CHECK: sha256output: 0xe42,0x2c6b 0xcdc4,0x6e39 0x6bcf,0x4c7e 0x4c8b,0x1e1c 0xc388,0x9558 0xb534,0xfd81 0x3713,0xa693 0x30e5,0xf106 -// CHECK: final accum: [0, 0, 0, 0] - Top () -} - diff --git a/zirgen/circuit/keccak/test2s.nop b/zirgen/circuit/keccak/test2s.nop deleted file mode 100644 index f033fee0..00000000 --- a/zirgen/circuit/keccak/test2s.nop +++ /dev/null @@ -1,11 +0,0 @@ -// RUN: zirgen -I %S --test %s --test-cycles 23000 --input-data-hex 0600000000000000436F6D6D616E64657220526F64657269636B20426C61696E65206C6F6F6B6564206672616E746963616C6C792061726F756E6420746865206272696467652E20776865726520686973206F66666963657273207765726520646972656374696E6720726570616972732077697468206C6F7720616E6420757267656E7420766F696365732C2073757267656F6E7320617373697374696E67206174206120646966666963756C74206F7065726174696F6E2E20546865206772617920737465656C20636F6D706172746D656E7420776173206120636F6E667573696F6E206F6620616374697669746965732C2065616368206F726465726C7920627920697473656C662062757420746865206F766572616C6C20696D7072657373696F6E20776173206F66206368616F732E2053637265656E732061626F7665206F6E652068656C6D736D616E27732073746174696F6E2073686F7765642074686520706C616E65742062656C6F7720616E6420746865206F746865722C20736869707320696E206F72626974206E656172204D61634172746875722C20627574206576657279776865726520656C7365207468652070616E656C20636F7665727320686164206265656E2072656D6F7665642066726F6D20636F6E736F6C65732C207465737420696E737472756D656E7473207765726520636C697070656420696E746F20746865697220696E73696465732C20616E6420746563686E696369616E732073746F6F64206279207769746820636F6C6F722D636F64656420656C656374726F6E696320617373656D626C69657320746F207265706C6163652065766572797468696E672074686174207365656D656420646F75627466756C2E205468756D707320616E64207768696E657320736F756E646564207468726F75676820746865207368697020383920736F6D657768657265206166742074686520656E67696E656572696E67206372657720776F726B6564206F6E207468652068756C6C2E0600000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000805db9add409333e7f0834569e8e0f6825d684a88363d398b1d0ead06e01d03c1e0200000000000000546865736520776F7264732077657265207574746572656420696E204A756C79203138303520627920416E6E61205061766C6F766E6120536368657265722C20612064697374696E67756973686564206C616479206F662074686520636F7572742C20616E6420636F6E666964656E7469616C206D6169642D6F662D686F6E6F757220746F2074686520456D7072657373204D617279612046796F646F726F766E612E2049742077617320686572206772656574696E6720746F205072696E63652056617373696C792C2061206D616E206869676820696E2072616E6B20616E64206F66666963652C2077686F207761732074686520666972737420746F20617272697665206174060000000000008076d8ddb3fc6c9825ed4a81157c3486e4f35df5cdcf93df3b5c80f1d93ec144fb0000000000000000 2>&1 | FileCheck %s - -import keccak; - -test TestKeccak02s { // test_cycles >= 22776 -// CHECK-LABEL: Running TestKeccak02s -// CHECK: sha256output: 0x7719,0xac59 0x8026,0x14d2 0x4b9,0xdd6e 0x4baa,0xb1d1 0x4d35,0xd6a6 0x7bb9,0xea73 0x9d53,0x801b 0xbdb,0x768f -// CHECK: final accum: [0, 0, 0, 0] - Top () -} - diff --git a/zirgen/circuit/keccak/test_keccak_01.txt b/zirgen/circuit/keccak/test_keccak_01.txt deleted file mode 100644 index 47af7173..00000000 --- a/zirgen/circuit/keccak/test_keccak_01.txt +++ /dev/null @@ -1,3 +0,0 @@ -010000000000000054686520717569636B2062726F776E20666F78206A756D7073206F76657220746865206C617A7920646F672E0100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000080578951e24efd62a3d63a86f7cd19aaa53c898fe287d2552133220370240b572d0000000000000000 - -The quick brown fox jumps over the lazy dog. diff --git a/zirgen/circuit/keccak/test_keccak_02.txt b/zirgen/circuit/keccak/test_keccak_02.txt deleted file mode 100644 index 8fdd2dba..00000000 --- a/zirgen/circuit/keccak/test_keccak_02.txt +++ /dev/null @@ -1,5 +0,0 @@ -0600000000000000436F6D6D616E64657220526F64657269636B20426C61696E65206C6F6F6B6564206672616E746963616C6C792061726F756E6420746865206272696467652E20776865726520686973206F66666963657273207765726520646972656374696E6720726570616972732077697468206C6F7720616E6420757267656E7420766F696365732C2073757267656F6E7320617373697374696E67206174206120646966666963756C74206F7065726174696F6E2E20546865206772617920737465656C20636F6D706172746D656E7420776173206120636F6E667573696F6E206F6620616374697669746965732C2065616368206F726465726C7920627920697473656C662062757420746865206F766572616C6C20696D7072657373696F6E20776173206F66206368616F732E2053637265656E732061626F7665206F6E652068656C6D736D616E27732073746174696F6E2073686F7765642074686520706C616E65742062656C6F7720616E6420746865206F746865722C20736869707320696E206F72626974206E656172204D61634172746875722C20627574206576657279776865726520656C7365207468652070616E656C20636F7665727320686164206265656E2072656D6F7665642066726F6D20636F6E736F6C65732C207465737420696E737472756D656E7473207765726520636C697070656420696E746F20746865697220696E73696465732C20616E6420746563686E696369616E732073746F6F64206279207769746820636F6C6F722D636F64656420656C656374726F6E696320617373656D626C69657320746F207265706C6163652065766572797468696E672074686174207365656D656420646F75627466756C2E205468756D707320616E64207768696E657320736F756E646564207468726F75676820746865207368697020383920736F6D657768657265206166742074686520656E67696E656572696E67206372657720776F726B6564206F6E207468652068756C6C2E01000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008028c3f5c69c21be780e5508d355ebf7d5e060f203ca8717447b71cb44544df5c70200000000000000546865736520776F7264732077657265207574746572656420696E204A756C79203138303520627920416E6E61205061766C6F766E6120536368657265722C20612064697374696E67756973686564206C616479206F662074686520636F7572742C20616E6420636F6E666964656E7469616C206D6169642D6F662D686F6E6F757220746F2074686520456D7072657373204D617279612046796F646F726F766E612E2049742077617320686572206772656574696E6720746F205072696E63652056617373696C792C2061206D616E206869676820696E2072616E6B20616E64206F66666963652C2077686F207761732074686520666972737420746F2061727269766520617401000000000000804bdc1874a3125f1f911fe8c76ac8443a6ec623ef91bc58eabf54c5762097894d0000000000000000 - -Commander Roderick Blaine looked frantically around the bridge. where his officers were directing repairs with low and urgent voices, surgeons assisting at a difficult operation. The gray steel compartment was a confusion of activities, each orderly by itself but the overall impression was of chaos. Screens above one helmsman's station showed the planet below and the other, ships in orbit near MacArthur, but everywhere else the panel covers had been removed from consoles, test instruments were clipped into their insides, and technicians stood by with color-coded electronic assemblies to replace everything that seemed doubtful. Thumps and whines sounded through the ship 89 somewhere aft the engineering crew worked on the hull. - -These words were uttered in July 1805 by Anna Pavlovna Scherer, a distinguished lady of the court, and confidential maid-of-honour to the Empress Marya Fyodorovna. It was her greeting to Prince Vassily, a man high in rank and office, who was the first to arrive at diff --git a/zirgen/circuit/keccak2/top.zir b/zirgen/circuit/keccak/top.zir similarity index 100% rename from zirgen/circuit/keccak2/top.zir rename to zirgen/circuit/keccak/top.zir diff --git a/zirgen/circuit/keccak2/xor5.zir b/zirgen/circuit/keccak/xor5.zir similarity index 100% rename from zirgen/circuit/keccak2/xor5.zir rename to zirgen/circuit/keccak/xor5.zir diff --git a/zirgen/circuit/keccak2/BUILD.bazel b/zirgen/circuit/keccak2/BUILD.bazel deleted file mode 100644 index 063b43bb..00000000 --- a/zirgen/circuit/keccak2/BUILD.bazel +++ /dev/null @@ -1,95 +0,0 @@ -load("@rules_pkg//pkg:zip.bzl", "pkg_zip") -load("//bazel/rules/lit:defs.bzl", "glob_lit_tests") -load("//bazel/rules/zirgen:dsl-defs.bzl", "zirgen_build") -load("//bazel/rules/zirgen:edsl-defs.bzl", "ZIRGEN_OUTS", "build_circuit") - -package(default_visibility = ["//visibility:public"]) - -filegroup( - name = "imports", - srcs = glob(["*.zir"]), -) - -glob_lit_tests( - data = [":imports"], - size_override = { - "top.zir": "medium", - "sha2.zir": "medium", - }, - test_file_exts = ["zir"], -) - -zirgen_build( - name = "cppinc", - out = "keccak.cpp.inc", - data = [":imports"], - opts = [ - "--emit=cpp", - "--validity=false", - ], - zir_file = ":top.zir", -) - -SPLIT_VALIDITY = 5 - -SPLIT_STEP = 16 - -OUTS = ZIRGEN_OUTS + [ - fn - for i in range(SPLIT_VALIDITY) - for fn in [ - "rust_poly_fp_" + str(i) + ".cpp", - "eval_check_" + str(i) + ".cu", - ] -] + [ - fn - for i in range(SPLIT_STEP) - for fn in [ - "steps_" + str(i) + ".cpp", - "steps_" + str(i) + ".cu", - ] -] + [ - "eval_check.cuh", - "steps.h", - "steps.cuh", - "layout.h.inc", - "layout.cuh.inc", -] - -build_circuit( - name = "codegen", - outs = OUTS, - bin = "//zirgen/Main:gen_zirgen", - data = [":imports"], - extra_args = [ - "zirgen/circuit/keccak2/top.zir", - "-I", - "zirgen/circuit/keccak2", - "--circuit-name=keccak", - "--validity-split-count=" + str(SPLIT_VALIDITY), - "--step-split-count=" + str(SPLIT_STEP), - "--parallel-witgen", - "--protocol-info=KECCAK:v1_______" - ], -) - -ZKRS = [("keccak_lift_" + str(po2)) for po2 in range(14, 19)] - -build_circuit( - name = "predicates", - srcs = ["predicates.cpp"], - outs = [fn for zkr in ZKRS for fn in [ - zkr + ".zkr", - ]], - data = ["@zirgen//zirgen/circuit/keccak2:validity.ir"], - extra_args = ["--keccak-ir=$(location :validity.ir)"], - deps = ["//zirgen/circuit/predicates:lib"], -) - -filegroup( - name = "bootstrap", - srcs = [ - ":codegen", - ":predicates", - ], -) diff --git a/zirgen/circuit/keccak2/bits.zir b/zirgen/circuit/keccak2/bits.zir deleted file mode 100644 index 200d1cb2..00000000 --- a/zirgen/circuit/keccak2/bits.zir +++ /dev/null @@ -1,70 +0,0 @@ -// This file contains utilities that work with bits and twits. -// RUN: zirgen --test %s - -// Assert that a given value is a bit -#[picus_inline] -function AssertBit(val: Val) { - val * (1 - val) = 0; -} - -// Set a register nodeterministically, and then verify it is a bit -#[picus_inline] -component NondetBitReg(val: Val) { - reg := NondetReg(val); - AssertBit(reg); - reg -} - -component BitReg(val: Val) { - reg := NondetBitReg(val); - val = reg; - reg -} - -// Simple bit ops -component BitAnd(a: Val, b: Val) { - a * b -} - -component BitOr(a: Val, b: Val) { - a + b - a * b -} - -component BitXor(a: Val, b: Val) { - a + b - 2 * a * b -} - -// Tests.... - -// Check that valid bits are valid -test BitInRange { - AssertBit(0); - AssertBit(1); -} - -// Check that 2 is not a bit -test_fails BitOutOfRange { - AssertBit(2); -} - -test TestAnd { - BitAnd(0, 0) = 0; - BitAnd(0, 1) = 0; - BitAnd(1, 0) = 0; - BitAnd(1, 1) = 1; -} - -test TestOr { - BitOr(0, 0) = 0; - BitOr(0, 1) = 1; - BitOr(1, 0) = 1; - BitOr(1, 1) = 1; -} - -test TestXor { - BitXor(0, 0) = 0; - BitXor(0, 1) = 1; - BitXor(1, 0) = 1; - BitXor(1, 1) = 0; -} - diff --git a/zirgen/circuit/keccak2/keccak.zir b/zirgen/circuit/keccak2/keccak.zir deleted file mode 100644 index 0ea88141..00000000 --- a/zirgen/circuit/keccak2/keccak.zir +++ /dev/null @@ -1,206 +0,0 @@ -// RUN: zirgen -I %S --test %s - -import bits; -import one_hot; -import xor5; -import arr; -import pack; - -// Computes the xor5 part of Theta, results are 'bits' and can be aliased -component ThetaP1(a: Array, 5>, 5>) { - for j : 0..5 { - for k : 0..64 { - Xor5(for i : 0..5 { a[i][j][k] } ) - } - } -} - -// Computes part 2 of theta, results are not by register -component ThetaP2(a: Array, 5>, 5>, c: Array, 5>) { - d := for j : 0..5 { - for k : 0..64 { - jm1 := if (Isz(j)) { 4 } else { j - 1 }; - jp1 := if (Isz(j-4)) { 0 } else { j + 1 }; - kp1 := if (Isz(k)) { 63 } else { k - 1 }; - BitXor(c[jm1][k], c[jp1][kp1]) - } - }; - for i : 0..5 { - for j : 0..5 { - for k : 0..64 { - BitXor(a[i][j][k], d[j][k]) - } - } - } -} - -// One-shot version of theta -component Theta(a: Array, 5>, 5>) { - ThetaP2(a, ThetaP1(a)) -} - -component RhoMatrix() { - [[0,36,3,41,18],[1,44,10,45,2],[62,6,43,15,61],[28,55,25,21,56],[27,20,39,8,14]] -} - -component Rho(a: Array, 5>, 5>) { - for i : 0..5 { - for j : 0..5 { - RotateLeft<64>(a[i][j], RhoMatrix()[j][i]) - } - } -} - -component PiMatrix() { - [[0,3,1,4,2],[1,4,2,0,3],[2,0,3,1,4],[3,1,4,2,0],[4,2,0,3,1]] -} - -component Pi(a: Array, 5>, 5>) { - for i : 0..5 { - for j : 0..5 { - newi := PiMatrix()[j][i]; - a[j][newi] - } - } -} - -component Chi(a: Array, 5>, 5>) { - for i : 0..5 { - for j : 0..5 { - for k : 0..64 { - jp1 := if (Isz(4-j)) { 0 } else { j + 1 }; - jp2 := if (Isz(4-jp1)) { 0 } else { jp1 + 1 }; - BitXor(a[i][j][k], (1 - a[i][jp1][k]) * a[i][jp2][k]) - } - } - } -} - -component IotaTable() { - [ - [0x0001, 0x0000, 0x0000, 0x0000], - [0x8082, 0x0000, 0x0000, 0x0000], - [0x808a, 0x0000, 0x0000, 0x8000], - [0x8000, 0x8000, 0x0000, 0x8000], - [0x808b, 0x0000, 0x0000, 0x0000], - [0x0001, 0x8000, 0x0000, 0x0000], - [0x8081, 0x8000, 0x0000, 0x8000], - [0x8009, 0x0000, 0x0000, 0x8000], - [0x008a, 0x0000, 0x0000, 0x0000], - [0x0088, 0x0000, 0x0000, 0x0000], - [0x8009, 0x8000, 0x0000, 0x0000], - [0x000a, 0x8000, 0x0000, 0x0000], - [0x808b, 0x8000, 0x0000, 0x0000], - [0x008b, 0x0000, 0x0000, 0x8000], - [0x8089, 0x0000, 0x0000, 0x8000], - [0x8003, 0x0000, 0x0000, 0x8000], - [0x8002, 0x0000, 0x0000, 0x8000], - [0x0080, 0x0000, 0x0000, 0x8000], - [0x800a, 0x0000, 0x0000, 0x0000], - [0x000a, 0x8000, 0x0000, 0x8000], - [0x8081, 0x8000, 0x0000, 0x8000], - [0x8080, 0x0000, 0x0000, 0x8000], - [0x0001, 0x8000, 0x0000, 0x0000], - [0x8008, 0x8000, 0x0000, 0x8000] - ] -} - -component ExpandedIotaTable() { - for i : 0..24 { UnpackNondet<64, 16>(IotaTable()[i]) } -} - -component RoundToArray(idx: Val) { - table := ExpandedIotaTable(); - split := OneHot<24>(idx); - for k : 0..64 { - reduce for i : 0..24 { split[i] * table[i][k] } init 0 with Add - } -} - -component Iota(a: Array, 5>, 5>, round: Val) { - iotaArray := RoundToArray(round); - for i : 0..5 { - for j : 0..5 { - if (Isz(i) * Isz(j)) { - for k: 0..64 { BitXor(iotaArray[k], a[i][j][k]) } - } else { - a[i][j] - } - } - } -} - -/* Testing only components */ - -component RegisterizeKeccak(a: Array, 5>, 5>) { - for i : 0..5 { - for j : 0..5 { - for k : 0..64 { - Reg(a[i][j][k]) - } - } - } -} - -component TestDoRound(a: Array, 5>, 5>, round: Val) { - a := RegisterizeKeccak(Pi(Rho(Theta(a)))); - RegisterizeKeccak(Iota(Chi(a), round)) -} - -component PrintState(in: Array, 5>, 5>) { - for i : 0..5 { - for j : 0..5 { - p := Pack<64, 16>(in[i][j]); - Log("%x, %x, %x, %x", p[0], p[1], p[2], p[3]) - } - } -} - -/* -test TestTheta { - input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); - PrintState(input); - Log("-----"); - output := Theta(input); - PrintState(output); -} - -test TestRho { - input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); - PrintState(input); - Log("-----"); - output := Rho(input); - PrintState(output); -} - -test TestPi { - input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); - PrintState(input); - Log("-----"); - output := Pi(input); - PrintState(output); -} - -test TestChi { - input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); - PrintState(input); - Log("-----"); - output := Chi(input); - PrintState(output); -} - -test TestIota { - input := ExpandState(for i : 0..5 { for j : 0..5 { [ j, 0, i, 0] } }); - PrintState(input); - Log("-----"); - output := Iota(input, 3); - PrintState(output); -} - -test Permute { - input := for i : 0..5 { for j : 0..5 { for k : 0..64 { 0 } } }; - output := reduce 0..4 init input with TestDoRound; - PrintState(output); -} -*/ - diff --git a/zirgen/circuit/keccak2/one_hot.zir b/zirgen/circuit/keccak2/one_hot.zir deleted file mode 100644 index 438dbc04..00000000 --- a/zirgen/circuit/keccak2/one_hot.zir +++ /dev/null @@ -1,33 +0,0 @@ -// RUN: zirgen -I %S --test %s - -import bits; - -component OneHot(v: Val) { - // Make N bit registers, with bit v set and all others 0 - public bits := for i : 0..N { NondetBitReg(Isz(i - v)) }; - // Verify exactly one bit is set - reduce bits init 0 with Add = 1; - // Verify the right bit is set - reduce for i : 0..N { bits[i] * i } init 0 with Add = v; - bits -} - -component Switch() { - for i : 0..N { Isz(i - idx) } -} - -test Simple { - x := OneHot<8>(3); - x.bits[0] = 0; - x.bits[1] = 0; - x.bits[2] = 0; - x.bits[3] = 1; - x.bits[4] = 0; - x.bits[5] = 0; - x.bits[6] = 0; - x.bits[7] = 0; -} - -test_fails OutOfRange { - x := OneHot<8>(8); -}