Merge pull request #1281 from arnaudgolfouse/int-ghost-methods

`Int` ghost methods

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, Pat};
+use syn::{spanned::Spanned, ExprMacro, Pat, UnOp};
 
 use pearlite_syn::term::*;
 use quote::{quote, quote_spanned, ToTokens};
@@ -50,14 +50,27 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
             let mut right = right;
 
             use syn::BinOp::*;
-            if matches!(op, Eq(_) | Ne(_) | Ge(_) | Le(_) | Gt(_) | Lt(_)) {
+            if matches!(
+                op,
+                Eq(_)
+                    | Ne(_)
+                    | Ge(_)
+                    | Le(_)
+                    | Gt(_)
+                    | Lt(_)
+                    | Add(_)
+                    | Sub(_)
+                    | Mul(_)
+                    | Div(_)
+                    | Rem(_)
+            ) {
                 left = match &**left {
-                    RT::Paren(TermParen { expr, .. }) => &expr,
-                    _ => &*left,
+                    RT::Paren(TermParen { expr, .. }) => expr,
+                    _ => left,
                 };
                 right = match &**right {
-                    RT::Paren(TermParen { expr, .. }) => &expr,
-                    _ => &*right,
+                    RT::Paren(TermParen { expr, .. }) => expr,
+                    _ => right,
                 };
             }
 
@@ -82,6 +95,21 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
                 Gt(_) => Ok(
                     quote_spanned! {sp=> ::creusot_contracts::logic::OrdLogic::gt_log(#left, #right) },
                 ),
+                Add(_) => Ok(
+                    quote_spanned! {sp=> ::creusot_contracts::logic::ops::AddLogic::add(#left, #right) },
+                ),
+                Sub(_) => Ok(
+                    quote_spanned! {sp=> ::creusot_contracts::logic::ops::SubLogic::sub(#left, #right) },
+                ),
+                Mul(_) => Ok(
+                    quote_spanned! {sp=> ::creusot_contracts::logic::ops::MulLogic::mul(#left, #right) },
+                ),
+                Div(_) => Ok(
+                    quote_spanned! {sp=> ::creusot_contracts::logic::ops::DivLogic::div(#left, #right) },
+                ),
+                Rem(_) => Ok(
+                    quote_spanned! {sp=> ::creusot_contracts::logic::ops::RemLogic::rem(#left, #right) },
+                ),
                 _ => Ok(quote_spanned! {sp=> #left #op #right }),
             }
         }
@@ -209,9 +237,13 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
         RT::Type(ty) => Ok(quote_spanned! {sp=> #ty }),
         RT::Unary(TermUnary { op, expr }) => {
             let term = encode_term(expr)?;
-            Ok(quote_spanned! {sp=>
-                #op #term
-            })
+            if matches!(op, UnOp::Neg(_)) {
+                Ok(quote_spanned! {sp=> ::creusot_contracts::logic::ops::NegLogic::neg(#term) })
+            } else {
+                Ok(quote_spanned! {sp=>
+                    #op #term
+                })
+            }
         }
         RT::Final(TermFinal { term, .. }) => {
             let term = encode_term(term)?;
@@ -253,7 +285,7 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
         }
         RT::Quant(TermQuant { quant_token, args, trigger, term, .. }) => {
             let mut ts = encode_term(term)?;
-            ts = encode_trigger(&trigger, ts)?;
+            ts = encode_trigger(trigger, ts)?;
             ts = quote_spanned! {sp=>
                 ::creusot_contracts::__stubs::#quant_token(
                     #[creusot::no_translate]
@@ -267,7 +299,7 @@ pub fn encode_term(term: &RT) -> Result<TokenStream, EncodeError> {
         RT::Closure(clos) => {
             let inputs = &clos.inputs;
             let retty = &clos.output;
-            let clos = encode_term(&*clos.body)?;
+            let clos = encode_term(&clos.body)?;
 
             Ok(
                 quote_spanned! {sp=> ::creusot_contracts::__stubs::mapping_from_fn(#[creusot::no_translate] |#inputs| #retty #clos)},
@@ -293,7 +325,7 @@ fn encode_trigger(
     Ok(ts)
 }
 
-pub fn encode_block(block: &Vec<TermStmt>) -> Result<TokenStream, EncodeError> {
+pub fn encode_block(block: &[TermStmt]) -> Result<TokenStream, EncodeError> {
     let stmts: Vec<_> = block.iter().map(encode_stmt).collect::<Result<_, _>>()?;
     Ok(quote! { { #(#stmts)* } })
 }

creusot-contracts/src/lib.rs

@@ -397,7 +397,7 @@ pub mod well_founded;
 mod base_prelude {
     pub use crate::{
         ghost::GhostBox,
-        logic::{IndexLogic as _, Int, OrdLogic, Seq},
+        logic::{ops::IndexLogic as _, Int, OrdLogic, Seq},
         model::{DeepModel, View},
         resolve::*,
         snapshot::Snapshot,

creusot-contracts/src/logic.rs

@@ -8,7 +8,7 @@ mod fmap;
 mod fset;
 mod int;
 mod mapping;
-mod ops;
+pub mod ops;
 pub mod ord;
 mod seq;
 mod set;
@@ -17,7 +17,6 @@ pub use fmap::FMap;
 pub use fset::FSet;
 pub use int::Int;
 pub use mapping::Mapping;
-pub use ops::IndexLogic;
 pub use ord::OrdLogic;
 pub use seq::Seq;
 pub use set::Set;

creusot-contracts/src/logic/int.rs

@@ -1,4 +1,5 @@
 use crate::{
+    logic::ops::{AddLogic, DivLogic, MulLogic, NegLogic, RemLogic, SubLogic},
     std::ops::{Add, Div, Mul, Neg, Rem, Sub},
     *,
 };
@@ -58,8 +59,8 @@ impl Int {
     #[pure]
     #[ensures(*result == value@)]
     #[allow(unreachable_code)]
+    #[allow(unused_variables)]
     pub fn new(value: i128) -> GhostBox<Self> {
-        let _ = value;
         ghost!(panic!())
     }
 
@@ -74,8 +75,8 @@ impl Int {
     #[trusted]
     #[logic]
     #[creusot::builtins = "int.Power.power"]
+    #[allow(unused_variables)]
     pub fn pow(self, p: Int) -> Int {
-        let _ = p;
         dead
     }
 
@@ -90,8 +91,8 @@ impl Int {
     #[trusted]
     #[logic]
     #[creusot::builtins = "int.MinMax.max"]
+    #[allow(unused_variables)]
     pub fn max(self, x: Int) -> Int {
-        let _ = x;
         dead
     }
 
@@ -106,8 +107,8 @@ impl Int {
     #[logic]
     #[creusot::builtins = "int.MinMax.min"]
     #[trusted]
+    #[allow(unused_variables)]
     pub fn min(self, x: Int) -> Int {
-        let _ = x;
         dead
     }
 
@@ -122,8 +123,8 @@ impl Int {
     #[trusted]
     #[logic]
     #[creusot::builtins = "int.EuclideanDivision.div"]
+    #[allow(unused_variables)]
     pub fn div_euclid(self, d: Int) -> Int {
-        let _ = d;
         dead
     }
 
@@ -138,8 +139,8 @@ impl Int {
     #[trusted]
     #[logic]
     #[creusot::builtins = "int.EuclideanDivision.mod"]
+    #[allow(unused_variables)]
     pub fn rem_euclid(self, d: Int) -> Int {
-        let _ = d;
         dead
     }
 
@@ -164,68 +165,150 @@ impl Int {
     }
 }
 
-#[cfg(creusot)]
-impl Add<Int> for Int {
-    type Output = Int;
+impl AddLogic for Int {
+    type Output = Self;
+    #[logic]
     #[trusted]
     #[creusot::no_translate]
     #[creusot::builtins = "add_int"]
-    fn add(self, _: Int) -> Self {
-        panic!()
+    #[allow(unused_variables)]
+    fn add(self, other: Self) -> Self {
+        dead
     }
 }
 
-#[cfg(creusot)]
-impl Sub<Int> for Int {
-    type Output = Int;
+impl SubLogic for Int {
+    type Output = Self;
+    #[logic]
     #[trusted]
     #[creusot::no_translate]
     #[creusot::builtins = "sub_int"]
-    fn sub(self, _: Int) -> Self {
-        panic!()
+    #[allow(unused_variables)]
+    fn sub(self, other: Self) -> Self {
+        dead
     }
 }
 
-#[cfg(creusot)]
-impl Mul<Int> for Int {
-    type Output = Int;
+impl MulLogic for Int {
+    type Output = Self;
+    #[logic]
     #[trusted]
     #[creusot::no_translate]
     #[creusot::builtins = "mul_int"]
-    fn mul(self, _: Int) -> Self {
-        panic!()
+    #[allow(unused_variables)]
+    fn mul(self, other: Self) -> Self {
+        dead
     }
 }
 
-#[cfg(creusot)]
-impl Div<Int> for Int {
-    type Output = Int;
+impl DivLogic for Int {
+    type Output = Self;
+    #[logic]
     #[trusted]
     #[creusot::no_translate]
     #[creusot::builtins = "div_int"]
-    fn div(self, _: Int) -> Self {
-        panic!()
+    #[allow(unused_variables)]
+    fn div(self, other: Self) -> Self {
+        dead
     }
 }
 
-#[cfg(creusot)]
-impl Rem<Int> for Int {
-    type Output = Int;
+impl RemLogic for Int {
+    type Output = Self;
+    #[logic]
     #[trusted]
     #[creusot::no_translate]
     #[creusot::builtins = "rem_int"]
-    fn rem(self, _: Int) -> Self {
-        panic!()
+    #[allow(unused_variables)]
+    fn rem(self, other: Self) -> Self {
+        dead
     }
 }
 
-#[cfg(creusot)]
-impl Neg for Int {
-    type Output = Int;
+impl NegLogic for Int {
+    type Output = Self;
+    #[logic]
     #[trusted]
     #[creusot::no_translate]
     #[creusot::builtins = "neg_int"]
     fn neg(self) -> Self {
-        panic!()
+        dead
+    }
+}
+
+// ========== Ghost operations =============
+
+impl PartialEq for Int {
+    #[trusted]
+    #[pure]
+    #[ensures(result == (*self == *other))]
+    #[allow(unused_variables)]
+    fn eq(&self, other: &Self) -> bool {
+        unreachable!("BUG: called ghost function in normal code")
+    }
+}
+
+impl Add for Int {
+    type Output = Int;
+    #[trusted]
+    #[pure]
+    #[ensures(result == self + other)]
+    #[allow(unused_variables)]
+    fn add(self, other: Int) -> Self {
+        unreachable!("BUG: called ghost function in normal code")
+    }
+}
+
+impl Sub for Int {
+    type Output = Int;
+    #[trusted]
+    #[pure]
+    #[ensures(result == self - other)]
+    #[allow(unused_variables)]
+    fn sub(self, other: Int) -> Self {
+        unreachable!("BUG: called ghost function in normal code")
+    }
+}
+
+impl Mul for Int {
+    type Output = Int;
+    #[trusted]
+    #[pure]
+    #[ensures(result == self * other)]
+    #[allow(unused_variables)]
+    fn mul(self, other: Int) -> Self {
+        unreachable!("BUG: called ghost function in normal code")
+    }
+}
+
+impl Div for Int {
+    type Output = Int;
+    #[trusted]
+    #[pure]
+    #[ensures(result == self / other)]
+    #[allow(unused_variables)]
+    fn div(self, other: Int) -> Self {
+        unreachable!("BUG: called ghost function in normal code")
+    }
+}
+
+impl Rem for Int {
+    type Output = Int;
+    #[trusted]
+    #[pure]
+    #[ensures(result == self % other)]
+    #[allow(unused_variables)]
+    fn rem(self, other: Int) -> Self {
+        unreachable!("BUG: called ghost function in normal code")
+    }
+}
+
+impl Neg for Int {
+    type Output = Int;
+    #[trusted]
+    #[pure]
+    #[ensures(result == -self)]
+    fn neg(self) -> Self {
+        unreachable!("BUG: called ghost function in normal code")
     }
 }