proofs/crypto/curve25519/num.bend checks

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

6 imports

import Base
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/word.bend as WD
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA

Definitions

def cong_l source · line 13 · raw

@+x:Nat -> @+y:Nat -> @+z:Nat -> @+e:{x == y : Nat} -> {Nat.add(x, z) == Nat.add(y, z) : Nat}

def cong_r source · line 16 · raw

@+z:Nat -> @+x:Nat -> @+y:Nat -> @+e:{x == y : Nat} -> {Nat.add(z, x) == Nat.add(z, y) : Nat}

def cong_add source · line 19 · raw

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

def cong_mul source · line 22 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+e1:{a == b : Nat} -> @+e2:{c == d : Nat} -> {Nat.mul(a, c) == Nat.mul(b, d) : Nat}

def cong_sc source · line 25 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+e:{x == y : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, y) : Nat}

def cong_mod source · line 28 · raw

@+m:Nat -> @+x:Nat -> @+y:Nat -> @+e:{x == y : Nat} -> {Nat.mod(x, m) == Nat.mod(y, m) : Nat}

def add4 source · line 32 · raw

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

(a + b) + (c + d) == (a + c) + (b + d)

def sc_add source · line 38 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, y)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, Nat.add(x, y)) : Nat}

2^k x + 2^k y == 2^k (x + y)

def sc_dbl source · line 48 · raw

@+k:Nat -> @+x:Nat -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(1n+k, x) : Nat}

2^k x + 2^k x == 2^(k+1) x

def sc_sc source · line 52 · raw

@+j:Nat -> @+k:Nat -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(Nat.add(j, k), x) : Nat}

2^j (2^k x) == 2^(j+k) x

def mul_sc_r source · line 56 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> {Nat.mul(x, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, one)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x) : Nat}

x 2^k == 2^k x

def mul_sc2 source · line 60 · raw

@+j:Nat -> @+k:Nat -> @+x:Nat -> @+y:Nat -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(j, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, y)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(Nat.add(j, k), Nat.mul(x, y)) : Nat}

(2^j x)(2^k y) == 2^(j+k) (x y)

def le_refl source · line 69 · raw

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

def le_add_r source · line 73 · raw

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

x <= a -> x + y <= a + y

def le_add2 source · line 79 · raw

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

def le_mul2 source · line 83 · raw

@+x:Nat -> @+y:Nat -> @+a:Nat -> @+b:Nat -> @+hx:{Nat.is_le(x, a) == True{} : Bool} -> @+hy:{Nat.is_le(y, b) == True{} : Bool} -> {Nat.is_le(Nat.mul(x, y), Nat.mul(a, b)) == True{} : Bool}

x <= a, y <= b -> x y <= a b

def le_sc source · line 90 · raw

@+k:Nat -> @+x:Nat -> @+a:Nat -> @+h:{Nat.is_le(x, a) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(k, a)) == True{} : Bool}

def sc_mono source · line 94 · raw

@+d:Nat -> @+a:Nat -> @+x:Nat -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(a, x), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/lib/word.sc(Nat.add(d, a), x)) == True{} : Bool}

2^a <= 2^b for a <= b, with b = d + a