// tests/lib/red-proof.test.mjs
// Proof of red (P9 (1)): the step's test is run by a command against the start
// point, where it must FAIL, and against the result, where it must PASS. The
// model's word that "the test was red first" is never the proof.
// Exit 0 = proven, 1 = rejected (green at the start point, or red at the result),
// 2 = could not run (never green).

import { test } from 'node:test';
import { strict as assert } from 'node:assert';
import { spawnSync } from 'node:child_process';
import { mkdirSync, mkdtempSync, readFileSync, rmSync, writeFileSync } from 'node:fs';
import { tmpdir } from 'node:os';
import { dirname, join } from 'node:path';
import { fileURLToPath } from 'node:url';
import { proveRed } from '../../lib/verification/red-proof.mjs';

const HERE = dirname(fileURLToPath(import.meta.url));
const ROOT = join(HERE, '..', '..');
const CLI = join(ROOT, 'lib', 'verification', 'red-proof.mjs');
const TEST_CMD = 'node --test tests/sum.test.mjs';

const SUM_TEST = [
  "import { test } from 'node:test';",
  "import { strict as assert } from 'node:assert';",
  "import { sum } from '../lib/sum.mjs';",
  "test('sum adds', () => { assert.equal(sum(1, 2), 3); });",
  '',
].join('\n');

function sh(cwd, cmd, args) {
  const r = spawnSync(cmd, args, { cwd, encoding: 'utf8' });
  assert.equal(r.status, 0, `${cmd} ${args.join(' ')}: ${r.stderr}`);
  return r.stdout.trim();
}

/** A repo whose base commit has `body` as sum(); returns {dir, base}. */
function repo(body) {
  const dir = mkdtempSync(join(tmpdir(), 'red-proof-'));
  sh(dir, 'git', ['init', '-q']);
  sh(dir, 'git', ['config', 'user.email', 't@example.invalid']);
  sh(dir, 'git', ['config', 'user.name', 'test']);
  mkdirSync(join(dir, 'lib'));
  writeFileSync(join(dir, 'lib', 'sum.mjs'), `export function sum(a, b) { return ${body}; }\n`);
  sh(dir, 'git', ['add', 'lib/sum.mjs']);
  sh(dir, 'git', ['commit', '-q', '-m', 'base']);
  return { dir, base: sh(dir, 'git', ['rev-parse', 'HEAD']) };
}

function addTest(dir) {
  mkdirSync(join(dir, 'tests'), { recursive: true });
  writeFileSync(join(dir, 'tests', 'sum.test.mjs'), SUM_TEST);
}

function cli(args) {
  const r = spawnSync(process.execPath, [CLI, ...args], { encoding: 'utf8' });
  return { status: r.status, stdout: r.stdout, stderr: r.stderr };
}

test('red proof: red at the start point, green at the result -> proven, exit 0', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    writeFileSync(join(dir, 'lib', 'sum.mjs'), 'export function sum(a, b) { return a + b; }\n');
    const r = proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] });
    assert.equal(r.status, 'proven', JSON.stringify(r));
    assert.notEqual(r.base.exit, 0);
    assert.equal(r.result.exit, 0);
    const c = cli(['--cwd', dir, '--base', base, '--cmd', TEST_CMD, '--tests', 'tests/sum.test.mjs', '--json']);
    assert.equal(c.status, 0, c.stdout + c.stderr);
    assert.equal(JSON.parse(c.stdout).status, 'proven');
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: a test that already PASSES at the start point is rejected, exit 1', () => {
  const { dir, base } = repo('a + b');
  try {
    addTest(dir);
    const r = proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] });
    assert.equal(r.status, 'rejected');
    assert.equal(r.reason, 'not-red-at-base');
    const c = cli(['--cwd', dir, '--base', base, '--cmd', TEST_CMD, '--tests', 'tests/sum.test.mjs']);
    assert.equal(c.status, 1, c.stdout + c.stderr);
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: a test that still FAILS at the result is rejected, exit 1', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    const r = proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] });
    assert.equal(r.status, 'rejected');
    assert.equal(r.reason, 'not-green-at-result');
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof --red-only: the gate before building - red at the start point only, the result is not run', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir); // test written, nothing built yet: the working tree is still red
    const r = proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'], redOnly: true });
    assert.equal(r.status, 'proven', JSON.stringify(r));
    assert.equal(r.result, undefined, '--red-only never runs the result');
    const c = cli(['--red-only', '--cwd', dir, '--base', base, '--cmd', TEST_CMD, '--tests', 'tests/sum.test.mjs']);
    assert.equal(c.status, 0, c.stdout + c.stderr);
  } finally { rmSync(dir, { recursive: true, force: true }); }
  const green = repo('a + b');
  try {
    addTest(green.dir);
    const r = proveRed({ cwd: green.dir, base: green.base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'], redOnly: true });
    assert.equal(r.reason, 'not-red-at-base');
  } finally { rmSync(green.dir, { recursive: true, force: true }); }
});

