// Consensus, checked against a second implementation of Raft that is written
// here from the paper's Figure 2 and shares no code with the page, and then
// broken on purpose.
//
// The engine collapses each exchange into one step: a vote request and its
// reply, or a leader's whole back-off-and-retry loop with a follower. The
// oracle below does not. It builds the messages Figure 2 describes, with
// prevLogIndex, prevLogTerm, nextIndex decremented one refusal at a time, and
// replies that carry terms, and delivers them. If the shortcut were wrong
// anywhere in the reachable space, the two would reach different states.
//
// Four comparisons, each a different question:
//   1. the same set of states, every one, for three servers through four
//      terms, under both commit rules, with the engine's symmetry reduction
//      switched off and its states encoded here rather than by the engine;
//   2. the engine's reduced count against an orbit count done here over all
//      six renamings;
//   3. the five properties, checked by code written here, in every state;
//   4. a long seeded walk on five servers with cuts and heals, comparing
//      every server after every step.
//
// Then the paper itself: Figure 8's caption is parsed from the archived text
// for who voted in (b) and (d), and the five panels are compared with a
// transcription of the figure made from the page at 300 dots per inch.
//
// The archive is docs/sources/<id>/*.txt, written by la-source-audit
// --archive. Before it exists, LA_SOURCES_DIR may point at a scratch copy laid
// out the same way.

import { readFileSync, existsSync } from 'node:fs';
import { fileURLToPath } from 'node:url';
import { dirname, join } from 'node:path';

const HERE = dirname(fileURLToPath(import.meta.url));
const ROOT = join(HERE, '..');
let p = 0;
let f = 0;
const check = (label, ok, detail = '') => {
  if (ok) { p += 1; console.log(`  ok   ${label}${detail ? `  [${detail}]` : ''}`); }
  else { f += 1; console.error(`  FAIL ${label}${detail ? `\n       ${detail}` : ''}`); }
};

const SRC = readFileSync(join(ROOT, 'site/js/consensus.js'), 'utf8');
function engine(src = SRC) {
  const window = {};
  new Function('window', src)(window);
  return window.Consensus;
}
const C = engine();

/* ==== the oracle ========================================================== */
/*
 * Raft from Figure 2, with messages. Servers are numbered from 0. A log entry
 * is {term}. Nothing here is imported from, or shaped like, the engine's
 * representation; the bridge functions at the end translate.
 */
function oServer() {
  return { currentTerm: 0, votedFor: null, log: [], commitIndex: 0,
           state: 'follower', votesGranted: new Set(), nextIndex: [], matchIndex: [] };
}
function oCluster(n) {
  const servers = [];
  for (let i = 0; i < n; i += 1) servers.push(oServer());
  return { n, servers, side: new Array(n).fill(0), elected: new Map(), committed: new Map() };
}
function oClone(c) {
  return {
    n: c.n,
    servers: c.servers.map((s) => ({
      currentTerm: s.currentTerm, votedFor: s.votedFor, log: s.log.map((e) => ({ term: e.term })),
      commitIndex: s.commitIndex, state: s.state, votesGranted: new Set(s.votesGranted),
      nextIndex: s.nextIndex.slice(), matchIndex: s.matchIndex.slice(),
    })),
    side: c.side.slice(),
    elected: new Map(c.elected),
    committed: new Map([...c.committed].map(([k, v]) => [k, { ...v }])),
  };
}
const quorum = (n) => Math.floor(n / 2) + 1;
const lastLogTerm = (s) => (s.log.length ? s.log[s.log.length - 1].term : 0);

// "If RPC request or response contains term T > currentTerm: set currentTerm
// = T, convert to follower". votedFor belongs to a term, so it is cleared.
function oSeeTerm(s, T) {
  if (T > s.currentTerm) {
    s.currentTerm = T; s.state = 'follower'; s.votedFor = null;
    s.votesGranted = new Set(); s.nextIndex = []; s.matchIndex = [];
  }
}
function oBecomeLeader(c, i) {
  const s = c.servers[i];
  s.state = 'leader';
  s.votesGranted = new Set();
  s.nextIndex = new Array(c.n).fill(s.log.length + 1);
  s.matchIndex = new Array(c.n).fill(0);
  const had = c.elected.get(s.currentTerm);
  c.elected.set(s.currentTerm, had === undefined || had === i ? i : 'twice');
}
function oTimeout(c, i) {
  const s = c.servers[i];
  s.currentTerm += 1; s.state = 'candidate'; s.votedFor = i;
  s.votesGranted = new Set([i]); s.nextIndex = []; s.matchIndex = [];
  if (s.votesGranted.size >= quorum(c.n)) oBecomeLeader(c, i);
}
// RequestVote, receiver implementation.
function oHandleRequestVote(r, m) {
  oSeeTerm(r, m.term);
  if (m.term < r.currentTerm) return { term: r.currentTerm, voteGranted: false };
  const logOk = m.lastLogTerm > lastLogTerm(r)
    || (m.lastLogTerm === lastLogTerm(r) && m.lastLogIndex >= r.log.length);
  const grant = (r.votedFor === null || r.votedFor === m.candidateId) && logOk;
  if (grant) r.votedFor = m.candidateId;
  return { term: r.currentTerm, voteGranted: grant };
}
function oRequestVote(c, i, j) {
  const s = c.servers[i];
  const reply = oHandleRequestVote(c.servers[j], {
    term: s.currentTerm, candidateId: i, lastLogIndex: s.log.length, lastLogTerm: lastLogTerm(s),
  });
  if (reply.term > s.currentTerm) { oSeeTerm(s, reply.term); return; }
  if (s.state === 'candidate' && reply.term === s.currentTerm && reply.voteGranted) {
    s.votesGranted.add(j);
    if (s.votesGranted.size >= quorum(c.n)) oBecomeLeader(c, i);
  }
}
function oWrite(c, i) {
  const s = c.servers[i];
  s.log.push({ term: s.currentTerm });
}
// AppendEntries, receiver implementation, rules 1 to 5.
function oHandleAppendEntries(r, m) {
  oSeeTerm(r, m.term);
  if (m.term < r.currentTerm) return { term: r.currentTerm, success: false };
  // A candidate that hears from the leader of its own term goes back to following.
  r.state = 'follower'; r.votesGranted = new Set(); r.nextIndex = []; r.matchIndex = [];
  if (m.prevLogIndex > 0 && (r.log.length < m.prevLogIndex
      || r.log[m.prevLogIndex - 1].term !== m.prevLogTerm)) {
    return { term: r.currentTerm, success: false };
  }
  m.entries.forEach((e, k) => {
    const index = m.prevLogIndex + 1 + k;
    if (r.log.length >= index && r.log[index - 1].term !== e.term) r.log.length = index - 1;
    if (r.log.length < index) r.log.push({ term: e.term });
  });
  if (m.leaderCommit > r.commitIndex) {
    r.commitIndex = Math.min(m.leaderCommit, m.prevLogIndex + m.entries.length);
  }
  return { term: r.currentTerm, success: true, matched: m.prevLogIndex + m.entries.length };
}
function oAppendEntries(c, i, j, rule) {
  const s = c.servers[i];
  // The leader retries, decrementing nextIndex, until the follower agrees or
  // a reply carries a newer term. Each pass is one message and one reply.
  for (let guard = 0; guard < 1000; guard += 1) {
    const prevLogIndex = s.nextIndex[j] - 1;
    const reply = oHandleAppendEntries(c.servers[j], {
      term: s.currentTerm, leaderId: i, prevLogIndex,
      prevLogTerm: prevLogIndex > 0 ? s.log[prevLogIndex - 1].term : 0,
      entries: s.log.slice(prevLogIndex).map((e) => ({ term: e.term })),
      leaderCommit: s.commitIndex,
    });
    if (reply.term > s.currentTerm) { oSeeTerm(s, reply.term); return; }
    if (reply.success) {
      s.nextIndex[j] = reply.matched + 1;
      s.matchIndex[j] = Math.max(s.matchIndex[j], reply.matched);
      oAdvanceCommit(c, i, rule);
      return;
    }
    s.nextIndex[j] -= 1;
  }
  throw new Error('AppendEntries never converged');
}
// "If there exists an N such that N > commitIndex, a majority of
// matchIndex[i] >= N, and log[N].term == currentTerm: set commitIndex = N".
// The leader is one of the majority. With rule 'majority' the last clause is
// dropped, which is the rule Figure 8 is about.
function oAdvanceCommit(c, i, rule) {
  const s = c.servers[i];
  const candidates = [];
  for (let N = s.commitIndex + 1; N <= s.log.length; N += 1) {
    let agree = 1;
    for (let k = 0; k < c.n; k += 1) if (k !== i && s.matchIndex[k] >= N) agree += 1;
    if (agree >= quorum(c.n) && (rule === 'majority' || s.log[N - 1].term === s.currentTerm)) {
      candidates.push(N);
    }
  }
  if (!candidates.length) return;
  const N = Math.max(...candidates);
  for (let x = s.commitIndex + 1; x <= N; x += 1) {
    const had = c.committed.get(x);
    if (!had) c.committed.set(x, { entryTerm: s.log[x - 1].term, inTerm: s.currentTerm });
    else if (had.entryTerm !== s.log[x - 1].term) had.entryTerm = 'two';
  }
  s.commitIndex = N;
}
const oReach = (c, i, j) => c.side[i] === c.side[j];

