Prove `sub` by TheodoreEhrenborg · Pull Request #44 · Beneficial-AI-Foundation/dalek-lite

TheodoreEhrenborg · 2025-08-11T10:24:34Z

No description provided.

TheodoreEhrenborg · 2025-08-11T10:36:04Z


 #[verifier::external_body]
-pub fn select(x: &u64, y: &u64, c: Choice) -> (res: u64)
-    ensures boolify(c) ==> res == x,


The version of this on main (which I wrote) is wrong 🤦‍♂️

I've flipped it to be correct. And I've changed the bool to be an enum with similar names to https://docs.rs/subtle/latest/subtle/trait.ConditionallySelectable.html#tymethod.conditional_select, so now it's easier to compare to that doc and see that it's the right way around

TheodoreEhrenborg · 2025-08-11T10:38:53Z

        // subtract l if the sum is >= l
        proof { lemma_l_value_properties(&constants::L, &sum); }
+        assert(to_nat(&sum.limbs) >= 0);
+        assume(to_nat(&sum.limbs) < 2 * group_order());


I've added this assume in add so it can call sub. I think this can be propagated back to become another precondition for add

assert(to_nat(&sum.limbs) >= 0);

Isn't this a tautology based on types? to_nat returns a nat, which is always >= 0

TheodoreEhrenborg · 2025-08-11T10:42:52Z


        // a - b
        let mut borrow: u64 = 0;
+        assert(seq_u64_to_nat(a.limbs@.subrange(0, 0 as int)) - seq_u64_to_nat(b.limbs@.subrange(0, 0 as int )) ==


I've moved most of the proof of sub into lemmas, but I've left in the invariants and a few asserts. I could probably squish a few more asserts into lemmas, although some of them are needed to get Verus to recognize that a lemma has the right preconditions

TheodoreEhrenborg · 2025-08-11T10:43:59Z

    seq_to_nat(limbs@.map(|i, x| x as nat))
 }

+pub open spec fn seq_u64_to_nat(limbs: Seq<u64>) -> nat


Just another wrapper around seq_to_nat

TheodoreEhrenborg · 2025-08-11T10:50:39Z

    assert(0x000d63c715bea69fu64 < (1u64 << 52)) by (bit_vector);
 }
+
+pub proof fn lemma_seq_u64_to_nat_subrange_extend(seq: Seq<u64>, i: int)


I asked Claude to do this and fed it a very similar proof from https://github.com/Beneficial-AI-Foundation/dafny-bignums, but it couldn't---maybe it didn't realize how similar Dafny and Verus are? I did get it to do most of the base case though

TheodoreEhrenborg · 2025-08-11T10:51:44Z

+    assert(a as nat == (a >> 52) as nat * pow2(52) + (a & mask) as nat);
+}
+
+pub proof fn lemma_sub_loop1_invariant(difference: Scalar52, borrow: u64, i: usize, a: &Scalar52, b: &Scalar52, old_borrow: u64, mask: u64, difference_loop1_start: Scalar52)


I haven't put much effort into cutting unnecessary asserts from these lemmas

TheodoreEhrenborg · 2025-08-11T10:54:43Z

+        // Without the following condition, all we can prove is something like:
+        // to_nat(&a.limbs) >= to_nat(&b.limbs) ==> to_nat(&s.limbs) == to_nat(&a.limbs) - to_nat(&b.limbs),
+        // to_nat(&a.limbs) < to_nat(&b.limbs) ==> to_nat(&s.limbs) == (to_nat(&a.limbs) - to_nat(&b.limbs) + pow2(260) + group_order()) % (pow2(260) as int),
+        // In the 2nd case, `sub` doesn't always do subtraction mod group_order


It took me several tries to get the spec right

Kukovec

LGMT, though I'm curious if Claude can comment its code if asked; some of the lemmas would be a bit tough to read through manually if uncommented.

Kukovec · 2025-08-11T10:56:26Z

        // subtract l if the sum is >= l
        proof { lemma_l_value_properties(&constants::L, &sum); }
+        assert(to_nat(&sum.limbs) >= 0);
+        assume(to_nat(&sum.limbs) < 2 * group_order());


assert(to_nat(&sum.limbs) >= 0);

Isn't this a tautology based on types? to_nat returns a nat, which is always >= 0

Kukovec · 2025-08-11T10:59:42Z

+        // to_nat(&a.limbs) >= to_nat(&b.limbs) ==> to_nat(&s.limbs) == to_nat(&a.limbs) - to_nat(&b.limbs),
+        // to_nat(&a.limbs) < to_nat(&b.limbs) ==> to_nat(&s.limbs) == (to_nat(&a.limbs) - to_nat(&b.limbs) + pow2(260) + group_order()) % (pow2(260) as int),
+        // In the 2nd case, `sub` doesn't always do subtraction mod group_order
+        -group_order() <= to_nat(&a.limbs) - to_nat(&b.limbs) < group_order(),


How come this is necessary though?
If a and b are bounded, then to_nat(a) < order and a - b <= a, similar for b and -order.

