Post json fixes

.github/workflows/verify.yml

@@ -0,0 +1,35 @@
+name: Verify contributions
+
+# Validates the whole solution/ graph before a change lands, on both events so
+# that a direct push to main is covered as well as a pull request.
+#
+# Read-only, which is what makes it safe on a fork's branch. rebuild.yml is
+# separate because pushing artifacts back needs write access, and an untrusted
+# branch must not run with that.
+
+on: [push, pull_request]
+
+permissions:
+  contents: read
+
+concurrency:
+  # A pull request from a branch here raises both events; keying on its number
+  # puts them in one group so the duplicate is cancelled.
+  group: verify-${{ github.event.pull_request.number || github.ref }}
+  cancel-in-progress: true
+
+defaults:
+  run:
+    shell: bash   # for -o pipefail, so a failure piped through tee still fails
+
+jobs:
+  verify:
+    runs-on: ubuntu-latest
+    timeout-minutes: 30
+    steps:
+      - uses: actions/checkout@v7
+      - uses: actions/setup-python@v7
+        with: {python-version: '3.12'}
+
+      - name: Verify the whole graph
+        run: python solution/validate_solution.py | tee -a "$GITHUB_STEP_SUMMARY"

CONTRIBUTING.md

@@ -10,72 +10,82 @@ every Yellow reply or it does not. CI runs that check for you.
 Everything that defines the solution lives in `solution/`. Two files are
 hand-edited.
 
-**`solution/steady_states.txt`** holds one block of six rows per diagram, top
-row first, separated by blank lines:
-
-```
-.......
-.......
-.....|.
-..=|.+.
-2.=!1@-
-2.21112
+**`solution/steady_states.json`** is a list of diagrams, each a list of six
+rows, top row first:
+
+```json
+[
+  [
+    "   |   ",
+    "       ",
+    "   | | ",
+    "  =| + ",
+    "2 =!1@-",
+    "2 21112"
+  ]
+]
 ```
 
 - Exactly six rows of exactly seven characters.
-- `!` urgent, `@` miai, `|` claimodd, `.` claimeven, `+` plus, `=` equal,
+- `!` urgent, `@` miai, `|` claimodd, a space claimeven, `+` plus, `=` equal,
   `-` minus; `1` is a Red stone and `2` a Yellow stone.
 - The stones say which board a block belongs to, so it carries no separate
   identifier.
 - A `|` means different things on different rows. On an odd row it is a
   claimodd and can be played. On an even row it can never be played, and its
-  only effect is to stop that cell being a claimeven. `.` is the mirror of
+  only effect is to stop that cell being a claimeven. A space is the mirror of
   this, playable on an even row and silent on an odd one, so neither character
   is a blank.
 - A run of bars therefore marks the whole column as claimodd, each odd-row bar
   becoming playable as the column fills to that height, with the even-row bars
   between them suppressing the claimevens. Most such columns hold several
   claimodds rather than one.
-- Write claimeven as `.`, not a space. A trailing space is invisible and gets
-  stripped by editors, which would silently shorten a row.
+- A claimeven is a space, and the quoting keeps trailing ones intact, so count
+  the characters rather than trusting the eye: `"2      "` is a full row.
 - Only one of each mirror-equivalent pair is stored. The other orientation is
   re-derived when a representation is rendered, so do not add both.
 
-**`solution/branches.txt`** holds one line per non-leaf Red-to-move node,
-giving the single column Red commits to there:
+**`solution/branches.json`** maps each non-leaf Red-to-move node to the single
+column Red commits to there. The empty string is the empty board:
 
-```
-41->5
-4153->5
+```json
+{
+  "": "4",
+  "41": "5",
+  "4153": "5"
+}
 ```
 
-The two files interact. A node that gains a diagram stops being a
-non-leaf node, so its line comes out of `branches.txt`. Anything that was only reachable
-through it comes out too, both its branch lines and its diagrams. The validator
-rejects entries it cannot reach, so a contribution that only adds is usually
-incomplete.
+The two files interact. A node that gains a diagram stops being a non-leaf
+node, so its entry comes out of `branches.json`. Anything that was only
+reachable through it comes out too, both its branches and its diagrams. The
+validator rejects entries it cannot reach, so a contribution that only adds is
+usually incomplete. It reports the frontier rather than the whole set, so
+expect to run it, delete what it names, and run it again until it is quiet.
 
 A diagram contribution edits those two files and nothing else. Each
 subdirectory of `representations/` builds its artifacts from them with a
