Merge pull request #913 from xldenis/cdsat-final

CDSAT specifications
creusot-rs · Dec 5, 2023 · c39918f · c39918f
2 parents 9203a59 + 5646d67
commit c39918f
Show file tree

Hide file tree

Showing 15 changed files with 53 additions and 29 deletions.
diff --git a/creusot-contracts-proc/src/pretyping.rs b/creusot-contracts-proc/src/pretyping.rs
@@ -1,6 +1,6 @@
 use pearlite_syn::Term as RT;
 use proc_macro2::{Delimiter, Group, Span, TokenStream, TokenTree};
-use syn::{spanned::Spanned, ExprMacro, Macro, Pat};
+use syn::{spanned::Spanned, ExprMacro, Pat};
 
 use pearlite_syn::term::*;
 use quote::{quote, quote_spanned, ToTokens};
@@ -34,10 +34,16 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
         // it's impossible to handle proc macros whose parameters is not valid pearlite syntax,
         // or we don't translate parameters, but then we let the user write non-pearlite code
         // in pearlite...
-        RT::Macro(ExprMacro { mac: Macro { path, .. }, .. }) if path.is_ident("proof_assert") => {
-            Ok(term.to_token_stream())
+        RT::Macro(ExprMacro { mac, .. }) => {
+            if mac.path.is_ident("proof_assert") || mac.path.is_ident("pearlite") {
+                Ok(term.to_token_stream())
+            } else {
+                Err(EncodeError::Unsupported(
+                    term.span(),
+                    "Macros other than pearlite! or proof_assert! are unsupported".into(),
+                ))
+            }
         }
-        RT::Macro(_) => Err(EncodeError::Unsupported(term.span(), "Macro".into())),
         RT::Array(_) => Err(EncodeError::Unsupported(term.span(), "Array".into())),
         RT::Binary(TermBinary { left, op, right }) => {
             let mut left = left;

diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs
@@ -154,7 +154,7 @@ impl<T> Seq<&T> {
     #[open]
     #[trusted]
     #[creusot::builtins = "prelude.Seq.to_owned"]
-    pub fn to_owned(self) -> Seq<T> {
+    pub fn to_owned_seq(self) -> Seq<T> {
         pearlite! {absurd}
     }
 }

diff --git a/creusot-contracts/src/num_rational.rs b/creusot-contracts/src/num_rational.rs
@@ -1,6 +1,6 @@
 use std::marker::PhantomData;
 
-use crate::{ghost, open, trusted, DeepModel, OrdLogic};
+use crate::{ghost, open, pearlite, trusted, DeepModel, Int, OrdLogic};
 use num_rational::BigRational;
 use std::cmp::Ordering;
 
@@ -20,6 +20,15 @@ impl DeepModel for BigRational {
     }
 }
 
+impl Real {
+    #[ghost]
+    #[trusted]
+    #[open(self)]
+    pub fn from_int(_: Int) -> Self {
+        pearlite! { absurd }
+    }
+}
+
 impl OrdLogic for Real {
     #[ghost]
     #[open]

diff --git a/creusot-contracts/src/std/cmp.rs b/creusot-contracts/src/std/cmp.rs
@@ -13,6 +13,12 @@ extern_spec! {
                 where
                     Self: DeepModel,
                     Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
+
+                #[ensures(result == (self.deep_model() != rhs.deep_model()))]
+                fn ne(&self, rhs: &Rhs) -> bool
+                where
+                    Self: DeepModel,
+                    Rhs: DeepModel<DeepModelTy = Self::DeepModelTy>;
             }
 
             // TODO: for now, we only support total orders

diff --git a/creusot/src/cleanup_spec_closures.rs b/creusot/src/cleanup_spec_closures.rs
@@ -85,7 +85,10 @@ impl<'tcx> MutVisitor<'tcx> for NoTranslateNoMoves<'tcx> {
                 {
                     substs.iter_mut().for_each(|p| {
                         if p.is_move() {
-                            self.unused.insert(p.place().unwrap().as_local().unwrap());
+                            let place = p.place().unwrap();
+                            if let Some(loc) = place.as_local() {
+                                self.unused.insert(loc);
+                            }
                         }
                     });
                     *substs = IndexVec::new();

diff --git a/creusot/tests/should_succeed/bdd.mlcfg b/creusot/tests/should_succeed/bdd.mlcfg
@@ -4013,7 +4013,7 @@ module Core_Cmp_Impls_Impl63_Cmp_Interface
   clone CreusotContracts_Logic_Ord_Impl3_CmpLog_Stub as CmpLog0
   clone CreusotContracts_Std1_Num_Impl10_DeepModel_Stub as DeepModel0
   val cmp (self : uint64) (other : uint64) : Core_Cmp_Ordering_Type.t_ordering
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 44 26 44 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
 
 end
 module CreusotContracts_Logic_Ord_Impl3_CmpLeLog_Stub

diff --git a/creusot/tests/should_succeed/bug/387.mlcfg b/creusot/tests/should_succeed/bug/387.mlcfg
@@ -215,11 +215,11 @@ module Core_Cmp_Ord_Max_Interface
   val max (self : self) (other : self) : self
     requires {Inv0.inv self}
     requires {Inv0.inv other}
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 47 26 47 66] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model self) }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 48 26 48 63] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model other) }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 7 0 56 1] result = self \/ result = other }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 50 16 50 79] LeLog0.le_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) -> result = other }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 51 16 51 81] LtLog0.lt_log (DeepModel0.deep_model other) (DeepModel0.deep_model self) -> result = self }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 53 26 53 66] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model self) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 54 26 54 63] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model other) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 7 0 62 1] result = self \/ result = other }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 56 16 56 79] LeLog0.le_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) -> result = other }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 57 16 57 81] LtLog0.lt_log (DeepModel0.deep_model other) (DeepModel0.deep_model self) -> result = self }
     ensures { Inv0.inv result }
 
 end

