aprender-contracts 0.68.1

use super::*;

#[test]
fn obligation_type_display() {
    assert_eq!(ObligationType::Invariant.to_string(), "invariant");
    assert_eq!(ObligationType::Equivalence.to_string(), "equivalence");
    assert_eq!(ObligationType::Bound.to_string(), "bound");
    assert_eq!(ObligationType::Monotonicity.to_string(), "monotonicity");
    assert_eq!(ObligationType::Idempotency.to_string(), "idempotency");
    assert_eq!(ObligationType::Linearity.to_string(), "linearity");
    assert_eq!(ObligationType::Symmetry.to_string(), "symmetry");
    assert_eq!(ObligationType::Associativity.to_string(), "associativity");
    assert_eq!(ObligationType::Conservation.to_string(), "conservation");
    assert_eq!(ObligationType::Ordering.to_string(), "ordering");
    assert_eq!(ObligationType::Completeness.to_string(), "completeness");
    assert_eq!(ObligationType::Soundness.to_string(), "soundness");
    assert_eq!(ObligationType::Involution.to_string(), "involution");
    assert_eq!(ObligationType::Determinism.to_string(), "determinism");
    assert_eq!(ObligationType::Roundtrip.to_string(), "roundtrip");
    assert_eq!(ObligationType::StateMachine.to_string(), "state_machine");
    assert_eq!(ObligationType::Classification.to_string(), "classification");
    assert_eq!(ObligationType::Independence.to_string(), "independence");
    assert_eq!(ObligationType::Termination.to_string(), "termination");
    // Eiffel DbC types
    assert_eq!(ObligationType::Precondition.to_string(), "precondition");
    assert_eq!(ObligationType::Postcondition.to_string(), "postcondition");
    assert_eq!(ObligationType::Frame.to_string(), "frame");
    assert_eq!(ObligationType::LoopInvariant.to_string(), "loop_invariant");
    assert_eq!(ObligationType::LoopVariant.to_string(), "loop_variant");
    assert_eq!(ObligationType::OldState.to_string(), "old_state");
    assert_eq!(ObligationType::Subcontract.to_string(), "subcontract");
}

#[test]
fn lean_status_display() {
    assert_eq!(LeanStatus::Proved.to_string(), "proved");
    assert_eq!(LeanStatus::Sorry.to_string(), "sorry");
    assert_eq!(LeanStatus::Wip.to_string(), "wip");
    assert_eq!(LeanStatus::NotApplicable.to_string(), "not-applicable");
}

#[test]
fn lean_status_default_is_sorry() {
    assert_eq!(LeanStatus::default(), LeanStatus::Sorry);
}

#[test]
fn kani_strategy_display() {
    assert_eq!(KaniStrategy::Exhaustive.to_string(), "exhaustive");
    assert_eq!(KaniStrategy::StubFloat.to_string(), "stub_float");
    assert_eq!(KaniStrategy::Compositional.to_string(), "compositional");
    assert_eq!(KaniStrategy::BoundedInt.to_string(), "bounded_int");
}

#[test]
fn contract_kind_display() {
    assert_eq!(ContractKind::Kernel.to_string(), "kernel");
    assert_eq!(ContractKind::Registry.to_string(), "registry");
    assert_eq!(ContractKind::ModelFamily.to_string(), "model-family");
    assert_eq!(
        ContractKind::ModelFamilyVariant.to_string(),
        "model-family-variant",
    );
    assert_eq!(ContractKind::Tokenizer.to_string(), "tokenizer");
    assert_eq!(ContractKind::TrainingLoop.to_string(), "training-loop");
    assert_eq!(
        ContractKind::PretrainingCorpus.to_string(),
        "pretraining-corpus",
    );
    assert_eq!(
        ContractKind::TrainingPreconditionGate.to_string(),
        "training-precondition-gate",
    );
    assert_eq!(ContractKind::CorpusAssembly.to_string(), "corpus-assembly");
    assert_eq!(ContractKind::Pattern.to_string(), "pattern");
    assert_eq!(ContractKind::Schema.to_string(), "schema");
}

