Support lifting reverse implication: <==

verus-lang · Dec 19, 2024 · 97b8d77 · 97b8d77
1 parent 9fd46e3
commit 97b8d77
Show file tree

Hide file tree

Showing 6 changed files with 14 additions and 3 deletions.
diff --git a/crates/hir-ty/src/mir/lower.rs b/crates/hir-ty/src/mir/lower.rs
@@ -1034,6 +1034,9 @@ impl<'ctx> MirLowerCtx<'ctx> {
                         syntax::ast::LogicOp::Imply => {
                             todo!()
                         }
+                        syntax::ast::LogicOp::RevImply => {
+                            todo!()
+                        }
                         syntax::ast::LogicOp::Iff => {
                             todo!()
                         }
@@ -1075,6 +1078,7 @@ impl<'ctx> MirLowerCtx<'ctx> {
                                 hir_def::hir::LogicOp::And => BinOp::BitAnd, // FIXME: make these short circuit
                                 hir_def::hir::LogicOp::Or => BinOp::BitOr,
                                 hir_def::hir::LogicOp::Imply => todo!(),
+                                hir_def::hir::LogicOp::RevImply => todo!(),
                                 hir_def::hir::LogicOp::Iff => todo!(),
                             },
                             hir_def::hir::BinaryOp::ArithOp(op) => BinOp::from(op),

diff --git a/crates/syntax/src/ast/expr_ext.rs b/crates/syntax/src/ast/expr_ext.rs
@@ -158,10 +158,12 @@ impl ast::BinExpr {
             let bin_op = match c.kind() {
                 T![||] => BinaryOp::LogicOp(LogicOp::Or),
                 T![&&] => BinaryOp::LogicOp(LogicOp::And),
+                // verus
                 T![|||] => BinaryOp::LogicOp(LogicOp::Or),
                 T![&&&] => BinaryOp::LogicOp(LogicOp::And),
                 T![==>]=> BinaryOp::LogicOp(LogicOp::Imply),
                 T![<==>] => BinaryOp::LogicOp(LogicOp::Iff),
+                T![<==]=> BinaryOp::LogicOp(LogicOp::RevImply),
 
                 T![==] => BinaryOp::CmpOp(CmpOp::Eq { negated: false }),
                 T![!=] => BinaryOp::CmpOp(CmpOp::Eq { negated: true }),

diff --git a/crates/syntax/src/ast/operators.rs b/crates/syntax/src/ast/operators.rs
@@ -36,6 +36,7 @@ pub enum LogicOp {
     Or,
     // verus
     Imply,
+    RevImply,
     Iff,
 }
 
@@ -71,6 +72,7 @@ impl fmt::Display for LogicOp {
             LogicOp::And => "&&",
             LogicOp::Or => "||",
             LogicOp::Imply => "==>",
+            LogicOp::RevImply => "<==",
             LogicOp::Iff => "<==>",
         };
         f.write_str(res)

diff --git a/crates/syntax/src/ast/prec.rs b/crates/syntax/src/ast/prec.rs
@@ -156,6 +156,7 @@ impl Expr {
                         And => (9, 10),
                         // verus
                         Imply => (0, 0),
+                        RevImply => (0, 0),
                         Iff => (0, 0),
                     },
                     CmpOp(_) => (11, 11),

diff --git a/crates/va-test/examples/misc-parsing/src/main.rs b/crates/va-test/examples/misc-parsing/src/main.rs
@@ -1,9 +1,11 @@
 verus! {
 
-spec fn mul_auto(x:bool, y:bool) -> bool {
-    x &&& y
+spec fn lemma_div_basics(a:bool, b:bool)
+{
+    a <== b
 }
 
+
 } // verus!
 
 fn main() { }
diff --git a/crates/va-test/src/main.rs b/crates/va-test/src/main.rs
@@ -100,7 +100,7 @@ fn main() {
                         println!("Failed to lift function {:?}: got error: {:?}", foo.name(&db), fn_vst_result);
                         continue;
                     }
-                    let fn_vst: vst::Fn = fn_vst_result.expect("shouldn't have been an Error at this point"); //fn_cst.value.try_into().expect("vst lifting failure");
+                    let _fn_vst: vst::Fn = fn_vst_result.expect("shouldn't have been an Error at this point"); //fn_cst.value.try_into().expect("vst lifting failure");
                     //dbg!(&fn_vst.name);
 
                     // TODO: use the source-level proof rewrite