Update prelude + update proofs.

sarsko · Jul 27, 2022 · 1fd8d67 · 1fd8d67
1 parent 2b14ec1
commit 1fd8d67
Show file tree

Hide file tree

Showing 19 changed files with 16,550 additions and 14,838 deletions.
diff --git a/Cargo.lock b/Cargo.lock
diff --git a/CreuSAT/Cargo.toml b/CreuSAT/Cargo.toml
@@ -25,7 +25,7 @@ opt-level = 3
 [dependencies]
 clap = "2.33.3"
 rand = "*"
-creusot-contracts = { git = "https://github.com/xldenis/creusot", rev = "3c30869", version = "^0" }
+creusot-contracts = { git = "https://github.com/xldenis/creusot", rev = "e1560b7", version = "^0" }
 
 
 [dev-dependencies]

diff --git a/CreuSAT/src/decision.rs b/CreuSAT/src/decision.rs
@@ -1,4 +1,5 @@
 extern crate creusot_contracts;
+use creusot_contracts::derive::Clone;
 use creusot_contracts::logic::Ghost;
 use creusot_contracts::std::*;
 use creusot_contracts::*;

diff --git a/CreuSAT/src/lit.rs b/CreuSAT/src/lit.rs
@@ -3,6 +3,8 @@ use ::std::ops;
 use creusot_contracts::std::*;
 use creusot_contracts::*;
 
+use creusot_contracts::derive::Clone;
+
 use crate::assignments::*;
 
 #[cfg(feature = "contracts")]

diff --git a/CreuSAT/src/trail.rs b/CreuSAT/src/trail.rs
@@ -248,12 +248,6 @@ impl Trail {
         proof_assert!(step.invariant(*_f));
         proof_assert!(lemma_push_maintains_lit_not_in_less(*self, *_f, step); true);
         self.trail.push(step);
-        proof_assert! {
-            match step.reason {
-                Reason::Long(k) => { clause_post_with_regards_to_inner((@_f.clauses)[@k], @(*self).assignments, step.lit.index_logic()) },
-                    _ => true,
-                }
-        };
 
         proof_assert!(self.lit_is_unique());
         proof_assert!(self.lit_not_in_less(*_f));

diff --git a/Friday/Cargo.toml b/Friday/Cargo.toml
@@ -24,7 +24,7 @@ opt-level = 3
 
 [dependencies]
 #clap = "2.33.3"
-creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0" }
+creusot-contracts = { git = "https://github.com/xldenis/creusot", rev = "e1560b7", version = "^0" }
 
 [features]
 contracts = ["creusot-contracts/contracts"]
diff --git a/Friday/src/lib.rs b/Friday/src/lib.rs
@@ -6,18 +6,22 @@ extern crate creusot_contracts;
 use creusot_contracts::std::*;
 use creusot_contracts::*;
 
+use creusot_contracts::derive::Clone;
+
 // This is a very naive, but verified SAT solver.
 // It is a port of a verified WhyML solver, and is therefore
 // an imperative implementation of a functional prgram.
 // In other words: very naive, very slow.
 
+#[derive(Clone)]
 struct Assignments(Vec<bool>);
 struct Lit {
     var: usize,
     value: bool,
 }
 struct Clause(Vec<Lit>);
 
+#[derive(Clone)]
 struct Pasn {
     assign: Assignments,
     ix: usize,
@@ -27,22 +31,6 @@ pub struct Formula {
     num_vars: usize,
 }
 
-impl Clone for Assignments {
-    #[trusted]
-    #[ensures(*self == result)]
-    fn clone(&self) -> Self {
-        Assignments(self.0.clone())
-    }
-}
-
-impl Clone for Pasn {
-    #[trusted]
-    #[ensures(*self == result)]
-    fn clone(&self) -> Self {
-        Pasn { assign: self.assign.clone(), ix: self.ix }
-    }
-}
-
 impl Formula {
     #[predicate]
     fn invariant(self) -> bool {

diff --git a/Robinson/Cargo.toml b/Robinson/Cargo.toml
@@ -24,7 +24,7 @@ opt-level = 3
 
 [dependencies]
 clap = "2.33.3"
-creusot-contracts = { git = "https://github.com/xldenis/creusot", version = "^0" }
+creusot-contracts = { git = "https://github.com/xldenis/creusot", rev = "e1560b7", version = "^0" }
 
 # This is just copied verbatim from CreuSAT.
 [features]

diff --git a/Robinson/src/lit.rs b/Robinson/src/lit.rs
@@ -4,6 +4,8 @@ use creusot_contracts::std::*;
 #[allow(unused)]
 use creusot_contracts::*;
 
+use creusot_contracts::derive::Clone;
+
 use crate::assignments::*;
 
 #[cfg(feature = "contracts")]