#[test]
fn contract_kind_default_is_kernel() {
    assert_eq!(ContractKind::default(), ContractKind::Kernel);
}

#[test]
fn kernel_contract_requires_proofs() {
    let mut c = Contract::default();
    c.metadata.kind = ContractKind::Kernel;
    assert!(c.requires_proofs());
    assert_eq!(c.kind(), ContractKind::Kernel);
    assert!(!c.is_registry());
    // Provability violations: no proof_obligations, no falsification_tests,
    // no kani_harnesses.
    assert!(!c.provability_violations().is_empty());
}

#[test]
fn non_kernel_kinds_exempt_from_provability() {
    for kind in [
        ContractKind::Registry,
        ContractKind::ModelFamily,
        ContractKind::ModelFamilyVariant,
        ContractKind::Tokenizer,
        ContractKind::TrainingLoop,
        ContractKind::PretrainingCorpus,
        ContractKind::TrainingPreconditionGate,
        ContractKind::CorpusAssembly,
        ContractKind::Pattern,
        ContractKind::Schema,
    ] {
        let mut c = Contract::default();
        c.metadata.kind = kind;
        assert!(
            !c.requires_proofs(),
            "kind {kind:?} should not require proofs",
        );
        assert!(
            c.provability_violations().is_empty(),
            "kind {kind:?} should have no provability violations",
        );
    }
}

#[test]
fn legacy_registry_flag_maps_to_registry_kind() {
    let mut c = Contract::default();
    c.metadata.registry = true;
    // kind remains Kernel (default), but is_registry() and kind() both
    // reflect the legacy flag for back-compat.
    assert!(c.is_registry());
    assert_eq!(c.kind(), ContractKind::Registry);
    assert!(!c.requires_proofs());
    assert!(c.provability_violations().is_empty());
}

#[test]
fn explicit_kind_overrides_default() {
    let mut c = Contract::default();
    c.metadata.kind = ContractKind::ModelFamily;
    assert_eq!(c.kind(), ContractKind::ModelFamily);
    // ModelFamily is not a registry
    assert!(!c.is_registry());
}

// ── Beat::evaluate — the falsifiable verdict (PMAT-741) ───────────────────────

/// Build a minimal Beat with the given direction + threshold.
fn beat(direction: &str, threshold: Option<f64>) -> Beat {
    Beat {
        direction: direction.to_string(),
        beat_threshold: threshold,
        ..Beat::default()
    }
}

#[test]
fn beat_evaluate_higher_is_better() {
    let b = beat("higher_is_better", Some(0.92));
    // at/above threshold = won (accuracy: bigger is better)
    assert_eq!(b.evaluate(0.94), Some(BeatOutcome::Won));
    assert_eq!(b.evaluate(0.92), Some(BeatOutcome::Won)); // boundary is a win
    assert_eq!(b.evaluate(0.91), Some(BeatOutcome::Regressed));
    assert!(b.is_won(0.99));
    assert!(!b.is_won(0.50));
}

#[test]
fn beat_evaluate_lower_is_better() {
    let b = beat("lower_is_better", Some(440.0));
    // at/below threshold = won (wall-clock ms: smaller is better)
    assert_eq!(b.evaluate(400.0), Some(BeatOutcome::Won));
    assert_eq!(b.evaluate(440.0), Some(BeatOutcome::Won)); // boundary is a win
    assert_eq!(b.evaluate(441.0), Some(BeatOutcome::Regressed));
    assert!(b.is_won(10.0));
    assert!(!b.is_won(1000.0));
}

#[test]
fn beat_evaluate_malformed_is_none_not_pass() {
    // No threshold → cannot judge.
    assert_eq!(beat("higher_is_better", None).evaluate(0.99), None);
    // Unknown direction → cannot judge.
    assert_eq!(beat("sideways", Some(0.9)).evaluate(0.99), None);
    // Non-finite inputs → cannot judge.
    assert_eq!(beat("higher_is_better", Some(f64::NAN)).evaluate(0.9), None);
    assert_eq!(
        beat("higher_is_better", Some(0.9)).evaluate(f64::INFINITY),
        None
    );
    // A malformed contract is NOT a win.
    assert!(!beat("sideways", Some(0.9)).is_won(0.99));
    assert!(!beat("higher_is_better", None).is_won(0.99));
}

