1	import Base
2	import ./natural_addition.bend as Addition
3	import ./word_arithmetic.bend as WordArithmetic
4	import ./word_encoding.bend as WordEncoding
5	
6	law undo:
7	  for +n: Nat
8	  for +a: Word(n)
9	  for +b: Word(n)
10	  for +f: Bool
11	  for +c: Bool
12	  {Word.adc(n,Word.adc(n,a,b,f,c),b,Bool.not(f),Bool.not(c)) == a : Word(n)}
13	def undo(n,a,b,f,c):
14	  match n:
15	    case 0n:
16	      WNil{} = a
17	      {==}
18	    case 1n+ +p:
19	      match a b f c:
20	        case WCon{False{},+at} WCon{False{},+bt} False{} False{}:
21	          %undo(p,at,bt,False{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{False{},
22	              _} : Word(1n+p)}
23	          {==}
24	        case WCon{False{},+at} WCon{False{},+bt} False{} True{}:
25	          %undo(p,at,bt,False{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{False{},
26	              _} : Word(1n+p)}
27	          {==}
28	        case WCon{False{},+at} WCon{False{},+bt} True{} False{}:
29	          %undo(p,at,bt,True{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{False{},
30	              _} : Word(1n+p)}
31	          {==}
32	        case WCon{False{},+at} WCon{False{},+bt} True{} True{}:
33	          %undo(p,at,bt,True{},True{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{False{},
34	              _} : Word(1n+p)}
35	          {==}
36	        case WCon{False{},+at} WCon{True{},+bt} False{} False{}:
37	          %undo(p,at,bt,False{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{False{},
38	              _} : Word(1n+p)}
39	          {==}
40	        case WCon{False{},+at} WCon{True{},+bt} False{} True{}:
41	          %undo(p,at,bt,False{},True{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{False{},
42	              _} : Word(1n+p)}
43	          {==}
44	        case WCon{False{},+at} WCon{True{},+bt} True{} False{}:
45	          %undo(p,at,bt,True{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{False{},
46	              _} : Word(1n+p)}
47	          {==}
48	        case WCon{False{},+at} WCon{True{},+bt} True{} True{}:
49	          %undo(p,at,bt,True{},False{}) : {WCon{False{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{False{},
50	              _} : Word(1n+p)}
51	          {==}
52	        case WCon{True{},+at} WCon{False{},+bt} False{} False{}:
53	          %undo(p,at,bt,False{},False{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},False{}),bt,True{},True{})} == WCon{True{},
54	              _} : Word(1n+p)}
55	          {==}
56	        case WCon{True{},+at} WCon{False{},+bt} False{} True{}:
57	          %undo(p,at,bt,False{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{True{},_} : Word(1n+p)}
58	          {==}
59	        case WCon{True{},+at} WCon{False{},+bt} True{} False{}:
60	          %undo(p,at,bt,True{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{True{},_} : Word(1n+p)}
61	          {==}
62	        case WCon{True{},+at} WCon{False{},+bt} True{} True{}:
63	          %undo(p,at,bt,True{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{True{},_} : Word(1n+p)}
64	          {==}
65	        case WCon{True{},+at} WCon{True{},+bt} False{} False{}:
66	          %undo(p,at,bt,False{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{True{},_} : Word(1n+p)}
67	          {==}
68	        case WCon{True{},+at} WCon{True{},+bt} False{} True{}:
69	          %undo(p,at,bt,False{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,False{},True{}),bt,True{},False{})} == WCon{True{},_} : Word(1n+p)}
70	          {==}
71	        case WCon{True{},+at} WCon{True{},+bt} True{} False{}:
72	          %undo(p,at,bt,True{},False{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},False{}),bt,False{},True{})} == WCon{True{},_} : Word(1n+p)}
73	          {==}
74	        case WCon{True{},+at} WCon{True{},+bt} True{} True{}:
75	          %undo(p,at,bt,True{},True{}) : {WCon{True{},Word.adc(p,Word.adc(p,at,bt,True{},True{}),bt,False{},False{})} == WCon{True{},_} : Word(1n+p)}
76	          {==}
77	
78	def subtract_add(+a: U32,+b: U32) -> {U32.sub(U32.add(a,b),b) == a : U32}:
79	  match a b:
80	    case U32{+x} U32{+y}:
81	      %undo(32n,x,y,False{},False{}) : {U32{Word.sub(32n,Word.add(32n,x,y),y)} == U32{_} : U32}
82	      {==}
83	
84	def add_subtract(+a: U32,+b: U32) -> {U32.add(U32.sub(a,b),b) == a : U32}:
85	  match a b:
86	    case U32{+x} U32{+y}:
87	      %undo(32n,x,y,True{},True{}) : {U32{Word.add(32n,Word.sub(32n,x,y),y)} == U32{_} : U32}
88	      {==}
89	
90	def encoded_subtract_add(+a: Nat,+b: Nat) -> {U32.sub(U32.from_nat(Nat.add(a,b)),U32.from_nat(b)) == U32.from_nat(a) : U32}:
91	  %WordArithmetic.native_add(a,b) : {U32.sub(_,U32.from_nat(b)) == U32.from_nat(a) : U32}
92	  subtract_add(U32.from_nat(a),U32.from_nat(b))
93	
94	def restore(+a: Nat,+b: Nat,h: {Nat.is_le(b,a) == True{} : Bool}) -> {Nat.add(Nat.sub(a,b),b) == a : Nat}:
95	  match a b:
96	    case 0n 0n:
97	      {==}
98	    case 0n 1n+b:
99	      Empty.absurd({Nat.add(Nat.sub(0n,1n+b),1n+b) == 0n : Nat},WordEncoding.false_true(h))
100	    case 1n+ +a 0n:
101	      Addition.zero_right(1n+a)
102	    case 1n+ +a 1n+ +b:
103	      %Equal.sym(Nat,Nat.add(Nat.sub(a,b),1n+b),1n+Nat.add(Nat.sub(a,b),b),Addition.successor_right(Nat.sub(a,b),b)) : {_ == 1n+a : Nat}
104	      %restore(a,b,h) : {1n+Nat.add(Nat.sub(a,b),b) == 1n+_ : Nat}
105	      {==}
106	
107	def encoded_subtract(+a: Nat,+b: Nat,h: {Nat.is_le(b,a) == True{} : Bool}) -> {U32.sub(U32.from_nat(a),
108	    U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}:
109	  %restore(a,b,h) : {U32.sub(U32.from_nat(_),U32.from_nat(b)) == U32.from_nat(Nat.sub(a,b)) : U32}
110	  encoded_subtract_add(Nat.sub(a,b),b)