Hint function enhancements

examples/fixture/asm/kimchi/hint.asm

@@ -10,6 +10,8 @@ DoubleGeneric<1,-1>
 DoubleGeneric<1,-1>
 DoubleGeneric<1,-1>
 DoubleGeneric<1,0,0,0,-16>
+DoubleGeneric<1,0,0,0,-32>
+DoubleGeneric<1,0,0,0,-4>
 DoubleGeneric<1,-1>
 DoubleGeneric<1,0,0,0,-3>
 DoubleGeneric<1,0,-1,0,1>
@@ -20,11 +22,11 @@ DoubleGeneric<1,0,-1,0,1>
 DoubleGeneric<1,0,0,0,-1>
 DoubleGeneric<1,0,0,0,-1>
 DoubleGeneric<1,-1>
-(0,0) -> (18,0)
-(1,0) -> (2,0) -> (9,1)
+(0,0) -> (20,0)
+(1,0) -> (2,0) -> (11,1)
 (4,0) -> (6,1)
 (4,2) -> (5,1)
-(5,0) -> (7,1) -> (18,1)
-(9,0) -> (11,0)
-(14,1) -> (15,0)
-(15,2) -> (16,0)
+(5,0) -> (7,1) -> (20,1)
+(11,0) -> (13,0)
+(16,1) -> (17,0)
+(17,2) -> (18,0)

examples/fixture/asm/r1cs/hint.asm

@@ -7,10 +7,12 @@
 v_5 == (v_6) * (1)
 v_4 == (v_7) * (1)
 16 == (v_8) * (1)
-v_2 == (v_9) * (1)
-3 == (v_10) * (1)
-1 == (v_11) * (1)
-1 == (v_12) * (1)
-1 == (-1 * v_13 + 1) * (1)
+32 == (v_9) * (1)
+4 == (v_10) * (1)
+v_2 == (v_11) * (1)
+3 == (v_12) * (1)
+1 == (v_13) * (1)
 1 == (v_14) * (1)
+1 == (-1 * v_15 + 1) * (1)
+1 == (v_16) * (1)
 v_4 == (v_1) * (1)

examples/hint.no

@@ -3,6 +3,14 @@ struct Thing {
     pub yy: Field,
 }
 
+fn init_arr(const LEN: Field) -> [Field; LEN] {
+    return [0; LEN];
+}
+
+hint fn cst_div(const lhs: Field, const rhs: Field) -> Field {
+    return lhs / rhs;
+}
+
 hint fn mul(lhs: Field, rhs: Field) -> Field {
     return lhs * rhs;
 }
@@ -20,16 +28,20 @@ hint fn ite(lhs: Field, rhs: Field) -> Field {
     return if lhs != rhs { lhs } else { rhs };
 }
 