// Which messages may be sent at all is a modelling choice, not Raft, and it
// has to be the same choice for the two to explore the same space: a timeout
// for anyone but a leader, while terms remain; a vote request from a
// candidate to anyone it has no vote from, or a late one from a leader to
// anyone yet to vote in its term; a write to a leader while logs are short;
// a send from a leader to anyone.
function oActions(c, maxTerm, maxLog) {
  const out = [];
  c.servers.forEach((s, i) => {
    if (s.state !== 'leader' && !(maxTerm && s.currentTerm >= maxTerm)) out.push(['T', i]);
    if (s.state === 'candidate' || s.state === 'leader') {
      for (let j = 0; j < c.n; j += 1) {
        if (j === i || s.votesGranted.has(j) || !oReach(c, i, j)) continue;
        const r = c.servers[j];
        if (s.state === 'leader' && r.currentTerm === s.currentTerm && r.votedFor !== null) continue;
        out.push(['V', i, j]);
      }
    }
    if (s.state === 'leader') {
      if (!(maxLog && s.log.length >= maxLog)) out.push(['W', i]);
      for (let j = 0; j < c.n; j += 1) if (j !== i && oReach(c, i, j)) out.push(['A', i, j]);
    }
  });
  return out;
}
function oApply(c, a, rule) {
  const d = oClone(c);
  if (a[0] === 'T') oTimeout(d, a[1]);
  else if (a[0] === 'V') oRequestVote(d, a[1], a[2]);
  else if (a[0] === 'W') oWrite(d, a[1]);
  else if (a[0] === 'A') oAppendEntries(d, a[1], a[2], rule);
  else if (a[0] === 'P') d.side = d.side.map((_, i) => ((a[1] >> i) & 1));
  else if (a[0] === 'H') d.side = d.side.map(() => 0);
  return d;
}

// The five properties of Figure 3, written again.
function oBroken(c, before) {
  const out = new Set();
  for (const v of c.elected.values()) if (v === 'twice') out.add('election');
  const S = c.servers;
  for (let a = 0; a < c.n; a += 1) {
    for (let b = a + 1; b < c.n; b += 1) {
      const m = Math.min(S[a].log.length, S[b].log.length);
      for (let x = 1; x <= m; x += 1) {
        if (S[a].log[x - 1].term !== S[b].log[x - 1].term) continue;
        for (let y = 1; y < x; y += 1) {
          if (S[a].log[y - 1].term !== S[b].log[y - 1].term) out.add('matching');
        }
      }
    }
  }
  S.forEach((s) => {
    if (s.state !== 'leader') return;
    for (const [idx, v] of c.committed) {
      if (v.inTerm < s.currentTerm && (!s.log[idx - 1] || s.log[idx - 1].term !== v.entryTerm)) {
        out.add('completeness');
      }
    }
  });
  for (const v of c.committed.values()) if (v.entryTerm === 'two') out.add('machine');
  S.forEach((s) => {
    for (let x = 1; x <= s.commitIndex; x += 1) {
      const v = c.committed.get(x);
      if (!v || !s.log[x - 1] || s.log[x - 1].term !== v.entryTerm) out.add('machine');
    }
  });
  if (before) {
    before.servers.forEach((s, i) => {
      const t = S[i];
      if (s.state !== 'leader' || t.state !== 'leader' || s.currentTerm !== t.currentTerm) return;
      if (t.log.length < s.log.length || s.log.some((e, k) => t.log[k].term !== e.term)) {
        out.add('append');
      }
    });
  }
  return out;
}

/* ---- the bridge: one neutral string for a state from either side ------------ */
// Role letter, term, vote, the log as terms, the commit index, a candidate's
// votes and a leader's matchIndex (its own entry left out), and the history:
// who was elected in which term and what was committed where, in which term.
const ROLE = { follower: 'F', candidate: 'C', leader: 'L' };
function neutralFromOracle(c, perm = null) {
  const at = (i) => (perm ? perm[i] : i);
  const servers = [];
  c.servers.forEach((s, i) => {
    let extra = '';
    if (s.state === 'candidate') extra = `v${[...s.votesGranted].map(at).sort().join('')}`;
    if (s.state === 'leader') {
      const m = new Array(c.n).fill('*');
      for (let k = 0; k < c.n; k += 1) if (k !== i) m[at(k)] = s.matchIndex[k];
      extra = `m${m.join(',')}`;
    }
    servers[at(i)] = `${ROLE[s.state]}${s.currentTerm}/${s.votedFor === null ? '-' : at(s.votedFor)}`
      + `/${s.log.map((e) => e.term).join('')}/${s.commitIndex}${extra}`;
  });
  const el = [...c.elected].sort((a, b) => a[0] - b[0])
    .map(([t, v]) => `${t}:${v === 'twice' ? 'x' : at(v)}`).join(',');
  const cm = [...c.committed].sort((a, b) => a[0] - b[0])
    .map(([x, v]) => `${x}:${v.entryTerm === 'two' ? 'x' : v.entryTerm}@${v.inTerm}`).join(',');
  return `${servers.join(' ')}|${el}|${cm}`;
}
function neutralFromEngine(st) {
  const servers = st.s.map((x, i) => {
    let extra = '';
    if (x.role === 'C') {
      const v = [];
      for (let k = 0; k < st.n; k += 1) if ((x.votes >> k) & 1) v.push(k);
      extra = `v${v.join('')}`;
    }
    if (x.role === 'L') {
      const m = [];
      for (let k = 0; k < st.n; k += 1) m[k] = k === i ? '*' : x.match[k];
      extra = `m${m.join(',')}`;
    }
    return `${x.role}${x.term}/${x.voted < 0 ? '-' : x.voted}/${x.log.join('')}/${x.commit}${extra}`;
  });
  const el = [];
  st.ghost.elected.forEach((w, t) => { if (w !== undefined) el.push(`${t}:${w === -2 ? 'x' : w}`); });
  const cm = [];
  st.ghost.committed.forEach((c, x) => { if (c) cm.push(`${x}:${c.et === -1 ? 'x' : c.et}@${c.ct}`); });
  return `${servers.join(' ')}|${el.join(',')}|${cm.join(',')}`;
}
const toOracleAct = (a) => (a.k === 'P' ? ['P', a.mask] : a.k === 'H' ? ['H'] : [a.k, a.i, a.j]);

