// AERE Device Operation (roadmap 26, 2026-10-20): what a machine with an identity (../aere-device-identity) says about its own
// operation over time, in a form a stranger judges without trusting the machine. Node 24 only (node:crypto: ML-DSA-65, FIPS 204).
//
// THE LOG. The device signs, at intervals, an operation record with its device key K (ML-DSA-65, the key the manufacturer certified):
//   seq          its position in the log (0, 1, 2, ... across key rotations)
//   prev         the hash of the record before it; record 0 names the hash of the manufacture credential of the first key, so the log is
//                rooted in one identity and cannot be shown under another credential of the same key
//   at           the device's clock (its word, unless a witness bounds it: below)
//   state        operating | idle | fault | maintenance
//   counter      a number the device keeps and never lowers (cycles, energy, distance, seconds of operation)
//   measurement  the sha256 of what it measured, or null: the data stays with the device or its owner, only the digest is signed
//   after        a block the device read before signing ({ chainId, block, hash }), or null: a block hash cannot be known before the block
//                exists, so with the verifier's own reading of that block the record cannot be older than the block (a lower bound)
//   next         a rotation ({ deviceId, key }), or null: from the next record on the log is signed by that key, which a manufacture
//                credential of the same manufacturer, for the same model and serial, must certify (the old key consents by signing the
//                rotation, the manufacturer by certifying the new key)
// A record is exactly { statement, signature }; the signature is ML-DSA-65 with K over a domain of its own ('aere-device-operation/v1/
// record'), so it verifies as nothing else the device signs (its attestations use 'aere-device/v1/attestation').
//
// THE WITNESS. An anchor is an AIP-23 envelope of the existing kind `time` whose subjectHash is the hash of a record: notarized, and read
// back by the VERIFIER through the AIP-23 reference verifier under a post-quantum certified anchor, it says that record (and every record
// before it, which it names through `prev`) already existed at the moment the chain wrote. That is an upper bound on time; `after` gives a
// lower bound. Without either, the time of a record is the device's word, and the verdict says so.
//
// THE VERDICT. verifyOperation makes every check of each record it reaches and names every rule that refused (REGULI; each check carries
// a PAZA marker). It does not turn a failure of its own into a refusal: an exception is a defect of the verifier, and it is thrown. The log is accepted up to the first record that a rule refuses; what comes after is not judged, and counted. INVALID: a
// rule refused. PARTIAL: nothing refused, and something was not brought or not read (the manufacturers the verifier trusts, the recall
// list, the manufacturer's registry, a notarization nobody read, records beyond the log shown). VALID: everything brought was judged.
// The identity of each key is judged by the device verifier (../aere-device-identity/device.mjs), not again here.
//
// WHAT IT DOES NOT SAY. That the machine did the physical work its records describe: a record is what the holder of K signed, and K is a
// software key (nothing here binds it to a chip). A copied K signs records as well as the device. See README.md.
import crypto from 'node:crypto';
import { canonical, idOf, credentialHash } from '../identity/identity.mjs';
import * as D from '../device-identity/device.mjs';
import { buildProof } from '../proof-kinds/proof-kinds.mjs';

export const VERSION = 1;
export const ALG = 'ml-dsa-65';
export const RECORD_KIND = 'aere-device-operation';
export const LOG_KIND = 'aere-device-operation-log';
export const EQUIVOCATION_KIND = 'aere-device-operation-equivocation';
export const FACTS_KIND = 'aere-device-operation-facts';
export const ANCHOR_KIND = 'aere-proof-of-time';   // the AIP-23 kind `time` of ../proof-kinds
/** The kind of a block reading as the `block` command writes it (operation-cli.mjs): the one place its form is named. */
export const BLOCK_READING_KIND = 'aere-device-operation-block-reading';
export const STATES = ['operating', 'idle', 'fault', 'maintenance'];
export const CLOCK_SKEW_S = 60;
// How much of what the log carries and what the verifier hands is judged. Beyond the bound the rest is NOT read, and the verdict says so.
export const MAX_KEYS = 16, MAX_RECORDS = 100000, MAX_ANCHORS = 4096, MAX_READINGS = 4096, MAX_BEACONS = 100000, MAX_OTHER = 4096, MAX_STATUS_RECORDS = 512;
const DOMENIU = 'aere-device-operation/v1/record\n';
const H32 = /^0x[0-9a-f]{64}$/;
const DEV = /^aere-device:[0-9a-f]{40}$/;
const AERE_ID = /^aere-id:[0-9a-f]{40}$/;
// the device id a status record names, read as the device verifier reads it (../aere-device-identity/device.mjs, idScris): its hex without
// regard to case; null when what is written there is not a device id at all (a space after it, another form)
const DEV_SCRIS = /^aere-device:([0-9a-fA-F]{40})$/;
const idScris = (x) => { const m = typeof x === 'string' ? DEV_SCRIS.exec(x) : null; return m ? 'aere-device:' + m[1].toLowerCase() : null; };
const DATA = /^\d{4}-\d{2}-\d{2}T\d{2}:\d{2}:\d{2}(\.\d{1,3})?Z$/;
const CAMPURI = ['v', 'kind', 'deviceId', 'seq', 'prev', 'at', 'state', 'counter', 'measurement', 'after', 'next'];

