Try Bitwise

creusot-contracts/Cargo.toml

@@ -13,6 +13,7 @@ description = "Provides contracts and logic helpers for Creusot"
 creusot-contracts-proc = { path = "../creusot-contracts-proc", version = "0.3.0" }
 creusot-contracts-dummy = { path = "../creusot-contracts-dummy", version = "0.3.0" }
 num-rational = "0.3.2"
+paste = "1.0"
 
 [features]
 default = []

creusot-contracts/src/logic/ord.rs

@@ -127,7 +127,7 @@ macro_rules! ord_laws_impl {
 pub use ord_laws_impl;
 
 macro_rules! ord_logic_impl {
-    ($t:ty) => {
+    ($t:ty, $module:literal) => {
         impl OrdLogic for $t {
             #[logic]
             #[open]
@@ -150,7 +150,8 @@ macro_rules! ord_logic_impl {
 
             #[trusted]
             #[logic]
-            #[creusot::builtins = "int.Int.(<)"]
+            // #[creusot::builtins = "int.Int.(<)"]
+            #[creusot::builtins = concat!($module, ".(<)")]
             fn lt_log(self, _: Self) -> bool {
                 dead
             }
@@ -174,21 +175,98 @@ macro_rules! ord_logic_impl {
     };
 }
 
-ord_logic_impl!(Int);
-
-ord_logic_impl!(u8);
-ord_logic_impl!(u16);
-ord_logic_impl!(u32);
-ord_logic_impl!(u64);
-ord_logic_impl!(u128);
-ord_logic_impl!(usize);
-
-ord_logic_impl!(i8);
-ord_logic_impl!(i16);
-ord_logic_impl!(i32);
-ord_logic_impl!(i64);
-ord_logic_impl!(i128);
-ord_logic_impl!(isize);
+// laurent voir si on garde  ord_logic_impl_with_signed et ord_logic_impl_with_signed_symbol.
+macro_rules! ord_logic_impl_with_signed_symbol {
+    ($t:ty, $module:literal, $signed_sym:expr) => {
+        impl OrdLogic for $t {
+            #[logic]
+            #[open]
+            fn cmp_log(self, o: Self) -> Ordering {
+                if self < o {
+                    Ordering::Less
+                } else if self == o {
+                    Ordering::Equal
+                } else {
+                    Ordering::Greater
+                }
+            }
+
+            #[trusted]
+            #[open]
+            #[logic]
+            #[creusot::builtins = concat!($module, ".", $signed_sym, "le")]
+            fn le_log(self, _: Self) -> bool {
+                true
+            }
+
+            #[trusted]
+            #[open]
+            #[logic]
+            #[creusot::builtins = concat!($module, ".", $signed_sym, "lt")]
+            fn lt_log(self, _: Self) -> bool {
+                true
+            }
+
+            #[trusted]
+            #[open]
+            #[logic]
+            #[creusot::builtins = concat!($module, ".", $signed_sym, "ge")]
+            fn ge_log(self, _: Self) -> bool {
+                true
+            }
+
+            #[trusted]
+            #[open]
+            #[logic]
+            #[creusot::builtins = concat!($module, ".", $signed_sym, "gt")]
+            fn gt_log(self, _: Self) -> bool {
+                true
+            }
+
+            ord_laws_impl! {}
+        }
+    };
+}
+
+macro_rules! ord_logic_unsigned_impl {
+    ($t:ty, $module:literal) => {
+        ord_logic_impl_with_signed_symbol!($t, $module, "u");
+    }
+}
+
+
+macro_rules! ord_logic_signed_impl {
+    ($t:ty, $module:literal) => {
+        ord_logic_impl_with_signed_symbol!($t, $module, "s");
+    }
+}
+
+ord_logic_impl!(Int, "int.Int");
+
+ord_logic_unsigned_impl!(u8, "prelude.prelude.UInt8");
+ord_logic_unsigned_impl!(u16, "prelude.prelude.UInt16");
+ord_logic_unsigned_impl!(u32, "prelude.prelude.UInt32");
+ord_logic_unsigned_impl!(u64, "prelude.prelude.UInt64");
+ord_logic_unsigned_impl!(u128, "prelude.prelude.UInt128");
+#[cfg(target_pointer_width = "64")]
+ord_logic_unsigned_impl!(usize, "prelude.prelude.UInt64");
+#[cfg(target_pointer_width = "32")]
+ord_logic_unsigned_impl!(usize, "prelude.prelude.UInt32");
+#[cfg(target_pointer_width = "16")]
+ord_logic_unsigned_impl!(usize, "prelude.prelude.UInt16");
+
+
+ord_logic_signed_impl!(i8, "prelude.prelude.Int8");
+ord_logic_signed_impl!(i16, "prelude.prelude.Int16");
+ord_logic_signed_impl!(i32, "prelude.prelude.Int32");
+ord_logic_signed_impl!(i64, "prelude.prelude.Int64");
+ord_logic_signed_impl!(i128, "prelude.prelude.Int128");
+#[cfg(target_pointer_width = "64")]
+ord_logic_signed_impl!(isize, "prelude.prelude.Int64");
+#[cfg(target_pointer_width = "32")]
+ord_logic_signed_impl!(isize, "prelude.prelude.Int32");
+#[cfg(target_pointer_width = "16")]
+ord_logic_signed_impl!(isize, "prelude.prelude.Int16");
 
 impl OrdLogic for bool {
     #[open]

creusot-contracts/src/std/array.rs

@@ -13,9 +13,34 @@ impl<T, const N: usize> Invariant for [T; N] {
 impl<T, const N: usize> View for [T; N] {
     type ViewTy = Seq<T>;
 
+    //TODO laurent valider l'approche de separation en 3 block
+
+    #[cfg(target_pointer_width = "64")]
     #[logic]
     #[trusted]
-    #[creusot::builtins = "prelude.prelude.Slice.id"]
+    #[creusot::builtins = "prelude.prelude.Slice64.id"]
+    // TODO:
+    // #[ensures(result.len() == N@)]
+    // Warning: #[ensures] and #[trusted] are incompatible, so this might require
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+
+    #[cfg(target_pointer_width = "32")]
+    #[logic]
+    #[trusted]
+    #[creusot::builtins = "prelude.prelude.Slice32.id"]
+    // TODO:
+    // #[ensures(result.len() == N@)]
+    // Warning: #[ensures] and #[trusted] are incompatible, so this might require
+    fn view(self) -> Self::ViewTy {
+        dead
+    }
+
+    #[cfg(target_pointer_width = "16")]
+    #[logic]
+    #[trusted]
+    #[creusot::builtins = "prelude.prelude.Slice16.id"]
     // TODO:
     // #[ensures(result.len() == N@)]
     // Warning: #[ensures] and #[trusted] are incompatible, so this might require

creusot-contracts/src/std/num.rs

@@ -1,5 +1,6 @@
 use crate::{Default, *};
 pub use ::std::num::*;
+use paste::paste;
 
 macro_rules! mach_int {
     ($t:ty, $ty_nm:expr, $zero:expr) => {
@@ -32,19 +33,64 @@ macro_rules! mach_int {
     };
 }
 
-mach_int!(u8, "prelude.prelude.UInt8", 0u8);
-mach_int!(u16, "prelude.prelude.UInt16", 0u16);
-mach_int!(u32, "prelude.prelude.UInt32", 0u32);
-mach_int!(u64, "prelude.prelude.UInt64", 0u64);
-mach_int!(u128, "prelude.prelude.UInt128", 0u128);
-mach_int!(usize, "prelude.prelude.UIntSize", 0usize);
+macro_rules! mach_uint { // TODO laurent factoriser avec mach_int
+    ($t:ty, $ty_nm:expr, $zero:expr) => {
+        paste! {
+            impl View for $t {
+                type ViewTy = Int;
+                #[logic]
+                #[trusted]
+                #[creusot::builtins = $ty_nm ".t'int"] // TODO laurent: on ne génère pas ".to_int" pour les types non signé car on a besoin de la version non signée, or le clone substitue la
+                fn view(self) -> Self::ViewTy {
+                    dead
+                }
+            }
+
+            impl DeepModel for $t {
+                type DeepModelTy = Int;
+                #[logic]
+                #[open]
+                fn deep_model(self) -> Self::DeepModelTy {
+                    pearlite! { self@ }
+                }
+            }
+
+            impl Default for $t {
+                #[predicate]
+                #[open]
+                fn is_default(self) -> bool {
+                    pearlite! { self == $zero }
+                }
+            }
+        }
+    };
+}
+
+mach_uint!(u8, "prelude.prelude.UInt8", 0u8);
+mach_uint!(u16, "prelude.prelude.UInt16", 0u16);
+mach_uint!(u32, "prelude.prelude.UInt32", 0u32);
+mach_uint!(u64, "prelude.prelude.UInt64", 0u64);
+mach_uint!(u128, "prelude.prelude.UInt128", 0u128);
+// mach_int!(usize, "prelude.prelude.UIntSize.to_uint", 0usize);
+#[cfg(target_pointer_width = "64")]
+mach_uint!(usize, "prelude.prelude.UInt64", 0usize); // laurent voir si on garde 0usize
+#[cfg(target_pointer_width = "32")]
+mach_uint!(usize, "prelude.prelude.UInt64", 0usize); // laurent voir si on garde 0usize
+#[cfg(target_pointer_width = "16")]
+mach_uint!(usize, "prelude.prelude.UInt64", 0usize); // laurent voir si on garde 0usize
 
 mach_int!(i8, "prelude.prelude.Int8", 0i8);
 mach_int!(i16, "prelude.prelude.Int16", 0i16);
 mach_int!(i32, "prelude.prelude.Int32", 0i32);
 mach_int!(i64, "prelude.prelude.Int64", 0i64);
 mach_int!(i128, "prelude.prelude.Int128", 0i128);
-mach_int!(isize, "prelude.prelude.IntSize", 0isize);
+#[cfg(target_pointer_width = "64")]
+mach_int!(isize, "prelude.prelude.Int64", 0isize); // laurent voir si on garde 0isize
+#[cfg(target_pointer_width = "32")]
+mach_int!(isize, "prelude.prelude.Int64", 0isize); // laurent voir si on garde 0isize
+#[cfg(target_pointer_width = "16")]
+mach_int!(isize, "prelude.prelude.Int64", 0isize); // laurent voir si on garde 0isize
+
 
 /// Adds specifications for checked, wrapping, saturating, and overflowing operations on the given
 /// integer type

creusot-contracts/src/std/slice.rs

@@ -44,9 +44,27 @@ impl<T: DeepModel> DeepModel for [T] {
     }
 }
 
+//TODO laurent valider l'approche de separation en 3 block
+#[cfg(target_pointer_width = "64")]
 #[logic]
 #[trusted]
-#[creusot::builtins = "prelude.prelude.Slice.id"]
+#[creusot::builtins = "prelude.prelude.Slice64.id"]
+fn slice_model<T>(_: &[T]) -> Seq<T> {
+    dead
+}
+
+#[cfg(target_pointer_width = "32")]
+#[logic]
+#[trusted]
+#[creusot::builtins = "prelude.prelude.Slice32.id"]
+fn slice_model<T>(_: &[T]) -> Seq<T> {
+    dead
+}
+
+#[cfg(target_pointer_width = "16")]
+#[logic]
+#[trusted]
+#[creusot::builtins = "prelude.prelude.Slice16.id"]
 fn slice_model<T>(_: &[T]) -> Seq<T> {
     dead
 }

creusot-deps.opam

@@ -16,4 +16,4 @@ depends: [
 pin-depends: [
   [ "why3.git-ec97" "git+https://gitlab.inria.fr/why3/why3.git#ec97d9abc" ]
   [ "why3-ide.git-ec97" "git+https://gitlab.inria.fr/why3/why3.git#ec97d9abc" ]
-]
+]

creusot/Cargo.toml

@@ -24,14 +24,20 @@ serde_json = { version = "1.0" }
 lazy_static = "1.4.0"
 pathdiff = "0.2"
 
+[build-dependencies]
+paste = "1.0"
+indoc = "2.0.5"
+
 [dev-dependencies]
 regex = "1.10.5"
 glob = "*"
 assert_cmd = "1.0"
 similar = "2.2"
 termcolor = "1.1"
 arraydeque = "0.4"
-creusot-contracts = { path = "../creusot-contracts", features = ["typechecker"] }
+creusot-contracts = { path = "../creusot-contracts", features = [
+    "typechecker",
+] }
 escargot = { version = "0.5" }
 creusot-dev-config = { path = "../creusot-dev-config" }