Upgrade Verus version (#484)

Signed-off-by: Xudong Sun <xudongs3@illinois.edu>

Author: marshtompsxd

.github/workflows/ci.yml

@@ -21,7 +21,7 @@ jobs:
         with:
           repository: verus-lang/verus
           path: verus
-          ref: 1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          ref: 8e24346e9a93e25bca6b66505f4007645118df43
       - name: Move Verus
         run: mv verus ../verus
       - name: Install Rust toolchain
@@ -44,7 +44,7 @@ jobs:
         with:
           repository: verus-lang/verus
           path: verus
-          ref: 1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          ref: 8e24346e9a93e25bca6b66505f4007645118df43
       - name: Move Verus
         run: mv verus ../verus
       - name: Install Rust toolchain
@@ -67,7 +67,7 @@ jobs:
         with:
           repository: verus-lang/verus
           path: verus
-          ref: 1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          ref: 8e24346e9a93e25bca6b66505f4007645118df43
       - name: Move Verus
         run: mv verus ../verus
       - name: Install Rust toolchain
@@ -90,7 +90,7 @@ jobs:
         with:
           repository: verus-lang/verus
           path: verus
-          ref: 1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          ref: 8e24346e9a93e25bca6b66505f4007645118df43
       - name: Move Verus
         run: mv verus ../verus
       - name: Install Rust toolchain
@@ -113,7 +113,7 @@ jobs:
         with:
           repository: verus-lang/verus
           path: verus
-          ref: 1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          ref: 8e24346e9a93e25bca6b66505f4007645118df43
       - name: Move Verus
         run: mv verus ../verus
       - name: Install Rust toolchain
@@ -147,7 +147,7 @@ jobs:
         with:
           repository: verus-lang/verus
           path: verus
-          ref: 1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          ref: 8e24346e9a93e25bca6b66505f4007645118df43
       - 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=1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8 .
-          docker tag ghcr.io/${{ env.IMAGE_NAME }}/verus:latest ghcr.io/${{ env.IMAGE_NAME }}/verus:1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          docker build -t ghcr.io/${{ env.IMAGE_NAME }}/verus:latest --build-arg VERUS_VER=8e24346e9a93e25bca6b66505f4007645118df43 .
+          docker tag ghcr.io/${{ env.IMAGE_NAME }}/verus:latest ghcr.io/${{ env.IMAGE_NAME }}/verus:8e24346e9a93e25bca6b66505f4007645118df43
       - name: Push Verus image
         run: |
           docker push ghcr.io/${{ env.IMAGE_NAME }}/verus:latest
-          docker push ghcr.io/${{ env.IMAGE_NAME }}/verus:1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8
+          docker push ghcr.io/${{ env.IMAGE_NAME }}/verus:8e24346e9a93e25bca6b66505f4007645118df43

README.md

@@ -7,7 +7,7 @@ Anvil is a framework for building and formally verifying Kubernetes controllers.
 
 So far, we have built and verified three Kubernetes controllers (for managing ZooKeeper, RabbitMQ and FluentBit) using Anvil. We used the [Pravega ZooKeeper operator](https://github.com/pravega/zookeeper-operator), [official RabbitMQ operator](https://github.com/rabbitmq/cluster-operator) and [official Fluent operator](https://github.com/fluent/fluent-operator) as references when building our controllers. We are now using Anvil to build (and verify) more controllers, including Kubernetes built-in controllers.
 
-For now, the best way to use Anvil is to download the source code and import its components into your controller projects, like what we did for our controller [examples](src/controller_examples/). To use Anvil, you will need to install [Verus](https://github.com/verus-lang/verus) (See the [installation instructions](https://github.com/verus-lang/verus/blob/main/INSTALL.md)). Currently Anvil uses Verus version `1a9e3c577847b4a230ff7fe15b5b080a71cdf3c8`.
+For now, the best way to use Anvil is to download the source code and import its components into your controller projects, like what we did for our controller [examples](src/controller_examples/). To use Anvil, you will need to install [Verus](https://github.com/verus-lang/verus) (See the [installation instructions](https://github.com/verus-lang/verus/blob/main/INSTALL.md)). Currently Anvil uses Verus version `8e24346e9a93e25bca6b66505f4007645118df43`.
 
 If you want to reproduce the results in the OSDI'24 paper "Anvil: Verifying Liveness of Cluster Management Controllers", please refer to the [osdi24](https://github.com/vmware-research/verifiable-controllers/tree/osdi24) branch.
 

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.73.0"
+channel = "1.76.0"

src/vstd_ext/string_map.rs

@@ -58,7 +58,7 @@ impl StringMap {
             v.is_Some() ==> v.get_Some_0()@ == self@[key@],
     {
         match self.inner.get(key.as_rust_string_ref()) {
-            Some(v) => Some(StrSlice::from_rust_str(v)),
+            Some(v) => Some(v),
             None => None,
         }
     }