RAM for non-scalar values (#174)

It is very naive. It assumes that any top-level array should be represented as a RAM, and that all internal structure should be unfolded.

examples/ZoKrates/pf/mem/arr_arr_of_str_of_arr.zok

@@ -0,0 +1,18 @@
+const u32 LEN = 2
+const u32 LEN2 = 100
+const u32 ACCESSES = 37
+const u32 P_ = 8
+
+struct Pt {
+    field[P_] x
+    field[P_] x2
+}
+const Pt [LEN][LEN2] array = [[Pt {x: [0; P_], x2: [0; P_]}; LEN2], ...[[Pt {x: [100; P_], x2: [100; P_]}; LEN2] ; LEN-1]] // 638887 when LEN = 8190 // 63949 when LEN = 819
+
+def main(private field[ACCESSES][2] idx) -> field:
+    field sum = 0
+    for u32 i in 0..ACCESSES do
+        field[2] access = idx[i]
+        sum = sum + array[access[1]][access[0]].x[0]
+    endfor
+    return sum

examples/ZoKrates/pf/mem/arr_of_str.zok

@@ -0,0 +1,18 @@
+const u32 LEN = 6
+const u32 ACCESSES = 3
+
+struct Pt {
+    field x
+    field y
+    field z
+}
+const Pt [LEN] array = [Pt {x: 4, y: 5, z: 6}, ...[Pt {x: 0, y: 1, z: 2}; LEN - 1]]
+
+def main(private field[ACCESSES] idx) -> field:
+    field prod = 1
+    for u32 i in 0..ACCESSES do
+        field access = idx[i]
+        Pt pt = array[access]
+        prod = prod * pt.x * pt.y * pt.z
+    endfor
+    return prod

examples/ZoKrates/pf/mem/arr_of_str.zok.pin

@@ -0,0 +1,7 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (idx.0 #f0)
+    (idx.1 #f1)
+    (idx.2 #f2)
+) false ; ignored
+))

examples/ZoKrates/pf/mem/arr_of_str.zok.vin

@@ -0,0 +1,5 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (return #f0)
+) false ; ignored
+))

examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok

@@ -0,0 +1,21 @@
+const u32 LEN = 4
+const u32 INNER_LEN = 2
+const u32 ACCESSES = 2
+
+struct Pt {
+    field[INNER_LEN] x
+    field[INNER_LEN] y
+}
+const Pt [LEN] array = [Pt {x: [0; INNER_LEN], y: [5; INNER_LEN]}, ...[Pt {x: [1; INNER_LEN], y: [2; INNER_LEN]}; LEN - 1]]
+
+def main(private field[ACCESSES] idx) -> field:
+    field prod = 1
+    for u32 i in 0..ACCESSES do
+        field access = idx[i]
+        Pt pt = array[access]
+        for u32 j in 0..INNER_LEN do
+            prod = prod * pt.x[j] * pt.y[j]
+        endfor
+    endfor
+    return prod
+

examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok.pin

@@ -0,0 +1,7 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (idx.0 #f0)
+    (idx.1 #f1)
+) false ; ignored
+))
+

examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok.vin

