def double_value

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/division_no_overflow.bend:70

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Shift

70def double_value(d: U32, high: {W.last(32n, bits(d)) == False{} : Bool}) -> {U32.to_nat(U32.shl(d)) == Nat.double(U32.to_nat(d)) : Nat}:
71  match d:
72    case U32{+w}:
73      %Equal.sym(Word(32n), Word.shl(32n, w), Word.shl.put(32n, False{}, w), Shift.same_as_put(32n, w)) : {Word.to_nat(32n, _) == Nat.double(Word.to_nat(32n, w)) : Nat}
74      decoded_high(w, False{}, high)