Use the official Verus repo and cargo-verus

.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/vest/src/regular/repeat.rs

@@ -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/utils.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);

rust-toolchain.toml

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

tools/activate.sh

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

verdict-bin/Cargo.toml

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

verdict-parser/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
 

verdict-parser/src/asn1/base128.rs

@@ -118,7 +118,7 @@ impl Base128UInt {
     /// Serialize v in base-128 encoding
     /// last_byte is true iff the encoding should have the highest bit of the last byte set to 0
     closed spec fn spec_serialize_helper(v: UInt, last_byte: bool) -> Seq<u8>
-        decreases v via Self::spec_serialize_dereases
+        decreases v via Self::spec_serialize_decreases
     {
         if v == 0 {
             if last_byte {
@@ -289,8 +289,7 @@ impl Base128UInt {
     }
 
     #[via_fn]
-    proof fn spec_serialize_dereases(v: UInt, last_byte: bool)
-    {
+    proof fn spec_serialize_decreases(v: UInt, last_byte: bool) {
         assert(v != 0 ==> v >> 7 < v) by (bit_vector);
     }
 
@@ -467,6 +466,7 @@ impl Base128UInt {
             invariant
                 0 <= len <= s.len(),
                 Self::all_high_8_bit_set(s@.take(len as int)),
+            decreases s.len() - len
         {
             len = len + 1;
 
@@ -512,13 +512,15 @@ impl Base128UInt {
 
     /// TODO: change this to a non-recursive function
     #[inline(always)]
-    fn serialize_helper(v: UInt) -> (r: Vec<u8>)
+    fn serialize_helper(v: u64) -> (r: Vec<u8>)
         ensures r@ == Self::spec_serialize_helper(v, false)
+        decreases v
     {
         if v == 0 {
             Vec::with_capacity(4) // usually OID arcs fit in 4 bytes
         } else {
             // Add the lowest 7 bits with the highest bit set to 0
+            assert(v != 0 ==> v >> 7 < v) by (bit_vector);
             let mut r = Self::serialize_helper(v >> 7);
             let ghost old_r = r@;
 
@@ -591,6 +593,8 @@ impl Combinator for Base128UInt {
                 !Self::is_high_8_bit_set(s@[len - 1]),
                 Self::spec_parse_helper(s@.take(i as int), false).is_some(),
                 v == Self::spec_parse_helper(s@.take(i as int), false).unwrap(),
+
+            decreases len - 1 - i
         {
             assert(s@.take(i + 1).drop_last() == s@.take(i as int));
             assert(Self::is_high_8_bit_set(s@.take(len - 1)[i as int]));

verdict-parser/src/asn1/bounds.rs

@@ -262,6 +262,7 @@ pub fn min_num_bytes_unsigned_exec(v: UInt) -> (res: UInt)
         invariant
             0 <= n <= uint_size!(),
             fits_n_bytes_unsigned!(v, n),
+        decreases n
     {
         if !fits_n_bytes_unsigned!(v, n - 1) {
             return n;
@@ -286,6 +287,7 @@ pub fn min_num_bytes_signed_exec(v: Int) -> (res: UInt)
         invariant
             0 <= n <= uint_size!(),
             fits_n_bytes_signed!(v, n),
+        decreases n
     {
         if !fits_n_bytes_signed!(v, n - 1) {
             assert(v == 0 && !fits_n_bytes_signed!(v, n - 1) ==> n == 1) by (bit_vector);

verdict-parser/src/asn1/var_int.rs

@@ -280,6 +280,7 @@ impl Combinator for VarUInt {
 
                 // At each iteration, res is the parse result of a suffix of s
                 res == Self((len - i) as usize).spec_parse(s@.skip(i as int)).unwrap().1,
+            decreases i
         {
             let byte = s[i - 1];
 
@@ -359,6 +360,7 @@ impl Combinator for VarUInt {
                     (pos + i) as usize,
                     Self((len - i) as usize).spec_serialize(v & n_byte_max_unsigned!(len - i)).unwrap(),
                 ),
+            decreases i
         {
             let byte = get_nth_byte!(v, len - i);
 

verdict-parser/src/common/base64.rs

@@ -380,6 +380,7 @@ impl Combinator for Base64 {
 
                 Self::spec_parse_helper(s@.skip(i as int)) is Err ==>
                     Self::spec_parse_helper(s@) is Err,
+            decreases len - i
         {
             assert(len - i == s@.skip(i as int).len());
 
@@ -458,6 +459,7 @@ impl Combinator for Base64 {
 
                 // Self::spec_serialize_helper(v@.skip(i as int)) is Err ==>
                 //     Self::spec_serialize_helper(v@) is Err,
+            decreases len - i
         {
             let v1 = v[i];
             let v2 = if len - i > 1 { v[i + 1] } else { 0 };

verdict-parser/src/common/repeat.rs

@@ -158,6 +158,8 @@ impl<C: Combinator> Repeat<C> where
                     res@ =~= old(res)@ + v
             },
             r is Err ==> self@.spec_parse(s@) is Err
+
+        decreases s.len(),
     {
         if s.len() == 0 {
             return Ok(());
@@ -187,6 +189,8 @@ 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);

verdict-parser/src/common/wrapped.rs

@@ -176,14 +176,14 @@ macro_rules! wrap_combinator_impls {
                 type SpecResult = $spec_result;
 
                 // $inner_expr.view().spec_parse(s)
-                closed spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>;
+                uninterp spec fn spec_parse(&self, s: Seq<u8>) -> Result<(usize, Self::SpecResult), ()>;
 
                 // $inner_expr.view().spec_parse_wf(s)
                 #[verifier::external_body]
                 proof fn spec_parse_wf(&self, s: Seq<u8>) {}
 
                 // $inner_expr.view().spec_serialize(v)
-                closed spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>;
+                uninterp spec fn spec_serialize(&self, v: Self::SpecResult) -> Result<Seq<u8>, ()>;
             }
 
             impl SecureSpecCombinator for $name {
@@ -212,7 +212,7 @@ macro_rules! wrap_combinator_impls {
                 type Result<$lt> = $result;
                 type Owned =  $owned;
 
-                closed spec fn spec_length(&self) -> Option<usize>;
+                uninterp spec fn spec_length(&self) -> Option<usize>;
 
                 #[verifier::external_body]
                 fn length(&self) -> Option<usize> {
@@ -230,8 +230,8 @@ macro_rules! wrap_combinator_impls {
                 fn parse<'a>(&self, s: &'a [u8]) -> (res: Result<(usize, Self::Result<'a>), ParseError>) {
                     $(let $field_name: $field_type = self.$field_name;)*
                     let res = $inner_expr.parse(s);
-                    #[cfg(trace)] {
-                        use polyfill::*;
+                    #[cfg(feature = "trace")] {
+                        use verdict_polyfill::*;
                         eprintln_join!("[", stringify!($name), "] ", format_dbg(&res));
                     }
                     res

verdict-parser/src/x509/oid.rs

@@ -151,7 +151,7 @@ macro_rules! spec_oid {
 pub use spec_oid;
 
 /// Used to suppress Verus warning about broadcast missing triggers
-pub closed spec fn lemma_disjoint_trigger() -> bool;
+pub uninterp spec fn lemma_disjoint_trigger() -> bool;
 
 /// Macro to generate a lemma that states the disjointness of a list of spec terms
 /// NOTE: the disjointness of the provided terms are trusted

verdict-polyfill/src/lib.rs

@@ -161,8 +161,8 @@ pub fn result_or<T, E, E2>(result: Result<T, E>, default: Result<T, E2>) -> (res
 
 /// Currently we do not have a specification in Verus for UTF-8
 /// so we just assume the implementation of `from_utf8` is correct
-pub closed spec fn spec_parse_utf8(s: Seq<u8>) -> Option<Seq<char>>;
-pub closed spec fn spec_serialize_utf8(s: Seq<char>) -> Seq<u8>;
+pub uninterp spec fn spec_parse_utf8(s: Seq<u8>) -> Option<Seq<char>>;
+pub uninterp spec fn spec_serialize_utf8(s: Seq<char>) -> Seq<u8>;
 
 #[verifier::external_body]
 pub proof fn spec_utf8_parse_serialize_roundtrip(buf: Seq<u8>)
@@ -191,7 +191,7 @@ pub fn str_to_utf8(s: &str) -> (res: &[u8])
 }
 
 /// We trust the implementation of `u64::to_string` for now
-pub closed spec fn spec_u64_to_string(x: u64) -> (res: Seq<char>);
+pub uninterp spec fn spec_u64_to_string(x: u64) -> (res: Seq<char>);
 
 #[verifier::external_body]
 pub fn char_to_string(c: char) -> (res: String)
@@ -233,6 +233,7 @@ pub fn vec_map<T, U>(v: &Vec<T>, f: impl Fn(&T) -> U) -> (res: Vec<U>)
             0 <= j <= v.len(),
             j == res.len(),
             forall|i| #![trigger v[i]] 0 <= i < j ==> call_ensures(f, (&v[i],), #[trigger] res[i]),
+        decreases v.len() - j
     {
         res.push(f(&v[j]));
         j += 1;
@@ -509,8 +510,8 @@ pub fn eprintln_debug<T: Debug>(s: T) {
 #[verifier::external_body]
 pub struct CharsIter<'a>(std::str::Chars<'a>);
 
-pub closed spec fn spec_chars_iter_str<'a>(iter: CharsIter<'a>) -> Seq<char>;
-pub closed spec fn spec_chars_iter_index<'a>(iter: CharsIter<'a>) -> int;
+pub uninterp spec fn spec_chars_iter_str<'a>(iter: CharsIter<'a>) -> Seq<char>;
+pub uninterp spec fn spec_chars_iter_index<'a>(iter: CharsIter<'a>) -> int;
 
 #[verifier::external_body]
 pub fn chars_iter_next<'a>(iter: &mut CharsIter<'a>) -> (res: Option<char>)

verdict-rspec/src/lib.rs

@@ -721,7 +721,7 @@ fn get_guarded_quantifier(closure: &ExprClosure, is_forall: bool) -> Result<Guar
         return Err(Error::new_spanned(closure, "only support single quantified variable"));
     }
 
-    let (quant_var, Some(quant_type)) = get_simple_pat(&closure.inputs[0])? else {
+    let (quant_var, Some(quant_type)) = get_simple_pat(&closure.inputs[0].pat)? else {
         return Err(Error::new_spanned(closure, "only supports a typed variable as quantifier"));
     };
 
@@ -1481,7 +1481,7 @@ fn compile_rspec(items: Items, trace: bool) -> Result<TokenStream2, Error> {
     // For each function, generate an exec version
     for item_fn in ctx.fns.values() {
         let exec_fn = compile_spec_fn(&ctx, item_fn, trace)?;
-        output.push(quote! { #[verifier::loop_isolation(false)] #exec_fn });
+        output.push(quote! { #[verifier::loop_isolation(false)] #[verifier::exec_allows_no_decreases_clause] #exec_fn });
     }
 
     // println!("########################################");