limbs_bounded(a) guarantees that to_nat(a) < 2^260, but group_order ~ 2^252. So I tried requiring 0 <= a < group_order && 0 <= b < group_order, but add passes in values sometimes larger than group_order. I think add's call to sub satisfies 0 <= a < 2 * group_order && 0 <= b < 2 * group_order, which is simpler than the precondition I went with, but that precondition is too loose for sub to always be correct

Also montgomery_reduce calls sub, and I don't yet understand it well enough to know if it satisfies sub's preconditions.

In that case, I'd consider relaxing this requirement, but changing ensures to

to_nat(&s.limbs) % (group_order() as int) == (to_nat(&a.limbs) - to_nat(&b.limbs)) % (group_order() as int),

result limbs are bounded, but may represent a value greater than the order, in which case you have to take mod p on the left too.

The weird thing about sub is that

to_nat(&s.limbs) % (group_order() as int) == (to_nat(&a.limbs) - to_nat(&b.limbs)) % (group_order() as int),

isn't always true. If to_nat(&a.limbs) < to_nat(&b.limbs), we get

to_nat(&s.limbs) == (to_nat(&a.limbs) - to_nat(&b.limbs) + pow2(260) + group_order()) % (pow2(260) as int),

And then if to_nat(&a.limbs) - to_nat(&b.limbs) < -group_order, this simplifies to

to_nat(&s.limbs) == to_nat(&a.limbs) - to_nat(&b.limbs) + pow2(260) + group_order(),

And mod group_order, we get

s % group_order == (a - b + pow(260)) % group order != (a - b) % group order

Here's a test demonstrating this: https://github.com/Beneficial-AI-Foundation/curve25519-dalek/tree/sub_test

Kukovec · 2025-08-11T11:07:28Z

Seems like there are a lot of spurious asserts, but if it's correct it's correct.

At some point I should run verus_cleaner.py, but that script takes a while and doesn't catch everything

TheodoreEhrenborg · 2025-08-11T12:05:13Z

some of the lemmas would be a bit tough to read through manually if uncommented

That's my fault; I've added some comments

TheodoreEhrenborg commented Aug 11, 2025

View reviewed changes

TheodoreEhrenborg marked this pull request as ready for review August 11, 2025 10:55

TheodoreEhrenborg requested a review from a team August 11, 2025 10:55

Kukovec approved these changes Aug 11, 2025

View reviewed changes

TheodoreEhrenborg added 19 commits August 11, 2025 13:30

Add to the spec

fe7a70c

Make some asserts with correct syntax

7f2eac5

Remove unneeded code

ede60fb

Put in invariant and prove it's initially true

d75c942

Claude adds helpful lemma

d9bf793

Remove comments

cea8650

Claude adds a calc statement

1292443

Fix syntax

226f417

Put in a bunch of assumes

824c76c

Add asserts after the loop

9dccb0e

Some work on 2nd loop

731d328

Claude updates subtle_assumes.rs

0d057e9

Change variable names

a409fc5

IMPORTANT: Fix assumption that was wrong on main

e61cdd3

Hence fix up scalar.rs

734329e

Continue pushing easy case of loop 2

ffe9fac

Continue easy part of loop 2

589c87d

Clean a bit

e0fe40f

Prove 2nd loop in easy case is a no-op

c203a81

TheodoreEhrenborg added 27 commits August 11, 2025 13:30

More preconditions

22890c0

Lemma now verifies

e52fd05

Remove some asserts

4b006bd

Combine if statements

7ab61f7

Combine if statements, again

49446f6

Move loop 2 proof into lemma

9cb6018

Fix syntax errors

28f303e

Add postconditions to lemma

241738c

Add preconditions to lemma

552989a

More preconditions

bcc015a

Down to 5 errors

fc7e60b

Tell the lemma what addend is

401ec4c

Get lemma to verify

4379c7b

Format

b834c05

Remove unneeded assert

3e2c80c

More small tweaks

fd4eec6

Remove unused imports

07f1765

Remove unused parameter

0ef0f3d

Remove unused import

b687b10

Rename variable

25bc694

Reduce diff

c3f8fbd

Fix my typo

fff73f2

Add link to subtle docs

8d7e9e2

Clarify comment

435f0fd

Delete unneeded assert

856e203

Add comments

0ed1f5e

Small typo

55d56c8

TheodoreEhrenborg force-pushed the prove_sub branch from 30a2274 to 55d56c8 Compare August 11, 2025 12:30

TheodoreEhrenborg merged commit bc45994 into main Aug 11, 2025
41 checks passed

TheodoreEhrenborg deleted the prove_sub branch August 11, 2025 12:33

Conversation

TheodoreEhrenborg commented Aug 11, 2025

Uh oh!

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

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!

Kukovec left a comment

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!

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

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!

TheodoreEhrenborg commented Aug 11, 2025

Uh oh!

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

TheodoreEhrenborg Aug 11, 2025 •

edited

Loading

TheodoreEhrenborg Aug 11, 2025 •

edited

Loading