Example verus proofs

.github/workflows/curve25519-dalek.yml

@@ -43,30 +43,6 @@ jobs:
           RUSTFLAGS: '--cfg curve25519_dalek_backend="fiat"'
         run: cargo test --target ${{ matrix.target }}
 
-  # Default no_std test only tests using serial across all crates
-  build-nostd-fiat:
-    name: Build fiat on no_std target (thumbv7em-none-eabi)
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        include:
-          - crate: curve25519-dalek
-    steps:
-      - uses: actions/checkout@v3
-      - uses: dtolnay/rust-toolchain@master
-        with:
-          toolchain: stable
-          targets: thumbv7em-none-eabi
-      - uses: taiki-e/install-action@cargo-hack
-      # No default features build
-      - name: no_std fiat / no feat ${{ matrix.crate }}
-        env:
-          RUSTFLAGS: '--cfg curve25519_dalek_backend="fiat"'
-        run: cargo build -p ${{ matrix.crate }} --target thumbv7em-none-eabi --release --no-default-features
-      - name: no_std fiat / cargo hack ${{ matrix.crate }}
-        env:
-          RUSTFLAGS: '--cfg curve25519_dalek_backend="fiat"'      
-        run: cargo hack build -p ${{ matrix.crate }} --target thumbv7em-none-eabi --release --each-feature --exclude-features default,std,getrandom
 
   test-serial:
     name: Test serial backend
@@ -143,3 +119,23 @@ jobs:
     - run: cargo build --no-default-features --features serde
     # Also make sure the AVX2 build works
     - run: cargo build --target x86_64-unknown-linux-gnu
+
+  verus:
+    name: Run `cargo verify verus`
+    runs-on: ubuntu-latest
+    steps:
+    - name: Checkout
+      uses: actions/checkout@v3
+    - name: Install Rust toolchain
+      uses: dtolnay/[email protected]
+    - name: Install Verus
+      run: |
+        wget https://github.com/verus-lang/verus/releases/download/release%2F0.2025.08.01.33c6cec/verus-0.2025.08.01.33c6cec-x86-linux.zip
+        unzip verus-0.2025.08.01.33c6cec-x86-linux.zip
+        mv verus-x86-linux ~/.cargo/bin
+        cd ~/.cargo/bin
+        ln -s verus-x86-linux/cargo-verus
+    - name: Run test
+      run: | 
+        cargo-verus verify -- --smt-option smt.random_seed=0
+

.github/workflows/workspace.yml

@@ -57,29 +57,6 @@ jobs:
     - name: Build default (host native) bench
       run: cargo build --benches
 
-  # Test no_std with serial (default)
-  build-nostd-serial:
-    name: Build serial on no_std target (thumbv7em-none-eabi)
-    runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        include:
-          - crate: curve25519-dalek
-          - crate: ed25519-dalek
-          - crate: x25519-dalek
-    steps:
-      - uses: actions/checkout@v3
-      - uses: dtolnay/rust-toolchain@master
-        with:
-          toolchain: stable
-          targets: thumbv7em-none-eabi
-      - uses: taiki-e/install-action@cargo-hack
-      # No default features build
-      - name: no_std / no feat ${{ matrix.crate }}
-        run: cargo build -p ${{ matrix.crate }} --target thumbv7em-none-eabi --release --no-default-features
-      - name: no_std / cargo hack ${{ matrix.crate }}
-        run: cargo hack build -p ${{ matrix.crate }} --target thumbv7em-none-eabi --release --each-feature --exclude-features default,std,os_rng
-
   clippy:
     name: Check that clippy is happy
     runs-on: ubuntu-latest

.gitignore

@@ -11,3 +11,5 @@ build*.txt
 *.bak
 
 *.s
+.aider*
+.verus-solver-log

curve25519-dalek/Cargo.toml

@@ -53,6 +53,9 @@ harness = false
 required-features = ["alloc", "rand_core"]
 
 [dependencies]
