1	# Modular arithmetic identities used before applying bounded Nat conversion.
2	import Base
3	import ./natural_addition.bend as Addition
4	import ./u32_successor.bend as U32Successor
5	
6	law carry:
7	  for +n: Nat
8	  for +a: Word(n)
9	  for +b: Word(n)
10	  {Word.adc(n,a,b,False{},True{}) == Word.inc(n,Word.add(n,a,b)) : Word(n)}
11	def carry(n,a,b):
12	  match n:
13	    case 0n:
14	      {==}
15	    case 1n+ +p:
16	      match a b:
17	        case WCon{False{},at} WCon{False{},bt}:
18	          {==}
19	        case WCon{False{},+at} WCon{True{},+bt}:
20	          %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)}
21	          {==}
22	        case WCon{True{},+at} WCon{False{},+bt}:
23	          %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)}
24	          {==}
25	        case WCon{True{},at} WCon{True{},bt}:
26	          {==}
27	
28	law inc_left:
29	  for +n: Nat
30	  for +a: Word(n)
31	  for +b: Word(n)
32	  {Word.add(n,Word.inc(n,a),b) == Word.inc(n,Word.add(n,a,b)) : Word(n)}
33	def inc_left(n,a,b):
34	  match n:
35	    case 0n:
36	      {==}
37	    case 1n+ +p:
38	      match a b:
39	        case WCon{False{},at} WCon{False{},bt}:
40	          {==}
41	        case WCon{False{},+at} WCon{True{},+bt}:
42	          %carry(p,at,bt) : {WCon{False{},Word.adc(p,at,bt,False{},True{})} == WCon{False{},_} : Word(1n+p)}
43	          {==}
44	        case WCon{True{},+at} WCon{False{},+bt}:
45	          %inc_left(p,at,bt) : {WCon{False{},Word.add(p,Word.inc(p,at),bt)} == WCon{False{},_} : Word(1n+p)}
46	          {==}
47	        case WCon{True{},+at} WCon{True{},+bt}:
48	          %Equal.sym(Word(p),Word.adc(p,at,bt,False{},True{}),Word.inc(p,Word.add(p,at,bt)),carry(p,at,bt)) : {WCon{True{},Word.add(p,Word.inc(p,
49	                  at),bt)} == WCon{True{},_} : Word(1n+p)}
50	          %inc_left(p,at,bt) : {WCon{True{},Word.add(p,Word.inc(p,at),bt)} == WCon{True{},_} : Word(1n+p)}
51	          {==}
52	
53	def encode(a: Nat,+width: Nat) -> Word(width):
54	  match a:
55	    case 0n:
56	      Word.zero(width)
57	    case 1n+p:
58	      Word.inc(width,encode(p,width))
59	
60	law encode_add:
61	  for +a: Nat
62	  for +b: Nat
63	  for +width: Nat
64	  {Word.add(width,encode(a,width),encode(b,width)) == encode(Nat.add(a,b),width) : Word(width)}
65	def encode_add(a,b,width):
66	  match a:
67	    case 0n:
68	      %Equal.sym(Word(width),Word.add(width,Word.zero(width),encode(b,width)),Word.add(width,encode(b,width),Word.zero(width)),
69	        Word.add_comm(width,Word.zero(width),encode(b,width))) : {_ == encode(b,width) : Word(width)}
70	      U32Successor.adc_zero(width,encode(b,width))
71	    case 1n+ +p:
72	      %Equal.sym(Word(width),Word.add(width,Word.inc(width,encode(p,width)),encode(b,width)),Word.inc(width,Word.add(width,encode(p,width),
73	            encode(b,width))),inc_left(width,encode(p,width),encode(b,width))) : {_ == Word.inc(width,encode(Nat.add(p,b),width)) : Word(width)}
74	      %encode_add(p,b,width) : {Word.inc(width,Word.add(width,encode(p,width),encode(b,width))) == Word.inc(width,_) : Word(width)}
75	      {==}
76	
77	law double_carry:
78	  for +n: Nat
79	  for +w: Word(n)
80	  for +c: Bool
81	  {Word.adc(n,w,w,False{},c) == Word.shl.put(n,c,w) : Word(n)}
82	def double_carry(n,w,c):
83	  match n:
84	    case 0n:
85	      {==}
86	    case 1n+ +p:
87	      match w c:
88	        case WCon{False{},+t} False{}:
89	          %double_carry(p,t,False{}) : {WCon{False{},Word.adc(p,t,t,False{},False{})} == WCon{False{},_} : Word(1n+p)}
90	          {==}
91	        case WCon{False{},+t} True{}:
92	          %double_carry(p,t,False{}) : {WCon{True{},Word.adc(p,t,t,False{},False{})} == WCon{True{},_} : Word(1n+p)}
93	          {==}
94	        case WCon{True{},+t} False{}:
95	          %double_carry(p,t,True{}) : {WCon{False{},Word.adc(p,t,t,False{},True{})} == WCon{False{},_} : Word(1n+p)}
96	          {==}
97	        case WCon{True{},+t} True{}:
98	          %double_carry(p,t,True{}) : {WCon{True{},Word.adc(p,t,t,False{},True{})} == WCon{True{},_} : Word(1n+p)}
99	          {==}
100	
101	def shift_put(+n: Nat,+w: Word(n)) -> {Word.shl(n,w) == Word.shl.put(n,False{},w) : Word(n)}:
102	  match n:
103	    case 0n:
104	      {==}
105	    case 1n+p:
106	      WCon{b,t} = w
107	      {==}
108	
109	def double_word(+n: Nat,+w: Word(n)) -> {Word.add(n,w,w) == Word.shl(n,w) : Word(n)}:
110	  %Equal.sym(Word(n),Word.shl(n,w),Word.shl.put(n,False{},w),shift_put(n,w)) : {Word.add(n,w,w) == _ : Word(n)}
111	  double_carry(n,w,False{})
112	
113	def encode_double(+a: Nat,+width: Nat) -> {encode(Nat.double(a),width) == Word.shl(width,encode(a,width)) : Word(width)}:
114	  %Addition.double(a) : {encode(_,width) == Word.shl(width,encode(a,width)) : Word(width)}
115	  %encode_add(a,a,width) : {_ == Word.shl(width,encode(a,width)) : Word(width)}
116	  double_word(width,encode(a,width))
117	
118	law native_encoding:
119	  for +a: Nat
120	  {U32.from_nat(a) == U32{encode(a,32n)} : U32}
121	def native_encoding(a):
122	  match a:
123	    case 0n:
124	      {==}
125	    case 1n+ +p:
126	      %native_encoding(p) : {U32.inc(U32.from_nat(p)) == U32.inc(_) : U32}
127	      {==}
128	
129	def native_add(+a: Nat,+b: Nat) -> {U32.add(U32.from_nat(a),U32.from_nat(b)) == U32.from_nat(Nat.add(a,b)) : U32}:
130	  %Equal.sym(U32,U32.from_nat(Nat.add(a,b)),U32{encode(Nat.add(a,b),32n)},native_encoding(Nat.add(a,b))) : {U32.add(U32.from_nat(a),
131	      U32.from_nat(b)) == _ : U32}
132	  %Equal.sym(U32,U32.from_nat(a),U32{encode(a,32n)},native_encoding(a)) : {U32.add(_,U32.from_nat(b)) == U32{encode(Nat.add(a,b),32n)} : U32}
133	  %Equal.sym(U32,U32.from_nat(b),U32{encode(b,32n)},native_encoding(b)) : {U32.add(U32{encode(a,32n)},_) == U32{encode(Nat.add(a,b),32n)} : U32}
134	  %encode_add(a,b,32n) : {U32{Word.add(32n,encode(a,32n),encode(b,32n))} == U32{_} : U32}
135	  {==}