const sha = (b) => crypto.createHash('sha256').update(b).digest();
const hex0x = (b) => '0x' + b.toString('hex');
const ob = (x) => !!x && typeof x === 'object' && !Array.isArray(x);
const iso = (d) => new Date(d).toISOString();
const numai = (o, chei) => ob(o) && Object.keys(o).every((k) => chei.includes(k));
const toate = (o, chei) => ob(o) && chei.every((k) => k in o) && numai(o, chei);
const b64canonic = (s) => typeof s === 'string' && s.length > 0 && Buffer.from(s, 'base64').toString('base64') === s;
const intreg = (x, min = 0) => Number.isSafeInteger(x) && x >= min;
/** The day a text of the form of DATA names exists (a date parser MOVES 2026-02-30 to March 2): the same rule as the device verifier's. */
const exista = (s) => new Date(Date.parse(s)).getUTCDate() === Number(String(s).slice(8, 10));
const eTimp = (s) => typeof s === 'string' && DATA.test(s) && exista(s);
function data(s, ce) { if (!eTimp(s)) throw new Error(`aere-device-operation: ${ce} is not an RFC 3339 UTC time`); return Date.parse(s); }
const aceeasi = (a, b) => ob(a) && ob(b) && a.id === b.id && canonical(a.keys) === canonical(b.keys);
const idDin = (keys) => { try { return idOf(keys); } catch { return NaN; } };
const cheieObiect = (b64) => crypto.createPublicKey({ key: Buffer.from(b64, 'base64'), format: 'der', type: 'spki' });
const mesaj = (statement) => Buffer.from(DOMENIU + canonical(statement), 'utf8');
/** The device's signature over a record statement (the published formula): ML-DSA-65 with K over the domain of operation records. */
export function signRecord(statement, device) {
  if (!device || !device.privat) throw new Error('aere-device-operation: signing needs the device private key');
  return { alg: ALG, value: crypto.sign(null, mesaj(statement), device.privat).toString('base64') };
}

/** The hash of a record ({ statement, signature }): what the record after it names in `prev`. */
export const recordHash = (r) => D.linkHash(r);
/** A measurement as the record carries it: a digest (kept, lower case) or bytes (hashed). Nothing else: the record carries no raw data. */
export function measurementDigest(m) {
  if (m == null) return null;
  if (typeof m === 'string' && /^0x[0-9a-fA-F]{64}$/.test(m)) return m.toLowerCase();
  if (Buffer.isBuffer(m) || m instanceof Uint8Array) return hex0x(sha(Buffer.from(m)));
  throw new Error('aere-device-operation: a measurement is a digest (0x and 64 hex digits) or bytes');
}

// ---------------------------------------------------------------- producers
/** A new log, rooted in the manufacture credential of the device's first key. */
export function newLog({ manufacture }) {
  if (!ob(manufacture) || !ob(manufacture.statement) || !ob(manufacture.statement.claims) || !DEV.test(String(manufacture.statement.claims.deviceId))) throw new Error('aere-device-operation: a log starts from a manufacture credential of the device');
  const radacina = [manufacture];   // the credential of the first key: the root of the log
  return { v: VERSION, kind: LOG_KIND, credentials: radacina, records: [], anchors: [] };
}
/** The device id that signs the next record of a log: the first key, then the key each rotation names. */
export function keyInForce(log) {
  let k = log.credentials[0].statement.claims.deviceId;
  for (const r of log.records) if (r.statement.next) k = r.statement.next.deviceId;
  return k;
}
/**
 * The next operation record of a log, signed with the device key. `after`: { chainId, block, hash } of a block the device read; `next`:
 * the public half of the device key that signs from the following record on ({ deviceId, publicKey }).
 */
export function operationRecord({ device, log, state, counter, measurement = null, after = null, next = null, now = new Date() }) {
  if (!device || !device.privat) throw new Error('aere-device-operation: a record needs the device private key');
  if (!ob(log) || log.kind !== LOG_KIND || !Array.isArray(log.records)) throw new Error('aere-device-operation: not an operation log');
  if (device.deviceId !== keyInForce(log)) throw new Error(`aere-device-operation: the key that signs this log now is ${keyInForce(log)}, not ${device.deviceId}`);
  if (!STATES.includes(state)) throw new Error('aere-device-operation: state is one of ' + STATES.join(', '));
  if (!intreg(counter)) throw new Error('aere-device-operation: counter is a whole number from 0 up');
  const ultim = log.records.length ? log.records[log.records.length - 1].statement : null;
  const at = iso(now);
  if (ultim && Date.parse(at) < Date.parse(ultim.at)) throw new Error('aere-device-operation: the time of a record does not go back');
  if (ultim && counter < ultim.counter) throw new Error('aere-device-operation: the counter does not go down');
  if (after !== null && !(toate(after, ['chainId', 'block', 'hash']) && intreg(after.chainId, 1) && intreg(after.block) && H32.test(String(after.hash).toLowerCase()))) throw new Error('aere-device-operation: after is { chainId, block, hash } of a block the device read');
  let nx = null;
  if (next !== null) { if (!next || D.deviceIdOf(next.publicKey) !== next.deviceId || next.deviceId === device.deviceId) throw new Error('aere-device-operation: next is the public half of another device key'); nx = { deviceId: next.deviceId, key: next.publicKey }; }
  const statement = { v: VERSION, kind: RECORD_KIND, deviceId: device.deviceId, seq: log.records.length,
    prev: log.records.length ? recordHash(log.records[log.records.length - 1]) : credentialHash(log.credentials[0]),
    at, state, counter, measurement: measurementDigest(measurement), after: after === null ? null : { chainId: after.chainId, block: after.block, hash: String(after.hash).toLowerCase() }, next: nx };
  return { statement, signature: signRecord(statement, device) };
}
/** The log with one record more (and, for a rotation, the manufacture credential of the new key). Pure: the log given is not changed. */
export function append(log, record, credential = null) {
  return { ...log, credentials: credential ? [...log.credentials, credential] : log.credentials, records: [...log.records, record] };
}
/** The AIP-23 envelope (kind `time`) that commits to a record by hash: notarize it, and a verifier's reading of it bounds the time from above. */
export function anchorEnvelope(record) {
  const s = record.statement;
  return buildProof('time', { subjectHash: recordHash(record), source: s.deviceId, at: s.at, createdAt: s.at });
}
/** The log with an anchor envelope more (as notarized, with its `notarization`, or not yet). */
export const addAnchor = (log, envelope) => ({ ...log, anchors: [...(log.anchors || []), envelope] });

