ZIR-164: Add circuit/keccak with basic tests (#29)

* 1st step (aka theta) of keccak, using 1+35=36 cycles

* subcomponents with types to avoid repetition (multiple args for backs)

* degree=5 instead of 9, less than 44 extra columns, 25 cycles instead of 35

* RotateLeft64bit with babybear-split offsets, and test vectors

* rho+pi steps, test-cycles=81

* chi step, test-cycles=136

* full keccak (without sponge), test-cycles=3265=1+24*136

* init sponge, example test-cycles=19707=6*(3265+18)+2*4+1

* optimize: deg3 constraints, example cycles 6*((136-25)*24+19)+2*4+1==16107

* minor

* nondet input via extern (with single num_of_blocks word)

* minor: nondet input is always 64bit words

* use_once_mem_arg: keccak.zir writes, sha256_for_keccak.zir reads

* rename inner/outer to minor/major

* bugfix: degree=6 and reg linear sum mem arg

* Top() also for emit=stats

* bugfix: unneeded register array

* mv to zirgen/circuit/keccak

* restored driver.cpp

* test vectors via configureInput/readInput

* max babybear idx (unneeded) constraints

* Add circuit/keccak with basic tests

Still todo:

* Make zirgen faster
* Document test cases better

---------

Co-authored-by: iddo <[email protected]>

accel_inp

@@ -0,0 +1 @@
+00050000000000006854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E676854206575716369206B7262776F206E6F662078756A706D2073766F7265742065686C207A6120796F642E672E2E00010000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008000bd773c88b4ce72b65d44b79e9008be08cbbe0bd362ace9d6fee547c1a0e91e890001000000000000654b63636b61322d3635542073652074614868730001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000008000D7A8071BAFF4A42621FF7F02FF622660F97FC955F063C442A56DE32EAFCF3C3D0000000000000000

bazel/rules/lit/defs.bzl

@@ -26,7 +26,7 @@ _ALWAYS_EXCLUDE = [
     "**/* */**",
 ]
 
-def _run_lit_test(name, test_name, data, size, tags, driver, features, exec_properties):
+def _run_lit_test(name, test_name, data, size, tags, driver, features, exec_properties, **kwargs):
     """Runs lit on all tests it can find in `data`
 
     Note that, due to Bazel's hermetic builds, lit only sees the tests that
@@ -65,6 +65,7 @@ def _run_lit_test(name, test_name, data, size, tags, driver, features, exec_prop
         size = size,
         main = "lit.py",
         exec_properties = exec_properties,
+        **kwargs
     )
 
 def glob_lit_tests(
@@ -78,7 +79,8 @@ def glob_lit_tests(
         tags_override = {},
         driver = _default_driver,
         features = [],
-        exec_properties = {}):
+        exec_properties = {},
+        **kwargs):
     """Creates all plausible Lit tests (and their inputs) under this directory.
 
     Args:
@@ -118,4 +120,5 @@ def glob_lit_tests(
             driver = driver,
             features = features,
             exec_properties = exec_properties,
+            **kwargs
         )

zirgen/circuit/keccak/BUILD.bazel

@@ -0,0 +1,25 @@
+load("@rules_pkg//pkg:zip.bzl", "pkg_zip")
+load("//bazel/rules/lit:defs.bzl", "glob_lit_tests")
+load("//bazel/rules/zirgen:edsl-defs.bzl", "build_circuit")
+
+package(
+    default_visibility = ["//visibility:public"],
+)
+
+glob_lit_tests(
+    # TODO: shorten timeout once zirgen is faster
+    timeout = "long",
+    data = [
+        "bits.zir",
+        "keccak.zir",
+        "one_hot.zir",
+        "sha256_for_keccak.zir",
+    ],
+    exclude = [
+        "bits.zir",
+        "keccak.zir",
+        "one_hot.zir",
+        "sha256_for_keccak.zir",
+    ],
+    test_file_exts = ["zir"],
+)

zirgen/circuit/keccak/bits.zir

@@ -0,0 +1,84 @@
+// This file contains utilities that work with bits and twits.
+// RUN: zirgen --test %s
+
+// Assert that a given value is a bit
+function AssertBit(val: Val) {
+  val * (1 - val) = 0;
+}
+
+// Set a register nodeterministically, and then verify it is a bit
+component NondetBitReg(val: Val) {
+  reg := NondetReg(val);
+  AssertBit(reg);
+  reg
+}
+
+component BitReg(val: Val) {
+  reg := NondetBitReg(val);
+  val = reg;
+  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;
+}
+
+component BitAnd(a: Val, b: Val) {
+  Reg(a * b)
+}
+
+component BitOr(a: Val, b: Val) {
+  Reg(1 - (1 - a) * (1 - b))
+}
+
+// Set a register nodeterministically, and then verify it is a twit
+component NondetTwitReg(val: Val) {
+  reg := NondetReg(val);
+  AssertTwit(reg);
+  reg
+}
+
+// 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
+}
+
+component TwitReg(val: Val) {
+  reg := NondetTwitReg(val);
+  val = reg;
+  reg
+}
+
+component FakeTwitReg(val: Val) {
+  reg := NondetFakeTwitReg(val);
+  val = reg;
+  reg
+}
+
+// Check that all valid twit values are OK
+test TwitInRange{
+  AssertTwit(0);
+  AssertTwit(1);
+  AssertTwit(2);
+  AssertTwit(3);
+}
+
+// Check that 4 is not a twit
+test_fails TwitOutOfRange {
+  AssertTwit(4);
+}
+