lemma-engine 0.10.1

//! End-to-end tests for strict veto semantics under normalization.
//!
//! Normalization may only delete a subexpression whose removal cannot change the
//! result: a total operand, or a literal `false` operand of `and`, which decides the
//! conjunction whatever the other operands are. These tests pin the contract that the
//! folded and unfolded forms of the same expression produce identical evaluation
//! results for all of: value present, value missing, and operand vetoes.

use indexmap::IndexMap;
use lemma::{DateTimeValue, Engine, EvaluateDataValue};
use std::time::Instant;

fn load(code: &str) -> Engine {
    let mut engine = Engine::new();
    engine
        .load([(lemma::SourceType::Volatile, code.to_string())])
        .expect("spec must load");
    engine
}

fn run(engine: &Engine, spec: &str, inputs: &[(&str, &str)]) -> lemma::Response {
    let now = DateTimeValue::now();
    let data: IndexMap<String, EvaluateDataValue> = inputs
        .iter()
        .map(|(name, value)| (name.to_string(), (*value).into()))
        .collect();
    engine
        .evaluate(None, spec, Some(&now), data, None, false)
        .expect("evaluation must succeed")
}

fn rule_result<'response>(
    response: &'response lemma::Response,
    rule_name: &str,
) -> &'response lemma::RuleResult {
    response
        .results
        .values()
        .find(|result| result.rule.name == rule_name)
        .unwrap_or_else(|| panic!("rule '{rule_name}' must be in the response"))
}

#[test]
fn multiply_by_zero_with_missing_data_vetoes() {
    let engine = load(
        r#"
spec strict_multiply
data x: number
rule r: x * 0
"#,
    );

    let missing = run(&engine, "strict_multiply", &[]);
    let result = rule_result(&missing, "r");
    assert!(
        result.vetoed,
        "x is missing: the multiply must veto, not fold to 0"
    );

    let supplied = run(&engine, "strict_multiply", &[("x", "7")]);
    let result = rule_result(&supplied, "r");
    assert!(!result.vetoed);
    assert_eq!(result.result(), Some("0"));
}

#[test]
fn multiply_measure_data_by_zero_keeps_unit() {
    let engine = load(
        r#"
spec strict_measure_multiply
data money: measure -> unit eur: 1
data price: money
rule r: price * 0
"#,
    );

    let response = run(&engine, "strict_measure_multiply", &[("price", "5 eur")]);
    let result = rule_result(&response, "r");
    assert!(!result.vetoed);
    assert_eq!(
        result.result(),
        Some("0 eur"),
        "the runtime multiply must keep the measure's unit"
    );

    let missing = run(&engine, "strict_measure_multiply", &[]);
    let result = rule_result(&missing, "r");
    assert!(result.vetoed, "price is missing: the multiply must veto");
}

#[test]
fn multiply_measure_literal_by_zero_folds_to_typed_zero() {
    let engine = load(
        r#"
spec folded_measure_multiply
data money: measure -> unit eur: 1
data rate: 5 eur
rule r: rate * 0
"#,
    );

    // `rate` is bound in the spec, so the inlined literal product folds at
    // planning time; the folded zero must keep the unit signature.
    let response = run(&engine, "folded_measure_multiply", &[]);
    let result = rule_result(&response, "r");
    assert!(!result.vetoed);
    assert_eq!(result.result(), Some("0 eur"));
}

#[test]
fn multiply_vetoing_rule_by_zero_propagates_the_veto() {
    let engine = load(
        r#"
spec strict_veto_multiply
rule blocked: veto "credit check failed"
rule r: blocked * 0
"#,
    );

    let response = run(&engine, "strict_veto_multiply", &[]);
    let result = rule_result(&response, "r");
    assert!(
        result.vetoed,
        "the inlined veto must propagate through the multiply"
    );
    assert_eq!(result.veto_reason.as_deref(), Some("credit check failed"));
}

#[test]
fn and_with_literal_false_is_false_without_missing_data() {
    let engine = load(
        r#"
spec strict_and
data flag: boolean
rule r: flag and (1 > 2)
"#,
    );

    // `1 > 2` constant-folds to `false`, which decides the conjunction whatever
    // `flag` is, so a missing `flag` does not veto.
    let missing = run(&engine, "strict_and", &[]);
    let result = rule_result(&missing, "r");
    assert!(!result.vetoed, "flag is not needed: false decides the and");
    assert_eq!(result.result(), Some("false"));

    let supplied = run(&engine, "strict_and", &[("flag", "yes")]);
    let result = rule_result(&supplied, "r");
    assert!(!result.vetoed);
    assert_eq!(result.result(), Some("false"));
}