/* ---- the oracle's own search ------------------------------------------------ */
function oSearch(n, maxTerm, maxLog, rule) {
  const start = oCluster(n);
  const seen = new Map([[neutralFromOracle(start), start]]);
  const broken = new Map();
  const queue = [start];
  for (let h = 0; h < queue.length; h += 1) {
    const c = queue[h];
    for (const a of oActions(c, maxTerm, maxLog)) {
      const d = oApply(c, a, rule);
      const k = neutralFromOracle(d);
      const bad = oBroken(d, c);
      if (seen.has(k) && !bad.has('append')) continue;
      if (!seen.has(k)) seen.set(k, d);
      if (bad.size) { broken.set(k, bad); continue; }
      queue.push(d);
    }
  }
  return { seen, broken };
}

/* ==== 1. the engine's own claims =========================================== */
{
  const rows = C.verify();
  check('the page makes at least twelve checks at load', rows.length >= 12, String(rows.length));
  rows.forEach((r) => check(`load-time: ${r.claim.slice(0, 70)}`, r.ok && !r.untested, r.detail));
  // The broken history's row says which properties failed, by name, before
  // the first message. A name list that comes out empty still reads as a
  // sentence (" fail: S2 leads ..."), so check the names are there.
  const names = C.PROPS.map((q) => q.name);
  const bad = rows.find((r) => r.claim.startsWith('with the term check removed'));
  const said = bad ? bad.detail.split(' fail: ')[0] : '';
  check('the broken history\'s row names the properties it breaks',
    !!bad && said.length > 0 && said.split(' and ').every((s) => names.includes(s)),
    bad ? bad.detail : 'no such row');
}

/* ==== 2. the same states, every one ======================================== */
const BOX = { n: 3, maxTerm: 4, maxLog: 1 };
const results = {};
for (const rule of ['raft', 'majority']) {
  const t0 = Date.now();
  const eng = C.check({ ...BOX, rule, symmetry: false, collect: true });
  const orc = oSearch(BOX.n, BOX.maxTerm, BOX.maxLog, rule);
  const engSet = new Set(eng.kept.map(neutralFromEngine));
  const onlyEngine = [...engSet].filter((k) => !orc.seen.has(k));
  const onlyOracle = [...orc.seen.keys()].filter((k) => !engSet.has(k));
  check(`${rule}: the engine and the message-level oracle reach exactly the same states`,
    engSet.size === orc.seen.size && onlyEngine.length === 0 && onlyOracle.length === 0
      && engSet.size === eng.states,
    `engine ${eng.states} (${engSet.size} distinct here), oracle ${orc.seen.size}; `
      + `only engine ${onlyEngine.length}${onlyEngine[0] ? ` e.g. ${onlyEngine[0]}` : ''}, `
      + `only oracle ${onlyOracle.length}${onlyOracle[0] ? ` e.g. ${onlyOracle[0]}` : ''}`);

  // 3. The five properties, the engine's checker against the one above, in
  // every state the oracle reached.
  let disagree = 0, sample = '';
  let brokenHere = 0;
  for (const [k, c] of orc.seen) {
    const mine = oBroken(c, null);
    const st = toEngineState(c);
    const theirs = new Set(C.broken(st, null).map((b) => b.prop));
    if (mine.size) brokenHere += 1;
    if ([...mine].sort().join() !== [...theirs].sort().join()) {
      disagree += 1;
      if (!sample) sample = `${k}: oracle ${[...mine]} engine ${[...theirs]}`;
    }
  }
  check(`${rule}: the two property checkers agree in all ${orc.seen.size} states`,
    disagree === 0 && orc.seen.size > 0, sample || `${brokenHere} broken by both`);
  results[rule] = { eng, orc, brokenHere };
  console.log(`       (${rule}: ${Date.now() - t0} ms)`);
}
check('with Raft\'s rule, neither finds a broken state',
  results.raft.brokenHere === 0 && results.raft.orc.broken.size === 0 && !results.raft.eng.failed);
check('without the clause, both find broken states, and the same number',
  results.majority.brokenHere > 0 && results.majority.orc.broken.size === results.majority.brokenHere,
  `${results.majority.orc.broken.size} by the oracle's search, ${results.majority.brokenHere} by state`);
check('and every broken state is one the property checker can see without its history step',
  [...results.majority.orc.broken.values()].every((b) => !b.has('append')));

// The engine's state as an engine object, built from an oracle state, so the
// engine's checker and its canonical naming can be asked about it.
function toEngineState(c) {
  const st = C.fresh(c.n);
  c.servers.forEach((s, i) => {
    const x = st.s[i];
    x.term = s.currentTerm; x.role = ROLE[s.state]; x.voted = s.votedFor === null ? -1 : s.votedFor;
    x.log = s.log.map((e) => e.term); x.commit = s.commitIndex;
    x.votes = 0;
    if (s.state === 'candidate') for (const v of s.votesGranted) x.votes |= 1 << v;
    x.match = s.state === 'leader' ? s.matchIndex.map((m, k) => (k === i ? 0 : m)) : null;
  });
  for (const [t, v] of c.elected) st.ghost.elected[t] = v === 'twice' ? -2 : v;
  for (const [x, v] of c.committed) st.ghost.committed[x] = { et: v.entryTerm === 'two' ? -1 : v.entryTerm, ct: v.inTerm };
  st.cut = c.side.reduce((m, s, i) => m | (s << i), 0);
  return st;
}

/* ==== 2b. the symmetry reduction, counted a second way ===================== */
{
  const perms = [[0, 1, 2], [0, 2, 1], [1, 0, 2], [1, 2, 0], [2, 0, 1], [2, 1, 0]];
  for (const rule of ['raft', 'majority']) {
    const orbits = new Set();
    for (const c of results[rule].orc.seen.values()) {
      orbits.add(perms.map((pm) => neutralFromOracle(c, pm)).sort()[0]);
    }
    const reduced = C.check({ ...BOX, rule });
    check(`${rule}: the engine's reduced count is the number of orbits under renaming`,
      reduced.states === orbits.size, `${reduced.states} against ${orbits.size}`);
    // And the engine's canonical names agree with that partition exactly.
    const canon = new Map();
    let split = 0, shortcut = 0;
    for (const c of results[rule].orc.seen.values()) {
      const orbit = perms.map((pm) => neutralFromOracle(c, pm)).sort()[0];
      const st = toEngineState(c);
      const ek = canonicalViaEngine(st);
      if (C.canonical(st) !== ek) shortcut += 1;
      if (canon.has(orbit) && canon.get(orbit) !== ek) split += 1;
      canon.set(orbit, ek);
    }
    const distinct = new Set(canon.values()).size;
    check(`${rule}: and its canonical name splits no orbit and merges none`,
      split === 0 && distinct === orbits.size, `${split} split, ${distinct} names for ${orbits.size} orbits`);
    check(`${rule}: and trying only the renamings that sort the servers gives the same name as trying all six`,
      shortcut === 0, `${shortcut} differ`);
  }
}
function canonicalViaEngine(st) {
  // The engine exposes keyOf; its reduction picks the smallest key over the
  // renamings that sort the servers. Asked for over ALL renamings here, which
  // is the definition the shortcut claims to equal.
  const perms = [[0, 1, 2], [0, 2, 1], [1, 0, 2], [1, 2, 0], [2, 0, 1], [2, 1, 0]];
  return perms.map((pm) => C.keyOf(st, pm)).sort()[0];
}

