openlatch-client 0.3.3

//! Strong-Kleene three-valued logic — plan 02 §2e, PRD §Facts.
//!
//! A fact leaf is three-valued: present-and-matching, present-and-not-matching,
//! or *unknown* — and unknown is never silently a default.
//!
//! The type is what makes a fact-level default *impossible to express*, which is
//! the point (D12, "no fail-open/fail-closed dilemma"). There is no
//! `unwrap_or(false)` in this design and adding one is not an optimisation:
//! [`Kleene`] has no `Default`, no `From<Kleene> for bool`, and no accessor that
//! hands a caller a boolean without making them say what ⊥ means. A ⊥ that
//! reaches an atom's condition routes to that atom's `on_inconclusive`; it never
//! collapses into `false` on the way there.
//!
//! # The tables are written out, and there is no short-circuit
//!
//! [`Kleene::all`] and [`Kleene::any`] take a **slice of already-evaluated
//! values**, not closures. That is the whole reason for the signature: a
//! short-circuiting AND stops at the first `False` and never notices that a
//! later child was ⊥, which is exactly the information `inconclusive_facts[]`
//! carries. The corpus pins it — `04-kleene-no-short-circuit.json` is an AND
//! whose verdict is unchanged by the third child and whose
//! `inconclusive_facts[]` is not.
//!
//! # Which reason survives a fold
//!
//! ⊥ ∧ ⊥ and ⊥ ∨ ⊥ are ⊥, and the two operands may carry different reasons. The
//! **left** one wins, so a left-to-right fold is deterministic and a replay of
//! the same row yields the same bytes. Nothing downstream reads it: the record's
//! `inconclusive_facts[]` is accumulated at the LEAF, by `fact_id`, not derived
//! from the reason a folded ⊥ happens to carry.

/// Three-valued truth. `Unknown` carries **why**, because the reason is what the
/// decision reports in `inconclusive_facts[]`.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Kleene {
    True,
    False,
    Unknown(Inconclusive),
}

/// Why a leaf could not be decided — PRD §Facts, resolution order.
#[derive(Debug, Clone, Copy, PartialEq, Eq)]
pub enum Inconclusive {
    /// Absent, or a fact kind this engine does not know. Also what an
    /// unfetchable, oversize or hash-mismatching `fact_ref` resolves to — never
    /// a default, never a bundle rejection.
    Absent,
    /// `now_ms − observed_at > max_age_s + leeway_s`, or outside
    /// `valid_from`/`valid_until`.
    Stale,
    /// A miss against a fact that does not declare `closed_world`. A miss under
    /// `closed_world` is `False`, not this.
    OpenWorldMiss,
}

impl Inconclusive {
    /// Whether this ⊥ names a FACT that could not be resolved, and therefore
    /// belongs in `decision.inconclusive_facts[]`.
    ///
    /// [`Inconclusive::OpenWorldMiss`] does not: the fact resolved perfectly
    /// well and the engine read it — what is unknown is whether a *candidate* is
    /// in a set that does not claim to be exhaustive. Reporting the fact id
    /// there would say "we could not read `approved_domains`" about a bundle
    /// that shipped it, fresh, and was read. The corpus pins the distinction:
    /// `fact-open-world-miss-is-bottom` takes the ⊥ branch (`ask`) with
    /// `inconclusive_facts: []`, while `fact-stale-beyond-max-age` takes the
    /// same branch **and** names the fact.
    pub fn names_a_fact(self) -> bool {
        matches!(self, Inconclusive::Absent | Inconclusive::Stale)
    }
}

impl Kleene {
    /// The neutral unknown, for a caller that has no reason to give.
    pub const UNKNOWN: Kleene = Kleene::Unknown(Inconclusive::Absent);

    /// A plain boolean lifted into the lattice.
    pub fn from_bool(value: bool) -> Kleene {
        if value {
            Kleene::True
        } else {
            Kleene::False
        }
    }

    /// Whether this value is one of the two decided ones.
    pub fn is_known(self) -> bool {
        !matches!(self, Kleene::Unknown(_))
    }

