1	# The authoritative XP loop and its hero-state preservation proofs.
2	import Base
3	import ./game.bend as G
4	import ./health.bend as H
5	import ./growth.bend as Growth
6	
7	type Rewards.Result is Data:
8	  Rewards.Result{hero: G.Bq.Hero, xp: U32, levels: U32}
9	
10	def Rewards.hero(result: Rewards.Result) -> G.Bq.Hero:
11	  match result:
12	    case Rewards.Result{hero, xp, levels}:
13	      hero
14	
15	def Rewards.level(hero: G.Bq.Hero) -> Nat:
16	  match hero:
17	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
18	      level
19	
20	def Rewards.charm_amount(has_bonus: Bool) -> U32:
21	  match has_bonus:
22	    case True{}:
23	      30
24	    case False{}:
25	      0
26	
27	def Rewards.charm_bonus(charm: G.Bq.Maybe(Nat)) -> U32:
28	  match charm:
29	    case Fail{unit}:
30	      0
31	    case Done{kind}:
32	      Rewards.charm_amount(U32.is_eq(U32.from_nat(kind), 17))
33	
34	def Rewards.maximum(+hero: G.Bq.Hero, ceiling: U32) -> U32:
35	  match hero:
36	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
37	      Growth.Growth.maximum(level, vitality, Rewards.charm_bonus(charm), ceiling)
38	
39	def Rewards.cost(+level: U32) -> U32:
40	  U32.mul(U32.mul(25, level), level)
41	
42	def Rewards.eligible(+hero: G.Bq.Hero, +xp: U32) -> Bool:
43	  +level = U32.from_nat(Rewards.level(hero))
44	  Bool.and(U32.is_lt(level, 20), U32.is_ge(xp, Rewards.cost(level)))
45	
46	def Rewards.loop(fuel: Nat, eligible: Bool, +hero: G.Bq.Hero, +xp: U32, +levels: U32) -> Rewards.Result:
47	  match fuel:
48	    case Zero{}:
49	      Rewards.Result{hero, xp, levels}
50	    case Succ{remaining}:
51	      match eligible:
52	        case False{}:
53	          Rewards.Result{hero, xp, levels}
54	        case True{}:
55	          +next_hero = G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero)
56	          +next_xp = U32.sub(xp, Rewards.cost(U32.from_nat(Rewards.level(hero))))
57	          Rewards.loop(remaining, Rewards.eligible(next_hero, next_xp), next_hero, next_xp, U32.add(levels, 1))
58	
59	def Rewards.go(fuel: Nat, +hero: G.Bq.Hero, +xp: U32, levels: U32) -> Rewards.Result:
60	  Rewards.loop(fuel, Rewards.eligible(hero, xp), hero, xp, levels)
61	
62	def Rewards.gain(+hero: G.Bq.Hero, xp: U32, gained: U32) -> Rewards.Result:
63	  Rewards.go(20n, hero, U32.add(xp, gained), 0)
64	
65	law Rewards.level_up_health:
66	  for +hero: G.Bq.Hero
67	  for +hp: U32
68	  for +ceiling: U32
69	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
70	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero), ceiling))) == True{} : Bool}
71	
72	def Rewards.level_up_health(hero, hp, ceiling, valid):
73	  match hero:
74	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
75	      Growth.Growth.level_up_preserves_health(hp, level, vitality, Rewards.charm_bonus(charm), ceiling, valid)
76	
77	law Rewards.loop_health:
78	  for +fuel: Nat
79	  for +eligible: Bool
80	  for +hero: G.Bq.Hero
81	  for +xp: U32
82	  for +levels: U32
83	  for +hp: U32
84	  for +ceiling: U32
85	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
86	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.hero(Rewards.loop(fuel, eligible, hero, xp, levels)), ceiling))) == True{} : Bool}
87	
88	def Rewards.loop_health(fuel, eligible, hero, xp, levels, hp, ceiling, valid):
89	  match fuel:
90	    case Zero{}:
91	      valid
92	    case Succ{remaining}:
93	      match eligible:
94	        case False{}:
95	          valid
96	        case True{}:
97	          +next_hero = G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero)
98	          +next_xp = U32.sub(xp, Rewards.cost(U32.from_nat(Rewards.level(hero))))
99	          Rewards.loop_health(remaining, Rewards.eligible(next_hero, next_xp), next_hero, next_xp, U32.add(levels, 1), hp, ceiling, Rewards.level_up_health(hero, hp, ceiling, valid))
100	
101	law Rewards.gain_health:
102	  for +hero: G.Bq.Hero
103	  for +xp: U32
104	  for +gained: U32
105	  for +hp: U32
106	  for +ceiling: U32
107	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
108	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.hero(Rewards.gain(hero, xp, gained)), ceiling))) == True{} : Bool}
109	
110	def Rewards.gain_health(hero, xp, gained, hp, ceiling, valid):
111	  Rewards.loop_health(20n, Rewards.eligible(hero, U32.add(xp, gained)), hero, U32.add(xp, gained), 0, hp, ceiling, valid)
112	
113	law Rewards.loop_equipped:
114	  for +fuel: Nat
115	  for +eligible: Bool
116	  for +hero: G.Bq.Hero
117	  for +xp: U32
118	  for +levels: U32
119	  for +valid: G.Bq.WellEquipped(hero)
120	  G.Bq.WellEquipped(Rewards.hero(Rewards.loop(fuel, eligible, hero, xp, levels)))
121	
122	def Rewards.loop_equipped(fuel, eligible, hero, xp, levels, valid):
123	  match fuel:
124	    case Zero{}:
125	      valid
126	    case Succ{remaining}:
127	      match eligible:
128	        case False{}:
129	          valid
130	        case True{}:
131	          +next_hero = G.Bq.hero_step(G.Bq.HOp.LevelUp{}, hero)
132	          +next_xp = U32.sub(xp, Rewards.cost(U32.from_nat(Rewards.level(hero))))
133	          Rewards.loop_equipped(remaining, Rewards.eligible(next_hero, next_xp), next_hero, next_xp, U32.add(levels, 1), G.Bq.ops_respect_requirements(G.Bq.HOp.LevelUp{}, hero, valid))
134	
135	law Rewards.gain_equipped:
136	  for +hero: G.Bq.Hero
137	  for +xp: U32
138	  for +gained: U32
139	  for +valid: G.Bq.WellEquipped(hero)
140	  G.Bq.WellEquipped(Rewards.hero(Rewards.gain(hero, xp, gained)))
141	
142	def Rewards.gain_equipped(hero, xp, gained, valid):
143	  Rewards.loop_equipped(20n, Rewards.eligible(hero, U32.add(xp, gained)), hero, U32.add(xp, gained), 0, valid)
144	
145	# Server-authored grants change inventory or gold, never equipped slots or stats.
146	def Rewards.add_item(hero: G.Bq.Hero, kind: U32) -> G.Bq.Hero:
147	  match hero:
148	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
149	      G.Bq.Hero.Hero{G.Bq.Bag.add(G.Bq.one(U32.to_nat(kind)), inv), wea, arm, hel, charm, gold, level, strength, agility, vitality, points}
150	
151	def Rewards.add_gold(hero: G.Bq.Hero, amount: U32) -> G.Bq.Hero:
152	  match hero:
153	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
154	      G.Bq.Hero.Hero{inv, wea, arm, hel, charm, G.Bq.Nat.add(U32.to_nat(amount), gold), level, strength, agility, vitality, points}
155	
156	def Rewards.sidequest_nat(quest: Nat, hero: G.Bq.Hero) -> G.Bq.Hero:
157	  match quest:
158	    case Zero{}:
159	      Rewards.add_item(Rewards.add_item(Rewards.add_item(hero, 0), 0), 0)
160	    case Succ{rest}:
161	      match rest:
162	        case Zero{}:
163	          Rewards.add_item(hero, 13)
164	        case Succ{later}:
165	          Rewards.add_item(hero, 16)
166	
167	def Rewards.sidequest(hero: G.Bq.Hero, quest: U32) -> G.Bq.Hero:
168	  Rewards.sidequest_nat(U32.to_nat(quest), hero)
169	
170	law Rewards.add_item_health:
171	  for +hero: G.Bq.Hero
172	  for +kind: U32
173	  for +hp: U32
174	  for +ceiling: U32
175	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
176	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.add_item(hero, kind), ceiling))) == True{} : Bool}
177	
178	def Rewards.add_item_health(hero, kind, hp, ceiling, valid):
179	  match hero:
180	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
181	      valid
182	
183	law Rewards.add_item_equipped:
184	  for +hero: G.Bq.Hero
185	  for +kind: U32
186	  for +valid: G.Bq.WellEquipped(hero)
187	  G.Bq.WellEquipped(Rewards.add_item(hero, kind))
188	
189	def Rewards.add_item_equipped(hero, kind, valid):
190	  match hero:
191	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
192	      valid
193	
194	law Rewards.add_gold_health:
195	  for +hero: G.Bq.Hero
196	  for +amount: U32
197	  for +hp: U32
198	  for +ceiling: U32
199	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
200	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.add_gold(hero, amount), ceiling))) == True{} : Bool}
201	
202	def Rewards.add_gold_health(hero, amount, hp, ceiling, valid):
203	  match hero:
204	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
205	      valid
206	
207	law Rewards.add_gold_equipped:
208	  for +hero: G.Bq.Hero
209	  for +amount: U32
210	  for +valid: G.Bq.WellEquipped(hero)
211	  G.Bq.WellEquipped(Rewards.add_gold(hero, amount))
212	
213	def Rewards.add_gold_equipped(hero, amount, valid):
214	  match hero:
215	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
216	      valid
217	
218	law Rewards.sidequest_nat_health:
219	  for +quest: Nat
220	  for +hero: G.Bq.Hero
221	  for +hp: U32
222	  for +ceiling: U32
223	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
224	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.sidequest_nat(quest, hero), ceiling))) == True{} : Bool}
225	
226	def Rewards.sidequest_nat_health(quest, hero, hp, ceiling, valid):
227	  match quest:
228	    case Zero{}:
229	      Rewards.add_item_health(Rewards.add_item(Rewards.add_item(hero, 0), 0), 0, hp, ceiling, Rewards.add_item_health(Rewards.add_item(hero, 0), 0, hp, ceiling, Rewards.add_item_health(hero, 0, hp, ceiling, valid)))
230	    case Succ{rest}:
231	      match rest:
232	        case Zero{}:
233	          Rewards.add_item_health(hero, 13, hp, ceiling, valid)
234	        case Succ{later}:
235	          Rewards.add_item_health(hero, 16, hp, ceiling, valid)
236	
237	law Rewards.sidequest_nat_equipped:
238	  for +quest: Nat
239	  for +hero: G.Bq.Hero
240	  for +valid: G.Bq.WellEquipped(hero)
241	  G.Bq.WellEquipped(Rewards.sidequest_nat(quest, hero))
242	
243	def Rewards.sidequest_nat_equipped(quest, hero, valid):
244	  match quest:
245	    case Zero{}:
246	      Rewards.add_item_equipped(Rewards.add_item(Rewards.add_item(hero, 0), 0), 0, Rewards.add_item_equipped(Rewards.add_item(hero, 0), 0, Rewards.add_item_equipped(hero, 0, valid)))
247	    case Succ{rest}:
248	      match rest:
249	        case Zero{}:
250	          Rewards.add_item_equipped(hero, 13, valid)
251	        case Succ{later}:
252	          Rewards.add_item_equipped(hero, 16, valid)
253	
254	law Rewards.sidequest_health:
255	  for +hero: G.Bq.Hero
256	  for +quest: U32
257	  for +hp: U32
258	  for +ceiling: U32
259	  for +valid: {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
260	  {G.Bq.Nat.le(U32.to_nat(hp), U32.to_nat(Rewards.maximum(Rewards.sidequest(hero, quest), ceiling))) == True{} : Bool}
261	
262	def Rewards.sidequest_health(hero, quest, hp, ceiling, valid):
263	  Rewards.sidequest_nat_health(U32.to_nat(quest), hero, hp, ceiling, valid)
264	
265	law Rewards.sidequest_equipped:
266	  for +hero: G.Bq.Hero
267	  for +quest: U32
268	  for +valid: G.Bq.WellEquipped(hero)
269	  G.Bq.WellEquipped(Rewards.sidequest(hero, quest))
270	
271	def Rewards.sidequest_equipped(hero, quest, valid):
272	  Rewards.sidequest_nat_equipped(U32.to_nat(quest), hero, valid)
273	
274	law Rewards.maximum_positive:
275	  for +hero: G.Bq.Hero
276	  for +ceiling: U32
277	  for +limit_positive: {G.Bq.Nat.le(1n, U32.to_nat(ceiling)) == True{} : Bool}
278	  {G.Bq.Nat.le(1n, U32.to_nat(Rewards.maximum(hero, ceiling))) == True{} : Bool}
279	
280	def Rewards.maximum_positive(hero, ceiling, limit_positive):
281	  match hero:
282	    case G.Bq.Hero.Hero{inv, wea, arm, hel, charm, gold, level, strength, agility, vitality, points}:
283	      H.Health.cap_nat_word_positive(Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), ceiling,
284	        (%Equal.sym(Nat, Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), G.Bq.Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), H.Health.add_agrees(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality))) : {G.Bq.Nat.le(1n, _) == True{} : Bool};
285	          H.Health.le_trans(1n, G.Bq.max_hp(level, vitality), G.Bq.Nat.add(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)), {==}, Growth.Growth.le_add_prefix(U32.to_nat(Rewards.charm_bonus(charm)), G.Bq.max_hp(level, vitality)))), limit_positive)