1	import Base
2	import ./numeric.bend as Numeric
3	import ../spec/numeric.bend as S
4	import ./addition.bend as Add
5	import ./word_addition.bend as Addition
6	import ./modular_negation.bend as Negation
7	import ./map_index.bend as Index
8	
9	def 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.
15	def 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	
23	def 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.
27	def 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.
34	def 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))