Merge pull request #898 from dewert99/trigger

simple_triggers option that adds triggers to def and spec axioms
creusot-rs · Oct 24, 2023 · 71e33aa · 71e33aa
2 parents 385d5ff + 45fced7
commit 71e33aa
Show file tree

Hide file tree

Showing 37 changed files with 2,392 additions and 819 deletions.
diff --git a/cargo-creusot/src/options.rs b/cargo-creusot/src/options.rs
@@ -32,6 +32,9 @@ pub struct CreusotArgs {
     /// Check the installed why3 version.
     #[clap(long, default_value_t = true, action = clap::ArgAction::Set)]
     pub check_why3: bool,
+    /// Use `result` as the trigger of definition and specification axioms of logic/ghost/predicate functions
+    #[clap(long, default_value_t = false, action = clap::ArgAction::Set)]
+    pub simple_triggers: bool,
 }
 
 /// Parse a single key-value pair

diff --git a/creusot-contracts-proc/src/lib.rs b/creusot-contracts-proc/src/lib.rs
@@ -543,7 +543,8 @@ pub fn law(_: TS1, tokens: TS1) -> TS1 {
     let tokens = TokenStream::from(tokens);
     TS1::from(quote! {
         #[creusot::decl::law]
-        #[::creusot_contracts::ghost]
+        #[creusot::decl::no_trigger]
+        #[::creusot_contracts::logic]
         #tokens
     })
 }

diff --git a/creusot-contracts/src/logic.rs b/creusot-contracts/src/logic.rs
@@ -5,7 +5,7 @@ mod fset;
 mod int;
 mod mapping;
 mod ops;
-mod ord;
+pub mod ord;
 mod seq;
 mod set;
 

diff --git a/creusot-contracts/src/logic/ord.rs b/creusot-contracts/src/logic/ord.rs
@@ -70,6 +70,67 @@ pub trait OrdLogic {
     fn eq_cmp(x: Self, y: Self);
 }
 
+#[macro_export]
+macro_rules! ord_laws_impl {
+    () => {
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_le_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_lt_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_ge_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn cmp_gt_log(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn refl(_: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn trans(_: Self, _: Self, _: Self, _: Ordering) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn antisym1(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn antisym2(_: Self, _: Self) {
+            ()
+        }
+
+        #[::creusot_contracts::law]
+        #[::creusot_contracts::open(self)]
+        fn eq_cmp(_: Self, _: Self) {
+            ()
+        }
+    };
+}
+
+pub use ord_laws_impl;
+
 macro_rules! ord_logic_impl {
     ($t:ty) => {
         impl OrdLogic for $t {
@@ -117,59 +178,7 @@ macro_rules! ord_logic_impl {
                 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) {
-                ()
-            }
+            ord_laws_impl! {}
         }
     };
 }
@@ -202,41 +211,7 @@ impl OrdLogic for bool {
         }
     }
 
-    #[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) {}
+    ord_laws_impl! {}
 }
 
 impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
@@ -259,59 +234,25 @@ impl<A: OrdLogic, B: OrdLogic> OrdLogic for (A, B) {
         pearlite! { (self.0 == o.0 && self.1 <= o.1) || self.0 <= o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_le_log(_: Self, _: Self) {}
-
     #[ghost]
     #[open]
     fn lt_log(self, o: Self) -> bool {
         pearlite! { (self.0 == o.0 && self.1 < o.1) || self.0 < o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_lt_log(_: Self, _: Self) {}
-
     #[ghost]
     #[open]
     fn ge_log(self, o: Self) -> bool {
         pearlite! { (self.0 == o.0 && self.1 >= o.1) || self.0 >= o.0 }
     }
 
-    #[ghost]
-    #[open(self)]
-    fn cmp_ge_log(_: Self, _: Self) {}
-
     #[ghost]
     #[open]
     fn gt_log(self, o: Self) -> bool {
         pearlite! { (self.0 == o.0 && self.1 > o.1) || self.0 > o.0 }
     }
 
-    #[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) {}
+    ord_laws_impl! {}
 }
 
 impl<T: OrdLogic> OrdLogic for Option<T> {
@@ -326,52 +267,5 @@ impl<T: OrdLogic> OrdLogic for Option<T> {
         }
     }
 
-    #[law]
-    #[open(self)]
-    #[ensures(x.le_log(y) == (x.cmp_log(y) != Ordering::Greater))]
-    fn cmp_le_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.lt_log(y) == (x.cmp_log(y) == Ordering::Less))]
-    fn cmp_lt_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.ge_log(y) == (x.cmp_log(y) != Ordering::Less))]
-    fn cmp_ge_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.gt_log(y) == (x.cmp_log(y) == Ordering::Greater))]
-    fn cmp_gt_log(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures(x.cmp_log(x) == Ordering::Equal)]
-    fn refl(x: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[requires(x.cmp_log(y) == o)]
-    #[requires(y.cmp_log(z) == o)]
-    #[ensures(x.cmp_log(z) == o)]
-    fn trans(x: Self, y: Self, z: Self, o: Ordering) {}
-
-    #[law]
-    #[open(self)]
-    #[requires(x.cmp_log(y) == Ordering::Less)]
-    #[ensures(y.cmp_log(x) == Ordering::Greater)]
-    fn antisym1(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[requires(x.cmp_log(y) == Ordering::Greater)]
-    #[ensures(y.cmp_log(x) == Ordering::Less)]
-    fn antisym2(x: Self, y: Self) {}
-
-    #[law]
-    #[open(self)]
-    #[ensures((x == y) == (x.cmp_log(y) == Ordering::Equal))]
-    fn eq_cmp(x: Self, y: Self) {}
+    ord_laws_impl! {}
 }
diff --git a/creusot-contracts/src/num_rational.rs b/creusot-contracts/src/num_rational.rs
@@ -65,57 +65,5 @@ impl OrdLogic for Real {
         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) {
-        ()
-    }
+    crate::logic::ord::ord_laws_impl! {}
 }
diff --git a/creusot-rustc/src/options.rs b/creusot-rustc/src/options.rs
@@ -35,6 +35,9 @@ pub struct CreusotArgs {
     /// Check the installed why3 version.
     #[clap(long, default_value_t = true, action = clap::ArgAction::Set)]
     pub check_why3: bool,
+    /// uses `result` as the trigger of definition and specification axioms of logic/ghost/predicate functions
+    #[clap(long, default_value_t = false, action = clap::ArgAction::Set)]
+    pub simple_triggers: bool,
 }
 
 /// Parse a single key-value pair
@@ -93,6 +96,7 @@ impl CreusotArgs {
             in_cargo: cargo_creusot,
             span_mode: span_mode,
             match_str: self.focus_on,
+            simple_triggers: self.simple_triggers,
         }
     }
 }