test('red proof: what cannot be measured is "not-run", exit 2 - never proven', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    writeFileSync(join(dir, 'lib', 'sum.mjs'), 'export function sum(a, b) { return a + b; }\n');
    const args = (over) => ['--cwd', dir, '--base', base, '--cmd', TEST_CMD, '--tests', 'tests/sum.test.mjs', ...over];
    // A command outside the test-runner allowlist never reaches a shell.
    assert.equal(proveRed({ cwd: dir, base, cmd: 'node tests/sum.test.mjs', tests: ['tests/sum.test.mjs'] }).status, 'not-run');
    assert.equal(proveRed({ cwd: dir, base, cmd: `${TEST_CMD} || true`, tests: ['tests/sum.test.mjs'] }).status, 'not-run');
    // An unknown start point, a missing test file, no test file at all.
    assert.equal(proveRed({ cwd: dir, base: 'no-such-ref', cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] }).status, 'not-run');
    assert.equal(proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/missing.test.mjs'] }).status, 'not-run');
    assert.equal(proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: [] }).status, 'not-run');
    assert.equal(cli(args([])).status, 0, 'control: the same arguments do prove');
    assert.equal(cli(['--cwd', dir, '--base', base, '--cmd', TEST_CMD]).status, 2, 'no --tests');
    assert.equal(cli(['--cwd', join(dir, 'nope'), '--base', base, '--cmd', TEST_CMD, '--tests', 'tests/sum.test.mjs']).status, 2);
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: --cwd in a subdirectory still runs at the repo root (plan paths are root-relative)', () => {
  // Measured 2026-10-06: `git archive` run from a subdirectory packs only that
  // subdirectory, so a start point built from a subdir cwd would miss lib/.
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    writeFileSync(join(dir, 'lib', 'sum.mjs'), 'export function sum(a, b) { return a + b; }\n');
    mkdirSync(join(dir, 'docs'));
    const r = proveRed({ cwd: join(dir, 'docs'), base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] });
    assert.equal(r.status, 'proven', JSON.stringify({ status: r.status, reason: r.reason }));
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

// Review finding 2 (2026-10-06): a start-point copy that cannot run the test at
// all failed "red" for the wrong reason and was called proven. Three guards:
// the copy is a real git checkout, gitignored dependency dirs are linked in, and
// the same copy WITH the change must go green (the control run).