@@ -0,0 +1,6 @@
+(set_default_modulus 52435875175126190479447740508185965837690552500527637822603658699938581184513
+(let (
+    (return #f0)
+) false ; ignored
+))
+

examples/ZoKrates/pf/mem/large_arr_of_str_of_arr.zok

@@ -0,0 +1,22 @@
+const u32 LEN = 256
+const u32 INNER_LEN = 8
+const u32 ACCESSES = 10
+
+struct Pt {
+    field[INNER_LEN] x
+    field[INNER_LEN] y
+}
+const Pt [LEN] array = [Pt {x: [0; INNER_LEN], y: [5; INNER_LEN]}, ...[Pt {x: [1; INNER_LEN], y: [2; INNER_LEN]}; LEN - 1]]
+
+def main(private field[ACCESSES] idx) -> field:
+    field prod = 1
+    for u32 i in 0..ACCESSES do
+        field access = idx[i]
+        Pt pt = array[access]
+        for u32 j in 0..INNER_LEN do
+            prod = prod * pt.x[j] * pt.y[j]
+        endfor
+    endfor
+    return prod
+
+

examples/ZoKrates/pf/mem/two_level_ptr.zok

@@ -1,17 +1,13 @@
 const u32 LEN = 4
 const u32 ACCESSES = 2
 
-struct Pt {
-    field x
-    field y
-}
-const Pt [LEN] array = [Pt {x: 0, y:0}, ...[Pt {x: 100, y: 0} ; LEN-1]]
+const field[LEN] array = [0, ...[100; LEN-1]]
 
 def main(private field[ACCESSES] y) -> field:
     field result = 0
 
     for u32 i in 0..ACCESSES do
-        assert(array[y[i]].x == 0)
+        assert(array[y[i]] == 0)
     endfor
     return result
 

examples/circ.rs

@@ -267,16 +267,20 @@ fn main() {
             opts.push(Opt::ConstantFold(Box::new([])));
             opts.push(Opt::ParseCondStores);
             // Tuples must be eliminated before oblivious array elim
-            opts.push(Opt::Tuple);
             opts.push(Opt::ConstantFold(Box::new([])));
-            opts.push(Opt::Tuple);
             opts.push(Opt::Obliv);
             // The obliv elim pass produces more tuples, that must be eliminated
-            opts.push(Opt::Tuple);
             if options.circ.ram.enabled {
+                // Waksman can only route scalars, so tuple first!
+                if options.circ.ram.permutation == circ_opt::PermutationStrategy::Waksman {
+                    opts.push(Opt::Tuple);
+                }
                 opts.push(Opt::PersistentRam);
                 opts.push(Opt::VolatileRam);
                 opts.push(Opt::SkolemizeChallenges);
+                opts.push(Opt::ScalarizeVars);
+                opts.push(Opt::ConstantFold(Box::new([])));
+                opts.push(Opt::Obliv);
             }
             opts.push(Opt::LinearScan);
             // The linear scan pass produces more tuples, that must be eliminated

scripts/compiler_asymptotics.zsh

@@ -0,0 +1,40 @@
+#!/usr/bin/env zsh
+set -ex
+
+function usage {
+    echo "Usage: $0 COMPILER_COMMAND TEMPLATE PATTERN REPLACEMENTS..."
+    exit 2
+}
+
+compiler_command=($(eval echo $1))
+template_file=$2
+pattern=$3
+replacements=(${@:4})
+
+[[ ! -z $compiler_command ]] || (echo "Empty compiler command" && usage)
+if [[ ! -a $template_file ]]
+then
+    for arg in $compiler_command
+    do
+        if [[ $arg =~ .*.zok ]]
+        then
+            echo "template $arg"
+            template_file=$arg
+        fi
+    done
+fi
+[[ -a $template_file ]] || (echo "No file at $template_file" && usage)
+[[ ! -z $pattern ]] || (echo "Empty pattern" && usage)
+[[ ! -z $replacements ]] || (echo "Empty replacements" && usage)
+
+echo $replacements
+
+for replacement in $replacements
+do
+    t=$(mktemp compiler_asymptotics_XXXXXXXX.zok)
+    cat $template_file | sed "s/$pattern/$replacement/g" > $t
+    instantiated_command=$(echo $compiler_command | sed "s/$template_file/$t/")
+    echo $instantiated_command
+    rm $t
+done
+

scripts/ram_test.zsh

@@ -25,7 +25,10 @@ function ram_test {
 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"
 ram_test ./examples/ZoKrates/pf/mem/volatile_struct.zok groth16 "--ram-permutation waksman --ram-index sort --ram-range bit-split"
+ram_test ./examples/ZoKrates/pf/mem/arr_of_str.zok groth16 "--ram-permutation waksman --ram-index sort --ram-range bit-split"
 ram_test ./examples/ZoKrates/pf/mem/two_level_ptr.zok mirage ""
 ram_test ./examples/ZoKrates/pf/mem/volatile.zok mirage ""
 ram_test ./examples/ZoKrates/pf/mem/volatile_struct.zok mirage ""
+ram_test ./examples/ZoKrates/pf/mem/arr_of_str.zok mirage ""
+ram_test ./examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok mirage ""
 

scripts/test_c_r1cs.zsh

@@ -0,0 +1,21 @@
+#!/usr/bin/env zsh
+
+set -ex
+
+# cargo build --release --features lp,r1cs,smt,zok --example circ
+
+MODE=debug # release or debug
+BIN=./target/$MODE/examples/circ
+ZK_BIN=./target/$MODE/examples/zk
+
+# Test prove workflow, given an example name
+function c_pf_test {
+    proof_impl=groth16
+    ex_name=$1
+    $BIN examples/C/r1cs/$ex_name.c r1cs --action setup --proof-impl $proof_impl
+    $ZK_BIN --inputs examples/C/r1cs/$ex_name.c.pin --action prove --proof-impl $proof_impl
+    $ZK_BIN --inputs examples/C/r1cs/$ex_name.c.vin --action verify --proof-impl $proof_impl
+    rm -rf P V pi
+}
+
+c_pf_test add

src/ir/opt/mem/lin.rs

@@ -17,6 +17,12 @@ fn arr_val_to_tup(v: &Value) -> Value {
             }
             vec
         }),
+        Value::Tuple(vs) => Value::Tuple(
+            vs.iter()
+                .map(arr_val_to_tup)
+                .collect::<Vec<_>>()
+                .into_boxed_slice(),
+        ),
         v => v.clone(),
     }
 }