/* ==== 2c. the numbers the page prints ====================================== */
{
  // Each property row prints how many states gave it something to check.
  // Counted again here, over one representative of each orbit of the
  // oracle's states, with this file's own definitions of "something to check".
  // Log Matching counts a state only when two logs share a term at index 2
  // or later, the only place it can fail; Leader Append-Only counts the steps
  // that change the log of a server leading the same term before and after.
  const perms = [[0, 1, 2], [0, 2, 1], [1, 0, 2], [1, 2, 0], [2, 0, 1], [2, 1, 0]];
  const recount = (seen, box) => {
    const reps = new Map();
    for (const c of seen.values()) {
      const orbit = perms.map((pm) => neutralFromOracle(c, pm)).sort()[0];
      if (!reps.has(orbit)) reps.set(orbit, c);
    }
    const t = { election: 0, append: 0, matching: 0, completeness: 0, machine: 0 };
    let writes = 0;
    for (const c of reps.values()) {
      if (c.elected.size) t.election += 1;
      const S = c.servers;
      let deep = false;
      for (let a = 0; a < c.n; a += 1) for (let b = a + 1; b < c.n; b += 1) {
        for (let x = 2; x <= Math.min(S[a].log.length, S[b].log.length); x += 1) {
          if (S[a].log[x - 1].term === S[b].log[x - 1].term) deep = true;
        }
      }
      if (deep) t.matching += 1;
      const old = (s) => [...c.committed.values()].some((v) => v.inTerm < s.currentTerm);
      if (S.some((s) => s.state === 'leader' && old(s))) t.completeness += 1;
      if (S.some((s) => s.commitIndex > 0)) t.machine += 1;
      for (const a of oActions(c, box.maxTerm, box.maxLog)) {
        const d = oApply(c, a, 'raft');
        const changed = S.some((s, i) => s.state === 'leader' && d.servers[i].state === 'leader'
          && s.currentTerm === d.servers[i].currentTerm
          && s.log.map((e) => e.term).join() !== d.servers[i].log.map((e) => e.term).join());
        if (changed) { t.append += 1; if (a[0] === 'W') writes += 1; }
      }
    }
    return { t, writes };
  };
  const g = C.check({ ...BOX, rule: 'raft' });
  const { t } = recount(results.raft.orc.seen, BOX);
  check('the per-property counts the page prints are counted again from the oracle\'s states',
    JSON.stringify(t) === JSON.stringify(g.tested),
    `here ${JSON.stringify(t)}, engine ${JSON.stringify(g.tested)}`);
  check('and they are 15,604, 7,159 and 12,639 for the three rows read off the first box',
    t.election === 15604 && t.completeness === 7159 && t.machine === 12639);
  check('and none for Log Matching there, which is why its row reads the second box',
    t.matching === 0);
  const g2 = C.check({ ...C.LOAD2, rule: 'raft' });
  const o2 = recount(oSearch(C.LOAD2.n, C.LOAD2.maxTerm, C.LOAD2.maxLog, 'raft').seen, C.LOAD2);
  check('the second box\'s counts, again from the oracle\'s states',
    JSON.stringify(o2.t) === JSON.stringify(g2.tested) && o2.writes === g2.writes,
    `here ${JSON.stringify(o2.t)} writes ${o2.writes}, engine ${JSON.stringify(g2.tested)} writes ${g2.writes}`);
  check('and the two rows read off it are 374 leader-log changes, all client writes, and 734 states',
    o2.t.append === 374 && o2.writes === 374 && o2.t.matching === 734,
    `${o2.t.append}, ${o2.writes}, ${o2.t.matching}`);
  const c8 = C.replay(5, C.figure8('c'), 'raft');
  const e8 = C.replay(5, C.figure8('e'), 'raft');
  check('in (c) S1 has committed index 1 only, and in (e) index 3',
    c8.state.s[0].commit === 1 && e8.state.s[0].commit === 3);
  check('the history to (d) is 42 steps, and the other rule first breaks it at step 36',
    C.figure8('d').length === 42
      && C.replay(5, C.figure8('d'), 'majority').firstBroken === 35);
  // Every server that has applied an entry the committed record disagrees
  // with is named, up to and including its own commit index. On this history
  // the disagreement sits exactly at the commit index, so a scan that stops
  // one short names nobody and the page explains less than it found.
  const d8 = C.replay(5, C.figure8('d'), 'majority');
  let owed = 0; let named = 0;
  d8.trail.forEach((t) => {
    const st = t.state;
    st.s.forEach((srv, i) => {
      let at = 0;
      for (let x = 1; x <= srv.commit && !at; x += 1) {
        const rec = st.ghost.committed[x];
        if (!rec || srv.log[x - 1] !== rec.et) at = x;
      }
      if (!at) return;
      owed += 1;
      if (t.broken.some((b) => b.prop === 'machine' && b.text.startsWith(`S${i + 1} has applied index ${at} `))) named += 1;
    });
  });
  check('under the other rule, every server that applied a disputed entry is named, at its commit index too',
    owed > 0 && named === owed, `${named} of ${owed} named`);
}
{
  // These are what the page computes at load and prints. Each is derived above
  // by the oracle as well; the literal pins both against drifting together.
  const g = C.check({ ...BOX, rule: 'raft' });
  const b = C.check({ ...BOX, rule: 'majority' });
  const lower = C.check({ ...BOX, maxTerm: 3, rule: 'majority' });
  check('three servers, four terms, one entry each: 15,675 states with Raft\'s rule',
    g.states === 15675, String(g.states));
  check('and 14,424 counting copies of any entry, broken after 13 steps',
    b.states === 14424 && b.trace && b.trace.length === 13, `${b.states}, ${b.trace && b.trace.length}`);
  check('with terms up to 3 the other rule breaks nothing in 2,449 states',
    lower.states === 2449 && !lower.failed, String(lower.states));
  check('a majority of five is 3 and of three is 2, computed by the engine',
    C.majority(5) === 3 && C.majority(3) === 2 && C.majority(4) === 3);
  // The shortest failure, re-derived: the oracle's breadth-first search reaches
  // its first broken state at the same depth.
  const depthOf = (() => {
    const start = oCluster(3);
    let frontier = [start];
    const seen = new Set([neutralFromOracle(start)]);
    for (let d = 1; d <= 30; d += 1) {
      const next = [];
      for (const c of frontier) {
        for (const a of oActions(c, 4, 1)) {
          const x = oApply(c, a, 'majority');
          if (oBroken(x, c).size) return d;
          const k = neutralFromOracle(x);
          if (seen.has(k)) continue;
          seen.add(k); next.push(x);
        }
      }
      frontier = next;
    }
    return -1;
  })();
  check('and the oracle\'s own search first breaks at the same depth, 13',
    depthOf === 13, String(depthOf));
  // The trace the page offers to load really is a history: replay it through
  // the oracle, message by message.
  let c = oCluster(3);
  let firstBad = -1;
  b.trace.forEach((name, z) => {
    const before = c;
    c = oApply(c, toOracleAct(C.parse(name)), 'majority');
    if (firstBad < 0 && oBroken(c, before).size) firstBad = z;
  });
  check('the history the page loads breaks the oracle\'s cluster at its last step too',
    firstBad === 12, String(firstBad));
}

