~/bend-docscommunity

proofs/crypto/poly1305/modp.bend checks

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

13 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/poly1305.bend as R
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as AR
import ../../lib/u32alg.bend as UA
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
import ../../math/natural/arith.bend as NR
import ./arith.bend as A

Laws

law bigp provedsource · line 19 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, x) == Nat.add(Nat.mul(x, 1n+bp), Nat.mul(x, 5n)) : Nat}

law fold_eq provedsource · line 34 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+x:Nat -> {x == Nat.add(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(130n, x), 1n+bp), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.fold(x)) : Nat}

x == hi p + fold(x)

law fold_mod provedsource · line 50 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+x:Nat -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.fold(x), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}

law folds_mod provedsource · line 65 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+n:Nat -> @+x:Nat -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.folds(n, x), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}

law folds_fit provedsource · line 101 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+n:Nat -> @+x:Nat -> @+h:{Nat.is_lt(x, Nat.add(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one))) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(130n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.folds(n, x)) == True{} : Bool}

law canon_mod provedsource · line 161 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+y:Nat -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(130n, y) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.canon(y) == Nat.mod(y, 1n+bp) : Nat}

law modp_mod provedsource · line 176 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+x:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.modp(x) == Nat.mod(x, 1n+bp) : Nat}

modp(x) is x mod p, for every x

Definitions

def fold_lt_c source · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+k:Nat -> @+x:Nat -> @+h:{Nat.is_lt(x, Nat.add(1n+k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one))) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.high(130n, x), 0n) == c : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.fold(x), Nat.add(k, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one))) == True{} : Bool}

a fold on x < k + 1 + 2^130 gives a value below k + 2^130

def canon_c source · line 117 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+y:Nat -> @+hy:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(130n, y) == True{} : Bool} -> @+b:Bool -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(130n, Nat.add(y, 5n)) == b : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.pick(b, y, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(130n, Nat.add(y, 5n))) == Nat.mod(y, 1n+bp) : Nat}

y < 2^130: canon(y) == y mod p