~/bend-docscommunity

proofs/crypto/poly1305/final.bend checks

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

19 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 ../../lib/nat.bend as N
import ../../lib/logic.bend as L
import ../../lib/arith.bend as AR
import ../../lib/u32.bend as U3
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/typed/shrn.bend as SHN
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

Laws

law wand0 provedsource · line 31 · raw

@+n:Nat -> @+w:Word(n) -> {Word.and(n, Word.zero(n), w) == Word.zero(n) : Word(n)}

law wand1 provedsource · line 45 · raw

@+n:Nat -> @+w:Word(n) -> {Word.and(n, wones(n), w) == w : Word(n)}

law wxor0 provedsource · line 59 · raw

@+n:Nat -> @+w:Word(n) -> {Word.xor(n, w, Word.zero(n)) == w : Word(n)}

law wxor2 provedsource · line 76 · raw

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

law sel0 provedsource · line 108 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(a) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(b) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.select(0, a, b) == a : List<&2, U32>}

law sel1 provedsource · line 124 · raw

@+a:List<&2, U32> -> @+b:List<&2, U32> -> @+h:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(a) == 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(b) : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.select(4294967295, a, b) == b : List<&2, U32>}

law len_take_eq provedsource · line 140 · raw

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

law g_ev provedsource · line 169 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(gg(h)) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 5n) : Nat}

law hsplit provedsource · line 208 · raw

@+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h) == Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, h)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(16n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(16n, h))))) : Nat}

law hlt provedsource · line 220 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {Nat.is_lt(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(16n, one), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one))) == True{} : Bool}

ev(h) < 2^128 + 2^130

law gsplit provedsource · line 242 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 5n) == Nat.add(lg(h), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(128n, tg(h))) : Nat}

law bval provedsource · line 258 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.v(bb(h)) == qq(h) : Nat}

law qlt2 provedsource · line 281 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {Nat.is_lt(qq(h), 2n) == True{} : Bool}

law freeze_fit provedsource · line 327 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h), 8n) == True{} : Bool}

law freeze_len provedsource · line 337 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h)), 16n) == True{} : Bool}

law elg_k provedsource · line 355 · raw

@+k:Nat -> @+x:Nat -> @+lgv:Nat -> @+tgv:Nat -> @+d:Nat -> @+s2:Nat -> @+hs:{x == Nat.add(lgv, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, tgv)) : Nat} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, lgv) == True{} : Bool} -> @+hx:{x == Nat.add(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, s2)) : Nat} -> {lgv == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, d) : Nat}

the value: the low 128 bits of h mod p lgv == low(k, d) when x = lgv + 2^k tgv with lgv < 2^k and x = d + 2^k s2, for a symbolic k (so that no check unfolds low(128, _) level by level).

law fin_k provedsource · line 372 · raw

@+k:Nat -> @+a:Nat -> @+b:Nat -> @+c:Nat -> @+m:Nat -> @+e1:{a == b : Nat} -> @+e2:{b == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, c) : Nat} -> @+e3:{m == c : Nat} -> {a == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, m) : Nat}

law fe_k provedsource · line 386 · raw

@+k:Nat -> @+x:Nat -> @+lgv:Nat -> @+tgv:Nat -> @+d:Nat -> @+s2:Nat -> @+a:Nat -> @+m:Nat -> @+hs:{x == Nat.add(lgv, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, tgv)) : Nat} -> @+hf:{0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(k, lgv) == True{} : Bool} -> @+hx:{x == Nat.add(d, 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(k, s2)) : Nat} -> @+e1:{a == lgv : Nat} -> @+e3:{m == d : Nat} -> {a == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(k, m) : Nat}

law freeze_ev provedsource · line 448 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(128n, Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 1n+bp)) : Nat}

law bytes_le provedsource · line 462 · raw

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

law bytes_le_to provedsource · line 511 · raw

@+n:Nat -> @+ds:List<&2, U32> -> @+k:Nat -> @+t:Nat -> @+hb:{0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.bytes(n, ds, 0) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_bytes(n, Nat.add(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.v(0), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(ds)), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(n, k))) : List<&2, U32>} -> @+ht:{Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(ds), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(n, k)) == t : Nat} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.bytes(n, ds, 0) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_bytes(n, t) : List<&2, U32>}

