Inline struct accessors to avoid Why3 polymorphism

cargo-creusot/src/why3_launcher.rs

@@ -49,9 +49,12 @@ impl Why3Launcher {
         std::fs::create_dir(&prelude_dir)?;
 
         PRELUDE
-            .extract(prelude_dir)
+            .extract(&prelude_dir)
             .expect("can't launch why3, could extract prelude into temp dir");
 
+        let mut conf_path = prelude_dir;
+        conf_path.push("creusot-why3.conf");
+
         let mut command =
             if let Some(p) = &self.why3_path { Command::new(p) } else { Command::new("why3") };
         command
@@ -63,7 +66,9 @@ impl Why3Launcher {
                 "-L",
             ])
             .arg(temp_dir.as_os_str())
-            .arg(&self.output_file);
+            .arg(&self.output_file)
+            .arg("--extra-config")
+            .arg(conf_path.as_os_str());
         if let Some(cfg) = &self.config_file {
             command.arg("-C").arg(cfg);
         }

creusot-contracts/src/logic/seq.rs

@@ -38,6 +38,15 @@ impl<T> Seq<T> {
         absurd
     }
 
+    /// Similar to [`Seq::subsequence`] but corresponds exactly to Z3's seq.extract
+    #[trusted]
+    #[logic]
+    #[open(self)]
+    #[creusot::builtins = "prelude.seq_ext.SeqExt.extract"]
+    pub fn extract(self, _: Int, _: Int) -> Self {
+        absurd
+    }
+
     #[trusted]
     #[logic]
     #[open(self)]
