Skip to content

Commit

Permalink
print out unused HintIR witness values as a warning instead of throwi…
Browse files Browse the repository at this point in the history
…ng error
  • Loading branch information
katat committed Jan 4, 2025
1 parent 0a41031 commit 05dffb8
Show file tree
Hide file tree
Showing 2 changed files with 32 additions and 16 deletions.
22 changes: 16 additions & 6 deletions src/backends/kimchi/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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,
Expand Down Expand Up @@ -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
}
Expand Down Expand Up @@ -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()
Expand All @@ -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))?;
}
}
}
Expand All @@ -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());
}
}
Expand All @@ -415,7 +425,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<B: Backend>(
Expand All @@ -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)
Expand Down
26 changes: 16 additions & 10 deletions src/backends/r1cs/mod.rs
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -384,7 +384,7 @@ where
span,
};

self.witness_vector.insert(var.index, val);
self.witness_vector.insert(var.index, (val, span));

LinearCombination::from(var)
}
Expand Down Expand Up @@ -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);
}
}

Expand All @@ -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.
Expand All @@ -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()
Expand All @@ -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,
))?
}
}
Expand All @@ -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;
}

Expand All @@ -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>>>()?;
Expand Down Expand Up @@ -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());
}
Expand Down

0 comments on commit 05dffb8

Please sign in to comment.