Exhaustive walks

A journey proves one path works. The walks prove there is no path that breaks. They drive the Advocate the way people do, from every state they can reach, until nothing new is left.

The algorithm

flowchart TD
  seed[Seed: a student, at a depth] --> sig0[Signature of the starting state] --> q[(Queue)]
  q --> pop{Anything left?}
  pop -- no --> done([Fixpoint: every reachable state visited])
  pop -- yes --> node[Take a state]
  node --> acts[Every button on screen + navigation + things people type]
  acts --> fork[Fork the world]
  fork --> perform[Do the action]
  perform -- throws --> v1[Violation: crashed, with the exact path]
  perform --> check{Invariants}
  check -- fail --> v2[Violation, with the exact path]
  check --> sig{Seen this state before?}
  sig -- yes --> pop
  sig -- no --> q

Two walks

Each runs for all twelve students, at their own depth and again at brief and walk-me-through, every night. Only that full walk can certify a phase. On a push, the walk carries forward when nothing it executed has changed (below); otherwise a spot check walks four students whose settings differ most, bounded at 150 states per seed, and fails the build on any violation. Each student at each depth is an independent walk, so the full set runs one per CPU: more cores shorten the night, while the total compute stays the same.

Why it ends

The exact state of a student multiplies independent features together (every combination of drafts, reminders and held time) and never reaches a fixpoint. The walk uses an abstract state: each deadline's status, each playbook's step, whether a draft is waiting, whether a question is pending, which sources are on, and the buttons on screen. Settings are independent switches, so they are set by the seeds and walked on their own instead of being multiplied into every path.

flowchart LR
  exact[Exact state<br/>ids, timestamps, counts] -->|abstraction| abstract[Abstract state<br/>what changes behavior]
  abstract --> finite[Finite: the walk ends]
  settings[Settings switches] -->|seed variants + own walk| finite

Walk only when the walk could see the change

A walk runs under coverage, which records every source line it executed. On a later commit the change is diffed against the walked commit, and a walk is needed only if a hunk touches or borders an executed line, or changes data the app reads while it runs (playbooks, colleges, scouts, dependency versions). A change inside a function the walk never ran, such as an API handler the page walk never calls, cannot alter what the walk saw, so the earlier report is carried forward for the new commit and says so. The nightly run walks every student regardless and saves the coverage that pushes are compared against.

flowchart TB
  push([A push]) --> last[(Last full walk and the lines it executed)]
  last --> diff{Diff since the walked commit}
  diff -- touches an executed line --> walk[Walk under coverage]
  diff -- changes data the app reads --> walk
  diff -- only lines the walk never ran --> carry[Carry the report forward, naming the walked commit]
  walk --> rec[Record executed lines with the report]
  carry --> cert[Certificate for this commit]
  rec --> cert
  nightly([Nightly]) --> full[Walk all twelve students under coverage] --> save[(Saved as the last full walk)]

The one sanctioned skip is marked in the pipeline script, and the `zero-bypass` gate reads the scripts the required steps run, so any other way of skipping a walk fails the build.

What the walks found and fixed

Every finding is a fixture now; it cannot come back.

Verified by

• `apps/advocate/test/walks.test.ts` (2 test definitions)
• `tools/test/walk-coverage.test.ts` (9 test definitions)