def with_carry

bend-collections-laws-math@1.0.0.0 · proofs/lib/lemmas/proofs/word_addition.bend:20

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/addition.bend as Add
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as M

20def with_carry(+n: Nat, +a: Word(n), +b: Word(n), +carry: Bool) -> {Word.adc(n, a, b, False{}, carry) == S.from_nat(n, Nat.add(S.bit_value(carry), Nat.add(S.unsigned(n, a), S.unsigned(n, b)))) : Word(n)}:
21  %Add.adc_conservation(n, a, b, carry) : {Word.adc(n, a, b, False{}, carry) == S.from_nat(n, _) : Word(n)}
22  Equal.sym(Word(n), S.from_nat(n, Nat.add(S.unsigned(n, Word.adc(n, a, b, False{}, carry)), S.scale_binary(n, S.bit_value(Add.carry_out(n, a, b, carry))))), Word.adc(n, a, b, False{}, carry), M.reconstruct(n, Word.adc(n, a, b, False{}, carry), S.bit_value(Add.carry_out(n, a, b, carry))))