Support logical implication (==>) in annotations

src/analyze/annot.rs

@@ -145,6 +145,14 @@ pub fn exists_path() -> [Symbol; 3] {
     ]
 }
 
+pub fn implies_path() -> [Symbol; 3] {
+    [
+        Symbol::intern("thrust"),
+        Symbol::intern("def"),
+        Symbol::intern("implies"),
+    ]
+}
+
 pub fn invariant_marker_path() -> [Symbol; 3] {
     [
         Symbol::intern("thrust"),

src/analyze/annot_fn.rs

@@ -102,6 +102,7 @@ enum FormulaOrTerm<T> {
     BinOp(chc::Term<T>, AmbiguousBinOp, chc::Term<T>),
     And(Box<FormulaOrTerm<T>>, Box<FormulaOrTerm<T>>),
     Or(Box<FormulaOrTerm<T>>, Box<FormulaOrTerm<T>>),
+    Implies(Box<FormulaOrTerm<T>>, Box<FormulaOrTerm<T>>),
     Not(Box<FormulaOrTerm<T>>),
     Literal(bool),
 }
@@ -124,6 +125,7 @@ impl<T> FormulaOrTerm<T> {
             }
             FormulaOrTerm::And(lhs, rhs) => lhs.into_formula()?.and(rhs.into_formula()?),
             FormulaOrTerm::Or(lhs, rhs) => lhs.into_formula()?.or(rhs.into_formula()?),
+            FormulaOrTerm::Implies(lhs, rhs) => lhs.into_formula()?.implies(rhs.into_formula()?),
             FormulaOrTerm::Not(formula_or_term) => formula_or_term.into_formula()?.not(),
             FormulaOrTerm::Literal(b) => {
                 if b {
@@ -148,6 +150,7 @@ impl<T> FormulaOrTerm<T> {
             FormulaOrTerm::BinOp(lhs, AmbiguousBinOp::Lt, rhs) => lhs.lt(rhs),
             FormulaOrTerm::And(lhs, rhs) => lhs.into_term()?.and(rhs.into_term()?),
             FormulaOrTerm::Or(lhs, rhs) => lhs.into_term()?.or(rhs.into_term()?),
+            FormulaOrTerm::Implies(lhs, rhs) => lhs.into_term()?.not().or(rhs.into_term()?),
             FormulaOrTerm::Not(formula_or_term) => formula_or_term.into_term()?.not(),
             FormulaOrTerm::Literal(b) => chc::Term::bool(b),
         };
@@ -607,6 +610,14 @@ impl<'a, 'tcx> AnnotFnTranslator<'a, 'tcx> {
                                 body_formula,
                             ));
                         }
+                        if Some(def_id) == self.def_ids.implies() {
+                            let [lhs, rhs] = args else {
+                                panic!("implies takes exactly 2 arguments");
+                            };
+                            let lhs = self.to_formula_or_term(lhs);
+                            let rhs = self.to_formula_or_term(rhs);
+                            return FormulaOrTerm::Implies(lhs.into(), rhs.into());
+                        }
                         if Some(def_id) == self.def_ids.mut_model_new() {
                             assert_eq!(args.len(), 2, "Mut::new takes exactly 2 arguments");
                             let t1 = self.to_term(&args[0]);

src/analyze/did_cache.rs

@@ -25,6 +25,7 @@ struct DefIds {
     array_model_store: OnceCell<Option<DefId>>,
 
     exists: OnceCell<Option<DefId>>,
+    implies: OnceCell<Option<DefId>>,
     invariant_marker: OnceCell<Option<DefId>>,
 
     closure_precondition: OnceCell<Option<DefId>>,
@@ -181,6 +182,13 @@ impl<'tcx> DefIdCache<'tcx> {
             .get_or_init(|| self.annotated_def(&crate::analyze::annot::exists_path()))
     }
 
+    pub fn implies(&self) -> Option<DefId> {
+        *self
+            .def_ids
+            .implies
+            .get_or_init(|| self.annotated_def(&crate::analyze::annot::implies_path()))
+    }
+
     pub fn invariant_marker(&self) -> Option<DefId> {
         *self
             .def_ids

src/chc.rs

@@ -1251,6 +1251,7 @@ pub enum Formula<V = TermVarIdx> {
     Not(Box<Formula<V>>),
     And(Vec<Formula<V>>),
     Or(Vec<Formula<V>>),
+    Implies(Box<Formula<V>>, Box<Formula<V>>),
     Exists(Vec<(String, Sort)>, Box<Formula<V>>),
 }
 
@@ -1293,6 +1294,13 @@ where
                 );
                 inner.group()
             }
+            Formula::Implies(lhs, rhs) => lhs
+                .pretty_atom(allocator)
+                .append(allocator.space())
+                .append(allocator.text("==>"))
+                .append(allocator.line())
+                .append(rhs.pretty_atom(allocator))
+                .group(),
             Formula::Exists(vars, fo) => {
                 let vars = allocator.intersperse(
                     vars.iter().map(|(name, sort)| {
@@ -1327,7 +1335,7 @@ impl<V> Formula<V> {
         D::Doc: Clone,
     {
         match self {
-            Formula::And(_) | Formula::Or(_) | Formula::Exists { .. } => {
+            Formula::And(_) | Formula::Or(_) | Formula::Implies(_, _) | Formula::Exists { .. } => {
                 self.pretty(allocator).parens()
             }
             _ => self.pretty(allocator),
@@ -1348,6 +1356,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => fo.is_bottom(),
             Formula::And(fs) => fs.iter().all(Formula::is_top),
             Formula::Or(fs) => fs.iter().any(Formula::is_top),
+            Formula::Implies(lhs, rhs) => lhs.is_bottom() || rhs.is_top(),
             Formula::Exists(_, fo) => fo.is_top(),
         }
     }
@@ -1358,6 +1367,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => fo.is_top(),
             Formula::And(fs) => fs.iter().any(Formula::is_bottom),
             Formula::Or(fs) => fs.iter().all(Formula::is_bottom),
+            Formula::Implies(lhs, rhs) => lhs.is_top() && rhs.is_bottom(),
             Formula::Exists(_, fo) => fo.is_bottom(),
         }
     }
@@ -1389,6 +1399,10 @@ impl<V> Formula<V> {
         }
     }
 
+    pub fn implies(self, other: Self) -> Self {
+        Formula::Implies(Box::new(self), Box::new(other))
+    }
+
     pub fn exists(vars: Vec<(String, Sort)>, body: Self) -> Self {
         Formula::Exists(vars, Box::new(body))
     }
@@ -1406,6 +1420,9 @@ impl<V> Formula<V> {
                 Formula::And(fs.into_iter().map(|fo| fo.subst_var(&mut f)).collect())
             }
             Formula::Or(fs) => Formula::Or(fs.into_iter().map(|fo| fo.subst_var(&mut f)).collect()),
+            Formula::Implies(lhs, rhs) => {
+                Formula::Implies(Box::new(lhs.subst_var(&mut f)), Box::new(rhs.subst_var(f)))
+            }
             Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.subst_var(f))),
         }
     }
@@ -1421,6 +1438,9 @@ impl<V> Formula<V> {
             Formula::Not(fo) => Formula::Not(Box::new(fo.map_var(&mut f))),
             Formula::And(fs) => Formula::And(fs.into_iter().map(|fo| fo.map_var(&mut f)).collect()),
             Formula::Or(fs) => Formula::Or(fs.into_iter().map(|fo| fo.map_var(&mut f)).collect()),
+            Formula::Implies(lhs, rhs) => {
+                Formula::Implies(Box::new(lhs.map_var(&mut f)), Box::new(rhs.map_var(f)))
+            }
             Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.map_var(f))),
         }
     }
