//! The published **evaluation** corpus: cases an over-grading implementation
//! passes incorrectly.
//!
//! The wire vectors in `tests/vectors.rs` certify that an implementation
//! round-trips a receipt's bytes. They say nothing about whether it reaches
//! the right verdict, because they carry one scenario. This corpus is the
//! other half: each case is a complete set of evaluation inputs plus the
//! verdict §3 requires, chosen so that a plausible but wrong evaluator
//! disagrees.
//!
//! Every case names the **trap** it sets and the **direction** of the error
//! it catches. Most are over-grading: an implementation that reports
//! conformance never established, which is the failure this standard exists
//! to stop. At least one is under-grading, because a rule that refuses
//! everything is also wrong and an implementation can satisfy every
//! over-grading case by grading nothing at all.
//!
//! ## Where the expected verdicts come from
//!
//! They are written by hand from §3 of the specification, and they are
//! **not** regenerated from this implementation's output — a corpus whose
//! expectations are whatever the code produced would certify agreement with
//! itself. Setting `JOULESPEC_GEN_EVALUATION=1` republishes the input files
//! and the expectations as this test states them; it never reads a verdict
//! back out of the evaluator to decide what to expect.
//!
//! ## How another implementation uses it
//!
//! Each case directory holds `spec.json`, `state.json`, `witnesses.json`,
//! `work.json` and `expect.json`. Read the first four, evaluate, and compare
//! against the fifth.

use std::path::{Path, PathBuf};

use ed25519_dalek::SigningKey;
use joulespec_core::conform::{self, ArtifactState, Conformance, Work};
use joulespec_core::evidence::{
    Anchor, Attestation, Evidence, Formalization, Grade, Grounding, SignedWitness, Vacuity,
    Witness,
};
use joulespec_core::spec::{Clause, SignedSpec, Spec};
use joulespec_core::{Address, Energy, Provenance};
use serde::{Deserialize, Serialize};

fn key(seed: u8) -> SigningKey {
    SigningKey::from_bytes(&[seed; 32])
}

fn dir() -> PathBuf {
    Path::new(env!("CARGO_MANIFEST_DIR")).join("../../../conformance/v1/evaluation")
}

/// What a conforming evaluator must report for one case.
///
/// Deliberately small: the fields an over-generous implementation gets wrong.
/// Energy is omitted because these cases are about grading, and a corpus that
/// pinned microjoules would stop being reproducible for the reasons the
/// self-conformance record is not.
#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
struct Expect {
    /// What the case is for, in one line.
    intent: String,
    /// What a wrong implementation does here instead.
    trap: String,
    /// `over-grading` or `under-grading`: which way the wrong answer errs.
    direction: String,
    /// The specification's grade, absent where §3.2 requires absence.
    grade: Option<Grade>,
    /// The specification's attestation, on the second axis.
    attestation: Option<Attestation>,
    /// Flag kinds raised, by variant name, sorted.
    flags: Vec<String>,
    /// Per clause, in specification order.
    clauses: Vec<ExpectClause>,
    /// Whether the case conforms at `E3` and `A0`.
    conformant_at_e3: bool,
}

#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
struct ExpectClause {
    label: String,
    grade: Option<Grade>,
    /// How many of its witnesses were set aside as bound to another state.
    stale: usize,
}

fn flag_kind(f: &conform::Flag) -> String {
    match f {
        conform::Flag::NonGoalWitnessed { .. } => "NonGoalWitnessed",
        conform::Flag::Unbound { .. } => "Unbound",
        conform::Flag::ForeignSpec { .. } => "ForeignSpec",
        conform::Flag::Unverifiable { .. } => "Unverifiable",
    }
    .to_string()
}

fn observed(c: &Conformance, like: &Expect) -> Expect {
    let mut flags: Vec<String> = c.flags.iter().map(flag_kind).collect();
    flags.sort();
    Expect {
        intent: like.intent.clone(),
        trap: like.trap.clone(),
        direction: like.direction.clone(),
        grade: c.grade,
        attestation: c.attestation,
        flags,
        clauses: c
            .clauses
            .iter()
            .map(|v| ExpectClause {
                label: v.label.clone(),
                grade: v.grade,
                stale: v.stale.len(),
            })
            .collect(),
        conformant_at_e3: c.is_conformant(Grade::Falsifiable, Attestation::SelfAttested),
    }
}

// ── case construction ────────────────────────────────────────────────────

