Propagate known: thoughts

executor/src/witgen/jit/single_step_processor.rs

@@ -181,6 +181,16 @@ mod test {
         B' = B;
         ";
         let code = generate_single_step(input, "Main").unwrap();
+
+        // TODO:
+        // if VM::instr_add[0] == 1, we want to infer that VM::instr_mul[1] = 0
+        // the problem is that we have the submachine call only on row 0,
+        // and we want to keep it that way because we do not want to insert
+        // to submachine calls.
+        // this means we need a "pre-complete" submachine call on row 1,
+        // which is used to infer range constraints but does not actually add
+        // the call.
+
         assert_eq!(
             format_code(&code),
             "\

executor/src/witgen/jit/witgen_inference.rs

@@ -239,18 +239,6 @@ impl<'a, T: FieldElement, FixedEval: FixedEvaluator<T>> WitgenInference<'a, T, F
                 };
                 let result = (lhs_evaluated - rhs_evaluated).solve().unwrap();
                 if !result.effects.is_empty() {
-                    println!(
-                        "Got new effects:\n{}",
-                        result
-                            .effects
-                            .iter()
-                            .map(|e| match e {
-                                Effect::Assignment(v, expr) => format!("{v} = {expr}"),
-                                Effect::RangeConstraint(v, rc) => format!("{v}: {rc}"),
-                                _ => panic!("Unexpected effect."),
-                            })
-                            .format("\n")
-                    );
                     return result;
                 }
             }