rust_lean_playground/
lib.rs

1// From: https://github.com/AeneasVerif/aeneas/blob/3bf9aeecddb2600d788435bc83a6b84c6bdf054f/tests/src/tutorial/src/lib.rs#L186
2pub type Bignum = Vec<u32>;
3
4/// Add a bignum (`Vec<u32>`) in place, and return the carry.
5///
6/// We consider the bignum to be a little endian representation,
7/// i.e., the first element is the least significant.
8/// For adding we assume the bignums have the same length
9///
10/// ## Spec:
11///
12/// If we define:
13/// ```lean
14/// def toInt (l : List U32) : Int :=
15///  match l with
16///  | [] => 0
17///  | x :: l =>
18///    x + 2 ^ 32 * toInt l
19///```
20///
21/// Then the function satisfies:
22/// ```lean
23/// example (x : alloc.vec.Vec U32) (y : alloc.vec.Vec U32) (hLength : x.length = y.length) :
24///     ∃ x' c, add_with_carry x y = ok (c, x') ∧
25///     x'.length = x.length ∧
26///     c.val ≤ 1 ∧
27///     toInt x' + c.val * 2 ^ (32 * x'.length) = toInt x + toInt y :=
28///   add_with_carry_spec
29/// ```
30///
31/// I.e., if:
32/// - `x` has the same length as `y`
33///
34/// Then:
35/// - `add_with_carry x y` returns ok with result `c` and `x'`, updated value of `x`
36/// - `x'` has the same length as `x`
37/// - `c.val ≤ 1`
38/// - `toInt x' + c.val * 2 ^ (32 * x'.length) = toInt x + toInt y`.  
39///
40pub fn add_with_carry(x: &mut Bignum, y: &Bignum) -> u8 {
41    let mut c0 = 0u8;
42    let mut i = 0;
43    // Remark: we have (and need) the invariant that: c0 <= 1
44    while i < x.len() {
45        let (sum, c1) = x[i].overflowing_add(c0 as u32);
46        let (sum, c2) = sum.overflowing_add(y[i]);
47        // We have: c1 as u8 + c2 as u8 <= 1
48        c0 = c1 as u8 + c2 as u8;
49        x[i] = sum;
50        i += 1;
51    }
52    c0
53}
54
55// -----------------------------------------------------------------------//
56// Source:
57// [curve25519-dalek](https://docs.rs/curve25519-dalek/latest/src/curve25519_dalek/backend/serial/u64/field.rs.html#288)
58
59// pub const LOW_51_BIT_MASK: u64 = (1u64 << 51) - 1;
60pub const LOW_51_BIT_MASK: u64 = 2251799813685247u64; // 2^51  -1
61pub struct FieldElement51 {
62    pub limbs: [u64; 5],
63}
64
65// curve25519-dalek/src/backend/serial/u64/field.rs
66impl FieldElement51 {
67    /// Given 64-bit input limbs, reduce to enforce the bound 2^(51 + epsilon).
68    ///
69    /// ## Spec:
70    ///
71    /// If we define:
72    /// ```lean
73    /// def ArrayU645_to_Nat (limbs : Array U64 5#usize) : Nat :=
74    ///   ∑ i ∈ Finset.range 5, 2^(51 * i) * (limbs[i]!).val
75    ///
76    /// def p : Nat := 2^255 - 19
77    /// ```
78    ///
79    /// Then the function satisfies:
80    /// ```lean
81    /// example (limbs : Array U64 5#usize) :
82    ///     ∃ r, FieldElement51.reduce limbs = ok (r) ∧
83    ///     (∀ i, i < 5 → (r.limbs[i]!).val ≤ 2^51 + (2^13 - 1) * 19) ∧
84    ///     ArrayU645_to_Nat limbs ≡ ArrayU645_to_Nat r.limbs [MOD p] :=
85    ///   FieldElement51.reduce_spec limbs
86    /// ```
87    ///
88    /// I.e.,
89    /// - The function does not overflow and hence returns a result
90    /// - All the limbs of the result are small, ≤ 2^(51 + ε)
91    /// - The result is equal to the input mod p.
92    ///
93    #[inline(always)]
94    pub fn reduce(mut limbs: [u64; 5]) -> FieldElement51 {
95        // Since the input limbs are bounded by 2^64, the biggest
96        // carry-out is bounded by 2^13.
97        //
98        // The biggest carry-in is c4 * 19, resulting in
99        //
100        // 2^51 + 19*2^13 < 2^51.0000000001
101        //
102        // Because we don't need to canonicalize, only to reduce the
103        // limb sizes, it's OK to do a "weak reduction", where we
104        // compute the carry-outs in parallel.
105
106        let c0 = limbs[0] >> 51;
107        let c1 = limbs[1] >> 51;
108        let c2 = limbs[2] >> 51;
109        let c3 = limbs[3] >> 51;
110        let c4 = limbs[4] >> 51;
111
112        limbs[0] &= LOW_51_BIT_MASK;
113        limbs[1] &= LOW_51_BIT_MASK;
114        limbs[2] &= LOW_51_BIT_MASK;
115        limbs[3] &= LOW_51_BIT_MASK;
116        limbs[4] &= LOW_51_BIT_MASK;
117
118        limbs[0] += c4 * 19;
119        limbs[1] += c0;
120        limbs[2] += c1;
121        limbs[3] += c2;
122        limbs[4] += c3;
123
124        FieldElement51 { limbs }
125    }
126}
rust_lean_playground/lib.rs

rust_lean_playground/
lib.rs
