Example verus proofs #813

TheodoreEhrenborg · 2025-09-01T16:37:24Z

Thanks for the call with BAIF @rozbb. I'm informally reaching out to ask some questions and show you what Verus looks like when applied to your codebase.

Questions

Our current understanding is you don't want any Verus code merged into curve-dalek (i.e. you'd reject this PR), since there wouldn't be a proof engineer to maintain is. Is this correct?
We were considering maintaining a mirror repo which had a duplicate of your code and also contained the verus proofs, and then comparing to your official copy with https://crates.io/crates/cargo-expand to make sure we were in sync. (Verus annotations disappear when macros are expanded.) If we went down that route, we'd make some minor PRs to refactor the code into something Verus supports.

How much refactoring would you tolerate?

e.g. verus currently doesn't support tuple structs, so you'll notice that causes a lot of changes. My opinion is that removing tuple structs from curve-dalek is too much of a change, and we should just kindly ask the Verus team to add support for them. But for more minor changes, I might lean towards just making a PR to here

If we could find a proof engineer willing to maintain the Verus proofs for curve-dalek, would you be open to merging Verus code into curve-dalek? We can't commit to anything yet.

Summary of changes

I don't intend to merge this PR because we're still working inside the u64 folder.
In particular, my coworker Jure has done a lot of work with field.rs, which I haven't included in this branch.

This branch has 8 proved functions

m
add
sub
mul_internal
square_internal
montgomery_mul
montgomery_square
from_montgomery

add and sub are the most complicated functions and have the most complicated proofs.

I haven't rebased on upstream's main. This branch is based on c3f91f7 from July. I checked and there's a small conflict caused by a function getting pulled out. Easy to fix, I just haven't bothered

Happy to answer any questions

Plus a few other improvements that I've noted below Tentative style guide: - Any proof block over one line gets folded into a lemma - Multiline invariants don't get folded into a lemma (unsure about this), but the `invariant` keyword goes on a separate line to allow verus_cleaner to check the first invariant

Claude made most of the changes (I just fixed CI and deleted some comments). I gave Claude some hints---in particular: - Tightening the specs to completely determine the result - Claude trusted the already existing bytes_to_nat_rec, but I thought it was maybe wrong and told Claude to look at the exponent My prompts were: ``` 1. Read u64/scalar.rs and scalar_specs.rs. Add ensures/requires for all fns in scalar.rs that are missing them. Use assume(false) to prove 2. /model [using opus] 3. Keep going 4. Does it verify with assume false? 5. Can you mark all your specs with "// Not human-approved yet" after every spec line you added 6. OK, look again at from_bytes_wide. I'm pretty sure you can make a spec that says exactly what the output result should be. 7. Hmm, I'm actually not sure if bytes_to_nat_rec is using the correct exponent 8. Also tighten the specs for as_montogomery and from_montogomery 9. Make a spec fn that says forall|i: int| 0 <= i < 5 ==> result.limbs[i] < (1u64 << 52), and then refactor to shorten specs ``` I've attached the full conversation [2025-08-01-read-u64scalarrs-and-scalarspecsrs-add-ensure.txt](https://github.com/user-attachments/files/21547411/2025-08-01-read-u64scalarrs-and-scalarspecsrs-add-ensure.txt)

TheodoreEhrenborg · 2025-09-01T16:39:22Z

.github/workflows/curve25519-dalek.yml

          RUSTFLAGS: '--cfg curve25519_dalek_backend="fiat"'
        run: cargo test --target ${{ matrix.target }}

-  # Default no_std test only tests using serial across all crates


Almost all of the CI still works. The no_std tests annoyingly don't. I haven't looked into this deeply yet---I hope it's something trivial

See Beneficial-AI-Foundation#59 for an example of the CI passing

TheodoreEhrenborg · 2025-09-01T16:39:38Z

.github/workflows/curve25519-dalek.yml

+        ln -s verus-x86-linux/cargo-verus
+    - name: Run test
+      run: | 
+        cargo-verus verify -- --smt-option smt.random_seed=0


Checking the proofs in CI

TheodoreEhrenborg · 2025-09-01T16:40:43Z

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

