Implement ROM-checking based on Haboeck's lookup argument

Cargo.toml

@@ -64,7 +64,7 @@ approx = "0.5.0"
 default = []
 # frontends
 c = ["lang-c"]
-zok = ["zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]
+zok = ["smt", "zokrates_parser", "zokrates_pest_ast", "typed-arena", "petgraph"]
 datalog = ["pest", "pest-ast", "pest_derive", "from-pest", "lazy_static"]
 # backends
 smt = ["rsmt2", "ieee754"]

circ_opt/README.md

@@ -129,6 +129,16 @@ Options:
           - waksman: Use the AS-Waksman network
           - msh:     Use the (keyed) multi-set hash
 
+      --ram-rom <ROM>
+          ROM approach
+
+          [env: RAM_ROM=]
+          [default: haboeck]
+
+          Possible values:
+          - haboeck: Use Haboeck's argument
+          - permute: Use permute-and-check
+
       --fmt-use-default-field <USE_DEFAULT_FIELD>
           Which field to use
 
@@ -210,6 +220,8 @@ Options:
           How to argue that indices are only repeated in blocks [env: RAM_INDEX=] [default: uniqueness] [possible values: sort, uniqueness]
       --ram-permutation <PERMUTATION>
           How to argue that indices are only repeated in blocks [env: RAM_PERMUTATION=] [default: msh] [possible values: waksman, msh]
+      --ram-rom <ROM>
+          ROM approach [env: RAM_ROM=] [default: haboeck] [possible values: haboeck, permute]
       --fmt-use-default-field <USE_DEFAULT_FIELD>
           Which field to use [env: FMT_USE_DEFAULT_FIELD=] [default: true] [possible values: true, false]
       --fmt-hide-field <HIDE_FIELD>
@@ -253,6 +265,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -298,6 +311,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -341,6 +355,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -384,6 +399,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -427,6 +443,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -470,6 +487,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -513,6 +531,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -556,6 +575,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -602,6 +622,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -646,6 +667,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -692,6 +714,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -736,6 +759,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -782,6 +806,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,
@@ -826,6 +851,7 @@ BinaryOpt {
             range: Sort,
             index: Uniqueness,
             permutation: Msh,
+            rom: Haboeck,
         },
         fmt: FmtOpt {
             use_default_field: true,

circ_opt/src/lib.rs

@@ -239,6 +239,14 @@ pub struct RamOpt {
         default_value = "msh"
     )]
     pub permutation: PermutationStrategy,
+    /// ROM approach
+    #[arg(
+        long = "ram-rom",
+        env = "RAM_ROM",
+        value_enum,
+        default_value = "haboeck"
+    )]
+    pub rom: RomStrategy,
 }
 
 #[derive(ValueEnum, Debug, PartialEq, Eq, Clone, Copy)]
@@ -286,6 +294,21 @@ impl Default for PermutationStrategy {
     }
 }
 
+#[derive(ValueEnum, Debug, PartialEq, Eq, Clone, Copy)]
+/// How to argue that accesses have been permuted
+pub enum RomStrategy {
+    /// Use Haboeck's argument
+    Haboeck,
+    /// Use permute-and-check
+    Permute,
+}
+
+impl Default for RomStrategy {
+    fn default() -> Self {
+        RomStrategy::Haboeck
+    }
+}
+
 /// Options for the prime field used
 #[derive(Args, Debug, Clone, PartialEq, Eq)]
 pub struct FmtOpt {

examples/ZoKrates/pf/mem/rom.zok

@@ -0,0 +1,22 @@
+const u32 VAL_LEN = 3
+const u32 RAM_LEN = 20
+const u32 ACCESSES = 400
+
+struct Val {
+    field x
+    field y
+}
+
+const transcript Val[RAM_LEN] array = [Val{x: 0, y: 0}, ...[Val{x: 10, y: 10}; RAM_LEN-1]]
+
+def main(private field[ACCESSES] y) -> field:
+    field result = 0
+
+    for u32 i in 0..ACCESSES do
+        Val v = array[y[i]]
+        result = result + v.x + v.y
+    endfor
+    return result
+
+
+

scripts/ram_test.zsh

@@ -50,6 +50,15 @@ function transcript_type_test {
     fi
 }
 
+function cs_count_test {
+    ex_name=$1
+    cs_upper_bound=$2
+    rm -rf P V pi
+    output=$($BIN $ex_name r1cs --action count |& cat)
+    n_constraints=$(echo "$output" | grep 'Final R1cs size:' | grep -Eo '\b[0-9]+\b')
+    [[ $n_constraints -lt $cs_upper_bound ]] || (echo "Got $n_constraints, expected < $cs_upper_bound" && exit 1)
+}
+
 transcript_count_test ./examples/ZoKrates/pf/mem/volatile.zok 1
 transcript_count_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok 1
 transcript_count_test ./examples/ZoKrates/pf/mem/volatile_struct.zok 1
@@ -59,6 +68,9 @@ transcript_count_test ./examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok 1
 transcript_type_test ./examples/ZoKrates/pf/mem/volatile_struct.zok "RAM"
 transcript_type_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok "covering ROM"
 
+# A=400; N=20; L=2; expected cost ~= N + A(L+1) = 1220
+cs_count_test ./examples/ZoKrates/pf/mem/rom.zok 1230
+
 ram_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok groth16 "--ram-permutation waksman --ram-index sort --ram-range bit-split"
 ram_test ./examples/ZoKrates/pf/mem/volatile.zok groth16 "--ram-permutation waksman --ram-index sort --ram-range bit-split"
 # waksman is broken for non-scalar array values

src/ir/opt/mem/ram.rs

@@ -71,12 +71,13 @@ pub struct AccessCfg {
     split_times: bool,
     waksman: bool,
     covering_rom: bool,
+    haboeck: bool,
 }
 
 impl AccessCfg {
     /// Create a new configuration
     pub fn new(field: FieldT, opt: RamOpt, create: bool) -> Self {
-        use circ_opt::{IndexStrategy, PermutationStrategy, RangeStrategy};
+        use circ_opt::{IndexStrategy, PermutationStrategy, RangeStrategy, RomStrategy};
         Self {
             false_: bool_lit(false),
             true_: bool_lit(true),
@@ -88,6 +89,7 @@ impl AccessCfg {
             split_times: opt.range == RangeStrategy::BitSplit,
             waksman: opt.permutation == PermutationStrategy::Waksman,
             covering_rom: false,
+            haboeck: opt.rom == RomStrategy::Haboeck,
         }
     }
     /// Create a default configuration, with this field.
@@ -103,6 +105,7 @@ impl AccessCfg {
             split_times: false,
             waksman: false,
             covering_rom: false,
+            haboeck: true,
         }
     }
     /// Create a new default configuration
@@ -278,6 +281,7 @@ impl Access {
         }
     }
 
+    /// Serialize a value as field elements.
     fn val_to_field_elements(val: &Term, c: &AccessCfg, out: &mut Vec<Term>) {
         match check(val) {
             Sort::Field(_) | Sort::Bool | Sort::BitVector(_) => out.push(scalar_to_field(val, c)),