tessellate 0.1.0

use serde_json::Value;
use std::fs;
use std::io::Write;
use std::path::{Path, PathBuf};
use std::process::{Command, Output, Stdio};
use std::sync::atomic::{AtomicU64, Ordering};
use std::sync::{Mutex, MutexGuard};

static NEXT_DIRECTORY: AtomicU64 = AtomicU64::new(0);
static SOLVER_TEST_LOCK: Mutex<()> = Mutex::new(());

fn solver_test_guard() -> MutexGuard<'static, ()> {
    SOLVER_TEST_LOCK
        .lock()
        .unwrap_or_else(std::sync::PoisonError::into_inner)
}

const VALID_SOURCE: &str = r"module sample

enum Answer {
  Yes,
  No,
}

entity Subject {
  flag: Bool,
}

decision outcome(Subject s) -> Answer

rule yes(Subject s):
  when s.flag
  then outcome(s) = Yes

rule no(Subject s):
  when not s.flag
  then outcome(s) = No

case yes_case:
  let s = Subject {
    flag: true,
  }
  expect outcome(s) = Yes

invariant total:
  for all s: Subject
  exactly one outcome(s)
";

const BROKEN_ANALYSIS_SOURCE: &str = r"module sample

enum Answer {
  Yes,
  No,
}

entity Subject {
  flag: Bool,
}

decision outcome(Subject s) -> Answer

rule yes(Subject s):
  when s.flag
  then outcome(s) = Yes

invariant total:
  for all s: Subject
  exactly one outcome(s)
";

const BATCH_RUN_SOURCE: &str = r"module batch

enum Answer {
  Yes,
  No,
}

entity Subject {
  flag: Bool,
}

decision primary(Subject s) -> Answer
decision review(Subject s) -> Answer

rule primary_yes(Subject s):
  when s.flag
  then primary(s) = Yes

rule primary_no(Subject s):
  when not s.flag
  then primary(s) = No

rule review_all(Subject s):
  when true
  then review(s) = Yes

case z_case:
  let s = Subject {
    flag: true,
  }
  expect primary(s) = No
  expect review(s) = No

case a_case:
  let s = Subject {
    flag: false,
  }
  expect primary(s) = Yes
  expect review(s) = No
";

const EXPLANATION_STATES_SOURCE: &str = r"module explanation_states

enum Answer {
  Yes,
  No,
}

entity Subject {
  flag: Bool,
  alternate: Bool,
  maybe_flag: Bool?,
}

decision resolved(Subject s) -> Answer
decision empty(Subject s) -> Answer
decision uncertain(Subject s) -> Answer
decision disputed(Subject s) -> Answer
decision replaced(Subject s) -> Answer

rule resolved_yes(Subject s):
  when s.flag
  then resolved(s) = Yes

rule uncertain_yes(Subject s):
  when s.maybe_flag
  then uncertain(s) = Yes

rule disputed_yes(Subject s):
  when s.flag
  then disputed(s) = Yes

rule disputed_no(Subject s):
  when s.alternate
  then disputed(s) = No

rule replaced_base(Subject s):
  when s.flag
  then replaced(s) = No

rule replaced_exception(Subject s):
  when s.flag and s.alternate
  then replaced(s) = Yes
  then override replaced_base

case all_states:
  let s = Subject {
    flag: true,
    alternate: true,
  }
  expect resolved(s) = Yes
  expect empty(s) = Yes
  expect uncertain(s) = Yes
  expect disputed(s) = Yes
  expect replaced(s) = Yes
";

struct TestDirectory {
    path: PathBuf,
}

impl TestDirectory {
    fn new() -> Self {
        let ordinal = NEXT_DIRECTORY.fetch_add(1, Ordering::Relaxed);
        let path =
            std::env::temp_dir().join(format!("tess-cli-tests-{}-{ordinal}", std::process::id()));
        fs::create_dir_all(&path).unwrap();
        Self { path }
    }

    fn write(&self, name: &str, contents: &str) -> PathBuf {
        let path = self.path.join(name);
        if let Some(parent) = path.parent() {
            fs::create_dir_all(parent).unwrap();
        }
        fs::write(&path, contents).unwrap();
        path
    }
}

impl Drop for TestDirectory {
    fn drop(&mut self) {
        let _ = fs::remove_dir_all(&self.path);
    }
}