-`render.py`, and CI rejects a pull request that edits `graph.js` or a `.pb`.
-The webclient's 3D layout is a separate case: `spread_graph.py` nudges
-`representations/webclient/positions.txt` rather than deriving it, so nothing
-regenerates it automatically.
+`render.py`, and those are rebuilt automatically after a change lands, so a
+pull request should leave them alone. The webclient's 3D layout is a separate
+case: `spread_graph.py` nudges `representations/webclient/positions.txt`
+rather than deriving it, so nothing regenerates it automatically.
 
 ## What makes a diagram valid
 
 Red's move follows the priority list from the
 [explanation page](https://2swap.github.io/WeakC4/explanation/): win, block,
-`!`, `@` (only when exactly one is playable), `|` on an odd row or `.` on an
-even row, `+`, `=`, `-`. Red must win against *every* legal Yellow
+`!`, `@` (only when exactly one is playable), `|` on an odd row or a space on
+an even row, `+`, `=`, `-`. Red must win against *every* legal Yellow
 continuation; a draw is not enough.
 
 Two consequences of the site's guarantee that "there is always precisely one
 unique move suggested by this priority list":
 
 - **A tie between two markers at the same priority level is a failure**, not a
   coin flip. This has nothing to do with a drawn game. Two playable cells at
-  the applicable level means the diagram is rejected. Note that the viewer does
+  the applicable level means the diagram is rejected, with one exception: two
+  playable `@` do not tie, they cancel, and the next level decides instead.
+  Note that the viewer does
   not enforce this, since it only has to play a move and takes the leftmost of
   a tie, so watching the site play an ambiguous diagram will not reveal that it
   is ambiguous. Nothing there is checking.
@@ -96,25 +106,27 @@ subtree below a move is its own certificate.
 
 ## Checking before you open a pull request
 
-The checker needs only the standard library:
+CI runs this on your pull request, but running it first is quicker than
+waiting. It needs only the standard library:
 
 ```bash
 python solution/validate_solution.py
 ```
 
-It validates the whole solution in a few seconds. To see the shape of what you
-have changed:
+It validates the whole solution in a few seconds and prints a table of the
+nine checks, with the failing entries listed underneath. To see the shape of
+what you have changed:
 
 ```bash
 python solution/print_statistics.py
 ```
 
 ## What CI does
 
-Every push and pull request runs the same whole-solution check, and the result
-appears in the **Summary** panel of the workflow run, linked from the Checks
-tab. After a change lands on `main`, a second workflow re-renders whichever
-representations depend on what changed and commits them.
+Every push and pull request runs the whole-solution check, and the result
+appears in the **Summary** panel of the run, linked from the Checks tab. After
+a change lands on `main`, a second workflow re-renders the representations and
+commits whatever changed, and a third publishes the site.
 
 A first-time contribution needs a maintainer to approve the run, so an empty
 Checks tab at first is normal.

solution/validate_solution.py

@@ -358,8 +358,10 @@ def check_yellow_children(branches, steady_states):
                 continue
             child = [row[:] for row in board]
             child[y][x] = 2
+            # Red's committed move lost the game, so nothing below matters.
             if makes_four(child, x, y, 2):
-                continue
+                raise AssertionError([position, rmove, ymove,
+                                      "Yellow wins the game with this reply"])
             child_key = tuple(tuple(row) for row in child)
             canon = min(child_key, mirror_key(child_key))
 
@@ -416,6 +418,11 @@ def main():
                         help="parallel processes (default: one per core)")
     args = parser.parse_args()
 
+    # On Windows stdout falls back to the ANSI codepage whenever it is not a
+    # console (a pipe, a redirect, Git Bash), and cp1252 cannot encode the
+    # marks the table below is drawn with.
+    sys.stdout.reconfigure(encoding="utf-8")
+
     jobs = args.jobs or (os.cpu_count() or 1)
     started = time.time()