1	# Binary-word/natural conversion proofs for the game's actual Base codecs.
2	import Base
3	import ./game.bend as G
4	
5	# Largest natural representable by a word of n bits.
6	def Numeric.limit(n: Nat) -> Nat:
7	  match n:
8	    case Zero{}:
9	      0n
10	    case Succ{p}:
11	      Succ{Nat.double(Numeric.limit(p))}
12	
13	# Generalization of Base.U32.from_nat to arbitrary word widths.
14	def Numeric.encode(+n: Nat, k: Nat) -> Word(n):
15	  match k:
16	    case Zero{}:
17	      Word.zero(n)
18	    case Succ{p}:
19	      Word.inc(n, Numeric.encode(n, p))
20	
21	def Numeric.full(n: Nat, w: Word(n)) -> Bool:
22	  match n:
23	    case Zero{}:
24	      True{}
25	    case Succ{p}:
26	      match w:
27	        case WCon{False{}, tail}:
28	          False{}
29	        case WCon{True{}, tail}:
30	          Numeric.full(p, tail)
31	
32	law Numeric.encode_double:
33	  for +n: Nat
34	  for +k: Nat
35	  {Numeric.encode(Succ{n}, Nat.double(k)) == WCon{False{}, Numeric.encode(n, k)} : Word(Succ{n})}
36	
37	def Numeric.encode_double(n, k):
38	  match k:
39	    case Zero{}:
40	      {==}
41	    case Succ{p}:
42	      %Numeric.encode_double(n, p) : {Word.inc(Succ{n}, Word.inc(Succ{n}, Numeric.encode(Succ{n}, Nat.double(p)))) == Word.inc(Succ{n}, Word.inc(Succ{n}, _)) : Word(Succ{n})}
43	      {==}
44	
45	law Numeric.word_roundtrip:
46	  for +n: Nat
47	  for +w: Word(n)
48	  {Numeric.encode(n, Word.to_nat(n, w)) == w : Word(n)}
49	
50	def Numeric.word_roundtrip(n, w):
51	  match n:
52	    case Zero{}:
53	      match w:
54	        case WNil{}:
55	          {==}
56	    case Succ{p}:
57	      match w:
58	        case WCon{False{}, tail}:
59	          %Numeric.word_roundtrip(p, tail) : {Numeric.encode(Succ{p}, Nat.double(Word.to_nat(p, tail))) == WCon{False{}, _} : Word(Succ{p})}
60	          Numeric.encode_double(p, Word.to_nat(p, tail))
61	        case WCon{True{}, tail}:
62	          %Numeric.word_roundtrip(p, tail) : {Word.inc(Succ{p}, Numeric.encode(Succ{p}, Nat.double(Word.to_nat(p, tail)))) == WCon{True{}, _} : Word(Succ{p})}
63	          %Numeric.encode_double(p, Word.to_nat(p, tail)) : {Word.inc(Succ{p}, Numeric.encode(Succ{p}, Nat.double(Word.to_nat(p, tail)))) == Word.inc(Succ{p}, _) : Word(Succ{p})}
64	          {==}
65	
66	law Numeric.zero_value:
67	  for +n: Nat
68	  {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
69	
70	def Numeric.zero_value(n):
71	  match n:
72	    case Zero{}:
73	      {==}
74	    case Succ{p}:
75	      %Numeric.zero_value(p) : {Nat.double(Word.to_nat(p, Word.zero(p))) == Nat.double(_) : Nat}
76	      {==}
77	
78	law Numeric.full_value:
79	  for +n: Nat
80	  for +w: Word(n)
81	  for +full: {Numeric.full(n, w) == True{} : Bool}
82	  {Word.to_nat(n, w) == Numeric.limit(n) : Nat}
83	
84	def Numeric.full_value(n, w, full):
85	  match n:
86	    case Zero{}:
87	      {==}
88	    case Succ{p}:
89	      match w:
90	        case WCon{False{}, tail}:
91	          Empty.absurd({Nat.double(Word.to_nat(p, tail)) == Numeric.limit(Succ{p}) : Nat}, G.Bq.Bool.false_ne_true(full))
92	        case WCon{True{}, tail}:
93	          %Numeric.full_value(p, tail, full) : {Succ{Nat.double(Word.to_nat(p, tail))} == Succ{Nat.double(_)} : Nat}
94	          {==}
95	
96	law Numeric.true_ne_false:
97	  for +e: {True{} == False{} : Bool}
98	  Empty
99	
100	def Numeric.true_ne_false(e):
101	  G.Bq.Bool.false_ne_true(Equal.sym(Bool, True{}, False{}, e))
102	
103	law Numeric.inc_exact:
104	  for +n: Nat
105	  for +w: Word(n)
106	  for +room: {Numeric.full(n, w) == False{} : Bool}
107	  {Word.to_nat(n, Word.inc(n, w)) == Succ{Word.to_nat(n, w)} : Nat}
108	
109	def Numeric.inc_exact(n, w, room):
110	  match n:
111	    case Zero{}:
112	      Empty.absurd({0n == 1n : Nat}, Numeric.true_ne_false(room))
113	    case Succ{p}:
114	      match w:
115	        case WCon{False{}, tail}:
116	          {==}
117	        case WCon{True{}, tail}:
118	          %Numeric.inc_exact(p, tail, room) : {Nat.double(Word.to_nat(p, Word.inc(p, tail))) == Nat.double(_) : Nat}
119	          {==}
120	
121	law Numeric.no_self_successor:
122	  for +n: Nat
123	  {G.Bq.Nat.le(Succ{n}, n) == False{} : Bool}
124	
125	def Numeric.no_self_successor(n):
126	  match n:
127	    case Zero{}:
128	      {==}
129	    case Succ{p}:
130	      Numeric.no_self_successor(p)
131	
132	law Numeric.below_full.go:
133	  for +n: Nat
134	  for +w: Word(n)
135	  for +k: Nat
136	  for +value: {Word.to_nat(n, w) == k : Nat}
137	  for +below: {G.Bq.Nat.le(Succ{k}, Numeric.limit(n)) == True{} : Bool}
138	  for +flag: Bool
139	  for +test: {Numeric.full(n, w) == flag : Bool}
140	  {flag == False{} : Bool}
141	
142	def Numeric.below_full.go(n, w, k, value, below, flag, test):
143	  match flag:
144	    case False{}:
145	      {==}
146	    case True{}:
147	      +at_limit = Equal.trans(Nat, k, Word.to_nat(n, w), Numeric.limit(n), Equal.sym(Nat, Word.to_nat(n, w), k, value), Numeric.full_value(n, w, test))
148	      +self_below = Equal.trans(Bool, G.Bq.Nat.le(Succ{k}, Numeric.limit(n)), G.Bq.Nat.le(Succ{Numeric.limit(n)}, Numeric.limit(n)), False{}, Equal.cong(Nat, Bool, x => G.Bq.Nat.le(Succ{x}, Numeric.limit(n)), k, Numeric.limit(n), at_limit), Numeric.no_self_successor(Numeric.limit(n)))
149	      Empty.absurd({True{} == False{} : Bool}, G.Bq.Bool.false_ne_true(Equal.trans(Bool, False{}, G.Bq.Nat.le(Succ{k}, Numeric.limit(n)), True{}, Equal.sym(Bool, G.Bq.Nat.le(Succ{k}, Numeric.limit(n)), False{}, self_below), below)))
150	
151	law Numeric.nat_roundtrip:
152	  for +n: Nat
153	  for +k: Nat
154	  for +fits: {G.Bq.Nat.le(k, Numeric.limit(n)) == True{} : Bool}
155	  {Word.to_nat(n, Numeric.encode(n, k)) == k : Nat}
156	
157	def Numeric.nat_roundtrip(n, k, fits):
158	  match k:
159	    case Zero{}:
160	      Numeric.zero_value(n)
161	    case Succ{p}:
162	      +prev = Numeric.nat_roundtrip(n, p, G.Bq.le_step_down(p, Numeric.limit(n), fits))
163	      +room = Numeric.below_full.go(n, Numeric.encode(n, p), p, prev, fits, Numeric.full(n, Numeric.encode(n, p)), {==})
164	      %prev : {Word.to_nat(n, Word.inc(n, Numeric.encode(n, p))) == Succ{_} : Nat}
165	      Numeric.inc_exact(n, Numeric.encode(n, p), room)
166	
167	law Numeric.double_le:
168	  for +a: Nat
169	  for +b: Nat
170	  for +ab: {G.Bq.Nat.le(a, b) == True{} : Bool}
171	  {G.Bq.Nat.le(Nat.double(a), Nat.double(b)) == True{} : Bool}
172	
173	def Numeric.double_le(a, b, ab):
174	  match a:
175	    case Zero{}:
176	      {==}
177	    case Succ{p}:
178	      match b:
179	        case Zero{}:
180	          Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(ab))
181	        case Succ{q}:
182	          Numeric.double_le(p, q, ab)
183	
184	law Numeric.word_bounded:
185	  for +n: Nat
186	  for +w: Word(n)
187	  {G.Bq.Nat.le(Word.to_nat(n, w), Numeric.limit(n)) == True{} : Bool}
188	
189	def Numeric.word_bounded(n, w):
190	  match n:
191	    case Zero{}:
192	      {==}
193	    case Succ{p}:
194	      match w:
195	        case WCon{False{}, tail}:
196	          G.Bq.le_succ_r(Nat.double(Word.to_nat(p, tail)), Nat.double(Numeric.limit(p)), Numeric.double_le(Word.to_nat(p, tail), Numeric.limit(p), Numeric.word_bounded(p, tail)))
197	        case WCon{True{}, tail}:
198	          Numeric.double_le(Word.to_nat(p, tail), Numeric.limit(p), Numeric.word_bounded(p, tail))
199	
200	law Numeric.u32_encode_agrees:
201	  for +k: Nat
202	  {U32.from_nat(k) == U32{Numeric.encode(32n, k)} : U32}
203	
204	def Numeric.u32_encode_agrees(k):
205	  match k:
206	    case Zero{}:
207	      {==}
208	    case Succ{p}:
209	      %Numeric.u32_encode_agrees(p) : {U32.inc(U32.from_nat(p)) == U32.inc(_) : U32}
210	      {==}
211	
212	law Numeric.u32_roundtrip:
213	  for +w: U32
214	  {U32.from_nat(U32.to_nat(w)) == w : U32}
215	
216	def Numeric.u32_roundtrip(w):
217	  match w:
218	    case U32{bits}:
219	      %Numeric.word_roundtrip(32n, bits) : {U32.from_nat(Word.to_nat(32n, bits)) == U32{_} : U32}
220	      Numeric.u32_encode_agrees(Word.to_nat(32n, bits))
221	
222	# A representability witness avoids evaluating a closed 2^32-sized unary
223	# bound during type conversion. It carries an actual word with the exact
224	# natural value; it is not an assumed upper bound.
225	type Numeric.Fits<-n: Nat, -k: Nat> is Data:
226	  Numeric.Fits{word: Word(n), exact: {Word.to_nat(n, word) == k : Nat}}
227	
228	law Numeric.value_fits:
229	  for +n: Nat
230	  for +w: Word(n)
231	  Numeric.Fits<n, Word.to_nat(n, w)>
232	
233	def Numeric.value_fits(n, w):
234	  Numeric.Fits{w, {==}}
235	
236	law Numeric.fits_bound:
237	  for +n: Nat
238	  for +k: Nat
239	  for +fits: Numeric.Fits<n, k>
240	  {G.Bq.Nat.le(k, Numeric.limit(n)) == True{} : Bool}
241	
242	def Numeric.fits_bound(n, k, fits):
243	  match fits:
244	    case Numeric.Fits{word, exact}:
245	      %exact : {G.Bq.Nat.le(_, Numeric.limit(n)) == True{} : Bool}
246	      Numeric.word_bounded(n, word)
247	
248	law Numeric.representable_roundtrip:
249	  for +n: Nat
250	  for +k: Nat
251	  for +fits: Numeric.Fits<n, k>
252	  {Word.to_nat(n, Numeric.encode(n, k)) == k : Nat}
253	
254	def Numeric.representable_roundtrip(n, k, fits):
255	  Numeric.nat_roundtrip(n, k, Numeric.fits_bound(n, k, fits))
256	
257	law Numeric.le_trans:
258	  for +a: Nat
259	  for +b: Nat
260	  for +c: Nat
261	  for +ab: {G.Bq.Nat.le(a, b) == True{} : Bool}
262	  for +bc: {G.Bq.Nat.le(b, c) == True{} : Bool}
263	  {G.Bq.Nat.le(a, c) == True{} : Bool}
264	
265	def Numeric.le_trans(a, b, c, ab, bc):
266	  match a:
267	    case Zero{}:
268	      {==}
269	    case Succ{ap}:
270	      match b:
271	        case Zero{}:
272	          Empty.absurd({G.Bq.Nat.le(Succ{ap}, c) == True{} : Bool}, G.Bq.Bool.false_ne_true(ab))
273	        case Succ{bp}:
274	          match c:
275	            case Zero{}:
276	              Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(bc))
277	            case Succ{cp}:
278	              Numeric.le_trans(ap, bp, cp, ab, bc)
279	
280	law Numeric.fits_downward:
281	  for +n: Nat
282	  for +lower: Nat
283	  for +upper: Nat
284	  for +fits: Numeric.Fits<n, upper>
285	  for +below: {G.Bq.Nat.le(lower, upper) == True{} : Bool}
286	  Numeric.Fits<n, lower>
287	
288	def Numeric.fits_downward(n, lower, upper, fits, below):
289	  Numeric.Fits{Numeric.encode(n, lower), Numeric.nat_roundtrip(n, lower, Numeric.le_trans(lower, upper, Numeric.limit(n), below, Numeric.fits_bound(n, upper, fits)))}
290	
291	law Numeric.u32_value_fits:
292	  for +w: U32
293	  Numeric.Fits<32n, U32.to_nat(w)>
294	
295	def Numeric.u32_value_fits(w):
296	  match w:
297	    case U32{bits}:
298	      Numeric.value_fits(32n, bits)
299	
300	law Numeric.u32_nat_roundtrip:
301	  for +k: Nat
302	  for +fits: Numeric.Fits<32n, k>
303	  {U32.to_nat(U32.from_nat(k)) == k : Nat}
304	
305	def Numeric.u32_nat_roundtrip(k, fits):
306	  %Equal.sym(U32, U32.from_nat(k), U32{Numeric.encode(32n, k)}, Numeric.u32_encode_agrees(k)) : {U32.to_nat(_) == k : Nat}
307	  Numeric.representable_roundtrip(32n, k, fits)
308	
309	law Numeric.bool_cmp_refl:
310	  for +bit: Bool
311	  {Bool.cmp(bit, bit) == EQ{} : Cmp}
312	
313	def Numeric.bool_cmp_refl(bit):
314	  match bit:
315	    case False{}:
316	      {==}
317	    case True{}:
318	      {==}
319	
320	law Numeric.word_cmp_refl:
321	  for +n: Nat
322	  for +word: Word(n)
323	  {Word.cmp(n, word, word) == EQ{} : Cmp}
324	
325	def Numeric.word_cmp_refl(n, word):
326	  match n:
327	    case Zero{}:
328	      {==}
329	    case Succ{p}:
330	      match word:
331	        case WCon{bit, rest}:
332	          %Equal.sym(Cmp, Word.cmp(p, rest, rest), EQ{}, Numeric.word_cmp_refl(p, rest)) : {Word.cmp.fin(bit, bit, _) == EQ{} : Cmp}
333	          Numeric.bool_cmp_refl(bit)
334	
335	law Numeric.u32_eq_refl:
336	  for +word: U32
337	  {U32.is_eq(word, word) == True{} : Bool}
338	
339	def Numeric.u32_eq_refl(word):
340	  match word:
341	    case U32{bits}:
342	      %Equal.sym(Cmp, Word.cmp(32n, bits, bits), EQ{}, Numeric.word_cmp_refl(32n, bits)) : {Cmp.is_eq(_) == True{} : Bool}
343	      {==}
344	
345	law Numeric.cmp_eq:
346	  for +order: Cmp
347	  for +equal: {Cmp.is_eq(order) == True{} : Bool}
348	  {order == EQ{} : Cmp}
349	
350	def Numeric.cmp_eq(order, equal):
351	  match order:
352	    case LT{}:
353	      Empty.absurd({LT{} == EQ{} : Cmp}, G.Bq.Bool.false_ne_true(equal))
354	    case EQ{}:
355	      {==}
356	    case GT{}:
357	      Empty.absurd({GT{} == EQ{} : Cmp}, G.Bq.Bool.false_ne_true(equal))
358	
359	law Numeric.cmp_tail_eq:
360	  for +a: Bool
361	  for +b: Bool
362	  for +tail: Cmp
363	  for +equal: {Word.cmp.fin(a, b, tail) == EQ{} : Cmp}
364	  {tail == EQ{} : Cmp}
365	
366	def Numeric.cmp_tail_eq(a, b, tail, equal):
367	  match tail:
368	    case LT{}:
369	      Empty.absurd({LT{} == EQ{} : Cmp}, G.Bq.Bool.false_ne_true(Equal.cong(Cmp, Bool, (c => Cmp.is_eq(c)), LT{}, EQ{}, equal)))
370	    case EQ{}:
371	      {==}
372	    case GT{}:
373	      Empty.absurd({GT{} == EQ{} : Cmp}, G.Bq.Bool.false_ne_true(Equal.cong(Cmp, Bool, (c => Cmp.is_eq(c)), GT{}, EQ{}, equal)))
374	
375	law Numeric.bool_cmp_eq:
376	  for +a: Bool
377	  for +b: Bool
378	  for +equal: {Bool.cmp(a, b) == EQ{} : Cmp}
379	  {a == b : Bool}
380	
381	def Numeric.bool_cmp_eq(a, b, equal):
382	  match a:
383	    case False{}:
384	      match b:
385	        case False{}:
386	          {==}
387	        case True{}:
388	          Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(Equal.cong(Cmp, Bool, (c => Cmp.is_eq(c)), LT{}, EQ{}, equal)))
389	    case True{}:
390	      match b:
391	        case False{}:
392	          Empty.absurd({True{} == False{} : Bool}, G.Bq.Bool.false_ne_true(Equal.cong(Cmp, Bool, (c => Cmp.is_eq(c)), GT{}, EQ{}, equal)))
393	        case True{}:
394	          {==}
395	
396	law Numeric.word_cmp_eq:
397	  for +n: Nat
398	  for +a: Word(n)
399	  for +b: Word(n)
400	  for +equal: {Word.cmp(n, a, b) == EQ{} : Cmp}
401	  {a == b : Word(n)}
402	
403	def Numeric.word_cmp_eq(n, a, b, equal):
404	  match n:
405	    case Zero{}:
406	      match a:
407	        case WNil{}:
408	          match b:
409	            case WNil{}:
410	              {==}
411	    case Succ{p}:
412	      match a:
413	        case WCon{ah, at}:
414	          match b:
415	            case WCon{bh, bt}:
416	              +tail = Numeric.cmp_tail_eq(ah, bh, Word.cmp(p, at, bt), equal)
417	              %Numeric.bool_cmp_eq(ah, bh, (%tail : {Word.cmp.fin(ah, bh, _) == EQ{} : Cmp}; equal)) : {WCon{ah, at} == WCon{_, bt} : Word(Succ{p})}
418	              %Numeric.word_cmp_eq(p, at, bt, tail) : {WCon{ah, at} == WCon{ah, _} : Word(Succ{p})}
419	              {==}
420	
421	law Numeric.u32_eq_sound:
422	  for +a: U32
423	  for +b: U32
424	  for +equal: {U32.is_eq(a, b) == True{} : Bool}
425	  {a == b : U32}
426	
427	def Numeric.u32_eq_sound(a, b, equal):
428	  match a:
429	    case U32{ab}:
430	      match b:
431	        case U32{bb}:
432	          %Numeric.word_cmp_eq(32n, ab, bb, Numeric.cmp_eq(Word.cmp(32n, ab, bb), equal)) : {U32{ab} == U32{_} : U32}
433	          {==}