def pad_value

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

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

125def pad_value(+n: Nat, +w: Word(n)) -> {S.unsigned(1n+n, Word.shr.pad(n, w)) == S.unsigned(n, w) : Nat}:
126  match n:
127    case 0n:
128      match w:
129        case WNil{}:
130          {==}
131    case 1n+p:
132      match w:
133        case WCon{b, t}:
134          Equal.cong(Nat, Nat, v => Nat.add(S.bit_value(b), Nat.double(v)), S.unsigned(1n+p, Word.shr.pad(p, t)), S.unsigned(p, t), pad_value(p, t))