Commit Graph
100 Commits
Author SHA1 Message Date
pj ccc4941df3 Merge branch 'one-workflow' into correctness-and-spec-skills 2026-08-16 03:33:05 +05:30
pj e326216461 docs: point at the workflow that holds the release secrets now
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 02:32:32 +05:30
pj 5dce2624b4 ci(folio): name the run, not the fuzzer, in the clean-run message
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 02:32:32 +05:30
pj 8b8173da43 ci: check that no run: block interpolates an expression
A ${{ }} lands in the script text before bash reads the line, and
actionlint only flags the contexts it already knows are attacker
controlled. Nothing enforced the rule the workflow follows. Also drops the
matrix table lookup, which has no table to read now.

Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 02:32:27 +05:30
pj 65007c4f21 ci: inline the two composite actions with one caller each
Both existed to give the matrix a per-target hook. folio-app and
headless-chrome stay: three and three callers.

Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 02:32:27 +05:30
pj 3235800afe ci: collapse the four workflows into one
Nine jobs written out one by one, each with its own steps and its own
calibrated seed and budget as literals. Triggers are pull requests, master
and v* tags, and a dispatch with no inputs.

Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 02:32:20 +05:30
pj 1a16b4b424 Merge branch 'one-examples-workflow' into correctness-and-spec-skills 2026-08-16 01:56:26 +05:30
pj 4848b8c067 ci: lint the workflows on every pr
The workflows that fuzz the examples are dispatch-only, and GitHub will
not dispatch a workflow that is not on the default branch, so their first
real run is after merge. actionlint and the reference checker are the
only things that can fail before that.

actionlint is pinned by commit, and its tool version is pinned too so a
new release cannot change what CI enforces.
2026-08-16 01:55:06 +05:30
pj 8e8a908e07 ci: check that the workflow references resolve
actionlint reads a local action's inputs but never checks its path
exists: uses: ./.github/actions/typo lints clean and fails only when the
job runs. Covers composite action paths, make targets including the ones
the examples matrix builds from $SANDERLING, and the scripts a run: step
invokes plus their executable bit.

Fails when it parses fewer references out of a file than that file
mentions, because a checker that matches nothing reports a safety it
never looked for.
2026-08-16 01:55:06 +05:30
pj 515e7249eb fix(ci): read the route the spec reports, not the hierarchy dump
The android health gate grepped the trace for "AddTransactionScreen",
which occurs in exactly one place: the hierarchy dump, as a resource-id.
That is a debug artifact standing in for a fact the spec already reports,
and it was wrong in both directions. Against the real 8.4MB trace with
hierarchy stripped, the old gate failed a healthy 200-step run; against a
trace carrying the marker on a transition frame without the route ever
being reported, it passed and called it healthy.

It reads extractor_changes.route now, whose values come from SCREENS in
the spec, so the gate and the app agree on what being on a screen means.
routeOf answers null on a frame showing two screens, which is exactly the
frame the marker was matching.

The drift check grows to cover both new names: extract("route") and the
SCREENS key. The fixtures are re-derived keeping the route entry and no
hierarchy at all; the full artifacts and the fixtures give byte-identical
verdicts, which is what proves the coupling is gone.

Script and fixtures move together: either alone leaves the suite red.
2026-08-16 01:51:11 +05:30
pj 0b32db17d6 Merge branch 'web-logs-reach-the-state' into correctness-and-spec-skills 2026-08-16 01:49:13 +05:30
pj 217ea590c5 test(runner): cover the silently dropped log fetch
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:46:11 +05:30
pj 0cfda3fa18 fix(runner): report a log fetch the driver could not make
The comment claimed the failure was warned about; nothing warned, so a
device whose log fetch failed every step held noLogcatErrors on evidence
nobody collected.

Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:46:11 +05:30
pj d11cec4c08 Merge branch 'one-examples-workflow' into correctness-and-spec-skills 2026-08-16 01:44:26 +05:30
pj a6b3ccee58 test(browser): drive console.error through to a fired property
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:42:50 +05:30
pj 3bab5c3f5c test(spec): cover the host pushing state.logs into the page
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:42:46 +05:30
pj cbf2c313ec test(runner): cover the logs reaching the page and failing to
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:42:16 +05:30
pj 78d57bf94f fix(runner): install the step's logs before the page extracts
On web every extractor reading is replaced by the one the page computed,
and the page answered logs: [], so noLogcatErrors counted an empty array
however full of errors the console was.

Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:41:10 +05:30
pj 3dfd5df511 test(runner): teach the web fakes to take the step's logs
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:41:06 +05:30
pj 6ab719fb77 test(ci): drive the classifier over the real traces
Four cases on real data: each leg's real verdict, plus the android trace
cut before it reached the transaction screen, which is what proves the
route gate reads a real hierarchy dump.

