Commit Graph
333 Commits
Author SHA1 Message Date
pj a7c5193615 Merge branch 'one-examples-workflow' into correctness-and-spec-skills 2026-08-16 01:28:11 +05:30
pj c420b84768 Merge branch 'held-step-soundness' into correctness-and-spec-skills 2026-08-16 01:26:55 +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 92d70ad9b8 docs(sidecar): name the device the node counts came off 2026-08-16 01:23:14 +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