Represent formula implication explicitly

coord-e · claude · commit 2da28c255e78 · 2026-06-14T14:20:43.000Z
style fix
diff --git a/src/analyze/annot.rs b/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"),
diff --git a/src/analyze/annot_fn.rs b/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]);
diff --git a/src/analyze/did_cache.rs b/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
diff --git a/src/chc.rs b/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),
         }
     }
 }
diff --git a/src/chc/smtlib2.rs b/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)| {
diff --git a/src/chc/unbox.rs b/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)))
diff --git a/src/rty.rs b/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);
diff --git a/std.rs b/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)]
diff --git a/thrust-macros/src/formula.rs b/thrust-macros/src/formula.rs
diff --git a/thrust-macros/src/invariant.rs b/thrust-macros/src/invariant.rs
diff --git a/thrust-macros/src/rty.rs b/thrust-macros/src/rty.rs
diff --git a/thrust-macros/src/spec.rs b/thrust-macros/src/spec.rs

Original file line number	Diff line number	Diff line change
`@@ -145,6 +145,14 @@ pub fn exists_path() -> [Symbol; 3] {`
`145`	`145`	`]`
`146`	`146`	`}`
`147`	`147`
	`148`	`+pub fn implies_path() -> [Symbol; 3] {`
	`149`	`+ [`
	`150`	`+ Symbol::intern("thrust"),`
	`151`	`+ Symbol::intern("def"),`
	`152`	`+ Symbol::intern("implies"),`
	`153`	`+ ]`
	`154`	`+}`
	`155`	`+`
`148`	`156`	`pub fn invariant_marker_path() -> [Symbol; 3] {`
`149`	`157`	`[`
`150`	`158`	`Symbol::intern("thrust"),`
Original file line number	Diff line number	Diff line change
`@@ -1251,6 +1251,7 @@ pub enum Formula<V = TermVarIdx> {`
`1251`	`1251`	`Not(Box<Formula<V>>),`
`1252`	`1252`	`And(Vec<Formula<V>>),`
`1253`	`1253`	`Or(Vec<Formula<V>>),`
	`1254`	`+ Implies(Box<Formula<V>>, Box<Formula<V>>),`
`1254`	`1255`	`Exists(Vec<(String, Sort)>, Box<Formula<V>>),`
`1255`	`1256`	`}`
`1256`	`1257`
`@@ -1293,6 +1294,13 @@ where`
`1293`	`1294`	`);`
`1294`	`1295`	`inner.group()`
`1295`	`1296`	`}`
	`1297`	`+ Formula::Implies(lhs, rhs) => lhs`
	`1298`	`+ .pretty_atom(allocator)`
	`1299`	`+ .append(allocator.space())`
	`1300`	`+ .append(allocator.text("==>"))`
	`1301`	`+ .append(allocator.line())`
	`1302`	`+ .append(rhs.pretty_atom(allocator))`
	`1303`	`+ .group(),`
`1296`	`1304`	`Formula::Exists(vars, fo) => {`
`1297`	`1305`	`let vars = allocator.intersperse(`
`1298`	`1306`	`vars.iter().map(\|(name, sort)\| {`
`@@ -1327,7 +1335,7 @@ impl<V> Formula<V> {`
`1327`	`1335`	`D::Doc: Clone,`
`1328`	`1336`	`{`
`1329`	`1337`	`match self {`
`1330`		`- Formula::And(_) \| Formula::Or(_) \| Formula::Exists { .. } => {`
	`1338`	`+ Formula::And(_) \| Formula::Or(_) \| Formula::Implies(_, _) \| Formula::Exists { .. } => {`
`1331`	`1339`	`self.pretty(allocator).parens()`
`1332`	`1340`	`}`
`1333`	`1341`	`_ => self.pretty(allocator),`
`@@ -1348,6 +1356,7 @@ impl<V> Formula<V> {`
`1348`	`1356`	`Formula::Not(fo) => fo.is_bottom(),`
`1349`	`1357`	`Formula::And(fs) => fs.iter().all(Formula::is_top),`
`1350`	`1358`	`Formula::Or(fs) => fs.iter().any(Formula::is_top),`
	`1359`	`+ Formula::Implies(lhs, rhs) => lhs.is_bottom() \|\| rhs.is_top(),`
`1351`	`1360`	`Formula::Exists(_, fo) => fo.is_top(),`
`1352`	`1361`	`}`
`1353`	`1362`	`}`
`@@ -1358,6 +1367,7 @@ impl<V> Formula<V> {`
`1358`	`1367`	`Formula::Not(fo) => fo.is_top(),`
`1359`	`1368`	`Formula::And(fs) => fs.iter().any(Formula::is_bottom),`
`1360`	`1369`	`Formula::Or(fs) => fs.iter().all(Formula::is_bottom),`
	`1370`	`+ Formula::Implies(lhs, rhs) => lhs.is_top() && rhs.is_bottom(),`
`1361`	`1371`	`Formula::Exists(_, fo) => fo.is_bottom(),`
`1362`	`1372`	`}`
`1363`	`1373`	`}`
`@@ -1389,6 +1399,10 @@ impl<V> Formula<V> {`
`1389`	`1399`	`}`
`1390`	`1400`	`}`
`1391`	`1401`
	`1402`	`+ pub fn implies(self, other: Self) -> Self {`
	`1403`	`+ Formula::Implies(Box::new(self), Box::new(other))`
	`1404`	`+ }`
	`1405`	`+`
