~/bend-docscommunity

proofs/crypto/poly1305/value.bend checks

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

13 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

Laws

law le_mono provedsource · line 43 · raw

@+xs:List<&2, U32> -> @+b:Nat -> @+c:Nat -> @+hb:{Nat.is_le(b, c) == True{} : Bool} -> @+h:{le_all(xs, b) == True{} : Bool} -> {le_all(xs, c) == True{} : Bool}

law add_ev provedsource · line 63 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+b1:Nat -> @+b2:Nat -> @+ha:{le_all(a, b1) == True{} : Bool} -> @+hb:{le_all(b, b2) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.add(b1, b2)) == True{} : Bool} -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.add(a, b)) == Nat.add(ev(a), ev(b)) : Nat}

law add_le provedsource · line 87 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+b1:Nat -> @+b2:Nat -> @+ha:{le_all(a, b1) == True{} : Bool} -> @+hb:{le_all(b, b2) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.add(b1, b2)) == True{} : Bool} -> {le_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.add(a, b), Nat.add(b1, b2)) == True{} : Bool}

law scale_ev provedsource · line 114 · raw

@+c:U32 -> @+a:List<&2, U32> -> @+b:Nat -> @+bc:Nat -> @+ha:{le_all(a, b) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), bc) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.mul(b, bc)) == True{} : Bool} -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.scale(c, a)) == Nat.mul(ev(a), v(c)) : Nat}

law scale_le provedsource · line 137 · raw

@+c:U32 -> @+a:List<&2, U32> -> @+b:Nat -> @+bc:Nat -> @+ha:{le_all(a, b) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), bc) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.mul(b, bc)) == True{} : Bool} -> {le_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.scale(c, a), Nat.mul(b, bc)) == True{} : Bool}

law mul_le provedsource · line 158 · raw

@+x:List<&2, U32> -> @+r:List<&2, U32> -> @+bx:Nat -> @+br:Nat -> @+hx:{le_all(x, bx) == True{} : Bool} -> @+hr:{le_all(r, br) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool} -> {le_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.mul(x, r), Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool}

law mul_ev provedsource · line 181 · raw

@+x:List<&2, U32> -> @+r:List<&2, U32> -> @+bx:Nat -> @+br:Nat -> @+hx:{le_all(x, bx) == True{} : Bool} -> @+hr:{le_all(r, br) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.mul(List.length(&2, U32, r), Nat.mul(bx, br))) == True{} : Bool} -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.mul(x, r)) == Nat.mul(ev(x), ev(r)) : Nat}

law pos_zero provedsource · line 224 · raw

@+n:Nat -> {pos(n, 0n) == 0n : Nat}

law pos_add provedsource · line 233 · raw

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

law skip_nil provedsource · line 244 · raw

@+n:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, []) == [] : List<&2, U32>}

law ts_ev provedsource · line 254 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {ev(xs) == Nat.add(ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs)), pos(n, ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, xs)))) : Nat}

ev(xs) = ev(take n xs) + 2^(8n) ev(skip n xs)

law take_nil_ev provedsource · line 270 · raw

@+n:Nat -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, [])) == 0n : Nat}

law fit_ev provedsource · line 279 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.fit(n, xs)) == ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs)) : Nat}

law fits_zero provedsource · line 297 · raw

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

law carry_ev provedsource · line 353 · raw

@+n:Nat -> @+ds:List<&2, U32> -> @+u:U32 -> @+j:Nat -> @+hj:{Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool} -> @+hd:{fit_all(ds, Nat.add(8n, j)) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(8n, j), v(u)) == True{} : Bool} -> {Nat.add(ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.carry(n, ds, u)), pos(1n+n, ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(1n+n, ds)))) == Nat.add(v(u), ev(ds)) : Nat}

A carry pass over n limbs keeps the value: carry(n, ds, u) + 2^(8(n+1)) ds[n+1..] == u + ds.

law carry_lo provedsource · line 408 · raw

@+n:Nat -> @+ds:List<&2, U32> -> @+u:U32 -> {fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.carry(n, ds, u)), 8n) == True{} : Bool}

every limb below the top one has 8 bits

law carry_top provedsource · line 424 · raw

@+n:Nat -> @+ds:List<&2, U32> -> @+u:U32 -> @+j:Nat -> @+hj:{Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool} -> @+hd:{fit_all(ds, Nat.add(8n, j)) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(8n, j), v(u)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(9n, j), v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.carry(n, ds, u))))) == True{} : Bool}