@@ -96,11 +105,27 @@ impl<T> Seq<T> {
     #[trusted]
     #[logic]
     #[open(self)]
-    #[creusot::builtins = "seq.Reverse.reverse"]
+    #[ensures(result.len() == self.len())]
     pub fn reverse(self) -> Self {
         absurd
     }
 
+    // #[trusted]
+    // #[law]
+    // #[open(self)]
+    // #[ensures(forall<s1: Self, s2: Self, i: Int>
+    //     0 <= i && i < s1.len() ==> s1.concat(s2)[i] == s1[i])]
+    // #[ensures(forall<s1: Self, s2: Self, i: Int>
+    //     s1.len() <= i && i < s1.len() + s2.len() ==> s1.concat(s2)[i] == s2[i - s1.len()])]
+    // #[ensures(forall<s: Self, offset: Int, len: Int, i: Int>
+    //     0 <= i && i < len && 0 <= len && 0 <= offset && (offset+len) <= s.len()
+    //         ==> s.extract(offset, len)[i] == s[offset+i])]
+    // #[ensures(forall<s1: Self, i: Int>
+    //     0 <= i && i < s1.len() ==> s1.reverse()[i] == s1[s1.len() - i - 1])]
+    // pub fn seq_lemmas() {
+    //     absurd
+    // }
+
     #[predicate]
     #[open]
     pub fn permutation_of(self, o: Self) -> bool {

creusot-contracts/src/snapshot.rs

@@ -1,7 +1,7 @@
 use crate::{std::ops::Deref, *};
 
 #[rustc_diagnostic_item = "snapshot_ty"]
-#[cfg_attr(creusot, creusot::builtins = "prelude.prelude.Snapshot.snap_ty")]
+#[trusted]
 pub struct Snapshot<T>(pub(crate) std::marker::PhantomData<T>)
 where
     T: ?Sized;
@@ -13,7 +13,6 @@ impl<T: ?Sized> Deref for Snapshot<T> {
     #[logic]
     #[open(self)]
     #[rustc_diagnostic_item = "snapshot_deref"]
-    #[creusot::builtins = "prelude.prelude.Snapshot.inner"]
     fn deref(&self) -> &Self::Target {
         pearlite! { absurd }
     }
@@ -41,21 +40,19 @@ impl<T: ?Sized> Snapshot<T> {
     #[trusted]
     #[logic]
     #[open(self)]
-    #[creusot::builtins = "prelude.prelude.Snapshot.new"]
+    #[ensures(&*result == &x)]
     #[rustc_diagnostic_item = "snapshot_new"]
-    pub fn new(_: T) -> Snapshot<T> {
+    pub fn new(x: T) -> Snapshot<T> {
         pearlite! { absurd }
     }
 
-    #[trusted]
     #[logic]
-    #[open(self)]
+    #[open]
     #[rustc_diagnostic_item = "snapshot_inner"]
-    #[creusot::builtins = "prelude.prelude.Snapshot.inner"]
     pub fn inner(self) -> T
     where
         T: Sized, // TODO: don't require T: Sized here. Problem: return type is T.
     {
-        pearlite! { absurd }
+        *self
     }
 }

creusot/src/backend/ty.rs

@@ -576,6 +576,7 @@ fn build_ty_decl<'tcx>(
     kind
 }
 use rustc_data_structures::captures::Captures;
+use why3::declaration::Attribute;
 
 pub(crate) fn ty_params<'tcx, 'a>(
     ctx: &'a mut Why3Generator<'tcx>,
@@ -705,7 +706,7 @@ pub(crate) fn build_accessor(
     let sig = Signature {
         name: acc_name.clone(),
         trigger: None,
-        attrs: Vec::new(),
+        attrs: vec![Attribute::Attr("inline:trivial".into())],
         args: vec![Binder::typed("self".into(), this.clone())],
         retty: Some(field_ty.clone()),
         contract: Contract::new(),

creusot/src/run_why3.rs

@@ -17,7 +17,7 @@ use rustc_span::{
 use serde_json::Deserializer;
 use std::{
     collections::{hash_map::Entry, HashMap},
-    fmt::{Display, Formatter, Write},
+    fmt::Write,
     io::BufReader,
     path::PathBuf,
     process::{Command, Stdio},
@@ -27,12 +27,12 @@ use why3::ce_models::{ConcreteTerm, FunLitElt, Goal, Loc, ProverResult, TBool, T
 
 static PRELUDE: Dir<'static> = include_dir!("$CARGO_MANIFEST_DIR/../prelude");
 
-impl Display for Why3Sub {
-    fn fmt(&self, f: &mut Formatter<'_>) -> std::fmt::Result {
+impl Why3Sub {
+    fn to_str(&self) -> &str {
         match self {
-            Why3Sub::Prove => f.write_str("prove"),
-            Why3Sub::Ide => f.write_str("ide"),
-            Why3Sub::Replay => f.write_str("replay"),
+            Why3Sub::Prove => "prove",
+            Why3Sub::Ide => "ide",
+            Why3Sub::Replay => "replay",
         }
     }
 }
@@ -51,6 +51,8 @@ pub(super) fn run_why3<'tcx>(ctx: &Why3Generator<'tcx>, file: Option<PathBuf>) {
     std::fs::create_dir(&prelude_dir).unwrap();
 
     PRELUDE.extract(&prelude_dir).expect("could extract prelude into temp dir");
+    let mut conf_path = prelude_dir;
+    conf_path.push("creusot-why3.conf");
     let mut command = Command::new(&why3_cmd.path);
     command
         .args([
@@ -59,11 +61,13 @@ pub(super) fn run_why3<'tcx>(ctx: &Why3Generator<'tcx>, file: Option<PathBuf>) {
             "--warn-off=unused_variable",
             "--warn-off=clone_not_abstract",
             "--warn-off=axiom_abstract",
-            &why3_cmd.sub.to_string(),
+            why3_cmd.sub.to_str(),
             "-L",
         ])
         .arg(temp_dir.path().as_os_str())
         .arg(&output_file)
+        .arg("--extra-config")
+        .arg(conf_path.as_os_str())
         .args(why3_cmd.args.split_ascii_whitespace());
 
     if matches!(why3_cmd.sub, Why3Sub::Prove) {

creusot/tests/should_succeed/100doors.coma

@@ -111,12 +111,12 @@ module Core_Ops_Range_Range_Type
     | bad (start:'idx) (end':'idx)-> {C_Range start end' <> input} {false} any ]
 
 
-  function range_end (self : t_range 'idx) : 'idx =
+  function range_end [@inline:trivial] (self : t_range 'idx) : 'idx =
     match self with
       | C_Range _ a -> a
       end
 
-  function range_start (self : t_range 'idx) : 'idx =
+  function range_start [@inline:trivial] (self : t_range 'idx) : 'idx =
     match self with
       | C_Range a _ -> a
       end

creusot/tests/should_succeed/bdd.coma

@@ -253,12 +253,12 @@ module Bdd_Bdd_Type
     | bad (v:uint64) (childt:t_bdd) (childf:t_bdd)-> {C_If v childt childf <> input} {false} any ]
 
 
-  function bdd_1 (self : t_bdd) : uint64 =
+  function bdd_1 [@inline:trivial] (self : t_bdd) : uint64 =
     match self with
       | C_Bdd _ a -> a
       end
 
-  function bdd_0 (self : t_bdd) : t_node =
+  function bdd_0 [@inline:trivial] (self : t_bdd) : t_node =
     match self with
       | C_Bdd a _ -> a
       end
@@ -901,27 +901,32 @@ module Bdd_Context_Type
       any ]
 
 
-  function context_hashcons (self : t_context) : MyHashMap'0.t_myhashmap (Node'0.t_node) (Bdd'0.t_bdd) =
+  function context_hashcons [@inline:trivial] (self : t_context) : MyHashMap'0.t_myhashmap (Node'0.t_node) (Bdd'0.t_bdd)
+   =
     match self with
       | C_Context _ a _ _ _ _ -> a
       end
 
-  function context_cnt (self : t_context) : uint64 =
+  function context_cnt [@inline:trivial] (self : t_context) : uint64 =
     match self with
       | C_Context _ _ _ _ _ a -> a
       end
 
-  function context_hashcons_ghost (self : t_context) : Snapshot.snap_ty (Map.map uint64 (Node'0.t_node)) =
+  function context_hashcons_ghost [@inline:trivial] (self : t_context) : Snapshot.snap_ty (Map.map uint64 (Node'0.t_node))
+
+   =
     match self with
       | C_Context _ _ a _ _ _ -> a
       end
 
-  function context_not_memo (self : t_context) : MyHashMap'0.t_myhashmap (Bdd'0.t_bdd) (Bdd'0.t_bdd) =
+  function context_not_memo [@inline:trivial] (self : t_context) : MyHashMap'0.t_myhashmap (Bdd'0.t_bdd) (Bdd'0.t_bdd) =
     match self with
       | C_Context _ _ _ a _ _ -> a
       end
 
-  function context_and_memo (self : t_context) : MyHashMap'0.t_myhashmap (Bdd'0.t_bdd, Bdd'0.t_bdd) (Bdd'0.t_bdd) =
+  function context_and_memo [@inline:trivial] (self : t_context) : MyHashMap'0.t_myhashmap (Bdd'0.t_bdd, Bdd'0.t_bdd) (Bdd'0.t_bdd)
+
+   =
     match self with
       | C_Context _ _ _ _ a _ -> a
       end

creusot/tests/should_succeed/bug/206.coma

@@ -119,7 +119,7 @@ module C206_A_Type
     | bad (field_0:Vec'0.t_vec usize (Global'0.t_global))-> {C_A field_0 <> input} {false} any ]
 
 
-  function a_0 (self : t_a) : Vec'0.t_vec usize (Global'0.t_global) =
+  function a_0 [@inline:trivial] (self : t_a) : Vec'0.t_vec usize (Global'0.t_global) =
     match self with
       | C_A a -> a
       end

creusot/tests/should_succeed/bug/486.coma

@@ -12,7 +12,7 @@ module C486_HasMutRef_Type
     | bad (field_0:borrowed 't)-> {C_HasMutRef field_0 <> input} {false} any ]
 
 
-  function hasmutref_0 (self : t_hasmutref 't) : borrowed 't =
+  function hasmutref_0 [@inline:trivial] (self : t_hasmutref 't) : borrowed 't =
     match self with
       | C_HasMutRef a -> a
       end

creusot/tests/should_succeed/bug/570.coma

@@ -13,7 +13,7 @@ module C570_S1_Type
     [ good (f:int32)-> {C_S1 f = input} (! ret {f}) | bad (f:int32)-> {C_S1 f <> input} {false} any ]
 
 
-  function s1_f (self : t_s1) : int32 =
+  function s1_f [@inline:trivial] (self : t_s1) : int32 =
     match self with
       | C_S1 a -> a
       end
@@ -30,7 +30,7 @@ module C570_S2_Type
     [ good (s1:S1'0.t_s1)-> {C_S2 s1 = input} (! ret {s1}) | bad (s1:S1'0.t_s1)-> {C_S2 s1 <> input} {false} any ]
 
 
-  function s2_s1 (self : t_s2) : S1'0.t_s1 =
+  function s2_s1 [@inline:trivial] (self : t_s2) : S1'0.t_s1 =
     match self with
       | C_S2 a -> a
       end

creusot/tests/should_succeed/bug/691.coma

@@ -13,7 +13,7 @@ module C691_Foo_Type
     [ good (bar:uint32)-> {C_Foo bar = input} (! ret {bar}) | bad (bar:uint32)-> {C_Foo bar <> input} {false} any ]
 
 
-  function foo_bar (self : t_foo) : uint32 =
+  function foo_bar [@inline:trivial] (self : t_foo) : uint32 =
     match self with
       | C_Foo a -> a
       end

creusot/tests/should_succeed/bug/768.coma

@@ -14,7 +14,7 @@ module C768_A_Type
     | bad (l:usize) (r:usize)-> {C_A l r <> input} {false} any ]
 
 
-  function a_r (self : t_a) : usize =
+  function a_r [@inline:trivial] (self : t_a) : usize =
     match self with
       | C_A _ a -> a
       end

creusot/tests/should_succeed/bug/991.coma

@@ -119,12 +119,12 @@ module C991_Formula_Type
     | bad (vec:Vec'0.t_vec usize (Global'0.t_global)) (b:bool)-> {C_Formula vec b <> input} {false} any ]
 
 
-  function formula_vec (self : t_formula) : Vec'0.t_vec usize (Global'0.t_global) =
+  function formula_vec [@inline:trivial] (self : t_formula) : Vec'0.t_vec usize (Global'0.t_global) =
     match self with
       | C_Formula a _ -> a
       end
 
-  function formula_b (self : t_formula) : bool =
+  function formula_b [@inline:trivial] (self : t_formula) : bool =
     match self with
       | C_Formula _ a -> a
       end

creusot/tests/should_succeed/cell/02.coma

@@ -36,7 +36,7 @@ module C02_Cell_Type
     | bad (inner:Cell'0.t_cell 't) (ghost_inv:'i)-> {C_Cell inner ghost_inv <> input} {false} any ]
 
 
-  function cell_ghost_inv (self : t_cell 't 'i) : 'i =
+  function cell_ghost_inv [@inline:trivial] (self : t_cell 't 'i) : 'i =
     match self with
       | C_Cell _ a -> a
       end
@@ -113,7 +113,7 @@ module C02_Fib_Type
     [ good (ix:usize)-> {C_Fib ix = input} (! ret {ix}) | bad (ix:usize)-> {C_Fib ix <> input} {false} any ]
 
 
-  function fib_ix (self : t_fib) : usize =
+  function fib_ix [@inline:trivial] (self : t_fib) : usize =
     match self with
       | C_Fib a -> a
       end

creusot/tests/should_succeed/hashmap.coma

@@ -196,7 +196,9 @@ module Hashmap_MyHashMap_Type
       any ]
 
 
-  function myhashmap_buckets (self : t_myhashmap 'k 'v) : Vec'0.t_vec (List'0.t_list ('k, 'v)) (Global'0.t_global) =
+  function myhashmap_buckets [@inline:trivial] (self : t_myhashmap 'k 'v) : Vec'0.t_vec (List'0.t_list ('k, 'v)) (Global'0.t_global)
+
+   =
     match self with
       | C_MyHashMap a -> a
       end

creusot/tests/should_succeed/hillel.coma

@@ -1401,12 +1401,12 @@ module Core_Ops_Range_Range_Type
     | bad (start:'idx) (end':'idx)-> {C_Range start end' <> input} {false} any ]
 
 
-  function range_end (self : t_range 'idx) : 'idx =
+  function range_end [@inline:trivial] (self : t_range 'idx) : 'idx =
     match self with
       | C_Range _ a -> a
       end
 
-  function range_start (self : t_range 'idx) : 'idx =
+  function range_start [@inline:trivial] (self : t_range 'idx) : 'idx =
     match self with
       | C_Range a _ -> a
       end