diff --git a/.devcontainer/devcontainer.json b/.devcontainer/devcontainer.json index ba253ad..a2091b9 100644 --- a/.devcontainer/devcontainer.json +++ b/.devcontainer/devcontainer.json @@ -1,6 +1,6 @@ { "name": "Creusot tutorial", - "image": "ghcr.io/creusot-rs/creusot:v0.11.0", + "image": "ghcr.io/creusot-rs/creusot:latest", "containerEnv": { "CREUSOT_DATA_HOME": "/" diff --git a/.github/workflows/ci.yaml b/.github/workflows/ci.yaml index 5140419..1a31302 100644 --- a/.github/workflows/ci.yaml +++ b/.github/workflows/ci.yaml @@ -1,17 +1,14 @@ name: Build on: - push: - branches: [ main ] - pull_request: - branches: [ main ] + push concurrency: group: ${{ github.workflow }}-${{ github.ref }} cancel-in-progress: true env: - CREUSOT_VERSION: v0.11.0 + CREUSOT_VERSION: master jobs: rust: @@ -65,4 +62,4 @@ jobs: run: cargo update --dry-run - name: Run Creusot - run: cargo creusot prove -- -Fsolutions + run: cargo creusot -- -Fsolutions diff --git a/.github/workflows/nightly.yaml b/.github/workflows/nightly.yaml index e94d432..72762e1 100644 --- a/.github/workflows/nightly.yaml +++ b/.github/workflows/nightly.yaml @@ -1,5 +1,4 @@ name: Nightly -# Note: this job only checks out the dev branch! (see `ref: dev`) on: schedule: - cron: '0 2 * * *' @@ -10,8 +9,6 @@ jobs: runs-on: ubuntu-latest steps: - uses: actions/checkout@v4 - with: - ref: dev - uses: ocaml/setup-ocaml@v3 with: @@ -44,10 +41,5 @@ jobs: cd ../creusot ./INSTALL - - name: Patch Cargo config for nightly - run: | - mkdir .cargo - echo -e '[patch.crates-io]\ncreusot-std = { path = "../creusot/creusot-std" }' > .cargo/config.toml - - name: Run Creusot run: cargo creusot -- -Fsolutions diff --git a/.vscode/settings.json b/.vscode/settings.json index 5399ada..49fdc9c 100644 --- a/.vscode/settings.json +++ b/.vscode/settings.json @@ -14,6 +14,7 @@ "overrideCommand": [ "cargo", "creusot", + "--only=coma", "--", "--message-format=json" ] diff --git a/Cargo.lock b/Cargo.lock index 6ac632d..8c430e8 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -2,15 +2,39 @@ # It is not intended for manual editing. version = 4 +[[package]] +name = "anyhow" +version = "1.0.102" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7f202df86484c868dbad7eaa557ef785d5c66295e41b460ef922eca0723b842c" + [[package]] name = "autocfg" version = "1.5.0" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "c08606f8c3cbf4ce6ec8e28fb0014a2c086708fe954eaa885384a6165172e7e8" +[[package]] +name = "bitflags" +version = "2.13.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b4388bee8683e3d04af747c73422af53102d2bd24d9eadb6cbc100baef4b43f8" + +[[package]] +name = "bumpalo" +version = "3.20.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "72f5acc6cb2ba439de613abc23857ec3d78374d8ed5ac84e9d11336e87da8649" + +[[package]] +name = "cfg-if" +version = "1.0.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9330f8b2ff13f34540b44e946ef35111825727b38d33286ef986142615121801" + [[package]] name = "creusot-std" -version = "0.11.0" +version = "0.12.0" dependencies = [ "creusot-std-proc", "num-rational", @@ -18,13 +42,144 @@ dependencies = [ [[package]] name = "creusot-std-proc" -version = "0.11.0" +version = "0.12.0" dependencies = [ + "pearlite-syn", "proc-macro2", "quote", "syn", + "uuid", +] + +[[package]] +name = "equivalent" +version = "1.0.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "877a4ace8713b0bcf2a4e7eec82529c029f1d0619886d18145fea96c3ffe5c0f" + +[[package]] +name = "foldhash" +version = "0.1.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d9c4f5dac5e15c24eb999c26181a6ca40b39fe946cbe4c263c7209467bc83af2" + +[[package]] +name = "futures-core" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7e3450815272ef58cec6d564423f6e755e25379b217b0bc688e295ba24df6b1d" + +[[package]] +name = "futures-task" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "037711b3d59c33004d3856fbdc83b99d4ff37a24768fa1be9ce3538a1cde4393" + +[[package]] +name = "futures-util" +version = "0.3.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "389ca41296e6190b48053de0321d02a77f32f8a5d2461dd38762c0593805c6d6" +dependencies = [ + "futures-core", + "futures-task", + "pin-project-lite", + "slab", +] + +[[package]] +name = "getrandom" +version = "0.4.2" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0de51e6874e94e7bf76d726fc5d13ba782deca734ff60d5bb2fb2607c7406555" +dependencies = [ + "cfg-if", + "libc", + "r-efi", + "wasip2", + "wasip3", +] + +[[package]] +name = "hashbrown" +version = "0.15.5" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9229cfe53dfd69f0609a49f65461bd93001ea1ef889cd5529dd176593f5338a1" +dependencies = [ + "foldhash", +] + +[[package]] +name = "hashbrown" +version = "0.17.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ed5909b6e89a2db4456e54cd5f673791d7eca6732202bbf2a9cc504fe2f9b84a" + +[[package]] +name = "heck" +version = "0.5.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "2304e00983f87ffb38b55b444b5e3b60a884b5d30c0fca7d82fe33449bbe55ea" + +[[package]] +name = "id-arena" +version = "2.3.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "3d3067d79b975e8844ca9eb072e16b31c3c1c36928edf9c6789548c524d0d954" + +[[package]] +name = "indexmap" +version = "2.14.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d466e9454f08e4a911e14806c24e16fba1b4c121d1ea474396f396069cf949d9" +dependencies = [ + "equivalent", + "hashbrown 0.17.1", + "serde", + "serde_core", +] + +[[package]] +name = "itoa" +version = "1.0.18" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8f42a60cbdf9a97f5d2305f08a87dc4e09308d1276d28c869c684d7777685682" + +[[package]] +name = "js-sys" +version = "0.3.100" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f2025f20d7a4fa7785846e7b63d10a76d3f1cee98ee5cb79ea59703f95e42162" +dependencies = [ + "cfg-if", + "futures-util", + "wasm-bindgen", ] +[[package]] +name = "leb128fmt" +version = "0.1.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "09edd9e8b54e49e587e4f6295a7d29c3ea94d469cb40ab8ca70b288248a81db2" + +[[package]] +name = "libc" +version = "0.2.186" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "68ab91017fe16c622486840e4c83c9a37afeff978bd239b5293d61ece587de66" + +[[package]] +name = "log" +version = "0.4.32" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "953f07c43838f8e6f9758cab68bf5bed85465e7587ebe0b823f1bcd81978ad3a" + +[[package]] +name = "memchr" +version = "2.8.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "6b947ae49db0d222b1dbc6b113ce7248a3fc3a6ca21b696717bfc000ba4484d8" + [[package]] name = "num-bigint" version = "0.4.6" @@ -64,6 +219,37 @@ dependencies = [ "autocfg", ] +[[package]] +name = "once_cell" +version = "1.21.4" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9f7c3e4beb33f85d45ae3e3a1792185706c8e16d043238c593331cc7cd313b50" + +[[package]] +name = "pearlite-syn" +version = "0.12.0" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "pin-project-lite" +version = "0.2.17" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a89322df9ebe1c1578d689c92318e070967d1042b512afbe49518723f4e6d5cd" + +[[package]] +name = "prettyplease" +version = "0.2.37" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "479ca8adacdd7ce8f1fb39ce9ecccbfe93a3f1344b3d0d97f20bc0196208f62b" +dependencies = [ + "proc-macro2", + "syn", +] + [[package]] name = "proc-macro2" version = "1.0.106" @@ -82,6 +268,72 @@ dependencies = [ "proc-macro2", ] +[[package]] +name = "r-efi" +version = "6.0.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "f8dcc9c7d52a811697d2151c701e0d08956f92b0e24136cf4cf27b57a6a0d9bf" + +[[package]] +name = "rustversion" +version = "1.0.22" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b39cdef0fa800fc44525c84ccb54a029961a8215f9619753635a9c0d2538d46d" + +[[package]] +name = "semver" +version = "1.0.28" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "8a7852d02fc848982e0c167ef163aaff9cd91dc640ba85e263cb1ce46fae51cd" + +[[package]] +name = "serde" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9a8e94ea7f378bd32cbbd37198a4a91436180c5bb472411e48b5ec2e2124ae9e" +dependencies = [ + "serde_core", +] + +[[package]] +name = "serde_core" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "41d385c7d4ca58e59fc732af25c3983b67ac852c1a25000afe1175de458b67ad" +dependencies = [ + "serde_derive", +] + +[[package]] +name = "serde_derive" +version = "1.0.228" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d540f220d3187173da220f885ab66608367b6574e925011a9353e4badda91d79" +dependencies = [ + "proc-macro2", + "quote", + "syn", +] + +[[package]] +name = "serde_json" +version = "1.0.150" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "e8014e44b4736ed0538adeecded0fce2a272f22dc9578a7eb6b2d9993c74cfb9" +dependencies = [ + "itoa", + "memchr", + "serde", + "serde_core", + "zmij", +] + +[[package]] +name = "slab" +version = "0.4.12" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c790de23124f9ab44544d7ac05d60440adc586479ce501c1d6d7da3cd8c9cf5" + [[package]] name = "syn" version = "2.0.117" @@ -105,3 +357,217 @@ name = "unicode-ident" version = "1.0.24" source = "registry+https://github.com/rust-lang/crates.io-index" checksum = "e6e4313cd5fcd3dad5cafa179702e2b244f760991f45397d14d4ebf38247da75" + +[[package]] +name = "unicode-xid" +version = "0.2.6" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ebc1c04c71510c7f702b52b7c350734c9ff1295c464a03335b00bb84fc54f853" + +[[package]] +name = "uuid" +version = "1.23.3" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "144d6b123cef80b301b8f72a9e2ca4370ddec21950d0a103dd22c437006d2db7" +dependencies = [ + "getrandom", + "js-sys", + "wasm-bindgen", +] + +[[package]] +name = "wasip2" +version = "1.0.3+wasi-0.2.9" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "20064672db26d7cdc89c7798c48a0fdfac8213434a1186e5ef29fd560ae223d6" +dependencies = [ + "wit-bindgen 0.57.1", +] + +[[package]] +name = "wasip3" +version = "0.4.0+wasi-0.3.0-rc-2026-01-06" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "5428f8bf88ea5ddc08faddef2ac4a67e390b88186c703ce6dbd955e1c145aca5" +dependencies = [ + "wit-bindgen 0.51.0", +] + +[[package]] +name = "wasm-bindgen" +version = "0.2.123" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "a254a4b10c19a76f09a27640e7ffbf9bc30bf67e16a3bf28aaefa4920fe81563" +dependencies = [ + "cfg-if", + "once_cell", + "rustversion", + "wasm-bindgen-macro", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-macro" +version = "0.2.123" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "24a40fc75b0ec6f3746ceb10d36f53a93dcd68a93b11b6445983945d79eba0dc" +dependencies = [ + "quote", + "wasm-bindgen-macro-support", +] + +[[package]] +name = "wasm-bindgen-macro-support" +version = "0.2.123" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "908f34bd9b9ce3d4caf07b72dfab63d61504d156856c6bd3cd87fa350cf3985b" +dependencies = [ + "bumpalo", + "proc-macro2", + "quote", + "syn", + "wasm-bindgen-shared", +] + +[[package]] +name = "wasm-bindgen-shared" +version = "0.2.123" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "7acbf7616c27b194bbb550bf77ed0c2c3e5b7fd1260a93082b95fb7f47959b92" +dependencies = [ + "unicode-ident", +] + +[[package]] +name = "wasm-encoder" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "990065f2fe63003fe337b932cfb5e3b80e0b4d0f5ff650e6985b1048f62c8319" +dependencies = [ + "leb128fmt", + "wasmparser", +] + +[[package]] +name = "wasm-metadata" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "bb0e353e6a2fbdc176932bbaab493762eb1255a7900fe0fea1a2f96c296cc909" +dependencies = [ + "anyhow", + "indexmap", + "wasm-encoder", + "wasmparser", +] + +[[package]] +name = "wasmparser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "47b807c72e1bac69382b3a6fb3dbe8ea4c0ed87ff5629b8685ae6b9a611028fe" +dependencies = [ + "bitflags", + "hashbrown 0.15.5", + "indexmap", + "semver", +] + +[[package]] +name = "wit-bindgen" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "d7249219f66ced02969388cf2bb044a09756a083d0fab1e566056b04d9fbcaa5" +dependencies = [ + "wit-bindgen-rust-macro", +] + +[[package]] +name = "wit-bindgen" +version = "0.57.1" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "1ebf944e87a7c253233ad6766e082e3cd714b5d03812acc24c318f549614536e" + +[[package]] +name = "wit-bindgen-core" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ea61de684c3ea68cb082b7a88508a8b27fcc8b797d738bfc99a82facf1d752dc" +dependencies = [ + "anyhow", + "heck", + "wit-parser", +] + +[[package]] +name = "wit-bindgen-rust" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b7c566e0f4b284dd6561c786d9cb0142da491f46a9fbed79ea69cdad5db17f21" +dependencies = [ + "anyhow", + "heck", + "indexmap", + "prettyplease", + "syn", + "wasm-metadata", + "wit-bindgen-core", + "wit-component", +] + +[[package]] +name = "wit-bindgen-rust-macro" +version = "0.51.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "0c0f9bfd77e6a48eccf51359e3ae77140a7f50b1e2ebfe62422d8afdaffab17a" +dependencies = [ + "anyhow", + "prettyplease", + "proc-macro2", + "quote", + "syn", + "wit-bindgen-core", + "wit-bindgen-rust", +] + +[[package]] +name = "wit-component" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "9d66ea20e9553b30172b5e831994e35fbde2d165325bec84fc43dbf6f4eb9cb2" +dependencies = [ + "anyhow", + "bitflags", + "indexmap", + "log", + "serde", + "serde_derive", + "serde_json", + "wasm-encoder", + "wasm-metadata", + "wasmparser", + "wit-parser", +] + +[[package]] +name = "wit-parser" +version = "0.244.0" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "ecc8ac4bc1dc3381b7f59c34f00b67e18f910c2c0f50015669dde7def656a736" +dependencies = [ + "anyhow", + "id-arena", + "indexmap", + "log", + "semver", + "serde", + "serde_derive", + "serde_json", + "unicode-xid", + "wasmparser", +] + +[[package]] +name = "zmij" +version = "1.0.21" +source = "registry+https://github.com/rust-lang/crates.io-index" +checksum = "b8848ee67ecc8aedbaf3e4122217aff892639231befc6a1b58d29fff4c2cabaa" diff --git a/Cargo.toml b/Cargo.toml index b6d02df..fa416e0 100644 --- a/Cargo.toml +++ b/Cargo.toml @@ -4,7 +4,7 @@ version = "0.1.0" edition = "2024" [dependencies] -creusot-std = { version = "0.11.0-dev", features = ["sc-drf"] } +creusot-std = { version = "0.12.0", features = ["sc-drf"] } [features] solutions = [] diff --git a/README.md b/README.md index eade152..94e6226 100644 --- a/README.md +++ b/README.md @@ -62,7 +62,7 @@ on Github's servers, with a free quota of 120h monthly per user. ## Usage -To get started, in the terminal, run `cargo creusot prove` to check that it works. +To get started, in the terminal, run `cargo creusot` to check that it works. You should see some checkmarks in the output indicating that the initial examples have been proved correct. @@ -72,10 +72,12 @@ If you use VS Code with Rust Analyzer (*e.g.*, if you are on Codespaces), this t run SMT solvers to attempt to prove that the corresponding function satisfies its specification. -- Troubleshooting: If nothing happens in ~10 seconds after `cargo creusot` or `cargo creusot prove`, you can try to relaunch the LSP server with the following commands: `Ctrl+P` (or click the search bar at the top) > Write "> Creusot" (with the `>`!) > Select "Creusot: Restart language server"". +- Troubleshooting: If nothing happens in ~10 seconds after `cargo creusot`, you can try to relaunch the LSP server with the following commands: `Ctrl+P` (or click the search bar at the top) > Write "> Creusot" (with the `>`!) > Select "Creusot: Restart language server"". ### From the command line -- Run `cargo creusot` for type-checking and compilation to Coma (quick, but no proofs). -- Run `cargo creusot prove` to run Why3find and dispatch proof obligations to SMT solvers. (This command also implies `cargo creusot` so you don't need to do it separately.) -- Run `cargo creusot prove $NAME` to only try proving function `$NAME`. For example, `cargo creusot prove gnome_sort`. +- Run `cargo creusot` to run the whole pipeline: compile to Coma and run provers. +- Run `cargo creusot --prove $NAME` to only try proving function `$NAME`. For example, `cargo creusot --prove gnome_sort`. + This will run the Coma compiler as well to make sure the proofs are up to date. +- Run `cargo creusot --only=coma` to just type-check and compile to Coma. +- Run `cargo creusot --only=prove` to just run provers (the Coma code may be out of date!) diff --git a/src/ex0_examples.rs b/src/ex0_examples.rs index add5bd6..3388d1e 100644 --- a/src/ex0_examples.rs +++ b/src/ex0_examples.rs @@ -1,7 +1,7 @@ //! A couple of short exercises. //! //! Objective: remove all `#[trusted]` with an "Exercise: ..." comment -//! and make `cargo creusot prove` happy! +//! and make `cargo creusot` happy! //! //! Some exercises make use of the `creusot_std` API, which you can //! browse here: https://doc.creusot.rs/creusot_std/ diff --git a/src/solutions/ex0_examples.rs b/src/solutions/ex0_examples.rs index 5b03a90..b33483b 100644 --- a/src/solutions/ex0_examples.rs +++ b/src/solutions/ex0_examples.rs @@ -198,8 +198,8 @@ pub fn interior_mut() { unsafe { 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 }); + b1.set(ghost! { &mut *perm }, 1); + let _result = b2.take(ghost! { &mut *perm }); proof_assert! { _result == 1i32 }; } } diff --git a/src/solutions/ex3_parallel_add.rs b/src/solutions/ex3_parallel_add.rs index 293330e..eee5e1a 100644 --- a/src/solutions/ex3_parallel_add.rs +++ b/src/solutions/ex3_parallel_add.rs @@ -7,7 +7,10 @@ use creusot_std::{ logic::{Id, ra::excl::Excl}, prelude::*, std::{ - sync::{atomic::Ordering, atomic_sc::AtomicI32, committer::Committer}, + sync::{ + atomic_sc::{AtomicI32, ordering::SeqCst}, + committer::Committer, + }, thread::{self, JoinHandleExt}, }, }; @@ -15,7 +18,7 @@ use creusot_std::{ declare_namespace! { PARALLEL_ADD } struct ParallelAddAtomicInv { - own: Box>, + own: Perm, auth1: Authority>>, auth2: Authority>>, } @@ -24,9 +27,13 @@ impl Protocol for ParallelAddAtomicInv { type Public = (AtomicI32, Id, Id); #[logic(inline)] - fn protocol(self, data: (AtomicI32, Id, Id)) -> bool { + fn public(self) -> Self::Public { + (*self.own.ward(), self.auth1.id(), self.auth2.id()) + } + + #[logic(inline)] + fn protocol(self) -> bool { pearlite! { - data == (*self.own.ward(), self.auth1.id(), self.auth2.id()) && self.own.val()@ == if self.auth1@ == Some(Excl(true)) { 2 } else { 0 } + if self.auth2@ == Some(Excl(true)) { 2 } else { 0 } @@ -55,7 +62,6 @@ pub fn parallel_add() -> i32 { auth1: auth1.into_inner(), auth2: auth2.into_inner() }), - snapshot!((atomic, frag1.id(), frag2.id())), snapshot!(PARALLEL_ADD()), ); @@ -71,7 +77,7 @@ pub fn parallel_add() -> i32 { let t1 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| { + ghost! { |c: &mut Committer<_, _, SeqCst, SeqCst>| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth1.update(*frag1, snapshot!((Some(Excl(true)), Some(Excl(true))))); c.shoot_load(&inv.own); @@ -84,7 +90,7 @@ pub fn parallel_add() -> i32 { let t2 = s.spawn(move |tokens: Ghost| { atomic.fetch_add( 2, - ghost! { |c: &mut Committer<_, _, Ordering::SeqCst, Ordering::SeqCst>| { + ghost! { |c: &mut Committer<_, _, SeqCst, SeqCst>| { inv.open(tokens.into_inner(), |inv: &mut ParallelAddAtomicInv| { inv.auth2.update(*frag2, snapshot!((Some(Excl(true)), Some(Excl(true))))); c.shoot_load(&inv.own);