Update strategies + init Scratch + update README

Cargo.toml

@@ -1,5 +1,5 @@
 [workspace]
-members = ["CreuSAT", "Robinson", "Friday", "JigSAT", "tests"]
+members = ["CreuSAT", "Robinson", "Friday", "JigSAT", "Scratch", "tests"]
 
 [profile.release]
 debug = false

CreuSAT/Cargo.toml

@@ -64,3 +64,4 @@ trust_util = []
 trust_util_logic = []
 trust_watches = []
 trust_watches_logic = []
+problem_child = []

CreuSAT/src/conflict_analysis.rs

@@ -258,7 +258,7 @@ pub fn analyze_conflict(f: &Formula, trail: &Trail, cref: usize, d: &mut Decisio
     }
 }
 
-#[cfg_attr(feature = "trust_conflict", trusted)]
+#[cfg_attr(all(feature = "trust_conflict", not(feature = "problem_child")), trusted)]
 #[requires(f.invariant())]
 #[requires(trail.invariant(*f))]
 #[requires(@cref < (@f.clauses).len())]

CreuSAT/src/logic/logic_formula.rs

@@ -55,6 +55,7 @@ impl Formula {
             exists<a2 : Seq<AssignedState>> a2.len() == @self.num_vars && complete_inner(a2) && self.sat_inner(a2)
         }
     }
+
     #[predicate]
     pub fn equisat(self, o: Formula) -> bool {
         self.eventually_sat_complete() == o.eventually_sat_complete()

CreuSAT/src/trail.rs

@@ -50,8 +50,7 @@ impl Trail {
         }
     }
 
-    // For some reason the post takes forever(but it solved on Mac with auto level 3)
-    #[cfg_attr(feature = "trust_trail", trusted)]
+    #[cfg_attr(all(feature = "trust_trail", not(feature = "problem_child")), trusted)]
     #[inline(always)]
     #[requires(f.invariant())]
     #[requires(@f.num_vars > 0)]

CreuSAT/src/unit_prop.rs

@@ -48,9 +48,12 @@ fn check_and_move_watch(
     return false;
 }
 
-#[cfg_attr(feature = "trust_unit", trusted)]
+// TODO: Look at strategies or look at making lemmas / assertions to make it easier.
+// This has previously had issues on the trail invariant and on the formula equisatisfiability.
+// Solved fairly easily by Auto Level 3 when targeted direcly, but Auto Level 8/9 struggles.
+#[cfg_attr(all(feature = "trust_unit", not(feature = "problem_child")), trusted)]
 #[maintains((mut f).invariant())]
-#[maintains((*trail).invariant(mut f))]
+#[maintains((*trail).invariant(mut f))] // <-
 #[maintains((*watches).invariant(mut f))]
 #[requires((@(@f.clauses)[@cref]).len() >= 2)]
 #[requires(@cref < (@f.clauses).len())]
