LAWS.bend

minebender-game@1.0.0.0 · 668 lines · 76 definitions

1import Base
2import minebender-game@1.0.0.0/types.bend as T
3import minebender-game@1.0.0.0/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.
20def 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
26def mine(layout: T.Grid(Bool), p: T.Pos) -> Bool:
27  at(Bool, False{}, layout, p)
28
29def 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
34def 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
39def 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).
43def 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.
49def 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.
53def 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
60def 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.
68def 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.
72def 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.
80def neighbours(w: Nat, h: Nat, p: T.Pos) -> List<&2, T.Pos>:
81  touching(p, cells(w, h))
82
83def 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.
91def adj_mines(w: Nat, h: Nat, layout: T.Grid(Bool), p: T.Pos) -> Nat:
92  count_mines(layout, neighbours(w, h, p))
93
94def 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
101def 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
108def 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.
116def 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
123def 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
128def 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.
136def 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.
142def 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.
148def 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
157def 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.
169def 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.
177def 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.
184def Stuck(v: T.Knowledge) -> Type:
185  @p: T.Pos -> ProvablySafe(v, p) -> Empty
186
187# Every safe cell of the board is revealed.
188def 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
195def 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.
201def 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.
207def 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
220def is_won(s: T.Status) -> Bool:
221  match s:
222    case T.Won{}:
223      True{}
224    case o:
225      False{}
226
227def 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.
235def 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.
243def 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
247def 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.
255def 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
262def 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
270def 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
279def 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.
286def 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".
296law 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."
306law 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.
318law 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."
331law 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."
342law 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."
356law 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).
371law 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.)
388law 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."
404law 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."
411law 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).
419law 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.
430law 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."
437law 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."
445law 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.
454law 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."
466law 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."
477law 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."
494law 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
514def 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.
519def 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."
525law 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."
529law 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."
533law 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."
537law 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."
548law 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).
558law 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."
569law 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.)
579law 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.
595def 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.
599def 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
608def 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.
617law 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."
630law 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."
644law 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."
657law 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}