Optimized transcript checking for covering ROMs (#178)

circ_hc/src/lib.rs

@@ -69,6 +69,10 @@ pub trait Node<Op>: Sized + Clone + PartialEq + Eq + PartialOrd + Ord + Hash {
     fn op(&self) -> &Op;
     /// Get the children of this node.
     fn cs(&self) -> &[Self];
+    /// Get the operator and children of this node.
+    fn parts(&self) -> (&Op, &[Self]) {
+        (self.op(), self.cs())
+    }
     /// Get a token that does not retain this node during GC.
     fn downgrade(&self) -> Self::Weak;
 }

examples/ZoKrates/pf/mem/arr_of_str_of_arr.zok

@@ -6,7 +6,7 @@ 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]]
+const transcript 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

scripts/ram_test.zsh

@@ -7,7 +7,8 @@ disable -r time
 # cargo build --release --features r1cs,smt,zok --example circ
 # cargo build --features "zok smt bellman" --example circ --example zk
 
-MODE=release # debug or release
+MODE=release
+# MODE=debug
 BIN=./target/$MODE/examples/circ
 ZK_BIN=./target/$MODE/examples/zk
 
@@ -22,6 +23,42 @@ function ram_test {
     rm -rf P V pi
 }
 
+# Test for how many transcripts are extracted
+function transcript_count_test {
+    ex_name=$1
+    ex_num=$2
+    rm -rf P V pi
+    found_num=$(RUST_LOG=circ::ir::opt::mem=debug $BIN $ex_name r1cs --action count |& grep -Eo 'Found [0-9]* transcripts' | grep -Eo '\b[0-9]+\b')
+    if [[ ! $ex_num == $found_num ]]
+    then
+        echo "expected $ex_num transcripts;\n  found $found_num transcripts"
+        exit 2
+    fi
+}
+
+# Test for whether a particular type of transcript is found
+function transcript_type_test {
+    ex_name=$1
+    ex_type=$2
+    rm -rf P V pi
+    output=$(RUST_LOG=circ::ir::opt::mem=debug $BIN $ex_name r1cs --action count |& cat)
+    echo $output
+    if (echo $output |& grep "Checking $ex_type") then;
+    else
+        echo "Did not find a transcript of type $ex_type"
+        exit 2
+    fi
+}
+
+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
+transcript_count_test ./examples/ZoKrates/pf/mem/arr_of_str.zok 1
+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"
+
 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/cstore.rs

@@ -4,32 +4,63 @@ use crate::ir::term::*;
 
 use super::visit::RewritePass;
 