@@ -61,7 +64,7 @@ fn check_and_move_watch(
 #[ensures(@f.num_vars == @(^f).num_vars)]
 #[ensures((@f.clauses).len() == (@(^f).clauses).len())]
 //#[ensures((@(@f.clauses)[@cref]).len() == (@(@(^f).clauses)[@cref]).len())]
-#[ensures(f.equisat(^f))]
+#[ensures(f.equisat(^f))] // <-
 fn swap(f: &mut Formula, trail: &Trail, watches: &Watches, cref: usize, j: usize, k: usize) {
     let old_f: Ghost<&mut Formula> = ghost! { f };
 
@@ -72,6 +75,7 @@ fn swap(f: &mut Formula, trail: &Trail, watches: &Watches, cref: usize, j: usize
 
     proof_assert!(forall<a2 : Seq<AssignedState>> a2.len() == @f.num_vars && complete_inner(a2) && (@old_f.clauses)[@cref].sat_inner(a2) ==> (@f.clauses)[@cref].sat_inner(a2));
     proof_assert!(eventually_sat_complete(@old_f) ==> eventually_sat_complete(@f));
+    proof_assert!(^f == ^old_f.inner());
 }
 
 // This has to do f.clauses[cref] and not f[cref]

CreuSAT/src/watches.rs

@@ -23,7 +23,7 @@ pub struct Watches {
 // The root cause seems to be that Why3 doesn't wan't to "peek" into things, so when I made abstraction
 // barriers for the invariants, stuff took forever. It checks out, but I should probably come back later and clean up
 // #10 and #19 just take some time, but check out on Mac
-#[cfg_attr(feature = "trust_watches", trusted)]
+#[cfg_attr(all(feature = "trust_watches", not(feature = "problem_child")), trusted)]
 #[maintains((mut watches).invariant(*f))]
 #[requires(@f.num_vars < @usize::MAX/2)]
 #[requires(lit.index_logic() < @f.num_vars)]
@@ -148,7 +148,7 @@ impl Watches {
     }
 
     // This is just the first half of update_watch.
-    #[cfg_attr(feature = "trust_watches", trusted)]
+    #[cfg_attr(all(feature = "trust_watches", not(feature = "problem_child")), trusted)]
     #[maintains((mut self).invariant(*f))]
     #[requires(@f.num_vars < @usize::MAX/2)]
     #[requires(lit.index_logic() < @f.num_vars)]
@@ -165,6 +165,7 @@ impl Watches {
                 let end = self.watches[watchidx].len() - 1;
                 self.watches[watchidx].swap(i, end);
 
+                // TODO
                 // Ugly "ghost" match. Grr.
                 let old_w: Ghost<&mut Watches> = ghost! { self };
                 match self.watches[watchidx].pop() {

Friday/Cargo.toml

@@ -8,3 +8,6 @@ edition = "2021"
 [dependencies]
 #clap = "2.33.3"
 creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "6a963bf" }
+
+[features]
+contracts = ["creusot-contracts/contracts"]

Makefile.toml

@@ -197,3 +197,36 @@ rm -rf mlcfgs/CreuSAT*
 [tasks.clean-proofs]
 workspace = false
 dependencies = ["clean-Friday", "clean-Robinson", "clean-CreuSAT"]
+
+
+[tasks.creusot-Scratch]
+workspace = false
+command = "cargo"
+args = ["creusot", "--", "-p", "Scratch", "--features=${@}"]
+
+[tasks.move-Scratch]
+workspace = false
+script = '''
+[ ! -f ./target/debug/Scratch-rlib.mlcfg ] || cp ./target/debug/Scratch-rlib.mlcfg ./mlcfgs/Scratch.mlcfg
+'''
+
+[tasks.gen-cfg-Scratch]
+workspace = false
+dependencies = ["creusot-Scratch", "move-Scratch"]
+
+[tasks.ide-Scratch]
+workspace = false
+script = '''
+./ide ./mlcfgs/Scratch.mlcfg
+'''
+
+[tasks.prove-Scratch]
+workspace = false
+dependencies = ["gen-cfg-Scratch", "ide-Scratch"]
+
+
+[tasks.clean-Scratch]
+workspace = false
+script = '''
+rm -rf mlcfgs/Scratch*
+'''

README.md

@@ -51,6 +51,7 @@ To prove it you'll need to do the following:
 1. Install [Rust](https://www.rust-lang.org/tools/install).
 2. Install [Creusot](https://github.com/xldenis/creusot). Clone it, and then run `cargo install --path creusot`.
 3. Install Why3. I recommend following the guide in the [Creusot](https://github.com/xldenis/creusot#installing) repository.
+4. Install some SMT solvers: [Z3](https://github.com/Z3Prover/z3) (available by `brew`, `apt`, etc.), [CVC4](https://cvc4.github.io/) (`brew`, `apt`, etc.), [Alt-Ergo](https://alt-ergo.ocamlpro.com/) (`opam`, `apt`, etc.).
 
 CreuSAT is using [Cargo Make](https://github.com/sagiegurari/cargo-make) to make building easier. It can be installed by running:
 ```
@@ -63,7 +64,8 @@ cargo make prove-CreuSAT
 
 And hopefully the Why3 IDE will appear. If not, then most likely something is not installed or pathed correctly, or I have given the wrong instructions (sorry).
 
-If the Why3 IDE appears, then it should work to press <kbd>3</kbd> and wait a bit. If you are doing the proof from scratch, then you will need to wait a while.
+Once you are in the Why3 IDE, you may click "Tools -> Strategies -> PROVE EVERYTHING" (or press <kbd>4</kbd>). This should Just Work™ and have everything proved in ~5 minutes on decently modern hardware (I am using a 2019 MacBook Pro). If you have slower hardware, you may need to tweak [why3.conf](why3.conf) a bit. Feel free to reach out to me or open an issue if you experience any issues.
+
 
 The following `cargo make` commands are supported:
 - `prove-CreuSAT`/`p` : Generate the MLCFG for `CreuSAT` and run the Why3 IDE.

Scratch/Cargo.toml

@@ -0,0 +1,62 @@
+[package]
+name = "Scratch"
+version = "0.1.0"
+authors = ["Sarek Høverstad Skotåm <sarek.skotam@gmail.com>"]
+edition = "2021"
+
+[dependencies]
+clap = "2.33.3"
+creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0", rev = "6a963bf" }
+
+# This is just copied verbatim from CreuSAT.
+[features]
+trust_all = [
+    "trust_assignments",
+    "trust_clause",
+    "trust_conflict",
+    "trust_decision",
+    "trust_formula",
+    "trust_lit",
+    "trust_solver",
+    "trust_trail",
+    "trust_unit",
+    "trust_util",
+    "trust_watches",
+    "trust_logic",
+]
+trust_logic = [
+    "trust_clause_logic",
+    "trust_conflict_logic",
+    "trust_decision_logic",
+    "trust_formula_logic",
+    "trust_lit_logic",
+    "trust_solver_logic",
+    "trust_trail_logic",
+    "trust_unit_logic",
+    "trust_util_logic",
+    "trust_watches_logic",
+    "trust_logic_logic",
+]
+trust_assignments = []
+trust_assignments_logic = []
+trust_clause = []
+trust_clause_logic = []
+trust_conflict = ["trust_conflict_logic"]
+trust_conflict_logic = []
+trust_decision = []
+trust_decision_logic = []
+trust_formula = ["trust_formula_logic"]
+trust_formula_logic = []
+trust_lit = ["trust_lit_logic"]
+trust_lit_logic = []
+trust_logic_logic = []
+trust_solver = []
+trust_solver_logic = []
+trust_trail = ["trust_trail_logic"]
+trust_trail_logic = []
+trust_unit = []
+trust_unit_logic = []
+trust_util = []
+trust_util_logic = []
+trust_watches = []
+trust_watches_logic = []

Scratch/README.md

@@ -0,0 +1,3 @@
+# Scratch
+
+This is a scratch space for me to experiment with ideas. It is likely to be removed once those ideas are worked out.

Scratch/src/assignments.rs

@@ -0,0 +1,61 @@
+extern crate creusot_contracts;
+use creusot_contracts::std::*;
+use creusot_contracts::*;
+
+#[cfg(creusot)]
+use crate::logic::*;
+
+use crate::formula::*;
+
+// ===== Assignments =====
+pub type AssignedState = u8;
+
+pub struct Assignments(pub Vec<AssignedState>);
+
+#[cfg(creusot)]
+impl ShallowModel for Assignments {
+    type ShallowModelTy = Seq<AssignedState>;
+
+    #[logic]
+    fn shallow_model(self) -> Self::ShallowModelTy {
+        self.0.shallow_model()
+    }
+}
+
+#[predicate]
+pub fn compatible_inner(a: Seq<AssignedState>, a2: Seq<AssignedState>) -> bool {
+    pearlite! {
+        a.len() == a2.len() && (forall<i: Int> 0 <= i && i < a.len() ==>
+            (unset(a[i]) || a[i] == a2[i]))
+    }
+}
+
+#[predicate]
+pub fn complete_inner(a: Seq<AssignedState>) -> bool {
+    pearlite! {
+        forall<i: Int> 0 <= i && i < a.len() ==> !unset(a[i])
+    }
+}
+
+#[predicate]
+pub fn compatible_complete_inner(a: Seq<AssignedState>, a2: Seq<AssignedState>) -> bool {
+    compatible_inner(a, a2) && complete_inner(a2)
+}
+
+// Predicates
+impl Assignments {
+    #[predicate]
+    pub fn invariant(self, f: Formula) -> bool {
+        pearlite! {
+            @f.num_vars == (@self).len()
+            && forall<i : Int> 0 <= i && i < (@self).len() ==> @(@self)[i] <= 3
+        }
+    }
+
+    #[predicate]
+    pub fn complete(self) -> bool {
+        pearlite! {
+            forall<i: Int> 0 <= i && i < (@self).len() ==> !unset((@self)[i])
+        }
+    }
+}