proofs/crypto/curve25519/cong.bend checks

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

6 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ../../math/natural/modpow.bend as MP

Definitions

def ceq source · line 10 · raw

@+pp:Nat -> @+a:Nat -> @+b:Nat -> Data

def c_refl source · line 13 · raw

@+pp:Nat -> @+a:Nat -> ceq(pp, a, a)

def c_sym source · line 16 · raw

@+pp:Nat -> @+a:Nat -> @+b:Nat -> @+h:ceq(pp, a, b) -> ceq(pp, b, a)

def c_trans source · line 19 · raw

@+pp:Nat -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+h1:ceq(pp, a, b) -> @+h2:ceq(pp, b, c) -> ceq(pp, a, c)

def c_eq source · line 22 · raw

@+pp:Nat -> @+a:Nat -> @+b:Nat -> @+e:{a == b : Nat} -> ceq(pp, a, b)

def c_mod source · line 26 · raw

@+pp:Nat -> @+a:Nat -> ceq(pp, Nat.mod(a, 1n+pp), a)

the reduced value is congruent to the value

def c_add source · line 29 · raw

@+pp:Nat -> @+a:Nat -> @+a2:Nat -> @+b:Nat -> @+b2:Nat -> @+ha:ceq(pp, a, a2) -> @+hb:ceq(pp, b, b2) -> ceq(pp, Nat.add(a, b), Nat.add(a2, b2))

def c_mul source · line 43 · raw

@+pp:Nat -> @+a:Nat -> @+a2:Nat -> @+b:Nat -> @+b2:Nat -> @+ha:ceq(pp, a, a2) -> @+hb:ceq(pp, b, b2) -> ceq(pp, Nat.mul(a, b), Nat.mul(a2, b2))

def c_pow source · line 57 · raw

@+pp:Nat -> @+a:Nat -> @+a2:Nat -> @+k:Nat -> @+ha:ceq(pp, a, a2) -> ceq(pp, Nat.pow(a, k), Nat.pow(a2, k))

def pow_one_base source · line 65 · raw

@+k:Nat -> {Nat.pow(1n, k) == 1n : Nat}

def pow_pow source · line 74 · raw

@+x:Nat -> @+a:Nat -> @+b:Nat -> {Nat.pow(Nat.pow(x, a), b) == Nat.pow(x, Nat.mul(a, b)) : Nat}

def cancel_r source · line 86 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e:{Nat.add(a, c) == Nat.add(b, c) : Nat} -> {a == b : Nat}

def shift3 source · line 90 · raw

@+z:Nat -> @+m:Nat -> @+t:Nat -> @+k:Nat -> @+e:{Nat.add(m, t) == k : Nat} -> {Nat.add(Nat.add(z, m), t) == Nat.add(k, z) : Nat}

(z + m) + t == k + z when m + t == k

def c_cancel source · line 94 · raw

@+pp:Nat -> @+X:Nat -> @+Y:Nat -> @+m:Nat -> @+h:ceq(pp, Nat.add(X, m), Nat.add(Y, m)) -> ceq(pp, X, Y)

X + m == Y + m (mod p) -> X == Y (mod p): add p - (m mod p) to both

def le_add_l source · line 108 · raw

@+a:Nat -> @+b:Nat -> {Nat.is_le(b, Nat.add(a, b)) == True{} : Bool}

def c_subm source · line 112 · raw

@+pp:Nat -> @+X:Nat -> @+Y:Nat -> @+m:Nat -> @+h:ceq(pp, X, Y) -> @+hm:{Nat.is_le(m, 1n+pp) == True{} : Bool} -> ceq(pp, Nat.sub(Nat.add(X, 1n+pp), m), Nat.sub(Nat.add(Y, 1n+pp), m))

(X + p) - m == (Y + p) - m (mod p) for X == Y (mod p) and m <= p