1	import Base
2	import ../../lib/logic.bend as L
3	
4	# Bit-level facts about zero tests on words, for any width, then at U32.
5	# A word is zero when it compares EQ with Word.zero; Word.cmp compares the
6	# tail first and settles ties with the head (Word.cmp.fin).
7	
8	law and_true:
9	  for +b: Bool
10	  {Bool.and(b, True{}) == b : Bool}
11	
12	def and_true(b):
13	  match b:
14	    case False{}:
15	      {==}
16	    case True{}:
17	      {==}
18	
19	law and_false:
20	  for +b: Bool
21	  {Bool.and(b, False{}) == False{} : Bool}
22	
23	def and_false(b):
24	  match b:
25	    case False{}:
26	      {==}
27	    case True{}:
28	      {==}
29	
30	law and_assoc:
31	  for +a: Bool
32	  for +b: Bool
33	  for +c: Bool
34	  {Bool.and(Bool.and(a, b), c) == Bool.and(a, Bool.and(b, c)) : Bool}
35	
36	def and_assoc(a, b, c):
37	  match a:
38	    case False{}:
39	      {==}
40	    case True{}:
41	      {==}
42	
43	# A comparison is EQ exactly when the tails compare EQ and the heads agree.
44	law fin_eq:
45	  for +ab: Bool
46	  for +bb: Bool
47	  for +t: Cmp
48	  {Cmp.is_eq(Word.cmp.fin(ab, bb, t)) == Bool.and(Cmp.is_eq(t), Cmp.is_eq(Bool.cmp(ab, bb))) : Bool}
49	
50	def fin_eq(ab, bb, t):
51	  match t:
52	    case LT{}:
53	      {==}
54	    case EQ{}:
55	      {==}
56	    case GT{}:
57	      {==}
58	
59	law bits_or:
60	  for +a: Bool
61	  for +b: Bool
62	  for +x: Bool
63	  for +y: Bool
64	  {Bool.and(Bool.and(a, b), Cmp.is_eq(Bool.cmp(Bool.or(x, y), False{}))) ==
65	    Bool.and(Bool.and(a, Cmp.is_eq(Bool.cmp(x, False{}))), Bool.and(b, Cmp.is_eq(Bool.cmp(y, False{})))) : Bool}
66	
67	def bits_or(a, b, x, y):
68	  match a b x y:
69	    case False{} _ _ _:
70	      {==}
71	    case True{} False{} False{} _:
72	      {==}
73	    case True{} False{} True{} _:
74	      {==}
75	    case True{} True{} False{} False{}:
76	      {==}
77	    case True{} True{} False{} True{}:
78	      {==}
79	    case True{} True{} True{} False{}:
80	      {==}
81	    case True{} True{} True{} True{}:
82	      {==}
83	
84	law bits_xor:
85	  for +k: Bool
86	  for +x: Bool
87	  for +y: Bool
88	  {Bool.and(k, Cmp.is_eq(Bool.cmp(Bool.xor(x, y), False{}))) == Bool.and(k, Cmp.is_eq(Bool.cmp(x, y))) : Bool}
89	
90	def bits_xor(k, x, y):
91	  match x y:
92	    case False{} False{}:
93	      {==}
94	    case False{} True{}:
95	      {==}
96	    case True{} False{}:
97	      {==}
98	    case True{} True{}:
99	      {==}
100	
101	law bit_eq:
102	  for +x: Bool
103	  for +y: Bool
104	  for +h: {Cmp.is_eq(Bool.cmp(x, y)) == True{} : Bool}
105	  {x == y : Bool}
106	
107	def bit_eq(x, y, h):
108	  match x y:
109	    case False{} False{}:
110	      {==}
111	    case False{} True{}:
112	      Empty.absurd({False{} == True{} : Bool}, L.false_true(h))
113	    case True{} False{}:
114	      Empty.absurd({True{} == False{} : Bool}, L.false_true(h))
115	    case True{} True{}:
116	      {==}
117	
118	law bit_refl:
119	  for +k: Bool
120	  for +x: Bool
121	  {Bool.and(k, Cmp.is_eq(Bool.cmp(x, x))) == k : Bool}
122	
123	def bit_refl(k, x):
124	  match x:
125	    case False{}:
126	      and_true(k)
127	    case True{}:
128	      and_true(k)
129	
130	# zero(x | y) == zero(x) && zero(y)
131	law or_zero:
132	  for +n: Nat
133	  for +x: Word(n)
134	  for +y: Word(n)
135	  {Cmp.is_eq(Word.cmp(n, Word.or(n, x, y), Word.zero(n))) ==
136	    Bool.and(Cmp.is_eq(Word.cmp(n, x, Word.zero(n))), Cmp.is_eq(Word.cmp(n, y, Word.zero(n)))) : Bool}
137	
138	def or_zero(n, x, y):
139	  match n:
140	    case 0n:
141	      {==}
142	    case 1n+p:
143	      match x y:
144	        case WCon{a, xt} WCon{b, yt}:
145	          +co = Word.cmp(p, Word.or(p, xt, yt), Word.zero(p))
146	          +cx = Word.cmp(p, xt, Word.zero(p))
147	          +cy = Word.cmp(p, yt, Word.zero(p))
148	          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(Bool.or(a, b), False{}, co)),
149	            Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))),
150	            fin_eq(Bool.or(a, b), False{}, co)) :
151	            {_ == Bool.and(Cmp.is_eq(Word.cmp.fin(a, False{}, cx)), Cmp.is_eq(Word.cmp.fin(b, False{}, cy))) : Bool}
152	          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, False{}, cx)),
153	            Bool.and(Cmp.is_eq(cx), Cmp.is_eq(Bool.cmp(a, False{}))),
154	            fin_eq(a, False{}, cx)) :
155	            {Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))) == Bool.and(_, Cmp.is_eq(Word.cmp.fin(b, False{}, cy))) : Bool}
156	          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(b, False{}, cy)),
157	            Bool.and(Cmp.is_eq(cy), Cmp.is_eq(Bool.cmp(b, False{}))),
158	            fin_eq(b, False{}, cy)) :
159	            {Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))) == Bool.and(Bool.and(Cmp.is_eq(cx), Cmp.is_eq(Bool.cmp(a, False{}))), _) : Bool}
160	          %Equal.sym(Bool, Cmp.is_eq(co), Bool.and(Cmp.is_eq(cx), Cmp.is_eq(cy)), or_zero(p, xt, yt)) :
161	            {Bool.and(_, Cmp.is_eq(Bool.cmp(Bool.or(a, b), False{}))) == Bool.and(Bool.and(Cmp.is_eq(cx), Cmp.is_eq(Bool.cmp(a, False{}))), Bool.and(Cmp.is_eq(cy), Cmp.is_eq(Bool.cmp(b, False{})))) : Bool}
162	          bits_or(Cmp.is_eq(cx), Cmp.is_eq(cy), a, b)
163	
164	# zero(x ^ y) == (x == y)
165	law xor_zero:
166	  for +n: Nat
167	  for +x: Word(n)
168	  for +y: Word(n)
169	  {Cmp.is_eq(Word.cmp(n, Word.xor(n, x, y), Word.zero(n))) == Cmp.is_eq(Word.cmp(n, x, y)) : Bool}
170	
171	def xor_zero(n, x, y):
172	  match n:
173	    case 0n:
174	      {==}
175	    case 1n+p:
176	      match x y:
177	        case WCon{a, xt} WCon{b, yt}:
178	          +co = Word.cmp(p, Word.xor(p, xt, yt), Word.zero(p))
179	          +c = Word.cmp(p, xt, yt)
180	          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(Bool.xor(a, b), False{}, co)),
181	            Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.xor(a, b), False{}))),
182	            fin_eq(Bool.xor(a, b), False{}, co)) :
183	            {_ == Cmp.is_eq(Word.cmp.fin(a, b, c)) : Bool}
184	          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, b, c)),
185	            Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))), fin_eq(a, b, c)) :
186	            {Bool.and(Cmp.is_eq(co), Cmp.is_eq(Bool.cmp(Bool.xor(a, b), False{}))) == _ : Bool}
187	          %Equal.sym(Bool, Cmp.is_eq(co), Cmp.is_eq(c), xor_zero(p, xt, yt)) :
188	            {Bool.and(_, Cmp.is_eq(Bool.cmp(Bool.xor(a, b), False{}))) == Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))) : Bool}
189	          bits_xor(Cmp.is_eq(c), a, b)
190	
191	law cmp_sound:
192	  for +n: Nat
193	  for +x: Word(n)
194	  for +y: Word(n)
195	  for +h: {Cmp.is_eq(Word.cmp(n, x, y)) == True{} : Bool}
196	  {x == y : Word(n)}
197	
198	def cmp_sound(n, x, y, h):
199	  match n:
200	    case 0n:
201	      match x y:
202	        case WNil{} WNil{}:
203	          {==}
204	    case 1n+p:
205	      match x y:
206	        case WCon{a, xt} WCon{b, yt}:
207	          +c = Word.cmp(p, xt, yt)
208	          +h2 = Equal.trans(Bool, Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))),
209	            Cmp.is_eq(Word.cmp.fin(a, b, c)), True{},
210	            Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, b, c)),
211	              Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b))), fin_eq(a, b, c)), h)
212	          +et = cmp_sound(p, xt, yt, L.and_left(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b)), h2))
213	          +eb = bit_eq(a, b, L.and_right(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, b)), h2))
214	          %et : {WCon{a, xt} == WCon{b, _} : Word(1n+p)}
215	          %eb : {WCon{a, xt} == WCon{_, xt} : Word(1n+p)}
216	          {==}
217	
218	law cmp_refl:
219	  for +n: Nat
220	  for +x: Word(n)
221	  {Cmp.is_eq(Word.cmp(n, x, x)) == True{} : Bool}
222	
223	def cmp_refl(n, x):
224	  match n:
225	    case 0n:
226	      {==}
227	    case 1n+p:
228	      match x:
229	        case WCon{a, xt}:
230	          +c = Word.cmp(p, xt, xt)
231	          %Equal.sym(Bool, Cmp.is_eq(Word.cmp.fin(a, a, c)),
232	            Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, a))), fin_eq(a, a, c)) :
233	            {_ == True{} : Bool}
234	          %Equal.sym(Bool, Bool.and(Cmp.is_eq(c), Cmp.is_eq(Bool.cmp(a, a))), Cmp.is_eq(c), bit_refl(Cmp.is_eq(c), a)) : {_ == True{} : Bool}
235	          cmp_refl(p, xt)
236	
237	# ---- at U32
238	
239	law u32_or_zero:
240	  for +x: U32
241	  for +y: U32
242	  {U32.is_eq(U32.or(x, y), 0) == Bool.and(U32.is_eq(x, 0), U32.is_eq(y, 0)) : Bool}
243	
244	def u32_or_zero(x, y):
245	  match x y:
246	    case U32{a} U32{b}:
247	      or_zero(32n, a, b)
248	
249	law u32_xor_zero:
250	  for +x: U32
251	  for +y: U32
252	  {U32.is_eq(U32.xor(x, y), 0) == U32.is_eq(x, y) : Bool}
253	
254	def u32_xor_zero(x, y):
255	  match x y:
256	    case U32{a} U32{b}:
257	      xor_zero(32n, a, b)
258	
259	law u32_sound:
260	  for +x: U32
261	  for +y: U32
262	  for +h: {U32.is_eq(x, y) == True{} : Bool}
263	  {x == y : U32}
264	
265	def u32_sound(x, y, h):
266	  match x y:
267	    case U32{a} U32{b}:
268	      %cmp_sound(32n, a, b, h) : {U32{a} == U32{_} : U32}
269	      {==}
270	
271	law u32_refl:
272	  for +x: U32
273	  {U32.is_eq(x, x) == True{} : Bool}
274	
275	def u32_refl(x):
276	  match x:
277	    case U32{a}:
278	      cmp_refl(32n, a)