def pwv

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:340

import Base
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/logic.bend as L

340# a word known to be 2^k has value 2^k (the word stays a variable)
341def pwv(+n: Nat, +k: Nat, +hk: {Nat.is_lt(k, n) == True{} : Bool}, +one: Nat, +h1: {one == 1n : Nat}, +c: Word(n), +hc: {c == pw(n, k) : Word(n)}) -> {uw(n, c) == sc(k, one) : Nat}:
342  +e = L.subst(Word(n), w => {uw(n, w) == sc(k, 1n) : Nat}, pw(n, k), c, Equal.sym(Word(n), c, pw(n, k), hc), pw_val(n, k, hk))
343  L.subst(Nat, o => {uw(n, c) == S.scale_binary(k, o) : Nat}, 1n, one, Equal.sym(Nat, one, 1n, h1), e)