fn state() -> ArtifactState {
    ArtifactState::new(
        Address::of_bytes(b"eval-tree-v1"),
        [
            Address::of_bytes(b"eval-part-a"),
            Address::of_bytes(b"eval-part-b"),
        ],
    )
}

fn spec_of(clauses: Vec<Clause>) -> SignedSpec {
    let author = key(1);
    Spec::new(
        "A corpus case: the clauses exist to be graded, not to be implemented.",
        clauses,
        author.verifying_key().to_bytes(),
    )
    .sign(&author)
    .expect("signs")
}

fn obligation(spec: &SignedSpec, label: &str) -> joulespec_core::spec::Obligation {
    spec.spec
        .clauses
        .iter()
        .find(|c| c.label == label)
        .expect("label is in the specification")
        .obligation()
        .expect("addresses")
}

/// A witness carrying `evidence` for `label`, at `at` (the current state
/// unless a case is about staleness), signed by `signer`.
fn witness(
    spec: &SignedSpec,
    label: &str,
    evidence: Evidence,
    signer: &SigningKey,
    at: Address,
) -> SignedWitness {
    Witness::new(
        spec.spec.spec_id().unwrap(),
        obligation(spec, label),
        at,
        evidence,
        Energy::new(1_000, Provenance::Estimator),
        signer.verifying_key().to_bytes(),
    )
    .sign(signer)
    .expect("signs")
}

/// One unit of work by `author`, citing `label`.
///
/// Every case declares work, because the attestation axis is computed from
/// **work** authorship: with no implementer known, §2.8 makes attestation
/// absent, and a corpus of cases that all declared none would exercise one
/// axis and certify two.
fn work_by(spec: &SignedSpec, label: &str, author: &SigningKey) -> Vec<Work> {
    vec![Work::new(
        Address::of_bytes(b"eval-work"),
        vec![obligation(spec, label)],
        Energy::new(500_000, Provenance::Estimator),
        author.verifying_key().to_bytes(),
    )]
}

fn falsifiable(anchor: Anchor) -> Evidence {
    Evidence::Falsifiable {
        check: "a_named_check".into(),
        anchor,
        counter: Address::of_bytes(b"eval-counter"),
    }
}

fn proved(grounding: Grounding, vacuity: Vacuity) -> Evidence {
    Evidence::Proved {
        goal: Address::of_bytes(b"eval-goal"),
        tier: "corpus".into(),
        formalization: Formalization { statement: "forall x. p(x)".into(), grounding },
        vacuity,
    }
}

struct Case {
    name: &'static str,
    spec: SignedSpec,
    state: ArtifactState,
    witnesses: Vec<SignedWitness>,
    work: Vec<Work>,
    expect: Expect,
}

