numeric.bend

gralha-bendquest@0.1.0.0 · 433 lines · 32 definitions

1# Binary-word/natural conversion proofs for the game's actual Base codecs.
2import Base
3import gralha-bendquest@0.1.0.0/game.bend as G
4
5# Largest natural representable by a word of n bits.
6def 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.
14def 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
21def 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
32law 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
37def 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
45law 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
50def 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
66law Numeric.zero_value:
67  for +n: Nat
68  {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
69
70def 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
78law 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
84def 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
96law Numeric.true_ne_false:
97  for +e: {True{} == False{} : Bool}
98  Empty
99
100def Numeric.true_ne_false(e):
101  G.Bq.Bool.false_ne_true(Equal.sym(Bool, True{}, False{}, e))
102
103law 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
109def 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
121law Numeric.no_self_successor:
122  for +n: Nat
123  {G.Bq.Nat.le(Succ{n}, n) == False{} : Bool}
124
125def Numeric.no_self_successor(n):
126  match n:
127    case Zero{}:
128      {==}
129    case Succ{p}:
130      Numeric.no_self_successor(p)
131
132law 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
142def 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
151law 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
157def 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
167law 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
173def 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
184law 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
189def 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
200law Numeric.u32_encode_agrees:
201  for +k: Nat
202  {U32.from_nat(k) == U32{Numeric.encode(32n, k)} : U32}
203
204def 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
212law Numeric.u32_roundtrip:
213  for +w: U32
214  {U32.from_nat(U32.to_nat(w)) == w : U32}
215
216def 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.
225type Numeric.Fits<-n: Nat, -k: Nat> is Data:
226  Numeric.Fits{word: Word(n), exact: {Word.to_nat(n, word) == k : Nat}}
227
228law Numeric.value_fits:
229  for +n: Nat
230  for +w: Word(n)
231  Numeric.Fits<n, Word.to_nat(n, w)>
232
233def Numeric.value_fits(n, w):
234  Numeric.Fits{w, {==}}
235
236law 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
242def 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
248law 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
254def Numeric.representable_roundtrip(n, k, fits):
255  Numeric.nat_roundtrip(n, k, Numeric.fits_bound(n, k, fits))
256
257law 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
265def 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
280law 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
288def 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
291law Numeric.u32_value_fits:
292  for +w: U32
293  Numeric.Fits<32n, U32.to_nat(w)>
294
295def Numeric.u32_value_fits(w):
296  match w:
297    case U32{bits}:
298      Numeric.value_fits(32n, bits)
299
300law 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
305def 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
309law Numeric.bool_cmp_refl:
310  for +bit: Bool
311  {Bool.cmp(bit, bit) == EQ{} : Cmp}
312
313def Numeric.bool_cmp_refl(bit):
314  match bit:
315    case False{}:
316      {==}
317    case True{}:
318      {==}
319
320law Numeric.word_cmp_refl:
321  for +n: Nat
322  for +word: Word(n)
323  {Word.cmp(n, word, word) == EQ{} : Cmp}
324
325def 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
335law Numeric.u32_eq_refl:
336  for +word: U32
337  {U32.is_eq(word, word) == True{} : Bool}
338
339def 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
345law Numeric.cmp_eq:
346  for +order: Cmp
347  for +equal: {Cmp.is_eq(order) == True{} : Bool}
348  {order == EQ{} : Cmp}
349
350def 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
359law 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
366def 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
375law 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
381def 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
396law 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
403def 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
421law 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
427def 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          {==}