There are no proofs in the u32 folder. But we had to change the types for compatibility because we got rid of tuple structs in the u64 folder

TheodoreEhrenborg · 2025-09-01T16:41:15Z

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

-        s[29] =  (self.0[8] >>  0)                      as u8;
-        s[30] =  (self.0[8] >>  8)                      as u8;
-        s[31] =  (self.0[8] >> 16)                      as u8;
+        s[ 0] =  (self.limbs[0] >>  0)                      as u8;


More changes caused by Verus's lack of support for tuple structs

TheodoreEhrenborg · 2025-09-01T16:43:34Z

curve25519-dalek/src/backend/serial/u64/scalar_lemmas.rs

This is where the bulk of the proofs is. All of this is non-executable verus code. When macros are expanded, it shrinks down to

pub mod scalar_lemmas { #[allow(unused_imports)] use super::constants; #[allow(unused_imports)] use super::scalar::Scalar52; #[allow(unused_imports)] use super::scalar_specs::*; #[allow(unused_imports)] use vstd::arithmetic::div_mod::*; #[allow(unused_imports)] use vstd::arithmetic::mul::*; #[allow(unused_imports)] use vstd::arithmetic::power2::*; #[allow(unused_imports)] use vstd::bits::*; #[allow(unused_imports)] use vstd::calc; use vstd::prelude::*; }

TheodoreEhrenborg · 2025-09-01T16:44:14Z

curve25519-dalek/src/backend/serial/u64/scalar_specs.rs

+use vstd::prelude::*;
+
+verus! {
+pub open spec fn seq_to_nat(limbs: Seq<nat>) -> nat


Conversion function from limbs to a natural number

TheodoreEhrenborg · 2025-09-01T16:45:30Z

curve25519-dalek/src/backend/serial/u64/subtle_assumes.rs

@@ -0,0 +1,34 @@
+//! Tell Verus what Choice does


subtle doesn't have verus annotations, so instead we tell verus here what subtle does. Hence we wrap u64::conditional_select in an annotated function select

TheodoreEhrenborg · 2025-09-01T16:46:10Z

curve25519-dalek/src/lib.rs

-    missing_docs,
-    rust_2018_idioms,
-    unused_lifetimes,
-    unused_qualifications


Took this warning out for convenience, can likely put it back with only a little hassle

TheodoreEhrenborg · 2025-09-01T16:48:39Z

curve25519-dalek/src/backend/serial/u64/scalar.rs

+        assert(seq_u64_to_nat(a.limbs@.subrange(0, 5 as int)) + seq_u64_to_nat(b.limbs@.subrange(0, 5 as int)) ==
+               seq_u64_to_nat(sum.limbs@.subrange(0, 5 as int)) + (carry >> 52) * pow2((52 * (5) as nat)));
+
+        proof {lemma_add_sum_simplify(a, b, &sum, carry);}


A bunch of the proof has been refactored into lemmas like these, but you'll notice that add has gotten longer due to all the non-executable proof lines. Probably a few more could get refactored into lemmas, but not all of them

TheodoreEhrenborg · 2025-09-01T16:49:43Z

curve25519-dalek/src/backend/serial/u64/scalar.rs

    #[inline(always)]
-    #[rustfmt::skip] // keep alignment of return calculations
-    fn square_internal(a: &Scalar52) -> [u128; 9] {
-        let aa = [


Verus didn't like the aa shorthand. 🤷‍♂️ Hence the alterations

TheodoreEhrenborg · 2025-09-01T16:49:59Z

curve25519-dalek/src/backend/serial/u64/scalar.rs

+        limbs_bounded(&result),
+    {

-        #[inline(always)]


Verus didn't like inline functions

TheodoreEhrenborg · 2025-09-01T16:50:25Z

curve25519-dalek/src/backend/serial/u64/scalar.rs

    /// Compute `a * b` (mod l)
    #[inline(never)]
-    pub fn mul(a: &Scalar52, b: &Scalar52) -> Scalar52 {
+    #[verifier::external_body] // TODO Verify this function


external_body means that verus ignores this function

rozbb · 2025-09-06T03:09:37Z

Thank you so much for this! I might take a little bit to go thru it, but this is super exciting.

Stating an initial opinion: I'm happy to merge code changes (minor ones preferably), but it might be annoying to keep proof-related annotations in our code. I still want everything to be real Rust and parse in any contributor's IDE without modification. Would it be possible to keep all Verus-related stuff in a separate folder entirely? I'm not sure how strict the layout is.

TheodoreEhrenborg · 2025-09-12T12:32:21Z

(Sorry for the delay in responding; BAIF has entered crunch time for another project)

parse in any contributor's IDE without modification

This somewhat works, since rust-analyzer expands the verus macro and can't see the verus annotations. I'm not a VSCode user, but I just installed it and the rust-analyzer extension. Rust-analyzer seems to highlight the types correctly if you hover over a variable:

It's not perfect:

inlay type hints don't display inside the verus macro
if you use rust-analyzer to rename a variable, it only renames the variable in the Rust code, not in the annotations. So that would break a proof. (Although the bigger problem is that the proof of any function will likely break at least a little bit if the function itself changes. So ideally we could find a function that is guaranteed not to change for a while, which might not be a possible thing to guarantee)

Would it be possible to keep all Verus-related stuff in a separate folder entirely?

In Verus, the proof annotations (the ensures/requires in the signature) have to appear on the executable function, and usually there have to be a few calls to lemmas too. There are other proof approaches (e.g. https://github.com/cryspen/hax) where you first run an extraction tool to translate the Rust code to Lean/F*/etc, and then you write a proof in Lean, all without modifying the original Rust code (unless there's a feature that isn't supported, e.g. tuple structs for Verus above). Hax also doesn't solve the problem of proofs breaking when the function changes. I hope that BAIF can find a way to teach an LLM to be a good enough proof engineer to repair proofs (easier than writing proofs from scratch), but no promises yet

TheodoreEhrenborg and others added 30 commits July 31, 2025 16:44

Remove unneeded invariants

cf5bfed

Clean the lemmas Claude added

42237f8

Remove line

b3fa526

Insert spaces

576220e

Format

efe8de9

Reduce diff

22d6728

Fix cargo check

b1115fe

Fix warning

5ef1adb

Fix fiat backend

1eeca24

Format

119c118

2 tiny changes

2d69fd2

Claude adds specs

17596df

Claude notes which specs are AI-generated

d71b687

Update pin to fix CI

2e1f58c

Attempt to fix CI

4dc0aa9

Ask Claude to make spec more precise

3d96095

Probably fix this spec

efcddb3

Approve this spec

41b079f

I'm suspicious of this bit

589f4e8

The spec for helper functions depends on the proof

8efe767

Claude tightens the specs

f728bc5

Claude refactors

fa70874

Approve these specs

aab1cfb

Fix CI ahead of time

da914d9

Need to fix CI anyway

7752f1f

Claude does some proofs

e69a4f7

Claude moves proofs into lemmas

e9bbcd6

Claude proves square, but leaves in assumes

874fe9f

TheodoreEhrenborg and others added 15 commits August 11, 2025 13:30

Add comments

0ed1f5e

Small typo

55d56c8

Prove sub (#44)

bc45994

Restore scalar.rs and scalar_lemmas.rs from main

8ab4e79

Uncomment some code and remove import

a81e537

rm -r scripts/

538f7ed

Remove more files

506bf24

Remove field files but keep 2 lemmas

f5c1d42

Remove assumes

34e387f

Bring back tests

6080805

Remove comment

ccd3690

Remove unused specs

253fcfd

Get cargo fmt working

484d4b6

Remove unused proof

8d473e5

Format

cfd0e38

TheodoreEhrenborg commented Sep 1, 2025

View reviewed changes

kayabaNerve mentioned this pull request Sep 5, 2025

Fields with lazy reduction RustCrypto/traits#1997

Open

Uh oh!

Example verus proofs #813

Are you sure you want to change the base?

Example verus proofs #813

Uh oh!

Conversation

TheodoreEhrenborg commented Sep 1, 2025 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Questions

Summary of changes

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

rozbb commented Sep 6, 2025

Uh oh!

TheodoreEhrenborg commented Sep 12, 2025

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

4 participants

TheodoreEhrenborg commented Sep 1, 2025 •

edited

Loading