    /// The reason, when this value is ⊥.
    ///
    /// Deliberately NOT an `unwrap_or`-shaped accessor: it hands back why the
    /// engine could not decide, never a decision it did not make.
    pub fn reason(self) -> Option<Inconclusive> {
        match self {
            Kleene::Unknown(reason) => Some(reason),
            _ => None,
        }
    }

    /// Strong-Kleene negation: `¬⊥ = ⊥`, reason preserved.
    ///
    /// | `p` | `¬p` |
    /// | --- | ---- |
    /// | T   | F    |
    /// | F   | T    |
    /// | ⊥   | ⊥    |
    ///
    /// Also reachable as `!value`.
    pub fn negate(self) -> Kleene {
        match self {
            Kleene::True => Kleene::False,
            Kleene::False => Kleene::True,
            Kleene::Unknown(reason) => Kleene::Unknown(reason),
        }
    }

    /// Strong-Kleene conjunction — all nine cells, written out.
    ///
    /// | `∧` | T | F | ⊥ |
    /// | --- | - | - | - |
    /// | T   | T | F | ⊥ |
    /// | F   | F | F | **F** |
    /// | ⊥   | ⊥ | **F** | ⊥ |
    ///
    /// The two bold cells are what makes this *strong* Kleene and not the weak
    /// (Kleene-Bochvar) table: a decided `false` DOMINATES an unknown, because
    /// "this is false whatever the unknown turns out to be" is a thing the
    /// engine genuinely knows. Weakening them would turn every atom sitting
    /// beside an unresolvable fact into an `on_inconclusive`, which is how a
    /// single unpopulated fact set would take a whole zone's enforcement with it.
    pub fn and(self, other: Kleene) -> Kleene {
        match (self, other) {
            (Kleene::False, _) | (_, Kleene::False) => Kleene::False,
            (Kleene::True, Kleene::True) => Kleene::True,
            (Kleene::Unknown(reason), _) => Kleene::Unknown(reason),
            (Kleene::True, Kleene::Unknown(reason)) => Kleene::Unknown(reason),
        }
    }

    /// Strong-Kleene disjunction — all nine cells, written out.
    ///
    /// | `∨` | T | F | ⊥ |
    /// | --- | - | - | - |
    /// | T   | T | T | **T** |
    /// | F   | T | F | ⊥ |
    /// | ⊥   | **T** | ⊥ | ⊥ |
    ///
    /// The dual of [`Kleene::and`]: a decided `true` dominates an unknown.
    pub fn or(self, other: Kleene) -> Kleene {
        match (self, other) {
            (Kleene::True, _) | (_, Kleene::True) => Kleene::True,
            (Kleene::False, Kleene::False) => Kleene::False,
            (Kleene::Unknown(reason), _) => Kleene::Unknown(reason),
            (Kleene::False, Kleene::Unknown(reason)) => Kleene::Unknown(reason),
        }
    }

    /// Fold a conjunction over children that are **already evaluated**. Empty is
    /// [`Kleene::True`], the identity.
    ///
    /// It takes a slice and not an iterator of closures on purpose: building the
    /// slice is what forces every child to be evaluated, so no caller can
    /// short-circuit past a ⊥ that `inconclusive_facts[]` needed. See the module
    /// header.
    pub fn all(values: &[Kleene]) -> Kleene {
        values
            .iter()
            .fold(Kleene::True, |left, right| left.and(*right))
    }

    /// Fold a disjunction over children that are **already evaluated**. Empty is
    /// [`Kleene::False`], the identity. Same no-short-circuit rule as
    /// [`Kleene::all`].
    pub fn any(values: &[Kleene]) -> Kleene {
        values
            .iter()
            .fold(Kleene::False, |left, right| left.or(*right))
    }
}

impl std::ops::Not for Kleene {
    type Output = Kleene;

    fn not(self) -> Kleene {
        self.negate()
    }
}

#[cfg(test)]
mod tests {
    use super::*;