/* ==== 3. other cluster sizes, exhaustively, in smaller boxes ============== */
{
  // The oracle comparison above is for three servers. Four and five are
  // searched by the engine alone, in boxes small enough for a test run; the
  // larger boxes run when LA_CONSENSUS_FULL=1, because they take minutes.
  const boxes = [
    { n: 4, maxTerm: 3, maxLog: 1, breaks: false },
    { n: 5, maxTerm: 2, maxLog: 1, breaks: false },
  ];
  if (process.env.LA_CONSENSUS_FULL === '1') {
    boxes.push({ n: 4, maxTerm: 4, maxLog: 1, breaks: true });
    boxes.push({ n: 5, maxTerm: 3, maxLog: 1, breaks: false });
  } else {
    console.log('  --   four servers through four terms and five through three: NOT TESTED '
      + 'in this run (LA_CONSENSUS_FULL=1 runs them)');
  }
  for (const b of boxes) {
    const good = C.check({ ...b, rule: 'raft' });
    const bad = C.check({ ...b, rule: 'majority' });
    const label = `${b.n} servers, terms up to ${b.maxTerm}, ${b.maxLog} entry per log`;
    check(`${label}: Raft's rule breaks nothing in ${good.states} states`,
      !good.failed && good.states > 0 && good.tested.completeness > 0,
      `${good.tested.completeness} states with something for Leader Completeness to check`);
    check(`${label}: the other rule ${b.breaks ? 'breaks' : 'does not yet break'} it, in ${bad.states} states`,
      Boolean(bad.failed) === b.breaks,
      bad.failed ? `${bad.trace.length} steps: ${bad.failed.broken[0].text}` : 'nothing broken');
  }
}

/* ==== 4. five servers, cuts and heals, a seeded walk ======================= */
// mulberry32, so the walk is the same every run. The engine is a parameter so
// the same walk can be run against a copy broken on purpose.
function walk(E, walks) {
  let seed = 20141906;
  const rand = () => {
    seed |= 0; seed = (seed + 0x6D2B79F5) | 0;
    let t = Math.imul(seed ^ (seed >>> 15), 1 | seed);
    t = (t + Math.imul(t ^ (t >>> 7), 61 | t)) ^ t;
    return ((t ^ (t >>> 14)) >>> 0) / 4294967296;
  };
  let steps = 0, mismatches = 0, first = '', cuts = 0, deletions = 0, commits = 0;
  for (const rule of ['raft', 'majority']) {
    for (let w = 0; w < walks; w += 1) {
      let st = E.fresh(5);
      let oc = oCluster(5);
      for (let z = 0; z < 120; z += 1) {
        let acts = E.actions(st, { maxTerm: 12, maxLog: 6 });
        if (rand() < 0.08) {
          acts = [{ k: 'P', mask: 1 + Math.floor(rand() * 30) }];
          cuts += 1;
        } else if (st.cut && rand() < 0.05) acts = [{ k: 'H' }];
        if (!acts.length) break;
        const a = acts[Math.floor(rand() * acts.length)];
        const r = E.step(st, a, rule);
        const before = oc;
        oc = oApply(oc, toOracleAct(a), rule);
        const want = neutralFromOracle(oc);
        if (!r.ok) {
          // The engine refusing a step the oracle takes is a difference too.
          if (want !== neutralFromOracle(before)) {
            mismatches += 1;
            if (!first) first = `${rule} walk ${w} step ${z} ${E.name(a)} refused: ${r.why}`;
          }
          oc = before;
          continue;
        }
        st = r.state;
        steps += 1;
        if (r.removed && r.removed.length) deletions += 1;
        const got = neutralFromEngine(st);
        const brokenOracle = [...oBroken(oc, before)].sort().join();
        const brokenEngine = [...new Set(r.broken.map((x) => x.prop))].sort().join();
        if (want !== got || brokenOracle !== brokenEngine || st.cut !== toEngineState(oc).cut) {
          mismatches += 1;
          if (!first) {
            first = `${rule} walk ${w} step ${z} ${E.name(a)}:\n         engine ${got} ${brokenEngine}`
              + `\n         oracle ${want} ${brokenOracle}`;
          }
          break;      // the two have parted; the rest of this walk compares nothing
        }
        if (brokenEngine) break;
      }
      commits += st.s.reduce((m, x) => Math.max(m, x.commit), 0);
    }
  }
  return { steps, mismatches, first, cuts, deletions, commits };
}
{
  const w = walk(C, 60);
  check('a seeded walk on five servers with cuts and heals matches the oracle at every step',
    w.mismatches === 0 && w.steps > 0, w.first || `${w.steps} steps`);
  // A walk that never cut, never deleted or never committed would have
  // compared nothing that matters, and it would still have matched.
  check('and the walk exercised what it is meant to: cuts, deletions and commits',
    w.cuts > 0 && w.deletions > 0 && w.commits > 0,
    `${w.cuts} cuts, ${w.deletions} steps that deleted entries, ${w.commits} commit index summed`);
}

/* ==== 5. Figure 8 against the paper ======================================== */
function sourcesDir() {
  if (process.env.LA_SOURCES_DIR && existsSync(join(process.env.LA_SOURCES_DIR, 'manifest.json'))) {
    return process.env.LA_SOURCES_DIR;
  }
  return join(ROOT, 'docs/sources');
}
function archived(urlPart) {
  const dir = sourcesDir();
  const manPath = join(dir, 'manifest.json');
  if (!existsSync(manPath)) return null;
  const man = JSON.parse(readFileSync(manPath, 'utf8')).sources;
  const e = man.find((m) => m.url.includes(urlPart) && m.status !== 'unfetchable');
  if (!e || !existsSync(join(dir, e.file))) return null;
  // pdftotext breaks lines inside words with a hyphen; join only those, and
  // collapse the rest of the whitespace.
  return readFileSync(join(dir, e.file), 'utf8')
    .replace(/(\w)-\n(\w)/g, '$1-$2').replace(/\s+/g, ' ');
}
const paper = archived('atc14-paper-ongaro.pdf');
const extended = archived('raft.github.io/raft.pdf');
const thesis = archived('OngaroPhD.pdf');
const tla = archived('raft.tla');
let archiveMissing = !paper || !extended || !thesis || !tla;

