vitals.bend
gralha-bendquest@0.1.0.0 · 363 lines · 41 definitions
1
2import Base
3import gralha-bendquest@0.1.0.0/game.bend as G
4import gralha-bendquest@0.1.0.0/health.bend as H
5import gralha-bendquest@0.1.0.0/rewards.bend as R
6
7type Vitals.State is Data:
8 Vitals.State{hp: U32, xp: U32, dead: U32, respawn: U32, attack: U32, spin: U32}
9
10def Vitals.hp(state: Vitals.State) -> U32:
11 match state:
12 case Vitals.State{hp, xp, dead, respawn, attack, spin}:
13 hp
14
15def Vitals.dead(state: Vitals.State) -> U32:
16 match state:
17 case Vitals.State{hp, xp, dead, respawn, attack, spin}:
18 dead
19
20type 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
24type 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
27def 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
32def 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
37law 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
43def 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
48law 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
54def 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
59type Vitals.Hit is Data:
60 Vitals.Hit{state: Vitals.State, fell: Bool}
61
62def Vitals.hit_state(hit: Vitals.Hit) -> Vitals.State:
63 match hit:
64 case Vitals.Hit{state, fell}:
65 state
66
67def 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
76def 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
84def 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
87law 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
97def 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
106law 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
115def 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
124law 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
132def 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
135def Vitals.dec(word: U32) -> U32:
136 H.Health.hurt_word(word, 1)
137
138def 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
143def 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
148type Vitals.Upkeep is Data:
149 Vitals.Upkeep{state: Vitals.State, revived: Bool, walk: Bool}
150
151def Vitals.upkeep_state(upkeep: Vitals.Upkeep) -> Vitals.State:
152 match upkeep:
153 case Vitals.Upkeep{state, revived, walk}:
154 state
155
156def 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
163def 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
170def 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
175law 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
181def 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
188law 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
196def 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
201law 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
209def 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
216law 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
224def 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
237law 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
244def 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
248law 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
256def 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
267law 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
274def 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
280def 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
283law 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
292def 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
295def Vitals.spawn(maximum: U32) -> Vitals.State:
296 Vitals.State{maximum, 0, 0, 0, 0, 0}
297
298law 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
303def Vitals.spawn_ok(maximum, positive):
304 Vitals.OK{H.Health.le_refl(U32.to_nat(maximum)), Vitals.Alive{{==}, positive}}
305
306law 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
312def 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
315def Vitals.fell(hit: Vitals.Hit) -> Bool:
316 match hit:
317 case Vitals.Hit{state, fell}:
318 fell
319
320law 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
328def 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
339law 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
347def 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
354law 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
361def 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 {==}