health.bend

gralha-bendquest@0.1.0.0 · 548 lines · 52 definitions

1# Health rules used by the world simulation. Arithmetic is natural-number
2# arithmetic; the machine-word boundary is kept separate below.
3import Base
4import gralha-bendquest@0.1.0.0/game.bend as G
5import gralha-bendquest@0.1.0.0/numeric.bend as N
6
7def Health.spec_clamp(+hp: Nat, +maximum: Nat) -> Nat:
8  G.Bq.nmin(hp, maximum)
9
10def Health.spec_heal(+hp: Nat, +amount: Nat, +maximum: Nat) -> Nat:
11  Health.spec_clamp(G.Bq.Nat.add(hp, amount), maximum)
12
13def Health.spec_hurt(+hp: Nat, +damage: Nat) -> Nat:
14  G.Bq.Nat.sub(hp, damage)
15
16law Health.le_refl:
17  for +n: Nat
18  {G.Bq.Nat.le(n, n) == True{} : Bool}
19
20def Health.le_refl(n):
21  match n:
22    case Zero{}:
23      {==}
24    case Succ{p}:
25      Health.le_refl(p)
26
27law Health.le_trans:
28  for +a: Nat
29  for +b: Nat
30  for +c: Nat
31  for +ab: {G.Bq.Nat.le(a, b) == True{} : Bool}
32  for +bc: {G.Bq.Nat.le(b, c) == True{} : Bool}
33  {G.Bq.Nat.le(a, c) == True{} : Bool}
34
35def Health.le_trans(a, b, c, ab, bc):
36  match a:
37    case Zero{}:
38      {==}
39    case Succ{ap}:
40      match b:
41        case Zero{}:
42          Empty.absurd({G.Bq.Nat.le(Succ{ap}, c) == True{} : Bool}, G.Bq.Bool.false_ne_true(ab))
43        case Succ{bp}:
44          match c:
45            case Zero{}:
46              Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(bc))
47            case Succ{cp}:
48              Health.le_trans(ap, bp, cp, ab, bc)
49
50law Health.spec_clamp_bounded:
51  for +hp: Nat
52  for +maximum: Nat
53  {G.Bq.Nat.le(Health.spec_clamp(hp, maximum), maximum) == True{} : Bool}
54
55def Health.spec_clamp_bounded(hp, maximum):
56  G.Bq.nmin_le_r(hp, maximum)
57
58law Health.spec_clamp_unchanged:
59  for +hp: Nat
60  for +maximum: Nat
61  for +valid: {G.Bq.Nat.le(hp, maximum) == True{} : Bool}
62  {Health.spec_clamp(hp, maximum) == hp : Nat}
63
64def Health.spec_clamp_unchanged(hp, maximum, valid):
65  match hp:
66    case Zero{}:
67      {==}
68    case Succ{p}:
69      match maximum:
70        case Zero{}:
71          Empty.absurd({0n == Succ{p} : Nat}, G.Bq.Bool.false_ne_true(valid))
72        case Succ{m}:
73          %Health.spec_clamp_unchanged(p, m, valid) : {Succ{Health.spec_clamp(p, m)} == Succ{_} : Nat}
74          {==}
75
76law Health.spec_hurt_decreases:
77  for +hp: Nat
78  for +damage: Nat
79  {G.Bq.Nat.le(Health.spec_hurt(hp, damage), hp) == True{} : Bool}
80
81def Health.spec_hurt_decreases(hp, damage):
82  match hp:
83    case Zero{}:
84      {==}
85    case Succ{p}:
86      match damage:
87        case Zero{}:
88          Health.le_refl(p)
89        case Succ{d}:
90          G.Bq.le_succ_r(Health.spec_hurt(p, d), p, Health.spec_hurt_decreases(p, d))
91
92law Health.spec_hurt_preserves_bound:
93  for +hp: Nat
94  for +damage: Nat
95  for +maximum: Nat
96  for +valid: {G.Bq.Nat.le(hp, maximum) == True{} : Bool}
97  {G.Bq.Nat.le(Health.spec_hurt(hp, damage), maximum) == True{} : Bool}
98
99def Health.spec_hurt_preserves_bound(hp, damage, maximum, valid):
100  Health.le_trans(Health.spec_hurt(hp, damage), hp, maximum, Health.spec_hurt_decreases(hp, damage), valid)
101
102law Health.spec_heal_bounded:
103  for +hp: Nat
104  for +amount: Nat
105  for +maximum: Nat
106  {G.Bq.Nat.le(Health.spec_heal(hp, amount, maximum), maximum) == True{} : Bool}
107
108def Health.spec_heal_bounded(hp, amount, maximum):
109  Health.spec_clamp_bounded(G.Bq.Nat.add(hp, amount), maximum)
110
111law Health.le_add:
112  for +hp: Nat
113  for +amount: Nat
114  {G.Bq.Nat.le(hp, G.Bq.Nat.add(hp, amount)) == True{} : Bool}
115
116def Health.le_add(hp, amount):
117  match hp:
118    case Zero{}:
119      {==}
120    case Succ{p}:
121      Health.le_add(p, amount)
122
123law Health.le_min:
124  for +hp: Nat
125  for +a: Nat
126  for +b: Nat
127  for +ha: {G.Bq.Nat.le(hp, a) == True{} : Bool}
128  for +hb: {G.Bq.Nat.le(hp, b) == True{} : Bool}
129  {G.Bq.Nat.le(hp, G.Bq.nmin(a, b)) == True{} : Bool}
130
131def Health.le_min(hp, a, b, ha, hb):
132  match hp:
133    case Zero{}:
134      {==}
135    case Succ{p}:
136      match a:
137        case Zero{}:
138          Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(ha))
139        case Succ{ap}:
140          match b:
141            case Zero{}:
142              Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(hb))
143            case Succ{bp}:
144              Health.le_min(p, ap, bp, ha, hb)
145
146law Health.spec_heal_never_harms:
147  for +hp: Nat
148  for +amount: Nat
149  for +maximum: Nat
150  for +valid: {G.Bq.Nat.le(hp, maximum) == True{} : Bool}
151  {G.Bq.Nat.le(hp, Health.spec_heal(hp, amount, maximum)) == True{} : Bool}
152
153def Health.spec_heal_never_harms(hp, amount, maximum, valid):
154  Health.le_min(hp, G.Bq.Nat.add(hp, amount), maximum, Health.le_add(hp, amount), valid)
155
156law Health.spec_hurt_survives:
157  for +hp: Nat
158  for +damage: Nat
159  for +below: {G.Bq.Nat.lt(damage, hp) == True{} : Bool}
160  {G.Bq.Nat.le(1n, Health.spec_hurt(hp, damage)) == True{} : Bool}
161
162def Health.spec_hurt_survives(hp, damage, below):
163  match hp:
164    case Zero{}:
165      Empty.absurd({False{} == True{} : Bool}, G.Bq.Bool.false_ne_true(below))
166    case Succ{p}:
167      match damage:
168        case Zero{}:
169          {==}
170        case Succ{d}:
171          Health.spec_hurt_survives(p, d, below)
172
173# These implementations use Base arithmetic, which the native compiler
174# implements with big integers. The refinement proofs below tie the fast
175# implementations to the inductive specification above.
176def Health.pick(+order: Cmp, +a: Nat, +b: Nat) -> Nat:
177  match order:
178    case LT{}:
179      a
180    case EQ{}:
181      a
182    case GT{}:
183      b
184
185def Health.clamp(+hp: Nat, +maximum: Nat) -> Nat:
186  Health.pick(Nat.cmp(hp, maximum), hp, maximum)
187
188def Health.heal(+hp: Nat, +amount: Nat, +maximum: Nat) -> Nat:
189  Health.clamp(Nat.add(hp, amount), maximum)
190
191def Health.hurt(hp: Nat, damage: Nat) -> Nat:
192  Nat.sub(hp, damage)
193
194law Health.pick_succ:
195  for +order: Cmp
196  for +a: Nat
197  for +b: Nat
198  {Health.pick(order, Succ{a}, Succ{b}) == Succ{Health.pick(order, a, b)} : Nat}
199
200def Health.pick_succ(order, a, b):
201  match order:
202    case LT{}:
203      {==}
204    case EQ{}:
205      {==}
206    case GT{}:
207      {==}
208
209law Health.clamp_agrees:
210  for +hp: Nat
211  for +maximum: Nat
212  {Health.clamp(hp, maximum) == Health.spec_clamp(hp, maximum) : Nat}
213
214def Health.clamp_agrees(hp, maximum):
215  match hp:
216    case Zero{}:
217      match maximum:
218        case Zero{}:
219          {==}
220        case Succ{m}:
221          {==}
222    case Succ{p}:
223      match maximum:
224        case Zero{}:
225          {==}
226        case Succ{m}:
227          %Health.clamp_agrees(p, m) : {Health.clamp(Succ{p}, Succ{m}) == Succ{_} : Nat}
228          Health.pick_succ(Nat.cmp(p, m), p, m)
229
230law Health.add_agrees:
231  for +a: Nat
232  for +b: Nat
233  {Nat.add(a, b) == G.Bq.Nat.add(a, b) : Nat}
234
235def Health.add_agrees(a, b):
236  match a:
237    case Zero{}:
238      {==}
239    case Succ{p}:
240      %Health.add_agrees(p, b) : {Succ{Nat.add(p, b)} == Succ{_} : Nat}
241      {==}
242
243law Health.hurt_agrees:
244  for +hp: Nat
245  for +damage: Nat
246  {Health.hurt(hp, damage) == Health.spec_hurt(hp, damage) : Nat}
247
248def Health.hurt_agrees(hp, damage):
249  match hp:
250    case Zero{}:
251      match damage:
252        case Zero{}:
253          {==}
254        case Succ{d}:
255          {==}
256    case Succ{p}:
257      match damage:
258        case Zero{}:
259          {==}
260        case Succ{d}:
261          Health.hurt_agrees(p, d)
262
263law Health.heal_agrees:
264  for +hp: Nat
265  for +amount: Nat
266  for +maximum: Nat
267  {Health.heal(hp, amount, maximum) == Health.spec_heal(hp, amount, maximum) : Nat}
268
269def Health.heal_agrees(hp, amount, maximum):
270  %Health.add_agrees(hp, amount) : {Health.heal(hp, amount, maximum) == Health.spec_clamp(_, maximum) : Nat}
271  Health.clamp_agrees(Nat.add(hp, amount), maximum)
272
273law Health.heal_bounded:
274  for +hp: Nat
275  for +amount: Nat
276  for +maximum: Nat
277  {G.Bq.Nat.le(Health.heal(hp, amount, maximum), maximum) == True{} : Bool}
278
279def Health.heal_bounded(hp, amount, maximum):
280  %Equal.sym(Nat, Health.heal(hp, amount, maximum), Health.spec_heal(hp, amount, maximum), Health.heal_agrees(hp, amount, maximum)) : {G.Bq.Nat.le(_, maximum) == True{} : Bool}
281  Health.spec_heal_bounded(hp, amount, maximum)
282
283law Health.heal_never_harms:
284  for +hp: Nat
285  for +amount: Nat
286  for +maximum: Nat
287  for +valid: {G.Bq.Nat.le(hp, maximum) == True{} : Bool}
288  {G.Bq.Nat.le(hp, Health.heal(hp, amount, maximum)) == True{} : Bool}
289
290def Health.heal_never_harms(hp, amount, maximum, valid):
291  %Equal.sym(Nat, Health.heal(hp, amount, maximum), Health.spec_heal(hp, amount, maximum), Health.heal_agrees(hp, amount, maximum)) : {G.Bq.Nat.le(hp, _) == True{} : Bool}
292  Health.spec_heal_never_harms(hp, amount, maximum, valid)
293
294law Health.hurt_preserves_bound:
295  for +hp: Nat
296  for +damage: Nat
297  for +maximum: Nat
298  for +valid: {G.Bq.Nat.le(hp, maximum) == True{} : Bool}
299  {G.Bq.Nat.le(Health.hurt(hp, damage), maximum) == True{} : Bool}
300
301def Health.hurt_preserves_bound(hp, damage, maximum, valid):
302  %Equal.sym(Nat, Health.hurt(hp, damage), Health.spec_hurt(hp, damage), Health.hurt_agrees(hp, damage)) : {G.Bq.Nat.le(_, maximum) == True{} : Bool}
303  Health.spec_hurt_preserves_bound(hp, damage, maximum, valid)
304
305law Health.hurt_survives:
306  for +hp: Nat
307  for +damage: Nat
308  for +below: {G.Bq.Nat.lt(damage, hp) == True{} : Bool}
309  {G.Bq.Nat.le(1n, Health.hurt(hp, damage)) == True{} : Bool}
310
311def Health.hurt_survives(hp, damage, below):
312  %Equal.sym(Nat, Health.hurt(hp, damage), Health.spec_hurt(hp, damage), Health.hurt_agrees(hp, damage)) : {G.Bq.Nat.le(1n, _) == True{} : Bool}
313  Health.spec_hurt_survives(hp, damage, below)
314
315# Existing U32 records enter the rules here. The refinement and preservation
316# theorems below prove these exact word wrappers cannot wrap their results.
317def Health.clamp_word(hp: U32, maximum: U32) -> U32:
318  U32.from_nat(Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)))
319
320def Health.heal_word(hp: U32, amount: U32, maximum: U32) -> U32:
321  U32.from_nat(Health.heal(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum)))
322
323def Health.hurt_word(hp: U32, damage: U32) -> U32:
324  U32.from_nat(Health.hurt(U32.to_nat(hp), U32.to_nat(damage)))
325
326law Health.clamp_bounded:
327  for +hp: Nat
328  for +maximum: Nat
329  {G.Bq.Nat.le(Health.clamp(hp, maximum), maximum) == True{} : Bool}
330
331def Health.clamp_bounded(hp, maximum):
332  %Equal.sym(Nat, Health.clamp(hp, maximum), Health.spec_clamp(hp, maximum), Health.clamp_agrees(hp, maximum)) : {G.Bq.Nat.le(_, maximum) == True{} : Bool}
333  Health.spec_clamp_bounded(hp, maximum)
334
335law Health.hurt_decreases:
336  for +hp: Nat
337  for +damage: Nat
338  {G.Bq.Nat.le(Health.hurt(hp, damage), hp) == True{} : Bool}
339
340def Health.hurt_decreases(hp, damage):
341  %Equal.sym(Nat, Health.hurt(hp, damage), Health.spec_hurt(hp, damage), Health.hurt_agrees(hp, damage)) : {G.Bq.Nat.le(_, hp) == True{} : Bool}
342  Health.spec_hurt_decreases(hp, damage)
343
344law Health.clamp_word_exact:
345  for +hp: U32
346  for +maximum: U32
347  {U32.to_nat(Health.clamp_word(hp, maximum)) == Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)) : Nat}
348
349def Health.clamp_word_exact(hp, maximum):
350  N.Numeric.u32_nat_roundtrip(Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)), N.Numeric.fits_downward(32n, Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)), U32.to_nat(maximum), N.Numeric.u32_value_fits(maximum), Health.clamp_bounded(U32.to_nat(hp), U32.to_nat(maximum))))
351
352law Health.heal_word_exact:
353  for +hp: U32
354  for +amount: U32
355  for +maximum: U32
356  {U32.to_nat(Health.heal_word(hp, amount, maximum)) == Health.heal(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum)) : Nat}
357
358def Health.heal_word_exact(hp, amount, maximum):
359  N.Numeric.u32_nat_roundtrip(Health.heal(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum)), N.Numeric.fits_downward(32n, Health.heal(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum)), U32.to_nat(maximum), N.Numeric.u32_value_fits(maximum), Health.heal_bounded(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum))))
360
361law Health.hurt_word_exact:
362  for +hp: U32
363  for +damage: U32
364  {U32.to_nat(Health.hurt_word(hp, damage)) == Health.hurt(U32.to_nat(hp), U32.to_nat(damage)) : Nat}
365
366def Health.hurt_word_exact(hp, damage):
367  N.Numeric.u32_nat_roundtrip(Health.hurt(U32.to_nat(hp), U32.to_nat(damage)), N.Numeric.fits_downward(32n, Health.hurt(U32.to_nat(hp), U32.to_nat(damage)), U32.to_nat(hp), N.Numeric.u32_value_fits(hp), Health.hurt_decreases(U32.to_nat(hp), U32.to_nat(damage))))
368
369law Health.clamp_word_bounded:
370  for +hp: U32
371  for +maximum: U32
372  {G.Bq.Nat.le(U32.to_nat(Health.clamp_word(hp, maximum)), U32.to_nat(maximum)) == True{} : Bool}
373
374def Health.clamp_word_bounded(hp, maximum):
375  %Equal.sym(Nat, U32.to_nat(Health.clamp_word(hp, maximum)), Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)), Health.clamp_word_exact(hp, maximum)) : {G.Bq.Nat.le(_, U32.to_nat(maximum)) == True{} : Bool}
376  Health.clamp_bounded(U32.to_nat(hp), U32.to_nat(maximum))
377
378law Health.heal_word_bounded:
379  for +hp: U32
380  for +amount: U32
381  for +maximum: U32
382  {G.Bq.Nat.le(U32.to_nat(Health.heal_word(hp, amount, maximum)), U32.to_nat(maximum)) == True{} : Bool}
383
384def Health.heal_word_bounded(hp, amount, maximum):
385  %Equal.sym(Nat, U32.to_nat(Health.heal_word(hp, amount, maximum)), Health.heal(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum)), Health.heal_word_exact(hp, amount, maximum)) : {G.Bq.Nat.le(_, U32.to_nat(maximum)) == True{} : Bool}
386  Health.heal_bounded(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum))
387
388law Health.heal_word_never_harms:
389  for +hp: U32
390  for +amount: U32
391  for +maximum: U32
392  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(maximum)) == True{} : Bool}
393  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Health.heal_word(hp, amount, maximum))) == True{} : Bool}
394
395def Health.heal_word_never_harms(hp, amount, maximum, valid):
396  %Equal.sym(Nat, U32.to_nat(Health.heal_word(hp, amount, maximum)), Health.heal(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum)), Health.heal_word_exact(hp, amount, maximum)) : {G.Bq.Nat.le(U32.to_nat(hp), _) == True{} : Bool}
397  Health.heal_never_harms(U32.to_nat(hp), U32.to_nat(amount), U32.to_nat(maximum), valid)
398
399law Health.hurt_word_preserves_bound:
400  for +hp: U32
401  for +damage: U32
402  for +maximum: U32
403  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(maximum)) == True{} : Bool}
404  {G.Bq.Nat.le(U32.to_nat(Health.hurt_word(hp, damage)), U32.to_nat(maximum)) == True{} : Bool}
405
406def Health.hurt_word_preserves_bound(hp, damage, maximum, valid):
407  %Equal.sym(Nat, U32.to_nat(Health.hurt_word(hp, damage)), Health.hurt(U32.to_nat(hp), U32.to_nat(damage)), Health.hurt_word_exact(hp, damage)) : {G.Bq.Nat.le(_, U32.to_nat(maximum)) == True{} : Bool}
408  Health.hurt_preserves_bound(U32.to_nat(hp), U32.to_nat(damage), U32.to_nat(maximum), valid)
409
410law Health.hurt_word_survives:
411  for +hp: U32
412  for +damage: U32
413  for +below: {G.Bq.Nat.lt(U32.to_nat(damage), U32.to_nat(hp)) == True{} : Bool}
414  {G.Bq.Nat.le(1n, U32.to_nat(Health.hurt_word(hp, damage))) == True{} : Bool}
415
416def Health.hurt_word_survives(hp, damage, below):
417  %Equal.sym(Nat, U32.to_nat(Health.hurt_word(hp, damage)), Health.hurt(U32.to_nat(hp), U32.to_nat(damage)), Health.hurt_word_exact(hp, damage)) : {G.Bq.Nat.le(1n, _) == True{} : Bool}
418  Health.hurt_survives(U32.to_nat(hp), U32.to_nat(damage), below)
419
420# Natural stat-derived maxima must be clamped before conversion, too.
421def Health.cap_nat_word(value: Nat, maximum: U32) -> U32:
422  U32.from_nat(Health.clamp(value, U32.to_nat(maximum)))
423
424law Health.cap_nat_word_exact:
425  for +value: Nat
426  for +maximum: U32
427  {U32.to_nat(Health.cap_nat_word(value, maximum)) == Health.clamp(value, U32.to_nat(maximum)) : Nat}
428
429def Health.cap_nat_word_exact(value, maximum):
430  N.Numeric.u32_nat_roundtrip(Health.clamp(value, U32.to_nat(maximum)), N.Numeric.fits_downward(32n, Health.clamp(value, U32.to_nat(maximum)), U32.to_nat(maximum), N.Numeric.u32_value_fits(maximum), Health.clamp_bounded(value, U32.to_nat(maximum))))
431
432law Health.spec_clamp_decreases:
433  for +a: Nat
434  for +b: Nat
435  {G.Bq.Nat.le(Health.spec_clamp(a, b), a) == True{} : Bool}
436
437def Health.spec_clamp_decreases(a, b):
438  match a:
439    case Zero{}:
440      {==}
441    case Succ{p}:
442      match b:
443        case Zero{}:
444          {==}
445        case Succ{q}:
446          Health.spec_clamp_decreases(p, q)
447
448law Health.clamp_decreases:
449  for +a: Nat
450  for +b: Nat
451  {G.Bq.Nat.le(Health.clamp(a, b), a) == True{} : Bool}
452
453def Health.clamp_decreases(a, b):
454  %Equal.sym(Nat, Health.clamp(a, b), Health.spec_clamp(a, b), Health.clamp_agrees(a, b)) : {G.Bq.Nat.le(_, a) == True{} : Bool}
455  Health.spec_clamp_decreases(a, b)
456
457law Health.clamp_monotone:
458  for +a: Nat
459  for +b: Nat
460  for +maximum: Nat
461  for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
462  {G.Bq.Nat.le(Health.clamp(a, maximum), Health.clamp(b, maximum)) == True{} : Bool}
463
464def Health.clamp_monotone(a, b, maximum, grow):
465  %Equal.sym(Nat, Health.clamp(b, maximum), Health.spec_clamp(b, maximum), Health.clamp_agrees(b, maximum)) : {G.Bq.Nat.le(Health.clamp(a, maximum), _) == True{} : Bool}
466  Health.le_min(Health.clamp(a, maximum), b, maximum, Health.le_trans(Health.clamp(a, maximum), a, b, Health.clamp_decreases(a, maximum), grow), Health.clamp_bounded(a, maximum))
467
468law Health.cap_nat_word_monotone:
469  for +a: Nat
470  for +b: Nat
471  for +maximum: U32
472  for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
473  {G.Bq.Nat.le(U32.to_nat(Health.cap_nat_word(a, maximum)), U32.to_nat(Health.cap_nat_word(b, maximum))) == True{} : Bool}
474
475def Health.cap_nat_word_monotone(a, b, maximum, grow):
476  %Equal.sym(Nat, U32.to_nat(Health.cap_nat_word(a, maximum)), Health.clamp(a, U32.to_nat(maximum)), Health.cap_nat_word_exact(a, maximum)) : {G.Bq.Nat.le(_, U32.to_nat(Health.cap_nat_word(b, maximum))) == True{} : Bool}
477  %Equal.sym(Nat, U32.to_nat(Health.cap_nat_word(b, maximum)), Health.clamp(b, U32.to_nat(maximum)), Health.cap_nat_word_exact(b, maximum)) : {G.Bq.Nat.le(Health.clamp(a, U32.to_nat(maximum)), _) == True{} : Bool}
478  Health.clamp_monotone(a, b, U32.to_nat(maximum), grow)
479
480law Health.add_mono_left:
481  for +amount: Nat
482  for +a: Nat
483  for +b: Nat
484  for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
485  {G.Bq.Nat.le(Nat.add(amount, a), Nat.add(amount, b)) == True{} : Bool}
486
487def Health.add_mono_left(amount, a, b, grow):
488  match amount:
489    case Zero{}:
490      grow
491    case Succ{p}:
492      Health.add_mono_left(p, a, b, grow)
493
494# Add the charm bonus before conversion. The server supplies U32 maximum
495# as the ceiling; keeping it explicit makes the theorem apply to any ceiling.
496def Health.maximum_word(+raw: Nat, bonus: U32, ceiling: U32) -> U32:
497  Health.cap_nat_word(Nat.add(U32.to_nat(bonus), raw), ceiling)
498
499law Health.maximum_word_monotone:
500  for +a: Nat
501  for +b: Nat
502  for +bonus: U32
503  for +ceiling: U32
504  for +grow: {G.Bq.Nat.le(a, b) == True{} : Bool}
505  {G.Bq.Nat.le(U32.to_nat(Health.maximum_word(a, bonus, ceiling)), U32.to_nat(Health.maximum_word(b, bonus, ceiling))) == True{} : Bool}
506
507def Health.maximum_word_monotone(a, b, bonus, ceiling, grow):
508  Health.cap_nat_word_monotone(Nat.add(U32.to_nat(bonus), a), Nat.add(U32.to_nat(bonus), b), ceiling, Health.add_mono_left(U32.to_nat(bonus), a, b, grow))
509
510law Health.cap_nat_word_positive:
511  for +value: Nat
512  for +maximum: U32
513  for +positive: {G.Bq.Nat.le(1n, value) == True{} : Bool}
514  for +limit_positive: {G.Bq.Nat.le(1n, U32.to_nat(maximum)) == True{} : Bool}
515  {G.Bq.Nat.le(1n, U32.to_nat(Health.cap_nat_word(value, maximum))) == True{} : Bool}
516
517def Health.cap_nat_word_positive(value, maximum, positive, limit_positive):
518  %Equal.sym(Nat, U32.to_nat(Health.cap_nat_word(value, maximum)), Health.clamp(value, U32.to_nat(maximum)), Health.cap_nat_word_exact(value, maximum)) : {G.Bq.Nat.le(1n, _) == True{} : Bool}
519  %Equal.sym(Nat, Health.clamp(value, U32.to_nat(maximum)), Health.spec_clamp(value, U32.to_nat(maximum)), Health.clamp_agrees(value, U32.to_nat(maximum))) : {G.Bq.Nat.le(1n, _) == True{} : Bool}
520  Health.le_min(1n, value, U32.to_nat(maximum), positive, limit_positive)
521
522law Health.spec_hurt_zero:
523  for +hp: Nat
524  for +damage: Nat
525  for +lethal: {G.Bq.Nat.le(hp, damage) == True{} : Bool}
526  {Health.spec_hurt(hp, damage) == 0n : Nat}
527
528def Health.spec_hurt_zero(hp, damage, lethal):
529  match hp:
530    case Zero{}:
531      {==}
532    case Succ{rest}:
533      match damage:
534        case Zero{}:
535          Empty.absurd({Succ{rest} == 0n : Nat}, G.Bq.Bool.false_ne_true(lethal))
536        case Succ{less}:
537          Health.spec_hurt_zero(rest, less, lethal)
538
539law Health.hurt_word_zero:
540  for +hp: U32
541  for +damage: U32
542  for +lethal: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(damage)) == True{} : Bool}
543  {U32.to_nat(Health.hurt_word(hp, damage)) == 0n : Nat}
544
545def Health.hurt_word_zero(hp, damage, lethal):
546  %Equal.sym(Nat, U32.to_nat(Health.hurt_word(hp, damage)), Health.hurt(U32.to_nat(hp), U32.to_nat(damage)), Health.hurt_word_exact(hp, damage)) : {_ == 0n : Nat}
547  %Equal.sym(Nat, Health.hurt(U32.to_nat(hp), U32.to_nat(damage)), Health.spec_hurt(U32.to_nat(hp), U32.to_nat(damage)), Health.hurt_agrees(U32.to_nat(hp), U32.to_nat(damage))) : {_ == 0n : Nat}
548  Health.spec_hurt_zero(U32.to_nat(hp), U32.to_nat(damage), lethal)