{
  // A transcription of the figure, made from the paper's page at 300 dots
  // per inch on 2026-10-07 and checked against the dissertation's Figure 3.7,
  // which draws the same five logs. Index 0 is S1. The leader is the server
  // drawn with the heavy border.
  const DRAWN = {
    a: { logs: ['12', '12', '1', '1', '1'], leader: 'S1' },
    b: { logs: ['12', '12', '1', '1', '13'], leader: 'S5' },
    c: { logs: ['124', '12', '12', '1', '13'], leader: 'S1' },
    d: { logs: ['13', '13', '13', '13', '13'], leader: 'S5' },
    e: { logs: ['124', '124', '124', '1', '13'], leader: 'S1' },
  };
  for (const panel of 'abcde') {
    const r = C.replay(5, C.figure8(panel), 'raft');
    const logs = r.state.s.map((x) => x.log.join(''));
    const lead = `S${C.leaderOf(r.state) + 1}`;
    check(`Figure 8 (${panel}): the engine's history reaches the drawn logs and leader`,
      r.ok && logs.join(' ') === DRAWN[panel].logs.join(' ') && lead === DRAWN[panel].leader,
      `${logs.join(' ')} led by ${lead}`);
    const typed = C.FIG8.find((q) => q.panel === panel);
    check(`Figure 8 (${panel}): and the engine's own copy of the figure is the transcription`,
      typed.logs.map((l) => l.join('')).join(' ') === DRAWN[panel].logs.join(' ')
        && `S${typed.leader + 1}` === DRAWN[panel].leader);
  }
  // The caption opens (b), (c) and (d) with a crash: "S1 crashes; S5 is
  // elected", "S5 crashes; S1 restarts", "If S1 crashes as in (d)". The
  // history the page replays tells it in that order, so its trail reads like
  // the sentence it quotes. Swapping the crash with the next step reaches the
  // same logs, which is why only this sees it.
  const opens = { b: 'P1', c: 'P5', d: 'P1' };
  for (const [panel, first] of Object.entries(opens)) {
    const typed = C.FIG8.find((q) => q.panel === panel);
    check(`Figure 8 (${panel}): the history opens with the crash the caption names first, ${first}`,
      typed.steps[0] === first, typed.steps.slice(0, 2).join(' '));
  }

  // (d) and (e) are alternatives from (c), as the dissertation's "or" draws
  // them: (e) is not reached through (d).
  const d = C.figure8('d'), e = C.figure8('e'), c = C.figure8('c');
  check('(d) and (e) both continue (c), and neither runs through the other',
    d.slice(0, c.length).join() === c.join() && e.slice(0, c.length).join() === c.join()
      && e.length < d.length && e.slice(c.length).join() !== d.slice(c.length, c.length + 2).join());

  // Who voted, from the caption.
  if (paper) {
    const b = /S5 is elected leader for term (\d) with votes from (S\d), (S\d), and itself/.exec(paper);
    const dd = /S5 could be elected leader \(with votes from (S\d), (S\d), and (S\d)\)/.exec(paper);
    check('the caption names the voters for (b) and (d)', Boolean(b && dd));
    if (b && dd) {
      const votersOf = (panel, leader) => {
        const r = C.replay(5, C.figure8(panel), 'raft');
        const t = r.state.s[leader].term;
        // Read the votes out of the history rather than the final state: in (d)
        // the voters later hear newer terms from nobody, but asking the trail
        // is what the caption describes.
        const got = new Set();
        r.trail.forEach((step) => step.events.forEach((w) => {
          const m = new RegExp(`^(S\\d) votes for S${leader + 1} in term ${t}$`).exec(w);
          if (m) got.add(m[1]);
        }));
        return { term: t, voters: [...got].sort() };
      };
      const vb = votersOf('b', 4);
      check(`(b): S5 leads term ${b[1]} with votes from ${b[2]} and ${b[3]}, as the caption says`,
        vb.term === Number(b[1]) && vb.voters.join() === [b[2], b[3]].sort().join(),
        `term ${vb.term}, voters ${vb.voters}`);
      const vd = votersOf('d', 4);
      check(`(d): S5's voters are ${dd[1]}, ${dd[2]} and ${dd[3]}, as the caption says`,
        vd.voters.join() === [dd[1], dd[2], dd[3]].sort().join(), `term ${vd.term}, voters ${vd.voters}`);
    }
    check('the caption says (c) holds the term-2 entry on a majority and not committed',
      /the log entry from term 2 has been replicated on a majority of the servers, but it is not committed/.test(paper));
    check('and that in (e) S5 cannot win an election',
      /\(S5 cannot win an election\)/.test(paper));
  }
  if (extended) {
    check('the extended version carries the same caption',
      /S5 could be elected leader \(with votes from S2, S3, and S4\)/.test(extended)
      && /S5 is elected leader for term 3 with votes from S3, S4, and itself/.test(extended));
  }
  if (thesis) {
    check('and the dissertation draws it as Figure 3.7, with (d1) and (d2)',
      /Figure 3\.7: A time sequence showing why a leader cannot determine commitment using log entries from older terms/.test(thesis)
      && /as in \(d1\)/.test(thesis) && /as in \(d2\)/.test(thesis));
  }
}

/* ==== 6. the paper says what the page says ================================= */
{
  const spec = JSON.parse(readFileSync(join(ROOT, 'machines/consensus.json'), 'utf8'));
  const prose = JSON.stringify(spec);
  const quotes = [...prose.matchAll(/&ldquo;(.+?)&rdquo;/g)].map((m) => m[1].replace(/&gt;/g, '>'));
  check('the page quotes the paper at least three times', quotes.length >= 3, String(quotes.length));
  if (paper) {
    quotes.forEach((q) => check(`quoted from the paper: "${q.slice(0, 50)}..."`, paper.includes(q)));
    // The same quotations, written out, so a test names each one: la-claims-audit
    // looks for the literal text in a test and a drifted quotation is a misattribution.
    for (const q of [
      'chosen randomly from a fixed interval (e.g., 150–300ms)',
      'act as a logical clock',
      'If there exists an N such that N > commitIndex, a majority of matchIndex[i] ≥ N, and log[N].term == currentTerm: set commitIndex = N',
    ]) {
      const flat = (t) => t.replace(/\s+/g, ' ');
      check(`pinned quotation is in the paper: "${q.slice(0, 40)}..."`, flat(paper).includes(flat(q)));
    }
    check('the timeout interval is 150–300ms in the paper',
      paper.includes('(e.g., 150–300ms)'));
    check('the five properties are named as the engine names them',
      C.PROPS.every((x) => paper.includes(`${x.name}:`)), C.PROPS.map((x) => x.name).join(', '));
    check('the conference is June 19–20, 2014, in Philadelphia',
      paper.includes('June 19–20, 2014 • Philadelphia, PA'));
    check('the commit rule in Figure 2 ends with the clause the page lets you remove',
      paper.includes('a majority of matchIndex[i] ≥ N, and log[N].term == currentTerm'));
    check('and the paper says the voter refuses a candidate whose log is behind',
      paper.includes('the voter denies its vote if its own log is more up-to-date than that of the candidate'));
    check('the paper says a crashed server restarts with its log, which this page draws as a cut',
      /S1 restarts, is elected leader/.test(paper));
    check('Viewstamped Replication is the algorithm the paper names as most like Raft',
      paper.includes('most notably, Oki and Liskov’s Viewstamped Replication'));
    check('the paper reports a TLA+ specification and a written proof of State Machine Safety',
      paper.includes('We have developed a formal specification and a proof of safety')
      && paper.includes('proof [28] of the State Machine Safety property'));
  }
  if (tla) {
    check('the TLA+ specification\'s commit rule carries the same clause',
      /log\[i\]\[Max\(agreeIndexes\)\]\.term = currentTerm\[i\]/.test(tla));
  }
  if (thesis) {
    check('the dissertation is dated August 2014', thesis.includes('August 2014'));
  }
}

/* ==== 7. break it on purpose =============================================== */
{
  // Each copy changes one rule. Every one must turn a load-time row red, and
  // the oracle must see the difference too. A replacement that finds nothing
  // is itself a failure, not a pass.
  const MUTANTS = [
    ['the commit rule loses its term clause',
      'if (rule === "raft" && me.log[N - 1] !== me.term) continue;', ''],
    ['a voter ignores how up to date the candidate is',
      'if (!atLeastAsUpToDate(c.log, v.log)) {', 'if (false) {'],
    ['a voter votes twice in a term',
      'if (vVoted !== -1 && vVoted !== i) {', 'if (false) {'],
    ['a majority is half, rounded down',
      'return Math.floor(n / 2) + 1;', 'return Math.floor(n / 2);'],
    ['a follower keeps its conflicting entries',
      'you.log.length = x;', ''],
    ['the up-to-date test compares lengths only',
      'if (a !== b) return a > b;', ''],
    ['a leader that hears a newer term carries on',
      'adopt(me, you.term);\n        return done(st, nx, act, rule, ev, { stale: true }, quick);',
      'return refuse("ignored");'],
  ];
  for (const [what, from, to] of MUTANTS) {
    if (!SRC.includes(from)) { check(`mutant "${what}" applies`, false, 'its target text is gone'); continue; }
    const M = engine(SRC.replace(from, to));
    let rows;
    try { rows = M.verify(); } catch (e) { rows = null; }
    check(`broken on purpose, ${what}: verify() says no on some row`,
      Array.isArray(rows) && rows.some((r) => !r.ok), rows ? rows.filter((r) => !r.ok).length + ' rows say no' : 'it threw');
    // And the oracle notices, on its own search, without asking verify().
    let differs = false;
    for (const rule of ['raft']) {
      // Bounded: a mutant can make the space explode, and a state count past
      // twice the oracle's is already a difference.
      const eng = M.check({ ...BOX, rule, symmetry: false, collect: true,
                            limit: 2 * results.raft.orc.seen.size });
      if (eng.aborted) { differs = true; break; }
      const set = new Set(eng.kept.map(neutralFromEngine));
      if (set.size !== results.raft.orc.seen.size
        || [...set].some((k) => !results.raft.orc.seen.has(k))) differs = true;
    }
    const w = walk(M, 20);
    check(`  and the oracle sees it, in the state space or in the walk`,
      differs || w.mismatches > 0, `state space ${differs ? 'differs' : 'same'}, `
        + `${w.mismatches} walks part from the oracle`);
  }
}