#[test]
fn beat_evaluate_matches_pilot_iris_contract() {
    // The shipped pilot: accuracy, higher_is_better, threshold 0.92. apr's
    // measured 0.94 must read as WON, a hypothetical 0.90 as REGRESSED.
    let b = beat("higher_is_better", Some(0.9200));
    assert_eq!(b.evaluate(0.9400), Some(BeatOutcome::Won));
    assert_eq!(b.evaluate(0.9000), Some(BeatOutcome::Regressed));
}

/// #3314: `id:` must survive deserialization, and its absence must be `None`.
///
/// Until this field existed, `ProofObligation` had no `id` and there is no
/// `deny_unknown_fields`, so `id:` was written to disk and **silently dropped
/// on parse**. 3,612 generated ids were decoration: no consumer could read one.
/// This test is the durable form of that check -- deleting the field, or
/// renaming it in serde, turns it red rather than quietly reverting the corpus
/// to unciteable.
#[test]
fn proof_obligation_id_survives_deserialization() {
    let yaml = "
- id: GDN-BND-001
  type: bound
  property: Decay in unit interval
- type: invariant
  property: an obligation with no id
";
    let obs: Vec<ProofObligation> =
        serde_yaml::from_str(yaml).expect("two obligations, one with an id");
    assert_eq!(obs.len(), 2);
    assert_eq!(
        obs[0].id.as_deref(),
        Some("GDN-BND-001"),
        "id: was dropped on parse — every generated obligation id is decoration again"
    );
    assert_eq!(
        obs[1].id, None,
        "an obligation with no id must read as None"
    );
}

/// The id must also survive a round trip, because `pv unlock` writes contracts
/// back. It does so through `serde_yaml::Value` today, so unknown keys survive
/// regardless — but if anyone ever "improves" that into a typed round trip,
/// `skip_serializing_if` plus this test are what stop it silently stripping
/// 3,750 ids file by file.
#[test]
fn proof_obligation_id_survives_a_typed_round_trip() {
    let ob = ProofObligation {
        id: Some("QHF-INV-004".to_string()),
        property: "Block outputs from exactly one attention type".to_string(),
        ..Default::default()
    };
    let round: ProofObligation =
        serde_yaml::from_str(&serde_yaml::to_string(&ob).expect("serialize")).expect("deserialize");
    assert_eq!(round.id.as_deref(), Some("QHF-INV-004"));

    // and an obligation without one must not gain an empty `id:` key
    let bare = ProofObligation::default();
    let text = serde_yaml::to_string(&bare).expect("serialize");
    assert!(
        !text.contains("id:"),
        "a None id must be omitted, not written as null: {text}"
    );
}

// ── PMAT-3091: not-applicable-to-unit-tests obligations ───────────────────

fn na_obligation_from(yaml: &str) -> ProofObligation {
    serde_yaml::from_str(yaml).expect("obligation fixture must parse")
}

#[test]
fn applies_to_not_applicable_deserializes_to_not_applicable_not_other() {
    let ob = na_obligation_from("property: p\napplies_to: not_applicable\n");
    assert_eq!(ob.applies_to, Some(AppliesTo::NotApplicable));
    assert_ne!(ob.applies_to, Some(AppliesTo::Other));
}

#[test]
fn applies_to_na_alias_maps_ahead_of_the_catch_all() {
    let ob = na_obligation_from("property: p\napplies_to: N/A\n");
    assert_eq!(ob.applies_to, Some(AppliesTo::NotApplicable));
}

#[test]
fn applies_to_unknown_target_still_parses_as_other() {
    let ob = na_obligation_from("property: p\napplies_to: huber\n");
    assert_eq!(ob.applies_to, Some(AppliesTo::Other));
}