@@ -1435,6 +1455,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => Box::new(fo.fv()),
             Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::fv)),
             Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::fv)),
+            Formula::Implies(lhs, rhs) => Box::new(lhs.fv().chain(rhs.fv())),
             Formula::Exists(_, fo) => Box::new(fo.fv()),
         }
     }
@@ -1449,6 +1470,7 @@ impl<V> Formula<V> {
             Formula::Not(fo) => Box::new(fo.iter_atoms()),
             Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
             Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),
+            Formula::Implies(lhs, rhs) => Box::new(lhs.iter_atoms().chain(rhs.iter_atoms())),
             Formula::Exists(_, fo) => Box::new(fo.iter_atoms()),
         }
     }
@@ -1469,6 +1491,17 @@ impl<V> Formula<V> {
         match self {
             Formula::Atom(_atom) => {}
             Formula::Not(fo) => fo.simplify(),
+            Formula::Implies(lhs, rhs) => {
+                lhs.simplify();
+                rhs.simplify();
+                if lhs.is_bottom() || rhs.is_top() {
+                    *self = Formula::top();
+                } else if lhs.is_top() {
+                    *self = std::mem::take(&mut **rhs);
+                } else if rhs.is_bottom() {
+                    *self = std::mem::take(&mut **lhs).not();
+                }
+            }
             Formula::And(fs) => {
                 for fo in &mut *fs {
                     fo.simplify();
@@ -1624,7 +1657,7 @@ where
                 .into_iter()
                 .map(|a| a.guarded(guard.clone()))
                 .collect(),
-            formula: guard.not().or(formula),
+            formula: guard.implies(formula),
         }
     }
 }

src/chc/smtlib2.rs

@@ -288,6 +288,11 @@ impl<'ctx, 'a> std::fmt::Display for Formula<'ctx, 'a> {
                 let fs = List::open(fs.iter().map(|fo| Formula::new(self.ctx, self.clause, fo)));
                 write!(f, "(or {})", fs)
             }
+            chc::Formula::Implies(lhs, rhs) => {
+                let lhs = Formula::new(self.ctx, self.clause, lhs);
+                let rhs = Formula::new(self.ctx, self.clause, rhs);
+                write!(f, "(=> {lhs} {rhs})")
+            }
             chc::Formula::Exists(vars, fo) => {
                 let vars =
                     List::closed(vars.iter().map(|(v, s)| {

src/chc/unbox.rs

@@ -81,6 +81,9 @@ fn unbox_formula(formula: Formula) -> Formula {
         Formula::Not(fo) => Formula::Not(Box::new(unbox_formula(*fo))),
         Formula::And(fs) => Formula::And(fs.into_iter().map(unbox_formula).collect()),
         Formula::Or(fs) => Formula::Or(fs.into_iter().map(unbox_formula).collect()),
+        Formula::Implies(lhs, rhs) => {
+            Formula::Implies(Box::new(unbox_formula(*lhs)), Box::new(unbox_formula(*rhs)))
+        }
         Formula::Exists(vars, fo) => {
             let vars = vars.into_iter().map(|(v, s)| (v, unbox_sort(s))).collect();
             Formula::Exists(vars, Box::new(unbox_formula(*fo)))

src/rty.rs

@@ -1930,6 +1930,10 @@ fn subst_ty_params_in_formula<T, V>(formula: &mut chc::Formula<V>, subst: &TypeP
                 subst_ty_params_in_formula(f, subst);
             }
         }
+        chc::Formula::Implies(lhs, rhs) => {
+            subst_ty_params_in_formula(lhs, subst);
+            subst_ty_params_in_formula(rhs, subst);
+        }
         chc::Formula::Exists(vars, f) => {
             for (_, sort) in vars {
                 subst_ty_params_in_sort(sort, subst);

std.rs

@@ -325,6 +325,13 @@ mod thrust_models {
         unimplemented!()
     }
 
+    #[allow(dead_code)]
+    #[thrust::def::implies]
+    #[thrust::ignored]
+    pub fn implies(_lhs: bool, _rhs: bool) -> bool {
+        unimplemented!()
+    }
+
     #[thrust::def::invariant_marker]
     #[thrust::ignored]
     #[inline(never)]

tests/ui/fail/annot_implication.rs

@@ -0,0 +1,45 @@
+//@error-in-other-file: Unsat
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+use thrust_models::exists;
+
+#[thrust::trusted]
+#[thrust::callable]
+fn rand() -> i64 {
+    unimplemented!()
+}
+
+// Same contract as the `pass` counterpart, but the body returns a negative
+// value when `x > 0`, so the implication `(x > 0) ==> (result > 0)` is
+// violated. This confirms `==>` carries real implication semantics rather than
+// being silently accepted.
+#[thrust_macros::ensures((x > 0) ==> (result > 0))]
+fn f(x: i64) -> i64 {
+    if x > 0 {
+        -1
+    } else {
+        0
+    }
+}
+
+// An unparenthesized chain must parse right-associatively, i.e.
+// `(x > 10) ==> ((x > 5) ==> (result == 1))`. Left-associative parsing would
+// make this unprovable, so this case pins down associativity.
+#[thrust_macros::ensures((x > 10) ==> (x > 5) ==> (result == 1))]
+fn g(x: i64) -> i64 {
+    if x > 5 {
+        1
+    } else {
+        0
+    }
+}
+
+// Implication nested inside a quantifier's closure body.
+#[thrust_macros::ensures(exists(|y: i64| (1 == 1) ==> (result == 2 * y)))]
+fn k() -> i64 {
+    let x = rand();
+    x + x
+}
+
+fn main() {}

tests/ui/pass/annot_implication.rs

@@ -0,0 +1,43 @@
+//@check-pass
+//@compile-flags: -C debug-assertions=off
+//@rustc-env: THRUST_SOLVER=tests/thrust-pcsat-wrapper
+
+use thrust_models::exists;
+
+#[thrust::trusted]
+#[thrust::callable]
+fn rand() -> i64 {
+    unimplemented!()
+}
+
+// Basic implication in a postcondition: when the antecedent holds the
+// consequent must too; otherwise the obligation is vacuous.
+#[thrust_macros::ensures((x > 0) ==> (result > 0))]
+fn f(x: i64) -> i64 {
+    if x > 0 {
+        x
+    } else {
+        0
+    }
+}
+
+// An unparenthesized chain must parse right-associatively, i.e.
+// `(x > 10) ==> ((x > 5) ==> (result == 1))`. Left-associative parsing would
+// make this unprovable, so this case pins down associativity.
+#[thrust_macros::ensures((x > 10) ==> (x > 5) ==> (result == 1))]
+fn g(x: i64) -> i64 {
+    if x > 5 {
+        1
+    } else {
+        0
+    }
+}
+
+// Implication nested inside a quantifier's closure body.
+#[thrust_macros::ensures(exists(|y: i64| (1 == 1) ==> (result == 2 * y)))]
+fn k() -> i64 {
+    let x = rand();
+    x + x
+}
+
+fn main() {}

thrust-macros/Cargo.toml

@@ -10,4 +10,4 @@ proc-macro = true
 [dependencies]
 proc-macro2 = "1"
 quote = "1"
-syn = { version = "2", features = ["full", "visit", "visit-mut"] }
+syn = { version = "2", features = ["extra-traits", "full", "visit", "visit-mut"] }