#[test]
fn exp_of_log_keeps_domain_veto() {
    let engine = load(
        r#"
spec strict_exp_log
data offset: number
rule r: exp (log offset)
"#,
    );

    let negative = run(&engine, "strict_exp_log", &[("offset", "-5")]);
    let result = rule_result(&negative, "r");
    assert!(
        result.vetoed,
        "log of a negative operand must veto; the exp/log collapse would erase it"
    );

    let positive = run(&engine, "strict_exp_log", &[("offset", "5")]);
    let result = rule_result(&positive, "r");
    assert!(!result.vetoed);
}

#[test]
fn power_zero_with_missing_data_vetoes() {
    let engine = load(
        r#"
spec strict_power_zero
data x: number
rule r: x ^ 0
"#,
    );

    let missing = run(&engine, "strict_power_zero", &[]);
    let result = rule_result(&missing, "r");
    assert!(
        result.vetoed,
        "x is missing: the power must veto, not fold to 1"
    );

    let supplied = run(&engine, "strict_power_zero", &[("x", "9")]);
    let result = rule_result(&supplied, "r");
    assert!(!result.vetoed);
    assert_eq!(result.result(), Some("1"));
}

#[test]
fn self_doubling_rule_chain_shares_graph_cells() {
    // Each rule references its predecessor twice. Shared NormalForm graph
    // growth is linear in chain length — not Expression tree blowup.
    // Cell-count band is asserted in transitive_normalization_plan_shape::
    // doubling_chain_graph_stays_linear (crate-private normal_forms table).
    let n = 40;
    let mut code = String::from("\nspec doubling\ndata input: number\nrule r0: input > 0\n");
    for index in 1..=n {
        code.push_str(&format!(
            "rule r{index}: r{previous} and not r{previous}\n",
            previous = index - 1
        ));
    }

    let started = Instant::now();
    let mut engine = Engine::new();
    engine
        .load([(lemma::SourceType::Volatile, code.to_string())])
        .expect("shared-graph self-doubling chain must plan");
    let response = run(&engine, "doubling", &[("input", "1")]);
    let result = rule_result(&response, &format!("r{n}"));
    assert!(!result.vetoed);
    assert_eq!(result.result(), Some("false"));
    // Regression guard only (not a microbench). Pre-DAG-collect walks blew past
    // this at much smaller n (~18s at n=12).
    assert!(
        started.elapsed().as_secs_f64() < 2.0,
        "doubling n={n} load+run took {:?}; expected shared-graph path",
        started.elapsed()
    );
}

