142 lines
17 KiB
JavaScript
142 lines
17 KiB
JavaScript
#!/usr/bin/env node
|
|
// control-negativ-operation.mjs: the negative control of proba-operation.mjs. Each guard is taken out of a COPY of this directory (with the
|
|
// files it imports from its neighbours, resolved from the import statements), the probe runs on the copy, and the rows that depend on that
|
|
// guard, AND ONLY THEY, must go red.
|
|
// 1. the witness: the untouched copy is green;
|
|
// 2. one planting per RULE of the operation verifier (every marked check of it made true): the red rows must be exactly the rows whose
|
|
// `expects` lists that rule (read from the probe's own --json, not typed here);
|
|
// 3. the plantings below, each with the rows it must turn red beside it: one CONDITION of a compound check at a time (a whole rule taken
|
|
// out says nothing about each half of it; two conditions that guard one thing are taken out together, and the planting says so), the
|
|
// bounds and the counting of the facts, and both implementations of the reputation (its check, its form, its formula).
|
|
// Three states: VERDE (exactly those rows went red), ROSU (others did, or none), STRICAT (a pattern is not in the file exactly once, or the
|
|
// probe on the copy did not reach its summary: a red that measures nothing). STRICAT counts as a failure.
|
|
// node control-negativ-operation.mjs [--doar <text>] exit 0 = the witness green and every planting red on exactly its rows
|
|
import fs from 'node:fs'; import os from 'node:os'; import path from 'node:path'; import { spawn } from 'node:child_process'; import { fileURLToPath } from 'node:url';
|
|
|
|
const AICI = path.dirname(fileURLToPath(import.meta.url)); const NUME = path.basename(AICI);
|
|
const PLANT = " || String(1) === '1' /*PLANTAT*/";
|
|
const OP = 'operation.mjs', REP = 'reputation.mjs', PY = 'reputation.py';
|
|
const T1 = "String(1) === '1'";
|
|
/** [name, file, pattern(s), replacement(s), rows that must go red] */
|
|
export const PLANTARI = [
|
|
['form: the kind of the log not looked at', OP, 'L.kind === LOG_KIND && L.v === VERSION', `(L.kind === LOG_KIND || ${T1}) && L.v === VERSION`, ['A01']],
|
|
['form: a member more beside the log allowed', OP, "numai(L, ['v', 'kind', 'credentials', 'records', 'anchors'])", `(numai(L, ['v', 'kind', 'credentials', 'records', 'anchors']) || ${T1})`, ['A02']],
|
|
['form: no bound on the number of keys', OP, 'L.credentials.length <= MAX_KEYS', `(L.credentials.length <= MAX_KEYS || ${T1})`, ['A03']],
|
|
['record-form: the exact members of a statement not required', OP, 'toate(r.statement, CAMPURI)', `(toate(r.statement, CAMPURI) || ${T1})`, ['A04']],
|
|
['record-form: any state allowed', OP, 'STATES.includes(s.state) && intreg(s.counter)', `(STATES.includes(s.state) || ${T1}) && intreg(s.counter)`, ['A05']],
|
|
['record-form: any text taken for a time', OP, 'eTimp(s.at) &&', `(eTimp(s.at) || ${T1}) &&`, ['A06', 'A07']],
|
|
['record-time: a time that goes back allowed', OP, 't >= prevAt && t <= acum + sk', `(t >= prevAt || ${T1}) && t <= acum + sk`, ['A18']],
|
|
['record-time: a time ahead of the verifier\'s clock allowed', OP, 't >= prevAt && t <= acum + sk', `t >= prevAt && (t <= acum + sk || ${T1})`, ['A19']],
|
|
['key-window: a record before its credential was valid allowed', OP, 'k.S.vf - sk <= t && t <= k.S.vu', `(k.S.vf - sk <= t || ${T1}) && t <= k.S.vu`, ['A21']],
|
|
['key-window: a record after its credential ended allowed', OP, 'k.S.vf - sk <= t && t <= k.S.vu', `k.S.vf - sk <= t && (t <= k.S.vu || ${T1})`, ['A22']],
|
|
// the derivation of the next device id and the match of the next key guard one thing (a key that does not derive the id it is named
|
|
// under): either alone refuses A28, so they are taken out TOGETHER
|
|
['rotation: the next key neither derives its id nor is the one certified (two guards together)', OP, 'nid === s.next.deviceId && s.next.deviceId === nk.S.deviceId && s.next.key === nk.S.key',
|
|
`(nid === s.next.deviceId || ${T1}) && s.next.deviceId === nk.S.deviceId && (s.next.key === nk.S.key || ${T1})`, ['A28']],
|
|
// the next device id and the next key against the next credential: either alone refuses A27d, so TOGETHER
|
|
['rotation: the next credential certifies another key (two guards together)', OP, 's.next.deviceId === nk.S.deviceId && s.next.key === nk.S.key', `(s.next.deviceId === nk.S.deviceId || ${T1}) && (s.next.key === nk.S.key || ${T1})`, ['A27d']],
|
|
['rotation: a rotation to the same key allowed', OP, 'nk.S.deviceId !== k.S.deviceId', `(nk.S.deviceId !== k.S.deviceId || ${T1})`, ['A27c']],
|
|
['rotation: another manufacturer allowed', OP, 'aceeasi(nk.S.issuer, k.S.issuer)', `(aceeasi(nk.S.issuer, k.S.issuer) || ${T1})`, ['A26']],
|
|
['rotation: another model allowed', OP, 'nk.S.model === k.S.model', `(nk.S.model === k.S.model || ${T1})`, ['A27b']],
|
|
['rotation: another serial allowed', OP, 'nk.S.serial === k.S.serial', `(nk.S.serial === k.S.serial || ${T1})`, ['A27']],
|
|
['anchor-envelope: a hash that does not reproduce allowed', OP, "hex0x(sha(Buffer.from(JSON.stringify(E.statement), 'utf8'))) === E.statementHash", `(hex0x(sha(Buffer.from(JSON.stringify(E.statement), 'utf8'))) === E.statementHash || ${T1})`, ['A30']],
|
|
['anchor-envelope: another device as the source allowed', OP, 'E.statement.source === recs[j].statement.deviceId', `(E.statement.source === recs[j].statement.deviceId || ${T1})`, ['A31']],
|
|
['a record of a key used after the log rotated away from it not told apart from one that is ignored', OP, 'if (p !== undefined && o.statement.seq > p) folosite++;', 'if (p !== undefined && o.statement.seq > p && String(1) === \'2\') folosite++;', ['V14', 'V15']],
|
|
['the records of a retired key counted with no witness before the retirement', OP, 'T === null || (x.hi !== null && x.hi <= T)', `T === null || ${T1} || (x.hi !== null && x.hi <= T)`, ['P08', 'R04', 'R09']],
|
|
['the upper bound taken from the LATEST anchor after a record instead of the earliest', OP, 'hi = hi === null ? a.at : Math.min(hi, a.at)', 'hi = hi === null ? a.at : Math.max(hi, a.at)', ['R01', 'R02', 'R04', 'R09', 'V06', 'V16']],
|
|
['the lower bound taken from the EARLIEST block before a record instead of the latest', OP, 'Math.max(lo, citit.at * 1000)', 'Math.min(lo, citit.at * 1000)', ['R01', 'R02', 'R09', 'C01']],
|
|
// the adversarial review of 2026-10-20: each planting puts back the defect its row was written for
|
|
['equivocation: a sibling beside a log record that does not carry its position (whoever moved the records makes the device equivocate)', OP, 'r.statement.seq === q && r.statement.deviceId === o.statement.deviceId', 'r.statement.deviceId === o.statement.deviceId', ['A42', 'E07']],
|
|
['equivocation: a sibling signed by a retired key taken for the device\'s (one record of a thief undoes the history a retirement keeps)', OP, 'if (k.retras !== null) { retrase++; continue; }', "if (k.retras !== null && String(1) === '2') { retrase++; continue; }", ['V16', 'V18']],
|
|
['block readings: only the four members (the form the block command writes refused)', OP, "numai(x, ['v', 'kind', 'chainId', 'block', 'hash', 'at'])", "numai(x, ['chainId', 'block', 'hash', 'at'])", ['V17', 'C01']],
|
|
['status: a retirement by another manufacturer the verifier trusts passed over in silence', OP, 'if (deAltul) nejudecat(', "if (deAltul && String(1) === '2') nejudecat(", ['P14']],
|
|
['status: a record of the manufacturer whose device id cannot be read passed over in silence', OP, "if (idR === null) { nejudecat('status-unread'", "if (idR === null) { continue; nejudecat('status-unread'", ['P15']],
|
|
['record-form: a record dated before 1970 allowed (its facts are refused by the formula)', OP, '!(Date.parse(s.at) < 0) && ', '', ['A43']],
|
|
['facts: any text named as the manufacturer', OP, 'AERE_ID.test(String(chei[0].S.issuer.id))', 'true', ['A44']],
|
|
['status: a retirement dated before 1970 kept as that time (facts the formula refuses)', OP, 'if (t < 0) t = -Infinity;', "if (t < 0 && String(1) === '2') t = -Infinity;", ['A45']],
|
|
['facts: uncounted counts only the records judged, not the ones beyond the bound', OP, 'uncounted: toateInreg - ', 'uncounted: recs.length - ', ['R13']],
|
|
// the reputation, JavaScript
|
|
['reputation (JS): every stated reputation accepted', REP, 'try { egal = canonical(input.claimed)', `try { egal = ${T1} || canonical(input.claimed)`, ['R06', 'R09', 'R11', 'R14']],
|
|
['reputation (JS): records out of order read as facts', REP, 'if (i && !(R[i - 1].seq < r.seq', "if (i && String(1) === '2' && !(R[i - 1].seq < r.seq", ['R07', 'R09', 'R11']],
|
|
['reputation (JS): per mille rounded to the nearest instead of down', REP, 'claimedPerMille: idiv(cc * 1000, n), witnessedPerMille: idiv(wc * 1000, n)', 'claimedPerMille: Math.round(cc * 1000 / n), witnessedPerMille: Math.round(wc * 1000 / n)', ['R02', 'R08', 'R09', 'R11', 'R14']],
|
|
['reputation (JS): a witnessed interval counted in a window it does not fit in', REP, 'if (r.hi < fin && witnessed[i] === null)', 'if (witnessed[i] === null)', ['R02', 'R08', 'R09', 'R11', 'C01', 'R14']],
|
|
['reputation (JS): the last gap left out when it runs to the end', REP, 'gaps.push([i, j - i]); i = j;', 'if (j < n) gaps.push([i, j - i]); i = j;', ['R08', 'R09', 'R11']],
|
|
['reputation (JS): the proofs of equivocation left out of the list', REP, 'list: facts.equivocations.map((x) => [x.seq, x.a, x.b])', 'list: []', ['R03', 'R08', 'R09', 'R11']],
|
|
// the reputation, Python
|
|
['reputation (Python): every stated reputation accepted', PY, "same = canonical(inp['claimed']) == canonical(reputation(inp['facts'], inp['params']))", 'same = True', ['R12', 'R14']],
|
|
['reputation (Python): per mille rounded to the nearest instead of down', PY, "'claimedPerMille': len(first_claimed) * 1000 // n, 'witnessedPerMille': len(first_witnessed) * 1000 // n",
|
|
"'claimedPerMille': round(len(first_claimed) * 1000 / n), 'witnessedPerMille': round(len(first_witnessed) * 1000 / n)", ['R08', 'R12', 'R14']],
|
|
['reputation (Python): a boolean read as a number', PY, 'return isinstance(x, int) and not isinstance(x, bool) and lo <= x <= SAFE', 'return isinstance(x, int) and lo <= x <= SAFE', ['R12']],
|
|
['reputation (Python): a witnessed interval counted in a window it does not fit in', PY, 'if hi < min(start + (i + 1) * w, end):', 'if True:', ['C01', 'R08', 'R12', 'R14']],
|
|
['reputation (Python): a whole number read digit by digit (int() refuses more than 4300 digits)', PY, 'val, i = num(m.group()), m.end()', "val, i = (int(m.group()) if m.group().lstrip('-').isdigit() else num(m.group())), m.end()", ['R14']],
|
|
['reputation (Python): the files read with json.loads (one recursion per level)', PY, 'return loads(f.read())', 'return json.loads(f.read(), parse_float=num)', ['R14']],
|
|
['reputation (Python): a claim nested deeper than the encoder goes not caught', PY, 'except (ValueError, TypeError, OverflowError, RecursionError):', 'except (ValueError, TypeError, OverflowError):', ['R14']],
|
|
// 2026-10-21 (the stranger pass): the line end Python writes on Windows, planted on every system (the default would differ only there)
|
|
['reputation (Python): the command line writes CRLF, as Python does on Windows by default', PY, "sys.stdout.reconfigure(newline='\\n')", "sys.stdout.reconfigure(newline='\\r\\n')", ['C01']],
|
|
];
|
|
|
|
const a = process.argv.slice(2); const doar = a.includes('--doar') ? a[a.indexOf('--doar') + 1] : null;
|
|
let verzi = 0, rosii = 0, stricate = 0;
|
|
const rand = (stare, text) => { console.log(` [${stare.padEnd(7)}] ${text}`); if (stare === 'VERDE') verzi++; else if (stare === 'ROSU') rosii++; else stricate++; };
|
|
|
|
// the copy: this directory, and every file of a neighbour it imports (a static import or a new URL of a relative path), resolved transitively
|
|
const VECINI = (() => {
|
|
const gasite = new Set(), deVazut = fs.readdirSync(AICI).filter((f) => f.endsWith('.mjs')).map((f) => path.join(AICI, f));
|
|
while (deVazut.length) {
|
|
const f = deVazut.pop(); const t = fs.readFileSync(f, 'utf8');
|
|
for (const m of t.matchAll(/(?:from |new URL\()'(\.\.?\/[^']+)'/g)) { const q = path.resolve(path.dirname(f), m[1]); if (q.startsWith(AICI + path.sep) || gasite.has(q) || !fs.existsSync(q)) continue; gasite.add(q); deVazut.push(q); }
|
|
}
|
|
return [...gasite].map((q) => path.relative(path.dirname(AICI), q));
|
|
})();
|
|
const T = fs.mkdtempSync(path.join(os.tmpdir(), 'aere-operation-control-'));
|
|
function copie(nume) {
|
|
const R = path.join(T, nume); const d = path.join(R, NUME);
|
|
fs.cpSync(AICI, d, { recursive: true });
|
|
for (const v of VECINI) { const q = path.join(R, v); fs.mkdirSync(path.dirname(q), { recursive: true }); fs.copyFileSync(path.join(path.dirname(AICI), v), q); }
|
|
return d;
|
|
}
|
|
function proba(d) {
|
|
return new Promise((gata) => {
|
|
const c = spawn(process.execPath, [path.join(d, 'proba-operation.mjs'), '--json'], { env: process.env, stdio: ['ignore', 'pipe', 'pipe'] }); let out = '', err = '';
|
|
c.stdout.on('data', (x) => { out += x; }); c.stderr.on('data', (x) => { err += x; });
|
|
c.on('close', () => { try { gata(JSON.parse(out.trim().split('\n').slice(-1)[0])); } catch { gata({ eroare: (err || out).trim().split('\n').slice(-2).join(' | ').slice(0, 300) }); } });
|
|
});
|
|
}
|
|
async function inParalel(sarcini, n = 4) { const rez = new Array(sarcini.length); let k = 0; await Promise.all(Array.from({ length: Math.min(n, sarcini.length) }, async () => { while (k < sarcini.length) { const i = k++; rez[i] = await sarcini[i](); } })); return rez; }
|
|
|
|
try {
|
|
console.log(`1. the witness: the untouched copy (with ${VECINI.length} files of the neighbours: ${VECINI.join(', ')})`);
|
|
const martor = await proba(copie('martor'));
|
|
if (martor.eroare || !Array.isArray(martor.rows)) { rand('STRICAT', 'the probe on the untouched copy did not reach its summary: ' + (martor.eroare || '')); throw new Error('stop'); }
|
|
const rosiiMartor = martor.rows.filter((r) => r.state !== 'VERDE').map((r) => r.id);
|
|
rand(rosiiMartor.length ? 'ROSU' : 'VERDE', `the untouched copy: ${martor.verzi} green, ${martor.rosii} red, ${martor.nemasurat} not measured` + (rosiiMartor.length ? ' (' + rosiiMartor.join(', ') + ')' : ''));
|
|
if (rosiiMartor.length) throw new Error('stop');
|
|
const iduri = new Set(martor.rows.map((r) => r.id));
|
|
const { REGULI } = await import('./operation.mjs');
|
|
const cazuri = [];
|
|
for (const r of REGULI) cazuri.push({ nume: `rule ${r} taken out (every marked check of it made true)`, fisier: OP, regula: r, asteptate: martor.rows.filter((x) => x.expects.includes(r)).map((x) => x.id) });
|
|
PLANTARI.forEach(([nume, fisier, de, cu, asteptate]) => cazuri.push({ nume, fisier, de: [de].flat(), cu: [cu].flat(), asteptate }));
|
|
const alese = cazuri.filter((c) => !doar || c.nume.includes(doar));
|
|
if (doar) console.log(` (FILTERED: --doar ${doar}: ${alese.length} of ${cazuri.length} plantings; the others are NOT controlled by this run)`);
|
|
console.log(`2-3. ${alese.length} plantings, each on its own copy (${REGULI.length} whole rules, ${PLANTARI.length} more)`);
|
|
const rez = await inParalel(alese.map((c, k) => async () => {
|
|
if (!c.asteptate.length) return { stricat: 'the planting names no row: it could not show anything' };
|
|
const lipsa = c.asteptate.filter((id) => !iduri.has(id)); if (lipsa.length) return { stricat: `the planting names rows the probe does not have: ${lipsa.join(', ')}` };
|
|
const d = copie('p' + k); const f = path.join(d, c.fisier); const src = fs.readFileSync(f, 'utf8'); let text = src;
|
|
if (c.regula) { const n = src.split(`/*PAZA:${c.regula}*/`).length - 1; if (n < 1) return { stricat: `no /*PAZA:${c.regula}*/ marker in ${c.fisier}` }; text = src.split(`/*PAZA:${c.regula}*/`).join(PLANT); }
|
|
else for (const [j, de] of c.de.entries()) { const n = src.split(de).length - 1; if (n !== 1) return { stricat: `pattern ${j + 1} appears ${n} times in ${c.fisier} (exactly once is required)` }; const m = text.split(de).length - 1; if (m !== 1) return { stricat: `pattern ${j + 1} is no longer there once after the pattern before it was replaced` }; text = text.replace(de, () => c.cu[j]); }
|
|
fs.writeFileSync(f, text); const r = await proba(d); fs.rmSync(path.dirname(d), { recursive: true, force: true }); return r;
|
|
}));
|
|
alese.forEach((c, k) => {
|
|
const r = rez[k];
|
|
if (r.stricat || r.eroare || !Array.isArray(r.rows)) return rand('STRICAT', `${c.nume}: ${r.stricat || 'the probe on the planted copy did not reach its summary: ' + (r.eroare || '')}`);
|
|
if (r.rows.length !== martor.rows.length) return rand('STRICAT', `${c.nume}: the planted probe ran ${r.rows.length} rows, the witness ${martor.rows.length}`);
|
|
const cazute = r.rows.filter((x) => x.state !== 'VERDE').map((x) => x.id).sort(), ast = [...c.asteptate].sort();
|
|
const ok = cazute.join() === ast.join();
|
|
rand(ok ? 'VERDE' : 'ROSU', `${c.nume}: ${cazute.length} row(s) red` + (ok ? `, exactly its ${ast.length} (${ast.join(', ')})` : `; required exactly [${ast.join(', ')}], red [${cazute.join(', ')}]`));
|
|
});
|
|
if (doar) rand('STRICAT', `${cazuri.length - alese.length} plantings left out by --doar`);
|
|
} catch (e) { if (e.message !== 'stop') throw e; } finally { fs.rmSync(T, { recursive: true, force: true }); }
|
|
console.log(`\ndevice operation (control): ${verzi} VERDE, ${rosii} ROSU, ${stricate} STRICAT`);
|
|
process.exitCode = rosii || stricate ? 1 : 0;
|