Debug in progress

Author: Jiangkm3

circ_blocks/aaa

@@ -1,7 +1,7 @@
 // TODO: Might want to simplify Liveness Analysis & PMR now that scope changes are handled in optimization
 
 const PRINT_PROOF: bool = false;
-const INLINE_SPARTAN_PROOF: bool = true;
+const INLINE_SPARTAN_PROOF: bool = false;
 const TOTAL_NUM_VARS_BOUND: usize = 10000000000;
 const MAX_FILE_SIZE: usize = 1073741824;
 
@@ -951,9 +951,15 @@ fn get_run_time_knowledge<const VERBOSE: bool, S: SpartanExtensionField + Send +
         }
         let mut evaluator = StagedWitCompEvaluator::new(&prover_data_list[id].precompute);
         let mut eval = Vec::new();
+        if i == 0 {
+            println!("INPUT: {:?}", input);
+        }
         eval.extend(evaluator.eval_stage(input).into_iter().cloned());
         // Drop the last entry of io, which is the dummy return 0
         eval.pop();
+        if i == 0 {
+            println!("EVAL: {:?}", eval);
+        }
         eval.extend(
             evaluator
                 .eval_stage(Default::default())

circ_blocks/bbb

@@ -3183,11 +3183,11 @@ impl<'ast> ZGen<'ast> {
     }
 
     // Convert a list of blocks to circ_ir
-    pub fn bls_to_circ(&'ast self, blks: &Vec<Block>) {
+    pub fn bls_to_circ<const PROVER: bool>(&'ast self, blks: &Vec<Block>) {
         for b in blks {
             let f = &format!("Block_{}", b.name);
             self.circ_init_block(f);
-            self.bl_to_circ::<false>(&b, f);
+            self.bl_to_circ::<false, PROVER>(&b, f);
         }
     }
 
@@ -3721,7 +3721,8 @@ impl<'ast> ZGen<'ast> {
     // Convert a block to circ_ir
     // This can be done to either produce the constraints, or to estimate the size of constraints
     // In estimation mode, we rename all output variable from X -> oX, add assertion, and process the terminator
-    pub fn bl_to_circ<const ESTIMATE: bool>(&self, b: &Block, f: &str) {
+    // If in prover mode, declare all block outputs at the end of the block
+    pub fn bl_to_circ<const ESTIMATE: bool, const PROVER: bool>(&self, b: &Block, f: &str) {
         debug!("Bl to Circ: {}", b.name);
 
         // setup stack frame for entry function
@@ -3958,20 +3959,36 @@ impl<'ast> ZGen<'ast> {
 
         if let Some(r) = self.circ_exit_fn() {
             match self.mode {
-                Mode::Mpc(_) => {
-                    let ret_term = r.unwrap_term();
-                    let ret_terms = ret_term.terms();
-                    self.circ
-                        .borrow()
-                        .cir_ctx()
-                        .cs
-                        .borrow_mut()
-                        .get_mut(f)
-                        .unwrap()
-                        .outputs
-                        .extend(ret_terms);
-                }
                 Mode::Proof => {
+                    if PROVER {
+                        for (o_name, o_ty) in &b.outputs {
+                            if let Some(o_ty) = o_ty {
+                                println!("CVARS_STACK: {:?}", self.cvars_stack);
+                                println!("O_NAME: {}", o_name);
+                                let o_val = self.cvar_lookup(&o_name).unwrap();
+                                let o_var_val = self
+                                    .circ_declare_input(
+                                        &f,
+                                        o_name.to_string(),
+                                        o_ty,
+                                        ZVis::Public,
+                                        Some(o_val.clone()),
+                                        false,
+                                        &None,
+                                    )
+                                    .expect(&format!("circ_declare {o_name}"));
+                                let o_eq = eq(o_val, o_var_val).unwrap().term;
+                                let mut assertions = std::mem::take(&mut *self.assertions.borrow_mut());
+                                let o_assert = if assertions.is_empty() {
+                                    o_eq
+                                } else {
+                                    assertions.push(o_eq);
+                                    term(AND, assertions)
+                                };
+                                self.circ.borrow_mut().assert(&f, o_assert);
+                            }
+                        }
+                    }
                     let ty = ret_ty.as_ref().unwrap();
                     let name = "return".to_owned();
                     let ret_val = r.unwrap_term();
@@ -3996,28 +4013,6 @@ impl<'ast> ZGen<'ast> {
                     };
                     self.circ.borrow_mut().assert(&f, to_assert);
                 }
-                Mode::Opt => {
-                    let ret_term = r.unwrap_term();
-                    let ret_terms = ret_term.terms();
-                    assert!(
-                        ret_terms.len() == 1,
-                        "When compiling to optimize, there can only be one output"
-                    );
-                    let t = ret_terms.into_iter().next().unwrap();
-                    let t_sort = check(&t);
-                    if !matches!(t_sort, Sort::BitVector(_)) {
-                        panic!("Cannot maximize output of type {}", t_sort);
-                    }
-                    self.circ
-                        .borrow()
-                        .cir_ctx()
-                        .cs
-                        .borrow_mut()
-                        .get_mut(f)
-                        .unwrap()
-                        .outputs
-                        .push(t);
-                }
                 _ => {
                     panic!("Supported Mode!")
                 }

circ_blocks/ccc

@@ -2763,7 +2763,7 @@ impl<'ast> ZGen<'ast> {
     fn bl_count_num_cons(&self, bl: &Block<'ast>) -> usize {
         let block_name = &format!("Pseudo_Block_{}", bl.name);
         self.circ_init_block(block_name);
-        self.bl_to_circ::<true>(bl, block_name);
+        self.bl_to_circ::<true, false>(bl, block_name);
 
         let mut cs = Computations::new();
         cs.comps = self.circ.borrow().cir_ctx().cs.borrow_mut().clone();

circ_blocks/examples/zxc.rs

@@ -87,7 +87,7 @@ impl FrontEnd for ZSharpFE {
         // NOTE: The input of block 0 includes %BN, which should be removed when reasoning about function input
         let func_input_width = blks[0].get_num_inputs() - 1;
         println!("\n\n--\nCirc IR:");
-        g.bls_to_circ(&blks);
+        g.bls_to_circ::<false>(&blks);
 
         g.generics_stack_pop();
         g.file_stack_pop();
@@ -400,6 +400,15 @@ impl ZSharpFE {
         let convert_time = convert_start.elapsed();
         println!("\n--\nConvert time: {}ms", convert_time.as_millis());
 
+        g.bls_to_circ::<true>(&blks);
+        g.generics_stack_pop();
+        g.file_stack_pop();
+        let mut cs = Computations::new();
+        cs.comps = g.into_circify().cir_ctx().cs.borrow_mut().clone();
+        for (name, c) in cs.comps {
+            println!("{}: {:?}", name, c);
+        }
+
         return (
             ret,
             block_id_list,
@@ -1415,7 +1424,7 @@ impl<'ast> ZGen<'ast> {
                 .map_err(|e| format!("{e}"))
             }
             ast::Statement::Assertion(e) => {
-                match self.expr_impl_::<true>(&e.expression).and_then(|v| {
+                match self.expr_impl_::<IS_CNST>(&e.expression).and_then(|v| {
                     const_bool(v)
                         .ok_or_else(|| "interpreting expr as const bool failed".to_string())
                 }) {

circ_blocks/src/front/zsharp/blocks.rs

@@ -0,0 +1,5 @@
+low 0
+b 0
+c 0
+high 800
+END

circ_blocks/src/front/zsharp/blocks_optimization.rs

@@ -0,0 +1,26 @@
+def main(u32 low, u32 b, u32 c, u32 high) -> u32:
+    array_decl u32[ro high] arr
+    u32 sum = 0
+    for u32 i in 0..high do
+        sum = sum + i
+        arr[i] = sum
+    endfor
+
+
+    // random access to ensure array is written in memory
+    u32 x = arr[b]
+
+    u32 min = arr[low]
+    u32 min_idx = low
+
+    u32 i = low + 1
+    while i < high do
+        if arr[i] < min then
+            min = arr[i]
+            min_idx = i
+        endif
+        i = i + 1
+    endwhile
+
+
+    return min + (min_idx + x) * c