def load_len

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/mac.bend:201

import Base
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/limbs.bend as Li
import bend-collections-laws-crypto@1.0.0.0/src/crypto/poly1305/poly1305.bend as P
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/value.bend as V

201def load_len(+b: List<&2, U32>) -> {Nat.is_le(V.len(P.load(Li.take(16n, b))), 17n) == True{} : Bool}:
202  +t = Li.take(16n, b)
203  A.le_substl(V.len(List.append(&2, U32, t, [1])), V.len(P.load(t)), 17n, A.sy(V.len(P.load(t)), V.len(List.append(&2, U32, t, [1])), mask_len(List.append(&2, U32, t, [1]))),
204    A.le_substl(Nat.add(V.len(t), 1n), V.len(List.append(&2, U32, t, [1])), 17n, A.sy(V.len(List.append(&2, U32, t, [1])), Nat.add(V.len(t), 1n), app1(t)),
205      A.le_substl(1n+V.len(t), Nat.add(V.len(t), 1n), 17n, A.sy(Nat.add(V.len(t), 1n), 1n+V.len(t), A.tr(Nat.add(V.len(t), 1n), 1n+Nat.add(V.len(t), 0n), 1n+V.len(t), N.add_succ(V.len(t), 0n), Equal.cong(Nat, Nat, z => 1n+z, Nat.add(V.len(t), 0n), V.len(t), N.add_zero(V.len(t))))), V.len_take(16n, b))))