the top limb fits 9 + j bits

law carry_len provedsource · line 441 · raw

@+n:Nat -> @+ds:List<&2, U32> -> @+u:U32 -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.carry(n, ds, u)) == 1n+n : Nat}

law sq_ev provedsource · line 456 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {Nat.add(Nat.add(ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.split(n, xs)), pos(n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(2n, v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.quot(n, xs))))), pos(1n+n, ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(1n+n, xs)))) == ev(xs) : Nat}

law len_add provedsource · line 496 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+n:Nat -> @+ha:{Nat.is_le(len(a), n) == True{} : Bool} -> @+hb:{Nat.is_le(len(b), n) == True{} : Bool} -> {Nat.is_le(len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.add(a, b)), n) == True{} : Bool}

law len_scale provedsource · line 513 · raw

@+c:U32 -> @+a:List<&2, U32> -> {len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.scale(c, a)) == len(a) : Nat}

law len_mul provedsource · line 523 · raw

@+x:List<&2, U32> -> @+r:List<&2, U32> -> @+n:Nat -> @+hx:{Nat.is_le(len(x), n) == True{} : Bool} -> {Nat.is_le(len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.mul(x, r)), Nat.add(len(r), n)) == True{} : Bool}

law len_take provedsource · line 538 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {Nat.is_le(len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs)), n) == True{} : Bool}

law len_skip provedsource · line 549 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+h:{Nat.is_le(len(xs), Nat.add(n, b)) == True{} : Bool} -> {Nat.is_le(len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, xs)), b) == True{} : Bool}

law skip_long provedsource · line 562 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+h:{Nat.is_le(len(xs), n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, xs) == [] : List<&2, U32>}

law le_take provedsource · line 577 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+h:{le_all(xs, b) == True{} : Bool} -> {le_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs), b) == True{} : Bool}

law le_skip provedsource · line 590 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+b:Nat -> @+h:{le_all(xs, b) == True{} : Bool} -> {le_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, xs), b) == True{} : Bool}

law fit_le provedsource · line 603 · raw

@+xs:List<&2, U32> -> @+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:{fit_all(xs, k) == True{} : Bool} -> {le_all(xs, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool}

law le_fit provedsource · line 616 · raw

@+xs:List<&2, U32> -> @+b:Nat -> @+k:Nat -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+hb:{Nat.is_lt(b, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, one)) == True{} : Bool} -> @+h:{le_all(xs, b) == True{} : Bool} -> {fit_all(xs, k) == True{} : Bool}

law fit_mono provedsource · line 631 · raw

@+xs:List<&2, U32> -> @+a:Nat -> @+b:Nat -> @+hab:{Nat.is_le(a, b) == True{} : Bool} -> @+h:{fit_all(xs, a) == True{} : Bool} -> {fit_all(xs, b) == True{} : Bool}

law fit_take provedsource · line 644 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+k:Nat -> @+h:{fit_all(xs, k) == True{} : Bool} -> {fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs), k) == True{} : Bool}

law ev_lt provedsource · line 658 · raw

@+xs:List<&2, U32> -> @+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:{fit_all(xs, 8n) == True{} : Bool} -> {Nat.is_lt(ev(xs), pos(len(xs), one)) == True{} : Bool}

limbs of 8 bits: the value is below 2^(8 len)

law fit_take_nil provedsource · line 677 · raw

@+n:Nat -> @+k:Nat -> {fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, []), k) == True{} : Bool}

law split_fit provedsource · line 687 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+h:{fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs), 8n) == True{} : Bool} -> {fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.split(n, xs), 8n) == True{} : Bool}

law fit_split provedsource · line 703 · raw

@+n:Nat -> @+xs:List<&2, U32> -> @+k:Nat -> @+h1:{fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(n, xs), k) == True{} : Bool} -> @+h2:{fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, xs), k) == True{} : Bool} -> {fit_all(xs, k) == True{} : Bool}

law quot_top provedsource · line 717 · raw

@+n:Nat -> @+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.quot(n, xs) == U32.shrn(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(n, xs)), 2n) : U32}

law ev_one provedsource · line 728 · raw

@+xs:List<&2, U32> -> @+h:{Nat.is_le(len(xs), 1n) == True{} : Bool} -> {ev(xs) == v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(xs)) : Nat}

Definitions

def v source · line 21 · raw

@+x:U32 -> Nat

