def from_nat_value_k

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/u32.bend:66

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV

66# Width-generic wrappers: bounds are 2^k with k <= n, never a closed 2^32.
67def from_nat_value_k(+n: Nat, +k: Nat, +v: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}, +hv: {Nat.is_lt(v, SC.pow2(k)) == True{} : Bool}) -> {S.unsigned(n, S.from_nat(n, v)) == v : Nat}:
68  WV.from_nat_value(n, v, N.lt_le_trans(v, SC.pow2(k), Nat.pow(2n, n), hv, pow2_le_pow(n, k, hk)))