Also corrects the hand-written fixtures. They set is_error to false on a
plain violation; internal/trace/writer.go tags that field omitempty, so a
real trace omits it entirely. Harmless to the classifier, but a fixture
that does not look like reality is the thing that hides drift.
2026-08-16 01:40:25 +05:30
pj 1e2cfc78b8 test(ci): pin three real folio traces from run 31902501859
ios convicted on submitCommitsOneTransactionPerAction, web on both gated
properties, android ran its full 200 steps healthy. Every step is kept;
of each step only step, violations, witnesses and residuals survive.

hierarchy is replaced by the quoted "...Screen" resource ids it held, in
order. It cannot just be dropped: it is 95% of the bytes and also the
only place the android route gate's grep can match, so dropping it flips
that leg from healthy to 'never reached'. 8.4MB to 59KB.
2026-08-16 01:40:20 +05:30
pj 6d72410f55 feat(chrome): install the step's logs in the page
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:39:17 +05:30
pj e18dafeba9 feat(verifier): encode state.logs for the web host
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:38:42 +05:30
pj 226f5805aa feat(spec): let the runner install state.logs in the page
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:37:52 +05:30
pj 36caf6916f Merge branch 'web-logs-reach-the-spec' into correctness-and-spec-skills 2026-08-16 01:32:38 +05:30
pj b131c69e7b test(browser): cover console.error with an error object
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:29:58 +05:30
pj 59da61fecb fix(chrome): keep the message of an object console argument
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:29:58 +05:30
pj 73d2f16550 ci: run the folio classifier's test in make test-ci-scripts 2026-08-16 01:28:28 +05:30
pj a7c5193615 Merge branch 'one-examples-workflow' into correctness-and-spec-skills 2026-08-16 01:28:11 +05:30
pj 546c80885e docs(ioscompanion): name the vacuity behind the empty log slice
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:27:02 +05:30
pj c420b84768 Merge branch 'held-step-soundness' into correctness-and-spec-skills 2026-08-16 01:26:55 +05:30
pj fdc616247a test(browser): drive a console error through to the spec
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:23:58 +05:30
pj 264a78aca7 docs(ci): say why upload-pages-artifact needs no include-hidden-files
v3 to v5 crossed v4's change to exclude dot-files. build/site has none,
so nothing was dropped, and the underscore directory is not hidden.
2026-08-16 01:23:49 +05:30
pj beb036d2c1 fix(chrome): record console levels on the logcat scale
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:23:45 +05:30
pj 9b1fbdf60f fix(chrome): keep a log entry the level scale cannot rank
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:23:17 +05:30
pj 92d70ad9b8 docs(sidecar): name the device the node counts came off 2026-08-16 01:23:14 +05:30
pj a4c2a6b91c docs(driver): state the log level scale on LogEntry
Claude-Session: https://claude.ai/code/session_01ShuAy8q8ZfPi8KHxwc8JpQ
2026-08-16 01:23:04 +05:30
pj ae4323a704 ci(replay-ui): name the run directory for what it fuzzes
runs/dogfood and the '### replay-ui dogfood' heading carried the same
naming error as the job name: dogfooding is why the run exists, not what
it fuzzes.
2026-08-16 01:23:02 +05:30
pj baa2229abf ci: pin third-party actions to commit shas
buf-setup-action was already pinned with a comment saying why; the other
five rode mutable major tags, so a tag move is an unreviewed change to
what runs. Each major currently resolves to the release named in the
comment, so this freezes today's behaviour rather than changing it.

