try to use z3 sequences

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,28 @@ 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/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) {

prelude/creusot-why3.conf

@@ -0,0 +1,3 @@
+[prover_modifiers]
+name = "Z3"
+driver = "z3_nombqi_seq.drv"

prelude/seq_ext.mlw

@@ -1,6 +1,9 @@
 module SeqExt
 use seq.Seq
+use int.Int
 
-let function subsequence (s : seq 't) (i : int) (j : int) : seq 't = s[i..j]
+function subsequence [@inline:trivial] (s : seq 't) (i : int) (j : int) : seq 't = s[i..j]
+
+function extract (s: seq 't) (offset: int) (len: int) : seq 't = s[offset..offset+len]
 
 end

prelude/z3_nombqi_seq.drv

@@ -0,0 +1,142 @@
+(* This Source Code Form is subject to the terms of the Mozilla Public
+   License, v. 2.0. If a copy of the MPL was not distributed with this
+   file, You can obtain one at http://mozilla.org/MPL/2.0/.
+
+   Copyright (c) 2011-2021 ETH Zurich.
+*)
+prelude ";;; generated by no_mbqi extension"
+prelude "(set-option :smt.AUTO_CONFIG false)"
+prelude "(set-option :smt.PHASE_SELECTION 0)"
+prelude "(set-option :smt.RESTART_STRATEGY 0)"
+prelude "(set-option :smt.RESTART_FACTOR 1.5)"
+prelude "(set-option :smt.ARITH.RANDOM_INITIAL_VALUE true)"
+prelude "(set-option :smt.CASE_SPLIT 3)"
+prelude "(set-option :smt.DELAY_UNITS true)"
+prelude "(set-option :NNF.SK_HACK true)"
+prelude "(set-option :smt.MBQI false)"
+prelude "(set-option :smt.BV.REFLECT true)"
+prelude "(set-option :smt.qi.max_multi_patterns 1000)"
+prelude "(set-option :smt.QI.EAGER_THRESHOLD 10)"
+
+theory map.Const
+  syntax function const "((as const %t0) %1)"
+    meta "encoding:ignore_polymorphism_ls" function const
+end
+
+theory seq.Seq
+  prelude ";;; generated by sequence encoding"
+  prelude "(declare-fun seq.range (Int) (Seq Int))"
+  prelude "(assert (forall ((n Int)) (! (=> (<= 0 n) (= (seq.len (seq.range n)) n)) :pattern (seq.range n))))"
+  prelude "(assert (forall ((n Int) (i Int)) (! (=> (and (<= 0 i) (< i n)) (= (seq.nth_i (seq.range n) i) i)) :pattern (seq.nth_i (seq.range n) i))))"
+
+  syntax type seq            "(Seq %1)"
+  meta "encoding:ignore_polymorphism_ts" type seq
+
+
+  syntax function length     "(seq.len %1)"
+  meta "encoding:ignore_polymorphism_ls" function length
+  remove prop length_nonnegative
+  meta "encoding:ignore_polymorphism_pr" prop length_nonnegative
+
+  syntax function get        "(seq.nth_i %1 %2)"
+  meta "encoding:ignore_polymorphism_ls" function get
+
+  syntax function ([])       "(seq.nth_i %1 %2)"
+  meta "encoding:ignore_polymorphism_ls" function ([])
+
+  syntax predicate (==)      "(= %1 %2)"
+  meta "encoding:ignore_polymorphism_ls" predicate (==)
+  remove prop (==)'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop (==)'spec'0
+  remove prop (==)'spec
+  meta "encoding:ignore_polymorphism_pr" prop (==)'spec
+
+  (* see below for range*)
+  syntax function create     "(seq.map %2 (seq.range %1))"
+  meta "encoding:ignore_polymorphism_ls" function create
+  remove prop create'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop create'spec'0
+  remove prop create'spec
+  meta "encoding:ignore_polymorphism_pr" prop create'spec
+
+  syntax constant empty      "(as seq.empty %t0)"
+  remove prop empty'def
+  meta "encoding:ignore_polymorphism_pr" prop empty'def
+
+  syntax function set        "(seq.++ (seq.extract %1 0 %2) (seq.unit %3) (seq.extract %1 (+ %2 1) (- (seq.len %1) (+ %2 1))))"
+  meta "encoding:ignore_polymorphism_ls" function set
+  remove prop set'def
+  meta "encoding:ignore_polymorphism_pr" prop set'def
+  remove prop set'spec'1
+  meta "encoding:ignore_polymorphism_pr" prop set'spec'1
+  remove prop set'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop set'spec'0
+  remove prop set'spec
+  meta "encoding:ignore_polymorphism_pr" prop set'spec
+
+  syntax function ([<-])     "(seq.++ (seq.extract %1 0 %2) (seq.unit %3) (seq.extract %1 (+ %2 1) (- (seq.len %1) (+ %2 1))))"
+  meta "encoding:ignore_polymorphism_ls" function ([<-])
+  remove prop ([<-])'def
+  meta "encoding:ignore_polymorphism_pr" prop ([<-])'def
+
+  syntax function singleton  "(seq.unit %1)"
+  meta "encoding:ignore_polymorphism_ls" function singleton
+  remove prop singleton'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop singleton'spec'0
+  remove prop singleton'spec
+  meta "encoding:ignore_polymorphism_pr" prop singleton'spec
+
+  syntax function cons       "(seq.++ (seq.unit %1) %2)"
+  meta "encoding:ignore_polymorphism_ls" function cons
+  remove prop cons'spec'1
+  meta "encoding:ignore_polymorphism_pr" prop cons'spec'1
+  remove prop cons'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop cons'spec'0
+  remove prop cons'spec
+  meta "encoding:ignore_polymorphism_pr" prop cons'spec
+
+  syntax function snoc       "(seq.++ %1 (seq.unit %2))"
+  meta "encoding:ignore_polymorphism_ls" function snoc
+  remove prop snoc'spec'1
+  meta "encoding:ignore_polymorphism_pr" prop snoc'spec'1
+  remove prop snoc'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop snoc'spec'0
+  remove prop snoc'spec
+  meta "encoding:ignore_polymorphism_pr" prop snoc'spec
+
+  syntax function ([..])     "(seq.extract %1 %2 (- %3 %2))"
+  meta "encoding:ignore_polymorphism_ls" function singleton
+  remove prop ([..])'def
+  meta "encoding:ignore_polymorphism_pr" prop ([..])'def
+  remove prop ([..])'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop ([..])'spec'0
+  remove prop ([..])'spec
+  meta "encoding:ignore_polymorphism_pr" prop ([..])'spec
+
+  syntax function ([_..])    "(seq.extract %1 %2 (- (seq.len %1) %2))"
+  meta "encoding:ignore_polymorphism_ls" function ([_..])
+  remove prop ([_..])'def
+  meta "encoding:ignore_polymorphism_pr" prop ([_..])'def
+
+  syntax function ([.._])    "(seq.extract %1 0 %2)"
+  meta "encoding:ignore_polymorphism_ls" function ([.._])
+  remove prop ([.._])'def
+  meta "encoding:ignore_polymorphism_pr" prop ([.._])'def
+
+  syntax function (++)       "(seq.++ %1 %2)"
+  meta "encoding:ignore_polymorphism_ls" function (++)
+  remove prop (++)'spec'1
+  meta "encoding:ignore_polymorphism_pr" prop (++)'spec'1
+  remove prop (++)'spec'0
+  meta "encoding:ignore_polymorphism_pr" prop (++)'spec'0
+  remove prop (++)'spec
+  meta "encoding:ignore_polymorphism_pr" prop (++)'spec
+end
+
+theory prelude.seq_ext.SeqExt
+use seq.Seq
+
+syntax function extract      "(seq.extract %1 %2 %3)"
+meta "encoding:ignore_polymorphism_ls" function extract
+
+end