1	import Base
2	import ./types.bend as T
3	import ./game.bend as G
4	
5	# minebender: the laws.
6	#
7	# APPROVED by the owner on 2026-10-25, law by law (see NOTES.md). Never weaken
8	# or delete a law or definition here without the owner's explicit consent.
9	#
10	# The game is reached only through: G.fresh, G.step, G.open, G.knowledge,
11	# G.status, G.flagged, G.setup and G.place_mines. Everything else below is a
12	# definition owned by these laws, written to be obviously right rather than
13	# fast; the game's own code is free to compute the same things differently.
14	
15	# ==========================================================================
16	# Definitions: the board
17	# ==========================================================================
18	
19	# The value of grid g at p, or d when p is off the grid.
20	def at(-A: Data, d: A, g: T.Grid(A), p: T.Pos) -> A:
21	  match p:
22	    case T.Pos{x, y}:
23	      row = Maybe.default(&2, List<&2, A>, List.get(&2, List<&2, A>, g, y), Nil{})
24	      Maybe.default(&2, A, List.get(&2, A, row, x), d)
25	
26	def mine(layout: T.Grid(Bool), p: T.Pos) -> Bool:
27	  at(Bool, False{}, layout, p)
28	
29	def on_board(w: Nat, h: Nat, p: T.Pos) -> Bool:
30	  match p:
31	    case T.Pos{x, y}:
32	      Nat.is_lt(x, w) && Nat.is_lt(y, h)
33	
34	def same(p: T.Pos, q: T.Pos) -> Bool:
35	  match p q:
36	    case T.Pos{px, py} T.Pos{qx, qy}:
37	      Nat.is_eq(px, qx) && Nat.is_eq(py, qy)
38	
39	def dist(+a: Nat, +b: Nat) -> Nat:
40	  Nat.add(Nat.sub(a, b), Nat.sub(b, a))
41	
42	# p and q are at most one step apart in each direction (or the same cell).
43	def within_one(p: T.Pos, q: T.Pos) -> Bool:
44	  match p q:
45	    case T.Pos{px, py} T.Pos{qx, qy}:
46	      Nat.is_le(dist(px, qx), 1n) && Nat.is_le(dist(py, qy), 1n)
47	
48	# p and q are two different cells that touch, by a side or a corner.
49	def adjacent(+p: T.Pos, +q: T.Pos) -> Bool:
50	  Bool.not(same(p, q)) && within_one(p, q)
51	
52	# The cells of row y, from column 0 up.
53	def row_cells(+y: Nat, xs: List<&2, Nat>) -> List<&2, T.Pos>:
54	  match xs:
55	    case Nil{}:
56	      Nil{}
57	    case x <> t:
58	      T.Pos{x, y} <> row_cells(y, t)
59	
60	def cells.go(+w: Nat, ys: List<&2, Nat>) -> List<&2, T.Pos>:
61	  match ys:
62	    case Nil{}:
63	      Nil{}
64	    case y <> t:
65	      List.append(&2, T.Pos, row_cells(y, List.range(w)), cells.go(w, t))
66	
67	# Every cell of a w-by-h board, row by row.
68	def cells(w: Nat, h: Nat) -> List<&2, T.Pos>:
69	  cells.go(w, List.range(h))
70	
71	# The cells of qs adjacent to p, in the order of qs.
72	def touching(+p: T.Pos, qs: List<&2, T.Pos>) -> List<&2, T.Pos>:
73	  match qs:
74	    case Nil{}:
75	      Nil{}
76	    case +q <> t:
77	      List.filter.put(T.Pos, q, touching(p, t), adjacent(p, q))
78	
79	# The cells of the board adjacent to p, row by row.
80	def neighbours(w: Nat, h: Nat, p: T.Pos) -> List<&2, T.Pos>:
81	  touching(p, cells(w, h))
82	
83	def count_mines(+layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> Nat:
84	  match ps:
85	    case Nil{}:
86	      0n
87	    case q <> t:
88	      Nat.add(Bool.pick(Nat, mine(layout, q), 1n, 0n), count_mines(layout, t))
89	
90	# The number a revealed safe cell p must show.
91	def adj_mines(w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> Nat:
92	  count_mines(layout, neighbours(w, h, p))
93	
94	def row_mines(row: List<&2, Bool>) -> Nat:
95	  match row:
96	    case Nil{}:
97	      0n
98	    case b <> t:
99	      Nat.add(Bool.pick(Nat, b, 1n, 0n), row_mines(t))
100	
101	def total_mines(layout: T.Grid(Bool)) -> Nat:
102	  match layout:
103	    case Nil{}:
104	      0n
105	    case r <> t:
106	      Nat.add(row_mines(r), total_mines(t))
107	
108	def rows_wide(-A: Data, +w: Nat, g: T.Grid(A)) -> Bool:
109	  match g:
110	    case Nil{}:
111	      True{}
112	    case r <> t:
113	      Nat.is_eq(List.length(&2, A, r), w) && rows_wide(A, w, t)
114	
115	# g has exactly h rows of exactly w cells.
116	def shaped(-A: Data, w: Nat, h: Nat, +g: T.Grid(A)) -> Bool:
117	  Nat.is_eq(List.length(&2, List<&2, A>, g), h) && rows_wide(A, w, g)
118	
119	# ==========================================================================
120	# Definitions: knowledge
121	# ==========================================================================
122	
123	def seen(v: T.Knowledge, p: T.Pos) -> T.Seen:
124	  match v:
125	    case T.Knowledge{w, h, n, rows}:
126	      at(T.Seen, T.Hidden{}, rows, p)
127	
128	def is_hidden(s: T.Seen) -> Bool:
129	  match s:
130	    case T.Hidden{}:
131	      True{}
132	    case o:
133	      False{}
134	
135	# p is a cell of the board that the player cannot see.
136	def hidden(v: T.Knowledge, +p: T.Pos) -> Bool:
137	  match v:
138	    case T.Knowledge{w, h, n, rows}:
139	      on_board(w, h, p) && is_hidden(at(T.Seen, T.Hidden{}, rows, p))
140	
141	# p is a cell of the board that the player can see.
142	def revealed(v: T.Knowledge, +p: T.Pos) -> Bool:
143	  match v:
144	    case T.Knowledge{w, h, n, rows}:
145	      on_board(w, h, p) && Bool.not(is_hidden(at(T.Seen, T.Hidden{}, rows, p)))
146	
147	# What the player sees at p agrees with the layout.
148	def agrees(w: Nat, h: Nat, +layout: T.Grid(Bool), +p: T.Pos, s: T.Seen) -> Bool:
149	  match s:
150	    case T.Hidden{}:
151	      True{}
152	    case T.Shown{k}:
153	      Bool.not(mine(layout, p)) && Nat.is_eq(adj_mines(w, h, layout, p), k)
154	    case T.Boom{}:
155	      mine(layout, p)
156	
157	def agrees_all(+w: Nat, +h: Nat, +rows: T.Grid(T.Seen), +layout: T.Grid(Bool),
158	  ps: List<&2, T.Pos>) -> Bool:
159	  match ps:
160	    case Nil{}:
161	      True{}
162	    case +p <> t:
163	      agrees(w, h, layout, p, at(T.Seen, T.Hidden{}, rows, p))
164	        && agrees_all(w, h, rows, layout, t)
165	
166	# The layout could be the real one, given everything the player sees: it has
167	# the board's shape, exactly the announced number of mines, a mine under
168	# every Boom, none under a number, and every number counts its neighbours.
169	def consistent(v: T.Knowledge, +layout: T.Grid(Bool)) -> Bool:
170	  match v:
171	    case T.Knowledge{+w, +h, n, +rows}:
172	      shaped(Bool, w, h, layout) && shaped(T.Seen, w, h, rows)
173	        && Nat.is_eq(total_mines(layout), n)
174	        && agrees_all(w, h, rows, layout, cells(w, h))
175	
176	# p is hidden, and no layout consistent with what the player knows has a mine on p.
177	def ProvablySafe(v: T.Knowledge, p: T.Pos) -> Type:
178	  {hidden(v, p) == True{} : Bool} &
179	  (@layout: T.Grid(Bool) ->
180	    {consistent(v, layout) == True{} : Bool} ->
181	    {mine(layout, p) == False{} : Bool})
182	
183	# No cell is provably safe: the player's only options are guesses.
184	def Stuck(v: T.Knowledge) -> Type:
185	  @p: T.Pos -> ProvablySafe(v, p) -> Empty
186	
187	# Every safe cell of the board is revealed.
188	def all_safe_revealed.go(+v: T.Knowledge, +layout: T.Grid(Bool), ps: List<&2, T.Pos>) -> Bool:
189	  match ps:
190	    case Nil{}:
191	      True{}
192	    case +p <> t:
193	      (mine(layout, p) || revealed(v, p)) && all_safe_revealed.go(v, layout, t)
194	
195	def all_safe_revealed(+v: T.Knowledge, layout: T.Grid(Bool)) -> Bool:
196	  match v:
197	    case T.Knowledge{w, h, n, rows}:
198	      all_safe_revealed.go(v, layout, cells(w, h))
199	
200	# A zero: a safe cell of the board with no adjacent mine.
201	def zero(+w: Nat, +h: Nat, +layout: T.Grid(Bool), +p: T.Pos) -> Bool:
202	  on_board(w, h, p) && Bool.not(mine(layout, p))
203	    && Nat.is_eq(adj_mines(w, h, layout, p), 0n)
204	
205	# Starting at p, the path steps from cell to adjacent cell of the board,
206	# leaving only zeros, and ends at q. The empty path goes from p to p.
207	def zero_walk(path: List<&2, T.Pos>, +w: Nat, +h: Nat, +layout: T.Grid(Bool),
208	  +p: T.Pos, q: T.Pos) -> Bool:
209	  match path:
210	    case Nil{}:
211	      same(p, q)
212	    case +r <> t:
213	      zero(w, h, layout, p) && adjacent(p, r) && on_board(w, h, r)
214	        && zero_walk(t, w, h, layout, r, q)
215	
216	# ==========================================================================
217	# Definitions: the game
218	# ==========================================================================
219	
220	def is_won(s: T.Status) -> Bool:
221	  match s:
222	    case T.Won{}:
223	      True{}
224	    case o:
225	      False{}
226	
227	def is_lost(s: T.Status) -> Bool:
228	  match s:
229	    case T.Lost{why}:
230	      True{}
231	    case o:
232	      False{}
233	
234	# Take the actions in order.
235	def play(acts: List<&2, T.Action>, g: G.Game) -> G.Game:
236	  match acts:
237	    case Nil{}:
238	      g
239	    case a <> t:
240	      play(t, G.step(g, a))
241	
242	# The game g arises from a fresh game on this layout by some actions.
243	def Reachable(w: Nat, h: Nat, layout: T.Grid(Bool), g: G.Game) -> Type:
244	  Exists(List<&2, T.Action>,
245	    acts => {play(acts, G.fresh(w, h, layout)) == g : G.Game})
246	
247	def reveals(ps: List<&2, T.Pos>) -> List<&2, T.Action>:
248	  match ps:
249	    case Nil{}:
250	      Nil{}
251	    case p <> t:
252	      T.Reveal{p} <> reveals(t)
253	
254	# How many cells of qs are flagged.
255	def flags_among(+g: G.Game, qs: List<&2, T.Pos>) -> Nat:
256	  match qs:
257	    case Nil{}:
258	      0n
259	    case q <> t:
260	      Nat.add(Bool.pick(Nat, G.flagged(g, q), 1n, 0n), flags_among(g, t))
261	
262	def hidden_unflagged(+g: G.Game, +v: T.Knowledge, qs: List<&2, T.Pos>) -> List<&2, T.Pos>:
263	  match qs:
264	    case Nil{}:
265	      Nil{}
266	    case +q <> t:
267	      List.filter.put(T.Pos, q, hidden_unflagged(g, v, t),
268	        hidden(v, q) && Bool.not(G.flagged(g, q)))
269	
270	def chord_targets.pick(+g: G.Game, v: T.Knowledge, +ns: List<&2, T.Pos>, s: T.Seen) ->
271	  List<&2, T.Pos>:
272	  match s:
273	    case T.Shown{k}:
274	      Bool.pick(List<&2, T.Pos>, Nat.is_eq(flags_among(g, ns), k),
275	        hidden_unflagged(g, v, ns), Nil{})
276	    case o:
277	      Nil{}
278	
279	def chord_targets.go(g: G.Game, +v: T.Knowledge, +p: T.Pos) -> List<&2, T.Pos>:
280	  match v:
281	    case T.Knowledge{w, h, n, rows}:
282	      chord_targets.pick(g, v, neighbours(w, h, p), seen(v, p))
283	
284	# Chording on p: if p shows a number k and exactly k of its neighbours are
285	# flagged, the hidden unflagged neighbours of p, row by row; otherwise none.
286	def chord_targets(+g: G.Game, p: T.Pos) -> List<&2, T.Pos>:
287	  chord_targets.go(g, G.knowledge(g), p)
288	
289	# ==========================================================================
290	# Laws: the real board
291	# ==========================================================================
292	
293	# LAW: "The real board is always consistent with what the player sees."
294	# Without it, the knowledge laws below would say nothing about the real game.
295	# It also covers "every number equals its count of adjacent mines".
296	law bridge:
297	  for w: Nat
298	  for h: Nat
299	  for layout: T.Grid(Bool)
300	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
301	  for g: G.Game
302	  for r: Reachable(w, h, layout, g)
303	  {consistent(G.knowledge(g), layout) == True{} : Bool}
304	
305	# LAW: "The game is won exactly when every safe cell is revealed."
306	law won_iff:
307	  for w: Nat
308	  for h: Nat
309	  for layout: T.Grid(Bool)
310	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
311	  for g: G.Game
312	  for r: Reachable(w, h, layout, g)
313	  {is_won(G.status(g)) == all_safe_revealed(G.knowledge(g), layout) : Bool}
314	
315	# LAW: "A revealed cell stays revealed, showing the same thing."
316	# With bridge, this makes every action that changes the knowledge reveal at least
317	# one more cell, so a game has at most w*h such actions.
318	law monotone:
319	  for w: Nat
320	  for h: Nat
321	  for layout: T.Grid(Bool)
322	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
323	  for g: G.Game
324	  for r: Reachable(w, h, layout, g)
325	  for a: T.Action
326	  for q: T.Pos
327	  for vis: {revealed(G.knowledge(g), q) == True{} : Bool}
328	  {seen(G.knowledge(G.step(g, a)), q) == seen(G.knowledge(g), q) : T.Seen}
329	
330	# LAW: "Once the game is won or lost, no action changes anything."
331	law frozen:
332	  for g: G.Game
333	  for over: {G.status(g) != T.Playing{} : T.Status}
334	  for a: T.Action
335	  {G.step(g, a) == g : G.Game}
336	
337	# ==========================================================================
338	# Laws: revealing
339	# ==========================================================================
340	
341	# LAW: "Revealing a mine loses, naming that mine, and shows it as Boom."
342	law open_mine:
343	  for w: Nat
344	  for h: Nat
345	  for layout: T.Grid(Bool)
346	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
347	  for g: G.Game
348	  for r: Reachable(w, h, layout, g)
349	  for playing: {G.status(g) == T.Playing{} : T.Status}
350	  for p: T.Pos
351	  for boom: {mine(layout, p) == True{} : Bool}
352	  {G.status(G.open(g, p)) == T.Lost{T.Exploded{p}} : T.Status} &
353	  {seen(G.knowledge(G.open(g, p)), p) == T.Boom{} : T.Seen}
354	
355	# LAW: "Revealing a safe cell never loses."
356	law open_safe:
357	  for w: Nat
358	  for h: Nat
359	  for layout: T.Grid(Bool)
360	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
361	  for g: G.Game
362	  for r: Reachable(w, h, layout, g)
363	  for playing: {G.status(g) == T.Playing{} : T.Status}
364	  for p: T.Pos
365	  for safe: {mine(layout, p) == False{} : Bool}
366	  {is_lost(G.status(G.open(g, p))) == False{} : Bool}
367	
368	# LAW: "Revealing a cell p reveals every cell reached from p by a path
369	# through zeros" (so a 0 opens its whole 0-region and the numbers around it;
370	# for a mine, that is p alone).
371	law flood_complete:
372	  for w: Nat
373	  for h: Nat
374	  for layout: T.Grid(Bool)
375	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
376	  for g: G.Game
377	  for r: Reachable(w, h, layout, g)
378	  for playing: {G.status(g) == T.Playing{} : T.Status}
379	  for p: T.Pos
380	  for on: {on_board(w, h, p) == True{} : Bool}
381	  for q: T.Pos
382	  for path: List<&2, T.Pos>
383	  for walk: {zero_walk(path, w, h, layout, p, q) == True{} : Bool}
384	  {revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
385	
386	# LAW: "Revealing p reveals nothing else": every newly revealed cell is
387	# reached from p by a path through zeros. (For a mine, that is p alone.)
388	law flood_exact:
389	  for w: Nat
390	  for h: Nat
391	  for layout: T.Grid(Bool)
392	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
393	  for g: G.Game
394	  for r: Reachable(w, h, layout, g)
395	  for playing: {G.status(g) == T.Playing{} : T.Status}
396	  for p: T.Pos
397	  for q: T.Pos
398	  for before: {hidden(G.knowledge(g), q) == True{} : Bool}
399	  for after: {revealed(G.knowledge(G.open(g, p)), q) == True{} : Bool}
400	  exs path: List<&2, T.Pos>
401	  {zero_walk(path, w, h, layout, p, q) == True{} : Bool}
402	
403	# LAW: "Clicking a flagged cell does nothing."
404	law reveal_flagged:
405	  for g: G.Game
406	  for p: T.Pos
407	  for flag: {G.flagged(g, p) == True{} : Bool}
408	  {G.step(g, T.Reveal{p}) == g : G.Game}
409	
410	# LAW: "Clicking an unflagged cell reveals it."
411	law reveal_unflagged:
412	  for g: G.Game
413	  for p: T.Pos
414	  for flag: {G.flagged(g, p) == False{} : Bool}
415	  {G.step(g, T.Reveal{p}) == G.open(g, p) : G.Game}
416	
417	# LAW: "Double-clicking a number reveals its hidden unflagged neighbours,
418	# one by one, row by row" (when exactly that many neighbours are flagged).
419	law chord:
420	  for g: G.Game
421	  for p: T.Pos
422	  {G.step(g, T.Chord{p}) == play(reveals(chord_targets(g, p)), g) : G.Game}
423	
424	# ==========================================================================
425	# Laws: flags
426	# ==========================================================================
427	
428	# LAW: "Flags are not knowledge": flagging changes neither what the player
429	# sees nor the game's status.
430	law flag_no_knowledge:
431	  for g: G.Game
432	  for p: T.Pos
433	  {G.knowledge(G.step(g, T.Flag{p})) == G.knowledge(g) : T.Knowledge} &
434	  {G.status(G.step(g, T.Flag{p})) == G.status(g) : T.Status}
435	
436	# LAW: "Flagging a hidden cell during play toggles its flag."
437	law flag_toggle:
438	  for g: G.Game
439	  for playing: {G.status(g) == T.Playing{} : T.Status}
440	  for p: T.Pos
441	  for hid: {hidden(G.knowledge(g), p) == True{} : Bool}
442	  {G.flagged(G.step(g, T.Flag{p}), p) == Bool.not(G.flagged(g, p)) : Bool}
443	
444	# LAW: "Flagging p leaves every other cell's flag alone."
445	law flag_others:
446	  for g: G.Game
447	  for p: T.Pos
448	  for q: T.Pos
449	  for diff: {p != q : T.Pos}
450	  {G.flagged(G.step(g, T.Flag{p}), q) == G.flagged(g, q) : Bool}
451	
452	# LAW: "Only hidden cells carry flags": revealing a flagged cell clears its
453	# flag, and no cell off the board is ever flagged.
454	law flags_hidden:
455	  for w: Nat
456	  for h: Nat
457	  for layout: T.Grid(Bool)
458	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
459	  for g: G.Game
460	  for r: Reachable(w, h, layout, g)
461	  for q: T.Pos
462	  for flag: {G.flagged(g, q) == True{} : Bool}
463	  {hidden(G.knowledge(g), q) == True{} : Bool}
464	
465	# LAW: "Flagging a cell that is not hidden does nothing."
466	law flag_revealed:
467	  for g: G.Game
468	  for p: T.Pos
469	  for vis: {hidden(G.knowledge(g), p) == False{} : Bool}
470	  {G.step(g, T.Flag{p}) == g : G.Game}
471	
472	# ==========================================================================
473	# Laws: the no-guess assist
474	# ==========================================================================
475	
476	# LAW: "Pressing the assist when stuck reveals a safe cell."
477	law assist_stuck:
478	  for w: Nat
479	  for h: Nat
480	  for layout: T.Grid(Bool)
481	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
482	  for g: G.Game
483	  for r: Reachable(w, h, layout, g)
484	  for playing: {G.status(g) == T.Playing{} : T.Status}
485	  for stuck: Stuck(G.knowledge(g))
486	  for k: Nat
487	  exs p: T.Pos
488	  {mine(layout, p) == False{} : Bool} &
489	  {hidden(G.knowledge(g), p) == True{} : Bool} &
490	  {G.step(g, T.Assist{k}) == G.open(g, p) : G.Game}
491	
492	# LAW: "Pressing the assist when some cell is provably safe loses, and shows
493	# a provably safe cell; the knowledge is unchanged."
494	law assist_too_early:
495	  for w: Nat
496	  for h: Nat
497	  for layout: T.Grid(Bool)
498	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
499	  for g: G.Game
500	  for r: Reachable(w, h, layout, g)
501	  for playing: {G.status(g) == T.Playing{} : T.Status}
502	  for q: T.Pos
503	  for option: ProvablySafe(G.knowledge(g), q)
504	  for k: Nat
505	  exs p: T.Pos
506	  ProvablySafe(G.knowledge(g), p) &
507	  {G.status(G.step(g, T.Assist{k})) == T.Lost{T.AssistTooEarly{p}} : T.Status} &
508	  {G.knowledge(G.step(g, T.Assist{k})) == G.knowledge(g) : T.Knowledge}
509	
510	# ==========================================================================
511	# Laws: levels, as in Windows XP
512	# ==========================================================================
513	
514	def clamp(lo: Nat, hi: Nat, x: Nat) -> Nat:
515	  Nat.max(lo, Nat.min(hi, x))
516	
517	# Windows XP's Custom Field dialog: width is clamped to 9..30, height to
518	# 9..25 and mines to 10..999, then mines are capped at width*height - 10.
519	def custom(w: Nat, h: Nat, m: Nat) -> T.Setup:
520	  +cw = clamp(9n, 30n, w)
521	  +ch = clamp(9n, 25n, h)
522	  T.Setup{cw, ch, Nat.min(clamp(10n, 999n, m), Nat.sub(Nat.mul(cw, ch), 10n))}
523	
524	# LAW: "Beginner is 9 by 9 with 10 mines."
525	law level_beginner:
526	  {G.setup(T.Beginner{}) == T.Setup{9n, 9n, 10n} : T.Setup}
527	
528	# LAW: "Intermediate is 16 by 16 with 40 mines."
529	law level_intermediate:
530	  {G.setup(T.Intermediate{}) == T.Setup{16n, 16n, 40n} : T.Setup}
531	
532	# LAW: "Expert is 30 wide by 16 high with 99 mines."
533	law level_expert:
534	  {G.setup(T.Expert{}) == T.Setup{30n, 16n, 99n} : T.Setup}
535	
536	# LAW: "A custom level is limited exactly as Windows XP limits it."
537	law level_custom:
538	  for w: Nat
539	  for h: Nat
540	  for m: Nat
541	  {G.setup(T.Custom{w, h, m}) == custom(w, h, m) : T.Setup}
542	
543	# ==========================================================================
544	# Laws: board generation
545	# ==========================================================================
546	
547	# LAW: "Generated boards have the requested shape."
548	law gen_shape:
549	  for w: Nat
550	  for h: Nat
551	  for n: Nat
552	  for first: T.Pos
553	  for rs: List<&2, U32>
554	  {shaped(Bool, w, h, G.place_mines(w, h, n, first, rs)) == True{} : Bool}
555	
556	# LAW: "Generated boards have exactly n mines" (when they fit beside the first
557	# click).
558	law gen_count:
559	  for w: Nat
560	  for h: Nat
561	  for n: Nat
562	  for first: T.Pos
563	  for rs: List<&2, U32>
564	  for on: {on_board(w, h, first) == True{} : Bool}
565	  for fits: {Nat.is_lt(n, Nat.mul(w, h)) == True{} : Bool}
566	  {total_mines(G.place_mines(w, h, n, first, rs)) == n : Nat}
567	
568	# LAW: "The first click is safe."
569	law gen_first_safe:
570	  for w: Nat
571	  for h: Nat
572	  for n: Nat
573	  for first: T.Pos
574	  for rs: List<&2, U32>
575	  {mine(G.place_mines(w, h, n, first, rs), first) == False{} : Bool}
576	
577	# LAW: "When there's room, the first click opens an area: no mine on it or
578	# next to it." (As in Windows Vista and later.)
579	law gen_opening:
580	  for w: Nat
581	  for h: Nat
582	  for n: Nat
583	  for first: T.Pos
584	  for rs: List<&2, U32>
585	  for room: {Nat.is_le(Nat.add(n, 9n), Nat.mul(w, h)) == True{} : Bool}
586	  for q: T.Pos
587	  for near: {within_one(first, q) == True{} : Bool}
588	  {mine(G.place_mines(w, h, n, first, rs), q) == False{} : Bool}
589	
590	# ==========================================================================
591	# Laws: the display
592	# ==========================================================================
593	
594	# What the screen shows at p.
595	def tile(g: G.Game, p: T.Pos) -> T.Tile:
596	  at(T.Tile, T.Covered{}, G.display(g), p)
597	
598	# How a cell looks given what the player sees there and their flag.
599	def tile_of(s: T.Seen, flag: Bool) -> T.Tile:
600	  match s:
601	    case T.Hidden{}:
602	      Bool.pick(T.Tile, flag, T.Flagged{}, T.Covered{})
603	    case T.Shown{n}:
604	      T.Number{n}
605	    case T.Boom{}:
606	      T.Blast{}
607	
608	def is_covered(t: T.Tile) -> Bool:
609	  match t:
610	    case T.Covered{}:
611	      True{}
612	    case o:
613	      False{}
614	
615	# LAW: "During play, the screen shows exactly what the player knows, and
616	# their flags": nothing about the hidden mines leaks onto the screen.
617	law display_play:
618	  for w: Nat
619	  for h: Nat
620	  for layout: T.Grid(Bool)
621	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
622	  for g: G.Game
623	  for r: Reachable(w, h, layout, g)
624	  for playing: {G.status(g) == T.Playing{} : T.Status}
625	  for p: T.Pos
626	  for on: {on_board(w, h, p) == True{} : Bool}
627	  {tile(g, p) == tile_of(seen(G.knowledge(g), p), G.flagged(g, p)) : T.Tile}
628	
629	# LAW: "After an explosion, the screen shows the mine that exploded."
630	law display_blast:
631	  for w: Nat
632	  for h: Nat
633	  for layout: T.Grid(Bool)
634	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
635	  for g: G.Game
636	  for r: Reachable(w, h, layout, g)
637	  for p: T.Pos
638	  for lost: {G.status(g) == T.Lost{T.Exploded{p}} : T.Status}
639	  for on: {on_board(w, h, p) == True{} : Bool}
640	  {tile(g, p) == T.Blast{} : T.Tile}
641	
642	# LAW: "After the assist is pressed too early, the screen shows the safe cell
643	# the player could have revealed."
644	law display_hint:
645	  for w: Nat
646	  for h: Nat
647	  for layout: T.Grid(Bool)
648	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
649	  for g: G.Game
650	  for r: Reachable(w, h, layout, g)
651	  for s: T.Pos
652	  for lost: {G.status(g) == T.Lost{T.AssistTooEarly{s}} : T.Status}
653	  for on: {on_board(w, h, s) == True{} : Bool}
654	  {tile(g, s) == T.Hint{} : T.Tile}
655	
656	# LAW: "Once the game is over, no mine stays covered."
657	law display_mines:
658	  for w: Nat
659	  for h: Nat
660	  for layout: T.Grid(Bool)
661	  for shape: {shaped(Bool, w, h, layout) == True{} : Bool}
662	  for g: G.Game
663	  for r: Reachable(w, h, layout, g)
664	  for over: {G.status(g) != T.Playing{} : T.Status}
665	  for q: T.Pos
666	  for on: {on_board(w, h, q) == True{} : Bool}
667	  for m: {mine(layout, q) == True{} : Bool}
668	  {is_covered(tile(g, q)) == False{} : Bool}