actions/* stay on major tags: they are first-party to the runner.
2026-08-16 01:22:58 +05:30
pj e2b53c1706 ci: move the folio jdk step to setup-java v5
The only setup-java left on v4; every other one moved.
2026-08-16 01:22:51 +05:30
pj c70d36d18d ci: reuse the headless-chrome action in the browser job
Same three steps the examples workflow needs, and the comment explaining
the AppArmor sysctl now lives in one place.
2026-08-16 01:22:51 +05:30
pj 52ee0ad424 ci(examples): one dispatch workflow for every example
folio.yml and replay-ui.yml ran the same operation: build sanderling for
a platform, bring a target up, run a spec against it, classify the trace,
upload the run. They are now one matrix over four examples, each naming
its own runner.

The job is named for what it fuzzes. 'dogfood' named why we run it, not
what runs, the same error as a diagnostic that reports a motivation
instead of an observation.

The matrix is computed by a plan job because jobs.<id>.if cannot read the
matrix context, so a static matrix has no way to leave a leg out. Seeds,
budgets, timeouts, runners and artifact names are unchanged.
2026-08-16 01:22:32 +05:30
pj 78ea4dd425 ci(examples): add the replay-ui fixture action
Records a trace and serves it with sanderling replay. The step page URL
is a composite output rather than GITHUB_ENV, so it is scoped to the one
step that drives it.
2026-08-16 01:22:25 +05:30
pj 71442bb85a ci(examples): add the folio setup actions
folio-app holds the per-platform toolchain and app build, so a caller
guards one step instead of eight. folio-simulator boots the simulator,
installs folio and leaves the app stopped.
2026-08-16 01:22:25 +05:30
pj de36939d67 ci: add a headless-chrome composite action
The setup-chrome / apparmor sysctl / launch-check trio is copied across
three jobs. The old comment described setup-chrome v1 semantics: under v2
stable is the default and the alternative is Chrome for Testing latest,
not a dev Chromium, so it is restated for what the pin actually does.
2026-08-16 01:22:20 +05:30
pj 0d588ff22f refactor(runner): name the settle predicate for what it means 2026-08-16 01:21:30 +05:30
pj 127234b58c docs(runner): say what makes the two reads comparable
the reread's comment claimed the round trip was the only interval between
them; what it left out is that the two rpcs have to read the same way, which
the repo's own android backend did not do.
2026-08-16 01:20:33 +05:30
pj 1afe9c3a7d fix(sidecar): the hierarchy rpc serves the tree the snapshot reads
the runner compares the two per step, but snapshot settles and closes a
keyboard while hierarchy was a bare contentDescriptor. measured on emulator
-5556 (api 34) with an ime open: 489 nodes against the snapshot's 134. both
now come off snapshotTree under the same lock; the reread still costs ~75ms
when no keyboard is up.
2026-08-16 01:20:28 +05:30
pj 565aea77e9 docs: a bound still needs the relaunch guard, and eventually does convict 2026-08-16 01:18:35 +05:30
pj 295d39220f Merge branch 'conjunct-that-cannot-fire' into correctness-and-spec-skills 2026-08-16 01:18:09 +05:30
pj 772eb1df5e Merge branch 'docs-that-are-true' into correctness-and-spec-skills 2026-08-16 01:15:30 +05:30
pj 32d78bfc0b docs(folio): say which form judged one step, not which node was read once 2026-08-16 01:15:30 +05:30
pj a3ed4608da fix(folio): an amount over the app's cap spends no window budget
the corpus reaches TxnSubmit with 999999999999999999999, AMOUNT_REGEX takes it
and AddTransactionViewModel refuses it against MAX_TRANSACTION_AMOUNT_CENTS, so
counting it was budget a double submit could hide behind.
2026-08-16 01:14:26 +05:30
pj e8cd43f85e Merge branch 'ios-recovery-and-clear-state' into correctness-and-spec-skills 2026-08-16 01:13:36 +05:30
pj 7a26a5575d docs(skills): folio drives three platforms from one spec 2026-08-16 01:13:15 +05:30
pj dfa3660659 docs(folio): the narrow window is not where the detection comes from
the double taps land on home, so the counting form convicts them; what turned
0 convictions into 4 on the recorded ios run is submitCouldCommit, which drops
the windows at those three steps from 5/4/7 to 2/1/2.
2026-08-16 01:12:51 +05:30
pj e6e71f9ba0 docs(folio): say which double submit the conjunct can see, and which it cannot
the home landing is the counting invariant's, three of three in the recorded
ios run; this one gets the interleaving whose second pop is cancelled. it is
still the only judge on the 18 ledger landings that run produced.
2026-08-16 01:12:32 +05:30
pj a275bf766c test(folio): the walk drives the composition the spec runs
countSubmitsInWindow never saw an amountText here, so every walk test counted
submits the app must have refused. with the field passed, a refused submit no
longer buys a later double tap an alibi: without it the window reads 3, not 1.
2026-08-16 01:12:09 +05:30
pj 969f58b329 test(folio): judge the conjunct on the landings a real run produces
three of the 18 frames the recorded ios run drove it down, each with the
second commit the bound is there to catch. neutering the comparison reddens
it: a second commit on 357900 went unjudged.
2026-08-16 01:10:49 +05:30
pj 7c5121801d docs(manual): the starter property only fires on web 2026-08-16 01:10:35 +05:30
pj 355ab38c2b docs(ci): three of the replay-ui properties are cross-panel 2026-08-16 01:10:19 +05:30
pj 40c39e93b9 fix(folio): the bound carries no unconfirmed-submit guard
deleting confirmedApplied here broke 0 of 355 tests: under a bound a submit
that may not have landed moves the balance by 0, which the bound already
permits, so the guard could only ever drop the double commit it exists to
catch. the relaunch guard stays for a reason the bound does not cover, and
both tests now assert a verdict that changes when their guard does.
2026-08-16 01:09:56 +05:30
pj 54e1f7e1a8 docs(manual): state.exceptions is web only and reportError does not exist 2026-08-16 01:09:32 +05:30
pj 0ef3ea03be docs(skills): three of the replay-ui properties are cross-panel 2026-08-16 01:09:01 +05:30
pj 4406d3b5ab test(ios): name the picker test for what it covers 2026-08-16 01:08:51 +05:30
pj 9dbc8f7c9a docs(skills): defaultActions bundles five of the eight generators 2026-08-16 01:08:47 +05:30
pj 41c6c1e4b9 test(ci): cover the folio classifier's verdicts
21 cases through a stubbed sanderling: every exit path, the drift check,
a missing trace, a zero-byte trace, an empty glob and a truncated line.
Asserts the flags that reached the binary, not just the exit code.

Invoked as bash -eo pipefail -c, which is what a run: block does. Running
folio-run.sh itself under -e would kill it at the first non-zero
sanderling test, which is the exit code it exists to read.
2026-08-16 01:08:45 +05:30
pj cd3bc51a0d fix(ci): fail folio when a gated property is not in the spec
Nothing tied GATED_PROPERTIES to the spec it gates. Renaming a property
left the classifier matching nothing: ios and web blamed the spec for
finding a different bug, and android silently reclassified a real
conviction as 'judging health only' and stayed green.

replay-ui-summary.sh already makes this check for its own list. The spec
path becomes SPEC-overridable the same way, so the check is testable.
2026-08-16 01:08:40 +05:30
pj 6263aa4c6c fix(ci): a run that wrote no trace is not evidence about folio
run_dir is empty when the run produced no output directory, and the
fallback made trace ./trace.jsonl. A stray trace in the working directory
was then read as this run's, so a run that wrote nothing reported 'found
the submit bug' and exited 0, defeating the missing-trace check below it.
2026-08-16 01:08:27 +05:30
pj 7c085c8c9d docs(skills): web selectors are exact, native ones are substrings 2026-08-16 01:08:19 +05:30
pj 906759dc15 docs(skills): substring selector matching is native only 2026-08-16 01:08:07 +05:30
pj 392e8dd445 docs(skills): screen= is the chrome driver's url, web only 2026-08-16 01:07:58 +05:30
pj 9172d1c378 docs(skills): quote the doctor the binary actually prints 2026-08-16 01:07:49 +05:30
pj 46aba1654f docs(skills): name the balance predicate that still exists 2026-08-16 01:06:59 +05:30
pj ef7466e61e docs(skills): both shipped balance forms are bounds now 2026-08-16 01:06:49 +05:30
pj cb45508e72 test(ios): a device driver can bring a runner up 2026-08-16 01:05:59 +05:30
pj 01f9ea942c fix(ios): one address picker for every bring-up
bringUpRunner reads the picker from a field, and NewDevice only ever set
the device one, so a device driver that reached bringUpRunner would call
nil. The two fields held the same function; keeping one leaves no path
that can be wired without it.
2026-08-16 01:05:59 +05:30
pj 4d14e9ca54 docs(manual): the flagship property is a bound, and say what that costs 2026-08-16 01:05:15 +05:30
pj d124354379 test(ios): a clear-state launch for an uncleared bundle is refused 2026-08-16 01:04:58 +05:30
pj 6beea91046 fix(ios): the clear-state guard checks the bundle that was cleared
A bool only said that something was cleared, so Launch(ctx, otherBundle,
clearState=true) passed the guard and reported a reset that had reached a
different app. Record what was cleared and compare against the bundle
being launched.
2026-08-16 01:04:58 +05:30
pj 8fbdc0296f docs(ci): the balance property demands a bound, not an equality 2026-08-16 01:04:12 +05:30
pj 18074e3bdd docs(skills): the stock properties each cover one platform 2026-08-16 01:04:05 +05:30
pj 99b9fe23f5 test(ios): a device clear-state without an app path ends the run 2026-08-16 01:03:48 +05:30
pj 220c7fe1d7 fix(ios): a device clear-state that cannot happen must fail
--clear-data on a physical device with no --ios-app-path warned and then
ran anyway, so the run started on the previous run's data while the flag
said it started clean. There is no data-container wipe on a device, so
there is nothing to fall back to.
2026-08-16 01:03:48 +05:30
pj be9cc78479 docs(skills): noUncaughtExceptions only fires on web 2026-08-16 01:03:47 +05:30
pj 45568f656b docs(skills): an unreached eventually convicts at run end 2026-08-16 01:03:35 +05:30
pj fea42e2899 docs(spec): an unbounded eventually is violated at run end 2026-08-16 01:03:25 +05:30
pj 9ede9dc3e2 test(ios): pin the stop that has to precede a clear
The ordering probe now records the stop, and a scripted xcrun holds what
reaches the tool: terminate before get_app_container, with the previous
run's files gone after. A simctl terminate that finds nothing to stop
still leaves the clear a success.
2026-08-16 01:03:02 +05:30
pj 119877c78a fix(ios): stop the app before clearing its state
Launch terminated and then cleared; the clear moved to construction and
left nothing stopping the app first. The container wipe deletes files a
live app still holds open, and the CI ios leg passes no app path so the
wipe is the path it takes. simctl stops it, since the clear now runs
before any automation session exists. On a device the uninstall that is
its only clear takes the running app with it.
2026-08-16 01:02:57 +05:30
pj 33c585de7b fix(testrun): a run that judged nothing is not a green run
every step skipped means no property ever evaluated, so no violations is the
absence of a verdict rather than a clean one. the hold makes that reachable
now, so the run says it instead of exiting 0.
2026-08-16 01:02:29 +05:30
pj 8e37be2afd test(runner): pin both guard writes to what the spec reads
deleting lastAction.Relaunched or lastAction.Applied left the whole suite
green, so the only producer of the two fields every spec-side guard reads
had nothing holding it. both now assert the value out of the trace.
2026-08-16 01:01:03 +05:30
pj f911079e32 test(ios): drive the launch recovery with what the transports return
The wedged-session fake answered with ctx.Err() raw, which is the one
shape the guard already matched. The recovery now runs against the error
each transport really produces for the same expiry, taken from a runner
and a legacy companion that never answer.
2026-08-16 01:00:49 +05:30
pj f1a5db886e fix(ios): recognise every shape a blown launch bound arrives in
The runner transport reports a blown budget two ways, its own comment says
so: the context's error once cancellation has landed, and the connection's
i/o timeout when the deadline armed from that context fires first. The
legacy transport reports it as a gRPC status. errors.Is against
context.DeadlineExceeded only matches the first, so the session restart
never fired for the other two and a wedged session stayed wedged.
2026-08-16 01:00:45 +05:30
pj 7f9c5df7db fix(ci): close shell injection into the npm publish job
A refname is attacker-controlled and git permits backtick, $, (, ; and |
in it. Three sites substituted it into a run: block, and NODE_AUTH_TOKEN
sat at job level, so a pushed tag ran arbitrary commands with the publish
credential in reach.

The tag now goes through env:, is validated against an anchored version
pattern before anything consumes it, and reaches the other jobs as a job
output. The token is scoped to the publish step. release-npm declares
contents: read instead of inheriting the repo default.
2026-08-16 01:00:40 +05:30
pj 0a7afbabec test(runner): pin what the two reads are compared on
structuralShape excluding text and bounds is the decision separating this
feature from a run that verifies nothing, and only prose held it. adding
either field back now turns a case red.
2026-08-16 00:59:13 +05:30
pj 86da6ed8ee fix(runner): a bounded hold puts the swallow back one step later
the hold carries one action; letting the runner act again while the verifier
is still skipped overwrites it, so the carried action reaches no spec. hold
for as long as the verifier is skipped, and settle on a held step so the
reread pair is not tighter than the window the detector was measured over.
2026-08-16 00:57:36 +05:30
pj 5b6816956f docs(ci): the cross-fade wait does not fire on ci, say so 2026-08-16 00:50:06 +05:30
pj 71134a3347 docs(ci): the ios leg convicts on the runner now, and why it did not before 2026-08-16 00:23:56 +05:30
pj d977265b30 Merge branch 'clear-state-must-happen' into correctness-and-spec-skills 2026-08-16 00:22:59 +05:30
pj ea952378fe test(android): name the uninstall failure for what it says, not why 2026-08-16 00:07:58 +05:30