@@ -29,7 +35,7 @@ impl RewritePass for Linearizer {
         rewritten_children: F,
     ) -> Option<Term> {
         match &orig.op() {
-            Op::Const(v @ Value::Array(..)) => Some(leaf_term(Op::Const(arr_val_to_tup(v)))),
+            Op::Const(v) => Some(leaf_term(Op::Const(arr_val_to_tup(v)))),
             Op::Var(name, Sort::Array(..)) => {
                 let precomp = extras::array_to_tuple(orig);
                 let new_name = format!("{name}.tup");

src/ir/opt/mem/obliv.rs

@@ -13,11 +13,14 @@
 //!
 //! So, essentially, what's going on is that T maps each term t to an (approximate) analysis of t
 //! that indicates which accesses can be perfectly resolved.
+//!
+//! We could make the analysis more precise (and/or efficient) with a better data structure for
+//! tracking information about value locations.
 
 use crate::ir::term::extras::as_uint_constant;
 use crate::ir::term::*;
 
-use log::{debug, trace};
+use log::trace;
 
 #[derive(Default)]
 struct OblivRewriter {
@@ -30,6 +33,7 @@ fn suitable_const(t: &Term) -> bool {
 }
 
 impl OblivRewriter {
+    /// Get, prefering tuple if possible.
     fn get_t(&self, t: &Term) -> &Term {
         self.tups.get(t).unwrap_or(self.terms.get(t).unwrap())
     }
@@ -57,7 +61,7 @@ impl OblivRewriter {
                 (
                     if let Some(aa) = self.tups.get(a) {
                         if suitable_const(i) {
-                            debug!("simplify store {}", i);
+                            trace!("simplify store {}", i);
                             Some(term![Op::Update(get_const(i)); aa.clone(), self.get_t(v).clone()])
                         } else {
                             None
@@ -73,7 +77,7 @@ impl OblivRewriter {
                 let i = &t.cs()[1];
                 if let Some(aa) = self.tups.get(a) {
                     if suitable_const(i) {
-                        debug!("simplify select {}", i);
+                        trace!("simplify select {}", i);
                         let tt = term![Op::Field(get_const(i)); aa.clone()];
                         (
                             Some(tt.clone()),
@@ -115,7 +119,37 @@ impl OblivRewriter {
                     },
                 )
             }
-            Op::Tuple => panic!("Tuple in obliv"),
+            Op::Tuple => (
+                if t.cs().iter().all(|c| self.tups.contains_key(c)) {
+                    Some(term(
+                        Op::Tuple,
+                        t.cs()
+                            .iter()
+                            .map(|c| self.tups.get(c).unwrap().clone())
+                            .collect(),
+                    ))
+                } else {
+                    None
+                },
+                None,
+            ),
+            Op::Field(i) => (
+                if t.cs().iter().all(|c| self.tups.contains_key(c)) {
+                    Some(term_c![Op::Field(*i); self.get_t(&t.cs()[0])])
+                } else {
+                    None
+                },
+                None,
+            ),
+            Op::Update(i) => (
+                if t.cs().iter().all(|c| self.tups.contains_key(c)) {
+                    Some(term_c![Op::Update(*i); self.get_t(&t.cs()[0]), self.get_t(&t.cs()[1])])
+                } else {
+                    None
+                },
+                None,
+            ),
+            //Op::Tuple => panic!("Tuple in obliv"),
             _ => (None, None),
         };
         if let Some(tup) = tup_opt {