Upgrade Verus version for time-expanded feature (#354)

Signed-off-by: Xudong Sun <[email protected]>

.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

.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

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 \
   "$@"

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
 
 # =============================================================================
 

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"

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! {

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<K, V>()
             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<K, V>(m: Map<K, V>)
-    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::<V>::empty());
-    }
-}
-
 }