#[test]
fn na_fields_are_typed_and_read() {
    let ob = na_obligation_from(
        "property: p\napplies_to: not_applicable\nna_reason: a checkpoint fact\nna_owner: pv check\n",
    );
    assert_eq!(ob.na_reason.as_deref(), Some("a checkpoint fact"));
    assert_eq!(ob.na_owner.as_deref(), Some("pv check"));
    assert!(ob.is_not_applicable());
}

#[test]
fn na_roundtrip_keeps_not_applicable_and_both_fields() {
    let ob = na_obligation_from(
        "property: p\napplies_to: N/A\nna_reason: an O() with no constant\nna_owner: bench qwen35\n",
    );
    let yaml = serde_yaml::to_string(&ob).expect("serialize");
    assert!(yaml.contains("applies_to: not_applicable"), "{yaml}");
    let back = na_obligation_from(&yaml);
    assert_eq!(back.applies_to, Some(AppliesTo::NotApplicable));
    assert_eq!(back.na_reason.as_deref(), Some("an O() with no constant"));
    assert_eq!(back.na_owner.as_deref(), Some("bench qwen35"));
}

#[test]
fn na_fields_absent_are_not_serialized() {
    let ob = na_obligation_from("property: p\napplies_to: all\n");
    let yaml = serde_yaml::to_string(&ob).expect("serialize");
    assert!(
        !yaml.contains("na_reason") && !yaml.contains("na_owner"),
        "{yaml}"
    );
    assert!(!ob.is_not_applicable());
}

/// PMAT-3091 migration: the Lean-N/A justification that silu-kernel-v1 and
/// tokenizer-v1 wrote as an untyped `na_reason:` (dropped by serde) now lives
/// in the typed `lean: { status: not-applicable, notes: ... }` form. This
/// test is the consumer that proves the text is READ, verbatim, and that the
/// unit-test N/A fields stay free for their own meaning.
#[test]
fn na_lean_migration_reason_text_is_read_from_typed_lean_notes() {
    let cases: [(&str, usize, &str); 5] = [
        ("silu-kernel-v1.yaml", 6, "Empirical floating-point ULP equivalence between the AVX2 exp approximation and the scalar path is a runtime/hardware property (IEEE-754 rounding), not an analytic real-number identity. Enforced by FALSIFY-SI-004 / KANI-SILU_K-007."),
        ("tokenizer-v1.yaml", 4, "File IO + JSON/GGUF/protobuf parsing of a real on-disk artifact — no algebraic identity to discharge; verified by loader unit tests (FALSIFY-TOK-001/003)."),
        ("tokenizer-v1.yaml", 5, "The '≈ modulo whitespace' relation is a runtime property of arbitrary UTF-8 byte streams / normalizer state, not a closed-form identity; the exact-inverse core is proved by Tokenizer.decode_encode, the byte-edge behaviour is empirical."),
        ("tokenizer-v1.yaml", 6, "Depends on the contents of a runtime JSON config (special_tokens_map / added_tokens); a data-driven parse, not an analytic statement."),
        ("tokenizer-v1.yaml", 7, "GGUF may report a padded vocab_size differing from the token count; reconciling a reported file field against the actual count is an empirical cross-file check, not an algebraic identity."),
    ];
    for (stem, index, reason) in cases {
        let path = std::path::Path::new(env!("CARGO_MANIFEST_DIR"))
            .join("../../contracts")
            .join(stem);
        let contract = crate::schema::parse_contract(&path).expect("contract must parse");
        let ob = &contract.proof_obligations[index];
        let lean = ob
            .lean
            .as_ref()
            .expect("migrated obligation carries a typed lean block");
        assert_eq!(lean.status, LeanStatus::NotApplicable, "{stem}[{index}]");
        assert_eq!(lean.notes.as_deref(), Some(reason), "{stem}[{index}]");
        assert!(
            ob.na_reason.is_none() && ob.na_owner.is_none(),
            "{stem}[{index}]"
        );
        assert!(
            !ob.is_not_applicable(),
            "Lean-N/A is not unit-test N/A: {stem}[{index}]"
        );
    }
}