Merge pull request #859 from xldenis/cdsat-final

Author: xldenis

.vscode/settings.json

@@ -1,3 +1,7 @@
 {
     "rust-analyzer.rustc.source": "discover",
+    "rust-analyzer.diagnostics.disabled": [
+      "unresolved-proc-macro",
+      "unresolved-extern-crate"
+    ]
 }

Cargo.lock

@@ -2,22 +2,14 @@
 
 *Le marteau-pilon, forges et aciéries de Saint-Chamond, Joseph-Fortuné LAYRAUD, 1889*
 
-----
-
-📢 Are you interested in verifying Rust code? Don't know where to start? Please contact me, I'm always looking for case-studies. 📢
-
-----
-
 # About
 
-**Creusot** is a tool for *deductive verification* of Rust code. It allows you to annotate your code with specifications, invariants and assertions and then *verify* them formally and automatically, *proving*, mathematically, that your code satisfies your specifications.
+**Creusot** is a *deductive verifier* for Rust code. It verifies your code is safe from panics, overflows, and assertion failures. By adding annotations you can take it further and verify your code does the *correct* thing.
 
 Creusot works by translating Rust code to WhyML, the verification and specification language of [Why3](https://why3.lri.fr). Users can then leverage the full power of Why3 to (semi)-automatically discharge the verification conditions!
 
 See [ARCHITECTURE.md](ARCHITECTURE.md) for technical details.
 
-:warning: This is _research_ software, and favors _progress_ over stability :warning:
-
 ## Citing Creusot
 
 If you would like to cite Creusot in academic contexts, we encourage you to use our [ICFEM'22 publication](https://hal.inria.fr/hal-03737878/file/main.pdf).

README.md

@@ -9,7 +9,7 @@ edition = "2018"
 [dependencies]
 creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "*" }
 creusot-contracts-dummy = { path = "../creusot-contracts-dummy", version = "*" }
-
+num-rational = "0.3.2"
 
 [features]
 default = []

creusot-contracts/Cargo.toml

@@ -166,6 +166,9 @@ pub mod logic;
 #[cfg_attr(not(creusot), allow(unused))]
 pub mod std;
 
+#[cfg(creusot)]
+pub mod num_rational;
+
 #[cfg(creusot)]
 pub mod ghost;
 

creusot-contracts/src/lib.rs

@@ -190,6 +190,55 @@ ord_logic_impl!(i64);
 ord_logic_impl!(i128);
 ord_logic_impl!(isize);
 
+impl OrdLogic for bool {
+    #[open]
+    #[ghost]
+    fn cmp_log(self, o: Self) -> Ordering {
+        match (self, o) {
+            (false, false) => Ordering::Equal,
+            (true, true) => Ordering::Equal,
+            (false, true) => Ordering::Less,
+            (true, false) => Ordering::Greater,
+        }
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_le_log(_: Self, _: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_lt_log(_: Self, _: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_ge_log(_: Self, _: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_gt_log(_: Self, _: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn refl(_: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn trans(_: Self, _: Self, _: Self, _: Ordering) {}
+
+    #[ghost]
+    #[open(self)]
+    fn antisym1(_: Self, _: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn antisym2(_: Self, _: Self) {}
+
+    #[ghost]
+    #[open(self)]
+    fn eq_cmp(_: Self, _: Self) {}
+}
+
 impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
     #[ghost]
     #[open]

creusot-contracts/src/logic/ord.rs

@@ -144,6 +144,16 @@ impl<T> Seq<T> {
     }
 }
 
+impl<T> Seq<&T> {
+    #[logic]
+    #[open]
+    #[trusted]
+    #[creusot::builtins = "prelude.Seq.to_owned"]
+    pub fn to_owned(self) -> Seq<T> {
+        pearlite! {absurd}
+    }
+}
+
 impl<T> IndexLogic<Int> for Seq<T> {
     type Item = T;
 

creusot-contracts/src/logic/seq.rs

@@ -0,0 +1,121 @@
+use std::marker::PhantomData;
+
+use crate::{ghost, open, trusted, DeepModel, OrdLogic};
+use num_rational::BigRational;
+use std::cmp::Ordering;
+
+#[cfg_attr(creusot, creusot::builtins = "prelude.Real.real")]
+#[trusted]
+pub struct Real(PhantomData<*mut ()>);
+
+#[cfg(creusot)]
+impl DeepModel for BigRational {
+    type DeepModelTy = Real;
+
+    #[ghost]
+    #[open(self)]
+    #[trusted]
+    fn deep_model(self) -> Self::DeepModelTy {
+        absurd
+    }
+}
+
+impl OrdLogic for Real {
+    #[ghost]
+    #[open]
+    fn cmp_log(self, o: Self) -> Ordering {
+        if self < o {
+            Ordering::Less
+        } else if self == o {
+            Ordering::Equal
+        } else {
+            Ordering::Greater
+        }
+    }
+
+    #[trusted]
+    #[open]
+    #[ghost]
+    #[creusot::builtins = "prelude.Real.(<=)"]
+    fn le_log(self, _: Self) -> bool {
+        true
+    }
+
+    #[trusted]
+    #[open]
+    #[ghost]
+    #[creusot::builtins = "prelude.Real.(<)"]
+    fn lt_log(self, _: Self) -> bool {
+        true
+    }
+
+    #[trusted]
+    #[open]
+    #[ghost]
+    #[creusot::builtins = "prelude.Real.(>=)"]
+    fn ge_log(self, _: Self) -> bool {
+        true
+    }
+
+    #[trusted]
+    #[open]
+    #[ghost]
+    #[creusot::builtins = "prelude.Real.(>)"]
+    fn gt_log(self, _: Self) -> bool {
+        true
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_le_log(_: Self, _: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_lt_log(_: Self, _: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_ge_log(_: Self, _: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn cmp_gt_log(_: Self, _: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn refl(_: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn trans(_: Self, _: Self, _: Self, _: Ordering) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn antisym1(_: Self, _: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn antisym2(_: Self, _: Self) {
+        ()
+    }
+
+    #[ghost]
+    #[open(self)]
+    fn eq_cmp(_: Self, _: Self) {
+        ()
+    }
+}

creusot-contracts/src/num_rational.rs

@@ -162,7 +162,7 @@ fn body_module<'tcx>(ctx: &mut Why3Generator<'tcx>, def_id: DefId) -> (Module, C
         let term = ctx.term(def_id).unwrap().clone();
         let body = lower_pure(ctx, &mut names, term);
 
-        if sig_contract.contract.variant.is_empty() {
+        if sig_contract.contract.variant.is_empty() && body.is_pure() {
             let decl = match util::item_type(ctx.tcx, def_id) {
                 ItemType::Ghost | ItemType::Logic => Decl::LogicDefn(Logic { sig, body }),
                 ItemType::Predicate => Decl::PredDecl(Predicate { sig, body }),

creusot/src/backend/logic.rs

@@ -260,6 +260,18 @@ impl<'tcx> Lower<'_, 'tcx> {
                     ("final".into(), self.lower_term(*fin)),
                 ],
             },
+            TermKind::Assert { cond } => {
+                let cond = self.lower_term(*cond);
+                if self.pure == Purity::Program && !cond.is_pure() {
+                    Exp::Let {
+                        pattern: Pat::VarP("a".into()),
+                        arg: Box::new(cond),
+                        body: Box::new(Exp::Assert(Box::new(Exp::impure_var("a".into())))),
+                    }
+                } else {
+                    Exp::Assert(Box::new(cond))
+                }
+            }
         }
     }