Upgrade to Creusot 0.11.0

.github/workflows/ci.yaml

@@ -11,7 +11,7 @@ concurrency:
   cancel-in-progress: true
 
 env:
-  CREUSOT_VERSION: v0.10.0+why3find-dep
+  CREUSOT_VERSION: v0.11.0
 
 jobs:
   rust:

.github/workflows/nightly.yaml

@@ -50,4 +50,4 @@ jobs:
           echo -e '[patch.crates-io]\ncreusot-std = { path = "../creusot/creusot-std" }' > .cargo/config.toml
 
       - name: Run Creusot
-        run: cargo creusot prove -- -Fsolutions
+        run: cargo creusot -- -Fsolutions

Cargo.toml

@@ -4,7 +4,7 @@ version = "0.1.0"
 edition = "2024"
 
 [dependencies]
-creusot-std = { version = "0.10.0", features = ["sc-drf"] }
+creusot-std = { version = "0.11.0-dev", features = ["sc-drf"] }
 
 [features]
 solutions = []

src/ex3_parallel_add.rs

@@ -6,7 +6,6 @@
 #[allow(unused)] // TODO: Remove this
 use creusot_std::{
     ghost::{
-        Committer,
         invariant::{AtomicInvariant, Protocol, Tokens, declare_namespace},
         perm::Perm,
         resource::{Authority, Fragment},
@@ -16,8 +15,8 @@ use creusot_std::{
 };
 
 use std::sync::atomic::AtomicI32;
-// TODO: Replace with the creusot_std version of AtomicI32
-// use creusot_std::std::sync::AtomicI32;
+// TODO: Replace with the creusot_std version of AtomicI32 (you will also need the committer ☺)
+// use creusot_std::sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer};
 
 use std::thread;
 // TODO: Replace with the creusot_std version of thread

src/solutions/ex3_parallel_add.rs

@@ -1,14 +1,15 @@
-use creusot_std::std::sync::atomic_sc::AtomicI32;
 use creusot_std::{
     ghost::{
-        Committer,
-        invariant::{AtomicInvariant, Protocol, Tokens, declare_namespace},
+        invariant::{AtomicInvariantSC, Protocol, Tokens, declare_namespace},
         perm::Perm,
         resource::{Authority, Fragment},
     },
     logic::{Id, ra::excl::Excl},
     prelude::*,
-    std::thread::{self, JoinHandleExt},
+    std::{
+        sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer},
+        thread::{self, JoinHandleExt},
+    },
 };
 
 declare_namespace! { PARALLEL_ADD }
@@ -48,7 +49,7 @@ pub fn parallel_add() -> i32 {
     };
 
     // Initialize our invariant
-    let inv = AtomicInvariant::new(
+    let inv = AtomicInvariantSC::new(
         ghost!(ParallelAddAtomicInv {
             own: own.into_inner(),
             auth1: auth1.into_inner(),
@@ -59,7 +60,7 @@ pub fn parallel_add() -> i32 {
     );
 
     thread::scope(|s| {
-        // We use move closure to make sure that they do not contain borrows of `Ghost<_>`, since
+        // We use move closures to make sure that they do not contain borrows of `Ghost<_>`, since
         // such a borrow would unnecesary consume space in these closures. So, we create the borrows
         // here.
         let mut frag1: Ghost<&mut _> = frag1.borrow_mut();
@@ -70,10 +71,11 @@ pub fn parallel_add() -> i32 {
         let t1 = s.spawn(move |tokens: Ghost<Tokens>| {
             atomic.fetch_add(
                 2,
-                ghost! { |c: &mut Committer<AtomicI32>| {
+                ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| {
                     inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| {
                         inv.auth1.update(*frag1, snapshot!((Some(Excl(true)), Some(Excl(true)))));
-                        c.shoot(&mut inv.own);
+                        c.shoot_load(&inv.own);
+                        c.shoot_store(&mut inv.own);
                     })
                 }},
             );
@@ -82,10 +84,11 @@ pub fn parallel_add() -> i32 {
         let t2 = s.spawn(move |tokens: Ghost<Tokens>| {
             atomic.fetch_add(
                 2,
-                ghost! { |c: &mut Committer<AtomicI32>| {
+                ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| {
                     inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| {
                         inv.auth2.update(*frag2, snapshot!((Some(Excl(true)), Some(Excl(true)))));
-                        c.shoot(&mut inv.own);
+                        c.shoot_load(&inv.own);
+                        c.shoot_store(&mut inv.own);
                     })
                 }},
             );