From 130f10201fc6f5bcaa77e38621b52cbdaaacd307 Mon Sep 17 00:00:00 2001 From: marshtompsxd Date: Tue, 17 Oct 2023 16:42:45 -0500 Subject: [PATCH] Upgrade Verus version for time-expanded feature (#354) Signed-off-by: Xudong Sun --- .github/workflows/ci.yml | 8 ++--- .github/workflows/controller-e2e-test.yml | 43 ----------------------- .github/workflows/verus-build.yml | 6 ++-- build.sh | 1 - docker/controller/Dockerfile | 3 +- rust-toolchain.toml | 2 +- src/temporal_logic/rules.rs | 2 +- src/vstd_ext/map_lib.rs | 35 +----------------- 8 files changed, 12 insertions(+), 88 deletions(-) delete mode 100644 .github/workflows/controller-e2e-test.yml diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml index e856bfd92..b1b7a54af 100644 --- a/.github/workflows/ci.yml +++ b/.github/workflows/ci.yml @@ -21,7 +21,7 @@ jobs: with: repository: verus-lang/verus path: verus - ref: 69243cb3b7990397c289d8a156576da3675a6b36 + ref: 8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 - name: Move Verus run: mv verus ../verus - name: Install Rust toolchain @@ -44,7 +44,7 @@ jobs: with: repository: verus-lang/verus path: verus - ref: 69243cb3b7990397c289d8a156576da3675a6b36 + ref: 8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 - name: Move Verus run: mv verus ../verus - name: Install Rust toolchain @@ -67,7 +67,7 @@ jobs: with: repository: verus-lang/verus path: verus - ref: 69243cb3b7990397c289d8a156576da3675a6b36 + ref: 8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 - name: Move Verus run: mv verus ../verus - name: Install Rust toolchain @@ -90,7 +90,7 @@ jobs: with: repository: verus-lang/verus path: verus - ref: 69243cb3b7990397c289d8a156576da3675a6b36 + ref: 8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 - name: Move Verus run: mv verus ../verus - name: Install Rust toolchain diff --git a/.github/workflows/controller-e2e-test.yml b/.github/workflows/controller-e2e-test.yml deleted file mode 100644 index b3a415391..000000000 --- a/.github/workflows/controller-e2e-test.yml +++ /dev/null @@ -1,43 +0,0 @@ -name: Controller e2e test -run-name: e2e tests run by ${{ github.actor }} -on: - workflow_dispatch: -jobs: - rabbitmq-e2e-test: - runs-on: ubuntu-20.04 - steps: - - uses: actions/checkout@v2 - - name: Setup Go - uses: actions/setup-go@v2 - with: - go-version: "^1.20" - - name: Install kind - run: go install sigs.k8s.io/kind@v0.18.0 - - name: Install Rust toolchain - run: | - curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y - - name: Create kind cluster - run: kind create cluster --config=./deploy/kind.yaml - - name: Deploy rabbitmq controller - run: ./deploy.sh rabbitmq remote - - name: Run rabbitmq e2e tests - run: cd e2e && cargo run -- rabbitmq - zookeeper-e2e-test: - runs-on: ubuntu-20.04 - steps: - - uses: actions/checkout@v2 - - name: Setup Go - uses: actions/setup-go@v2 - with: - go-version: "^1.20" - - name: Install kind - run: go install sigs.k8s.io/kind@v0.20.0 - - name: Install Rust toolchain - run: | - curl --proto '=https' --tlsv1.2 --retry 10 --retry-connrefused -fsSL "https://sh.rustup.rs" | sh -s -- --default-toolchain none -y - - name: Create kind cluster - run: kind create cluster --config=./deploy/kind.yaml - - name: Deploy zookeeper controller - run: ./deploy.sh zookeeper remote - - name: Run zookeeper e2e tests - run: cd e2e && cargo run -- zookeeper diff --git a/.github/workflows/verus-build.yml b/.github/workflows/verus-build.yml index 8519fa05a..9e81b6afc 100644 --- a/.github/workflows/verus-build.yml +++ b/.github/workflows/verus-build.yml @@ -17,9 +17,9 @@ jobs: - name: Build Verus image run: | cd docker/verus - docker build -t ghcr.io/${{ env.IMAGE_NAME }}/verus:latest --build-arg VERUS_VER=69243cb3b7990397c289d8a156576da3675a6b36 . - docker tag ghcr.io/${{ env.IMAGE_NAME }}/verus:latest ghcr.io/${{ env.IMAGE_NAME }}/verus:69243cb3b7990397c289d8a156576da3675a6b36 + docker build -t ghcr.io/${{ env.IMAGE_NAME }}/verus:latest --build-arg VERUS_VER=8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 . + docker tag ghcr.io/${{ env.IMAGE_NAME }}/verus:latest ghcr.io/${{ env.IMAGE_NAME }}/verus:8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 - name: Push Verus image run: | docker push ghcr.io/${{ env.IMAGE_NAME }}/verus:latest - docker push ghcr.io/${{ env.IMAGE_NAME }}/verus:69243cb3b7990397c289d8a156576da3675a6b36 + docker push ghcr.io/${{ env.IMAGE_NAME }}/verus:8a5eed3c564d7a3b0d865a1c8eb28c57b0e84137 diff --git a/build.sh b/build.sh index 127e7c41c..b7c040c18 100755 --- a/build.sh +++ b/build.sh @@ -16,6 +16,5 @@ cargo build cd .. "$rv" -L dependency=deps_hack/target/debug/deps \ --extern=deps_hack="deps_hack/target/debug/libdeps_hack.rlib" \ - --expand-errors \ --compile \ "$@" diff --git a/docker/controller/Dockerfile b/docker/controller/Dockerfile index 0113fa6f9..215a4d52e 100644 --- a/docker/controller/Dockerfile +++ b/docker/controller/Dockerfile @@ -9,7 +9,8 @@ COPY . . RUN apt install -y pkg-config libssl-dev -RUN VERUS_DIR=/verus ./build.sh ${APP}_controller.rs --no-verify --time -o controller +RUN VERUS_DIR=/verus ./build.sh ${APP}_controller.rs --no-verify --time +RUN mv /anvil/src/${APP}_controller /anvil/src/controller # ============================================================================= diff --git a/rust-toolchain.toml b/rust-toolchain.toml index 54aaaa4ff..d9e3f3361 100644 --- a/rust-toolchain.toml +++ b/rust-toolchain.toml @@ -1,4 +1,4 @@ # this should be synchronized with the Verus version, since we need to combine # k8s compiled with rustc and our own code compiled with rust-verify.sh [toolchain] -channel = "1.68.0" +channel = "1.70.0" diff --git a/src/temporal_logic/rules.rs b/src/temporal_logic/rules.rs index 99cbc9fc7..b72e35f2f 100644 --- a/src/temporal_logic/rules.rs +++ b/src/temporal_logic/rules.rs @@ -2,8 +2,8 @@ // SPDX-License-Identifier: MIT #![allow(unused_imports)] use crate::temporal_logic::defs::*; -use crate::vstd_ext::map_lib::*; use vstd::function::*; +use vstd::map_lib::*; use vstd::prelude::*; verus! { diff --git a/src/vstd_ext/map_lib.rs b/src/vstd_ext/map_lib.rs index f2f9a1a8a..7d16d662b 100644 --- a/src/vstd_ext/map_lib.rs +++ b/src/vstd_ext/map_lib.rs @@ -1,7 +1,7 @@ // Copyright 2022 VMware, Inc. // SPDX-License-Identifier: MIT #![allow(unused_imports)] -use vstd::{map_lib::*, prelude::*, seq_lib::*, set_lib::*, set::*}; +use vstd::{map_lib::*, prelude::*, seq_lib::*, set::*, set_lib::*}; verus! { @@ -25,37 +25,4 @@ pub proof fn union_prefer_right_self_changes_nothing() map.union_prefer_right(map) =~= map, {} -// TODO: We will use the Verus native lemma_values_finite once we update to the most recent Verus. -pub proof fn lemma_values_finite(m: Map) - requires m.dom().finite(), - ensures m.values().finite(), - decreases m.len(), -{ - if m.len() > 0 { - let k = m.dom().choose(); - let v = m[k]; - let m1 = m.remove(k); - assert(m.contains_key(k)); - assert(m.contains_value(v)); - assert_sets_equal!(m.values() == m1.values().insert(v), v0 => { - if m.values().contains(v0) { - assert(m1.values().insert(v).contains(v0)); - } - if m1.values().insert(v).contains(v0) { - if v0 == v { - assert(m.contains_value(v)); - assert(m.values().contains(v0)); - } else { - assert(m.values().contains(v0)); - } - } - }); - assert(m1.len() < m.len()); - lemma_values_finite(m1); - axiom_set_insert_finite(m1.values(), v); - } else { - assert(m.values() =~= Set::::empty()); - } -} - }