From 05dffb869ea1303bca599796084c869ed36425b9 Mon Sep 17 00:00:00 2001 From: kata Date: Sat, 4 Jan 2025 15:36:45 +0800 Subject: [PATCH] print out unused HintIR witness values as a warning instead of throwing error --- src/backends/kimchi/mod.rs | 22 ++++++++++++++++------ src/backends/r1cs/mod.rs | 26 ++++++++++++++++---------- 2 files changed, 32 insertions(+), 16 deletions(-) diff --git a/src/backends/kimchi/mod.rs b/src/backends/kimchi/mod.rs index ee5e9160b..9605eff39 100644 --- a/src/backends/kimchi/mod.rs +++ b/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>, + pub(crate) vars_to_value: HashMap, Span)>, /// The execution trace table with vars as placeholders. /// It is created during circuit generation, @@ -303,7 +303,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 } @@ -361,6 +361,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() @@ -374,7 +384,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))?; } } } @@ -399,7 +409,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()); } } @@ -415,7 +425,7 @@ impl Backend for KimchiVesta { var: &Self::Var, ) -> crate::error::Result { 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( @@ -442,7 +452,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) diff --git a/src/backends/r1cs/mod.rs b/src/backends/r1cs/mod.rs index a48160498..0fa9952d5 100644 --- a/src/backends/r1cs/mod.rs +++ b/src/backends/r1cs/mod.rs @@ -267,7 +267,7 @@ where { /// Constraints in the r1cs. constraints: Vec>, - witness_vector: Vec>, + witness_vector: Vec<(Value, Span)>, /// Debug information for each constraint. debug_info: Vec, /// 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::>>()?; @@ -973,7 +979,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()); }