    /// A ⊥ whose reason is not the one under test, so a table cell that quietly
    /// invented `Absent` would show up.
    const STALE: Kleene = Kleene::Unknown(Inconclusive::Stale);
    const MISS: Kleene = Kleene::Unknown(Inconclusive::OpenWorldMiss);

    #[test]
    fn the_negation_table_in_full() {
        assert_eq!(Kleene::True.negate(), Kleene::False);
        assert_eq!(Kleene::False.negate(), Kleene::True);
        assert_eq!(Kleene::UNKNOWN.negate(), Kleene::UNKNOWN);
        assert_eq!(STALE.negate(), STALE, "¬⊥ is ⊥ with the SAME reason");
        assert_eq!(MISS.negate(), MISS);
    }

    #[test]
    fn not_is_negate() {
        for value in [Kleene::True, Kleene::False, Kleene::UNKNOWN, STALE, MISS] {
            assert_eq!(!value, value.negate());
        }
    }

    #[test]
    fn the_conjunction_table_in_full() {
        // Row T
        assert_eq!(Kleene::True.and(Kleene::True), Kleene::True);
        assert_eq!(Kleene::True.and(Kleene::False), Kleene::False);
        assert_eq!(Kleene::True.and(STALE), STALE);
        // Row F — a decided false DOMINATES, including over ⊥. Strong Kleene.
        assert_eq!(Kleene::False.and(Kleene::True), Kleene::False);
        assert_eq!(Kleene::False.and(Kleene::False), Kleene::False);
        assert_eq!(Kleene::False.and(STALE), Kleene::False);
        // Row ⊥
        assert_eq!(STALE.and(Kleene::True), STALE);
        assert_eq!(STALE.and(Kleene::False), Kleene::False);
        assert_eq!(STALE.and(MISS), STALE, "the LEFT reason survives");
    }

    #[test]
    fn the_disjunction_table_in_full() {
        // Row T — a decided true DOMINATES, including over ⊥.
        assert_eq!(Kleene::True.or(Kleene::True), Kleene::True);
        assert_eq!(Kleene::True.or(Kleene::False), Kleene::True);
        assert_eq!(Kleene::True.or(STALE), Kleene::True);
        // Row F
        assert_eq!(Kleene::False.or(Kleene::True), Kleene::True);
        assert_eq!(Kleene::False.or(Kleene::False), Kleene::False);
        assert_eq!(Kleene::False.or(STALE), STALE);
        // Row ⊥
        assert_eq!(STALE.or(Kleene::True), Kleene::True);
        assert_eq!(STALE.or(Kleene::False), STALE);
        assert_eq!(STALE.or(MISS), STALE, "the LEFT reason survives");
    }

    #[test]
    fn both_connectives_are_commutative_in_truth_value() {
        let values = [Kleene::True, Kleene::False, STALE, MISS];
        for left in values {
            for right in values {
                let (a, b) = (left.and(right), right.and(left));
                assert_eq!(a.is_known(), b.is_known());
                if a.is_known() {
                    assert_eq!(a, b, "∧ commutes on decided values");
                }
                let (a, b) = (left.or(right), right.or(left));
                assert_eq!(a.is_known(), b.is_known());
                if a.is_known() {
                    assert_eq!(a, b, "∨ commutes on decided values");
                }
            }
        }
    }

    #[test]
    fn de_morgan_holds_across_all_three_values() {
        let values = [Kleene::True, Kleene::False, STALE];
        for left in values {
            for right in values {
                assert_eq!(!(left.and(right)), (!left).or(!right), "¬(p ∧ q) = ¬p ∨ ¬q");
                assert_eq!(!(left.or(right)), (!left).and(!right), "¬(p ∨ q) = ¬p ∧ ¬q");
            }
        }
    }

    #[test]
    fn the_excluded_middle_does_not_hold_and_that_is_the_point() {
        // `p ∨ ¬p` is TRUE in two-valued logic. Here it is ⊥, which is exactly
        // why an atom reading an unresolvable fact takes `on_inconclusive`
        // instead of quietly firing.
        assert_eq!(STALE.or(!STALE), STALE);
        assert_eq!(STALE.and(!STALE), STALE);
    }

