~/jendhub

def u16

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/poly1305/final.bend:273

import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/final.bend as Final
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/logic.bend as L
import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
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

273# 2^128 + 5 <= 2^130, 16 <= 2^128
274def u16(+one: Nat, +h1: {one == 1n : Nat}) -> {Nat.is_le(16n, V.pos(16n, one)) == True{} : Bool}:
275  N.le_trans(16n, C.shift(4n, one), V.pos(16n, one), L.subst(Nat, z => {Nat.is_le(16n, C.shift(4n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(124n, C.shift(4n, one)))

Uses (9)

Used by (2)