test('red proof: a gitignored dependency the test needs is linked into the start point - no false red', () => {
  const { dir, base } = repo('a + b');
  try {
    writeFileSync(join(dir, '.gitignore'), 'node_modules/\n');
    sh(dir, 'git', ['add', '.gitignore']);
    sh(dir, 'git', ['commit', '-q', '-m', 'ignore']);
    const base2 = sh(dir, 'git', ['rev-parse', 'HEAD']);
    mkdirSync(join(dir, 'node_modules', 'dep'), { recursive: true });
    writeFileSync(join(dir, 'node_modules', 'dep', 'index.mjs'), 'export const one = 1;\n');
    mkdirSync(join(dir, 'tests'));
    writeFileSync(join(dir, 'tests', 'dep.test.mjs'), [
      "import { test } from 'node:test';",
      "import { strict as assert } from 'node:assert';",
      "import { one } from '../node_modules/dep/index.mjs';",
      "import { sum } from '../lib/sum.mjs';",
      "test('dep', () => { assert.equal(sum(one, one), 2); });",
      '',
    ].join('\n'));
    // The test already passes without any change: it proves nothing.
    const r = proveRed({ cwd: dir, base: base2, cmd: 'node --test tests/dep.test.mjs', tests: ['tests/dep.test.mjs'] });
    assert.equal(r.status, 'rejected', JSON.stringify({ status: r.status, reason: r.reason }));
    assert.equal(r.reason, 'not-red-at-base');
    void base;
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: the start point is a git checkout - a git-reading command does not fail there for lack of .git', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    const r = proveRed({ cwd: dir, base, cmd: 'git status', tests: ['tests/sum.test.mjs'] });
    assert.notEqual(r.status, 'proven', JSON.stringify({ status: r.status, reason: r.reason }));
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: a copy that cannot go green even with the change is "not-run" (environment), never proven', () => {
  const { dir, base } = repo('a - b');
  try {
    mkdirSync(join(dir, 'tests'));
    // Red anywhere outside the real working tree, whatever the code says.
    writeFileSync(join(dir, 'tests', 'env.test.mjs'), [
      "import { test } from 'node:test';",
      "import { strict as assert } from 'node:assert';",
      "test('env', () => { assert.ok(!process.cwd().includes('voyage-red-proof-')); });",
      '',
    ].join('\n'));
    writeFileSync(join(dir, 'lib', 'sum.mjs'), 'export function sum(a, b) { return a + b; }\n');
    const r = proveRed({ cwd: dir, base, cmd: 'node --test tests/env.test.mjs', tests: ['tests/env.test.mjs'] });
    assert.equal(r.status, 'not-run', JSON.stringify({ status: r.status, reason: r.reason }));
    assert.match(r.reason, /control/);
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: an untracked file the change adds (not a listed test) is part of the result, so the control run goes green', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    // The fix lives in a NEW untracked module the step adds.
    writeFileSync(join(dir, 'lib', 'add.mjs'), 'export const add = (a, b) => a + b;\n');
    writeFileSync(join(dir, 'lib', 'sum.mjs'), "export { add as sum } from './add.mjs';\n");
    const r = proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] });
    assert.equal(r.status, 'proven', JSON.stringify({ status: r.status, reason: r.reason }));
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

test('red proof: the start-point run leaves the working tree untouched', () => {
  const { dir, base } = repo('a - b');
  try {
    addTest(dir);
    writeFileSync(join(dir, 'lib', 'sum.mjs'), 'export function sum(a, b) { return a + b; }\n');
    const before = sh(dir, 'git', ['status', '--porcelain']);
    proveRed({ cwd: dir, base, cmd: TEST_CMD, tests: ['tests/sum.test.mjs'] });
    assert.equal(sh(dir, 'git', ['status', '--porcelain']), before);
    assert.equal(readFileSync(join(dir, 'lib', 'sum.mjs'), 'utf8'), 'export function sum(a, b) { return a + b; }\n');
  } finally { rmSync(dir, { recursive: true, force: true }); }
});

// Reuse of tests/fixtures/red-first/02243c6-always-allow-shim.mjs: the measured
// red-first claim of 02243c6 ("6 of 55"), re-run through red-proof instead of by
// hand. Needs this repo's git history; a `git archive` tree has none, and there
// the test says so and skips rather than pretending to pass.
const HAS_HISTORY = spawnSync('git', ['cat-file', '-e', '02243c6^{commit}'], { cwd: ROOT }).status === 0;

test('red proof: reproduces the 02243c6 red-first measurement (6 of 55) and the bare load error (1 of 1)', { skip: !HAS_HISTORY && 'no git history (git archive tree)' }, () => {
  const dir = mkdtempSync(join(tmpdir(), 'red-proof-02243c6-'));
  const RUNNER = 'lib/verification/criteria-runner.mjs';
  const TEST_FILE = 'tests/lib/criteria-runner.test.mjs';
  const tar = join(dir, '..', `${dir.split('/').pop()}.tar`);
  try {
    sh(ROOT, 'git', ['archive', '--format=tar', '-o', tar, '02243c6']);
    sh(dir, 'tar', ['-xf', tar]);
    const parent = spawnSync('git', ['show', `02243c6^:${RUNNER}`], { cwd: ROOT, encoding: 'utf8' }).stdout;
    const real = readFileSync(join(dir, RUNNER), 'utf8');
    const shim = readFileSync(join(ROOT, 'tests', 'fixtures', 'red-first', '02243c6-always-allow-shim.mjs'), 'utf8');
    sh(dir, 'git', ['init', '-q']);
    sh(dir, 'git', ['config', 'user.email', 't@example.invalid']);
    sh(dir, 'git', ['config', 'user.name', 'test']);
    sh(dir, 'git', ['add', '.']);
    // Start point 1: the parent's runner as it was - the test file cannot even load.
    writeFileSync(join(dir, RUNNER), parent);
    sh(dir, 'git', ['commit', '-q', '-am', 'parent runner']);
    const bare = sh(dir, 'git', ['rev-parse', 'HEAD']);
    // Start point 2: the parent's runner plus the always-allow shim.
    writeFileSync(join(dir, RUNNER), parent + shim);
    sh(dir, 'git', ['commit', '-q', '-am', 'parent runner + shim']);
    const shimmed = sh(dir, 'git', ['rev-parse', 'HEAD']);
    writeFileSync(join(dir, RUNNER), real);
    const cmd = `node --test --test-reporter=tap ${TEST_FILE}`;
    const withShim = proveRed({ cwd: dir, base: shimmed, cmd, tests: [TEST_FILE] });
    assert.equal(withShim.status, 'proven', JSON.stringify(withShim));
    assert.deepEqual(withShim.base.tap, { tests: 55, fail: 6 });
    assert.deepEqual(withShim.result.tap, { tests: 55, fail: 0 });
    // Only the start point matters here; the result run above already showed 0 of 55.
    const bareRun = proveRed({ cwd: dir, base: bare, cmd, tests: [TEST_FILE], redOnly: true });
    assert.equal(bareRun.status, 'proven');
    assert.deepEqual(bareRun.base.tap, { tests: 1, fail: 1 }, 'the parent tree fails as ONE load error, not as named tests');
  } finally {
    rmSync(dir, { recursive: true, force: true });
    rmSync(tar, { force: true });
  }
});