fn tess(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_without_path(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env("PATH", "/definitely-not-present")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_with_automatic_color(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env_remove("NO_COLOR")
        .env_remove("CLICOLOR")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_with_forced_color(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env_remove("NO_COLOR")
        .env_remove("CLICOLOR")
        .env("CLICOLOR_FORCE", "1")
        .output()
        .unwrap()
}

fn tess_with_no_color_and_force(arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env("CLICOLOR_FORCE", "1")
        .output()
        .unwrap()
}

fn tess_in(directory: &Path, arguments: &[&str]) -> Output {
    Command::new(env!("CARGO_BIN_EXE_tess"))
        .current_dir(directory)
        .args(arguments)
        .env("NO_COLOR", "1")
        .env_remove("CLICOLOR_FORCE")
        .output()
        .unwrap()
}

fn tess_with_stdin(arguments: &[&str], stdin: &[u8]) -> Output {
    let mut child = Command::new(env!("CARGO_BIN_EXE_tess"))
        .args(arguments)
        .env("NO_COLOR", "1")
        .env_remove("CLICOLOR_FORCE")
        .stdin(Stdio::piped())
        .stdout(Stdio::piped())
        .stderr(Stdio::piped())
        .spawn()
        .unwrap();
    child.stdin.take().unwrap().write_all(stdin).unwrap();
    child.wait_with_output().unwrap()
}

fn path(path: &Path) -> &str {
    path.to_str().unwrap()
}

fn stdout(output: &Output) -> String {
    String::from_utf8(output.stdout.clone()).unwrap()
}

fn stderr(output: &Output) -> String {
    String::from_utf8(output.stderr.clone()).unwrap()
}

fn workspace_root() -> PathBuf {
    PathBuf::from(env!("CARGO_MANIFEST_DIR")).join("../..")
}

#[test]
fn validate_emits_success_and_failure_json_envelopes() {
    let directory = TestDirectory::new();
    let valid = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["validate", path(&valid)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), format!("validated {}\n", valid.display()));

    let output = tess(&["validate", path(&valid), "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], true);
    assert_eq!(json["command"], "validate");

    let invalid = directory.write("invalid.tes", "module invalid\nenum E { A B }\n");
    let output = tess(&["validate", path(&invalid), "--json"]);
    assert_eq!(output.status.code(), Some(1));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], false);
    assert_eq!(json["command"], "validate");
    assert!(!json["diagnostics"].as_array().unwrap().is_empty());
}

#[test]
fn help_uses_canonical_commands_targets_and_verification_flags() {
    let output = tess(&["--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("  lock      Generate or update the deterministic local package lockfile"),
        "{help}"
    );
    assert!(help.contains("  validate  Validate Tess syntax"), "{help}");
    assert!(
        help.contains("  verify    Verify quantified invariants and bounded state traces"),
        "{help}"
    );
    assert!(
        help.contains("  graph     Render the decision, rule, override, and source graph"),
        "{help}"
    );
    assert!(!help.lines().any(|line| line.starts_with("  check ")));
    assert!(!help.lines().any(|line| line.starts_with("  explore ")));

    let output = tess(&["lock", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(
        stdout(&output).contains("Usage: tess lock <TARGET>"),
        "{}",
        stdout(&output)
    );

    let output = tess(&["validate", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("Usage: tess validate [OPTIONS] <TARGET>"),
        "{help}"
    );

    let output = tess(&["verify", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("Usage: tess verify [OPTIONS] <TARGET>"),
        "{help}"
    );
    assert!(help.contains("--invariant <NAME>"), "{help}");
    assert!(help.contains("--max-evaluations <N>"), "{help}");
    assert!(!help.contains("--check"), "{help}");
    assert!(!help.contains("--max-combinations"), "{help}");

    let output = tess(&["graph", "--help"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let help = stdout(&output);
    assert!(
        help.contains("Usage: tess graph [OPTIONS] <TARGET>"),
        "{help}"
    );
    assert!(help.contains("--decision <NAME>"), "{help}");
    assert!(help.contains("--format <FORMAT>"), "{help}");
}

#[test]
fn removed_commands_and_verification_flags_are_usage_errors() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    for arguments in [
        vec!["check", path(&source)],
        vec!["explore", path(&source)],
        vec!["verify", path(&source), "--check", "total"],
        vec!["verify", path(&source), "--max-combinations", "10"],
    ] {
        let output = tess(&arguments);
        assert_eq!(
            output.status.code(),
            Some(2),
            "removed syntax unexpectedly succeeded: {arguments:?}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
    }

    let legacy = directory.write(
        "legacy-check.tes",
        &VALID_SOURCE.replace("invariant total:", "check total:"),
    );
    let output = tess(&["validate", path(&legacy)]);
    assert_eq!(output.status.code(), Some(1));
    let error = stderr(&output);
    assert!(
        error.contains("`check` declarations were renamed to `invariant`"),
        "{error}"
    );
    assert!(error.contains("invariant NAME:"), "{error}");
}

#[test]
fn lint_reports_warnings_and_can_apply_a_strict_failure_policy() {
    let directory = TestDirectory::new();
    let warning_source = VALID_SOURCE.replacen("when s.flag", "when true", 1);
    let source = directory.write("warning.tes", &warning_source);

    let output = tess(&["lint", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stderr(&output).contains("warning[W0401]"));
    assert!(stdout(&output).contains("0 error(s), 1 warning(s)"));

    let output = tess(&["lint", path(&source), "--warnings-as-errors", "--json"]);
    assert_eq!(output.status.code(), Some(1));
    assert!(output.stderr.is_empty());
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], false);
    assert_eq!(json["command"], "lint");
    assert_eq!(json["result"]["errors"], 0);
    assert_eq!(json["result"]["warnings"], 1);
    assert_eq!(json["result"]["warnings_as_errors"], true);
    assert_eq!(json["diagnostics"][0]["severity"], "warning");
}

#[test]
fn lint_reads_explicit_stdin_and_rejects_invalid_utf8() {
    let output = tess_with_stdin(&["lint", "-", "--json"], VALID_SOURCE.as_bytes());
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], true);
    assert_eq!(json["result"]["errors"], 0);

    let output = tess_with_stdin(&["lint", "-"], &[0xff, 0xfe]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("UTF-8 source from stdin"));

    let output = tess_with_stdin(
        &["lint", "-", "--warnings-as-errors"],
        b"module m\nimport \"model.tes\"\n",
    );
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("error[M0006]"));
    assert!(stderr(&output).contains("project-aware loader"));
}

#[test]
fn test_filters_cases_and_reports_expectation_failure() {
    let directory = TestDirectory::new();
    let valid = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["test", path(&valid), "--case", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("PASS"));

    let failing_source = VALID_SOURCE.replace("expect outcome(s) = Yes", "expect outcome(s) = No");
    let failing = directory.write("failing.tes", &failing_source);
    let output = tess(&["test", path(&failing), "--case", "yes_case"]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stdout(&output).contains("FAIL"));
}

#[test]
fn test_supports_versioned_json_details_and_junit_xml() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    let output = tess(&["test", path(&source), "--format", "json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(report["command"], "test");
    assert_eq!(report["result"]["schema_version"], "tess.test-report/v1");
    assert_eq!(report["result"]["module"], "sample");
    assert_eq!(
        report["result"]["outcomes"][0]["assertions"][0]["query"],
        "outcome(s)"
    );
    assert_eq!(
        report["result"]["outcomes"][0]["assertions"][0]["actual"]["status"],
        "resolved"
    );

    let output = tess(&["test", path(&source), "--format", "junit"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let xml = stdout(&output);
    assert!(xml.starts_with("<?xml version=\"1.0\""), "{xml}");
    assert!(
        xml.contains("<testsuite name=\"sample\" tests=\"1\""),
        "{xml}"
    );
    assert!(
        xml.contains("<testcase classname=\"sample\" name=\"yes_case\""),
        "{xml}"
    );

    let conflict = tess(&["test", path(&source), "--json", "--format", "junit"]);
    assert_eq!(conflict.status.code(), Some(2));
}

#[test]
fn snapshot_record_and_diff_are_deterministic_and_semantic() {
    let directory = TestDirectory::new();
    let source = directory.write("policy.tes", VALID_SOURCE);
    let baseline = directory.path.join("baseline.json");

    let output = tess(&[
        "snapshot",
        "record",
        path(&source),
        "--output",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("recorded 1 decision result(s)"));
    let first = fs::read(&baseline).unwrap();
    let snapshot: Value = serde_json::from_slice(&first).unwrap();
    assert_eq!(snapshot["schema_version"], "tess.decision-snapshot/v1");
    assert_eq!(
        snapshot["cases"][0]["decisions"][0]["result"]["status"],
        "resolved"
    );

    let output = tess(&[
        "snapshot",
        "record",
        path(&source),
        "--output",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(fs::read(&baseline).unwrap(), first);

    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("snapshot matches"));

    let changed_source = VALID_SOURCE.replace("then outcome(s) = Yes", "then outcome(s) = No");
    fs::write(&source, changed_source).unwrap();
    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&baseline),
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    assert!(stdout(&output).contains("CHANGED yes_case :: outcome(s)#1"));

    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&baseline),
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(report["ok"], false);
    assert_eq!(
        report["result"]["diff"]["schema_version"],
        "tess.snapshot-diff/v1"
    );
    assert_eq!(
        report["result"]["diff"]["changes"][0]["change"],
        "decision_changed"
    );

    let malformed = directory.write("malformed-snapshot.json", "{not json}");
    let output = tess(&[
        "snapshot",
        "diff",
        path(&source),
        "--baseline",
        path(&malformed),
    ]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("invalid decision snapshot"));

    let output = tess(&[
        "snapshot",
        "record",
        path(&source),
        "--output",
        path(&baseline),
        "--case",
        "missing",
    ]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("case `missing` was not found"));
}

#[test]
fn run_and_explain_default_to_detailed_output_and_compact_preserves_the_result_line() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["run", path(&source), "--case", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer::Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("yes"), "{output}");

    let output = tess(&["explain", path(&source), "--case", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer::Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("yes"), "{output}");

    let output = tess(&["run", path(&source), "--case", "yes_case", "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "outcome(s) = Answer::Yes\n");

    let output = tess(&["explain", path(&source), "--case", "yes_case", "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "outcome(s) = Answer::Yes\n");

    let output = tess(&["explain", path(&source), "--case", "yes_case", "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["status"], "resolved");
    assert_eq!(json["result"]["rules"][0]["rule"], "no");
    assert_eq!(json["result"]["rules"][1]["rule"], "yes");

    let output = tess(&[
        "explain",
        path(&source),
        "--case",
        "yes_case",
        "--json",
        "--provenance",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["provenance"]["schema_version"], 1);
    assert_eq!(
        json["result"]["evaluation"]["result"]["status"]["status"],
        "resolved"
    );
    let nodes = json["result"]["provenance"]["nodes"].as_array().unwrap();
    assert!(nodes.iter().any(|node| node["kind"] == "input_field"));
    assert!(nodes.iter().any(|node| node["kind"] == "decision_result"));

    let output = tess(&[
        "explain",
        path(&source),
        "--case",
        "yes_case",
        "--provenance",
    ]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("--json"));
}

#[test]
fn human_output_colors_only_when_the_output_environment_supports_it() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let arguments = ["run", path(&source), "--case", "yes_case"];

    let automatic = tess_with_automatic_color(&arguments);
    assert_eq!(automatic.status.code(), Some(0), "{}", stderr(&automatic));
    assert!(!stdout(&automatic).contains("\u{1b}["));

    let forced = tess_with_forced_color(&arguments);
    assert_eq!(forced.status.code(), Some(0), "{}", stderr(&forced));
    let forced = stdout(&forced);
    assert!(forced.contains("\u{1b}["), "{forced:?}");
    assert!(forced.contains('✓'), "{forced:?}");

    let states = directory.write("states.tes", EXPLANATION_STATES_SOURCE);
    let forced_states = tess_with_forced_color(&["run", path(&states)]);
    assert_eq!(forced_states.status.code(), Some(1));
    let forced_states = stdout(&forced_states);
    for (code, meaning) in [
        ("\u{1b}[32m", "resolved"),
        ("\u{1b}[33m", "undefined/unknown"),
        ("\u{1b}[31m", "conflict"),
    ] {
        assert!(
            forced_states.contains(code),
            "missing {meaning} color in {forced_states:?}"
        );
    }

    let no_color = tess_with_no_color_and_force(&arguments);
    assert_eq!(no_color.status.code(), Some(0), "{}", stderr(&no_color));
    assert!(!stdout(&no_color).contains("\u{1b}["));

    let compact =
        tess_with_forced_color(&["run", path(&source), "--case", "yes_case", "--compact"]);
    assert_eq!(stdout(&compact), "outcome(s) = Answer::Yes\n");

    let json = tess_with_forced_color(&["run", path(&source), "--case", "yes_case", "--json"]);
    assert!(!stdout(&json).contains("\u{1b}["));
    let _: Value = serde_json::from_slice(&json.stdout).unwrap();

    let verify_arguments = ["verify", path(&source), "--invariant", "total"];
    let automatic = tess_with_automatic_color(&verify_arguments);
    assert_eq!(automatic.status.code(), Some(0), "{}", stderr(&automatic));
    assert!(!stdout(&automatic).contains("\u{1b}["));

    let forced = tess_with_forced_color(&verify_arguments);
    assert_eq!(forced.status.code(), Some(0), "{}", stderr(&forced));
    let forced = stdout(&forced);
    assert!(forced.contains("\u{1b}[32m"), "{forced:?}");
    assert!(forced.contains('✓'), "{forced:?}");

    let broken = directory.write("broken.tes", BROKEN_ANALYSIS_SOURCE);
    let failed = tess_with_forced_color(&["verify", path(&broken), "--invariant", "total"]);
    assert_eq!(failed.status.code(), Some(1));
    assert!(stdout(&failed).contains("\u{1b}[31m"));

    let inconclusive = tess_with_forced_color(&[
        "verify",
        path(&source),
        "--invariant",
        "total",
        "--max-evaluations",
        "1",
        "--solver",
        "off",
    ]);
    assert_eq!(inconclusive.status.code(), Some(1));
    let inconclusive = stdout(&inconclusive);
    assert!(inconclusive.contains("\u{1b}[33m"), "{inconclusive:?}");
    assert!(inconclusive.contains('?'), "{inconclusive:?}");

    let no_color = tess_with_no_color_and_force(&verify_arguments);
    assert_eq!(no_color.status.code(), Some(0));
    assert!(!stdout(&no_color).contains("\u{1b}["));

    let json = tess_with_forced_color(&["verify", path(&source), "--invariant", "total", "--json"]);
    assert!(!stdout(&json).contains("\u{1b}["));
    let _: Value = serde_json::from_slice(&json.stdout).unwrap();
}

#[test]
fn bare_run_uses_declared_expectations_and_bare_explain_uses_the_only_case() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer::Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("yes"), "{output}");

    let output = tess(&["explain", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("outcome(s) = Answer::Yes"), "{output}");
    assert!(output.contains("yes_case"), "{output}");
    assert!(output.contains("yes"), "{output}");
}

#[test]
fn bare_run_evaluates_every_case_and_expectation_in_stable_order() {
    let directory = TestDirectory::new();
    let source = directory.write("batch.tes", BATCH_RUN_SOURCE);

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    let a_case = output.find("a_case").expect("a_case explanation");
    let z_case = output.find("z_case").expect("z_case explanation");
    assert!(a_case < z_case, "{output}");
    assert_eq!(output.matches("a_case").count(), 1, "{output}");
    assert_eq!(output.matches("z_case").count(), 1, "{output}");
    assert_eq!(output.matches("let s = Subject {").count(), 2, "{output}");
    assert_eq!(output.matches("flag: false").count(), 1, "{output}");
    assert_eq!(output.matches("flag: true").count(), 1, "{output}");
    assert!(output.contains("\n\nz_case\n"), "{output}");
    assert!(!output.contains("case `"), "{output}");
    assert!(!output.contains("input:"), "{output}");
    assert!(output.contains("primary(s) = Answer::No"), "{output}");
    assert!(output.contains("primary(s) = Answer::Yes"), "{output}");
    assert!(output.contains("review(s) = Answer::Yes"), "{output}");

    let output = tess(&["run", path(&source), "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(
        stdout(&output),
        "a_case:\n  primary(s) = Answer::No\n  review(s) = Answer::Yes\n\nz_case:\n  primary(s) = Answer::Yes\n  review(s) = Answer::Yes\n"
    );

    let output = tess(&["run", path(&source), "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["ok"], true);
    assert_eq!(json["result"]["cases"][0]["case"], "a_case");
    assert_eq!(json["result"]["cases"][1]["case"], "z_case");
    assert_eq!(
        json["result"]["cases"][0]["evaluations"]
            .as_array()
            .unwrap()
            .len(),
        2
    );
    assert_eq!(
        json["result"]["cases"][0]["evaluations"][0]["values"][0],
        "No"
    );
    assert!(
        json["result"]["cases"][0]["evaluations"][0]
            .get("rules")
            .is_none()
    );

    let output = tess(&["run", path(&source), "--case", "z_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("primary(s) = Answer::Yes"), "{output}");
    assert!(output.contains("primary_yes"), "{output}");

    let output = tess(&["run", path(&source), "--case", "z_case", "--compact"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "primary(s) = Answer::Yes\n");

    let output = tess(&[
        "run",
        path(&source),
        "--case",
        "z_case",
        "--query",
        "review(s)",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("review(s) = Answer::Yes"), "{output}");
    assert!(output.contains("review_all"), "{output}");

    let output = tess(&[
        "run",
        path(&source),
        "--case",
        "z_case",
        "--query",
        "review(s)",
        "--compact",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(stdout(&output), "review(s) = Answer::Yes\n");
}

#[test]
fn bare_run_exit_status_depends_on_evaluation_not_expectation_comparison() {
    let directory = TestDirectory::new();
    let resolved = directory.write("resolved.tes", BATCH_RUN_SOURCE);
    let output = tess(&["run", path(&resolved)]);
    assert_eq!(
        output.status.code(),
        Some(0),
        "resolved values should succeed even when the case's expected values differ"
    );

    let unresolved_source = BATCH_RUN_SOURCE.replace(
        "rule review_all(Subject s):\n  when true",
        "rule review_all(Subject s):\n  when false",
    );
    let unresolved = directory.write("unresolved.tes", &unresolved_source);
    let output = tess(&["run", path(&unresolved)]);
    assert_eq!(output.status.code(), Some(1));
    let output = stdout(&output);
    assert!(output.contains("primary(s) = Answer::No"), "{output}");
    assert!(output.contains("primary(s) = Answer::Yes"), "{output}");
    assert!(output.contains("review(s) = undefined"), "{output}");
}

#[test]
fn detailed_batch_run_explains_resolved_undefined_unknown_conflict_and_override() {
    let directory = TestDirectory::new();
    let source = directory.write("states.tes", EXPLANATION_STATES_SOURCE);

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let output = stdout(&output);

    let resolved = output
        .find("resolved(s) = Answer::Yes")
        .expect("resolved result");
    let undefined = output
        .find("empty(s) = undefined")
        .expect("undefined result");
    let unknown = output
        .find("uncertain(s) = unknown")
        .expect("unknown result");
    let conflict = output
        .find("disputed(s) = conflict")
        .expect("conflict result");
    let overridden = output
        .find("replaced(s) = Answer::Yes")
        .expect("override result");
    assert!(
        resolved < undefined && undefined < unknown && unknown < conflict && conflict < overridden,
        "{output}"
    );
    for evidence in [
        "resolved_yes",
        "uncertain_yes",
        "s.maybe_flag",
        "disputed_yes",
        "disputed_no",
        "replaced_base",
        "replaced_exception",
    ] {
        assert!(
            output.contains(evidence),
            "missing `{evidence}` in:\n{output}"
        );
    }
    assert_eq!(output.matches("all_states").count(), 1, "{output}");
    assert_eq!(output.matches("let s = Subject {").count(), 1, "{output}");
    for status in [
        "  ✓ resolved(s) = Answer::Yes",
        "  ○ empty(s) = undefined",
        "  ? uncertain(s) = unknown",
        "  ✗ disputed(s) = conflict [Answer::No, Answer::Yes]",
        "  ✓ replaced(s) = Answer::Yes",
    ] {
        assert!(output.contains(status), "missing `{status}` in:\n{output}");
    }

    let compact = tess(&["run", path(&source), "--compact"]);
    assert_eq!(compact.status.code(), Some(1), "{}", stderr(&compact));
    assert_eq!(
        stdout(&compact),
        "resolved(s) = Answer::Yes\nempty(s) = undefined\nuncertain(s) = unknown\nmissing: s.maybe_flag\ndisputed(s) = conflict [Answer::No, Answer::Yes]\n  reason: different values remain after explicit overrides\nreplaced(s) = Answer::Yes\n"
    );
}

#[test]
fn detailed_run_marks_allowed_empty_results_as_resolved() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "empty-results.tes",
        r"module empty_results

enum Answer { Yes }
entity Subject { flag: Bool }
decision maybe_answer(Subject s) -> Answer zero or one
decision collection(Subject s) -> Answer many

case empty:
  let s = Subject { flag: false }
  expect maybe_answer(s) = Yes
  expect collection(s) = Yes
",
    );

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("  ✓ maybe_answer(s) = []"), "{output}");
    assert!(output.contains("  ✓ collection(s) = []"), "{output}");
    assert_eq!(output.matches("empty").count(), 1, "{output}");
    assert!(!output.contains("  ○ "), "{output}");
}

#[test]
fn detailed_run_merges_equal_support_and_reports_the_imported_rule_location() {
    let directory = TestDirectory::new();
    let rules = directory.write(
        "rules.tes",
        r"module imported
rule first(Subject s):
  when s.flag
  then outcome(s) = Yes
rule second(Subject s):
  when s.flag
  then outcome(s) = Yes
",
    );
    let entry = directory.write(
        "entry.tes",
        r#"module imported
import "rules.tes"
enum Answer { Yes, No }
entity Subject { flag: Bool }
decision outcome(Subject s) -> Answer
case c:
  let s = Subject { flag: true }
  expect outcome(s) = Yes
"#,
    );

    let output = tess(&["run", path(&entry)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(
        output.contains("merged candidate `Answer::Yes`"),
        "{output}"
    );
    assert!(
        output.contains("equal values are merged and count once"),
        "{output}"
    );
    assert!(
        output.contains(&format!("{}:", rules.display())),
        "{output}"
    );
    assert!(output.contains("rule `first`"), "{output}");
    assert!(output.contains("rule `second`"), "{output}");
}

#[test]
fn bare_run_reports_a_case_without_expectations() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "empty-case.tes",
        &format!(
            "{BROKEN_ANALYSIS_SOURCE}\ncase empty:\n  let s = Subject {{\n    flag: true,\n  }}\n"
        ),
    );

    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(1));
    let error = stderr(&output);
    assert!(error.contains("error[C3003]"), "{error}");
    assert!(error.contains("case `empty` has no expectation"), "{error}");
}

#[test]
fn run_without_an_input_explains_how_to_choose_when_case_count_is_not_one() {
    let directory = TestDirectory::new();
    let no_cases = directory.write("no-cases.tes", BROKEN_ANALYSIS_SOURCE);
    let output = tess(&["run", path(&no_cases)]);
    assert_eq!(output.status.code(), Some(2));
    let error = stderr(&output);
    assert!(error.contains("no cases are declared"), "{error}");
    assert!(error.contains("--input JSON_FILE"), "{error}");

    let multiple_cases_source = format!(
        "{VALID_SOURCE}\ncase no_case:\n  let s = Subject {{\n    flag: false,\n  }}\n  expect outcome(s) = No\n"
    );
    let multiple_cases = directory.write("multiple-cases.tes", &multiple_cases_source);
    let output = tess(&["explain", path(&multiple_cases)]);
    assert_eq!(output.status.code(), Some(2));
    let error = stderr(&output);
    assert!(error.contains("multiple cases are declared"), "{error}");
    assert!(error.contains("`yes_case`"), "{error}");
    assert!(error.contains("`no_case`"), "{error}");
    assert!(error.contains("--case NAME"), "{error}");
    assert!(error.contains("--input JSON_FILE"), "{error}");
}

#[test]
fn run_accepts_a_bare_filename_from_the_current_directory() {
    let directory = TestDirectory::new();
    directory.write("valid.tes", VALID_SOURCE);

    let output = tess_in(&directory.path, &["run", "valid.tes", "--case", "yes_case"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("Yes"));
    assert!(output.contains("--> valid.tes:"), "{output}");
    assert!(
        !output.contains(&directory.path.display().to_string()),
        "{output}"
    );
}

#[test]
fn run_accepts_json_input_and_requires_a_query_for_it() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let input = directory.write("input.json", r#"{"flag":true}"#);
    let output = tess(&[
        "run",
        path(&source),
        "--input",
        path(&input),
        "--query",
        "outcome(s)",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["status"], "resolved");
    assert_eq!(json["result"]["values"][0], "Yes");
    assert!(json["result"].get("rules").is_none());

    let output = tess(&["run", path(&source), "--input", path(&input)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("--query is required"));
}

#[test]
fn run_preserves_full_decimal_precision_in_json_numbers() {
    let directory = TestDirectory::new();
    let source = workspace_root().join("examples/expense-audit/expense.tes");
    let input = directory.write(
        "expense.json",
        r#"{
  "청구금액": 0.1234567890123456789012345679,
  "승인한도": 0.1234567890123456789012345678,
  "영수증첨부": true
}"#,
    );
    let output = tess(&[
        "run",
        path(&source),
        "--input",
        path(&input),
        "--query",
        "감사표시(e)",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let json: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(json["result"]["status"], "resolved");
    assert!(
        json["result"]["values"]
            .as_array()
            .is_some_and(|values| values.iter().any(|value| value == "승인한도초과")),
        "{}",
        stdout(&output)
    );
}

#[test]
fn compact_conflicts_with_json() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);

    for command in ["run", "explain"] {
        let output = tess(&[
            command,
            path(&source),
            "--case",
            "yes_case",
            "--compact",
            "--json",
        ]);
        assert_eq!(output.status.code(), Some(2));
        let error = stderr(&output);
        assert!(error.contains("--compact"), "{error}");
        assert!(error.contains("--json"), "{error}");
    }
}

#[test]
fn repl_supports_piped_dynamic_input_and_queries() {
    let directory = TestDirectory::new();
    let source = directory.write("valid.tes", VALID_SOURCE);
    let script =
        b"help\n:case\n:set s.flag = false\noutcome(s)\n:explain\n:reset\noutcome(s)\nexit\n";

    let output = tess_with_stdin(&["repl", path(&source)], script);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("loaded sole case `yes_case`"), "{output}");
    assert!(output.contains("try: outcome(s)"), "{output}");
    assert!(output.contains("Press Tab once"), "{output}");
    assert!(output.contains("* yes_case (current)"), "{output}");
    assert!(output.contains("s.flag = false"), "{output}");
    assert!(output.contains("outcome(s) = Answer::No"), "{output}");
    assert!(output.contains("✓ outcome(s) = Answer::No"), "{output}");
    assert!(
        output.contains("selected candidate `Answer::No`"),
        "{output}"
    );
    assert!(output.contains("restored case `yes_case`"), "{output}");
    assert!(output.contains("outcome(s) = Answer::Yes"), "{output}");
}

#[test]
fn verify_distinguishes_proved_and_refuted_invariants() {
    let directory = TestDirectory::new();
    let valid = directory.write("valid.tes", VALID_SOURCE);
    let output = tess(&["verify", path(&valid), "--invariant", "total"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(
        stdout(&output).contains("✓ total\n  proved for all inputs"),
        "{}",
        stdout(&output)
    );

    let broken = directory.write("broken.tes", BROKEN_ANALYSIS_SOURCE);
    let output = tess(&["verify", path(&broken), "--invariant", "total"]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    assert!(stdout(&output).contains("counterexample"));

    let output = tess(&["verify", path(&valid), "--max-evaluations", "0"]);
    assert_eq!(output.status.code(), Some(2));

    let output = tess(&["verify", path(&valid), "--max-evaluations", "100_000"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
}

#[test]
fn verify_reports_existential_witnesses_and_exact_no_witness_failures() {
    let _solver_guard = solver_test_guard();
    let directory = TestDirectory::new();
    let source = directory.write(
        "existential.tes",
        r"module existential_cli

enum Answer { Yes, No }
entity Subject { score: Int range -100..100 }
decision outcome(Subject s) -> Answer

rule yes(Subject s):
  when s.score > 10
  then outcome(s) = Yes

rule no(Subject s):
  when s.score <= 10
  then outcome(s) = No

invariant reachable_yes:
  for some s: Subject
  if s.score > 0
  then outcome(s) = Yes

invariant unreachable_yes:
  for some s: Subject
  if s.score <= 10
  then outcome(s) = Yes
",
    );

    let output = tess(&[
        "verify",
        path(&source),
        "--invariant",
        "reachable_yes",
        "--solver",
        "z3",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let text = stdout(&output);
    assert!(
        text.contains("satisfying input found · exact solver (Z3)"),
        "{text}"
    );
    assert!(text.contains("witness"), "{text}");
    assert!(text.contains("s: Subject {"), "{text}");

    let output = tess(&[
        "verify",
        path(&source),
        "--invariant",
        "reachable_yes",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["quantifier"], "some");
    assert_eq!(invariant["verdict"], "passed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert_eq!(invariant["evaluated"], 1);
    assert_eq!(invariant["witness"]["bindings"]["s"]["entity"], "Subject");
    assert!(invariant["counterexamples"].as_array().unwrap().is_empty());

    let output = tess(&[
        "verify",
        path(&source),
        "--invariant",
        "unreachable_yes",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["quantifier"], "some");
    assert_eq!(invariant["verdict"], "failed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert!(invariant.get("witness").is_none());
    assert!(invariant["counterexamples"].as_array().unwrap().is_empty());
}

#[test]
fn verify_covers_the_cartesian_product_of_multiple_quantified_entities() {
    let directory = TestDirectory::new();
    let source_text = r"module multi_quantified

enum Answer { Free, Paid }
enum Tier { Standard, Preferred }

entity Order { amount: Int range 0..100_000 }
entity Customer { tier: Tier }

decision outcome(Order o, Customer c) -> Answer

rule amount_free(Order o, Customer c):
  when o.amount >= 50_000
  then outcome(o, c) = Free

rule preferred_free(Order o, Customer c):
  when c.tier = Preferred
  then outcome(o, c) = Free

rule standard_paid(Order o, Customer c):
  when o.amount < 50_000 and c.tier = Standard
  then outcome(o, c) = Paid

invariant total:
  for all o: Order, c: Customer
  exactly one outcome(o, c)
";
    let valid = directory.write("multi-valid.tes", source_text);

    let output = tess(&["verify", path(&valid), "--invariant", "total"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(
        stdout(&output).contains("proved for all inputs · 4 exact regions checked"),
        "{}",
        stdout(&output)
    );

    let output = tess(&["verify", path(&valid), "--invariant", "total", "--json"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(report["command"], "verify");
    assert!(report["result"].get("checks").is_none());
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["invariant"], "total");
    assert_eq!(invariant["planned_evaluations"], 4);
    assert_eq!(invariant["evaluated"], 4);
    assert_eq!(invariant["completeness"], "threshold_partitioned");
    assert_eq!(invariant["verdict"], "passed");
    for removed_key in ["check", "candidate_combinations", "explored"] {
        assert!(
            invariant.get(removed_key).is_none(),
            "old key `{removed_key}` survived"
        );
    }

    let broken_text = source_text.replace(
        "o.amount < 50_000 and c.tier = Standard",
        "o.amount < 50_000 and c.tier = Preferred",
    );
    let broken = directory.write("multi-broken.tes", &broken_text);
    let output = tess(&["verify", path(&broken), "--invariant", "total"]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let output = stdout(&output);
    assert!(output.contains("counterexample · undefined"), "{output}");
    assert!(output.contains("c: Customer {"), "{output}");
    assert!(output.contains("o: Order {"), "{output}");
}

#[test]
fn verify_uses_z3_for_relational_integer_gaps_without_false_passes() {
    let _solver_guard = solver_test_guard();
    let directory = TestDirectory::new();
    let source_text = r"module relational_gap

enum Shipping { Free, Paid }

entity Order { amount: Int range 0..100_000 }
entity Coupon { discount: Int range 0..100_000 }

decision shipping(Order o, Coupon c) -> Shipping

rule free(Order o, Coupon c):
  when o.amount - c.discount > 50_000
  then shipping(o, c) = Free

rule paid(Order o, Coupon c):
  when o.amount - c.discount < 50_000
  then shipping(o, c) = Paid

invariant total:
  for all o: Order, c: Coupon
  exactly one shipping(o, c)
";
    let broken = directory.write("relational-gap.tes", source_text);

    let output = tess(&[
        "verify",
        path(&broken),
        "--invariant",
        "total",
        "--solver",
        "off",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "failed");
    let counterexample = &invariant["counterexamples"][0];
    assert_eq!(counterexample["invariant"], "total");
    assert_eq!(counterexample["kind"], "undefined");
    assert!(counterexample.get("check").is_none());
    assert!(invariant.get("solver").is_none());

    let fixed_text = source_text.replace(
        "o.amount - c.discount > 50_000",
        "o.amount - c.discount >= 50_000",
    );
    let fixed = directory.write("relational-fixed.tes", &fixed_text);
    let output = tess(&[
        "verify",
        path(&fixed),
        "--invariant",
        "total",
        "--solver",
        "off",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "inconclusive");
    assert_ne!(invariant["completeness"], "solver_exact");
    assert!(invariant.get("solver").is_none());

    let output = tess_without_path(&[
        "verify",
        path(&broken),
        "--invariant",
        "total",
        "--solver",
        "z3",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let text = stdout(&output);
    assert!(
        text.contains("✗ total\n  counterexample found · exact solver (Z3)"),
        "{text}"
    );
    assert!(text.contains("counterexample · undefined"), "{text}");
    assert!(!text.contains("solver_exact"), "{text}");
    assert!(!text.contains("negated property"), "{text}");

    let output = tess(&[
        "verify",
        path(&broken),
        "--invariant",
        "total",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(1), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "failed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert_eq!(invariant["evaluated"], 1);
    assert_eq!(invariant["planned_evaluations"], 0);
    assert_eq!(invariant["solver"]["backend"], "z3");
    assert_eq!(invariant["solver"]["logic"], "QF_LIA");
    assert!(
        invariant["notes"][0]
            .as_str()
            .is_some_and(|note| note.contains("model was replayed"))
    );
    assert!(
        invariant["solver"]["version"]
            .as_str()
            .is_some_and(|version| !version.is_empty())
    );
    let bindings = &invariant["counterexamples"][0]["input"]["bindings"];
    let amount = bindings["o"]["fields"]["amount"]["value"].as_i64().unwrap();
    let discount = bindings["c"]["fields"]["discount"]["value"]
        .as_i64()
        .unwrap();
    assert_eq!(amount - discount, 50_000);

    let output = tess(&[
        "verify",
        path(&fixed),
        "--invariant",
        "total",
        "--solver",
        "z3",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let invariant = &report["result"]["invariants"][0];
    assert_eq!(invariant["verdict"], "passed");
    assert_eq!(invariant["completeness"], "solver_exact");
    assert_eq!(invariant["evaluated"], 0);
    assert_eq!(invariant["planned_evaluations"], 0);
    assert_eq!(invariant["solver"]["backend"], "z3");
    assert!(
        invariant["notes"][0]
            .as_str()
            .is_some_and(|note| note.contains("negated property is unsatisfiable"))
    );
}

#[test]
fn every_verifiable_example_uses_a_compact_exact_strategy() {
    let _solver_guard = solver_test_guard();
    let root = workspace_root();
    let targets = [
        ("examples/course-grading/course.tes", 0),
        ("examples/course-grading/broken-exception.tes", 1),
        ("examples/course-grading/broken-gap.tes", 1),
        ("examples/course-grading/broken-overlap.tes", 1),
        ("examples/course-grading/fixed-exception.tes", 0),
        ("examples/creator-payout/payout.tes", 0),
        ("examples/expense-audit/expense.tes", 0),
        ("examples/incident-response/incident.tes", 0),
        ("examples/projects/package-consumer", 0),
        ("examples/projects/shipping-policy", 0),
        ("examples/schedule-conflicts/conflicts.tes", 0),
        ("examples/tutorial/13-invariant-all-inputs.tes", 0),
        ("examples/tutorial/14-find-a-gap.tes", 1),
        ("examples/tutorial/15-multiple-inputs.tes", 0),
        ("examples/tutorial/16-relational-gap.tes", 1),
    ];

    for (relative, expected_exit) in targets {
        let target = root.join(relative);
        let output = tess(&["verify", path(&target), "--json"]);
        assert_eq!(
            output.status.code(),
            Some(expected_exit),
            "{relative}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
        let report: Value = serde_json::from_slice(&output.stdout).unwrap();
        let invariants = report["result"]["invariants"].as_array().unwrap();
        assert!(!invariants.is_empty(), "{relative}");
        for invariant in invariants {
            if invariant["quantifier"] == "some" && invariant["verdict"] == "passed" {
                assert!(
                    invariant["witness"].is_object(),
                    "{relative}: existential success omitted its witness: {invariant}"
                );
            } else {
                assert!(
                    matches!(
                        invariant["completeness"].as_str(),
                        Some("threshold_partitioned" | "solver_exact")
                    ),
                    "{relative}: {invariant}"
                );
            }
            assert_ne!(invariant["verdict"], "inconclusive", "{relative}");
        }
    }
}

#[test]
fn verify_runs_bounded_traces_and_supports_trace_selection() {
    let target = workspace_root().join("examples/order-lifecycle/lifecycle.tes");
    let output = tess(&[
        "verify",
        path(&target),
        "--trace",
        "every_order_settles",
        "--json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let report: Value = serde_json::from_slice(&output.stdout).unwrap();
    let trace = &report["result"]["traces"][0];
    assert_eq!(trace["trace"], "every_order_settles");
    assert_eq!(trace["verdict"], "passed");
    assert_eq!(trace["completeness"], "bounded_exhaustive");
    assert_eq!(trace["bound"], 4);
    assert!(
        trace["reachable_states"]
            .as_u64()
            .is_some_and(|value| value > 0)
    );

    let missing = tess(&["verify", path(&target), "--trace", "missing", "--json"]);
    assert_eq!(missing.status.code(), Some(1));
    let report: Value = serde_json::from_slice(&missing.stdout).unwrap();
    assert_eq!(report["diagnostics"][0]["code"], "C2002");
}

#[test]
fn local_path_packages_enforce_exports_and_use_qualified_aliases() {
    let directory = TestDirectory::new();
    directory.write(
        "common/tess.toml",
        "[project]\nname = \"common\"\nentry = \"src/main.tes\"\n\
         [exports]\nsymbols = [\"Answer\", \"Subject\", \"outcome\"]\n",
    );
    directory.write(
        "common/src/main.tes",
        "module common\n\
         enum Answer { Yes, No }\n\
         entity Subject { enabled: Bool }\n\
         decision outcome(Subject subject) -> Answer\n\
         rule enabled(Subject subject):\n\
           when subject.enabled\n\
           then outcome(subject) = Yes\n\
         rule disabled(Subject subject):\n\
           when not subject.enabled\n\
           then outcome(subject) = No\n",
    );
    directory.write(
        "app/tess.toml",
        "[project]\nname = \"app\"\nentry = \"src/main.tes\"\n\
         [dependencies.common]\npath = \"../common\"\n\
         symbols = [\"Answer\", \"Subject\", \"outcome\"]\n",
    );
    directory.write(
        "app/src/main.tes",
        "module app\n\
         case imported_rule_bundle:\n\
           let subject = common::Subject { enabled: true }\n\
           expect common::outcome(subject) = Yes\n\
         invariant imported_policy_is_total:\n\
           for all subject: common::Subject\n\
           exactly one common::outcome(subject)\n",
    );
    let app = directory.path.join("app");
    let lock = tess(&["lock", path(&app)]);
    assert_eq!(lock.status.code(), Some(0), "{}", stderr(&lock));
    for command in ["validate", "test", "verify"] {
        let output = tess(&[command, path(&app), "--json"]);
        assert_eq!(
            output.status.code(),
            Some(0),
            "{command}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
    }
    let dependency_source = directory.path.join("common/src/main.tes");
    let dependency_before = fs::read_to_string(&dependency_source).unwrap();
    let output = tess(&["fmt", path(&app)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert_eq!(
        fs::read_to_string(&dependency_source).unwrap(),
        dependency_before,
        "formatting a consumer must not rewrite a path dependency"
    );

    directory.write(
        "bad/tess.toml",
        "[project]\nname = \"bad\"\nentry = \"main.tes\"\n\
         [dependencies.common]\npath = \"../common\"\n\
         symbols = [\"private_helper\"]\n",
    );
    directory.write("bad/main.tes", "module bad\n");
    let output = tess(&["validate", path(&directory.path.join("bad")), "--json"]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("does not export requested symbol"));
}

#[test]
fn transitive_local_packages_honor_versions_and_the_checked_in_lock() {
    let directory = TestDirectory::new();
    directory.write(
        "utility/tess.toml",
        "[project]\nname = \"utility\"\nversion = \"1.3.0\"\nentry = \"main.tes\"\n\
         [exports]\nsymbols = [\"allowed\"]\n",
    );
    directory.write(
        "utility/main.tes",
        "module utility\nderive allowed(Bool enabled) -> Bool: enabled\n",
    );
    directory.write(
        "policy/tess.toml",
        "[project]\nname = \"policy\"\nversion = \"2.0.1\"\nentry = \"main.tes\"\n\
         [exports]\nsymbols = [\"Answer\", \"Subject\", \"outcome\"]\n\
         [dependencies.utility]\npath = \"../utility\"\nversion = \"^1.0\"\nsymbols = [\"allowed\"]\n",
    );
    directory.write(
        "policy/main.tes",
        "module policy\n\
         enum Answer { Yes, No }\n\
         entity Subject { enabled: Bool }\n\
         decision outcome(Subject subject) -> Answer\n\
         rule enabled(Subject subject):\n\
           when utility::allowed(subject.enabled)\n\
           then outcome(subject) = Yes\n\
         rule disabled(Subject subject):\n\
           when not utility::allowed(subject.enabled)\n\
           then outcome(subject) = No\n",
    );
    directory.write(
        "app/tess.toml",
        "[project]\nname = \"app\"\nversion = \"1.0.0\"\nentry = \"main.tes\"\n\
         [dependencies.policy]\npath = \"../policy\"\nversion = \"~2.0\"\n\
         symbols = [\"Answer\", \"Subject\", \"outcome\"]\n",
    );
    directory.write(
        "app/main.tes",
        "module app\n\
         case transitive_policy_runs:\n\
           let subject = policy::Subject { enabled: true }\n\
           expect policy::outcome(subject) = Yes\n",
    );
    let app = directory.path.join("app");
    let missing = tess(&["validate", path(&app)]);
    assert_eq!(missing.status.code(), Some(2));
    assert!(stderr(&missing).contains("tess lock"));
    assert!(!app.join("tess.lock").exists());

    let generated = tess(&["lock", path(&app)]);
    assert_eq!(
        generated.status.code(),
        Some(0),
        "stdout: {}\nstderr: {}",
        stdout(&generated),
        stderr(&generated)
    );
    let output = tess(&["test", path(&app), "--json"]);
    assert_eq!(
        output.status.code(),
        Some(0),
        "stdout: {}\nstderr: {}",
        stdout(&output),
        stderr(&output)
    );
    let lock_path = app.join("tess.lock");
    let lock = fs::read_to_string(&lock_path).unwrap();
    assert!(lock.contains("lock-version = 1"));
    assert!(lock.contains(
        "alias = \"policy\", requirement = \"~2.0\", manifest = \"../policy/tess.toml\", symbols = [\"Answer\", \"Subject\", \"outcome\"]"
    ));
    assert!(lock.contains(
        "alias = \"utility\", requirement = \"^1.0\", manifest = \"../utility/tess.toml\", symbols = [\"allowed\"]"
    ));

    let second = tess(&["validate", path(&app), "--json"]);
    assert_eq!(second.status.code(), Some(0), "{}", stderr(&second));
    assert_eq!(fs::read_to_string(&lock_path).unwrap(), lock);

    fs::write(&lock_path, "lock-version = 999\n").unwrap();
    let stale = tess(&["validate", path(&app)]);
    assert_eq!(stale.status.code(), Some(2));
    assert!(stderr(&stale).contains("out of date"));
    let updated = tess(&["lock", path(&app)]);
    assert_eq!(updated.status.code(), Some(0), "{}", stderr(&updated));
    assert_eq!(fs::read_to_string(&lock_path).unwrap(), lock);
}

#[test]
fn graph_loads_projects_and_renders_stable_dot_and_filtered_json() {
    let directory = TestDirectory::new();
    let project = directory.path.join("graph-project");
    directory.write(
        "graph-project/tess.toml",
        "[project]\nname = \"graph-project\"\nentry = \"main.tes\"\n",
    );
    directory.write(
        "graph-project/main.tes",
        "module policy\nimport \"model.tes\"\nimport \"rules.tes\"\n",
    );
    directory.write(
        "graph-project/model.tes",
        r#"module policy

enum Answer { Yes, No }
entity Subject { enabled: Bool }
decision outcome(Subject s) -> Answer
decision audit(Subject s) -> Bool many

source Statute {
  title: "Policy \"A\"",
  section: "4.2",
}
source Unused { title: "Unused" }
"#,
    );
    directory.write(
        "graph-project/rules.tes",
        r#"module policy

rule base(Subject s):
  when s.enabled
  then outcome(s) = Yes
  source Statute

rule exception(Subject s):
  when not s.enabled
  then outcome(s) = No
  then override base
  source "Legacy\nMemo"

rule audit_rule(Subject s):
  when s.enabled
  then audit(s) = true
"#,
    );

    let first = tess(&["graph", path(&project)]);
    assert_eq!(first.status.code(), Some(0), "{}", stderr(&first));
    let dot = stdout(&first);
    assert!(
        dot.starts_with("digraph policy {\n  rankdir=LR;\n"),
        "{dot}"
    );
    assert!(dot.contains("Policy \\\"A\\\""), "{dot}");
    assert!(dot.contains("Legacy\\nMemo"), "{dot}");
    assert!(dot.contains("[label=\"overrides\"]"), "{dot}");
    let second = tess(&["graph", path(&project), "--format", "dot"]);
    assert_eq!(first.stdout, second.stdout);

    let output = tess(&[
        "graph",
        path(&project),
        "--decision",
        "outcome",
        "--format",
        "json",
    ]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(output.stderr.is_empty());
    let graph: Value = serde_json::from_slice(&output.stdout).unwrap();
    assert_eq!(graph["schema_version"], 1);
    assert_eq!(graph["module"], "policy");
    assert_eq!(graph["decision"], "outcome");
    let ids = graph["nodes"]
        .as_array()
        .unwrap()
        .iter()
        .map(|node| node["id"].as_str().unwrap())
        .collect::<Vec<_>>();
    assert_eq!(
        ids,
        [
            "decision:outcome",
            "rule:base",
            "rule:exception",
            "source:inline:Legacy\nMemo",
            "source:named:Statute",
        ]
    );
    assert_eq!(graph["edges"].as_array().unwrap().len(), 5);
}

#[test]
fn graph_reports_selector_language_failures_and_target_io_failures() {
    let directory = TestDirectory::new();
    let source = directory.write(
        "valid.tes",
        &VALID_SOURCE.replace("rule no(Subject s):", "rule no_rule(Subject s):"),
    );
    let output = tess(&[
        "graph",
        path(&source),
        "--decision",
        "missing",
        "--format",
        "json",
    ]);
    assert_eq!(output.status.code(), Some(1));
    assert!(output.stdout.is_empty());
    let error = stderr(&output);
    assert!(error.contains("error[C4001]"), "{error}");
    assert!(error.contains("available decisions: outcome"), "{error}");

    let invalid = directory.write("invalid.tes", "module invalid\nenum E { A B }\n");
    let output = tess(&["graph", path(&invalid)]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("error[P0101]"));

    let output = tess(&["graph", path(&directory.path.join("missing.tes"))]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("could not read"));
}

#[test]
fn fmt_check_stdout_and_in_place_modes_are_non_destructive_when_requested() {
    let directory = TestDirectory::new();
    let original =
        "# module docs\nmodule m // header\n\n// answers\nenum E { A, // first\nB } # enum end\n";
    let source = directory.write("format.tes", original);

    let output = tess(&["fmt", path(&source), "--check"]);
    assert_eq!(output.status.code(), Some(1));
    assert_eq!(fs::read_to_string(&source).unwrap(), original);

    let output = tess(&["fmt", path(&source), "--stdout"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("  A,  // first\n  B,\n"));
    for comment in [
        "# module docs",
        "// header",
        "// answers",
        "// first",
        "# enum end",
    ] {
        assert!(stdout(&output).contains(comment));
    }
    assert_eq!(fs::read_to_string(&source).unwrap(), original);

    let output = tess(&["fmt", path(&source)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let formatted = fs::read_to_string(&source).unwrap();
    assert!(formatted.contains("  A,  // first\n  B,\n}  # enum end\n"));
    assert!(formatted.starts_with("# module docs\nmodule m  // header\n"));
    let output = tess(&["fmt", path(&source), "--check"]);
    assert_eq!(output.status.code(), Some(0));
}

#[test]
fn io_and_usage_errors_exit_with_code_two() {
    let directory = TestDirectory::new();
    let missing = directory.path.join("missing.tes");
    let output = tess(&["validate", path(&missing)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("could not read"));

    let source = directory.write("no-cases.tes", BROKEN_ANALYSIS_SOURCE);
    let output = tess(&["run", path(&source)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("no cases are declared"));
}

#[test]
fn init_creates_a_working_multi_file_project() {
    let directory = TestDirectory::new();
    let project = directory.path.join("shipping-policy");
    let output = tess(&["init", path(&project)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(stdout(&output).contains("tess validate ."));
    assert!(project.join("tess.toml").is_file());
    assert!(
        fs::read_to_string(project.join("tess.toml"))
            .unwrap()
            .contains("version = \"0.1.0\"")
    );
    assert!(project.join("src/main.tes").is_file());
    assert!(project.join("src/model/request.tes").is_file());
    assert!(project.join("src/rules/eligibility.tes").is_file());
    assert!(project.join("tests/cases.tes").is_file());
    assert!(
        fs::read_to_string(project.join("src/main.tes"))
            .unwrap()
            .contains("import \"model/request.tes\"")
    );
    let declarations = fs::read_to_string(project.join("tests/cases.tes")).unwrap();
    assert!(declarations.contains("invariant eligibility_is_total:"));
    assert!(!declarations.contains("check eligibility_is_total:"));
    let readme = fs::read_to_string(project.join("README.md")).unwrap();
    assert!(readme.contains("tess validate ."));
    assert!(readme.contains("tess verify ."));
    assert!(!readme.contains("tess check ."));
    assert!(!readme.contains("tess explore ."));

    for arguments in [
        vec!["validate", path(&project)],
        vec!["lint", path(&project), "--warnings-as-errors"],
        vec!["test", path(&project)],
        vec!["verify", path(&project)],
        vec!["run", path(&project), "--case", "enabled_is_eligible"],
        vec![
            "explain",
            path(&project.join("tess.toml")),
            "--case",
            "enabled_is_eligible",
        ],
        vec!["fmt", path(&project), "--check"],
    ] {
        let output = tess(&arguments);
        assert_eq!(
            output.status.code(),
            Some(0),
            "command {arguments:?}\nstdout: {}\nstderr: {}",
            stdout(&output),
            stderr(&output)
        );
    }

    let output = tess(&["init", path(&project)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("non-empty"));
}

#[test]
fn import_graph_diagnostics_report_the_importing_file() {
    let directory = TestDirectory::new();
    let main = directory.write(
        "project/main.tes",
        "module policy\nimport \"rules.tes\"\nimport \"rules.tes\"\n",
    );
    directory.write(
        "project/rules.tes",
        "module wrong\nimport \"main.tes\"\nenum Answer { Yes, }\n",
    );
    let output = tess(&["validate", path(&main)]);
    assert_eq!(output.status.code(), Some(1));
    let error = stderr(&output);
    assert!(error.contains("error[M0003]"), "{error}");
    assert!(error.contains("error[M0004]"), "{error}");
    assert!(error.contains("error[M0005]"), "{error}");
    assert!(error.contains("rules.tes:1:8"), "{error}");
    assert!(error.contains("main.tes:3:8"), "{error}");
}

#[test]
fn directory_formatting_covers_all_reachable_files_and_rejects_stdout() {
    let directory = TestDirectory::new();
    let project = directory.path.join("format-project");
    let output = tess(&["init", path(&project), "--module", "format_project"]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    let model = project.join("src/model/request.tes");
    let unformatted = fs::read_to_string(&model)
        .unwrap()
        .replace("  Eligible,", "Eligible,");
    fs::write(&model, unformatted).unwrap();

    let output = tess(&["fmt", path(&project), "--check"]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("request.tes"));
    let output = tess(&["fmt", path(&project)]);
    assert_eq!(output.status.code(), Some(0), "{}", stderr(&output));
    assert!(fs::read_to_string(&model).unwrap().contains("  Eligible,"));
    assert!(
        fs::read_to_string(project.join("src/main.tes"))
            .unwrap()
            .contains("import \"model/request.tes\"")
    );

    let output = tess(&["fmt", path(&project), "--stdout"]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("exactly one reachable source"));
}

#[test]
fn malformed_manifest_and_missing_import_have_distinct_exit_codes() {
    let directory = TestDirectory::new();
    let manifest = directory.write("bad/tess.toml", "[project]\nname = \"bad\"\n");
    let output = tess(&["validate", path(&manifest)]);
    assert_eq!(output.status.code(), Some(2));
    assert!(stderr(&output).contains("missing required `entry`"));

    let source = directory.write(
        "missing/main.tes",
        "module missing\nimport \"does-not-exist.tes\"\n",
    );
    let output = tess(&["validate", path(&source)]);
    assert_eq!(output.status.code(), Some(1));
    assert!(stderr(&output).contains("error[M0001]"));
    assert!(stderr(&output).contains("main.tes:2:8"));
}