Fix rustc build and test parallel_add example

Author: Lysxia

Cargo.toml

@@ -8,6 +8,7 @@ creusot-std = "0.9.0"
 
 [features]
 solutions = []
+nightly = []
 
 [lints.rust]
 unexpected_cfgs = { level = "warn", check-cfg = ['cfg(creusot)'] }

src/ex0_examples.rs

@@ -76,8 +76,8 @@ pub fn sum_slice(xs: &[u64]) -> u64 {
     sum_slice_lemma(xs);
     let _ = xs
         .iter()
-        .map_inv(|x, produced| {
-            proof_assert! { sum@ + x@ == sum_seq(xs@[0..produced.len() + 1]) };
+        .map_inv(|x, _produced| {
+            proof_assert! { sum@ + x@ == sum_seq(xs@[0.._produced.len() + 1]) };
             sum += *x;
         })
         .collect::<()>();
@@ -104,6 +104,7 @@ pub fn sum_seq(xs: Seq<u64>) -> Int {
 #[ensures(forall<i> 0 <= i && i < xs@.len() ==> xs@[0..i+1][0..i] == xs@[0..i])]
 #[ensures(xs@[0..xs@.len()] == xs@)]
 pub fn sum_slice_lemma(xs: &[u64]) {
+    _ = xs;
     let _ = snapshot! { sum_seq_sub(xs@) };
 }
 
@@ -210,8 +211,8 @@ pub fn interior_mut() {
         let cell = UnsafeCell::new(0); // `PermCell::new` will return a cell and a permission
         let (b1, b2) = (&cell, &cell); // Share the cell (this line won't change)
         *&mut *b1.get() = 1; // Replace this with `PermCell::set` or `PermCell::borrow_mut` to write to it
-        let result = *&*b2.get(); // Replace this with `PermCell::get` or `PermCell::borrow` to read from it
-        proof_assert! { result == 1i32 };
+        let _result = *&*b2.get(); // Replace this with `PermCell::get` or `PermCell::borrow` to read from it
+        proof_assert! { _result == 1i32 };
     }
 }
 

src/ex3_parallel_add.rs

@@ -26,7 +26,8 @@ use std::thread;
 // Spawn two threads that add 2 to a shared atomic variable.
 // Prove that the final value is 4.
 #[trusted]
-pub fn parallel_add() {
+#[ensures(result == 4i32)]
+pub fn parallel_add() -> i32 {
     let atomic = AtomicI32::new(0);
 
     thread::scope(|s| {
@@ -44,6 +45,10 @@ pub fn parallel_add() {
         let _ = t2.join().unwrap();
     });
 
-    let n = atomic.into_inner(); // Non-atomically read the atomic
-    proof_assert!(n == 4i32)
+    atomic.into_inner() // Non-atomically read the atomic
+}
+
+#[test]
+fn test() {
+    assert! { parallel_add() == 4 }
 }

src/solutions/ex0_examples.rs

@@ -73,8 +73,8 @@ pub fn sum_slice(xs: &[u64]) -> u64 {
     sum_slice_lemma(xs);
     let _ = xs
         .iter()
-        .map_inv(|x, produced| {
-            proof_assert! { sum@ + x@ == sum_seq(xs@[0..produced.len() + 1]) };
+        .map_inv(|x, _produced| {
+            proof_assert! { sum@ + x@ == sum_seq(xs@[0.._produced.len() + 1]) };
             sum += *x;
         })
         .collect::<()>();
@@ -86,6 +86,7 @@ pub fn sum_slice(xs: &[u64]) -> u64 {
 #[ensures(forall<i> 0 <= i && i < xs@.len() ==> xs@[0..i+1][0..i] == xs@[0..i])]
 #[ensures(xs@[0..xs@.len()] == xs@)]
 pub fn sum_slice_lemma(xs: &[u64]) {
+    _ = xs;
     let _ = snapshot! { sum_seq_sub(xs@) };
 }
 
@@ -182,8 +183,8 @@ pub fn interior_mut() {
         let (cell, mut perm) = PermCell::new(0);
         let (b1, b2) = (&cell, &cell);
         b1.set(ghost! { &mut **perm }, 1);
-        let result = b2.take(ghost! { &mut **perm });
-        proof_assert! { result == 1i32 };
+        let _result = b2.take(ghost! { &mut **perm });
+        proof_assert! { _result == 1i32 };
     }
 }
 

src/solutions/ex3_parallel_add.rs

@@ -35,8 +35,9 @@ impl Protocol for ParallelAddAtomicInv {
     }
 }
 
-#[requires(tokens.contains(PARALLEL_ADD()))]
-pub fn parallel_add(mut tokens: Ghost<Tokens>) {
+#[cfg(feature = "nightly")]
+#[ensures(result == 4i32)]
+pub fn parallel_add() -> i32 {
     let (atomic, own) = AtomicI32::new(0);
 
     // Create our ghost state
@@ -104,6 +105,11 @@ pub fn parallel_add(mut tokens: Ghost<Tokens>) {
         inv.auth2.frag_lemma(&frag2);
         inv.own
     };
-    let n = atomic.into_inner(own); // Non-atomically read the atomic
-    proof_assert!(n == 4i32)
+    atomic.into_inner(own) // Non-atomically read the atomic
+}
+
+#[cfg(feature = "nightly")]
+#[test]
+fn test() {
+    assert! { parallel_add() == 4 }
 }