fix: Wrong Evaluation of Constraint Expressions using Expansion

src/transformer/ifs.rs

@@ -126,7 +126,11 @@ fn raise_ifs(mut e: Node) -> Node {
  .fold(true, |b, e| b && !matches!(e.e(), Expression::Void)));
  //
  match func {
- Intrinsic::Add
+ Intrinsic::Neg
+ | Intrinsic::Inv
+ | Intrinsic::Normalize
+ | Intrinsic::Exp
+ | Intrinsic::Add
  | Intrinsic::Sub
  | Intrinsic::Mul
  | Intrinsic::VectorAdd
@@ -147,7 +151,7 @@ fn raise_ifs(mut e: Node) -> Node {
  let new_then = func.unchecked_call(&then_args).unwrap();
  let mut new_args = vec![cond, new_then];
  // Pull out false branch (if applicable):
- // (func a b (if cond then else) c)
+ // (func a b (if cond c d) e)
  // ==> (if !cond (func a b d e))
  if let Some(arg_else) = args_if.get(2).cloned() {
  let mut else_args = args.clone();
@@ -163,13 +167,7 @@ fn raise_ifs(mut e: Node) -> Node {
  }
  e
  }
- Intrinsic::IfZero
- | Intrinsic::IfNotZero
- | Intrinsic::Neg
- | Intrinsic::Inv
- | Intrinsic::Normalize
- | Intrinsic::Exp
- | Intrinsic::Begin => e,
+ Intrinsic::IfZero | Intrinsic::IfNotZero | Intrinsic::Begin => e,
  }
  }
  Expression::List(xs) => {
@@ -330,7 +328,9 @@ pub fn expand_ifs(cs: &mut ConstraintSet) {
  // Raise ifs
  for c in cs.constraints.iter_mut() {
  if let Constraint::Vanishes { expr, .. } = c {
- *expr = Box::new(raise_ifs(*expr.clone()));
+ let nexpr = raise_ifs(*expr.clone());
+ // Replace old expression with new
+ *expr = Box::new(nexpr);
  }
  }
  for c in cs.constraints.iter_mut() {

tests/issue219_a.lisp

@@ -0,0 +1,5 @@
+(defcolumns X)
+
+(defconstraint Constraint ()
+ (neq! (if (is-zero 1) X X) X)
+)

tests/issue219_b.lisp

@@ -0,0 +1,4 @@
+(defcolumns ST X)
+
+(defconstraint constraint-test ()
+ (if-not-zero ST (is-not-zero! (if (vanishes! X) 1 1))))

tests/issue219_c.lisp

@@ -0,0 +1,4 @@
+(defcolumns ST X)
+
+(defconstraint constraint-test ()
+ (if-not-zero ST (vanishes! (- 1 (if (vanishes! X) 1 1)))))

tests/issue219_d.lisp

@@ -0,0 +1,4 @@
+(defcolumns ST X Y)
+
+(defconstraint constraint-test ()
+ (if-not-zero ST (vanishes! (- 1 (if (vanishes! X) Y 1)))))

tests/issue241_a.lisp

@@ -0,0 +1,7 @@
+(defcolumns X)
+
+(defconstraint constraint-1 () (is-not-zero! (if (is-zero 1) 1 1)))
+(defconstraint constraint-2 () (eq! (is-not-zero! (if (is-zero X) 1 X)) 0))
+(defconstraint constraint-3 () (eq! (~and! (is-not-zero! (if (is-zero 0) 1 0)) 0) 0))
+(defconstraint constraint-4 () (is-not-zero! (if (is-zero 0) 1 0)))
+(defconstraint constraint-5 () (is-not-zero! (if (is-zero X) 1 X)))

tests/issue241_b.lisp

@@ -0,0 +1,6 @@
+(defcolumns X ST)
+
+;; ST ==> x != 1
+(defconstraint constraint-6 () (if-not-zero ST (neq! 1 (if (is-zero 0) X X))))
+;; ST ==> x != 0
+(defconstraint constraint-7 () (if-not-zero ST (neq! 0 (if (is-zero X) X X))))

tests/models.rs

@@ -4,7 +4,7 @@
 /// be accepted and which should be rejected. In essence, we are
 /// comparing a Rust function (the model) against the constraints
 /// evaluated on the trace.
 struct Model {
  /// The name of this test (which should correspond to a lisp
  /// file).
  name: &'static str,
@@ -16,7 +16,7 @@
 }
 
 impl Model {
  const MIN_ELEMENT: isize = -1;
  const MAX_ELEMENT: isize = 1;
 
  /// Generate all traces matching the model configuration upto
@@ -111,7 +111,7 @@
 
 /// Represents an individial trace which, for a given number of rows,
 /// contains values for each of the columns.
 struct Trace {
  /// Simplistic column schema.
  cols: &'static [&'static str],
  /// The trace data, whose length must be divisible by `width`.
@@ -122,7 +122,7 @@
 }
 
 impl Trace {
  pub fn new(cols: &'static [&'static str], data: Vec<isize>) -> Self {
  Self {
  cols,
  data,
@@ -163,7 +163,7 @@
 
 /// Represents a single column which can contain zero (or more) rows
 /// of padding at the beginning.
 struct Column<'a> {
  // The raw data underlying this column
  data: &'a [isize],
  // The number of rows of passing which are assumed to be prepended
@@ -189,7 +189,7 @@
 
 /// The master list of active models. Tests will be automatically
 /// generated for each item in this list.
 static MODELS: &[Model] = &[
  Model {
  name: "arrays_1",
  cols: &["A", "B_1", "B_2", "B_3"],
@@ -230,6 +230,36 @@
  cols: &["X"],
  oracle: Some(|_| false),
  },
+ Model {
+ name: "issue241_a",
+ cols: &["X"],
+ oracle: Some(|_| true),
+ },
+ Model {
+ name: "issue241_b",
+ cols: &["ST", "X"],
+ oracle: Some(issue241_b_oracle),
+ },
+ Model {
+ name: "issue219_a",
+ cols: &["X"],
+ oracle: Some(|_| false),
+ },
+ Model {
+ name: "issue219_b",
+ cols: &["ST", "X"],
+ oracle: Some(|_| true),
+ },
+ Model {
+ name: "issue219_c",
+ cols: &["ST", "X"],
+ oracle: Some(|_| true),
+ },
+ Model {
+ name: "issue219_d",
+ cols: &["ST", "X", "Y"],
+ oracle: Some(issue219_d_oracle),
+ },
 ];
 
 // ===================================================================
@@ -237,7 +267,7 @@
 // ===================================================================
 
 #[allow(non_snake_case)]
 fn arrays_1_oracle(tr: &Trace) -> bool {
  let (A, B_1, B_2, B_3) = (tr.col("A"), tr.col("B_1"), tr.col("B_2"), tr.col("B_3"));
 
  for k in 0..tr.height() {
@@ -251,12 +281,12 @@
  true
 }
 
-// // ===================================================================
-// // IsZero
-// // ===================================================================
+// ===================================================================
+// IsZero
+// ===================================================================
 
 #[allow(non_snake_case)]
 fn iszero_oracle(tr: &Trace) -> bool {
  let (A, B) = (tr.col("A"), tr.col("B"));
 
  for k in 0..tr.height() {
@@ -267,9 +297,9 @@
  true
 }
 
-// // ===================================================================
-// // Shift
-// // ===================================================================
+// ===================================================================
+// Shift
+// ===================================================================
 
 #[allow(non_snake_case)]
 fn shift_1_oracle(tr: &Trace) -> bool {
@@ -323,3 +353,36 @@
  }
  true
 }
+
+// ===================================================================
+// Issue 241
+// ===================================================================
+
+#[allow(non_snake_case)]
+fn issue241_b_oracle(tr: &Trace) -> bool {
+ let (X, ST) = (tr.col("X"), tr.col("ST"));
+ for k in 0..tr.height() {
+ let c1 = ST[k] == 0 || X[k] != 1;
+ let c2 = ST[k] == 0 || X[k] != 0;
+ if !c1 || !c2 {
+ return false;
+ }
+ }
+ true
+}
+
+// ===================================================================
+// Issue 219
+// ===================================================================
+
+#[allow(non_snake_case)]
+fn issue219_d_oracle(tr: &Trace) -> bool {
+ let (ST, X, Y) = (tr.col("ST"), tr.col("X"), tr.col("Y"));
+
+ for k in 0..tr.height() {
+ if ST[k] != 0 && X[k] == 0 && Y[k] != 1 {
+ return false;
+ }
+ }
+ true
+}