Gates and proof
A green run is not a feeling; it is a printed receipt. Ståge is proven by 36 shell programs in script/, each of which compiles the shipped sources beside a harness and runs it on the local JVM — no JUnit, no Gradle, no emulator.
How a gate works
script/check-*.sh
├─ script/kotlinc.sh drives the compiler Gradle already cached — it fetches nothing
├─ Harness.kt the harness, compiled beside the shipped sources
├─ fixtures every gate has a NEGATIVE fixture: the case that must be refused
└─ proof/transcripts/… the receipt it writes, quoted by the proof document
Three rules make a gate worth having:
- A gate that cannot fail is not a gate. Each one carries a negative fixture and is proven against it before it is trusted —
check-hygiene.shplants a violation, proves the pattern catches it, and only then scans the trees. - A reading that moves because the scheduler moved is not a reading.
check-all.shruns the gates in a bounded pool (STAAGE_CHECK_JOBS, default 5) but assembles the summary in the declared order, whatever order they finished in. - A receipt is written, not remembered. Committed receipts under
proof/transcripts/are quoted by the proof documents and refreshed only by an explicit<check>.sh --write-receipt; a plain run writes under a run-stamped path sogit statusstays clean.
The suite
| Gate | Subject |
|---|---|
check-wire.sh | the codec round-trips; strict refusals; the credential gate over a real socket |
check-reducer.sh | the real reducer against a scripted host on loopback |
check-loom.sh | the host-side journal and surface: retention, eviction, the attach race |
check-loopback.sh | the real client against the real surface, over 127.0.0.1 |
check-determinism.sh | same input, byte-identical output across two JVMs; the no-clock gate |
check-gates.sh | the client's refusal contract, with a positive control per gate |
check-cli.sh | the reference client: command table, in-process loop, the v3 create → run loop, the real program as a second JVM |
check-daemon-store.sh | our schema and store: migrations, keyset pagination, abort/delete, one writer |
check-daemon-loop.sh | the turn loop and its state machine; every gate has a negative fixture |
check-daemon-loopback.sh | the already-proven client against our daemon, over the loopback |
check-daemon-provider.sh | the model plug: both real adapters over recorded SSE, no network and no keys |
check-daemon-v3.sh | wire v3: roster, create, search, models, activity — eight gates, plus mutations |
check-daemon-tools.sh | the tool-calling loop: batch boundary, one result per call, abort/unknown results, caps, duplicates, truncation, the registry — G1–G12 |
check-daemon-files.sh | the file instruments: the sealed outcome vocabulary, the digest anchor, confinement, the re-read receipt — F1–F11 |
check-daemon-find.sh | the search instruments: glob listing, content search, named bounds and cursors, locate-before-read |
check-daemon-skills.sh | the skills: the index and its sort, the description rule, the verbatim body, unknown names, empty/missing roots |
check-daemon-bash.sh | the command tool: the sandbox modes, the approval, what the box may not reach |
check-daemon-boot.sh | the boot's floor — the report a stranger reads, named and stable |
check-daemon-compact.sh | the request projection — compaction as a lens, not a summary |
check-daemon-delegation.sh | the child contract: the envelope's shape, the budgets, the named ends |
check-daemon-librarian.sh | the librarian: one hunt, a manifest, the merge by slug |
check-daemon-rails.sh | the rails: fail-closed declarations, the credential report, --require-rails |
check-daemon-release.sh | the release shelf's routes and the file's measure |
check-daemon-senses.sh | the Senses journal |
check-daemon-steer.sh | steering at the safe checkpoint |
check-daemon-profile.sh | the turn's tool profile: the wire carries the flag |
check-worker.sh | the workforce state machine's grid |
check-team-fixtures.sh | the team's configuration corpus |
check-standin.sh | the stand-in: first sight, the posture's class rule |
check-license.sh | the offline entitlement verifier |
check-store-roles.sh | one explicit store path per role |
check-hygiene.sh | no shipped file names internal tooling; no credential fails before serving; the bearer is never argv |
Not gates, and never in check-all:
| Program | What it is |
|---|---|
check-all.sh | the pool runner and the summary |
check-size.sh | the size report — list over 400, ~500 the soft target. A guideline |
check-summary.sh | the per-gate timing table for one run |
check-stability.sh | is this a flake? — one gate N times from a single compile: check-stability.sh check-daemon-loop 50 --load 6 |
mutation-*.sh | the proof that the gates can fail, each mutation run against exactly its own gate, in throwaway copies |
smoke-*.sh | the live runs: a real credential and a real socket. smoke-provider, smoke-daemon, smoke-files, smoke-find. Never in check-all |
Proof
proof/ holds one document per unit, in order, from 01-contract.md to the highest numbered reading: what was claimed, what was proven, and which receipt proves it. The message grammar and the reasoning behind each shape is proof/01-contract.md; the wire's receipt is 02; determinism is 04; the tool-calling loop is 19; the file instruments 32; the search instruments 33.
probes/ is the other half: a reproduced question lives there with a five-week TTL and leaves or becomes a gate.
The one habit
[object Object]
A red gate is not a failure of the tool, it is a reading: the change is wrong, or the gate is, and which one is decided by reading the receipt — never by re-running until it goes green.