bytes_le with the target value rewritten, for any n (so that the rewrite does not unfold le_bytes n levels on both sides).

law tag_eq provedsource · line 525 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+s:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(s, 8n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.bytes(16n, 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.add(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h), s), 0) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_bytes(16n, Nat.add(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 1n+bp), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(s))) : List<&2, U32>}

the tag: (h mod p + s) mod 2^128 as 16 bytes

law fin_eq provedsource · line 559 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+s:List<&2, U32> -> @+hs:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(s, 8n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.fin(h, s) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/crypto/poly1305.le_bytes(16n, Nat.add(Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 1n+bp), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(s))) : List<&2, U32>}

tag_eq through Li.fin (the implementation's entry point).

Definitions

def wones source · line 26 · raw

@n:Nat -> Word(n)

def pick0 source · line 94 · raw

@+x:U32 -> @+y:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.pick(0, x, y) == x : U32}

def pick1 source · line 101 · raw

@+x:U32 -> @+y:U32 -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.pick(4294967295, x, y) == y : U32}

def lt_dbl source · line 155 · raw

@+x:Nat -> @+h:{Nat.is_le(1n, x) == True{} : Bool} -> {Nat.is_lt(x, Nat.double(x)) == True{} : Bool}

x < 2x for x >= 1

def hval source · line 160 · raw

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

the facts about h, g = carry(h + 5) and the choice bit shared by both cases

def gg source · line 163 · raw

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

def qq source · line 166 · raw

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

def lenh source · line 196 · raw

@+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.len(h) == 17n : Nat}

def fith source · line 199 · raw

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

def toph source · line 202 · raw

@+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> {Nat.is_le(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.v(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.hd0(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.skip(16n, h))), 4n) == True{} : Bool}

def len16 source · line 205 · raw

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

def lg source · line 236 · raw

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

def tg source · line 239 · raw

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

def flg source · line 252 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> {0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.fits(128n, lg(h)) == True{} : Bool}

def bb source · line 255 · raw

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

def u16 source · line 274 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(16n, 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(16n, one)) == True{} : Bool}

2^128 + 5 <= 2^130, 16 <= 2^128

def uu source · line 277 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> {Nat.is_le(Nat.add(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(16n, one), 0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.pos(16n, one)), 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one)) == True{} : Bool}

def heqlen source · line 299 · raw

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

def qone source · line 302 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+hc:{Nat.is_eq(qq(h), 0n) == False{} : Bool} -> {qq(h) == 1n : Nat}

def which0 source · line 305 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+hc:{Nat.is_eq(qq(h), 0n) == True{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, h) : List<&2, U32>}

def which1 source · line 311 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+hc:{Nat.is_eq(qq(h), 0n) == False{} : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, gg(h)) : List<&2, U32>}

def which_c source · line 317 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(qq(h), 0n) == c : Bool} -> Or({0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, h) : List<&2, U32>}, {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, gg(h)) : List<&2, U32>})

def fz_fit_o source · line 322 · raw

@+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @o:Or({0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, h) : List<&2, U32>}, {0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h) == 0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.take(16n, gg(h)) : List<&2, U32>}) -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.fit_all(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h), 8n) == True{} : Bool}

def fz_len_o source · line 344 · raw

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

def frz_c source · line 405 · raw

@+one:Nat -> @+h1:{one == 1n : Nat} -> @+bp:Nat -> @+h5:{Nat.add(1n+bp, 5n) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.shift(130n, one) : Nat} -> @+h:List<&2, U32> -> @+hh:{0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/step.inv(h) == True{} : Bool} -> @+c:Bool -> @+hc:{Nat.is_eq(qq(h), 0n) == c : Bool} -> {0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(0xa7e654f9780078ca65bf9e187da99d3e/src/crypto/poly1305/limbs.freeze(h)) == 0xa7e654f9780078ca65bf9e187da99d3e/spec/lib/common.low(128n, Nat.mod(0xa7e654f9780078ca65bf9e187da99d3e/proofs/crypto/poly1305/value.ev(h), 1n+bp)) : Nat}