~/bend-docscommunity

proofs/crypto/poly1305/arith.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as Arith

9 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as AR
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/typed/width.bend as WW
import ../../math/typed/w64mul.bend as WM
import ../../math/typed/w64sh.bend as SH

Definitions

def tr source · line 15 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e1:{a == b : Nat} -> @+e2:{b == c : Nat} -> {a == c : Nat}

def sy source · line 18 · raw

@+a:Nat -> @+b:Nat -> @+e:{a == b : Nat} -> {b == a : Nat}

def cadd source · line 22 · raw

@+a:Nat -> @+a2:Nat -> @+b:Nat -> @+b2:Nat -> @+ea:{a == a2 : Nat} -> @+eb:{b == b2 : Nat} -> {Nat.add(a, b) == Nat.add(a2, b2) : Nat}

a + b == a' + b'

def cmul source · line 25 · raw

@+a:Nat -> @+a2:Nat -> @+b:Nat -> @+b2:Nat -> @+ea:{a == a2 : Nat} -> @+eb:{b == b2 : Nat} -> {Nat.mul(a, b) == Nat.mul(a2, b2) : Nat}

def csh source · line 28 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+e:{a == b : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, a) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, b) : Nat}

def btrue source · line 32 · raw

@+x:Bool -> @+y:Bool -> @+e:{x == y : Bool} -> @+h:{y == True{} : Bool} -> {x == True{} : Bool}

Bool rewriting of a proposition {x == True}

def le_subst source · line 35 · raw

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

def le_substl source · line 38 · raw

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

def lt_subst source · line 41 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e:{b == c : Nat} -> @+h:{Nat.is_lt(a, b) == True{} : Bool} -> {Nat.is_lt(a, c) == True{} : Bool}

def lt_substl source · line 44 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+e:{a == b : Nat} -> @+h:{Nat.is_lt(a, c) == True{} : Bool} -> {Nat.is_lt(b, c) == True{} : Bool}

def fits_subst source · line 47 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+e:{a == b : Nat} -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, b) == True{} : Bool}

def le_add_l source · line 51 · raw

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

b <= a + b

def le_add2 source · line 55 · raw

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

a <= c, b <= d: a + b <= c + d

def le_mul2 source · line 59 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_le(a, c) == True{} : Bool} -> @+h2:{Nat.is_le(b, d) == True{} : Bool} -> {Nat.is_le(Nat.mul(a, b), Nat.mul(c, d)) == True{} : Bool}

a <= c, b <= d: a b <= c d

def fits_le source · line 63 · raw

@+k:Nat -> @+x:Nat -> @+y:Nat -> @+h:{Nat.is_le(x, y) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, x) == True{} : Bool}

x <= y and y fits k bits: x fits k bits

def fits_add_l source · line 67 · raw

@+k:Nat -> @+y:Nat -> @+z:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, Nat.add(y, z)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, y) == True{} : Bool}

x <= y + z and fits(k, y + z)

def fits_add_r source · line 70 · raw

@+k:Nat -> @+y:Nat -> @+z:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, Nat.add(y, z)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, z) == True{} : Bool}

def lt_add2 source · line 74 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_lt(a, c) == True{} : Bool} -> @+h2:{Nat.is_lt(b, d) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, b), Nat.add(c, d)) == True{} : Bool}

a < c, b < d: a + b < c + d

def lt_le_add source · line 78 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> @+h1:{Nat.is_lt(a, c) == True{} : Bool} -> @+h2:{Nat.is_le(b, d) == True{} : Bool} -> {Nat.is_lt(Nat.add(a, b), Nat.add(c, d)) == True{} : Bool}

a < c, b <= d: a + b < c + d

def fits_add source · line 82 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, a) == True{} : Bool} -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, b) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(1n+k, Nat.add(a, b)) == True{} : Bool}

a and b fit k bits: a + b fits k + 1 bits

def lt_mul source · line 88 · raw

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

x < A, y < B: x y < A B

def pow2_add source · line 99 · raw

@+a:Nat -> @+b:Nat -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(b)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(Nat.add(a, b)) : Nat}

def fits_mul source · line 107 · raw

@+a:Nat -> @+b:Nat -> @+x:Nat -> @+y:Nat -> @+hx:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(a, x) == True{} : Bool} -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(b, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(a, b), Nat.mul(x, y)) == True{} : Bool}

x fits a bits, y fits b bits: x y fits a + b bits

def le_one source · line 111 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, x) == True{} : Bool} -> {Nat.is_le(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool}

x fits k bits: x <= 2^k (with 2^k written C.shift(k, one), one = 1)

def one_le_shift source · line 115 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(1n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool}

1 <= 2^k

def fits_le_one source · line 119 · raw

@+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+x:Nat -> @+h:{Nat.is_le(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(1n+k, x) == True{} : Bool}

x <= 2^k: x fits k + 1 bits

def shmul source · line 125 · raw

@+a:Nat -> @+b:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(a, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(b, one)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(Nat.add(a, b), one) : Nat}

2^a 2^b = 2^(a+b)

def mul_pow source · line 133 · raw

@+k:Nat -> @+x:Nat -> {Nat.mul(x, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.pow2(k)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, x) : Nat}

x * 2^k = shift(k, x)

def lt_mul_l source · line 137 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+ha:{Nat.is_le(1n, a) == True{} : Bool} -> @+h:{Nat.is_lt(b, c) == True{} : Bool} -> {Nat.is_lt(Nat.mul(a, b), Nat.mul(a, c)) == True{} : Bool}

a >= 1, b < c: a b < a c

def cancel_c source · line 143 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, b)) == True{} : Bool} -> @o:Or({Nat.is_lt(a, b) == True{} : Bool}, {Nat.is_lt(a, b) == False{} : Bool}) -> {Nat.is_lt(a, b) == True{} : Bool}

def shift_cancel source · line 151 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+h:{Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, a), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, b)) == True{} : Bool} -> {Nat.is_lt(a, b) == True{} : Bool}

shift(k, a) < shift(k, b): a < b

def fits_5q source · line 155 · raw

@+k:Nat -> @+q:Nat -> @+a:Nat -> @+hq:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, q) == True{} : Bool} -> @+ha:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, a) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(3n+k, Nat.add(Nat.mul(q, 5n), a)) == True{} : Bool}

q and a fit k bits: 5 q + a fits k + 3 bits