Update to use the official Verus repo

Author: zhengyao-lin

.github/workflows/build.yml

@@ -10,17 +10,36 @@ env:
   CARGO_TERM_COLOR: always
 
 jobs:
-  build:
+  verified-build:
     runs-on: ubuntu-latest
 
     steps:
     - name: Checkout
       uses: actions/checkout@v4
       with:
         submodules: true
-    - name: Build Debug
-      run: source tools/activate.sh && vargo build
-    - name: Build Release
-      run: source tools/activate.sh && vargo build --release
+    - name: Build debug
+      run: source tools/activate.sh && cargo verus build
+    - name: Build debug with tracing
+      run: source tools/activate.sh && cargo verus build --features trace
+    - name: Build release
+      run: source tools/activate.sh && cargo verus build --release
+    - name: Build release with aws-lc feature
+      run: source tools/activate.sh && cargo verus build --release --features aws-lc
     - name: Test
-      run: source tools/activate.sh && vargo test --workspace
+      run: source tools/activate.sh && cargo test --workspace
+
+  unverified-build:
+    runs-on: ubuntu-latest
+
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v4
+      with:
+        submodules: true
+    - name: Build debug
+      run: cargo build
+    - name: Build release
+      run: cargo build --release
+    - name: Build release with aws-lc feature
+      run: cargo build --release --features aws-lc

.gitmodules

@@ -1,6 +1,6 @@
 [submodule "deps/verus"]
 	path = deps/verus
-	url = https://github.com/zhengyao-lin/verus.git
+	url = https://github.com/verus-lang/verus.git
 	branch = x509
 [submodule "deps/libcrux"]
 	path = deps/libcrux

README.md

@@ -18,26 +18,25 @@ To build, first run (Bash or Zsh)
 ```
 . tools/activate.sh
 ```
-This will first compile a vendored version of Verus, and then
-provide a command `vargo` with the same usage as `cargo`.
+This will first compile a vendored version of Verus and add relevant binaries to `PATH`.
 
 To verify and build the entire project, run
 ```
-vargo build --release
+cargo verus build --release
 ```
 Then use `target/release/verdict` to validate certificate chains or run benchmarks.
 See `target/release/verdict --help` for details.
 
-By default, we only use crypto primitives that are verified from [libcrux](https://github.com/cryspen/libcrux) and [aws-lc-rs](https://github.com/aws/aws-lc-rs).
+By default, we only use *verified* crypto primitives from [libcrux](https://github.com/cryspen/libcrux) and [aws-lc-rs](https://github.com/aws/aws-lc-rs).
 To use primitives entirely from `aws-lc-rs` which might have better performance but include unverified signature checking for RSA and ECDSA P-256,
 compile with
 ```
-vargo build --release --features aws-lc
+cargo verus build --release --features aws-lc
 ```
 
 To run some sanity checks
 ```
-vargo test --workspace
+cargo test --workspace
 ```
 
 ### Build without verification
@@ -56,7 +55,7 @@ which should work like in a normal Rust package, with all verification annotatio
 
 Use
 ```
-RUSTFLAGS="--cfg trace" vargo build [--release]
+cargo verus build [--release] --features trace
 ```
 to build a version with tracing enabled.
 This will print out every successfully parsed construct and the result of each predicate in the policy DSL.

deps/verus

@@ -202,6 +202,7 @@ impl<C: Combinator> Repeat<C> where
                 },
                 offset < s@.len() ==>
                     (self@.spec_parse(s@.subrange(offset as int, s@.len() as int)) is Err ==> self@.spec_parse(s@) is Err),
+            decreases s.len() - offset
         {
             let (n, v) = self.0.parse(slice_subrange(s, offset, s.len()))?;
             if n == 0 {
@@ -240,6 +241,7 @@ impl<C: Combinator> Repeat<C> where
                 &&& self@.spec_serialize(old(v)@) matches Ok(s) ==> n == (len + s.len()) && data@
                     =~= seq_splice(old(data)@, (pos + len) as usize, s)
             },
+        decreases old(v)@.len()
     {
         if pos > usize::MAX - len || pos + len >= data.len() {
             return Err(SerializeError::InsufficientBuffer);

deps/vest/src/regular/repeat.rs

@@ -194,6 +194,7 @@ pub fn set_range<'a>(data: &mut Vec<u8>, i: usize, input: &[u8])
             forall|k| i + input@.len() <= k < data@.len() ==> data@[k] == old(data)@[k],
             0 <= i <= i + j <= i + input@.len() <= data@.len() <= usize::MAX,
             forall|k| 0 <= k < j ==> data@[i + k] == input@[k],
+        decreases input.len() - j
     {
         data.set(i + j, *slice_index_get(input, j));
         j = j + 1
@@ -249,6 +250,7 @@ pub exec fn init_vec_u8(n: usize) -> (res: Vec<u8>)
         invariant
             0 <= i <= n,
             ret@.len() == i,
+        decreases n - i
     {
         ret.push(0);
         assert(ret@[i as int] == 0);

deps/vest/src/utils.rs

@@ -1,2 +1,2 @@
 [toolchain]
-channel = "1.82.0"
+channel = "1.86.0"

rust-toolchain.toml

@@ -1,13 +1,6 @@
 # Usage: source this script at the root of the repo
 
-# Similar to how Verus's internal vargo would work
-# https://github.com/verus-lang/verus/blob/main/tools/activate
-
-unset -f cargo 2>/dev/null || true
-unset -f vargo 2>/dev/null || true
-
 REPO_ROOT=$(pwd)
-REAL_CARGO="$(which cargo)"
 
 git submodule update --init
 
@@ -18,16 +11,4 @@ rustup toolchain install &&
 source ../tools/activate &&
 vargo build --release) || return 1
 
-# Build verusc
-(cd "tools/verusc" && cargo build --release) || return 1
-
-vargo() {
-    RUSTC_WRAPPER="$REPO_ROOT/tools/verusc/target/release/verusc" "$REAL_CARGO" "$@"
-}
-
-cargo() {
-    echo You have activated the build environment of Verus, so it is likely that
-    echo you want to use \`vargo\` instead of \`cargo\`. Restart the shell to disable.
-}
-
 export PATH="$REPO_ROOT/deps/verus/source/target-verus/release:$PATH"

tools/activate.sh

@@ -24,3 +24,4 @@ rand = "0.8.5"
 [features]
 default = []
 aws-lc = ["verdict/aws-lc"]
+trace = ["verdict/trace"]

verdict-bin/Cargo.toml

@@ -14,6 +14,10 @@ der = { version = "0.7.9", features = [ "alloc", "oid" ] }
 base64 = "0.22.1"
 paste = "1.0.15"
 
+[features]
+default = []
+trace = []
+
 [package.metadata.verus]
 verify = true