proofs/crypto/poly1305/mac.bend checks

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

18 imports

import Base
import ../../../spec/lib/common.bend as C
import ../../../spec/crypto/poly1305.bend as R
import ../../../src/crypto/poly1305/limbs.bend as Li
import ../../../src/crypto/poly1305/poly1305.bend as P
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/w64sh.bend as SH
import ../../math/typed/f64bits.bend as FB
import ../../math/natural/arith.bend as NR
import ./arith.bend as A
import ./value.bend as V
import ./step.bend as ST
import ./modp.bend as MP
import ./final.bend as F

Laws

law mask_ev provedsource · line 29 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.mask(xs)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_num(xs) : Nat}

law mask_fit provedsource · line 38 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.mask(xs), 8n) == True{} : Bool}

law mask_len provedsource · line 50 · raw

@+xs:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.mask(xs)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(xs) : Nat}

law take_prefix provedsource · line 59 · raw

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

law skip_suffix provedsource · line 70 · raw

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

law cmask provedsource · line 81 · raw

@+i:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.clamp_mask(i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.clamp_mask(i) : U32}

law clamp_eq provedsource · line 105 · raw

@+xs:List<&2, U32> -> @+i:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.clamp(xs, i) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.clamp_from(xs, i) : List<&2, U32>}

law clamp_len provedsource · line 118 · raw

@+xs:List<&2, U32> -> @+i:Nat -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.clamp(xs, i)) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(xs) : Nat}

law fit_fit provedsource · line 128 · raw

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

law take_all provedsource · line 139 · raw

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

law r_ev provedsource · line 153 · raw

@+key:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.r_key(key)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_num(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.clamp(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.prefix(16n, key))) : Nat}

the key's r and s limbs

law s_ev provedsource · line 167 · raw

@+key:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.s_key(key)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_num(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.prefix(16n, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.suffix(16n, key))) : Nat}

law app1 provedsource · line 178 · raw

@+t:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(List.append(&2, U32, t, [1])) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(t), 1n) : Nat}

law pp_eq provedsource · line 188 · raw

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

p == 1 + bp

law absorb_ok provedsource · line 207 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+fuel:Nat -> @+msg:List<&2, U32> -> @+r:List<&2, U32> -> @+h:List<&2, U32> -> @+a:Nat -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> @+hrf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(r, 8n) == True{} : Bool} -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+ha:{Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 1n+bp) == a : Nat} -> {Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.absorb(fuel, msg, r, h)), 1n+bp) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.absorb(0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.blocks(fuel, msg), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(r), a) : Nat}

law absorb_inv provedsource · line 223 · raw

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

law bp5 provedsource · line 307 · raw

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

law tag_main provedsource · line 317 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+key:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.tag(key, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.poly1305_mac(key, msg) : List<&2, U32>}

law mac_correct provedsource · line 345 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.mac(key, msg) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg) : List<&2, U32>}

The implementation's tag is the RFC 8439 tag, for every key and message.

law le_bytes_len provedsource · line 355 · raw

@+n:Nat -> @+x:Nat -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_bytes(n, x)) == n : Nat}

law mac_length provedsource · line 366 · raw

@+key:List<&2, U32> -> @+msg:List<&2, U32> -> {List.length(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.mac(key, msg)) == 16n : Nat}

The tag has 16 bytes.

Definitions

def load_len source · line 201 · raw

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

def step_mod source · line 249 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+r:List<&2, U32> -> @+h:List<&2, U32> -> @+m:List<&2, U32> -> @+a:Nat -> @+hrl:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(r) == 16n : Nat} -> @+hrf:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(r, 8n) == True{} : Bool} -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+ha:{Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 1n+bp) == a : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.modp(Nat.mul(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(r), Nat.add(a, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_num(List.append(&2, U32, 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.prefix(16n, m), [1]))))) == Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.block(r, h, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/poly1305.load(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, m)))), 1n+bp) : Nat}

one block: (r (a + n)) mod p == ev(block) mod p

def bpv source · line 304 · raw

@+one:Nat -> Nat