#[derive(Debug)]
enum Outcome {
    Result(&'static str),
    Missing(Vec<&'static str>),
    Veto(&'static str),
}

fn assert_outcome(result: &lemma::RuleResult, expected: &Outcome, context: &str) {
    match expected {
        Outcome::Result(value) => {
            assert!(
                !result.vetoed,
                "{context}: expected {value}, got {result:?}"
            );
            assert_eq!(result.result(), Some(*value), "{context}");
        }
        Outcome::Missing(names) => {
            assert!(
                result.vetoed,
                "{context}: expected missing data, got {result:?}"
            );
            let mut actual = result.missing_data().to_vec();
            actual.sort();
            let mut wanted: Vec<String> = names.iter().map(|name| name.to_string()).collect();
            wanted.sort();
            assert_eq!(actual, wanted, "{context}");
        }
        Outcome::Veto(reason) => {
            assert!(result.vetoed, "{context}: expected veto, got {result:?}");
            assert_eq!(result.veto_reason.as_deref(), Some(*reason), "{context}");
            assert!(result.missing_data().is_empty(), "{context}");
        }
    }
}

const RESIDUAL_FIRST_FOLDED: &str = r#"
spec order
data model: text
data extra: boolean
data flag_c: boolean
data amount: number
rule r: 0
  unless model is "b" and extra then amount
  unless flag_c and model is "c" then 3
"#;

const RESIDUAL_FIRST_UNFOLDED: &str = r#"
spec order
data model: text
data extra: boolean
data flag_c: boolean
data amount: number
rule r: 0
  unless model is "b" and extra then amount
  unless flag_c and model is "c" then 3
  unless model is "z" then 9
"#;

#[test]
fn residual_first_conjunction_folded_and_unfolded_agree() {
    let cases: [(&[(&str, &str)], Outcome); 6] = [
        (
            &[("model", "b"), ("extra", "true"), ("amount", "5")],
            Outcome::Result("5"),
        ),
        (
            &[("model", "b"), ("extra", "true")],
            Outcome::Missing(vec!["amount"]),
        ),
        (&[("model", "b"), ("extra", "false")], Outcome::Result("0")),
        (&[("model", "c")], Outcome::Missing(vec!["flag_c"])),
        (&[("model", "c"), ("flag_c", "false")], Outcome::Result("0")),
        (&[("model", "c"), ("flag_c", "true")], Outcome::Result("3")),
    ];
    for (form, source) in [
        ("folded", RESIDUAL_FIRST_FOLDED),
        ("unfolded", RESIDUAL_FIRST_UNFOLDED),
    ] {
        let engine = load(source);
        for (inputs, expected) in &cases {
            let response = run(&engine, "order", inputs);
            let result = rule_result(&response, "r");
            let context = format!("{form} {inputs:?}");
            match (form, expected) {
                // The unfolded piecewise keeps lower-priority arms live while an
                // undecided arm is unknown, so its missing list may add data.
                ("unfolded", Outcome::Missing(names)) => {
                    assert!(
                        result.vetoed,
                        "{context}: expected missing data, got {result:?}"
                    );
                    for name in names {
                        assert!(
                            result.missing_data().iter().any(|actual| actual == name),
                            "{context}: missing list {:?} does not include {name}",
                            result.missing_data()
                        );
                    }
                }
                _ => assert_outcome(result, expected, &context),
            }
        }
    }
}

#[derive(Clone, Copy, Debug, PartialEq)]
enum OperandKind {
    True,
    False,
    Missing,
    Veto,
}

/// Operand text for the matrix spec. `Veto` operands are the rule `blocked`.
fn operand_expression(kind: OperandKind, name: &'static str) -> &'static str {
    match kind {
        OperandKind::Veto => "blocked",
        OperandKind::True | OperandKind::False | OperandKind::Missing => name,
    }
}

/// Expected outcome of `first and second`, in evaluation order. A false operand
/// decides regardless of position. Otherwise the first missing or vetoed operand in
/// source order propagates.
fn expected_and(
    first: (OperandKind, &'static str),
    second: (OperandKind, &'static str),
) -> Outcome {
    let operands = [first, second];
    if operands.iter().any(|(kind, _)| *kind == OperandKind::False) {
        return Outcome::Result("false");
    }
    for (kind, _) in operands {
        match kind {
            OperandKind::True => {}
            OperandKind::False => unreachable!("BUG: false operand decided above"),
            OperandKind::Missing => {
                let names = operands
                    .iter()
                    .filter(|(kind, _)| *kind == OperandKind::Missing)
                    .map(|(_, name)| *name)
                    .collect();
                return Outcome::Missing(names);
            }
            OperandKind::Veto => return Outcome::Veto("blocked"),
        }
    }
    Outcome::Result("true")
}

#[test]
fn and_is_order_independent_for_every_operand_kind_pair() {
    let kinds = [
        OperandKind::True,
        OperandKind::False,
        OperandKind::Missing,
        OperandKind::Veto,
    ];
    for first_kind in kinds {
        for second_kind in kinds {
            let first = (first_kind, "a");
            let second = (second_kind, "b");
            let engine = load(&format!(
                r#"
spec matrix
data a: boolean
data b: boolean
rule blocked: veto "blocked"
rule forward: {} and {}
rule backward: {} and {}
"#,
                operand_expression(first_kind, "a"),
                operand_expression(second_kind, "b"),
                operand_expression(second_kind, "b"),
                operand_expression(first_kind, "a"),
            ));
            let mut inputs: Vec<(&str, &str)> = Vec::new();
            match first_kind {
                OperandKind::True => inputs.push(("a", "true")),
                OperandKind::False => inputs.push(("a", "false")),
                OperandKind::Missing | OperandKind::Veto => {}
            }
            match second_kind {
                OperandKind::True => inputs.push(("b", "true")),
                OperandKind::False => inputs.push(("b", "false")),
                OperandKind::Missing | OperandKind::Veto => {}
            }
            let response = run(&engine, "matrix", &inputs);
            assert_outcome(
                rule_result(&response, "forward"),
                &expected_and(first, second),
                &format!("forward {first_kind:?} and {second_kind:?}"),
            );
            assert_outcome(
                rule_result(&response, "backward"),
                &expected_and(second, first),
                &format!("backward {second_kind:?} and {first_kind:?}"),
            );
        }
    }
}