proofs/crypto/poly1305/poly.bend checks

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

7 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/poly1305.bend as R
import ../../lib/lemmas/proofs/nat_algebra.bend as NA
import ../../math/natural/arith.bend as NR
import ./modp.bend as MP
import ./mac.bend as M

Laws

law step_alg provedsource · line 26 · raw

@+r:Nat -> @+a:Nat -> @+n:Nat -> @+x:Nat -> @+p:Nat -> {Nat.add(Nat.mul(Nat.mul(r, Nat.add(a, n)), x), p) == Nat.add(Nat.mul(a, Nat.mul(r, x)), Nat.add(Nat.mul(n, Nat.mul(r, x)), p)) : Nat}

(r (a + n)) X == a (r X) + n (r X)

law horner_poly provedsource · line 45 · raw

@+bs:List<&2, List<&2, U32>> -> @+r:Nat -> @+a:Nat -> {horner(bs, r, a) == Nat.add(Nat.mul(a, Nat.pow(r, len(bs))), 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.poly(bs, r)) : Nat}

horner(bs, r, a) == a r^q + poly(bs, r)

law horner_mod provedsource · line 62 · raw

@+bp:Nat -> @+bs:List<&2, List<&2, U32>> -> @+r:Nat -> @+x:Nat -> {Nat.mod(horner(bs, r, Nat.mod(x, 1n+bp)), 1n+bp) == Nat.mod(horner(bs, r, x), 1n+bp) : Nat}

horner only depends on its start value mod n.

law absorb_horner provedsource · line 91 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, List<&2, U32>> -> @+r:Nat -> @+a:Nat -> @+ha:{Nat.is_lt(a, 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/mac.bpv(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.absorb(bs, r, a) == Nat.mod(horner(bs, r, a), 1n+0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/mac.bpv(one)) : Nat}

absorb(bs, r, a) == horner(bs, r, a) mod p, for a < p.

law absorb_poly provedsource · line 115 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bs:List<&2, List<&2, U32>> -> @+r:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.absorb(bs, r, 0n) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.poly(bs, r), Nat.sub(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one), 5n)) : Nat}

The accumulator is the polynomial at r, reduced mod 2^130 - 5.

Definitions

def horner source · line 17 · raw

@bs:List<&2, List<&2, U32>> -> @+r:Nat -> @a:Nat -> Nat

Horner's rule without reduction.

def len source · line 22 · raw

@+bs:List<&2, List<&2, U32>> -> Nat

def next_mod source · line 69 · raw

@+bp:Nat -> @+r:Nat -> @+x:Nat -> @+n:Nat -> {Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, 1n+bp), n)), 1n+bp) == Nat.mod(Nat.mul(r, Nat.add(x, n)), 1n+bp) : Nat}