/* ==== 8. a check that ran on nothing says so ================================ */
{
  // An engine that can take no step explores one state. Every property row
  // must then say not tested, never yes.
  const from = 'function actions(st, bounds) {\n    var out = [], i, j, n = st.n;';
  check('the vacuity mutant applies', SRC.includes(from));
  const M = engine(SRC.replace(from, `${from}\n    return out;`));
  const rows = M.verify();
  const props = rows.filter((r) => /holds in every state/.test(r.claim));
  check('with nothing reachable, no property row says yes',
    props.length === 5 && props.every((r) => !r.ok), props.map((r) => `${r.ok}/${r.untested}`).join(' '));
  check('and the ones with nothing to check say not tested',
    props.filter((r) => r.untested).length >= 4, props.map((r) => r.detail).join(' | '));
}

/* ==== 9. what the page says, against what the engine does ================== */
{
  // A refusal does not use up a vote. S4 asks S3 first and is refused for its
  // log; S1 asks next, in the same term, and gets the vote. A sentence saying
  // a server votes for "whichever candidate asks first" is false here.
  const h = ['T2', 'V21', 'V23', 'W2', 'A21', 'A23', 'T4', 'T4', 'T1', 'V43', 'V13'];
  const r = C.replay(5, h, 'raft');
  const last = r.ok ? r.trail.slice(-2).map((t) => t.events.join('; ')) : [];
  check('a voter that refuses the first candidate for its log still votes for the next, in the same term',
    r.ok && /S3 refuses S4: its last entry/.test(last[0]) && /S3 votes for S1 in term 2/.test(last[1]),
    last.join(' || '));
  const spec = readFileSync(join(ROOT, 'machines/consensus.json'), 'utf8');
  check('and the page does not say a server votes for whichever candidate asks first',
    !/whichever candidate asks first/.test(spec) && /Refusing a candidate does not use up its vote/.test(spec));
  // "Behind" on this page means older: a log behind another. The term-4
  // entry in (e) comes after the term-2 one, so it is not behind it.
  const row = C.verify().find((x) => /in \(c\) the term-2 entry/.test(x.claim));
  check('the (c) and (e) row says the term-4 entry comes after the term-2 one',
    !!row && /entry from term 4 after it/.test(row.claim) && !/behind/.test(row.claim), row && row.claim);
  // The grid's mark is said to a sighted reader, not only in a hidden caption.
  check('the log grid says what its heavy border means, outside the screen-reader caption',
    /<p class=\\"rf-caption\\">Every server's log\.[^<]*heavy border marks a committed entry/.test(spec));
  // 15,675 is a count of states with renamings merged. Three servers reach
  // more states than that once each naming counts (the oracle's own search,
  // section 2), so a row saying "all 15,675 states three servers can reach"
  // is false. Each property row must say how it counted.
  const g = C.check({ ...BOX, rule: 'raft' });
  const g2 = C.check({ ...C.LOAD2, rule: 'raft' });
  const propRows = C.verify().filter((x) => /^(Election Safety|Leader Append-Only|Log Matching|Leader Completeness|State Machine Safety) /.test(x.claim));
  // Log Matching and Leader Append-Only are read off the second box.
  const boxOf = (x) => (/^(Log Matching|Leader Append-Only) /.test(x.claim) ? g2 : g);
  check('the property rows say their count merges renamings, and the unmerged count is larger',
    propRows.length === 5 && results.raft.orc.seen.size > g.states
      && propRows.every((x) => !/in all [\d,]+ states three servers can reach/.test(x.claim)
        && x.claim.includes(`${boxOf(x).states.toLocaleString('en-US')} states, counting a renaming of the servers as the same state`)),
    `${results.raft.orc.seen.size} named states, ${g.states} merged; ${propRows[0] && propRows[0].claim}`);
  check('and the hint beside the readouts says the numbers are counted that way',
    /It counts two states as one when they differ only in which server is called which, and the numbers below are counted that way/.test(spec));
  // A proof is the other way to say the clause makes the difference; the
  // page itself cites one, so "every history has to be tried" is false.
  check('the page does not say every history has to be tried',
    !/every history has to be tried/.test(spec) && /takes a proof, or trying every history/.test(spec));
}

/* ==== 10. a row that cannot fail is not a check ========================== */
// Red team, 2026-10-08. With one entry per log, Log Matching has no earlier
// entry to compare and Leader Append-Only never sees a leader write into a
// non-empty log, so both rows said yes on code that could not fail there.
// They are now read off a second box, terms up to 2 with two entries per log.
// Each block below breaks something on purpose and names the row that must
// say no.
{
  const BOX2 = C.LOAD2;
  check('the second box is three servers, terms up to 2, two entries per log',
    BOX2.n === 3 && BOX2.maxTerm === 2 && BOX2.maxLog === 2, JSON.stringify(BOX2));

  // The first box really is vacuous for both: every log has at most one entry.
  const first = C.check({ ...BOX, rule: 'raft', collect: true });
  const longest = Math.max(...first.kept.map((st) => Math.max(...st.s.map((x) => x.log.length))));
  check('in the first box no log ever holds two entries, so Log Matching has nothing to check there',
    longest === 1 && first.tested.matching === 0, `longest ${longest}, ${first.tested.matching} counted`);

  // The second box, against the oracle: same states, same verdicts.
  const eng = C.check({ ...BOX2, rule: 'raft', symmetry: false, collect: true });
  const orc = oSearch(BOX2.n, BOX2.maxTerm, BOX2.maxLog, 'raft');
  const engSet = new Set(eng.kept.map(neutralFromEngine));
  check('second box: the engine and the message-level oracle reach exactly the same states',
    engSet.size === orc.seen.size && [...engSet].every((k) => orc.seen.has(k)) && engSet.size === eng.states,
    `engine ${eng.states}, oracle ${orc.seen.size}`);
  let deep = 0, disagree = 0;
  for (const [, c] of orc.seen) {
    const S = c.servers;
    let pair = false;
    for (let a = 0; a < c.n && !pair; a += 1) for (let b = a + 1; b < c.n && !pair; b += 1) {
      for (let x = 2; x <= Math.min(S[a].log.length, S[b].log.length); x += 1) {
        if (S[a].log[x - 1].term === S[b].log[x - 1].term) pair = true;
      }
    }
    if (pair) deep += 1;
    if ([...oBroken(c, null)].sort().join() !== C.broken(toEngineState(c), null).map((b) => b.prop).sort().join()) disagree += 1;
  }
  check('second box: nothing broken, and the property checkers agree in every state',
    orc.broken.size === 0 && !eng.failed && disagree === 0, `${disagree} disagree`);
  check('second box: the oracle finds states where two logs agree at index 2 or later',
    deep > 0, `${deep} of ${orc.seen.size} named states`);
  const g2 = C.check({ ...BOX2, rule: 'raft' });
  check('second box: 1,480 states with renamings merged',
    g2.states === 1480 && g2.tested.matching > 0 && g2.tested.append > 0,
    `${g2.states}, matching ${g2.tested.matching}, append ${g2.tested.append}`);

  // The property checkers themselves, on states built by hand. If the Log
  // Matching or Leader Append-Only check is switched off, these fail.
  const st = C.fresh(3);
  st.s[0].log = [1, 2]; st.s[1].log = [2, 2];
  check('broken() sees two logs that agree at index 2 and differ at index 1',
    C.broken(st, null).some((b) => b.prop === 'matching'), JSON.stringify(C.broken(st, null)));
  const was = C.fresh(3);
  was.s[0].term = 2; was.s[0].role = 'L'; was.s[0].log = [1]; was.s[0].match = [0, 0, 0];
  const now = C.copy(was); now.s[0].log = [2];
  check('broken() sees a leader that overwrote an entry in its own term',
    C.broken(now, was).some((b) => b.prop === 'append'), JSON.stringify(C.broken(now, was)));

  // Engines broken on purpose. Each must turn its own row red at load.
  const rowFor = (rows, name) => rows.find((r) => r.claim.startsWith(name + ' '));
  const MUT = [
    ['a leader does not back off to where the logs agree', 'Log Matching',
      'while (p > 0 && you.log[p - 1] !== me.log[p - 1]) p -= 1;', ''],
    ['a follower keeps its conflicting entries', 'Log Matching',
      'you.log.length = x;', ''],
    ['a client write overwrites the leader\'s newest entry', 'Leader Append-Only',
      'me.log.push(me.term);',
      'if (me.log.length) me.log[me.log.length - 1] = me.term; else me.log.push(me.term);'],
    ['the Log Matching check is switched off', 'Log Matching',
      'if (A[x - 1] !== B[x - 1]) continue;', 'if (true) continue;'],
    ['the Leader Append-Only check is switched off', 'Leader Append-Only',
      'if (!kept) out.push(', 'if (false) out.push('],
  ];
  for (const [what, prop, from, to] of MUT) {
    if (!SRC.includes(from)) { check(`mutant "${what}" applies`, false, 'its target text is gone'); continue; }
    const M = engine(SRC.replace(from, to));
    let rows = null;
    try { rows = M.verify(); } catch (e) { rows = null; }
    const row = rows && rowFor(rows, prop);
    // A switched-off check makes the engine right and the detector blind, so
    // the rows stay green; the hand-built states above are what catch it.
    if (/switched off/.test(what)) {
      const s2 = C.fresh(3); s2.s[0].log = [1, 2]; s2.s[1].log = [2, 2];
      const caught = prop === 'Log Matching'
        ? M.broken(s2, null).some((b) => b.prop === 'matching')
        : M.broken(now, was).some((b) => b.prop === 'append');
      check(`broken on purpose, ${what}: the hand-built state shows it`, !caught,
        'expected the mutant to miss it (this is the proof the test above can fail)');
      continue;
    }
    check(`broken on purpose, ${what}: the ${prop} row says no`,
      !!row && !row.ok, row ? `${row.detail}` : 'no such row');
    if (prop === 'Leader Append-Only') {
      // And the first box alone could not have seen it.
      const r1 = M.check({ ...BOX, rule: 'raft' });
      check('  and the first box alone finds nothing wrong with it', !r1.failed,
        r1.failed ? r1.failed.broken[0].text : `${r1.states} states`);
    }
  }
}

/* ==== 11. the clause as written, not a near miss ========================== */
// Red team, 2026-10-08. Testing the term of the leader's newest entry instead
// of log[N] gives the same 15,675 states for three servers and was green at
// load. Five servers tell them apart, from Figure 8 (c).
{
  const from = 'if (rule === "raft" && me.log[N - 1] !== me.term) continue;';
  const to = 'if (rule === "raft" && me.log[me.log.length - 1] !== me.term) continue;';
  check('the newest-entry mutant applies', SRC.includes(from));
  const M = engine(SRC.replace(from, to));
  const g = M.check({ ...BOX, rule: 'raft' });
  check('three servers cannot tell the newest-entry rule from the clause: same count, nothing broken',
    g.states === 15675 && !g.failed, `${g.states}`);
  const h = C.figure8('c').concat(C.NEWEST);
  const real = C.replay(5, h, 'raft'), bad = M.replay(5, h, 'raft');
  check('from (c), the clause as written breaks nothing on that history',
    real.ok && real.firstBroken === null, real.ok ? 'ok' : real.why);
  check('and the newest-entry rule breaks Leader Completeness at step 37',
    bad.ok && bad.firstBroken === 36 && bad.trail[36].broken.some((b) => b.prop === 'completeness'),
    bad.ok && bad.firstBroken !== null ? `${bad.firstBroken + 1}: ${bad.trail[bad.firstBroken].broken[0].text}` : 'nothing broke');
  // The oracle, written from Figure 2, agrees with the real engine there.
  let c = oCluster(5), oBad = -1;
  h.forEach((nm, z) => {
    const before = c;
    c = oApply(c, toOracleAct(C.parse(nm)), 'raft');
    if (oBad < 0 && oBroken(c, before).size) oBad = z;
  });
  check('the oracle replays it under Raft\'s rule with nothing broken', oBad === -1, String(oBad));
  const rows = M.verify();
  const row = rows.find((r) => r.claim.startsWith('the clause tests the term of the entry being counted'));
  check('the load-time row for it says no under the newest-entry rule',
    !!row && !row.ok, row ? row.detail : 'no such row');
  const real13 = C.verify().find((r) => r.claim.startsWith('the clause tests the term of the entry being counted'));
  check('and yes under the real one', !!real13 && real13.ok, real13 ? real13.detail : 'no such row');
}

/* ==== 12. the counterexample's trail says what happened ================== */
// Red team, 2026-10-08. In the 13-step history S1 is a leader when it sends
// its late vote requests; the trail called it the candidate and said it
// stopped standing.
{
  const b = C.check({ ...BOX, rule: 'majority' });
  const r = C.replay(3, b.trace, 'majority');
  const lines = r.trail.map((t) => t.events.join('; '));
  check('step 5: the leader of term 1 hears term 2 and steps down',
    /S1, which leads term 1, hears term 2 and steps down/.test(lines[4]) && !/stops standing/.test(lines[4]), lines[4]);
  let wrong = 0;
  r.trail.forEach((t, z) => {
    const a = C.parse(t.act);
    if (a.k === 'V' && t.before.s[a.i].role === 'L' && /candidate/.test(lines[z])) wrong += 1;
  });
  check('no step sent by a leader calls it the candidate', wrong === 0, `${wrong} steps`);
  check('step 11 says the leader\'s log, not the candidate\'s',
    /the leader's is from term 1/.test(lines[10]), lines[10]);
  // Step 5 is a request S2 already answered at step 2: a duplicate. The
  // ledger has to allow for it.
  const st2 = r.trail[1].events.join(' '), st5 = r.trail[4];
  check('step 5 repeats the request S2 answered at step 2', r.trail[1].act === 'V12' && st5.act === 'V12'
    && /S2 votes for S1 in term 1/.test(st2), `${r.trail[1].act} ${st5.act}`);
  const spec = readFileSync(join(ROOT, 'machines/consensus.json'), 'utf8');
  check('and the ledger says a late request can be a second copy, counted in the totals',
    /a late request can also be a second copy of one already answered, and the counts include the states reached that way/.test(spec));
  check('the lede says every history of this model, a message and its reply as one step',
    /tries every history of this model that three servers can reach in four terms, with one entry per log and each message delivered with its reply in one step/.test(spec));
  check('and so does the hint beside the checker',
    /That is every history of this model, where a message and its reply are one step, and not every history a real network allows/.test(spec));
  check('the hint says Log Matching and Leader Append-Only come from a second search',
    /reads those two from a second search, terms up to two with two entries per log/.test(spec)
      && C.LOAD2.maxTerm === 2 && C.LOAD2.maxLog === 2);
}

if (archiveMissing) {
  f += 1;
  console.error('  FAIL archive missing: run la-source-audit --archive'
    + ' (or point LA_SOURCES_DIR at a copy laid out the same way)');
}
console.log(`\nconsensus: ${p} passed, ${f} failed`);
process.exit(f ? 1 : 0);