diff --git a/creusot/tests/should_succeed/heapsort_generic.mlcfg b/creusot/tests/should_succeed/heapsort_generic.mlcfg
@@ -1406,7 +1406,7 @@ module Core_Cmp_PartialOrd_Lt_Interface
   val lt (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 27 26 27 76] result = LtLog0.lt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 33 26 33 76] result = LtLog0.lt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module Core_Cmp_PartialOrd_Le_Interface
@@ -1430,7 +1430,7 @@ module Core_Cmp_PartialOrd_Le_Interface
   val le (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 30 26 30 77] result = LeLog0.le_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77] result = LeLog0.le_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module CreusotContracts_Std1_Slice_Impl0_ShallowModel_Stub

diff --git a/creusot/tests/should_succeed/instant.mlcfg b/creusot/tests/should_succeed/instant.mlcfg
@@ -323,7 +323,7 @@ module Core_Cmp_PartialOrd_Ge_Interface
   val ge (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77] result = GeLog0.ge_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 42 26 42 77] result = GeLog0.ge_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module CreusotContracts_Std1_Option_Impl0_DeepModel_Stub
@@ -629,7 +629,7 @@ module Core_Cmp_PartialOrd_Gt_Interface
   val gt (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 33 26 33 76] result = GtLog0.gt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 39 26 39 76] result = GtLog0.gt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module Std_Time_Impl0_DurationSince_Interface

diff --git a/creusot/tests/should_succeed/ord_trait.mlcfg b/creusot/tests/should_succeed/ord_trait.mlcfg
@@ -166,7 +166,7 @@ module Core_Cmp_Impls_Impl10_Le_Interface
   val le (self : a) (other : b) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 30 26 30 77] result = LeLog0.le_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77] result = LeLog0.le_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module TyInv_Trivial
