~/bend-docscommunity

proofs/crypto/poly1305/step.bend checks

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

14 imports
import Base
import ../../../spec/lib/common.bend as C
import ../../../src/crypto/poly1305/limbs.bend as Li
import ../../lib/nat.bend as N
import ../../lib/logic.bend as L
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/w64add.bend as WA
import ../../math/typed/w64sh.bend as SH
import ../../math/typed/shrn.bend as SHN
import ../../math/typed/f64bits.bend as FB
import ./arith.bend as A
import ./value.bend as V

Laws

law p5 provedsource · line 25 · raw

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

law big130 provedsource · line 36 · raw

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

2^130 x = x p + 5 x

law dbound_lt provedsource · line 61 · raw

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

law dbound_fits provedsource · line 72 · raw

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

law fold_ev provedsource · line 80 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, U32> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.le_all(z, s21(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(z) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.fold(z)), Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(6n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(17n, z))), pm(one))) : Nat}

law fold_fit provedsource · line 108 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+z:List<&2, U32> -> @+hz:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.le_all(z, s21(one)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.fold(z), 30n) == True{} : Bool}

law fold_len provedsource · line 123 · raw

@+z:List<&2, U32> -> @+hl:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(z), 33n) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.fold(z)), 17n) == True{} : Bool}

law q29 provedsource · line 143 · raw

@+d:List<&2, U32> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(d, 30n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(29n, pv(d)) == True{} : Bool}

v(quot) fits 29 bits: the pass-1 top limb fits 31

law pass2_ev provedsource · line 156 · raw

@+d:List<&2, U32> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(d, 30n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.reduce(d)) == Nat.add(Nat.mul(pv(d), 5n), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.split(16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.carry(16n, d, 0)))) : Nat}

pass 2 on the split: its value is 5 q + the split

law reduce_ev provedsource · line 205 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, U32> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(d, 30n) == True{} : Bool} -> @+hl:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(d), 17n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(d) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.reduce(d)), Nat.mul(pv(d), pm(one))) : Nat}

law reduce_top provedsource · line 233 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, U32> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(d, 30n) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.reduce(d)))), 4n) == True{} : Bool}

the top limb after the reduction is at most 4 (its value is below 5 * 2^128)

law reduce_inv provedsource · line 274 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+d:List<&2, U32> -> @+hd:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(d, 30n) == True{} : Bool} -> {inv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.reduce(d)) == True{} : Bool}

law z_le provedsource · line 301 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(h, 8n) == True{} : Bool} -> @+hcf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(c, 8n) == True{} : Bool} -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> @+hrf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(r, 8n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.le_all(zz(r, h, c), s21(one)) == True{} : Bool}

the product's limbs are at most 2^21, its length at most 33

law z_ev provedsource · line 337 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(h, 8n) == True{} : Bool} -> @+hcf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(c, 8n) == True{} : Bool} -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> @+hrf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(r, 8n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(zz(r, h, c)) == Nat.mul(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(r)) : Nat}

law z_len provedsource · line 362 · raw

@+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> @+hhl:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(h), 17n) == True{} : Bool} -> @+hcl:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(c), 17n) == True{} : Bool} -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(zz(r, h, c)), 33n) == True{} : Bool}

law block_ev provedsource · line 376 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> @+hh:{inv(h) == True{} : Bool} -> @+hcl:{Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(c), 17n) == True{} : Bool} -> @+hcf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(c, 8n) == True{} : Bool} -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> @+hrf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(r, 8n) == True{} : Bool} -> {Nat.mul(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(c)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(r)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.block(r, h, c)), Nat.mul(bk(r, h, c), pm(one))) : Nat}

(h + c) r == block(r, h, c) + bk p

law block_inv provedsource · line 412 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> @+hh:{inv(h) == True{} : Bool} -> @+hcf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(c, 8n) == True{} : Bool} -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> @+hrf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(r, 8n) == True{} : Bool} -> {inv(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.block(r, h, c)) == True{} : Bool}

Definitions

def pm source · line 22 · raw

@+one:Nat -> Nat

def rot source · line 49 · raw

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

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

def s21 source · line 54 · raw

@+one:Nat -> Nat

def dbound source · line 58 · raw

@+one:Nat -> Nat

the fold's limb bound: 321 * 2^21 < 2^30

def pv source · line 135 · raw

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

def inv source · line 139 · raw

@+h:List<&2, U32> -> Bool

the limb invariant: 17 limbs, all of 8 bits, limb 16 at most 4

def zz source · line 293 · raw

@+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> List<&2, U32>

def bk source · line 297 · raw

@+r:List<&2, U32> -> @+h:List<&2, U32> -> @+c:List<&2, U32> -> Nat

the multiple of p dropped by one block

def s8fit source · line 313 · raw

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

def mbound source · line 319 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+r:List<&2, U32> -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> {Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r), Nat.mul(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, one))) == s21(one) : Nat}

len(r) * (2^9 * 2^8) == 2^21