proofs/crypto/curve25519/eqf.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as Eqf

12 imports

import Base
import ../../../spec/crypto/curve25519/field.bend as FS
import ../../../src/crypto/curve25519/field.bend as F
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ./limbs.bend as LM
import ./fieldops.bend as FO
import ./canon.bend as CN
import ./cong.bend as G

Definitions

def pw source · line 18 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> Nat

def w_eq source · line 21 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+hB:{Nat.is_lt(B, 1n+pp) == True{} : Bool} -> {Nat.add(pw(pp, A, B), B) == Nat.add(A, 1n+pp) : Nat}

def w_zero source · line 26 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+hB:{Nat.is_lt(B, 1n+pp) == True{} : Bool} -> @+e:{A == B : Nat} -> {Nat.mod(pw(pp, A, B), 1n+pp) == 0n : Nat}

def q_one source · line 35 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+q:Nat -> @+hA:{Nat.is_lt(A, 1n+pp) == True{} : Bool} -> @+hB:{Nat.is_lt(B, 1n+pp) == True{} : Bool} -> @+hw:{Nat.add(Nat.mul(q, 1n+pp), B) == Nat.add(A, 1n+pp) : Nat} -> {A == B : Nat}

w mod p == 0 gives A == B: the quotient q has w == q p, and q is 1

def w_ne source · line 54 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+hA:{Nat.is_lt(A, 1n+pp) == True{} : Bool} -> @+hB:{Nat.is_lt(B, 1n+pp) == True{} : Bool} -> @+h:{Nat.mod(pw(pp, A, B), 1n+pp) == 0n : Nat} -> {A == B : Nat}

def eq_false source · line 64 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+hA:{Nat.is_lt(A, 1n+pp) == True{} : Bool} -> @+hB:{Nat.is_lt(B, 1n+pp) == True{} : Bool} -> @+hb:{Nat.is_eq(A, B) == False{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == c : Bool} -> {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == Nat.is_eq(A, B) : Bool}

def eq_bool source · line 74 · raw

@+pp:Nat -> @+A:Nat -> @+B:Nat -> @+hA:{Nat.is_lt(A, 1n+pp) == True{} : Bool} -> @+hB:{Nat.is_lt(B, 1n+pp) == True{} : Bool} -> @+b:Bool -> @+hb:{Nat.is_eq(A, B) == b : Bool} -> {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == Nat.is_eq(A, B) : Bool}

def eq_val source · line 82 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+pp:Nat -> @+hP:{Nat.add(1n+pp, 19n) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(255n, one) : Nat} -> @+a:List<&2, U32> -> @+b:List<&2, U32> -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, a, 255n) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/curve25519/limbs.okb(32n, b, 255n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/curve25519/field.eq(a, b) == Nat.is_eq(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(a), 1n+pp), Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/curve25519/field.value(b), 1n+pp)) : Bool}