Compare commits
1 Commits
main
...
ee9bf03403
| Author | SHA1 | Date | |
|---|---|---|---|
| ee9bf03403 |
32
README.md
32
README.md
@@ -1052,20 +1052,24 @@ driving the real code with hostile values — and, for every field whose only
|
|||||||
defence is that nothing dereferences it, by booting the real popup entry point
|
defence is that nothing dereferences it, by booting the real popup entry point
|
||||||
over that value onto every view the popup can reopen onto. That last part is
|
over that value onto every view the popup can reopen onto. That last part is
|
||||||
what makes the claim falsifiable, because this defect class lives on the restore
|
what makes the claim falsifiable, because this defect class lives on the restore
|
||||||
path rather than on the home screen. Read the claim narrowly, as that file
|
path rather than on the home screen: whenever one of those boots reaches a
|
||||||
states it: what those boots prove is no structural dereference on the code paths
|
structural dereference on the view it restored onto, `make check` fails —
|
||||||
a WHOLLY-CORRUPTED PROFILE takes, which is not every path a stored record takes.
|
including a dereference that takes two corrupted fields at once, because the
|
||||||
Not driven: any pairing of values the four slots do not produce, a view only
|
verdict is the combined boot and the per-field re-boot that names a culprit can
|
||||||
forward navigation opens, anything behind a click, and everything a healthy
|
only decorate the message. Each swept field is driven at both polarities, or
|
||||||
profile reaches. Within that boundary the verdict is unconditional — if one of
|
proven unable to be falsy after the floor, since a value nothing writes is
|
||||||
those boots leaves the popup unhealthy or off the view it stored, `make check`
|
wrong-typed and therefore truthy and would otherwise leave every `if (!state.x)`
|
||||||
fails, including when it takes two corrupted fields at once, because the verdict
|
branch unentered. So does a field that gains a floor while its row still claims
|
||||||
is the combined boot and the per-field re-boot that names a culprit can only
|
it has none, and so does a field added to `PERSISTED_FIELDS` with no row at all.
|
||||||
decorate the message. So does a field that gains a floor while its row still
|
What the boots do not drive is every combination: four value combinations per
|
||||||
claims it has none, and so does a field added to `PERSISTED_FIELDS` with no row
|
view, not the product of the twelve swept fields. The last of the four is itself
|
||||||
at all. The per-field justification that used to live in the header of
|
a mix — every falsy-capable field falsy against the ones that cannot be falsy —
|
||||||
`src/shared/stateSchema.js` shipped a false claim in three consecutive changes,
|
so many two-field interactions are driven; one needing a pairing none of the
|
||||||
each caught only by a reviewer re-deriving thirty fields by hand.
|
four produces is not. Nor is anything no stored record reaches by itself — a
|
||||||
|
view only forward navigation opens, and anything behind a click. The per-field
|
||||||
|
justification that used to live in the header of `src/shared/stateSchema.js`
|
||||||
|
shipped a false claim in three consecutive changes, each caught only by a
|
||||||
|
reviewer re-deriving thirty fields by hand.
|
||||||
|
|
||||||
The `allowedSites` case is why the entry check is not optional. A stored
|
The `allowedSites` case is why the entry check is not optional. A stored
|
||||||
`{"0x…": "notalist"}` is a well-formed object holding a malformed entry: it
|
`{"0x…": "notalist"}` is a well-formed object holding a malformed entry: it
|
||||||
|
|||||||
18
TODO.md
18
TODO.md
@@ -85,15 +85,15 @@ but the review is broader than any of them.
|
|||||||
the path this whole class of defect lives on. Each such field is driven at
|
the path this whole class of defect lives on. Each such field is driven at
|
||||||
both polarities — a value nothing writes is wrong-typed and so truthy, so a
|
both polarities — a value nothing writes is wrong-typed and so truthy, so a
|
||||||
falsy slot is driven too, or the field is proven unable to be falsy after the
|
falsy slot is driven too, or the field is proven unable to be falsy after the
|
||||||
floor. The claim is narrow and stated as such: no structural dereference on
|
floor. A field with no row, a field that gains a floor while its row still
|
||||||
the code paths a wholly-corrupted profile takes, which is not every path a
|
claims it has none, and any structural dereference one of those boots reaches
|
||||||
stored record takes — a pairing of values the four slots do not produce, a
|
on the view it restored onto now all fail `make check` — including a
|
||||||
view only forward navigation opens, anything behind a click, and everything a
|
dereference that takes two corrupted fields at once, because the verdict is
|
||||||
healthy profile reaches are all undriven. Within that boundary the verdict is
|
the combined boot and the per-field re-boot that names a culprit can only
|
||||||
unconditional, including a dereference that takes two corrupted fields at
|
decorate the message. What is not driven is every combination: four value
|
||||||
once, since the assertion is on the combined boot and the per-field re-boot
|
combinations per view rather than the product of the twelve swept fields, so
|
||||||
can only decorate the message. A field with no row and a field that gains a
|
an interaction needing a pairing none of the four produces goes unseen, as
|
||||||
floor while its row still claims it has none also fail `make check`.
|
does anything no stored record reaches by itself.
|
||||||
- 2026-08-23: A swap amount and the token it is counted in now always come from
|
- 2026-08-23: A swap amount and the token it is counted in now always come from
|
||||||
the same hop, on both sides of the approval screen
|
the same hop, on both sides of the approval screen
|
||||||
([#359](https://git.eeqj.de/sneak/AutistMask/issues/359) and
|
([#359](https://git.eeqj.de/sneak/AutistMask/issues/359) and
|
||||||
|
|||||||
@@ -38,16 +38,24 @@
|
|||||||
// real popup entry point onto EVERY view the popup can reopen onto.
|
// real popup entry point onto EVERY view the popup can reopen onto.
|
||||||
//
|
//
|
||||||
// That last part is the whole point, because this defect class lives on the
|
// That last part is the whole point, because this defect class lives on the
|
||||||
// RESTORE path and not on Home. Take the claim NARROWLY, exactly as that file
|
// RESTORE path and not on Home: whenever one of those boots reaches a
|
||||||
// states it: what those boots prove is no structural dereference on the code
|
// structural dereference on the view it restored onto, that suite goes red —
|
||||||
// paths a WHOLLY-CORRUPTED PROFILE takes — which is not every path a stored
|
// including a dereference that takes two corrupted fields at once, since the
|
||||||
// record takes. Not driven: any pairing of values the four slots do not
|
// verdict is the combined boot and the per-field re-boot that names a culprit
|
||||||
// produce, a view only forward navigation opens, anything behind a click, and
|
// can only decorate the message. Each swept field is driven at both
|
||||||
// everything a healthy profile reaches. Within that boundary the verdict is
|
// polarities, or proven unable to be falsy after the floor: a value nothing
|
||||||
// unconditional, including a dereference that takes two corrupted fields at
|
// writes is wrong-typed and so truthy, which would otherwise leave every
|
||||||
// once. That suite also goes red on a field that gains a floor while its row
|
// `if (!state.x)` branch unentered. So does a field that gains a floor while
|
||||||
// still claims it has none, and on a field added to PERSISTED_FIELDS with no
|
// its row still claims it has none, and a field added to PERSISTED_FIELDS with
|
||||||
// row at all.
|
// no row at all.
|
||||||
|
//
|
||||||
|
// What the boots do NOT drive is every combination: four value combinations
|
||||||
|
// per view, not the product of the twelve swept fields. The last of the four
|
||||||
|
// is itself a mix — every falsy-capable field falsy against the ones that
|
||||||
|
// cannot be falsy — so many two-field interactions are driven; one needing a
|
||||||
|
// pairing none of the four produces is not. Nor is anything no stored record
|
||||||
|
// reaches by itself: a view only forward navigation opens, and anything behind
|
||||||
|
// a click.
|
||||||
//
|
//
|
||||||
// That test exists because this comment did not work. It carried a
|
// That test exists because this comment did not work. It carried a
|
||||||
// hand-written justification per field, and it shipped a false one in three
|
// hand-written justification per field, and it shipped a false one in three
|
||||||
|
|||||||
@@ -44,32 +44,23 @@
|
|||||||
// reason, and a field that cannot be falsy after the floor says so in its row
|
// reason, and a field that cannot be falsy after the floor says so in its row
|
||||||
// and is proven so.
|
// and is proven so.
|
||||||
//
|
//
|
||||||
// READ THE CLAIM NARROWLY. What this file proves is: NO STRUCTURAL
|
// What that buys: whenever one of those boots reaches a structural
|
||||||
// DEREFERENCE ON THE CODE PATHS A WHOLLY-CORRUPTED PROFILE TAKES. That is not
|
// dereference on the view it restored onto, this file goes red — INCLUDING a
|
||||||
// every path a stored record takes, and the difference is the whole of what
|
// dereference that takes two corrupted fields at once, because the verdict is
|
||||||
// this file does not cover:
|
// the combined boot itself and the per-field re-boot below can only decorate
|
||||||
|
// the message. That is the one thing an earlier version of this file got
|
||||||
|
// wrong: it asserted on the per-field list, so an observed dead popup that no
|
||||||
|
// single field reproduced was reported green.
|
||||||
//
|
//
|
||||||
// - Only the values in the table, in the SLOT arrangement below: four value
|
// What it does NOT buy is every combination — four value combinations per
|
||||||
// combinations per view, not the product of twelve fields. A dereference
|
// view are driven, not the product of twelve fields. Note that the last slot
|
||||||
// reached only under a pairing no slot produces is not driven at all.
|
// is itself a MIX rather than a uniform polarity: every falsy-capable field is
|
||||||
// - Only what a stored record reaches by ITSELF. A view only forward
|
// falsy on it while the neverFalsy ones stay hostile-truthy, so many two-field
|
||||||
// navigation opens, and anything behind a click, is not driven.
|
// interactions are driven and fatal. One that needs a pairing none of the four
|
||||||
// - Nothing about the paths a HEALTHY profile takes, which is most of the
|
// slots produces is not driven at all. Nor is anything no stored record
|
||||||
// popup. This file is a floor under one defect class, not a proof about
|
// reaches by itself: a view only forward navigation opens, and anything behind
|
||||||
// the renderers.
|
// a click. Booting every field separately at every value would be several
|
||||||
//
|
// hundred boots and most of the suite's budget; this is forty-four.
|
||||||
// Within that boundary it is unconditional: if one of these boots leaves the
|
|
||||||
// popup unhealthy or off the view it stored, this file goes red — including
|
|
||||||
// when it takes two corrupted fields at once, because the verdict is the
|
|
||||||
// combined boot itself and the per-field re-boot below can only decorate the
|
|
||||||
// message. That last part is the one thing an earlier version got wrong: it
|
|
||||||
// asserted on the per-field list, so an observed dead popup that no single
|
|
||||||
// field reproduced was reported green.
|
|
||||||
//
|
|
||||||
// Booting every field separately at every value would be several hundred boots
|
|
||||||
// and most of the suite's budget; this is forty-four. Widening it further is
|
|
||||||
// out of scope — proving no field is dereferenced on any reachable render path
|
|
||||||
// is exhaustive verification of the popup, not a floor under a stored record.
|
|
||||||
//
|
//
|
||||||
// The three claims this replaced, all false, all caught here by construction:
|
// The three claims this replaced, all false, all caught here by construction:
|
||||||
// rpcUrl reaching `new JsonRpcProvider()` (a synchronous throw, not a caught
|
// rpcUrl reaching `new JsonRpcProvider()` (a synchronous throw, not a caught
|
||||||
@@ -120,6 +111,19 @@ const swept = (row) => row.kind === KIND.LOOSE || Boolean(row.alsoSweep);
|
|||||||
// `if (!state.x) { state.y.deref() }`, so the falsy slot is not optional.
|
// `if (!state.x) { state.y.deref() }`, so the falsy slot is not optional.
|
||||||
const sweptValues = (row) => [...row.hostile, ...(row.falsy || [])];
|
const sweptValues = (row) => [...row.hostile, ...(row.falsy || [])];
|
||||||
|
|
||||||
|
// What may count toward a row's POLARITY: the swept values, plus only those
|
||||||
|
// `hostileRestore` entries driven onto every restorable view. An entry that
|
||||||
|
// carries `views: [...]` reaches only those renderers, so counting it would
|
||||||
|
// let a future row claim a polarity that one view sees and the other ten do
|
||||||
|
// not. No current row does that — the restricted entries are all viewData's,
|
||||||
|
// and viewData is neverFalsy — and this is what keeps it so.
|
||||||
|
const polarityValues = (row) => [
|
||||||
|
...sweptValues(row),
|
||||||
|
...(row.hostileRestore || [])
|
||||||
|
.filter((entry) => !entry.views)
|
||||||
|
.map((entry) => entry.value),
|
||||||
|
];
|
||||||
|
|
||||||
// ------------------------------------------------------------------ the table
|
// ------------------------------------------------------------------ the table
|
||||||
//
|
//
|
||||||
// `hostile` is values a stored record can carry that nothing in src/ ever
|
// `hostile` is values a stored record can carry that nothing in src/ ever
|
||||||
@@ -606,10 +610,9 @@ describe("both polarities of every swept field are driven", () => {
|
|||||||
test(`${row.field}: truthy and falsy`, () => {
|
test(`${row.field}: truthy and falsy`, () => {
|
||||||
// What the boots below actually drive, floored the way a renderer
|
// What the boots below actually drive, floored the way a renderer
|
||||||
// sees it — not what the row says it drives.
|
// sees it — not what the row says it drives.
|
||||||
const driven = [
|
const driven = polarityValues(row).map((value) =>
|
||||||
...sweptValues(row),
|
floored(row.field, value),
|
||||||
...(row.hostileRestore || []).map((entry) => entry.value),
|
);
|
||||||
].map((value) => floored(row.field, value));
|
|
||||||
|
|
||||||
expect({
|
expect({
|
||||||
truthy: driven.some((value) => Boolean(value)),
|
truthy: driven.some((value) => Boolean(value)),
|
||||||
|
|||||||
Reference in New Issue
Block a user