From 258368ab8714e74f74dabe9a4defc4e1440b357f Mon Sep 17 00:00:00 2001 From: dewert99 Date: Wed, 31 Jul 2024 18:29:35 -0700 Subject: [PATCH] try to use z3 sequences --- creusot-contracts/src/logic/seq.rs | 28 +++++- creusot/src/run_why3.rs | 18 ++-- prelude/creusot-why3.conf | 3 + prelude/seq_ext.mlw | 5 +- prelude/z3_nombqi_seq.drv | 142 +++++++++++++++++++++++++++++ 5 files changed, 187 insertions(+), 9 deletions(-) create mode 100644 prelude/creusot-why3.conf create mode 100644 prelude/z3_nombqi_seq.drv diff --git a/creusot-contracts/src/logic/seq.rs b/creusot-contracts/src/logic/seq.rs index 60e30cf220..90896a2aec 100644 --- a/creusot-contracts/src/logic/seq.rs +++ b/creusot-contracts/src/logic/seq.rs @@ -38,6 +38,15 @@ impl Seq { 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 Seq { #[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 + 0 <= i && i < s1.len() ==> s1.concat(s2)[i] == s1[i])] + #[ensures(forall + s1.len() <= i && i < s1.len() + s2.len() ==> s1.concat(s2)[i] == s2[i - s1.len()])] + #[ensures(forall + 0 <= i && i < len && 0 <= len && 0 <= offset && (offset+len) <= s.len() + ==> s.extract(offset, len)[i] == s[offset+i])] + #[ensures(forall + 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 { diff --git a/creusot/src/run_why3.rs b/creusot/src/run_why3.rs index 522f9785a3..6ac91c80e1 100644 --- a/creusot/src/run_why3.rs +++ b/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) { 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) { "--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) { diff --git a/prelude/creusot-why3.conf b/prelude/creusot-why3.conf new file mode 100644 index 0000000000..7d55883713 --- /dev/null +++ b/prelude/creusot-why3.conf @@ -0,0 +1,3 @@ +[prover_modifiers] +name = "Z3" +driver = "z3_nombqi_seq.drv" \ No newline at end of file diff --git a/prelude/seq_ext.mlw b/prelude/seq_ext.mlw index e40cef5846..b54b3e7b2e 100644 --- a/prelude/seq_ext.mlw +++ b/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 diff --git a/prelude/z3_nombqi_seq.drv b/prelude/z3_nombqi_seq.drv new file mode 100644 index 0000000000..52eb9825c1 --- /dev/null +++ b/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 \ No newline at end of file