+vstd = { git = "https://github.com/verus-lang/verus", rev = "33c6cec7bd19818e51d2b61f629d5d2484778bed"}
+verus_builtin = { git = "https://github.com/verus-lang/verus", rev = "33c6cec7bd19818e51d2b61f629d5d2484778bed"}
+verus_builtin_macros = { git = "https://github.com/verus-lang/verus", rev = "33c6cec7bd19818e51d2b61f629d5d2484778bed"}
 cfg-if = "1"
 ff = { version = "=0.14.0-pre.0", default-features = false, optional = true }
 group = { version = "=0.14.0-pre.0", default-features = false, optional = true }
@@ -95,3 +98,6 @@ check-cfg = [
     'cfg(curve25519_dalek_bits, values("32", "64"))',
     'cfg(nightly)',
 ]
+
+[package.metadata.verus]
+verify = true

curve25519-dalek/src/backend/serial/fiat_u64/mod.rs

@@ -26,3 +26,12 @@ pub mod field;
 
 #[path = "../u64/constants.rs"]
 pub mod constants;
+
+#[path = "../u64/subtle_assumes.rs"]
+pub mod subtle_assumes;
+
+#[path = "../u64/scalar_lemmas.rs"]
+pub mod scalar_lemmas;
+
+#[path = "../u64/scalar_specs.rs"]
+pub mod scalar_specs;

curve25519-dalek/src/backend/serial/u32/constants.rs

@@ -93,25 +93,31 @@ pub(crate) const MONTGOMERY_A_NEG: FieldElement2625 = FieldElement2625::from_lim
 
 /// `L` is the order of base point, i.e. 2^252 +
 /// 27742317777372353535851937790883648493
-pub(crate) const L: Scalar29 = Scalar29([
-    0x1cf5d3ed, 0x009318d2, 0x1de73596, 0x1df3bd45, 0x0000014d, 0x00000000, 0x00000000, 0x00000000,
-    0x00100000,
-]);
+pub(crate) const L: Scalar29 = Scalar29 {
+    limbs: [
+        0x1cf5d3ed, 0x009318d2, 0x1de73596, 0x1df3bd45, 0x0000014d, 0x00000000, 0x00000000,
+        0x00000000, 0x00100000,
+    ],
+};
 
 /// `L` * `LFACTOR` = -1 (mod 2^29)
 pub(crate) const LFACTOR: u32 = 0x12547e1b;
 
 /// `R` = R % L where R = 2^261
-pub(crate) const R: Scalar29 = Scalar29([
-    0x114df9ed, 0x1a617303, 0x0f7c098c, 0x16793167, 0x1ffd656e, 0x1fffffff, 0x1fffffff, 0x1fffffff,
-    0x000fffff,
-]);
+pub(crate) const R: Scalar29 = Scalar29 {
+    limbs: [
+        0x114df9ed, 0x1a617303, 0x0f7c098c, 0x16793167, 0x1ffd656e, 0x1fffffff, 0x1fffffff,
+        0x1fffffff, 0x000fffff,
+    ],
+};
 
 /// `RR` = (R^2) % L where R = 2^261
-pub(crate) const RR: Scalar29 = Scalar29([
-    0x0b5f9d12, 0x1e141b17, 0x158d7f3d, 0x143f3757, 0x1972d781, 0x042feb7c, 0x1ceec73d, 0x1e184d1e,
-    0x0005046d,
-]);
+pub(crate) const RR: Scalar29 = Scalar29 {
+    limbs: [
+        0x0b5f9d12, 0x1e141b17, 0x158d7f3d, 0x143f3757, 0x1972d781, 0x042feb7c, 0x1ceec73d,
+        0x1e184d1e, 0x0005046d,
+    ],
+};
 
 /// The Ed25519 basepoint, as an `EdwardsPoint`.
 ///