1	# Player vital state and its authoritative death/respawn transitions.
2	import Base
3	import ./game.bend as G
4	import ./health.bend as H
5	import ./rewards.bend as R
6	
7	type Vitals.State is Data:
8	  Vitals.State{hp: U32, xp: U32, dead: U32, respawn: U32, attack: U32, spin: U32}
9	
10	def Vitals.hp(state: Vitals.State) -> U32:
11	  match state:
12	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
13	      hp
14	
15	def Vitals.dead(state: Vitals.State) -> U32:
16	  match state:
17	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
18	      dead
19	
20	type Vitals.Life<-hp: U32, -dead: U32> is Data:
21	  Vitals.Alive{flag: {dead == 0 : U32}, positive: {G.Bq.Nat.le(1n, U32.to_nat(hp)) == True{} : Bool}}
22	  Vitals.Dead{flag: {dead == 1 : U32}, zero: {hp == 0 : U32}}
23	
24	type Vitals.OK<-state: Vitals.State, -maximum: U32> is Data:
25	  Vitals.OK{bound: {G.Bq.Nat.le(U32.to_nat(Vitals.hp(state)), U32.to_nat(maximum)) == True{} : Bool}, life: Vitals.Life<Vitals.hp(state), Vitals.dead(state)>}
26	
27	def Vitals.fall(state: Vitals.State, timer: U32) -> Vitals.State:
28	  match state:
29	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
30	      Vitals.State{0, xp, 1, timer, attack, spin}
31	
32	def Vitals.revive(state: Vitals.State, maximum: U32) -> Vitals.State:
33	  match state:
34	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
35	      Vitals.State{maximum, xp, 0, 0, 0, 0}
36	
37	law Vitals.fall_ok:
38	  for +state: Vitals.State
39	  for +timer: U32
40	  for +maximum: U32
41	  Vitals.OK<Vitals.fall(state, timer), maximum>
42	
43	def Vitals.fall_ok(state, timer, maximum):
44	  match state:
45	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
46	      Vitals.OK{{==}, Vitals.Dead{{==}, {==}}}
47	
48	law Vitals.revive_ok:
49	  for +state: Vitals.State
50	  for +maximum: U32
51	  for +positive: {G.Bq.Nat.le(1n, U32.to_nat(maximum)) == True{} : Bool}
52	  Vitals.OK<Vitals.revive(state, maximum), maximum>
53	
54	def Vitals.revive_ok(state, maximum, positive):
55	  match state:
56	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
57	      Vitals.OK{H.Health.le_refl(U32.to_nat(maximum)), Vitals.Alive{{==}, positive}}
58	
59	type Vitals.Hit is Data:
60	  Vitals.Hit{state: Vitals.State, fell: Bool}
61	
62	def Vitals.hit_state(hit: Vitals.Hit) -> Vitals.State:
63	  match hit:
64	    case Vitals.Hit{state, fell}:
65	      state
66	
67	def Vitals.finish_hit(remaining: Nat, word: U32, state: Vitals.State, timer: U32) -> Vitals.Hit:
68	  match remaining:
69	    case Zero{}:
70	      Vitals.Hit{Vitals.fall(state, timer), True{}}
71	    case Succ{positive}:
72	      match state:
73	        case Vitals.State{hp, xp, dead, respawn, attack, spin}:
74	          Vitals.Hit{Vitals.State{word, xp, 0, respawn, attack, spin}, False{}}
75	
76	def Vitals.hit_gate(is_dead: Bool, +state: Vitals.State, damage: U32, timer: U32) -> Vitals.Hit:
77	  match is_dead:
78	    case True{}:
79	      Vitals.Hit{state, False{}}
80	    case False{}:
81	      +remaining = H.Health.hurt_word(Vitals.hp(state), damage)
82	      Vitals.finish_hit(U32.to_nat(remaining), remaining, state, timer)
83	
84	def Vitals.hit(+state: Vitals.State, damage: U32, timer: U32) -> Vitals.Hit:
85	  Vitals.hit_gate(U32.is_eq(Vitals.dead(state), 1), state, damage, timer)
86	
87	law Vitals.finish_hit_ok:
88	  for +remaining: Nat
89	  for +word: U32
90	  for +state: Vitals.State
91	  for +timer: U32
92	  for +maximum: U32
93	  for +exact: {U32.to_nat(word) == remaining : Nat}
94	  for +bound: {G.Bq.Nat.le(U32.to_nat(word), U32.to_nat(maximum)) == True{} : Bool}
95	  Vitals.OK<Vitals.hit_state(Vitals.finish_hit(remaining, word, state, timer)), maximum>
96	
97	def Vitals.finish_hit_ok(remaining, word, state, timer, maximum, exact, bound):
98	  match remaining:
99	    case Zero{}:
100	      Vitals.fall_ok(state, timer, maximum)
101	    case Succ{positive}:
102	      match state:
103	        case Vitals.State{hp, xp, dead, respawn, attack, spin}:
104	          Vitals.OK{bound, Vitals.Alive{{==}, (%Equal.sym(Nat, U32.to_nat(word), Succ{positive}, exact) : {G.Bq.Nat.le(1n, _) == True{} : Bool}; {==})}}
105	
106	law Vitals.hit_gate_ok:
107	  for +is_dead: Bool
108	  for +state: Vitals.State
109	  for +damage: U32
110	  for +timer: U32
111	  for +maximum: U32
112	  for +valid: Vitals.OK<state, maximum>
113	  Vitals.OK<Vitals.hit_state(Vitals.hit_gate(is_dead, state, damage, timer)), maximum>
114	
115	def Vitals.hit_gate_ok(is_dead, state, damage, timer, maximum, valid):
116	  match is_dead:
117	    case True{}:
118	      valid
119	    case False{}:
120	      match valid:
121	        case Vitals.OK{bound, life}:
122	          Vitals.finish_hit_ok(U32.to_nat(H.Health.hurt_word(Vitals.hp(state), damage)), H.Health.hurt_word(Vitals.hp(state), damage), state, timer, maximum, {==}, H.Health.hurt_word_preserves_bound(Vitals.hp(state), damage, maximum, bound))
123	
124	law Vitals.hit_ok:
125	  for +state: Vitals.State
126	  for +damage: U32
127	  for +timer: U32
128	  for +maximum: U32
129	  for +valid: Vitals.OK<state, maximum>
130	  Vitals.OK<Vitals.hit_state(Vitals.hit(state, damage, timer)), maximum>
131	
132	def Vitals.hit_ok(state, damage, timer, maximum, valid):
133	  Vitals.hit_gate_ok(U32.is_eq(Vitals.dead(state), 1), state, damage, timer, maximum, valid)
134	
135	def Vitals.dec(word: U32) -> U32:
136	  H.Health.hurt_word(word, 1)
137	
138	def Vitals.wait(state: Vitals.State) -> Vitals.State:
139	  match state:
140	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
141	      Vitals.State{hp, xp, dead, Vitals.dec(respawn), attack, spin}
142	
143	def Vitals.live_tick(state: Vitals.State, amount: U32, maximum: U32) -> Vitals.State:
144	  match state:
145	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
146	      Vitals.State{H.Health.heal_word(hp, amount, maximum), xp, 0, 0, Vitals.dec(attack), Vitals.dec(spin)}
147	
148	type Vitals.Upkeep is Data:
149	  Vitals.Upkeep{state: Vitals.State, revived: Bool, walk: Bool}
150	
151	def Vitals.upkeep_state(upkeep: Vitals.Upkeep) -> Vitals.State:
152	  match upkeep:
153	    case Vitals.Upkeep{state, revived, walk}:
154	      state
155	
156	def Vitals.dead_tick(ready: Bool, state: Vitals.State, maximum: U32) -> Vitals.Upkeep:
157	  match ready:
158	    case True{}:
159	      Vitals.Upkeep{Vitals.revive(state, maximum), True{}, False{}}
160	    case False{}:
161	      Vitals.Upkeep{Vitals.wait(state), False{}, False{}}
162	
163	def Vitals.upkeep_gate(is_dead: Bool, ready: Bool, state: Vitals.State, amount: U32, maximum: U32) -> Vitals.Upkeep:
164	  match is_dead:
165	    case True{}:
166	      Vitals.dead_tick(ready, state, maximum)
167	    case False{}:
168	      Vitals.Upkeep{Vitals.live_tick(state, amount, maximum), False{}, True{}}
169	
170	def Vitals.upkeep(+state: Vitals.State, amount: U32, maximum: U32) -> Vitals.Upkeep:
171	  match state:
172	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
173	      Vitals.upkeep_gate(U32.is_eq(dead, 1), U32.is_le(respawn, 1), Vitals.State{hp, xp, dead, respawn, attack, spin}, amount, maximum)
174	
175	law Vitals.wait_ok:
176	  for +state: Vitals.State
177	  for +maximum: U32
178	  for +valid: Vitals.OK<state, maximum>
179	  Vitals.OK<Vitals.wait(state), maximum>
180	
181	def Vitals.wait_ok(state, maximum, valid):
182	  match state:
183	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
184	      match valid:
185	        case Vitals.OK{bound, life}:
186	          Vitals.OK{bound, life}
187	
188	law Vitals.live_tick_ok:
189	  for +state: Vitals.State
190	  for +amount: U32
191	  for +maximum: U32
192	  for +bound: {G.Bq.Nat.le(U32.to_nat(Vitals.hp(state)), U32.to_nat(maximum)) == True{} : Bool}
193	  for +positive: {G.Bq.Nat.le(1n, U32.to_nat(Vitals.hp(state))) == True{} : Bool}
194	  Vitals.OK<Vitals.live_tick(state, amount, maximum), maximum>
195	
196	def Vitals.live_tick_ok(state, amount, maximum, bound, positive):
197	  match state:
198	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
199	      Vitals.OK{H.Health.heal_word_bounded(hp, amount, maximum), Vitals.Alive{{==}, H.Health.le_trans(1n, U32.to_nat(hp), U32.to_nat(H.Health.heal_word(hp, amount, maximum)), positive, H.Health.heal_word_never_harms(hp, amount, maximum, bound))}}
200	
201	law Vitals.dead_tick_ok:
202	  for +ready: Bool
203	  for +state: Vitals.State
204	  for +maximum: U32
205	  for +valid: Vitals.OK<state, maximum>
206	  for +positive: {G.Bq.Nat.le(1n, U32.to_nat(maximum)) == True{} : Bool}
207	  Vitals.OK<Vitals.upkeep_state(Vitals.dead_tick(ready, state, maximum)), maximum>
208	
209	def Vitals.dead_tick_ok(ready, state, maximum, valid, positive):
210	  match ready:
211	    case True{}:
212	      Vitals.revive_ok(state, maximum, positive)
213	    case False{}:
214	      Vitals.wait_ok(state, maximum, valid)
215	
216	law Vitals.upkeep_ok:
217	  for +state: Vitals.State
218	  for +amount: U32
219	  for +maximum: U32
220	  for +valid: Vitals.OK<state, maximum>
221	  for +positive: {G.Bq.Nat.le(1n, U32.to_nat(maximum)) == True{} : Bool}
222	  Vitals.OK<Vitals.upkeep_state(Vitals.upkeep(state, amount, maximum)), maximum>
223	
224	def Vitals.upkeep_ok(state, amount, maximum, valid, positive):
225	  match state:
226	    case Vitals.State{hp, xp, dead, respawn, attack, spin}:
227	      match valid:
228	        case Vitals.OK{bound, life}:
229	          match life:
230	            case Vitals.Alive{flag, live}:
231	              %Equal.sym(U32, dead, 0, flag) : Vitals.OK<Vitals.upkeep_state(Vitals.upkeep(Vitals.State{hp, xp, _, respawn, attack, spin}, amount, maximum)), maximum>
232	              Vitals.live_tick_ok(Vitals.State{hp, xp, 0, respawn, attack, spin}, amount, maximum, bound, live)
233	            case Vitals.Dead{flag, zero}:
234	              %Equal.sym(U32, dead, 1, flag) : Vitals.OK<Vitals.upkeep_state(Vitals.upkeep(Vitals.State{hp, xp, _, respawn, attack, spin}, amount, maximum)), maximum>
235	              Vitals.dead_tick_ok(U32.is_le(respawn, 1), Vitals.State{hp, xp, 1, respawn, attack, spin}, maximum, Vitals.OK{bound, Vitals.Dead{{==}, zero}}, positive)
236	
237	law Vitals.dead_hit_noop:
238	  for +state: Vitals.State
239	  for +damage: U32
240	  for +timer: U32
241	  for +dead: {Vitals.dead(state) == 1 : U32}
242	  {Vitals.hit(state, damage, timer) == Vitals.Hit{state, False{}} : Vitals.Hit}
243	
244	def Vitals.dead_hit_noop(state, damage, timer, dead):
245	  %Equal.sym(U32, Vitals.dead(state), 1, dead) : {Vitals.hit_gate(U32.is_eq(_, 1), state, damage, timer) == Vitals.Hit{state, False{}} : Vitals.Hit}
246	  {==}
247	
248	law Vitals.finish_hit_exact:
249	  for +remaining: Nat
250	  for +word: U32
251	  for +state: Vitals.State
252	  for +timer: U32
253	  for +exact: {U32.to_nat(word) == remaining : Nat}
254	  {U32.to_nat(Vitals.hp(Vitals.hit_state(Vitals.finish_hit(remaining, word, state, timer)))) == remaining : Nat}
255	
256	def Vitals.finish_hit_exact(remaining, word, state, timer, exact):
257	  match remaining:
258	    case Zero{}:
259	      match state:
260	        case Vitals.State{hp, xp, dead, respawn, attack, spin}:
261	          {==}
262	    case Succ{positive}:
263	      match state:
264	        case Vitals.State{hp, xp, dead, respawn, attack, spin}:
265	          exact
266	
267	law Vitals.live_hit_exact:
268	  for +state: Vitals.State
269	  for +damage: U32
270	  for +timer: U32
271	  for +alive: {Vitals.dead(state) == 0 : U32}
272	  {U32.to_nat(Vitals.hp(Vitals.hit_state(Vitals.hit(state, damage, timer)))) == H.Health.hurt(U32.to_nat(Vitals.hp(state)), U32.to_nat(damage)) : Nat}
273	
274	def Vitals.live_hit_exact(state, damage, timer, alive):
275	  %Equal.sym(U32, Vitals.dead(state), 0, alive) : {U32.to_nat(Vitals.hp(Vitals.hit_state(Vitals.hit_gate(U32.is_eq(_, 1), state, damage, timer)))) == H.Health.hurt(U32.to_nat(Vitals.hp(state)), U32.to_nat(damage)) : Nat}
276	  %H.Health.hurt_word_exact(Vitals.hp(state), damage) : {U32.to_nat(Vitals.hp(Vitals.hit_state(Vitals.finish_hit(U32.to_nat(H.Health.hurt_word(Vitals.hp(state), damage)), H.Health.hurt_word(Vitals.hp(state), damage), state, timer)))) == _ : Nat}
277	  Vitals.finish_hit_exact(U32.to_nat(H.Health.hurt_word(Vitals.hp(state), damage)), H.Health.hurt_word(Vitals.hp(state), damage), state, timer, {==})
278	
279	# The live server uses this entry with the U32 ceiling.
280	def Vitals.upkeep_hero(state: Vitals.State, amount: U32, +hero: G.Bq.Hero, ceiling: U32) -> Vitals.Upkeep:
281	  Vitals.upkeep(state, amount, R.Rewards.maximum(hero, ceiling))
282	
283	law Vitals.upkeep_hero_ok:
284	  for +state: Vitals.State
285	  for +amount: U32
286	  for +hero: G.Bq.Hero
287	  for +ceiling: U32
288	  for +valid: Vitals.OK<state, R.Rewards.maximum(hero, ceiling)>
289	  for +limit_positive: {G.Bq.Nat.le(1n, U32.to_nat(ceiling)) == True{} : Bool}
290	  Vitals.OK<Vitals.upkeep_state(Vitals.upkeep_hero(state, amount, hero, ceiling)), R.Rewards.maximum(hero, ceiling)>
291	
292	def Vitals.upkeep_hero_ok(state, amount, hero, ceiling, valid, limit_positive):
293	  Vitals.upkeep_ok(state, amount, R.Rewards.maximum(hero, ceiling), valid, R.Rewards.maximum_positive(hero, ceiling, limit_positive))
294	
295	def Vitals.spawn(maximum: U32) -> Vitals.State:
296	  Vitals.State{maximum, 0, 0, 0, 0, 0}
297	
298	law Vitals.spawn_ok:
299	  for +maximum: U32
300	  for +positive: {G.Bq.Nat.le(1n, U32.to_nat(maximum)) == True{} : Bool}
301	  Vitals.OK<Vitals.spawn(maximum), maximum>
302	
303	def Vitals.spawn_ok(maximum, positive):
304	  Vitals.OK{H.Health.le_refl(U32.to_nat(maximum)), Vitals.Alive{{==}, positive}}
305	
306	law Vitals.spawn_hero_ok:
307	  for +hero: G.Bq.Hero
308	  for +ceiling: U32
309	  for +limit_positive: {G.Bq.Nat.le(1n, U32.to_nat(ceiling)) == True{} : Bool}
310	  Vitals.OK<Vitals.spawn(R.Rewards.maximum(hero, ceiling)), R.Rewards.maximum(hero, ceiling)>
311	
312	def Vitals.spawn_hero_ok(hero, ceiling, limit_positive):
313	  Vitals.spawn_ok(R.Rewards.maximum(hero, ceiling), R.Rewards.maximum_positive(hero, ceiling, limit_positive))
314	
315	def Vitals.fell(hit: Vitals.Hit) -> Bool:
316	  match hit:
317	    case Vitals.Hit{state, fell}:
318	      fell
319	
320	law Vitals.finish_hit_fell_dead:
321	  for +remaining: Nat
322	  for +word: U32
323	  for +state: Vitals.State
324	  for +timer: U32
325	  for +fell: {Vitals.fell(Vitals.finish_hit(remaining, word, state, timer)) == True{} : Bool}
326	  {Vitals.dead(Vitals.hit_state(Vitals.finish_hit(remaining, word, state, timer))) == 1 : U32}
327	
328	def Vitals.finish_hit_fell_dead(remaining, word, state, timer, fell):
329	  match remaining:
330	    case Zero{}:
331	      match state:
332	        case Vitals.State{hp, xp, dead, respawn, attack, spin}:
333	          {==}
334	    case Succ{positive}:
335	      match state:
336	        case Vitals.State{hp, xp, dead, respawn, attack, spin}:
337	          Empty.absurd({0 == 1 : U32}, G.Bq.Bool.false_ne_true(fell))
338	
339	law Vitals.hit_gate_fell_dead:
340	  for +is_dead: Bool
341	  for +state: Vitals.State
342	  for +damage: U32
343	  for +timer: U32
344	  for +fell: {Vitals.fell(Vitals.hit_gate(is_dead, state, damage, timer)) == True{} : Bool}
345	  {Vitals.dead(Vitals.hit_state(Vitals.hit_gate(is_dead, state, damage, timer))) == 1 : U32}
346	
347	def Vitals.hit_gate_fell_dead(is_dead, state, damage, timer, fell):
348	  match is_dead:
349	    case True{}:
350	      Empty.absurd({Vitals.dead(state) == 1 : U32}, G.Bq.Bool.false_ne_true(fell))
351	    case False{}:
352	      Vitals.finish_hit_fell_dead(U32.to_nat(H.Health.hurt_word(Vitals.hp(state), damage)), H.Health.hurt_word(Vitals.hp(state), damage), state, timer, fell)
353	
354	law Vitals.lethal_hit_reports_death:
355	  for +state: Vitals.State
356	  for +damage: U32
357	  for +timer: U32
358	  for +lethal: {G.Bq.Nat.le(U32.to_nat(Vitals.hp(state)), U32.to_nat(damage)) == True{} : Bool}
359	  {Vitals.fell(Vitals.hit_gate(False{}, state, damage, timer)) == True{} : Bool}
360	
361	def Vitals.lethal_hit_reports_death(state, damage, timer, lethal):
362	  %Equal.sym(Nat, U32.to_nat(H.Health.hurt_word(Vitals.hp(state), damage)), 0n, H.Health.hurt_word_zero(Vitals.hp(state), damage, lethal)) : {Vitals.fell(Vitals.finish_hit(_, H.Health.hurt_word(Vitals.hp(state), damage), state, timer)) == True{} : Bool}
363	  {==}