`1392`	`1406`	`pub fn exists(vars: Vec<(String, Sort)>, body: Self) -> Self {`
`1393`	`1407`	`Formula::Exists(vars, Box::new(body))`
`1394`	`1408`	`}`
`@@ -1406,6 +1420,9 @@ impl<V> Formula<V> {`
`1406`	`1420`	`Formula::And(fs.into_iter().map(\|fo\| fo.subst_var(&mut f)).collect())`
`1407`	`1421`	`}`
`1408`	`1422`	`Formula::Or(fs) => Formula::Or(fs.into_iter().map(\|fo\| fo.subst_var(&mut f)).collect()),`
	`1423`	`+ Formula::Implies(lhs, rhs) => {`
	`1424`	`+ Formula::Implies(Box::new(lhs.subst_var(&mut f)), Box::new(rhs.subst_var(f)))`
	`1425`	`+ }`
`1409`	`1426`	`Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.subst_var(f))),`
`1410`	`1427`	`}`
`1411`	`1428`	`}`
`@@ -1421,6 +1438,9 @@ impl<V> Formula<V> {`
`1421`	`1438`	`Formula::Not(fo) => Formula::Not(Box::new(fo.map_var(&mut f))),`
`1422`	`1439`	`Formula::And(fs) => Formula::And(fs.into_iter().map(\|fo\| fo.map_var(&mut f)).collect()),`
`1423`	`1440`	`Formula::Or(fs) => Formula::Or(fs.into_iter().map(\|fo\| fo.map_var(&mut f)).collect()),`
	`1441`	`+ Formula::Implies(lhs, rhs) => {`
	`1442`	`+ Formula::Implies(Box::new(lhs.map_var(&mut f)), Box::new(rhs.map_var(f)))`
	`1443`	`+ }`
`1424`	`1444`	`Formula::Exists(vars, fo) => Formula::Exists(vars, Box::new(fo.map_var(f))),`
`1425`	`1445`	`}`
`1426`	`1446`	`}`
`@@ -1435,6 +1455,7 @@ impl<V> Formula<V> {`
`1435`	`1455`	`Formula::Not(fo) => Box::new(fo.fv()),`
`1436`	`1456`	`Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::fv)),`
`1437`	`1457`	`Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::fv)),`
	`1458`	`+ Formula::Implies(lhs, rhs) => Box::new(lhs.fv().chain(rhs.fv())),`
`1438`	`1459`	`Formula::Exists(_, fo) => Box::new(fo.fv()),`
`1439`	`1460`	`}`
`1440`	`1461`	`}`
`@@ -1449,6 +1470,7 @@ impl<V> Formula<V> {`
`1449`	`1470`	`Formula::Not(fo) => Box::new(fo.iter_atoms()),`
`1450`	`1471`	`Formula::And(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),`
`1451`	`1472`	`Formula::Or(fs) => Box::new(fs.iter().flat_map(Formula::iter_atoms)),`
	`1473`	`+ Formula::Implies(lhs, rhs) => Box::new(lhs.iter_atoms().chain(rhs.iter_atoms())),`
`1452`	`1474`	`Formula::Exists(_, fo) => Box::new(fo.iter_atoms()),`
`1453`	`1475`	`}`
`1454`	`1476`	`}`
`@@ -1469,6 +1491,17 @@ impl<V> Formula<V> {`
`1469`	`1491`	`match self {`
`1470`	`1492`	`Formula::Atom(_atom) => {}`
`1471`	`1493`	`Formula::Not(fo) => fo.simplify(),`
	`1494`	`+ Formula::Implies(lhs, rhs) => {`
	`1495`	`+ lhs.simplify();`
	`1496`	`+ rhs.simplify();`
	`1497`	`+ if lhs.is_bottom() \|\| rhs.is_top() {`
	`1498`	`+ *self = Formula::top();`
	`1499`	`+ } else if lhs.is_top() {`
	`1500`	`+ self = std::mem::take(&mut *rhs);`
	`1501`	`+ } else if rhs.is_bottom() {`
	`1502`	`+ self = std::mem::take(&mut *lhs).not();`
	`1503`	`+ }`
	`1504`	`+ }`
`1472`	`1505`	`Formula::And(fs) => {`
`1473`	`1506`	`for fo in &mut *fs {`
`1474`	`1507`	`fo.simplify();`
`@@ -1624,7 +1657,7 @@ where`
`1624`	`1657`	`.into_iter()`
`1625`	`1658`	`.map(\|a\| a.guarded(guard.clone()))`
`1626`	`1659`	`.collect(),`
`1627`		`- formula: guard.not().or(formula),`
	`1660`	`+ formula: guard.implies(formula),`
`1628`	`1661`	`}`
`1629`	`1662`	`}`
`1630`	`1663`	`}`
Original file line number	Diff line number	Diff line change
`@@ -1930,6 +1930,10 @@ fn subst_ty_params_in_formula<T, V>(formula: &mut chc::Formula<V>, subst: &TypeP`
`1930`	`1930`	`subst_ty_params_in_formula(f, subst);`
`1931`	`1931`	`}`
`1932`	`1932`	`}`
	`1933`	`+ chc::Formula::Implies(lhs, rhs) => {`
	`1934`	`+ subst_ty_params_in_formula(lhs, subst);`
	`1935`	`+ subst_ty_params_in_formula(rhs, subst);`
	`1936`	`+ }`
`1933`	`1937`	`chc::Formula::Exists(vars, f) => {`
`1934`	`1938`	`for (_, sort) in vars {`
`1935`	`1939`	`subst_ty_params_in_sort(sort, subst);`