#[allow(clippy::too_many_lines)]
fn cases() -> Vec<Case> {
    let auditor = key(2);
    let implementer = key(4);
    let crosschecker = key(3);
    let mut out = Vec::new();

    // 1 ── The minimum, not the mean.
    {
        let spec = spec_of(vec![
            Clause::requirement("C1", "The first obligation is well evidenced."),
            Clause::requirement("C2", "The second obligation is only claimed."),
        ]);
        let ws = vec![
            witness(&spec, "C1", falsifiable(Anchor::Specification), &auditor, state().address),
            witness(&spec, "C2", Evidence::Cited, &implementer, state().address),
        ];
        out.push(Case {
            name: "01-a-mean-conceals-the-weakest-obligation",
            expect: Expect {
                intent: "One obligation at E3, one at E0.".into(),
                trap: "Averaging the rungs, or reporting the best, gives E3 or E1 \
                       where §3.2 requires the minimum."
                    .into(),
                direction: "over-grading".into(),
                grade: Some(Grade::Cited),
                attestation: Some(Attestation::SelfAttested),
                flags: vec![],
                clauses: vec![
                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
                    ExpectClause { label: "C2".into(), grade: Some(Grade::Cited), stale: 0 },
                ],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 2 ── An obligation nobody looked at empties the grade.
    {
        let spec = spec_of(vec![
            Clause::requirement("C1", "The first obligation is well evidenced."),
            Clause::requirement("C2", "The second obligation has no evidence at all."),
        ]);
        let ws = vec![witness(
            &spec,
            "C1",
            falsifiable(Anchor::Specification),
            &auditor,
            state().address,
        )];
        out.push(Case {
            name: "02-an-unevidenced-obligation-empties-the-grade",
            expect: Expect {
                intent: "One obligation at E3; the other has no witness.".into(),
                trap: "Skipping the unevidenced clause and grading the rest gives E3. \
                       Absence orders below every rung, so the grade is absent — not E0, \
                       which would claim a citation nobody made."
                    .into(),
                direction: "over-grading".into(),
                grade: None,
                attestation: None,
                flags: vec![],
                clauses: vec![
                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
                    ExpectClause { label: "C2".into(), grade: None, stale: 0 },
                ],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 3 ── A non-goal is not owed, and does not cap.
    {
        let spec = spec_of(vec![
            Clause::requirement("C1", "The obligation is well evidenced."),
            Clause::non_goal("C2", "This is deliberately not built."),
        ]);
        let ws = vec![witness(
            &spec,
            "C1",
            falsifiable(Anchor::Specification),
            &auditor,
            state().address,
        )];
        out.push(Case {
            name: "03-an-unwitnessed-non-goal-does-not-cap",
            expect: Expect {
                intent: "A requirement at E3 beside an unwitnessed non-goal.".into(),
                trap: "Treating the non-goal as an owed obligation with no evidence \
                       empties the grade. A non-goal is owed nothing, so its absence \
                       of evidence is the correct state and caps nothing."
                    .into(),
                direction: "under-grading".into(),
                grade: Some(Grade::Falsifiable),
                attestation: Some(Attestation::Independent),
                flags: vec![],
                clauses: vec![
                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
                    ExpectClause { label: "C2".into(), grade: None, stale: 0 },
                ],
                conformant_at_e3: true,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 4 ── A witnessed non-goal is a flag, and flags block conformance.
    {
        let spec = spec_of(vec![
            Clause::requirement("C1", "The obligation is well evidenced."),
            Clause::non_goal("C2", "This is deliberately not built."),
        ]);
        let ws = vec![
            witness(&spec, "C1", falsifiable(Anchor::Specification), &auditor, state().address),
            witness(&spec, "C2", falsifiable(Anchor::Specification), &auditor, state().address),
        ];
        out.push(Case {
            name: "04-evidence-for-a-non-goal-is-a-flag",
            expect: Expect {
                intent: "Something implements the clause that says not to.".into(),
                trap: "Counting the non-goal's evidence as a rung, or discarding it \
                       quietly. It is a flag, and §3.4 makes any flag block conformance \
                       even where every grade is satisfied."
                    .into(),
                direction: "over-grading".into(),
                grade: Some(Grade::Falsifiable),
                attestation: Some(Attestation::Independent),
                flags: vec!["NonGoalWitnessed".into()],
                clauses: vec![
                    ExpectClause { label: "C1".into(), grade: Some(Grade::Falsifiable), stale: 0 },
                    ExpectClause { label: "C2".into(), grade: None, stale: 0 },
                ],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 5 ── An unstated anchor caps a falsifiable check at E2.
    {
        let spec = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation is checked by something whose expectation is unstated.",
        )]);
        let ws = vec![witness(
            &spec,
            "C1",
            falsifiable(Anchor::Unstated),
            &auditor,
            state().address,
        )];
        out.push(Case {
            name: "05-an-unstated-anchor-caps-at-exercised",
            expect: Expect {
                intent: "A check with a killed counter-artifact but no stated anchor."
                    .into(),
                trap: "Reading the counter-artifact alone and awarding E3. An oracle \
                       derived from the system under test cannot disagree with it, so \
                       §2.5 caps an unstated anchor at E2 however the check behaved."
                    .into(),
                direction: "over-grading".into(),
                grade: Some(Grade::Exercised),
                attestation: Some(Attestation::Independent),
                flags: vec![],
                clauses: vec![ExpectClause {
                    label: "C1".into(),
                    grade: Some(Grade::Exercised),
                    stale: 0,
                }],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 6 ── A proof nobody independent read is E2, not E4.
    {
        let spec = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation is discharged as a proof under the prover's own formalization.",
        )]);
        let ws = vec![witness(
            &spec,
            "C1",
            proved(
                Grounding::Declared,
                Vacuity::Refuted { counter: Address::of_bytes(b"eval-counter-model") },
            ),
            &auditor,
            state().address,
        )];
        out.push(Case {
            name: "06-a-declared-formalization-caps-at-exercised",
            expect: Expect {
                intent: "A non-vacuous proof whose binding to the clause is the \
                         prover's own word."
                    .into(),
                trap: "Awarding E4 because a prover succeeded. The proof is real \
                       machine-checked evidence about something — E2 — and that the \
                       something is this clause is unconfirmed (§2.6)."
                    .into(),
                direction: "over-grading".into(),
                grade: Some(Grade::Exercised),
                attestation: Some(Attestation::Independent),
                flags: vec![],
                clauses: vec![ExpectClause {
                    label: "C1".into(),
                    grade: Some(Grade::Exercised),
                    stale: 0,
                }],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 7 ── A possibly-vacuous proof is E2, even cross-checked.
    {
        let spec = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation is discharged as a proof nobody checked for vacuity.",
        )]);
        let ws = vec![witness(
            &spec,
            "C1",
            proved(
                Grounding::CrossChecked { by: crosschecker.verifying_key().to_bytes() },
                Vacuity::Unchecked,
            ),
            &auditor,
            state().address,
        )];
        out.push(Case {
            name: "07-an-unchecked-vacuity-caps-at-exercised",
            expect: Expect {
                intent: "A proof with an independently cross-checked formalization, \
                         never shown capable of failing."
                    .into(),
                trap: "Awarding E4 because the formalization was cross-checked. A \
                       property can hold because nothing reaches the condition it \
                       guards; every rung above E2 rests on a demonstrated failure."
                    .into(),
                direction: "over-grading".into(),
                grade: Some(Grade::Exercised),
                attestation: Some(Attestation::Independent),
                flags: vec![],
                clauses: vec![ExpectClause {
                    label: "C1".into(),
                    grade: Some(Grade::Exercised),
                    stale: 0,
                }],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 8 ── A witness bound to a superseded state does not count.
    {
        let spec = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation was checked against an earlier tree.",
        )]);
        let ws = vec![witness(
            &spec,
            "C1",
            falsifiable(Anchor::Specification),
            &auditor,
            Address::of_bytes(b"eval-tree-v0"),
        )];
        out.push(Case {
            name: "08-a-superseded-state-makes-a-witness-stale",
            expect: Expect {
                intent: "The only witness observed a tree that is no longer the \
                         artifact, and declared no footprint."
                    .into(),
                trap: "Counting it because it verifies and names a stated obligation. \
                       An empty footprint means the whole artifact, so any change to \
                       the artifact invalidates it — and the clause is then unevidenced, \
                       which empties the grade rather than lowering it."
                    .into(),
                direction: "over-grading".into(),
                grade: None,
                attestation: None,
                flags: vec![],
                clauses: vec![ExpectClause {
                    label: "C1".into(),
                    grade: None,
                    stale: 1,
                }],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &implementer),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    // 9 ── A witness naming an obligation nobody stated is a flag.
    {
        let stated = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation as the specification now words it.",
        )]);
        // A witness bound to the wording the clause used to have.
        let older = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation as the specification used to word it.",
        )]);
        let ws = vec![Witness::new(
            stated.spec.spec_id().unwrap(),
            obligation(&older, "C1"),
            state().address,
            falsifiable(Anchor::Specification),
            Energy::new(1_000, Provenance::Estimator),
            auditor.verifying_key().to_bytes(),
        )
        .sign(&auditor)
        .expect("signs")];
        out.push(Case {
            name: "09-a-witness-for-a-reworded-clause-is-a-flag",
            expect: Expect {
                intent: "A verifying witness whose obligation address is the clause's \
                         previous wording."
                    .into(),
                trap: "Discarding it silently, which is how drift stops being visible. \
                       It is reported as unbound, and the clause it used to evidence \
                       is now unevidenced."
                    .into(),
                direction: "over-grading".into(),
                grade: None,
                attestation: None,
                flags: vec!["Unbound".into()],
                clauses: vec![ExpectClause {
                    label: "C1".into(),
                    grade: None,
                    stale: 0,
                }],
                conformant_at_e3: false,
            },
            work: work_by(&stated, "C1", &implementer),
            spec: stated,
            state: state(),
            witnesses: ws,
        });
    }

    // 10 ── A review by the clause's own author is a citation again.
    {
        let spec = spec_of(vec![Clause::requirement(
            "C1",
            "The obligation was reviewed by the party that wrote the specification.",
        )]);
        let ws = vec![witness(
            &spec,
            "C1",
            Evidence::Reviewed { reviewer: key(1).verifying_key().to_bytes() },
            &key(1),
            state().address,
        )];
        out.push(Case {
            name: "10-a-self-review-is-the-citation-again",
            expect: Expect {
                intent: "The reviewer and the specification's author are one key."
                    .into(),
                trap: "Awarding E1 because the evidence says `reviewed`. E1 requires a \
                       second party, and independence is computed from the keys rather \
                       than taken from the label."
                    .into(),
                direction: "over-grading".into(),
                grade: Some(Grade::Cited),
                attestation: Some(Attestation::SelfAttested),
                flags: vec![],
                clauses: vec![ExpectClause {
                    label: "C1".into(),
                    grade: Some(Grade::Cited),
                    stale: 0,
                }],
                conformant_at_e3: false,
            },
            work: work_by(&spec, "C1", &key(1)),
            spec,
            state: state(),
            witnesses: ws,
        });
    }

    out
}

fn json<T: Serialize>(value: &T) -> String {
    let mut s = serde_json::to_string_pretty(value).expect("serialises");
    s.push('\n');
    s
}

#[test]
fn every_case_reaches_the_verdict_the_specification_requires() {
    let generate = std::env::var("JOULESPEC_GEN_EVALUATION").is_ok();
    let mut mismatched = Vec::new();

    for case in cases() {
        let got = conform::evaluate(&case.spec, &case.state, &case.witnesses, &case.work)
            .unwrap_or_else(|e| panic!("{}: evaluation failed: {e}", case.name));
        let seen = observed(&got, &case.expect);

        if seen != case.expect {
            mismatched.push(format!(
                "{}\n  expected {:#?}\n  observed {:#?}",
                case.name, case.expect, seen
            ));
        }

        let into = dir().join(case.name);
        if generate {
            std::fs::create_dir_all(&into).expect("case directory");
            for (name, body) in [
                ("spec.json", json(&case.spec)),
                ("state.json", json(&case.state)),
                ("witnesses.json", json(&case.witnesses)),
                ("work.json", json(&case.work)),
                // The expectation as this test *states* it, never as the
                // evaluator produced it.
                ("expect.json", json(&case.expect)),
            ] {
                std::fs::write(into.join(name), body).expect("writes");
            }
        } else {
            let published = std::fs::read_to_string(into.join("expect.json")).unwrap_or_else(|e| {
                panic!("{}: cannot read published expectation: {e}", case.name)
            });
            let published: Expect =
                serde_json::from_str(&published).expect("published expectation parses");
            assert_eq!(
                published, case.expect,
                "{}: the published expectation and this test disagree",
                case.name
            );
        }
    }

    assert!(
        mismatched.is_empty(),
        "the evaluator disagrees with the specification on {} case(s):\n\n{}",
        mismatched.len(),
        mismatched.join("\n\n")
    );
}

/// A corpus that tested one direction would certify one direction, so this
/// asserts the shape of the set rather than trusting that it was built as
/// described.
///
/// Both directions have to be present. An implementation that graded nothing
/// at all would pass every over-grading case — the under-grading cases are
/// what stop a corpus from rewarding a rule that simply refuses everything.
#[test]
fn the_corpus_tests_both_directions_and_says_which() {
    let all = cases();
    assert!(all.len() >= 10, "the corpus has shrunk: {}", all.len());

    let mut over = 0;
    let mut under = 0;
    for case in &all {
        assert!(
            !case.expect.trap.is_empty() && !case.expect.intent.is_empty(),
            "{}: a case without a stated trap documents nothing",
            case.name
        );
        match case.expect.direction.as_str() {
            "over-grading" => {
                over += 1;
                // The correct verdict must fall short of the bar, or be
                // blocked by a flag. A case that conformed cleanly would be
                // passed by a generous implementation for the wrong reason.
                assert!(
                    !case.expect.conformant_at_e3 || !case.expect.flags.is_empty(),
                    "{}: labelled over-grading but conforms at E3 with no flag",
                    case.name
                );
            }
            "under-grading" => {
                under += 1;
                // The correct verdict must *reach* the bar, or the case
                // cannot catch an implementation that is too strict.
                assert!(
                    case.expect.conformant_at_e3,
                    "{}: labelled under-grading but does not conform at E3, so a \
                     refuse-everything implementation passes it",
                    case.name
                );
            }
            other => panic!("{}: unknown direction {other:?}", case.name),
        }
    }
    assert!(over >= 8, "too few over-grading cases: {over}");
    assert!(under >= 1, "no under-grading case: a refuse-everything evaluator passes");
}