@@ -803,7 +803,7 @@ module Core_Cmp_Impls_Impl10_Ge_Interface
   val ge (self : a) (other : b) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77] result = GeLog0.ge_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 42 26 42 77] result = GeLog0.ge_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module OrdTrait_GtOrLe_Interface

diff --git a/creusot/tests/should_succeed/red_black_tree.mlcfg b/creusot/tests/should_succeed/red_black_tree.mlcfg
@@ -6239,7 +6239,7 @@ module Core_Cmp_Ord_Cmp_Interface
   val cmp (self : self) (other : self) : Core_Cmp_Ordering_Type.t_ordering
     requires {Inv0.inv self}
     requires {Inv0.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 44 26 44 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
 
 end
 module RedBlackTree_Impl15_InsertRec_Interface

diff --git a/creusot/tests/should_succeed/selection_sort_generic.mlcfg b/creusot/tests/should_succeed/selection_sort_generic.mlcfg
@@ -1051,7 +1051,7 @@ module Core_Cmp_PartialOrd_Lt_Interface
   val lt (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 27 26 27 76] result = LtLog0.lt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../creusot-contracts/src/std/cmp.rs" 33 26 33 76] result = LtLog0.lt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module CreusotContracts_Std1_Slice_Impl0_ShallowModel_Stub

diff --git a/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg b/creusot/tests/should_succeed/syntax/10_mutual_rec_types.mlcfg
@@ -215,11 +215,11 @@ module Core_Cmp_Ord_Max_Interface
   val max (self : self) (other : self) : self
     requires {Inv0.inv self}
     requires {Inv0.inv other}
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 47 26 47 66] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model self) }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 48 26 48 63] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model other) }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 7 0 56 1] result = self \/ result = other }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 50 16 50 79] LeLog0.le_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) -> result = other }
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 51 16 51 81] LtLog0.lt_log (DeepModel0.deep_model other) (DeepModel0.deep_model self) -> result = self }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 53 26 53 66] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model self) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 54 26 54 63] GeLog0.ge_log (DeepModel0.deep_model result) (DeepModel0.deep_model other) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 7 0 62 1] result = self \/ result = other }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 56 16 56 79] LeLog0.le_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) -> result = other }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 57 16 57 81] LtLog0.lt_log (DeepModel0.deep_model other) (DeepModel0.deep_model self) -> result = self }
     ensures { Inv0.inv result }
 
 end

diff --git a/creusot/tests/should_succeed/vector/02_gnome.mlcfg b/creusot/tests/should_succeed/vector/02_gnome.mlcfg
@@ -805,7 +805,7 @@ module Core_Cmp_PartialOrd_Le_Interface
   val le (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 30 26 30 77] result = LeLog0.le_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 36 26 36 77] result = LeLog0.le_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module CreusotContracts_Std1_Slice_Impl0_ShallowModel_Stub

diff --git a/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg b/creusot/tests/should_succeed/vector/05_binary_search_generic.mlcfg
@@ -480,7 +480,7 @@ module Core_Cmp_Ord_Cmp_Interface
   val cmp (self : self) (other : self) : Core_Cmp_Ordering_Type.t_ordering
     requires {Inv0.inv self}
     requires {Inv0.inv other}
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 44 26 44 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 50 26 50 85] result = CmpLog0.cmp_log (DeepModel0.deep_model self) (DeepModel0.deep_model other) }
 
 end
 module CreusotContracts_Logic_Ord_OrdLogic_GtLog_Stub
@@ -526,7 +526,7 @@ module Core_Cmp_PartialOrd_Gt_Interface
   val gt (self : self) (other : rhs) : bool
     requires {Inv0.inv self}
     requires {Inv1.inv other}
-    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 33 26 33 76] result = GtLog0.gt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
+    ensures { [#"../../../../../creusot-contracts/src/std/cmp.rs" 39 26 39 76] result = GtLog0.gt_log (DeepModel0.deep_model self) (DeepModel1.deep_model other) }
 
 end
 module CreusotContracts_Std1_Vec_Impl0_ShallowModel_Stub