law flood_exact

minebender-game@1.0.0.0 · LAWS.bend:386

import Base
import minebender-game@1.0.0.0/types.bend as T
import minebender-game@1.0.0.0/game.bend as G

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}