    #[test]
    fn the_folds_carry_the_identities() {
        assert_eq!(Kleene::all(&[]), Kleene::True, "empty ∧ is the identity");
        assert_eq!(Kleene::any(&[]), Kleene::False, "empty ∨ is the identity");
        assert_eq!(Kleene::all(&[Kleene::True, Kleene::True]), Kleene::True);
        assert_eq!(Kleene::any(&[Kleene::False, Kleene::False]), Kleene::False);
    }

    #[test]
    fn a_conjunction_does_not_short_circuit_past_a_later_bottom() {
        // The corpus row `kleene-no-short-circuit-still-reports-the-bottom`:
        // the VERDICT is unchanged by the third child, and
        // `inconclusive_facts[]` is not. A fold that stopped at the first
        // `False` would answer the same and report less.
        let children = [Kleene::False, Kleene::True, STALE];
        assert_eq!(Kleene::all(&children), Kleene::False);
        assert!(
            children.iter().any(|child| !child.is_known()),
            "the caller can still see the ⊥ it must report — the slice is \
             already evaluated, which is what the signature is for"
        );
    }

    #[test]
    fn a_disjunction_does_not_short_circuit_past_a_later_bottom() {
        let children = [Kleene::True, MISS];
        assert_eq!(Kleene::any(&children), Kleene::True);
        assert!(children.iter().any(|child| !child.is_known()));
    }

    #[test]
    fn the_first_bottom_in_a_fold_owns_the_reason() {
        assert_eq!(Kleene::all(&[STALE, MISS]), STALE);
        assert_eq!(Kleene::all(&[MISS, STALE]), MISS);
        assert_eq!(Kleene::any(&[STALE, MISS]), STALE);
        assert_eq!(Kleene::any(&[MISS, STALE]), MISS);
    }

    #[test]
    fn only_an_unresolved_fact_belongs_in_inconclusive_facts() {
        assert!(Inconclusive::Absent.names_a_fact());
        assert!(Inconclusive::Stale.names_a_fact());
        assert!(
            !Inconclusive::OpenWorldMiss.names_a_fact(),
            "the fact resolved and was read — what is unknown is whether a \
             candidate is in a set that never claimed to be exhaustive"
        );
    }

    #[test]
    fn reason_hands_back_why_and_never_a_verdict() {
        assert_eq!(Kleene::True.reason(), None);
        assert_eq!(Kleene::False.reason(), None);
        assert_eq!(STALE.reason(), Some(Inconclusive::Stale));
        assert_eq!(MISS.reason(), Some(Inconclusive::OpenWorldMiss));
    }

    #[test]
    fn from_bool_and_is_known_agree() {
        assert_eq!(Kleene::from_bool(true), Kleene::True);
        assert_eq!(Kleene::from_bool(false), Kleene::False);
        assert!(Kleene::True.is_known());
        assert!(Kleene::False.is_known());
        assert!(!Kleene::UNKNOWN.is_known());
        assert!(!MISS.is_known());
    }

    /// D12, as a test rather than a comment: this module offers no way to turn a
    /// ⊥ into a boolean without the caller saying what it means.
    #[test]
    fn no_code_path_in_this_module_yields_a_truth_value_default() {
        // The SHIPPED half only: everything from `#[cfg(test)]` on is this
        // module's own tests, and the forbidden strings are spelled out below.
        let source = include_str!("kleene.rs");
        let shipped = source
            .split_once("#[cfg(test)]")
            .map_or(source, |(before, _)| before);
        let code: String = shipped
            .lines()
            .filter(|line| !line.trim_start().starts_with("//"))
            .collect::<Vec<_>>()
            .join("\n");
        for forbidden in [
            "unwrap_or(false)",
            "unwrap_or(true)",
            "unwrap_or_default()",
            "unwrap_or(Kleene",
            "unwrap_or_else",
            "impl Default for Kleene",
            "derive(Default)",
            "for bool",
        ] {
            assert!(
                !code.contains(forbidden),
                "`{forbidden}` expresses a fact-level default, which D12 says \
                 must be impossible to write here"
            );
        }
    }
}