-hint fn exp(const EXP: Field, val: Field) -> Field {
-    let mut res = val;
-
-    for num in 1..EXP {
-        res = res * val;
-    }
+hint fn exp(const EXP: Field, base: Field) -> Field {
+    let res = base ** EXP;
 
     return res;
 }
 
+hint fn lshift(val: Field, shift: Field) -> Field {
+    return val << shift;
+}
+
+hint fn rem(lhs: Field, rhs: Field) -> Field {
+    return lhs % rhs;
+}
+
 hint fn sub(lhs: Field, rhs: Field) -> Field {
     return lhs - rhs;
 }
@@ -68,6 +80,12 @@ fn main(pub public_input: Field, private_input: Field) -> Field {
     let kk = unsafe exp(4, public_input);
     assert_eq(kk, 16);
 
+    let k2 = unsafe lshift(public_input, 4);
+    assert_eq(k2, 32);
+
+    let ll = unsafe rem(kk, 12);
+    assert_eq(ll, 4);
+
     let thing = unsafe multiple_inputs_outputs([public_input, 3]);
     // have to include all the outputs from hint function, otherwise it throws vars not in circuit error.
     // this is because each individual element in the hint output maps to a separate cell var in noname.
@@ -82,5 +100,9 @@ fn main(pub public_input: Field, private_input: Field) -> Field {
     assert(!oo[1]);
     assert(oo[2]);
 
+    // mast phase can fold the constant value using hint functions
+    let one = unsafe cst_div(2, 2);
+    let arr = init_arr(one);
+    assert_eq(arr[0], 0);
     return xx;
 }

src/backends/kimchi/mod.rs

@@ -89,7 +89,7 @@ pub struct KimchiVesta {
 
     /// This is how you compute the value of each variable during witness generation.
     /// It is created during circuit generation.
-    pub(crate) vars_to_value: HashMap<usize, Value<Self>>,
+    pub(crate) vars_to_value: HashMap<usize, (Value<Self>, Span)>,
 
     /// The execution trace table with vars as placeholders.
     /// It is created during circuit generation,
@@ -307,7 +307,7 @@ impl Backend for KimchiVesta {
         self.next_variable += 1;
 
         // store it in the circuit_writer
-        self.vars_to_value.insert(var.index, val);
+        self.vars_to_value.insert(var.index, (val, span));
 
         var
     }
@@ -365,6 +365,16 @@ impl Backend for KimchiVesta {
 
         for var in 0..self.next_variable {
             if !written_vars.contains(&var) && !disable_safety_check {
+                let (val, span) = self
+                    .vars_to_value
+                    .get(&var)
+                    .expect("a var should be in vars_to_value");
+
+                if matches!(val, Value::HintIR(..)) {
+                    println!("a HintIR value not used in the circuit: {:?}", span);
+                    continue;
+                }
+
                 if let Some(private_cell_var) = self
                     .private_input_cell_vars
                     .iter()
@@ -378,7 +388,7 @@ impl Backend for KimchiVesta {
                     );
                     Err(err)?;
                 } else {
-                    Err(Error::new("contraint-finalization", ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"), Span::default()))?;
+                    Err(Error::new("contraint-finalization", ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"), *span))?;
                 }
             }
         }
@@ -403,7 +413,7 @@ impl Backend for KimchiVesta {
                 let var_idx = pub_var.cvar().unwrap().index;
                 let prev = self
                     .vars_to_value
-                    .insert(var_idx, Value::PublicOutput(Some(ret_var)));
+                    .insert(var_idx, (Value::PublicOutput(Some(ret_var)), ret_var.span));
                 assert!(prev.is_some());
             }
         }
@@ -419,7 +429,7 @@ impl Backend for KimchiVesta {
         var: &Self::Var,
     ) -> crate::error::Result<Self::Field> {
         let val = self.vars_to_value.get(&var.index).unwrap();
-        self.compute_val(env, val, var.index)
+        self.compute_val(env, &val.0, var.index)
     }
 
     fn generate_witness(
@@ -446,7 +456,7 @@ impl Backend for KimchiVesta {
                     // if it's a public output, defer it's computation
                     if matches!(
                         self.vars_to_value.get(&var.index),
-                        Some(Value::PublicOutput(_))
+                        Some((Value::PublicOutput(_), ..))
                     ) {
                         public_outputs_vars
                             .entry(*var)

src/backends/mod.rs

@@ -1,13 +1,12 @@
 use std::{fmt::Debug, str::FromStr};
 
 use ::kimchi::o1_utils::FieldHelpers;
-use ark_ff::{Field, One, PrimeField, Zero};
-use circ::ir::term::precomp::PreComp;
+use ark_ff::{Field, One, Zero};
 use fxhash::FxHashMap;
 use num_bigint::BigUint;
 
 use crate::{
-    circuit_writer::VarInfo,
+    circuit_writer::{ir::IRWriter, VarInfo},
     compiler::Sources,
     constants::Span,
     error::{Error, ErrorKind, Result},
@@ -206,14 +205,9 @@ pub trait Backend: Clone {
 
                 Ok(res)
             }
-            Value::HintIR(t, named_vars) => {
-                let mut precomp = PreComp::new();
-                // For hint evaluation purpose, precomp only has only one output and no connections with other parts,
-                // so just use a dummy output var name.
-                precomp.add_output("x".to_string(), t.clone());
-
+            Value::HintIR(t, named_vars, logs) => {
                 // map the named vars to env
-                let env = named_vars
+                let ir_env = named_vars
                     .iter()
                     .map(|(name, var)| {
                         let val = match var {
@@ -227,24 +221,21 @@ pub trait Backend: Clone {
                     })
                     .collect::<FxHashMap<String, circ::ir::term::Value>>();
 
-                // evaluate and get the only one output
-                let eval_map = precomp.eval(&env);
-                let value = eval_map.get("x").unwrap();
-                // convert to field
-                let res = match value {
-                    circ::ir::term::Value::Field(f) => {
-                        let bytes = f.i().to_digits::<u8>(rug::integer::Order::Lsf);
-                        Self::Field::from_le_bytes_mod_order(&bytes)
-                    }
-                    circ::ir::term::Value::Bool(b) => {
-                        if *b {
-                            Self::Field::one()
-                        } else {
-                            Self::Field::zero()
-                        }
-                    }
-                    _ => panic!("unexpected output type"),
-                };
+                // evaluate logs
+                for log in logs {
+                    // check the cache on env and log, and only evaluate if not in cache
+                    let res: Vec<Self::Field> = IRWriter::<Self>::eval_ir(&ir_env, log);
+                    // format and print out array
+                    println!(
+                        "log: {:#?}",
+                        res.iter().map(|f| f.pretty()).collect::<Vec<String>>()
+                    );
+                }
+
+                // evaluate the term
+                let res = IRWriter::<Self>::eval_ir(&ir_env, t)[0];
+
+                env.cached_values.insert(cache_key, res); // cache
 
                 Ok(res)
             }

src/backends/r1cs/mod.rs

@@ -267,7 +267,7 @@ where
 {
     /// Constraints in the r1cs.
     constraints: Vec<Constraint<F>>,
-    witness_vector: Vec<Value<Self>>,
+    witness_vector: Vec<(Value<Self>, Span)>,
     /// Debug information for each constraint.
     debug_info: Vec<DebugInfo>,
     /// Debug information for var info.
@@ -384,7 +384,7 @@ where
             span,
         };
 
-        self.witness_vector.insert(var.index, val);
+        self.witness_vector.insert(var.index, (val, span));
 
         LinearCombination::from(var)
     }
@@ -419,8 +419,9 @@ where
                 // replace the computation of the public output vars with the actual variables being returned here
                 let var_idx = pub_var.cvar().unwrap().to_cell_var().index;
                 let prev = &self.witness_vector[var_idx];
-                assert!(matches!(prev, Value::PublicOutput(None)));
-                self.witness_vector[var_idx] = Value::PublicOutput(Some(ret_var));
+                assert!(matches!(prev.0, Value::PublicOutput(None)));
+                self.witness_vector[var_idx] =
+                    (Value::PublicOutput(Some(ret_var.clone())), ret_var.span);
             }
         }
 
@@ -435,7 +436,7 @@ where
         }
 
         // check if every cell vars end up being a cell var in the circuit or public output
-        for (index, _) in self.witness_vector.iter().enumerate() {
+        for (index, (val, span)) in self.witness_vector.iter().enumerate() {
             // Skip the first var which is always 1
             // - In a linear combination, each of the vars can be paired with a coefficient.
             // - The first var is assumed to be the factor of the constant of a linear combination.
@@ -444,6 +445,11 @@ where
             }
 
             if !written_vars.contains(&index) && !disable_safety_check {
+                // ignore HintIR val
+                if let Value::HintIR(..) = val {
+                    println!("a HintIR value not used in the circuit: {:?}", span);
+                    continue;
+                }
                 if let Some(private_cell_var) = self
                     .private_input_cell_vars
                     .iter()
@@ -458,7 +464,7 @@ where
                     Err(Error::new(
                         "constraint-finalization",
                         ErrorKind::UnexpectedError("there's a bug in the circuit_writer, some cellvar does not end up being a cellvar in the circuit!"),
-                        Span::default(),
+                        *span,
                     ))?
                 }
             }
@@ -478,7 +484,7 @@ where
 
         for (var, factor) in &lc.terms {
             let var_val = self.witness_vector.get(var.index).unwrap();
-            let calc = self.compute_val(env, var_val, var.index)? * factor;
+            let calc = self.compute_val(env, &var_val.0, var.index)? * factor;
             val += calc;
         }
 
@@ -501,11 +507,11 @@ where
             .iter()
             .enumerate()
             .map(|(index, val)| {
-                match val {
+                match val.0 {
                     // Defer calculation for output vars.
                     // The reasoning behind this is to avoid deep recursion potentially triggered by the public output var at the beginning.
                     Value::PublicOutput(_) => Ok(F::zero()),
-                    _ => self.compute_val(witness_env, val, index),
+                    _ => self.compute_val(witness_env, &val.0, index),
                 }
             })
             .collect::<crate::error::Result<Vec<F>>>()?;
@@ -735,7 +741,7 @@ mod tests {
 
         // first var should be initialized as 1
         assert_eq!(r1cs.witness_vector.len(), 1);
-        match &r1cs.witness_vector[0] {
+        match &r1cs.witness_vector[0].0 {
             crate::var::Value::Constant(cst) => {
                 assert_eq!(*cst, R1csBls12381Field::one());
             }