Struct FieldElement51

pub struct FieldElement51 {
    pub limbs: [u64; 5],
}

Fields

limbs: [u64; 5]

Implementations

impl FieldElement51

pub fn reduce(limbs: [u64; 5]) -> FieldElement51

Given 64-bit input limbs, reduce to enforce the bound 2^(51 + epsilon).

Spec:

If we define:

def ArrayU645_to_Nat (limbs : Array U64 5#usize) : Nat :=
  ∑ i ∈ Finset.range 5, 2^(51 * i) * (limbs[i]!).val

def p : Nat := 2^255 - 19

Then the function satisfies:

example (limbs : Array U64 5#usize) :
    ∃ r, FieldElement51.reduce limbs = ok (r) ∧
    (∀ i, i < 5 → (r.limbs[i]!).val ≤ 2^51 + (2^13 - 1) * 19) ∧
    ArrayU645_to_Nat limbs ≡ ArrayU645_to_Nat r.limbs [MOD p] :=
  FieldElement51.reduce_spec limbs

I.e.,

• The function does not overflow and hence returns a result
• All the limbs of the result are small, ≤ 2^(51 + ε)
• The result is equal to the input mod p.