-/// Parse `ite` as a conditional store (arr, idx, val, guard)
-fn parse_cond_store(ite: &Term) -> Option<ConditionalStore> {
-    if ite.op() == &Op::Ite && ite.cs()[1].op() == &Op::Store && ite.cs()[1].cs()[0] == ite.cs()[2]
-    {
-        // (ite COND (store ARR IDX VAL) ARR)
-        Some(ConditionalStore {
-            arr: ite.cs()[2].clone(),
-            idx: ite.cs()[1].cs()[1].clone(),
-            val: ite.cs()[1].cs()[2].clone(),
-            guard: ite.cs()[0].clone(),
-        })
-    } else if ite.op() == &Op::Ite
-        && ite.cs()[2].op() == &Op::Store
-        && ite.cs()[2].cs()[0] == ite.cs()[1]
-    {
-        // (ite COND ARR (store ARR IDX VAL))
-        Some(ConditionalStore {
-            arr: ite.cs()[1].clone(),
-            idx: ite.cs()[2].cs()[1].clone(),
-            val: ite.cs()[2].cs()[2].clone(),
-            guard: term![NOT; ite.cs()[0].clone()],
-        })
-        // could do things like: (store ARR IDX (ite COND VAL (select ARR IDX)))
-    } else {
-        None
+/// Parse `ite` or `store` as a conditional store (arr, idx, val, guard)
+fn parse_cond_store(term: &Term) -> Option<ConditionalStore> {
+    if let (&Op::Ite, [guard, true_, false_]) = term.parts() {
+        match true_.parts() {
+            (&Op::Store, [arr, idx, val]) if arr == false_ => {
+                // (ite COND (store ARR IDX VAL) ARR)
+                return Some(ConditionalStore {
+                    arr: arr.clone(),
+                    idx: idx.clone(),
+                    val: val.clone(),
+                    guard: guard.clone(),
+                });
+            }
+            _ => {}
+        }
+        match false_.parts() {
+            (&Op::Store, [arr, idx, val]) if arr == false_ => {
+                // (ite COND ARR (store ARR IDX VAL))
+                return Some(ConditionalStore {
+                    arr: arr.clone(),
+                    idx: idx.clone(),
+                    val: val.clone(),
+                    guard: term![NOT; guard.clone()],
+                });
+            }
+            _ => {}
+        }
     }
+    if let (&Op::Store, [arr, idx, val]) = term.parts() {
+        if let (&Op::Ite, [guard, true_, false_]) = val.parts() {
+            match false_.parts() {
+                (&Op::Select, [arr2, idx2]) if arr == arr2 && idx == idx2 => {
+                    // (store ARR IDX (ite COND VAL (select ARR IDX)))
+                    return Some(ConditionalStore {
+                        arr: arr.clone(),
+                        idx: idx.clone(),
+                        val: true_.clone(),
+                        guard: guard.clone(),
+                    });
+                }
+                _ => {}
+            }
+            match true_.parts() {
+                (&Op::Select, [arr2, idx2]) if arr == arr2 && idx == idx2 => {
+                    // (store ARR IDX (ite COND (select ARR IDX) VAL))
+                    return Some(ConditionalStore {
+                        arr: arr.clone(),
+                        idx: idx.clone(),
+                        val: false_.clone(),
+                        guard: term![NOT; guard.clone()],
+                    });
+                }
+                _ => {}
+            }
+        }
+    }
+    None
 }
 
 #[derive(Debug)]

src/ir/opt/mem/ram.rs

@@ -70,6 +70,7 @@ pub struct AccessCfg {
     sort_indices: bool,
     split_times: bool,
     waksman: bool,
+    covering_rom: bool,
 }
 
 impl AccessCfg {
@@ -86,6 +87,7 @@ impl AccessCfg {
             sort_indices: opt.index == IndexStrategy::Sort,
             split_times: opt.range == RangeStrategy::BitSplit,
             waksman: opt.permutation == PermutationStrategy::Waksman,
+            covering_rom: false,
         }
     }
     /// Create a default configuration, with this field.
@@ -100,6 +102,7 @@ impl AccessCfg {
             sort_indices: false,
             split_times: false,
             waksman: false,
+            covering_rom: false,
         }
     }
     /// Create a new default configuration
@@ -118,7 +121,13 @@ impl AccessCfg {
         }
     }
     fn len(&self, s: &Sort) -> usize {
-        (if self.create { 5 } else { 4 }) + Self::val_sort_len(s)
+        (if self.covering_rom {
+            1
+        } else if self.create {
+            5
+        } else {
+            4
+        }) + Self::val_sort_len(s)
     }
     fn bool2pf(&self, t: Term) -> Term {
         term![Op::Ite; t, self.one.clone(), self.zero.clone()]
@@ -147,7 +156,7 @@ fn scalar_to_field(scalar: &Term, c: &AccessCfg) -> Term {
 }
 
 /// A bit encoded in the field.
-#[derive(Debug)]
+#[derive(Debug, Clone)]
 struct FieldBit {
     /// The field value (0 or 1)
     f: Term,
@@ -219,27 +228,34 @@ impl Access {
 
     fn field_names(c: &AccessCfg, sort: &Sort, order: Order) -> Vec<String> {
         let mut out = Vec::new();
+        let metadata = !c.covering_rom;
         match order {
             Order::Hash => {
                 Self::sort_subnames(sort, "v", &mut out);
                 out.push("i".into());
-                out.push("t".into());
-                out.push("w".into());
-                out.push("a".into());
-                if c.create {
-                    out.push("c".into());
+                if metadata {
+                    out.push("t".into());
+                    out.push("w".into());
+                    out.push("a".into());
+                    if c.create {
+                        out.push("c".into());
+                    }
                 }
             }
             // dead code, but for clarity...
             Order::Sort => {
                 out.push("i".into());
-                out.push("t".into());
-                if c.create {
-                    out.push("c".into());
+                if metadata {
+                    out.push("t".into());
+                    if c.create {
+                        out.push("c".into());
+                    }
                 }
                 Self::sort_subnames(sort, "v", &mut out);
-                out.push("w".into());
-                out.push("a".into());
+                if metadata {
+                    out.push("w".into());
+                    out.push("a".into());
+                }
             }
         }
         out
@@ -304,33 +320,50 @@ impl Access {
         }
     }
 
+    /// Encode this access as a sequence of field terms.
+    ///
+    /// The sequence depends on `order` and on `c`.
+    ///
+    /// For example, if `c.covering_rom` is set, then the sequence will only contain an encoding of
+    /// the indices and values.
     fn to_field_elems(&self, c: &AccessCfg, order: Order) -> Vec<Term> {
         let mut out = Vec::new();
+        let metadata = !c.covering_rom;
         match order {
             Order::Hash => {
                 Self::val_to_field_elements(&self.val, c, &mut out);
                 out.push(self.idx.clone());
-                out.push(self.time.clone());
-                out.push(self.write.f.clone());
-                out.push(self.active.f.clone());
-                if c.create {
-                    out.push(self.create.f.clone())
+                if metadata {
+                    out.push(self.time.clone());
+                    out.push(self.write.f.clone());
+                    out.push(self.active.f.clone());
+                    if c.create {
+                        out.push(self.create.f.clone())
+                    }
                 }
             }
             Order::Sort => {
                 out.push(self.idx.clone());
-                out.push(self.time.clone());
-                if c.create {
-                    out.push(self.create.f.clone())
+                if metadata {
+                    out.push(self.time.clone());
+                    if c.create {
+                        out.push(self.create.f.clone())
+                    }
                 }
                 Self::val_to_field_elements(&self.val, c, &mut out);
-                out.push(self.write.f.clone());
-                out.push(self.active.f.clone());
+                if metadata {
+                    out.push(self.write.f.clone());
+                    out.push(self.active.f.clone());
+                }
             }
         }
         out
     }
 
+    /// Decode this access as a sequence of field terms, assuming that those field terms are the
+    /// encoding of an access.
+    ///
+    /// The expected order of field terms depends on `c` and `order`; see [Access::to_field_elems].
     fn from_field_elems_trusted(
         elems: Vec<Term>,
         val_sort: &Sort,
@@ -344,15 +377,25 @@ impl Access {
             debug_assert!(matches!(check(&t), Sort::Field(_)));
             t
         };
+        let metadata = !c.covering_rom;
+        let f = FieldBit::from_bool_lit(c, false);
         match order {
             Order::Hash => Self {
                 val: Self::val_from_field_elements_trusted(val_sort, &mut next),
                 val_hash: None,
                 idx: next(),
-                time: next(),
-                write: FieldBit::from_trusted_field(c, next()),
-                active: FieldBit::from_trusted_field(c, next()),
-                create: if c.create {
+                time: if metadata { next() } else { c.pf_lit(0) },
+                write: if metadata {
+                    FieldBit::from_trusted_field(c, next())
+                } else {
+                    f.clone()
+                },
+                active: if metadata {
+                    FieldBit::from_trusted_field(c, next())
+                } else {
+                    f.clone()
+                },
+                create: if c.create && metadata {
                     FieldBit::from_trusted_field(c, next())
                 } else {
                     FieldBit::from_bool_lit(c, false)
@@ -361,15 +404,23 @@ impl Access {
             Order::Sort => Self {
                 val_hash: None,
                 idx: next(),
-                time: next(),
-                create: if c.create {
+                time: if metadata { next() } else { c.pf_lit(0) },
+                create: if c.create && metadata {
                     FieldBit::from_trusted_field(c, next())
                 } else {
                     FieldBit::from_bool_lit(c, false)
                 },
                 val: Self::val_from_field_elements_trusted(val_sort, &mut next),
-                write: FieldBit::from_trusted_field(c, next()),
-                active: FieldBit::from_trusted_field(c, next()),
+                write: if metadata {
+                    FieldBit::from_trusted_field(c, next())
+                } else {
+                    f.clone()
+                },
+                active: if metadata {
+                    FieldBit::from_trusted_field(c, next())
+                } else {
+                    f.clone()
+                },
             },
         }
     }
@@ -574,4 +625,37 @@ impl Ram {
         self.accesses
             .push_front(Access::new_init(&self.cfg, idx, val));
     }
+    /// A ROM is a RAM in which there is only one write to any location, and that write happens
+    /// *before* any read.
+    ///
+    /// A covering ROM is a ROM with a write to every location.
+    ///
+    /// This function computes whether the first accesses are writes to distinct locations, and
+    /// whether the rest are reads.
+    fn is_covering_rom(&self) -> bool {
+        let mut written_addresses = TermSet::default();
+        for access in self.accesses.iter().take(self.size) {
+            if !access.idx.is_const()
+                || access.write.b != bool_lit(true)
+                || access.active.b != bool_lit(true)
+            {
+                trace!(
+                    "non-ROM because of an early non-const or non-read to {}",
+                    access.idx
+                );
+                return false;
+            }
+            if !written_addresses.insert(access.idx.clone()) {
+                trace!("non-ROM because of a 2nd access to {}", access.idx);
+                return false;
+            }
+        }
+        for access in self.accesses.iter().skip(self.size) {
+            if access.write.b != bool_lit(false) && access.active.b != bool_lit(false) {
+                trace!("non-ROM because of a late write to {}", access.idx);
+                return false;
+            }
+        }
+        true
+    }
 }

src/ir/opt/mem/ram/checker.rs

@@ -4,17 +4,24 @@ use super::*;
 use crate::front::PROVER_VIS;
 use crate::util::ns::Namespace;
 use circ_fields::FieldT;
-use log::trace;
+use log::{debug, trace};
 
 mod permutation;
 
 /// Check a RAM
 pub fn check_ram(c: &mut Computation, ram: Ram) {
-    trace!(
-        "Checking RAM {}, size {}, {} accesses",
+    debug!(
+        "Checking {} {}, size {}, {} accesses, keys {}, values {}",
+        if ram.cfg.covering_rom {
+            "covering ROM"
+        } else {
+            "RAM"
+        },
         ram.id,
         ram.size,
-        ram.accesses.len()
+        ram.accesses.len(),
+        ram.sort,
+        ram.val_sort,
     );
     let f = &ram.cfg.field;
     let (only_init, default) = match &ram.boundary_conditions {
@@ -26,8 +33,6 @@ pub fn check_ram(c: &mut Computation, ram: Ram) {
     let ns = Namespace::new().subspace(&format!("ram{id}"));
     let f_s = Sort::Field(f.clone());
     let v_s = ram.val_sort.clone();
-    let mut new_var =
-        |name: &str, val: Term| c.new_var(&ns.fqn(name), f_s.clone(), PROVER_VIS, Some(val));
 
     let mut assertions = Vec::new();
     // (1) sort the transcript, checking only that we've applied a permutation.
@@ -36,6 +41,8 @@ pub fn check_ram(c: &mut Computation, ram: Ram) {
             |name: &str, val: Term| c.new_var(&ns.fqn(name), Sort::Bool, PROVER_VIS, Some(val));
         permutation::waksman(&ram.accesses, &ram.cfg, &v_s, &mut new_bit_var)
     } else {
+        let mut new_var =
+            |name: &str, val: Term| c.new_var(&ns.fqn(name), f_s.clone(), PROVER_VIS, Some(val));
         permutation::msh(
             &ram.accesses,
             &ns,
@@ -50,98 +57,129 @@ pub fn check_ram(c: &mut Computation, ram: Ram) {
     let n = sorted_accesses.len();
     let mut accs = sorted_accesses;
 
-    // set c value if needed.
-    if !only_init {
-        accs[0].create = FieldBit::from_bool_lit(&ram.cfg, true);
-        for i in 0..(n - 1) {
-            let create = term![NOT; term![EQ; accs[i].idx.clone(), accs[i+1].idx.clone()]];
-            accs[i + 1].create = FieldBit::from_bool(&ram.cfg, create);
-        }
-    }
-
-    // (3a) v' = ite(a',v',v)
-    for i in 0..(n - 1) {
-        accs[i + 1].val = term_c![Op::Ite; accs[i+1].active.b.clone(), accs[i+1].val, accs[i].val];
-    }
-
-    assertions.push(accs[0].create.b.clone());
-
     let zero = pf_lit(f.new_v(0));
+    let one = pf_lit(f.new_v(1));
     fn sub(a: &Term, b: &Term) -> Term {
         term![PF_ADD; a.clone(), term![PF_NEG; b.clone()]]
     }
 
-    let mut deltas = Vec::new();
-    // To: check some condition on the start?
-    for j in 0..(n - 1) {
-        // previous entry
-        let i = &accs[j].idx;
-        let t = &accs[j].time;
-        let v = accs[j].val_hash.as_ref().expect("missing value hash");
-        // this entry
-        let i_n = &accs[j + 1].idx;
-        let t_n = &accs[j + 1].time;
-        let v_n = accs[j + 1].val_hash.as_ref().expect("missing value hash");
-        let c_n = &accs[j + 1].create;
-        let w_n = &accs[j + 1].write;
+    if ram.cfg.covering_rom {
+        // the covering ROM case
+        let mut new_var =
+            |name: &str, val: Term| c.new_var(&ns.fqn(name), f_s.clone(), PROVER_VIS, Some(val));
+        assertions.push(term_c![EQ; zero, accs[0].idx]);
+        for j in 0..(n - 1) {
+            // previous entry
+            let i = &accs[j].idx;
+            let v = accs[j].val_hash.as_ref().expect("missing value hash");
+            // this entry
+            let i_n = &accs[j + 1].idx;
+            let v_n = accs[j + 1].val_hash.as_ref().expect("missing value hash");
 
-        let v_p = if only_init {
-            v.clone()
-        } else {
-            term![ITE; c_n.b.clone(), default.clone(), v.clone()]
-        };
+            let i_d = sub(i_n, i);
+            let v_d = sub(v_n, v);
 
-        // delta = (1 - c')(t' - t)
-        deltas.push(term![PF_MUL; c_n.nf.clone(), sub(t_n, t)]);
+            // (i' - i)(i' - i - 1) = 0
+            assertions.push(term![EQ; term![PF_MUL; i_d.clone(), sub(&i_d, &one)], zero.clone()]);
 
-        // check c value if not computed: (i' - i)(1 - c') = 0
-        if only_init {
-            assertions.push(term![EQ; term![PF_MUL; sub(i_n, i), c_n.nf.clone()], zero.clone()]);
+            // r = 1/(i' - i)
+            let r = new_var(&format!("r{}", j), term_c![PF_RECIP; i_d]);
+            // (i' - i)r(v' - v) = v' - v  [v' = v OR i' != i]
+            assertions.push(term![EQ; term![PF_MUL; i_d, r, v_d.clone()], v_d]);
         }
-        // writes allow a value change: (v' - v)(1 - w') = 0
-        assertions.push(term![EQ; term![PF_MUL; sub(v_n, &v_p), w_n.nf.clone()], zero.clone()]);
-    }
-
-    // check that index blocks are unique
-    if !only_init {
-        if ram.cfg.sort_indices {
-            let bits = ram.size.next_power_of_two().ilog2() as usize;
-            trace!("Index difference checks ({bits} bits)");
-            assertions.push(term![Op::PfFitsInBits(bits); accs[0].idx.clone()]);
-            for j in 0..(n - 1) {
-                let d = pf_sub(accs[j + 1].idx.clone(), accs[j].idx.clone());
-                assertions.push(term![Op::PfFitsInBits(bits); d]);
-            }
-        } else {
-            derivative_gcd(
-                c,
-                accs.iter().map(|a| a.idx.clone()).collect(),
-                accs.iter().map(|a| a.create.b.clone()).collect(),
-                &ns,
-                &mut assertions,
-                f,
-            );
-        }
-    }
-
-    // check ranges
-    assertions.push(c.outputs[0].clone());
-    #[allow(clippy::type_complexity)]
-    let range_checker: Box<
-        dyn Fn(&mut Computation, Vec<Term>, &Namespace, &mut Vec<Term>, usize, &FieldT),
-    > = if ram.cfg.split_times {
-        Box::new(&bit_split_range_check)
+        assertions.push(term_c![EQ; ram.cfg.pf_lit(ram.size-1), accs[n - 1].idx]);
     } else {
-        Box::new(&range_check)
-    };
-    range_checker(
-        c,
-        deltas,
-        &ns.subspace("time"),
-        &mut assertions,
-        ram.next_time + 1,
-        f,
-    );
+        // the general RAM case
+        // set c value if needed.
+        if !only_init {
+            accs[0].create = FieldBit::from_bool_lit(&ram.cfg, true);
+            for i in 0..(n - 1) {
+                let create = term![NOT; term![EQ; accs[i].idx.clone(), accs[i+1].idx.clone()]];
+                accs[i + 1].create = FieldBit::from_bool(&ram.cfg, create);
+            }
+        }
+
+        // (3a) v' = ite(a',v',v)
+        for i in 0..(n - 1) {
+            accs[i + 1].val =
+                term_c![Op::Ite; accs[i+1].active.b.clone(), accs[i+1].val, accs[i].val];
+        }
+
+        assertions.push(accs[0].create.b.clone());
+
+        let mut deltas = Vec::new();
+        // To: check some condition on the start?
+        for j in 0..(n - 1) {
+            // previous entry
+            let i = &accs[j].idx;
+            let t = &accs[j].time;
+            let v = accs[j].val_hash.as_ref().expect("missing value hash");
+            // this entry
+            let i_n = &accs[j + 1].idx;
+            let t_n = &accs[j + 1].time;
+            let v_n = accs[j + 1].val_hash.as_ref().expect("missing value hash");
+            let c_n = &accs[j + 1].create;
+            let w_n = &accs[j + 1].write;
+
+            let v_p = if only_init {
+                v.clone()
+            } else {
+                term![ITE; c_n.b.clone(), default.clone(), v.clone()]
+            };
+
+            // delta = (1 - c')(t' - t)
+            deltas.push(term![PF_MUL; c_n.nf.clone(), sub(t_n, t)]);
+
+            // check c value if not computed: (i' - i)(1 - c') = 0
+            if only_init {
+                assertions
+                    .push(term![EQ; term![PF_MUL; sub(i_n, i), c_n.nf.clone()], zero.clone()]);
+            }
+            // writes allow a value change: (v' - v)(1 - w') = 0
+            assertions.push(term![EQ; term![PF_MUL; sub(v_n, &v_p), w_n.nf.clone()], zero.clone()]);
+        }
+
+        // check that index blocks are unique
+        if !only_init {
+            if ram.cfg.sort_indices {
+                let bits = ram.size.next_power_of_two().ilog2() as usize;
+                trace!("Index difference checks ({bits} bits)");
+                assertions.push(term![Op::PfFitsInBits(bits); accs[0].idx.clone()]);
+                for j in 0..(n - 1) {
+                    let d = pf_sub(accs[j + 1].idx.clone(), accs[j].idx.clone());
+                    assertions.push(term![Op::PfFitsInBits(bits); d]);
+                }
+            } else {
+                derivative_gcd(
+                    c,
+                    accs.iter().map(|a| a.idx.clone()).collect(),
+                    accs.iter().map(|a| a.create.b.clone()).collect(),
+                    &ns,
+                    &mut assertions,
+                    f,
+                );
+            }
+        }
+
+        // check ranges
+        assertions.push(c.outputs[0].clone());
+        #[allow(clippy::type_complexity)]
+        let range_checker: Box<
+            dyn Fn(&mut Computation, Vec<Term>, &Namespace, &mut Vec<Term>, usize, &FieldT),
+        > = if ram.cfg.split_times {
+            Box::new(&bit_split_range_check)
+        } else {
+            Box::new(&range_check)
+        };
+        range_checker(
+            c,
+            deltas,
+            &ns.subspace("time"),
+            &mut assertions,
+            ram.next_time + 1,
+            f,
+        );
+    }
     c.outputs[0] = term(AND, assertions);
 }
 

src/ir/opt/mem/ram/volatile.rs

@@ -97,7 +97,7 @@ impl ArrayGraph {
         // first, we grow the set of RAM terms, from leaves towards dependents.
         {
             // we start with the explicitly marked RAMs
-            trace!("Starting with {} RAMS", c.ram_arrays.len());
+            trace!("Starting with {} RAMs", c.ram_arrays.len());
             let mut stack: Vec<Term> = c
                 .ram_arrays
                 .iter()
@@ -355,6 +355,13 @@ impl RewritePass for Extactor {
             .iter()
             .map(|o| cache.get(o).unwrap().clone())
             .collect();
+        if !self.cfg.waksman {
+            for ram in &mut self.rams {
+                if ram.is_covering_rom() {
+                    ram.cfg.covering_rom = true;
+                }
+            }
+        }
     }
 }
 
@@ -378,10 +385,12 @@ pub fn extract(c: &mut Computation, cfg: AccessCfg) -> Vec<Ram> {
 /// Extract any volatile RAMS from a computation, and emit checks.
 pub fn apply(c: &mut Computation, cfg: &AccessCfg) {
     if c.ram_arrays.is_empty() {
-        debug!("Skipping VolatileRam; no RAM arrays");
+        debug!("Skipping VolatileRam; no RAM arrays marked.");
+        debug!("Found 0 RAMs");
         return;
     }
     let rams = extract(c, cfg.clone());
+    debug!("Found {} transcripts", rams.len());
     if !rams.is_empty() {
         for ram in rams {
             super::checker::check_ram(c, ram);

src/ir/opt/scalarize_vars.rs

@@ -1,5 +1,5 @@
 //! Replacing array and tuple variables with scalars.
-use log::debug;
+use log::trace;
 
 use crate::ir::opt::visit::RewritePass;
 use crate::ir::term::*;
@@ -52,7 +52,7 @@ fn create_vars(
         _ => {
             // don't request a new variable if we're not recursing...
             if !top_rec_level {
-                debug!("New scalar var: {}", prefix);
+                trace!("New scalar var: {}", prefix);
                 new_var_requests.push((prefix.into(), prefix_term));
             }
             leaf_term(Op::Var(prefix.into(), sort.clone()))
@@ -68,7 +68,7 @@ impl RewritePass for Pass {
         _rewritten_children: F,
     ) -> Option<Term> {
         if let Op::Var(name, sort) = &orig.op() {
-            debug!("Considering var: {}", name);
+            trace!("Considering var: {}", name);
             if !computation.metadata.lookup(name).committed {
                 let mut new_var_reqs = Vec::new();
                 let new = create_vars(name, orig.clone(), sort, &mut new_var_reqs, true);
@@ -77,7 +77,7 @@ impl RewritePass for Pass {
                 }
                 Some(new)
             } else {
-                debug!("Skipping b/c it is commited.");
+                trace!("Skipping b/c it is commited.");
                 None
             }
         } else {