proofs/lib/lemmas/proofs/word_subtraction.bend
bend-collections-laws-containers@1.0.0.0 · 39 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as Numeric
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as Add
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as Addition
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/modular_negation.bend as Negation
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_index.bend as Index
8
9def shape(+n: Nat, a: Word(n), b: Word(n), pair: Bool & Bool) -> {Word.adc.con(n, a, b, True{}, pair) == WCon{Add.sum_bit(pair), Word.adc(n, a, b, True{}, Add.carry_bit(pair))} : Word(1n+n)}:
10 (sum, carry) = pair
11 {==}
12
13# The subtraction branch of existing Base.adc equals addition of complemented
14# bits with the same input carry. No arithmetic algorithm is substituted.
15def flip(+n: Nat, a: Word(n), b: Word(n), +carry: Bool) -> {Word.adc(n, a, b, True{}, carry) == Word.adc(n, a, Word.not(n, b), False{}, carry) : Word(n)}:
16 match n:
17 case 0n: {==}
18 case 1n+ +p:
19 match a b:
20 case WCon{+x, +at} WCon{+y, +bt}:
21 Equal.trans(Word(1n+p), Word.adc.con(p, at, bt, True{}, Bool.full_add(x, Bool.not(y), carry)), WCon{Add.sum_bit(Bool.full_add(x, Bool.not(y), carry)), Word.adc(p, at, bt, True{}, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry)))}, Word.adc.con(p, at, Word.not(p, bt), False{}, Bool.full_add(x, Bool.not(y), carry)), shape(p, at, bt, Bool.full_add(x, Bool.not(y), carry)), Equal.trans(Word(1n+p), WCon{Add.sum_bit(Bool.full_add(x, Bool.not(y), carry)), Word.adc(p, at, bt, True{}, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry)))}, WCon{Add.sum_bit(Bool.full_add(x, Bool.not(y), carry)), Word.adc(p, at, Word.not(p, bt), False{}, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry)))}, Word.adc.con(p, at, Word.not(p, bt), False{}, Bool.full_add(x, Bool.not(y), carry)), Equal.cong(Word(p), Word(1n+p), w => WCon{Add.sum_bit(Bool.full_add(x, Bool.not(y), carry)), w}, Word.adc(p, at, bt, True{}, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry))), Word.adc(p, at, Word.not(p, bt), False{}, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry))), flip(p, at, bt, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry)))), Equal.sym(Word(1n+p), Word.adc.con(p, at, Word.not(p, bt), False{}, Bool.full_add(x, Bool.not(y), carry)), WCon{Add.sum_bit(Bool.full_add(x, Bool.not(y), carry)), Word.adc(p, at, Word.not(p, bt), False{}, Add.carry_bit(Bool.full_add(x, Bool.not(y), carry)))}, Add.adc_shape(p, at, Word.not(p, bt), Bool.full_add(x, Bool.not(y), carry)))))
22
23def complement_form(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.sub(n, a, b) == S.from_nat(n, 1n+Nat.add(S.unsigned(n, a), S.unsigned(n, Word.not(n, b)))) : Word(n)}:
24 Equal.trans(Word(n), Word.sub(n, a, b), Word.adc(n, a, Word.not(n, b), False{}, True{}), S.from_nat(n, 1n+Nat.add(S.unsigned(n, a), S.unsigned(n, Word.not(n, b)))), flip(n, a, b, True{}), Addition.with_carry(n, a, Word.not(n, b), True{}))
25
26# Exact modulo subtraction expressed using nonnegative mathematical magnitudes.
27def refines(+n: Nat, +a: Word(n), +b: Word(n)) -> {Word.sub(n, a, b) == S.from_nat(n, Nat.add(S.unsigned(n, a), Nat.sub(S.scale_binary(n, 1n), S.unsigned(n, b)))) : Word(n)}:
28 %Equal.sym(Nat, Nat.sub(S.scale_binary(n, 1n), S.unsigned(n, b)), 1n+S.unsigned(n, Word.not(n, b)), Negation.complement_distance(n, b)) : {Word.sub(n, a, b) == S.from_nat(n, Nat.add(S.unsigned(n, a), _)) : Word(n)}
29 %Equal.sym(Nat, Nat.add(S.unsigned(n, a), 1n+S.unsigned(n, Word.not(n, b))), 1n+Nat.add(S.unsigned(n, a), S.unsigned(n, Word.not(n, b))), Index.add_right_successor(S.unsigned(n, a), S.unsigned(n, Word.not(n, b)))) : {Word.sub(n, a, b) == S.from_nat(n, _) : Word(n)}
30 complement_form(n, a, b)
31
32# Concrete primitive used in wide.digit_result; the independent complement
33# conservation above gives the equivalent nonnegative modular-subtraction form.
34def u32_refines(a: U32, b: U32) -> {U32.sub(a, b) == U32{S.from_nat(32n, 1n+Nat.add(U32.to_nat(a), U32.to_nat(U32.not(b))))} : U32}:
35 match a b:
36 case U32{+x} U32{+y}:
37 %Equal.sym(Nat, Word.to_nat(32n, x), S.unsigned(32n, x), Numeric.primitive_word_interpretation(32n, x)) : {U32.sub(U32{x}, U32{y}) == U32{S.from_nat(32n, 1n+Nat.add(_, Word.to_nat(32n, Word.not(32n, y))))} : U32}
38 %Equal.sym(Nat, Word.to_nat(32n, Word.not(32n, y)), S.unsigned(32n, Word.not(32n, y)), Numeric.primitive_word_interpretation(32n, Word.not(32n, y))) : {U32.sub(U32{x}, U32{y}) == U32{S.from_nat(32n, 1n+Nat.add(S.unsigned(32n, x), _))} : U32}
39 Equal.cong(Word(32n), U32, w => U32{w}, Word.sub(32n, x, y), S.from_nat(32n, 1n+Nat.add(S.unsigned(32n, x), S.unsigned(32n, Word.not(32n, y)))), complement_form(32n, x, y))