Oregami
Repositories/oxedyne/daimond

oxedyne/daimond/dev/verify_pausecore.mjs

10.9 KiB, 1 run

created by r2519314175:577, which is this file's identity for as long as the history lasts, whatever it is later renamed to

download · who wrote it · its history

1// verify_pausecore.mjs — the pause tree's rule, proved without a browser.
2//
3// The rule the whole PPTW rests on: a leaf is binary, a branch is green when
4// every ARMED leaf under it plays, red when none does, and amber otherwise —
5// with amber DERIVED and never settable. That is a statement about a tree and a
6// set, so it can be tested as one. `www/js/pause.js` exports its pure core for
7// exactly this; nothing here needs a page, a server or a clock.
8//
9// THE WORD "ARMED" IS NEW AND IT MOVED THE ANSWER, so the checks it changed are
10// written out rather than quietly edited. The light used to count every leaf, so
11// a node nobody had paused read green — and green was read, correctly, as
12// "running". The owner read the Email panel exactly that way: it "shows green
13// when all mailboxes are updated manually", which is green while nothing was
14// automated at all. It now counts only leaves with something set up to spend
15// WITHOUT BEING ASKED, and a node with none of those is `idle`: red, and said in
16// words as "nothing set up to run on its own", because red alone cannot tell
17// that apart from "the automation here is stopped".
18//
19// Two of these checks failed the first time they were run, which is the reason
20// the file exists rather than being folded into the widget's browser test:
21//
22// - `leavesUnder` treated a node with an EMPTY children array as a leaf, so an
23// empty branch — a mailbox whose folders have not loaded, a new account's
24// Diamonds section — got a pause flag of its own. Pausing the root then
25// wrote a phantom id that nothing would ever resume, and the empty-branch
26// rule in `stateOf` could never fire.
27//
28// The sorted-record and equal-stamp checks are here for the other reason: the
29// sync parcel has to be a FIXED POINT, and a set serialised in hash order is not
30// one. Two devices then push at each other for ever. See
31// `dev/verify_parcelstable.mjs`.
32//
33// node dev/verify_pausecore.mjs
34//
35// Needs nothing running.
36import { createRequire } from 'node:module';
37import path from 'node:path';
38import { fileURLToPath } from 'node:url';
39
40const HERE = path.dirname(fileURLToPath(import.meta.url));
41const require = createRequire(import.meta.url);
42const Pause = require(path.join(HERE, '..', 'www', 'js', 'pause.js'));
43const core = Pause._core;
44
45let bad = 0;
46const check = (pass, name, detail) => {
47 if (!pass) bad++;
48 console.log((pass ? ' ok ' : ' FAIL ') + name + (detail ? ' — ' + detail : ''));
49};
50
51// A tree with every shape that matters: a branch of branches, a Diamond with a
52// trigger beside its own `self` leaf, a bare leaf, and an EMPTY branch.
53const tree = {
54 id: 'root', children: [
55 { id: 'root/diamonds', children: [
56 { id: 'root/diamonds/a', children: [
57 { id: 'root/diamonds/a/self' },
58 { id: 'root/diamonds/a/triggers/t1' },
59 ] },
60 { id: 'root/diamonds/b', children: [ { id: 'root/diamonds/b/self' } ] },
61 ] },
62 { id: 'root/chats', children: [ { id: 'root/chats/c1' } ] },
63 { id: 'root/mail', children: [] }, // a mailbox list not yet loaded
64 { id: 'root/workers' },
65 ],
66};
67const ALL = {};
68for (const l of core.leavesUnder(tree)) ALL[l] = true;
69
70console.log('the tree');
71check(core.leavesUnder(tree).length === 5, 'five leaves, and the empty branch is not one',
72 JSON.stringify(core.leavesUnder(tree)));
73check(core.leavesUnder({ id: 'x' }).length === 1, 'a leaf is its own only leaf');
74check(core.leavesUnder({ id: 'y', children: [] }).length === 0, 'an empty branch has no leaves');
75check(core.findNode(tree, 'root/diamonds/a/self') !== null, 'a leaf is findable at depth');
76check(core.findNode(tree, 'root/nowhere') === null, 'an absent id is null, not a guess');
77
78console.log('the four states');
79check(core.stateOf(tree, {}) === 'play', 'everything playing is green');
80check(core.stateOf(tree, ALL) === 'pause', 'everything paused is red');
81check(core.stateOf(tree, { 'root/workers': true }) === 'mixed', 'one paused leaf is amber');
82check(core.stateOf(core.findNode(tree, 'root/mail'), ALL) === 'idle',
83 'an empty branch is IDLE — there is nothing there to be running or stopped');
84
85console.log('armed, which is what the light counts');
86// A leaf with no `armed` field is armed. The default matters: a leaf added later
87// by somebody who has not read this file behaves exactly as it did before rather
88// than silently dropping out of every light above it.
89check(core.armedUnder({ id: 'x' }).length === 1,
90 'a leaf that says nothing about it is armed');
91check(core.armedUnder({ id: 'x', armed: false }).length === 0,
92 'and one that says otherwise is not');
93check(core.armedUnder({ id: 'x', armed: true }).length === 1,
94 'and one that says so is');
95
96// THE OWNER'S DEFAULT CASE, which is the whole reason for this section: a node
97// with leaves, none of them automated. It read GREEN, meaning "running", with
98// nothing whatever running. It is red now, and the word says why.
99const manual = { id: 'm', children: [
100 { id: 'm/1', armed: false },
101 { id: 'm/2', armed: false },
102 { id: 'm/3', armed: false },
103] };
104check(core.leavesUnder(manual).length === 3, 'the leaves are still there');
105check(core.armedUnder(manual).length === 0, 'and none of them is armed');
106check(core.stateOf(manual, {}) === 'idle',
107 'a node whose every leaf is manual is IDLE and not green');
108check(core.stateOf(manual, { 'm/1': true, 'm/2': true, 'm/3': true }) === 'idle',
109 'and pausing all of them does not make it red for a different reason');
110
111// An unarmed leaf CONTRIBUTES NOTHING TO THE COLOUR while staying in the tree,
112// which is the property that lets the global control keep pausing it. Asserted
113// as an invariance: the same node, two different pause sets, one answer.
114const mixedArm = { id: 'k', children: [
115 { id: 'k/auto', armed: true },
116 { id: 'k/hand', armed: false },
117] };
118check(core.stateOf(mixedArm, {}) === 'play',
119 'one armed leaf playing beside a manual one is green, not amber');
120check(core.stateOf(mixedArm, { 'k/hand': true }) === 'play',
121 'and pausing the manual one changes nothing the light says');
122check(core.stateOf(mixedArm, { 'k/auto': true }) === 'pause',
123 'while pausing the armed one turns it red');
124check(core.leavesUnder(mixedArm).length === 2 && core.applySet(mixedArm, {}, false)['k/hand'],
125 'and the manual leaf is STILL WRITTEN by a click, so the global control reaches it');
126
127// The light can never count a leaf that is not in the tree. Written as a subset
128// test over every node rather than as one example, because the failure this
129// guards is a recursion that visits a child list twice.
130let subsetOk = true;
131for (const id of ['root', 'root/diamonds', 'root/diamonds/a', 'root/mail', 'root/workers']) {
132 const n = core.findNode(tree, id);
133 const leaves = core.leavesUnder(n);
134 for (const a of core.armedUnder(n)) if (!leaves.includes(a)) subsetOk = false;
135}
136check(subsetOk, 'every armed leaf is a leaf — the light cannot count what is not there');
137
138// AND THE OWNER'S THREE SENTENCES, as one table. "In the default case, the light
139// should show red, since there is no automation running, and the play icon
140// should be normal with the pause icon greyed out. As soon as one TA is active,
141// it should switch to orange, with both play and pause not greyed."
142const ta = (n, armed) => ({ id: 'd/triggers/' + n, armed: armed });
143const dia = (...kids) => ({ id: 'd', children: [{ id: 'd/self', armed: false }].concat(kids) });
144check(core.stateOf(dia(), {}) === 'idle',
145 'a Diamond with no triggered action reads red — there is no automation running');
146check(core.stateOf(dia(ta(1, true), ta(2, false)), {}) === 'play',
147 'a TA that cannot fire is not counted, so the one that can makes it green');
148check(core.stateOf(dia(ta(1, true), ta(2, true)), { 'd/triggers/1': true }) === 'mixed',
149 'one of two armed triggers held is orange');
150check(core.stateOf(dia(ta(1, true)), { 'd/triggers/1': true }) === 'pause',
151 'and the only armed trigger held is red');
152
153console.log('clicking');
154const a = core.findNode(tree, 'root/diamonds/a');
155const paused = core.applySet(a, {}, false);
156check(paused['root/diamonds/a/self'] && paused['root/diamonds/a/triggers/t1'],
157 'pausing a branch writes every leaf under it');
158check(!paused['root/diamonds/b/self'] && !paused['root/workers'],
159 'and touches nothing outside it');
160check(core.stateOf(a, paused) === 'pause', 'the branch then reads red');
161check(core.clickWould(a, {}) === 'pause', 'a green branch clicks to paused');
162check(core.clickWould(a, { 'root/diamonds/a/self': true }) === 'play',
163 'an AMBER branch clicks to playing — the alternative fights the user');
164check(core.stateOf(a, core.applySet(a, { 'root/diamonds/a/self': true }, true)) === 'play',
165 'resuming an amber branch clears every leaf under it');
166// The property, stated as a property: no single click ever lands on amber.
167let amberReachable = false;
168for (const start of [{}, ALL, { 'root/diamonds/a/self': true }, { 'root/workers': true }]) {
169 for (const nodeId of ['root', 'root/diamonds', 'root/diamonds/a', 'root/workers']) {
170 const node = core.findNode(tree, nodeId);
171 const next = core.applySet(node, start, core.clickWould(node, start) === 'play');
172 if (core.stateOf(node, next) === 'mixed') amberReachable = true;
173 }
174}
175check(!amberReachable, 'no click on any node, from any state, leaves that node amber');
176
177console.log('the stored record');
178const r = core.toRecord({ z: true, a: true, m: true }, 7);
179check(JSON.stringify(r.paused) === '["a","m","z"]', 'the record is sorted', JSON.stringify(r));
180check(JSON.stringify(core.toRecord({ m: true, z: true, a: true }, 7)) === JSON.stringify(r),
181 'and independent of insertion order — the parcel must be a fixed point');
182check(JSON.stringify(core.toRecord(core.fromRecord(r), 7)) === JSON.stringify(r),
183 'a record round trips unchanged');
184check(JSON.stringify(core.fromRecord({ paused: [null, '', 3, 'ok'] })) === '{"ok":true}',
185 'junk in a record is dropped rather than stored');
186check(JSON.stringify(core.fromRecord(null)) === '{}', 'no record at all is everything playing');
187
188console.log('merging two devices');
189check(JSON.stringify(core.mergeRecords({ paused: ['a'], stamp: 1 }, { paused: ['b'], stamp: 2 }).paused)
190 === '["b"]', 'the later stamp wins whole, so a resume propagates');
191const eqA = core.mergeRecords({ paused: ['a'], stamp: 5 }, { paused: ['b'], stamp: 5 });
192const eqB = core.mergeRecords({ paused: ['b'], stamp: 5 }, { paused: ['a'], stamp: 5 });
193check(JSON.stringify(eqA.paused) === '["a","b"]',
194 'equal stamps take the union — erring towards paused, because a wrong pause costs a click and a wrong resume costs money');
195check(JSON.stringify(eqA) === JSON.stringify(eqB), 'and the merge is order-independent');
196check(JSON.stringify(core.mergeRecords(r, r)) === JSON.stringify(r),
197 'merging a record with itself changes nothing');
198
199console.log('node ids');
200check(Pause.id('root', 'mail', 'a@b.com', 'INBOX/Sub') === 'root/mail/a@b.com/INBOX%2FSub',
201 'a slash inside a name is escaped, so a folder cannot invent a level',
202 Pause.id('root', 'mail', 'a@b.com', 'INBOX/Sub'));
203check(Pause.id('root', '', null, 'workers') === 'root/workers', 'empty parts are dropped');
204
205console.log(bad ? `\n${bad} failed` : '\nall checks passed');
206process.exit(bad ? 1 : 0);