// ---------------------------------------------------------------- one record: its form and its signature
/**
 * The form of a record, as this verifier reads it. Its time is from 1970: the facts carry every time as milliseconds since 1970 (the
 * reputation reads no other), so a record dated before it would be accepted here and its facts refused by the formula.
 */
export function wellFormed(r) {
  if (!(toate(r, ['statement', 'signature']) && toate(r.statement, CAMPURI))) return false;
  const s = r.statement, a = s.after, n = s.next;
  return s.v === VERSION && s.kind === RECORD_KIND && typeof s.deviceId === 'string' && DEV.test(s.deviceId) && intreg(s.seq) && typeof s.prev === 'string' && H32.test(s.prev)
    && eTimp(s.at) && !(Date.parse(s.at) < 0) && STATES.includes(s.state) && intreg(s.counter) && (s.measurement === null || (typeof s.measurement === 'string' && H32.test(s.measurement)))
    && (a === null || (toate(a, ['chainId', 'block', 'hash']) && intreg(a.chainId, 1) && intreg(a.block) && typeof a.hash === 'string' && H32.test(a.hash)))
    && (n === null || (toate(n, ['deviceId', 'key']) && typeof n.deviceId === 'string' && typeof n.key === 'string'));
}
/** Is the record signed with this device key (a canonical ML-DSA-65 SPKI in base64), exactly { alg, value }, in canonical base64? */
export function signedBy(r, keyB64) {
  try {
    const k = cheieObiect(keyB64);
    return toate(r.signature, ['alg', 'value']) && r.signature.alg === ALG && b64canonic(r.signature.value) && crypto.verify(null, mesaj(r.statement), k, Buffer.from(r.signature.value, 'base64'));
  } catch { return false; }
}

// ---------------------------------------------------------------- equivocation: two records of one key for one position
/** The proof that one device key signed two different records for the same position. `key`: the device key (SPKI, base64). */
export const equivocationProof = (a, b, key) => ({ v: VERSION, kind: EQUIVOCATION_KIND, seq: a.statement.seq, key, a, b });
/** Checks a proof of equivocation with nothing but what it carries: both records well formed, of the device the key derives, at one position, different, both signed. */
export function verifyEquivocation(p) {
  if (!toate(p, ['v', 'kind', 'seq', 'key', 'a', 'b']) || p.v !== VERSION || p.kind !== EQUIVOCATION_KIND || !intreg(p.seq)) return { ok: false, error: 'not an ' + EQUIVOCATION_KIND };
  let id = null; try { id = D.deviceIdOf(p.key); } catch { return { ok: false, error: 'the key is not a canonical ML-DSA-65 public key' }; }
  for (const r of [p.a, p.b]) {
    if (!wellFormed(r)) return { ok: false, error: 'a record is not a well formed operation record' };
    if (r.statement.deviceId !== id || r.statement.seq !== p.seq) return { ok: false, error: 'the two records are not of the device the key derives, at the position named' };
    if (!signedBy(r, p.key)) return { ok: false, error: 'a record is not signed with the key' };
  }
  if (recordHash(p.a) === recordHash(p.b)) return { ok: false, error: 'the two records are the same' };
  return { ok: true, deviceId: id, seq: p.seq };
}

// ---------------------------------------------------------------- the verifier
export const REGULI = ['form', 'identity', 'record-form', 'record-key', 'record-signature', 'record-seq', 'record-prev', 'record-time', 'record-counter',
  'key-window', 'key-retired', 'rotation', 'anchor-envelope', 'witness-time', 'beacon-hash', 'beacon-time', 'equivocation'];
export const NEJUDECATE = ['manufacturer-trust', 'manufacture-status-unread', 'manufacture-status-none', 'hardware-root', 'status-unread', 'status-other-manufacturer', 'status-future', 'records-missing', 'records-unread',
  'records-beyond', 'retired-unwitnessed', 'witness-unread', 'beacon-unread', 'time-unwitnessed', 'other-ignored', 'rotated-key-used', 'retired-key-used', 'after-refusal'];
/**
 * The causes that are NAMED and do not keep the verdict from VALID: a credential with no recall list; a retirement dated in the verifier's
 * future (not in effect yet); a block named by a record that the verifier did not read (no lower bound from it); records whose time no
 * witness bounds (the device's word); records handed beside the log that are not records of its keys; a record signed by a key after
 * the log rotated away from it (somebody still holds and uses the old key: said, since the log itself does not depend on it); a record
 * handed beside the log that is signed by a key the manufacturer retired (whoever copied the key may have signed it after the retirement:
 * it proves nothing against the device, which is what the retirement is for); records after a refused one (the verdict is INVALID already).
 */
export const NOTATE = ['manufacture-status-none', 'status-future', 'beacon-unread', 'time-unwitnessed', 'other-ignored', 'rotated-key-used', 'retired-key-used', 'after-refusal'];
export const PARTIALE = NEJUDECATE.filter((c) => !NOTATE.includes(c));
export const OPRIRI = ['form', 'record-form'];
// the causes of the device verifier's manufacture link, carried over under the same names
const CAUZE_IDENTITATE = ['manufacturer-trust', 'manufacture-status-unread', 'manufacture-status-none', 'hardware-root'];
class Nedeclarata extends Error {}