def ev source · line 24 · raw

@xs:List<&2, U32> -> Nat

def le_all source · line 29 · raw

@xs:List<&2, U32> -> @+b:Nat -> Bool

def hd_le source · line 34 · raw

@+x:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+h:{le_all(x <> t, b) == True{} : Bool} -> {Nat.is_le(v(x), b) == True{} : Bool}

def tl_le source · line 37 · raw

@+x:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+h:{le_all(x <> t, b) == True{} : Bool} -> {le_all(t, b) == True{} : Bool}

def cons_le source · line 40 · raw

@+x:U32 -> @+t:List<&2, U32> -> @+b:Nat -> @+hx:{Nat.is_le(v(x), b) == True{} : Bool} -> @+ht:{le_all(t, b) == True{} : Bool} -> {le_all(x <> t, b) == True{} : Bool}

def add1 source · line 60 · raw

@+x:U32 -> @+y:U32 -> @+b1:Nat -> @+b2:Nat -> @+hx:{Nat.is_le(v(x), b1) == True{} : Bool} -> @+hy:{Nat.is_le(v(y), b2) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.add(b1, b2)) == True{} : Bool} -> {v(U32.add(x, y)) == Nat.add(v(x), v(y)) : Nat}

the exact U32 sum of two limbs whose bounds add up within 32 bits

def mul1 source · line 110 · raw

@+x:U32 -> @+c:U32 -> @+b:Nat -> @+bc:Nat -> @+hx:{Nat.is_le(v(x), b) == True{} : Bool} -> @+hc:{Nat.is_le(v(c), bc) == True{} : Bool} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(32n, Nat.mul(b, bc)) == True{} : Bool} -> {v(U32.mul(x, c)) == Nat.mul(v(x), v(c)) : Nat}

def pos source · line 219 · raw

@n:Nat -> @+y:Nat -> Nat

y at limb position n: y * 2^(8n)

def fit_all source · line 292 · raw

@xs:List<&2, U32> -> @+k:Nat -> Bool

def hd0_fit source · line 306 · raw

@+ds:List<&2, U32> -> @+k:Nat -> @+h:{fit_all(ds, k) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(ds))) == True{} : Bool}

def tl_fit source · line 311 · raw

@+ds:List<&2, U32> -> @+k:Nat -> @+h:{fit_all(ds, k) == True{} : Bool} -> {fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.tl(ds), k) == True{} : Bool}

def hd_tl_ev source · line 316 · raw

@+ds:List<&2, U32> -> {ev(ds) == Nat.add(v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(ds)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.tl(ds)))) : Nat}

def skip_succ source · line 321 · raw

@+k:Nat -> @+ds:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(1n+k, ds) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(k, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.tl(ds)) : List<&2, U32>}

def sh3 source · line 327 · raw

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

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

def sh4 source · line 332 · raw

@+a:Nat -> @+b:Nat -> @+c:Nat -> @+d:Nat -> {Nat.add(Nat.add(Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, b)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, c)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, d)) == Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(8n, Nat.add(Nat.add(b, c), d))) : Nat}

def step_fit source · line 338 · raw

@+ds:List<&2, U32> -> @+u:U32 -> @+j:Nat -> @+hd:{fit_all(ds, Nat.add(8n, j)) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(8n, j), v(u)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(9n, j), Nat.add(v(u), v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(ds)))) == True{} : Bool}

the sum u + ds[0] of one carry step, exact and within 9 + j bits

def step_ev source · line 341 · raw

@+ds:List<&2, U32> -> @+u:U32 -> @+j:Nat -> @+hj:{Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool} -> @+hd:{fit_all(ds, Nat.add(8n, j)) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(8n, j), v(u)) == True{} : Bool} -> {v(U32.add(u, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(ds))) == Nat.add(v(u), v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(ds))) : Nat}

def next_fit source · line 345 · raw

@+ds:List<&2, U32> -> @+u:U32 -> @+j:Nat -> @+hj:{Nat.is_le(Nat.add(9n, j), 32n) == True{} : Bool} -> @+hd:{fit_all(ds, Nat.add(8n, j)) == True{} : Bool} -> @+hu:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(8n, j), v(u)) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(Nat.add(8n, j), v(U32.shrn(U32.add(u, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(ds)), 8n))) == True{} : Bool}

the next carry high(8, s) fits 8 + j bits again

def len source · line 493 · raw

@xs:List<&2, U32> -> Nat