def fits_le_one

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/arith.bend:118

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
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/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW

118# x <= 2^k: x fits k + 1 bits
119def fits_le_one(+k: Nat, +one: Nat, +h1: {one == 1n : Nat}, +x: Nat, +h: {Nat.is_le(x, C.shift(k, one)) == True{} : Bool}) -> {C.fits(1n+k, x) == True{} : Bool}:
120  +s = C.shift(k, one)
121  +h2 = N.le_lt_trans(x, s, Nat.double(s), h, lt_subst(s, Nat.add(s, s), Nat.double(s), sy(Nat.double(s), Nat.add(s, s), NA.double_self(s)), lt_le_add(0n, s, s, s, N.lt_le_trans(0n, 1n, s, {==}, one_le_shift(k, one, h1)), N.le_refl(s))))
122  WW.fits_one(1n+k, one, h1, x, h2)