/**
 * Verifies an operation log with what the VERIFIER brings: its clock, the manufacturers it trusts, the manufacturer's recall lists and
 * status records it read (`statusRecords`: null when it read none, a list, empty included, when it did), its own readings of the notarized
 * anchors ({ statementHash, at: unix seconds, chainId }), its own readings of blocks ({ chainId, block, hash, at: unix seconds }), and
 * records of this machine it holds from elsewhere (`otherRecords`: a sibling signed by the same key for a position of the log is an
 * equivocation). Returns { verdict, valid, rows, rules, unjudged, accepted, counted, equivocations, facts }.
 */
export function verifyOperation(L, { now = new Date(), clockSkewS = CLOCK_SKEW_S, trustedManufacturers = null, statusLists = [], statusRecords = null, readings = [], beacons = [], otherRecords = [] } = {}) {
  const rows = [];
  const ok = (rule, scope, name, pass, detail = '') => { if (!REGULI.includes(rule)) throw new Nedeclarata('aere-device-operation: undeclared rule ' + rule); rows.push({ scope, name, pass: !!pass, detail: pass ? '' : detail, rule }); return !!pass; };
  const nejudecat = (cauza, scope, name, detail) => { if (!NEJUDECATE.includes(cauza)) throw new Nedeclarata('aere-device-operation: undeclared cause ' + cauza); rows.push({ scope, name, pass: null, detail, unjudged: cauza }); };
  // the verifier's own configuration first: a mistake of the verifier is not an invalid log
  const acum = now instanceof Date ? now.getTime() : typeof now === 'number' ? now : eTimp(now) ? Date.parse(now) : NaN;
  if (!Number.isFinite(acum)) throw new Error('verifyOperation: now is not a time (a Date, milliseconds since 1970, or an RFC 3339 UTC text)');
  if (!Number.isInteger(clockSkewS) || clockSkewS < 0 || clockSkewS > 600) throw new Error('verifyOperation: clockSkewS is 0..600 seconds');
  if (trustedManufacturers != null && !Array.isArray(trustedManufacturers)) throw new Error('verifyOperation: trustedManufacturers is a list of ids or public keys');
  if (![statusLists, readings, beacons, otherRecords].every(Array.isArray) || !(statusRecords === null || Array.isArray(statusRecords))) throw new Error('verifyOperation: statusLists, readings, beacons and otherRecords are lists; statusRecords is a list or null (not read)');
  try { D.verifyDevice({}, { now: acum, clockSkewS, trustedManufacturers, statusLists }); } catch (e) { throw new Error('verifyOperation: ' + String(e.message).replace(/^verifyDevice: /, '')); }
  // the ids of the manufacturers the verifier trusts (the device verifier above refused anything else): a status record of one of them about
  // a key of this log that is not the key's own manufacturer is named, as the device verifier names it
  const incredere = trustedManufacturers == null ? null : trustedManufacturers.map((x) => (typeof x === 'string' ? x : idDin(x)));
  const sk = clockSkewS * 1000;
  let accepted = [], counted = [], equivocations = [], chei = [], recs = [], toateInreg = 0, numarate = null, lanturi = { anchors: new Set(), beacons: new Set() };
  // the facts are always of the form the reputation reads (reputation.mjs, factsForm): the manufacturer is an aere-id or null (a credential
  // the device verifier refused may carry any text there), and `uncounted` is every record of the log not counted, the ones beyond the
  // bound of what is judged included
  const facts = () => ({ v: VERSION, kind: FACTS_KIND, verdict: null, rules: [], unjudged: [], manufacturer: chei.length && chei[0].S && AERE_ID.test(String(chei[0].S.issuer.id)) ? chei[0].S.issuer.id : null,
    keys: [...new Set(accepted.map((x) => x.deviceId))],
    records: (numarate || counted).map((x) => ({ seq: x.seq, hash: x.hash, at: x.at, lo: x.lo, hi: x.hi, state: x.state, counter: x.counter })),
    uncounted: toateInreg - (numarate || counted).length,
    equivocations: equivocations.map((p) => ({ seq: p.seq, a: recordHash(p.a), b: recordHash(p.b) })).sort((x, y) => x.seq - y.seq || (x.a < y.a ? -1 : x.a > y.a ? 1 : x.b < y.b ? -1 : x.b > y.b ? 1 : 0)),
    retirements: chei.filter((k) => k.S && k.retras !== null).map((k) => ({ deviceId: k.S.deviceId, at: Number.isFinite(k.retras) ? k.retras : null })),
    chains: { anchors: [...lanturi.anchors].sort((x, y) => x - y), beacons: [...lanturi.beacons].sort((x, y) => x - y) } });
  const gata = () => {
    const rules = [...new Set(rows.filter((r) => r.pass === false).map((r) => r.rule))].sort(), unjudged = [...new Set(rows.filter((r) => r.pass === null).map((r) => r.unjudged))].sort();
    const verdict = rules.length ? 'INVALID' : unjudged.some((c) => PARTIALE.includes(c)) ? 'PARTIAL' : 'VALID';
    const f = facts(); f.verdict = verdict; f.rules = rules; f.unjudged = unjudged;
    return { verdict, valid: !rules.length, rows, rules, unjudged, accepted: accepted.length, counted: (numarate || counted).length, equivocations, facts: f };
  };
  {
    if (!((ob(L) && L.kind === LOG_KIND && L.v === VERSION && Array.isArray(L.credentials) && L.credentials.length >= 1 && L.credentials.length <= MAX_KEYS && L.credentials.every(ob)
      && Array.isArray(L.records) && (L.anchors === undefined || Array.isArray(L.anchors)) && numai(L, ['v', 'kind', 'credentials', 'records', 'anchors'])) /*PAZA:form*/)) { ok('form', 'log', 'log: well formed', false, `not an ${LOG_KIND} with 1 to ${MAX_KEYS} manufacture credentials, a list of records and a list of anchors`); return gata(); }

    // ---- what the verifier handed: bounded, and nothing in it is skipped in silence (the device verifier's rule, here too)
    const adus = (lista, max, cauza, scope, ce, eBun) => {
      if (lista.length > max) nejudecat(cauza, scope, `${scope}: more ${ce}s than are judged`, `${lista.length} ${ce}s were handed and the first ${max} are judged: the others were not read`);
      const judecate = lista.slice(0, max), bune = judecate.filter(eBun);
      if (bune.length < judecate.length) nejudecat(cauza, scope, `${scope}: something handed as a ${ce} is not one`, `${judecate.length - bune.length} of the ${judecate.length} element(s) handed as ${ce}s are not ${ce}s: nothing in them was read`);
      return bune;
    };
    const SR = statusRecords === null ? null : adus(statusRecords, MAX_STATUS_RECORDS, 'status-unread', 'status', 'status record', (x) => ob(x) && ob(x.statement) && x.statement.kind === 'aere-device-status');
    const AN = adus(readings, MAX_READINGS, 'witness-unread', 'witness', 'reading', (x) => ob(x) && typeof x.statementHash === 'string');
    // a block reading is { chainId, block, hash, at }, and may carry the v and kind the `block` command writes beside them (and nothing else)
    const BK = adus(beacons, MAX_BEACONS, 'beacon-unread', 'beacon', 'block reading', (x) => ob(x) && ['chainId', 'block', 'hash', 'at'].every((k) => k in x) && numai(x, ['v', 'kind', 'chainId', 'block', 'hash', 'at'])
      && (!('v' in x) || x.v === 1) && (!('kind' in x) || x.kind === BLOCK_READING_KIND) && intreg(x.chainId, 1) && intreg(x.block) && typeof x.hash === 'string' && H32.test(x.hash) && intreg(x.at, 1) && x.at < 1e11);
    const OT = adus(otherRecords, MAX_OTHER, 'other-ignored', 'equivocation', 'record', (x) => ob(x));

    // ---- 1. identity: each manufacture credential, judged by the device verifier. The window of a credential is judged at the time of
    // each record (below), not on the verifier's clock: a log signed while the credential was valid stays a log of that time.
    chei = L.credentials.map((M, i) => {
      const r = D.verifyDevice({ v: 1, kind: 'aere-device-bundle', manufacture: M, transfers: [] }, { now: acum, clockSkewS, trustedManufacturers, statusLists });
      const refuzate = r.rows.filter((x) => (x.link === 'manufacture' || x.link === 'bundle') && x.pass === false && x.rule !== 'manufacture-window');
      const bun = ok('identity', 'identity', `key ${i + 1}/${L.credentials.length}: the manufacture credential, judged by the device verifier`, refuzate.length === 0 /*PAZA:identity*/,
        refuzate.map((x) => `device.${x.rule}: ${x.detail}`).join('; ').slice(0, 600));
      for (const c of CAUZE_IDENTITATE) { const x = r.rows.find((y) => y.link === 'manufacture' && y.unjudged === c); if (x) nejudecat(c, 'identity', `key ${i + 1}: ${x.name}`, x.detail); }
      let S = null;
      if (!r.rows.some((x) => x.rule === 'manufacture-form' || x.rule === 'unreadable')) {
        const s = M.statement;
        S = { deviceId: s.claims.deviceId, key: s.claims.deviceKey, model: s.claims.model, serial: s.claims.serial, issuer: s.issuer, vf: data(s.validFrom, 'validFrom'), vu: data(s.validUntil, 'validUntil') };
      }
      return { bun, S, retras: null };
    });

    // ---- 2. the manufacturer's registry: a retirement of a key, with its time. A record counts when it names the key's device id, says
    // `retired` and is signed by the manufacturer of that key's credential. Its time is the manufacturer's word (a status record carries the
    // date its signer chose); a record dated in the verifier's future is not in effect yet. One the manufacturer signed and this verifier
    // cannot read may be a retirement: the registry is not read as clean. Which key a record is about, and what is done with one this
    // verifier does not apply, is read as the device verifier reads it (../aere-device-identity, its status link): a record that names
    // another device is passed over; one of the key's manufacturer whose device id is not a device id at all may be meant for this key; and
    // a retirement by ANOTHER manufacturer the verifier trusts is not applied (a manufacturer does not retire the keys of another) and not
    // passed over (the same key may carry that manufacturer's credential too): both leave the registry not read as clean.
    if (SR === null) nejudecat('status-unread', 'status', 'status: the manufacturer\'s registry', 'not read (statusRecords was not given): a retirement of a key cannot be seen');
    else for (const k of chei) {
      if (!k.S) continue;
      for (const x of SR) {
        const s = x.statement, idR = idScris(s.deviceId);
        if (idR !== null && idR !== k.S.deviceId) continue;   // about another device
        let semnat = false; try { semnat = aceeasi(s.by, k.S.issuer) && idDin(s.by.keys) === s.by.id && D.verifyLink('status', s, x.signature, k.S.issuer.keys); } catch { semnat = false; }
        if (!semnat) {   // not this key's manufacturer: applied by nobody here, and named when a manufacturer the verifier trusts retires the key
          let deAltul = false;
          if (incredere !== null && ob(s.by) && incredere.includes(s.by.id) && !(s.v === 1 && D.STATES.includes(s.state) && s.state !== 'retired')) { try { deAltul = idDin(s.by.keys) === s.by.id && D.verifyLink('status', s, x.signature, s.by.keys); } catch { deAltul = false; } }
          if (deAltul) nejudecat('status-other-manufacturer', 'status', `status: a record of another trusted manufacturer (${k.S.deviceId})`, `${s.by.id}, a manufacturer the verifier trusts and not the one of this key's credential, signed a retirement of this key or a record this verifier cannot read: not applied, and not judged (the same key may carry that manufacturer's credential too)`);
          continue;
        }
        if (idR === null) { nejudecat('status-unread', 'status', `status: a record of the manufacturer whose device id cannot be read (${k.S.deviceId})`, 'a record signed by the manufacturer of this key names a device id that is not a device id: it may be meant for this key, so the registry is not read as clean'); continue; }
        if (!(s.v === 1 && D.STATES.includes(s.state))) { nejudecat('status-unread', 'status', `status: a record of the manufacturer that cannot be read (${k.S.deviceId})`, 'a record signed by the manufacturer for this key is of a version or a state this verifier does not read: it may be a retirement'); continue; }
        if (s.state !== 'retired') continue;   // a suspension concerns what the device may do, not what it signed (README)
        // a retirement whose date cannot be read holds from the start; so does one dated before 1970, before any record can be dated (the
        // facts carry times from 1970 only)
        let t = -Infinity; try { t = data(s.at, 'status at'); } catch { t = -Infinity; }
        if (t < 0) t = -Infinity;
        if (t > acum + sk) { nejudecat('status-future', 'status', `status: a retirement dated in the verifier's future (${k.S.deviceId})`, `dated ${s.at}: not in effect yet`); continue; }
        if (k.retras === null || t < k.retras) k.retras = t;
      }
    }

    // ---- 3. the records, their hashes, and what the log and the verifier say about them
    recs = L.records.slice(0, MAX_RECORDS); toateInreg = L.records.length;
    if (L.records.length > MAX_RECORDS) nejudecat('records-unread', 'log', 'log: more records than are judged', `${L.records.length} records, the first ${MAX_RECORDS} are judged: the others were not read`);
    if (!recs.length) nejudecat('records-missing', 'log', 'log: records', 'the log carries no operation record: nothing here says anything about the machine\'s operation');
    const hashes = recs.map((r) => { try { return recordHash(r); } catch { return null; } });
    // indexes, so that the work stays linear in what is judged (a lookup per record or per anchor over everything handed would not)
    const pozitie = new Map(); hashes.forEach((h, i) => { if (h !== null && !pozitie.has(h)) pozitie.set(h, i); });
    const grupa = (lista, cheie) => { const m = new Map(); for (const x of lista) { const c = cheie(x); const l = m.get(c); if (l) l.push(x); else m.set(c, [x]); } return m; };
    const citiriDe = grupa(AN, (x) => x.statementHash), blocuri = grupa(BK, (x) => x.chainId + ':' + x.block);
    const cheieDe = (id) => chei.find((k) => k.bun && k.S && k.S.deviceId === id) || null;

    // the anchors the log carries, and the verifier's readings of them: the earliest reading of the earliest anchor of a record bounds it
    const ancore = new Map();   // record index -> { at (ms), chainId }
    for (const [n, E] of (L.anchors || []).slice(0, MAX_ANCHORS).entries()) {
      let j = -1, plic = false;
      try { plic = ob(E) && E.v === 1 && E.kind === ANCHOR_KIND + '-attestation' && ob(E.statement) && E.statement.v === 1 && E.statement.kind === ANCHOR_KIND
        && hex0x(sha(Buffer.from(JSON.stringify(E.statement), 'utf8'))) === E.statementHash && typeof E.statement.subjectHash === 'string' && (j = pozitie.has(E.statement.subjectHash) ? pozitie.get(E.statement.subjectHash) : -1) >= 0
        && E.statement.source === recs[j].statement.deviceId; } catch { plic = false; }
      ok('anchor-envelope', 'witness', `witness: anchor ${n + 1} commits to a record of this log`, plic /*PAZA:anchor-envelope*/, 'not an aere-proof-of-time attestation whose hash reproduces, whose subjectHash is the hash of a record of this log and whose source is that record\'s device');
      if (!plic) continue;
      const pentru = citiriDe.get(E.statementHash) || [], citiri = pentru.filter((a) => Number.isInteger(a.at) && a.at > 0 && a.at < 1e11 && intreg(a.chainId, 1));
      if (pentru.length > citiri.length) nejudecat('witness-unread', 'witness', 'witness: a reading that cannot be used', `${pentru.length - citiri.length} reading(s) of anchor ${n + 1} carry no time in whole seconds since 1970 or no chain id: not used`);
      if (!citiri.length) { if (E.notarization != null && !pentru.length) nejudecat('witness-unread', 'witness', `witness: anchor ${n + 1}`, 'the envelope claims a notarization that the verifier did not read on the chain (a claim is not a reading)'); continue; }
      const prima = citiri.reduce((x, y) => (y.at < x.at ? y : x));
      const v = ancore.get(j); if (!v || prima.at * 1000 < v.at) ancore.set(j, { at: prima.at * 1000, chainId: prima.chainId });
    }
    if ((L.anchors || []).length > MAX_ANCHORS) nejudecat('witness-unread', 'witness', 'witness: more anchors than are judged', `${L.anchors.length} anchors, the first ${MAX_ANCHORS} are judged`);

    // records of this machine handed from elsewhere: a sibling signed by the same key for a position of the log is an equivocation. One
    // signed by a key of the log for a position held by another key, or beyond the log, is judged after the walk, which knows the rotations.
    // Two conditions keep a proof from being made by somebody who does not hold the key:
    //   - the log's record at that index must CARRY that position (seq): a log whose records were moved by whoever shows it puts the
    //     device's record n+1 at index n, and its real record n handed beside it would otherwise be "another record for position n";
    //   - a key the manufacturer RETIRED proves nothing beside the log: whoever copied it may sign a sibling after the retirement, and nothing
    //     here can show a record handed beside the log was signed before it. A retirement that keeps a key's history (README, Revocation)
    //     would otherwise be undone by one record of the thief. Named (retired-key-used), not counted.
    let furca = Infinity, ignorate = 0, retrase = 0; const deJudecat = [];
    for (const o of OT) {
      if (!wellFormed(o)) { ignorate++; continue; }
      const k = cheieDe(o.statement.deviceId); if (!k || !signedBy(o, k.S.key)) { ignorate++; continue; }
      const q = o.statement.seq, h = recordHash(o);
      if (q < recs.length && h === hashes[q]) continue;   // the same record
      if (k.retras !== null) { retrase++; continue; }
      if (q >= recs.length) { deJudecat.push(o); continue; }
      const r = recs[q];
      if (wellFormed(r) && r.statement.seq === q && r.statement.deviceId === o.statement.deviceId && signedBy(r, k.S.key)) {
        if (!equivocations.some((p) => p.seq === q && recordHash(p.b) === h)) equivocations.push(equivocationProof(r, o, k.S.key));
        furca = Math.min(furca, q);
      } else if (wellFormed(r) && r.statement.deviceId !== o.statement.deviceId) deJudecat.push(o);
      else ignorate++;   // the log's own record at that position is of this key and not signed by it: the walk below says why
    }

    // ---- the walk: each record against the one before it, the key in force, the time, the witness. The log is accepted up to the first
    // record a rule refuses; what follows is not judged.
    let idx = 0, prevHash = credentialHash(L.credentials[0]), prevAt = -Infinity, prevCounter = 0, lo = null, oprit = -1;
    for (let i = 0; i < recs.length; i++) {
      const r = recs[i], et = `record ${i}`, inainte = rows.length;
      if (!(wellFormed(r) /*PAZA:record-form*/)) { ok('record-form', 'record', `${et}: well formed`, false, `not an ${RECORD_KIND} record of exactly { statement, signature } with v, kind, deviceId, seq, prev, at (RFC 3339 UTC), state (${STATES.join(', ')}), counter, measurement, after and next`); oprit = i; break; }
      const s = r.statement, k = chei[idx];
      if (!k || !k.bun || !k.S) { oprit = i; break; }   // the credential of the key in force was refused (the identity row says why): nothing it signed counts
      const t = Date.parse(s.at);
      ok('record-key', 'record', `${et}: signed by the key in force (${k.S.deviceId})`, s.deviceId === k.S.deviceId /*PAZA:record-key*/, `the record names ${s.deviceId}` + (idx ? ' (after a rotation)' : ''));
      // the signature is checked with the key the record names when that key is certified in the log, else with the key in force
      const kn = cheieDe(s.deviceId) || k;
      ok('record-signature', 'record', `${et}: signed with the device key (ML-DSA-65)`, signedBy(r, kn.S.key) /*PAZA:record-signature*/, 'the signature does not verify with the device key, is not in canonical base64, or the signature object is not exactly { alg, value }');
      ok('record-seq', 'record', `${et}: carries its position`, s.seq === i /*PAZA:record-seq*/, `seq ${s.seq} at position ${i}`);
      ok('record-prev', 'record', `${et}: names the record before it`, s.prev === prevHash /*PAZA:record-prev*/, i ? 'prev is not the hash of the record before (a record was removed, changed or put in another order)' : 'prev of the first record is not the hash of the manufacture credential of the first key');
      ok('record-time', 'record', `${et}: its time does not go back and is not ahead of the verifier's clock`, t >= prevAt && t <= acum + sk /*PAZA:record-time*/, `dated ${s.at}: the record before is dated ${Number.isFinite(prevAt) ? iso(prevAt) : 'nothing'}, the verifier's clock is ${iso(acum)} (at most ${clockSkewS} s ahead)`);
      ok('record-counter', 'record', `${et}: the counter does not go down`, s.counter >= prevCounter /*PAZA:record-counter*/, `counter ${s.counter} after ${prevCounter}`);
      ok('key-window', 'record', `${et}: inside the validity of its key's manufacture credential`, k.S.vf - sk <= t && t <= k.S.vu /*PAZA:key-window*/, `dated ${s.at}, the credential is valid from ${iso(k.S.vf)} until ${iso(k.S.vu)}`);
      if (k.retras !== null) ok('key-retired', 'record', `${et}: dated before the manufacturer retired its key`, t < k.retras /*PAZA:key-retired*/, `dated ${s.at}; the manufacturer retired ${k.S.deviceId} ${Number.isFinite(k.retras) ? 'at ' + iso(k.retras) : 'at a time that cannot be read (it holds from the start)'}`);
      if (s.next !== null) {
        const nk = chei[idx + 1]; let nid = null; try { nid = D.deviceIdOf(s.next.key); } catch { nid = null; }
        ok('rotation', 'record', `${et}: a rotation to a key the same manufacturer certified for this machine`, !!nk && !!nk.S && nid === s.next.deviceId && s.next.deviceId === nk.S.deviceId && s.next.key === nk.S.key
          && nk.S.deviceId !== k.S.deviceId && aceeasi(nk.S.issuer, k.S.issuer) && nk.S.model === k.S.model && nk.S.serial === k.S.serial /*PAZA:rotation*/,
          'the next key is not a canonical ML-DSA-65 key of the device id named, or the next manufacture credential of the log is not of the same manufacturer, for the same model and serial, certifying that key');
      }
      let citit = null;
      if (s.after !== null) {
        const b = blocuri.get(s.after.chainId + ':' + s.after.block) || [];
        if (!b.length) nejudecat('beacon-unread', 'record', `${et}: the block it names`, `block ${s.after.block} of chain ${s.after.chainId} was not read by the verifier: no lower bound from it`);
        else {
          citit = b.find((x) => x.hash === s.after.hash) || null;
          ok('beacon-hash', 'record', `${et}: names a block the verifier read, with its hash`, !!citit /*PAZA:beacon-hash*/, `the record names block ${s.after.block} of chain ${s.after.chainId} with a hash the verifier did not read there`);
          if (citit) ok('beacon-time', 'record', `${et}: not dated before the block it names existed`, t >= citit.at * 1000 - sk /*PAZA:beacon-time*/, `dated ${s.at}, the block it names is dated ${iso(citit.at * 1000)}`);
        }
      }
      const a = ancore.get(i);
      if (a) ok('witness-time', 'record', `${et}: not dated after it was already on the chain (${iso(a.at)})`, t <= a.at + sk /*PAZA:witness-time*/, `dated ${s.at}, its anchor was already notarized at ${iso(a.at)}`);
      if (i === furca) ok('equivocation', 'record', `${et}: no other record of its key for this position`, i !== furca /*PAZA:equivocation*/, `the same key signed another record for position ${i} (the proof is kept)`);
      if (rows.slice(inainte).some((x) => x.pass === false)) { oprit = i; break; }
      if (citit) { lo = lo === null ? citit.at * 1000 : Math.max(lo, citit.at * 1000); lanturi.beacons.add(citit.chainId); }
      accepted.push({ seq: i, hash: hashes[i], at: t, lo, hi: null, state: s.state, counter: s.counter, deviceId: s.deviceId, key: idx });
      prevHash = hashes[i]; prevAt = t; prevCounter = s.counter;
      if (s.next !== null) idx++;
    }
    if (oprit >= 0 && oprit + 1 < recs.length) nejudecat('after-refusal', 'log', 'log: records after the first refused one', `${recs.length - oprit - 1} record(s) after record ${oprit} were not judged: the log is accepted up to the first record a rule refuses`);
    if (oprit >= 0 && !rows.some((x) => x.pass === false)) throw new Error('the walk stopped without a refusal');
    // the records handed beside the log that the pre-pass left: signed by a key AFTER the log rotated away from it (the old key is still in
    // use), beyond the log by the key in force at its end (the log shown is not the latest), or neither (ignored)
    const rotitLa = new Map(accepted.filter((x) => recs[x.seq].statement.next !== null).map((x) => [x.deviceId, x.seq]));
    const laCapat = chei[idx] && chei[idx].S ? chei[idx].S.deviceId : null; let folosite = 0, dincolo = 0;
    for (const o of deJudecat) { const p = rotitLa.get(o.statement.deviceId);
      if (p !== undefined && o.statement.seq > p) folosite++; else if (o.statement.seq >= recs.length && o.statement.deviceId === laCapat && oprit < 0) dincolo++; else ignorate++; }
    if (ignorate) nejudecat('other-ignored', 'equivocation', 'equivocation: records handed beside the log', `${ignorate} record(s) handed beside the log are not well formed, not signed by a key certified in it, or stand beside a record of the log that is not of their key or does not carry its position: ignored`);
    if (folosite) nejudecat('rotated-key-used', 'equivocation', 'equivocation: a key used after the log rotated away from it', `${folosite} record(s) handed beside the log are signed by a key for a position after the record that rotated the log away from it: somebody still holds and uses that key`);
    if (retrase) nejudecat('retired-key-used', 'equivocation', 'equivocation: records of a retired key beside the log', `${retrase} record(s) handed beside the log, other than the log's own, are signed by a key the manufacturer retired, and nothing shows they were signed before the retirement: whoever copied the key may have signed them after it, so they are neither a proof of equivocation nor a longer log`);
    if (dincolo) nejudecat('records-beyond', 'equivocation', 'equivocation: records beyond the log shown', `${dincolo} record(s) signed by the key in force at the end of this log stand at a position after its last record: the log shown is not the latest the verifier holds, so judge the longer one`);

    // the upper bound of each accepted record: the earliest anchor read at it or after it (a later record names it through prev)
    let hi = null;
    for (let j = accepted.length - 1; j >= 0; j--) { const a = ancore.get(accepted[j].seq); if (a) { hi = hi === null ? a.at : Math.min(hi, a.at); lanturi.anchors.add(a.chainId); } accepted[j].hi = hi; }
    // what counts: an accepted record; when the manufacturer retired its key, only if a witness shows it existed before the retirement
    counted = accepted.filter((x) => { const T = chei[x.key].retras; return T === null || (x.hi !== null && x.hi <= T); });
    const nu = accepted.length - counted.length;
    if (nu) nejudecat('retired-unwitnessed', 'status', 'status: records of a retired key with no witness before the retirement', `${nu} record(s) are dated before the manufacturer retired their key, and no anchor read shows they existed before it: a copied key can date a record as it likes, so they are not counted`);
    const farSus = counted.filter((x) => x.hi === null).length, farJos = counted.filter((x) => x.lo === null).length;
    if (farSus || farJos) nejudecat('time-unwitnessed', 'witness', 'witness: time', `${farSus} of ${counted.length} counted record(s) have no witnessed upper bound (no anchor read at or after them) and ${farJos} no witnessed lower bound (no block read at or before them): there, the time is the device's word`);
    numarate = counted;
    return gata();
  }
}