def exact

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/division_shift.bend:53

import Base
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/word_shift.bend as Shift
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/addition_bounds.bend as Bounds

53# The range premise concerns the inputs and discharges discarded carry.
54def exact(+n: Nat, +w: Word(n), +bit: Bool, bound: {Nat.is_lt(Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))), S.scale_binary(n, 1n)) == True{} : Bool}) -> {S.unsigned(n, Word.shl.put(n, bit, w)) == Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))) : Nat}:
55  Bounds.no_wrap(n, S.unsigned(n, Word.shl.put(n, bit, w)), Nat.add(S.bit_value(bit), Nat.double(S.unsigned(n, w))), Shift.carry(n, bit, w), Shift.conservation(n, bit, w), bound)