1	# Health rules used by the world simulation. Arithmetic is natural-number
2	# arithmetic; the machine-word boundary is kept separate below.
3	import Base
4	import ./game.bend as G
5	import ./numeric.bend as N
6	
7	def Health.spec_clamp(+hp: Nat, +maximum: Nat) -> Nat:
8	  G.Bq.nmin(hp, maximum)
9	
10	def Health.spec_heal(+hp: Nat, +amount: Nat, +maximum: Nat) -> Nat:
11	  Health.spec_clamp(G.Bq.Nat.add(hp, amount), maximum)
12	
13	def Health.spec_hurt(+hp: Nat, +damage: Nat) -> Nat:
14	  G.Bq.Nat.sub(hp, damage)
15	
16	law Health.le_refl:
17	  for +n: Nat
18	  {G.Bq.Nat.le(n, n) == True{} : Bool}
19	
20	def Health.le_refl(n):
21	  match n:
22	    case Zero{}:
23	      {==}
24	    case Succ{p}:
25	      Health.le_refl(p)
26	
27	law 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	
35	def 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	
50	law 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	
55	def Health.spec_clamp_bounded(hp, maximum):
56	  G.Bq.nmin_le_r(hp, maximum)
57	
58	law 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	
64	def 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	
76	law 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	
81	def 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	
92	law 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	
99	def 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	
102	law 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	
108	def Health.spec_heal_bounded(hp, amount, maximum):
109	  Health.spec_clamp_bounded(G.Bq.Nat.add(hp, amount), maximum)
110	
111	law 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	
116	def Health.le_add(hp, amount):
117	  match hp:
118	    case Zero{}:
119	      {==}
120	    case Succ{p}:
121	      Health.le_add(p, amount)
122	
123	law 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	
131	def 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	
146	law 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	
153	def 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	
156	law 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	
162	def 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.
176	def 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	
185	def Health.clamp(+hp: Nat, +maximum: Nat) -> Nat:
186	  Health.pick(Nat.cmp(hp, maximum), hp, maximum)
187	
188	def Health.heal(+hp: Nat, +amount: Nat, +maximum: Nat) -> Nat:
189	  Health.clamp(Nat.add(hp, amount), maximum)
190	
191	def Health.hurt(hp: Nat, damage: Nat) -> Nat:
192	  Nat.sub(hp, damage)
193	
194	law 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	
200	def Health.pick_succ(order, a, b):
201	  match order:
202	    case LT{}:
203	      {==}
204	    case EQ{}:
205	      {==}
206	    case GT{}:
207	      {==}
208	
209	law Health.clamp_agrees:
210	  for +hp: Nat
211	  for +maximum: Nat
212	  {Health.clamp(hp, maximum) == Health.spec_clamp(hp, maximum) : Nat}
213	
214	def 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	
230	law Health.add_agrees:
231	  for +a: Nat
232	  for +b: Nat
233	  {Nat.add(a, b) == G.Bq.Nat.add(a, b) : Nat}
234	
235	def 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	
243	law Health.hurt_agrees:
244	  for +hp: Nat
245	  for +damage: Nat
246	  {Health.hurt(hp, damage) == Health.spec_hurt(hp, damage) : Nat}
247	
248	def 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	
263	law 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	
269	def 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	
273	law 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	
279	def 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	
283	law 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	
290	def 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	
294	law 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	
301	def 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	
305	law 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	
311	def 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.
317	def Health.clamp_word(hp: U32, maximum: U32) -> U32:
318	  U32.from_nat(Health.clamp(U32.to_nat(hp), U32.to_nat(maximum)))
319	
320	def 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	
323	def Health.hurt_word(hp: U32, damage: U32) -> U32:
324	  U32.from_nat(Health.hurt(U32.to_nat(hp), U32.to_nat(damage)))
325	
326	law Health.clamp_bounded:
327	  for +hp: Nat
328	  for +maximum: Nat
329	  {G.Bq.Nat.le(Health.clamp(hp, maximum), maximum) == True{} : Bool}
330	
331	def 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	
335	law Health.hurt_decreases:
336	  for +hp: Nat
337	  for +damage: Nat
338	  {G.Bq.Nat.le(Health.hurt(hp, damage), hp) == True{} : Bool}
339	
340	def 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	
344	law 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	
349	def 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	
352	law 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	
358	def 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	
361	law 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	
366	def 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	
369	law 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	
374	def 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	
378	law 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	
384	def 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	
388	law 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	
395	def 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	
399	law 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	
406	def 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	
410	law 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	
416	def 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.
421	def Health.cap_nat_word(value: Nat, maximum: U32) -> U32:
422	  U32.from_nat(Health.clamp(value, U32.to_nat(maximum)))
423	
424	law 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	
429	def 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	
432	law 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	
437	def 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	
448	law Health.clamp_decreases:
449	  for +a: Nat
450	  for +b: Nat
451	  {G.Bq.Nat.le(Health.clamp(a, b), a) == True{} : Bool}
452	
453	def 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	
457	law 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	
464	def 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	
468	law 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	
475	def 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	
480	law 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	
487	def 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.
496	def Health.maximum_word(+raw: Nat, bonus: U32, ceiling: U32) -> U32:
497	  Health.cap_nat_word(Nat.add(U32.to_nat(bonus), raw), ceiling)
498	
499	law 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	
507	def 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	
510	law 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	
517	def 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	
522	law 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	
528	def 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	
539	law 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	
545	def 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)