// plantari-device.mjs: the plantings of the negative control of the device verifier, as DATA, in one place. Two controls read them: // control-negativ-device.mjs (each planting must turn exactly its ROWS of the probe red) and the conformance suite's control of the // halves (its proba-conformance.mjs --control-negativ: the plantings it names must make exactly their VECTORS fail). // A planting is [what is taken out, file, pattern or [patterns], replacement or [replacements], the rows that must go red]; every // pattern must be in the file EXACTLY ONCE (a control whose pattern is gone is broken, and counts as a failure, not as a pass). // // What is planted here by hand: the defects of BEHAVIOUR (whose record counts, what lifts what, which of two holds, what is said and // what is passed in silence, the command line) and the conditions a search by mutation does not derive (a tolerance GIVEN to an // ending, two checks that guard one thing taken out together, an order turned round). The conditions of the verifier one at a time // (each side of every && and ||, every comparison, every edge of an interval, every tolerance, every yes-or-no call) are derived from // the code by mutanti-device.mjs, which needs no list. export const M = 'device.mjs', C = 'device-cli.mjs'; // the rows a planting must turn red can be derived from the witness run: by the rule they expect, or by the verdict they require const cuRegula = (r) => (rows) => rows.filter((x) => x.expects.includes(r)).map((x) => x.id); // every row that requires a PARTIAL verdict: the rows of that kind, and the rows of other kinds that require one among other things const partiale = (rows) => [...rows.filter((x) => x.kind === 'partial').map((x) => x.id), 'D05', 'D08', 'D09', 'S24', 'W08']; // every attack row that reaches the end of the verifier (a bundle refused for its form, or one that cannot be read, has no subject to return) const cuSubiect = (rows) => rows.filter((x) => x.kind === 'attack' && !x.expects.includes('form') && !x.expects.includes('unreadable')).map((x) => x.id); // the conditions of the windows, as they stand in the verifier const FER = 'nb - sk <= acum && acum <= na && nb - sk <= tq && tq <= na /*PAZA:authorization-window*/'; const PRO = 'tq <= acum + sk && acum - tq <= maxAgeS * 1000 /*PAZA:freshness*/'; const MW = 'vf - sk <= acum && acum <= vu /*PAZA:manufacture-window*/'; const ACE = 'a.id === b.id && canonical(a.keys) === canonical(b.keys)'; const DATA_ = "if (typeof s !== 'string' || !DATA.test(s) || !exista(s))"; const LISTA_A_LUI = "aceeasi(l.statement.issuer, S.issuer) && verifyText('status-list', canonical(l.statement), l.signature, S.issuer.keys)"; const POLITICA_A_LUI = "&& aceeasi(q.issuer, fw.signer) && verifica('firmware-policy', q, p.signature, fw.signer.keys)"; const CITIBIL = 'const citibil = s.v === VERSION && STATES.includes(s.state) && Number.isInteger(s.seq);'; const VEDERE = 'if (!v || s.seq > v.seq) vederi.set(s.by.id,'; const ROL = "S !== null && aceeasi(s.by, S.issuer) ? 'manufacturer' : aceeasi(s.by, owner) ? 'owner' : fosti.some((x) => aceeasi(s.by, x)) ? 'previous' : null;"; const ALT_PRODUCATOR = "if (semnat && incredere !== null && incredere.includes(s.by.id)) nejudecat('status-other-manufacturer'"; const LISTE_CLI = "o.statusLists = toate('--status-list').flatMap(elemente); o.firmwarePolicies = toate('--policy').flatMap(elemente); o.statusRecords = toate('--status').flatMap(elemente); o.anchors = toate('--reading').flatMap(elemente);"; // [what is taken out, file, pattern (exactly once) or [pattern, pattern], replacement or [replacement, replacement], the rows that must go red] export const PLANTARI = [ // ---- signatures and keys // D08 goes red with it: the evidence recorded on the testnet was signed with the purpose in the message, and no longer verifies without it ['no purpose separation (one message whatever the purpose)', M, "return Buffer.from(DOMENIU + scop + '\\n' + text, 'utf8'); }", "return Buffer.from(text, 'utf8'); }", ['C39', 'D08']], ['one half of the hybrid signature is enough', M, "Buffer.from(sig.ed25519, 'base64')) && crypto.verify(", "Buffer.from(sig.ed25519, 'base64')) || crypto.verify(", ['C38b', 'S16']], ['the type of the device key is not checked', M, 'if (k.asymmetricKeyType !== ALG_DEVICE) throw', 'if (false) throw', ['C12', 'C13', 'C14', 'D02']], ['the device key is accepted in any base64 text (its canonical form is not required)', M, "if (k.export({ type: 'spki', format: 'der' }).toString('base64') !== b64) throw", 'if (false) throw', ['F20', 'F21']], ['a hybrid signature of a link is accepted in any base64 text', M, 'if (!hibridCanonic(sig)) return false;', 'if (false) return false;', ['F35']], ['the attestation signature is accepted in any base64 text', M, 'b64canonic(X.signature.value) && crypto.verify(', "typeof X.signature.value === 'string' && crypto.verify(", ['F36']], ['the manufacturer\'s signature is accepted in any base64 text', M, "hibridCanonic(M.signature) && verifyText('credential'", "verifyText('credential'", ['F37']], ['identities are compared by their keys alone (the id half of the comparison taken out)', M, ACE, 'canonical(a.keys) === canonical(b.keys)', ['F23']], ['identities are compared by their id alone (the keys half of the comparison taken out)', M, ACE, 'a.id === b.id', ['F24']], ['the scheme a hybrid signature declares is not read', M, 'if (sig.alg !== ALG_HIBRID) return false;', 'if (false) return false;', ['H20']], ['the scheme the attestation signature declares is not read', M, 'X.signature.alg === ALG_DEVICE && b64canonic(', 'b64canonic(', ['C16']], // a link is exactly { statement, signature }, a signature exactly its members ['a member more in a hybrid signature object is accepted', M, 'if (!numai(sig, SEMN_HIBRID)) return false;', 'if (false) return false;', ['M01', 'M09']], ['a member more beside the statement and the signature of the manufacture credential is accepted', M, 'numai(M, LEGATURA) && numai(M.signature, SEMN_HIBRID)', 'numai(M.signature, SEMN_HIBRID)', ['M03']], ['a member more in the manufacturer\'s signature object is accepted', M, 'numai(M.signature, SEMN_HIBRID) && hibridCanonic(M.signature)', 'hibridCanonic(M.signature)', ['M04', 'RM12']], ['a member more beside the statement and the signature of a release is accepted', M, "numai(F, LEGATURA) && verifica('firmware'", "verifica('firmware'", ['M05']], ['a member more beside the statement and the signature of a transfer is accepted', M, "numai(T[i], LEGATURA) && verifica('transfer'", "verifica('transfer'", ['M02']], ['a member more beside the statement and the signature of an authorization is accepted', M, "numai(A, LEGATURA) && verifica('authorization'", "verifica('authorization'", ['M06']], ['a member more beside the statement and the signature of an attestation is accepted', M, 'numai(X, LEGATURA) && numai(X.signature, SEMN_DISPOZITIV)', 'numai(X.signature, SEMN_DISPOZITIV)', ['M07']], ['a member more in the attestation\'s signature object is accepted', M, 'numai(X.signature, SEMN_DISPOZITIV) && X.signature.alg', 'X.signature.alg', ['M08']], // the form of a time: three conditions ['a time in another form than RFC 3339 UTC is read (whatever a date parser understands)', M, DATA_, "if (typeof s !== 'string' || Number.isNaN(Date.parse(s)))", ['H21', 'H22', 'W09', 'W10']], ['a time that has the form of a time and is not a date is read', M, DATA_, "if (typeof s !== 'string' || !DATA.test(s))", ['T23', 'W09', 'W10']], ['a time that is not a text is read', M, DATA_, 'if (!DATA.test(s) || !exista(s))', ['T22']], // 2026-10-14 (third review): the check before was "the parser reads something" (Number.isNaN), and a date parser MOVES a day that does not exist ['a day that does not exist is read where the parser moves it (only what it cannot read at all is refused)', M, DATA_, "if (typeof s !== 'string' || !DATA.test(s) || Number.isNaN(Date.parse(s)))", ['W09', 'W10']], ['the verifier\'s clock is read by a date parser (a text without a zone is local time, "1" is the year 2001)', M, "typeof now === 'string' && DATA.test(now) && exista(now) ? Date.parse(now) : NaN", "typeof now === 'string' ? new Date(now).getTime() : NaN", ['W12', 'D11']], // ---- the manufacture credential ['a manufacture credential that has not begun is accepted', M, MW, 'acum <= vu /*PAZA:manufacture-window*/', ['F01']], ['an expired manufacture credential is accepted', M, MW, 'vf - sk <= acum /*PAZA:manufacture-window*/', ['C05', 'H13']], ['the ending of a manufacture credential is given the tolerance', M, MW, 'vf - sk <= acum && acum <= vu + sk /*PAZA:manufacture-window*/', ['H13']], ['the beginning of a manufacture credential is given no tolerance', M, MW, 'vf <= acum && acum <= vu /*PAZA:manufacture-window*/', ['H14', 'T02']], ['claims under selective disclosure are accepted in a manufacture credential', M, ' && Array.isArray(s.sd) && s.sd.length === 0 && ob(s.claims)', ' && Array.isArray(s.sd) && ob(s.claims)', ['H07']], ['a recall list of another manufacturer is believed', M, LISTA_A_LUI, "verifyText('status-list', canonical(l.statement), l.signature, l.statement.issuer.keys)", ['B05']], ['a recall list is believed on the issuer it names (its signature is not checked)', M, LISTA_A_LUI, 'aceeasi(l.statement.issuer, S.issuer)', ['S17']], ['a recall list signed with the manufacturer\'s keys is believed whatever issuer it names', M, LISTA_A_LUI, "verifyText('status-list', canonical(l.statement), l.signature, S.issuer.keys)", ['S18']], ['a recall list under another id is read as the list the credential names', M, 'return l.statement.id === S.status.list && aceeasi(', 'return aceeasi(', ['H05', 'H06']], ['the last current recall list decides (a recall is lifted by a clean list after it)', M, 'rev = statusBit(L, S.status.index) || rev; citite++;', 'rev = statusBit(L, S.status.index); citite++;', ['C07']], ['an expired recall list is read as current', M, "inV = data(l.statement.validFrom, 'status validFrom') - sk <= acum && acum <= data(l.statement.validUntil, 'status validUntil');", 'inV = true;', ['B06', 'B06b', 'H19', 'T06']], ['the ending of a recall list is given the tolerance', M, "acum <= data(l.statement.validUntil, 'status validUntil');", "acum <= data(l.statement.validUntil, 'status validUntil') + sk;", ['H19']], ['a recall list whose validity is not a time is dropped in silence', M, 'if (inV === null) listeNecitite++; else if (inV) curente.push(l);', 'if (inV) curente.push(l);', ['B06b']], ['a hardware root in the manufacture credential passes in silence', M, "if (S.claims.hardwareRoot != null) nejudecat('hardware-root'", "if (false) nejudecat('hardware-root'", ['B18']], // ---- firmware ['the id of who signed a release is not derived from its keys', M, 'idDin(R.signer.keys) === R.signer.id && (S === null', '(S === null', ['F26']], ['with two firmware policies the loosest floor holds', M, 'prag = Math.max(...curente', 'prag = Math.min(...curente', ['C22']], ['a retraction is lifted by a policy that does not list it', M, 'const retras = curente.some((p) => p.statement.retracted.some(', 'const retras = curente.every((p) => p.statement.retracted.some(', ['C24', 'D09']], ['a retraction written in upper case is not seen', M, 'const scris = (x) => String(x).toLowerCase();', 'const scris = (x) => String(x);', ['C24b', 'W04']], ['a firmware policy of a stranger is believed', M, POLITICA_A_LUI, "&& verifica('firmware-policy', q, p.signature, q.issuer.keys)", ['B08', 'W06']], ['a firmware policy is believed on the issuer it names (its signature is not checked)', M, POLITICA_A_LUI, '&& aceeasi(q.issuer, fw.signer)', ['S19']], ['a firmware policy signed with the manufacturer\'s keys is believed whatever issuer it names', M, POLITICA_A_LUI, "&& verifica('firmware-policy', q, p.signature, fw.signer.keys)", ['S20']], ['a firmware policy of another model is believed', M, 'return q.model === fw.model && aceeasi(q.issuer, fw.signer)', 'return aceeasi(q.issuer, fw.signer)', ['F12', 'W05']], // 2026-10-14 (third review): with the release left out, the firmware the device attests was not judged against the policies at all ['with the release left out, the firmware the device attests is not judged against the policies', M, 'if (F == null && S !== null && Q !== null) judecaPolitici(', 'if (false) judecaPolitici(', ['W01', 'W02', 'W03', 'W04', 'W07']], ['a firmware policy of a version this verifier does not read is dropped in silence', M, "if (q.v !== VERSION) { necitite.push('it is of a version this verifier does not read'); continue; }", 'if (q.v !== VERSION) continue;', ['F19c']], // the end of a policy's validity is no longer read: an expired policy counts, and a validity that is not a time is never looked at ['an expired firmware policy is read as current', M, "inVigoare = data(q.validFrom, 'policy validFrom') - sk <= acum && acum <= data(q.validUntil, 'policy validUntil');", "inVigoare = data(q.validFrom, 'policy validFrom') - sk <= acum;", ['F13', 'F14', 'F19b', 'H18']], ['the ending of a firmware policy is given the tolerance', M, "acum <= data(q.validUntil, 'policy validUntil');", "acum <= data(q.validUntil, 'policy validUntil') + sk;", ['H18']], ['a firmware policy that has not begun is read as current', M, "inVigoare = data(q.validFrom, 'policy validFrom') - sk <= acum && acum <= data(q.validUntil, 'policy validUntil');", "inVigoare = acum <= data(q.validUntil, 'policy validUntil');", ['F15']], ['a retracted entry that is not a digest is read as nothing retracted', M, "q.retracted.every((x) => typeof x === 'string' && DIGEST_SCRIS.test(x))", "q.retracted.every((x) => typeof x === 'string')", ['F16', 'F17', 'F18']], ['a floor that is not a whole number is read as a floor', M, 'else if (!(Number.isInteger(q.minSequence) && q.minSequence >= 0)) necitite.push(', 'else if (false) necitite.push(', ['F19', 'H10']], ['a negative floor is read as a floor', M, 'else if (!(Number.isInteger(q.minSequence) && q.minSequence >= 0)) necitite.push(', 'else if (!(Number.isInteger(q.minSequence))) necitite.push(', ['H10']], ['a policy whose validity is not a time is dropped in silence', M, 'if (inVigoare === false) continue;', 'if (inVigoare !== true) continue;', ['F19b']], ['a policy that cannot be read passes in silence', M, "if (necitite.length) nejudecat('firmware-policy-unread'", "if (false) nejudecat('firmware-policy-unread'", ['F16', 'F17', 'F18', 'F19', 'F19b', 'F19c', 'H10', 'S21', 'S22']], ['the Proof of Software attestation is not required to list the image', M, ' && softwareCovers(softwareAttestation, R.digest) /*PAZA:firmware-software*/', ' /*PAZA:firmware-software*/', ['F28', 'H08', 'H09']], ['the Proof of Software attestation is not required to be the one named', M, 'softwareAttestation.statementHash === R.softwareAttestationHash && softwareCovers(softwareAttestation, R.digest)', 'softwareCovers(softwareAttestation, R.digest)', ['C29']], ['the Proof of Software attestation is not required to hash to its statementHash', M, "hex0x(sha(Buffer.from(JSON.stringify(att.statement), 'utf8'))) === att.statementHash", 'true', ['H09']], ['an attestation of another kind is taken for a Proof of Software attestation', M, "att.statement.kind === 'aere-proof-of-software' && ", '', ['H08']], ['a release is written over an attestation that does not cover its image', M, 'if (softwareAttestation != null && !softwareCovers(softwareAttestation, dg)) throw', 'if (false) throw', ['D02']], ['a policy is written with a retracted entry that is not a digest', M, 'if (r.some((x) => !H32.test(x))) throw', 'if (false) throw', ['D02']], // ---- ownership ['the id of who GIVES a transfer is not derived from its keys', M, 'idDin(D.from.keys) === D.from.id && idDin(D.to.keys) === D.to.id /*PAZA:transfer-ids*/', 'idDin(D.to.keys) === D.to.id /*PAZA:transfer-ids*/', ['F09']], ['the id of who RECEIVES a transfer is not derived from its keys', M, 'idDin(D.from.keys) === D.from.id && idDin(D.to.keys) === D.to.id /*PAZA:transfer-ids*/', 'idDin(D.from.keys) === D.from.id /*PAZA:transfer-ids*/', ['C43']], ['the position of a transfer is not required', M, 'D.seq === i + 1 && (head === null || D.prev === head) /*PAZA:transfer-prev*/', '(head === null || D.prev === head) /*PAZA:transfer-prev*/', ['F07']], ['a transfer is not required to name the link before it', M, 'D.seq === i + 1 && (head === null || D.prev === head) /*PAZA:transfer-prev*/', 'D.seq === i + 1 /*PAZA:transfer-prev*/', ['F08']], ['a transfer may be dated in the future', M, 't >= tInainte && t <= acum + sk /*PAZA:transfer-time*/', 't >= tInainte /*PAZA:transfer-time*/', ['C41']], ['a transfer may be dated before the link before it', M, 't >= tInainte && t <= acum + sk /*PAZA:transfer-time*/', 't <= acum + sk /*PAZA:transfer-time*/', ['C40', 'H29']], ['a transfer is required to come after the manufacture only, not after the transfer before it', M, 'tInainte = t; owner = D.to; head = linkHash(T[i]);', 'owner = D.to; head = linkHash(T[i]);', ['H29']], ['a chain of exactly the most transfers that are read is refused', M, 'T.length <= MAX_TRANSFERS /*PAZA:chain-length*/', 'T.length < MAX_TRANSFERS /*PAZA:chain-length*/', ['H04']], ['a chain broken at the form of a link keeps its owner and its head', M, 'if (!lantBun) { owner = null; head = null; }', 'if (false) { owner = null; head = null; }', ['H30']], // ---- authorization: the four conditions of its window, one at a time, then the two pairs, then an ending given the tolerance ['the id of who grants an authorization is not derived from its keys', M, 'idDin(Z.owner.keys) === Z.owner.id && (owner === null', '(owner === null', ['F27']], ['an authorization that has not begun on the verifier\'s clock is accepted', M, FER, 'acum <= na && nb - sk <= tq && tq <= na /*PAZA:authorization-window*/', ['F06']], ['an authorization that ended on the verifier\'s clock is accepted', M, FER, 'nb - sk <= acum && nb - sk <= tq && tq <= na /*PAZA:authorization-window*/', ['F04']], ['an authorization that had not begun when the device attested is accepted', M, FER, 'nb - sk <= acum && acum <= na && tq <= na /*PAZA:authorization-window*/', ['F03']], ['an authorization that ends before the time of the attestation is accepted', M, FER, 'nb - sk <= acum && acum <= na && nb - sk <= tq /*PAZA:authorization-window*/', ['F05']], ['the authorization is not judged at the time of the attestation at all', M, FER, 'nb - sk <= acum && acum <= na /*PAZA:authorization-window*/', ['F03', 'F05']], ['the beginning of an authorization is not judged at all', M, FER, 'acum <= na && tq <= na /*PAZA:authorization-window*/', ['F02', 'F03', 'F06']], ['the ending of an authorization is given the tolerance on the verifier\'s clock', M, FER, 'nb - sk <= acum && acum <= na + sk && nb - sk <= tq && tq <= na /*PAZA:authorization-window*/', ['F04']], ['the ending of an authorization is given the tolerance at the time of the attestation', M, FER, 'nb - sk <= acum && acum <= na && nb - sk <= tq && tq <= na + sk /*PAZA:authorization-window*/', ['F05']], // ---- status: whose record counts ['the manufacturer\'s retirement, and the owner\'s, are lifted like a suspension', M, "if (s.state === 'retired') { if (retras === null", "if (false) { if (retras === null", cuRegula('status-retired')], ['the manufacturer\'s records stop counting once the device is sold', M, "S !== null && aceeasi(s.by, S.issuer) ? 'manufacturer'", "S !== null && aceeasi(s.by, S.issuer) && aceeasi(s.by, owner) ? 'manufacturer'", ['A08', 'A08b', 'C51', 'C52', 'C53', 'C53b', 'C55', 'D05', 'G09', 'G11', 'G12', 'H28', 'J01', 'J04', 'K07', 'S01', 'S03', 'S06', 'S09', 'T16', 'W08']], ['anyone can write a status record', M, "fosti.some((x) => aceeasi(s.by, x)) ? 'previous' : null;", "fosti.some((x) => aceeasi(s.by, x)) ? 'previous' : 'owner';", ['A06', 'J05', 'K01', 'K02', 'K03', 'K04', 'K05', 'K06', 'S25']], ['a record of a PREVIOUS owner binds the owner of now', M, "aceeasi(s.by, x)) ? 'previous' : null;", "aceeasi(s.by, x)) ? 'owner' : null;", ['A07', 'D07', 'G06', 'G07', 'G08', 'G14', 'I10', 'J06']], ['an owner that owned the device before is taken for a previous owner (the order of the roles turned round)', M, ROL, "S !== null && aceeasi(s.by, S.issuer) ? 'manufacturer' : fosti.some((x) => aceeasi(s.by, x)) ? 'previous' : aceeasi(s.by, owner) ? 'owner' : null;", ['A11', 'G03', 'G04', 'G05']], ['the records of a previous owner pass in silence', M, "nejudecat('status-prior-ownership', 'status', `status: ${l.citite.length", "void ('status-prior-ownership', 'status', `status: ${l.citite.length", ['A07', 'D07', 'G06', 'G07', 'G08', 'G14', 'I10']], ['what the records of a previous owner say is not reported', M, 'priorOwnership: subAnteriori,', 'priorOwnership: [],', ['A07', 'D07', 'G06', 'G07', 'G08', 'I10']], ['what the records of a previous owner say is reported without their number', M, 'subAnteriori.push({ owner: id, state: spune, records: l.citite.length });', 'subAnteriori.push({ owner: id, state: spune, records: 1 });', ['A07', 'G08', 'I10']], ['of a previous owner\'s records, "suspended" is said when any says so (not the highest)', M, "l.citite.some((x) => x.seq === m && x.state === 'suspended') ? 'suspended'", "l.citite.some((x) => x.state === 'suspended') ? 'suspended'", ['G08']], ['of a previous owner\'s records, "retired" is said only when the highest says so', M, "l.citite.some((x) => x.state === 'retired') ? 'retired'", "l.citite.some((x) => x.seq === m && x.state === 'retired') ? 'retired'", ['G08']], // the defect this control did not see on 2026-10-05: a retirement of the owner of now under another head, or under none, was ignored ['the owner\'s retirement and suspension count only under the current ownership head', M, "if (rol === 'owner' && s.state === 'active' && s.ownership !== head) {", "if (rol === 'owner' && s.ownership !== head) {", ['G01', 'G02', 'G03', 'G04']], ['an "active" record of the owner is believed under any ownership head', M, "if (rol === 'owner' && s.state === 'active' && s.ownership !== head) {", 'if (false) {', ['G05']], ['a record of who may give it that cannot be read is ignored (the registry is read as clean)', M, "if (!citibil) { nejudecat('status-unread', 'status', 'status: a record of who may give it that cannot be read'", "if (!citibil) { nejudecat('status-ignored', 'status', 'status: a record of who may give it that cannot be read'", ['G12', 'G13', 'H11', 'H12']], ['a record of another version, or with a state the verifier does not know, is read as one of this version', M, CITIBIL, 'const citibil = true;', ['G12', 'G13', 'G14', 'H11', 'H12']], ['a record whose number is not a whole number is read', M, CITIBIL, 'const citibil = s.v === VERSION && STATES.includes(s.state);', ['H11', 'H12']], ['a record with a state this verifier does not know is read', M, CITIBIL, 'const citibil = s.v === VERSION && Number.isInteger(s.seq);', ['G13', 'G14']], ['a record of another version is read', M, CITIBIL, 'const citibil = STATES.includes(s.state) && Number.isInteger(s.seq);', ['G12']], // which device a record is about ['a record of another device is applied to this one', M, 'if (idInreg !== null && idInreg !== devScris) continue;', 'if (false) continue;', ['F22']], ['the device id of a record is compared with regard to case', M, 'const DEV_SCRIS = /^aere-device:([0-9a-fA-F]{40})$/;', 'const DEV_SCRIS = /^aere-device:([0-9a-f]{40})$/;', ['J01', 'J02']], ['a record whose device id is not a device id is passed over in silence', M, 'if (idInreg !== null && idInreg !== devScris) continue;', 'if (idInreg !== devScris) continue;', ['J03', 'J04', 'J05', 'J06', 'S06']], ['a record of who may give it whose device id cannot be read is ignored (the registry is read as clean)', M, "if (aLui) nejudecat('status-unread', 'status', 'status: a record whose device id cannot be read'", "if (false) nejudecat('status-unread', 'status', 'status: a record whose device id cannot be read'", ['J03', 'J04', 'S06']], ['a device id written as a one-element list is read as the id', M, "const m = typeof x === 'string' ? DEV_SCRIS.exec(x) : null;", 'const m = DEV_SCRIS.exec(x);', ['S06']], // TWO checks guard a record of the owner or of the manufacturer under an id its keys do not derive: the derivation in the status // loop, and the id half of every comparison of identities. Either alone refuses it (F25 stays green with one of them out), so they // are planted out together. The derivation ALONE is what keeps a stranger from speaking under the id of another trusted manufacturer. ['DOUBLE: a status record under an id its keys do not derive is applied (the derivation in the status loop AND the id half of the comparison, both out)', M, ["idDin(s.by.keys) === s.by.id && verifica('status'", ACE], ["verifica('status'", 'canonical(a.keys) === canonical(b.keys)'], ['F23', 'F25', 'S07']], ['a status record signed with any keys under the id of another trusted manufacturer is taken for that manufacturer\'s', M, "idDin(s.by.keys) === s.by.id && verifica('status'", "verifica('status'", ['S07']], ['a record of another manufacturer the verifier trusts is passed over', M, ALT_PRODUCATOR, "if (false) nejudecat('status-other-manufacturer'", ['K01', 'K02']], ['a signed record of any stranger keeps the verdict from VALID (whether the verifier trusts its signer is not read)', M, ALT_PRODUCATOR, "if (semnat && incredere !== null) nejudecat('status-other-manufacturer'", ['A06', 'H30', 'J05', 'K03', 'K05', 'K06']], ['an unsigned record under the id of a trusted manufacturer keeps the verdict from VALID', M, ALT_PRODUCATOR, "if (incredere !== null && ob(s.by) && incredere.includes(s.by.id)) nejudecat('status-other-manufacturer'", ['S07', 'S08']], ['a suspension is lifted by another signer\'s later record', M, "const v = vederi.get(s.by.id);\n if (!v || s.seq > v.seq) vederi.set(s.by.id,", "const v = vederi.get('x');\n if (!v || s.seq > v.seq) vederi.set('x',", ['C55']], ['a suspension expires with its record', M, "suspendat: s.state === 'suspended', pana: vu", "suspendat: s.state === 'suspended' && vu >= acum, pana: vu", ['C57', 'S27']], ['an expired "active" record is believed', M, '.some((v) => v.pana >= acum);', '.some(() => true);', ['B10', 'H15']], ['the ending of an "active" record is given the tolerance', M, '.some((v) => v.pana >= acum);', '.some((v) => v.pana + sk >= acum);', ['H15']], ['of two records with one number the laxer holds', M, "v.suspendat = v.suspendat || s.state === 'suspended';", "v.suspendat = v.suspendat && s.state === 'suspended';", ['C58', 'H02']], ['the last record in the list holds, not the one with the highest number', M, VEDERE, 'if (!v || s.seq !== v.seq) vederi.set(s.by.id,', ['H01', 'H03']], ['of two records with one number the last in the list holds', M, VEDERE, 'if (!v || s.seq >= v.seq) vederi.set(s.by.id,', ['H02']], ['the record with the lowest number holds (a later record changes nothing)', M, VEDERE, 'if (!v || s.seq < v.seq) vederi.set(s.by.id,', ['A05', 'A11', 'C56', 'G02', 'G03', 'H01', 'H03']], ['a record dated in the future is applied', M, "if (at > acum + sk) { nejudecat('status-future'", "if (false) { nejudecat('status-future'", ['A08', 'A08b']], ['a record dated in the future is skipped in silence', M, "{ nejudecat('status-future', 'status',", "{ void ('status-future', 'status',", ['A08', 'A08b']], ['a record dated just ahead of the verifier\'s clock is given no tolerance', M, "if (at > acum + sk) { nejudecat('status-future'", "if (at > acum) { nejudecat('status-future'", ['G11', 'T16']], ['a retirement whose date cannot be read is dropped', M, 'at = -Infinity; vu = -Infinity;', 'continue;', ['G09']], ['an "active" record whose time cannot be read is not said to be ignored', M, "if (s.state === 'active') { nejudecat('status-ignored', 'status', 'status: an \"active\" record whose time cannot be read'", "if (false) { nejudecat('status-ignored', 'status', 'status: an \"active\" record whose time cannot be read'", ['G10', 'H22']], ['when the owner and the manufacturer both retired it, the first in the list is named (not the one that is final)', M, "if (retras === null || rol === 'manufacturer') retras =", 'if (retras === null) retras =', ['H28']], ['an owner\'s status record is written with no ownership head (the old default)', M, "} else if (ownership == null) throw new Error('aere-device: a status record of anyone but the manufacturer", "} else if (false) throw new Error('aere-device: a status record of anyone but the manufacturer", ['D02']], ['anybody signs a status record as the manufacturer', M, ' || !aceeasi(cine(by), m.statement.issuer)) throw', ') throw', ['D02']], // ---- what the verifier is handed: its shape, and how much of it is judged ['what is handed beyond the bound on how many are judged is dropped in silence', M, 'if (lista.length > max) nejudecat(cauza, link,', 'if (false) nejudecat(cauza, link,', ['I08', 'I11', 'I12', 'I13']], ['no bound on how many of the things handed are judged', M, 'const judecate = lista.slice(0, max), bune = judecate.filter(eBun);', 'const judecate = lista, bune = judecate.filter(eBun);', ['I08', 'I11', 'I12', 'I13']], ['what is handed in another shape (a list inside the list, a registry object, a file of another kind) is dropped in silence', M, 'if (bune.length < judecate.length) nejudecat(cauza, link,', 'if (false) nejudecat(cauza, link,', ['D09', 'I01', 'I02', 'I03', 'I04', 'I05', 'I06', 'I07', 'S26']], // ---- the attestation ['the clone check compares the device id alone (the key half taken out)', M, 'Q.deviceId === S.claims.deviceId && Q.key === S.claims.deviceKey /*PAZA:attestation-device*/', 'Q.deviceId === S.claims.deviceId /*PAZA:attestation-device*/', ['C18']], ['the clone check compares the key alone (the device id half taken out)', M, 'Q.deviceId === S.claims.deviceId && Q.key === S.claims.deviceKey /*PAZA:attestation-device*/', 'Q.key === S.claims.deviceKey /*PAZA:attestation-device*/', ['S14']], // the defect found on 2026-10-05: an attestation dated in the future was accepted up to the allowed age ['an attestation dated in the future is accepted up to the allowed age', M, PRO, 'Math.abs(acum - tq) <= maxAgeS * 1000 /*PAZA:freshness*/', ['F32', 'F34']], ['an attestation dated in the future is accepted, however far', M, PRO, 'acum - tq <= maxAgeS * 1000 /*PAZA:freshness*/', ['C62', 'F32', 'F34']], ['an old attestation is accepted, however old', M, PRO, 'tq <= acum + sk /*PAZA:freshness*/', ['C61', 'H16']], ['an attestation older than the allowed age is given the tolerance', M, PRO, 'tq <= acum + sk && acum - tq <= maxAgeS * 1000 + sk /*PAZA:freshness*/', ['H16']], // without the tolerance an attestation dated ahead is refused by freshness as well: the rows that need such an attestation no longer fail for their rule alone ['an attestation dated ahead is given no tolerance', M, PRO, 'tq <= acum && acum - tq <= maxAgeS * 1000 /*PAZA:freshness*/', ['F05', 'F06', 'F33', 'T13']], ['the sequence the device attests is not compared with the release', M, 'Q.firmware.digest === R.digest && Q.firmware.sequence === R.sequence /*PAZA:attestation-firmware*/', 'Q.firmware.digest === R.digest /*PAZA:attestation-firmware*/', ['F10']], ['the digest the device attests is not compared with the release', M, 'Q.firmware.digest === R.digest && Q.firmware.sequence === R.sequence /*PAZA:attestation-firmware*/', 'Q.firmware.sequence === R.sequence /*PAZA:attestation-firmware*/', ['F11']], ['a hardware root in the attestation passes in silence', M, "if (q.hardwareRoot != null) nejudecat('hardware-root'", "if (false) nejudecat('hardware-root'", ['B17']], // ---- the witness ['the envelope is not bound to this attestation (its hash)', M, ' && E.statement.attestationHash === attestationHash(X)', '', ['C69', 'D08']], ['the envelope is not bound to this device (its id)', M, '(E.statement.deviceId === Q.deviceId && E.statement.attestationHash === attestationHash(X))', '(E.statement.attestationHash === attestationHash(X))', ['F29']], ['the envelope is not required to hash to its statementHash', M, "&& hex0x(sha(Buffer.from(JSON.stringify(E.statement), 'utf8'))) === E.statementHash && (Q === null", '&& (Q === null', ['C70']], ['an envelope of another kind is taken for the envelope of a device attestation', M, "E.kind === 'aere-proof-of-device-attestation' && ", '', ['H25']], ['an envelope whose statement is of another kind is taken for one of a device', M, " && E.statement.kind === 'aere-proof-of-device'", '', ['H26']], ['a claim of notarization passes for a reading', M, "if (E.notarization != null && !pentruEl.length) nejudecat('witness-unread'", "if (false) nejudecat('witness-unread'", ['C66', 'D08']], ['a reading of another envelope is taken for this one', M, 'AN.filter((a) => a.statementHash === E.statementHash)', 'AN.filter(() => true)', ['C71', 'D08']], ['a reading whose time is in milliseconds is taken for one in seconds', M, '&& a.at > 0 && a.at < 1e11)', '&& a.at > 0)', ['C71b', 'S28', 'T19']], ['a reading whose time is not a whole number is used', M, 'citiri = pentruEl.filter((a) => Number.isInteger(a.at) && a.at > 0 && a.at < 1e11)', 'citiri = pentruEl.filter((a) => a.at > 0 && a.at < 1e11)', ['H27', 'T19']], ['a reading that cannot be read passes in silence', M, "if (pentruEl.length > citiri.length) nejudecat('witness-unread'", "if (false) nejudecat('witness-unread'", ['C71b', 'H27', 'S28', 'T19']], ['of two readings the latest is the bound', M, 'citiri.reduce((x, y) => (y.at < x.at ? y : x))', 'citiri.reduce((x, y) => (y.at > x.at ? y : x))', ['H23', 'H24']], // ---- the bundle, the verdict, the verifier's configuration, the key files ['a bundle of another version is read', M, '&& b.v === VERSION && (b.transfers === undefined', '&& (b.transfers === undefined', ['F30']], ['transfers that are not a list are read', M, ' && (b.transfers === undefined || Array.isArray(b.transfers))) /*PAZA:form*/', ') /*PAZA:form*/', ['F31']], ['what was not brought or read does not keep the verdict from VALID', M, 'export const PARTIALE = NEJUDECATE.filter((c) => !NOTATE.includes(c));', 'export const PARTIALE = [];', partiale], ['the subject is returned also when a rule refused', M, 'subject: rules.length ? null : subject };', 'subject };', cuSubiect], ['a link with a refused rule is reported PASSED', M, "a.some((r) => r.pass === false) ? 'FAILED' :", "a.some((r) => r.pass === false) ? 'PASSED' :", ['A09']], ['the verifier takes a clock tolerance however large', M, 'if (!Number.isInteger(clockSkewS) || clockSkewS < 0 || clockSkewS > 600) throw', 'if (!Number.isInteger(clockSkewS) || clockSkewS < 0) throw', ['C76', 'T24']], ['a trusted manufacturer that is neither an id nor keys is taken as it is', M, "if (!AERE_ID.test(String(id))) throw new Error('verifyDevice: a trusted manufacturer", "if (false) throw new Error('verifyDevice: a trusted manufacturer", ['T24']], ['a key file with somebody else\'s public half is accepted', M, 'if (d.publicKey !== j.publicKey || d.deviceId !== j.deviceId) throw', 'if (false) throw', ['D01']], ['the private half of a device key is enumerable', M, "Object.defineProperty(d, 'privat', { value: priv, enumerable: false });", "Object.defineProperty(d, 'privat', { value: priv, enumerable: true });", ['D01']], // ---- text made visible ['visible(): a backslash is not doubled (a visible form can be forged)', M, 'if (n === 0x5c) out +=', 'if (false) out +=', ['V01']], ['visible(): the C1 control characters are sent as they are', M, '[0x7f, 0x9f]', '[0x7f, 0x7f]', ['D10', 'V01', 'W13', 'D10b']], ['visible(): the line and paragraph separators are sent as they are', M, '[0x2028, 0x202e]', '[0x202a, 0x202e]', ['D10', 'V01', 'W13', 'D10b']], // 2026-10-14 (third review): U+061C ARABIC LETTER MARK has the Unicode property Bidi_Control and was printed as it came ['visible(): the arabic letter mark is sent as it is', M, '[0x061c, 0x061c], ', '', ['D10', 'V01', 'W13', 'D10b']], // ---- the command line ['the command line exits 0 whatever the verdict', C, "return r.verdict === 'VALID' ? 0 : r.verdict === 'INVALID' ? 1 : 2;", 'return 0;', ['D05', 'D07', 'D09', 'D10']], ['the command line does not say what is named beside the verdict', C, 'if (notate.length) spune(', 'if (false) spune(', ['D07']], ['the command line does not say what the records of a previous owner say', C, 'for (const p of (r.subject && r.subject.priorOwnership) || []) spune(', 'for (const p of []) spune(', ['D07']], ['the command line hands a file that holds a list as ONE thing (it is not read element by element)', C, LISTE_CLI, "o.statusLists = toate('--status-list').map(citeste); o.firmwarePolicies = toate('--policy').map(citeste); o.statusRecords = toate('--status').map(citeste); o.anchors = toate('--reading').map(citeste);", ['D09']], ['the command line does not open a registry object { records: [...] }', C, " : x && typeof x === 'object' && Array.isArray(x.records) && x.statement === undefined ? netezeste(x.records, adancime + 1) : [x]);", ' : [x]);', ['D09']], ['the command line prints text from a bundle as it came (control characters reach the terminal)', C, 'const spune = (text) => { console.log(D.visible(text)); };', 'const spune = (text) => { console.log(text); };', ['D10']], ['the command line passes its JSON through visible() (it is no longer the bundle\'s text)', C, "if (rest.includes('--json')) console.log(D.visibleJson(r, 1));", "if (rest.includes('--json')) spune(D.visibleJson(r, 1));", ['D05', 'D07', 'D09', 'D10b']], // 2026-10-14 (third review): JSON.stringify escapes C0 only; DEL, C1, the marks of direction and the line separators reached the terminal ['the command line prints its JSON as JSON.stringify writes it', C, "if (rest.includes('--json')) console.log(D.visibleJson(r, 1));", "if (rest.includes('--json')) console.log(JSON.stringify(r, null, 1));", ['D10b']], ['a key file is written over a file that exists (the key it held is lost, and the file keeps its own mode)', C, "secret ? { mode: 0o600, flag: 'wx' } : {}", 'secret ? { mode: 0o600 } : {}', ['D12']], ['a trusted manufacturer file that holds no keys exits as an unexpected failure', C, 'catch (e) { throw new Folosire(`${f} holds no public keys', 'catch (e) { throw new Error(`${f} holds no public keys', ['D11']], ['an input that cannot be read exits with the code of a PARTIAL verdict', C, 'const COD_FOLOSIRE = 3, COD_CADERE = 4;', 'const COD_FOLOSIRE = 2, COD_CADERE = 4;', ['D11', 'D12']], ['a clock that is not a time exits as an unexpected failure, not as an input that cannot be read', C, 'if (/^verifyDevice: /.test(String(e && e.message))) throw new Folosire(e.message);', 'if (false) throw new Folosire(e.message);', ['D11']], ];