K4 Belnap Four-Valued Logic
Audience: policy authors, platform engineers, and reviewers who need to understand how Stella Ops reconciles conflicting and missing evidence when it scores a vulnerability. Scope: the conceptual model and worked examples. The authoritative implementation (truth tables, enum members) lives in
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/K4Lattice.cs— see Application in Policy Engine and Implementation.
Overview
Stella Ops uses K4 Belnap four-valued logic to handle uncertainty and conflicting evidence in policy decisions. Classical true/false logic cannot express the two situations that dominate real vulnerability triage: when independent sources disagree, and when no source has spoken yet. K4 adds two values for exactly these cases — Both (conflict: the evidence says true and false) and Neither (unknown: no evidence either way) — so the platform can preserve conflicting evidence for human review instead of silently collapsing it (the aggregation-not-merge principle).
Why Four Values?
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ THE PROBLEM WITH BINARY LOGIC │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ In classical two-valued logic (True/False): │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ Scenario: Is this vulnerability reachable? │ │
│ │ │ │
│ │ Evidence sources: │ │
│ │ • Static analysis: "Yes, I found a path" → True │ │
│ │ • Runtime observation: "No activity seen" → ??? (not False) │ │
│ │ • VEX statement: "Not affected in our configuration" → False │ │
│ │ │ │
│ │ Problem: How do we combine True + False? │ │
│ │ • AND(True, False) = False (lose the static evidence) │ │
│ │ • OR(True, False) = True (lose the VEX evidence) │ │
│ │ │ │
│ │ Neither preserves the fact that we have CONFLICTING evidence! │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ Another scenario: No evidence available │ │
│ │ │ │
│ │ • No static analysis run → ??? │ │
│ │ • No runtime observation → ??? │ │
│ │ • No VEX statement → ??? │ │
│ │ │ │
│ │ Problem: This isn't "False" - we just don't know yet! │ │
│ │ Classical logic forces us to pick True or False when we have no information.│ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
The Four Values
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ K4 BELNAP TRUTH VALUES │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ THE BILATTICE │ │
│ │ │ │
│ │ ┌───────────┐ │ │
│ │ │ ⊤ │ BOTH (Conflict) │ │
│ │ │ "Both" │ Evidence says BOTH true AND false │ │
│ │ │ │ (conflicting sources) │ │
│ │ └─────┬─────┘ │ │
│ │ │ │ │
│ │ ╱─────┴─────╲ │ │
│ │ ╱ ╲ │ │
│ │ ╱ ╲ │ │
│ │ ┌───────┴───────┐ ┌───────┴───────┐ │ │
│ │ │ T │ │ F │ │ │
│ │ │ "True" │ │ "False" │ │ │
│ │ │ │ │ │ │ │
│ │ │ Evidence │ │ Evidence │ │ │
│ │ │ supports │ │ supports │ │ │
│ │ │ "yes" │ │ "no" │ │ │
│ │ └───────┬───────┘ └───────┬───────┘ │ │
│ │ ╲ ╱ │ │
│ │ ╲ ╱ │ │
│ │ ╲─────┬─────╱ │ │
│ │ │ │ │
│ │ ┌─────┴─────┐ │ │
│ │ │ ⊥ │ NEITHER (Unknown) │ │
│ │ │ "Neither" │ No evidence either way │ │
│ │ │ │ (insufficient data) │ │
│ │ └───────────┘ │ │
│ │ │ │
│ │ │ │
│ │ Two orderings (dimensions): │ │
│ │ │ │
│ │ TRUTH ordering (vertical): INFORMATION ordering (horizontal): │ │
│ │ F < ⊥ < T < ⊤ (for meet) ⊥ < T, ⊥ < F, T < ⊤, F < ⊤ (for join) │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
Value Semantics
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ VALUE SEMANTICS │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ │ │
│ │ Value │ Symbol │ Meaning │ Example in StellaOps │ │
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
│ │ True │ T │ Evidence supports "yes" │ Static analysis found │ │
│ │ │ │ │ reachable path │ │
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
│ │ False │ F │ Evidence supports "no" │ VEX says "not affected" │ │
│ │ │ │ │ │ │
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
│ │ Both │ ⊤ │ Evidence supports BOTH │ Static says reachable, │ │
│ │ │ │ "yes" AND "no" │ VEX says not affected │ │
│ │ │ │ (contradiction/conflict) │ │ │
│ │ ──────┼────────┼──────────────────────────────┼────────────────────────────│ │
│ │ Neither│ ⊥ │ No evidence either way │ No analysis run yet, │ │
│ │ │ │ (unknown/insufficient data) │ no VEX available │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ INFORMATION CONTENT │ │
│ │ │ │
│ │ ⊥ (Neither): 0 bits - we know nothing │ │
│ │ T (True): 1 bit - we know "yes" │ │
│ │ F (False): 1 bit - we know "no" │ │
│ │ ⊤ (Both): 2 bits - we know "yes" AND "no" (conflicting sources) │ │
│ │ │ │
│ │ The JOIN operation adds information (moves up in the lattice) │ │
│ │ The MEET operation requires agreement (moves down in the lattice) │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
Lattice Operations
JOIN (∨) - Combining Evidence
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ JOIN OPERATION (∨) │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ JOIN combines evidence from multiple sources. │
│ It prefers "more information" - moves UP the information ordering. │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ JOIN TRUTH TABLE │ │
│ │ │ │
│ │ ┌─────────┬─────────┬─────────┬─────────┬─────────┐ │ │
│ │ │ ∨ │ ⊥ │ T │ F │ ⊤ │ │ │
│ │ ├─────────┼─────────┼─────────┼─────────┼─────────┤ │ │
│ │ │ ⊥ │ ⊥ │ T │ F │ ⊤ │ │ │
│ │ │ T │ T │ T │ ⊤ │ ⊤ │ │ │
│ │ │ F │ F │ ⊤ │ F │ ⊤ │ │ │
│ │ │ ⊤ │ ⊤ │ ⊤ │ ⊤ │ ⊤ │ │ │
│ │ └─────────┴─────────┴─────────┴─────────┴─────────┘ │ │
│ │ │ │
│ │ Key insight: T ∨ F = ⊤ (both) │ │
│ │ When evidence conflicts, we get "Both" - we don't lose either source! │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ EXAMPLES │ │
│ │ │ │
│ │ Example 1: Adding static analysis to unknown │ │
│ │ ───────────────────────────────────────── │ │
│ │ Before: ⊥ (no information) │ │
│ │ Static analysis: T (found reachable path) │ │
│ │ Result: ⊥ ∨ T = T │ │
│ │ │ │
│ │ Example 2: Static says yes, VEX says no │ │
│ │ ──────────────────────────────────────── │ │
│ │ Static analysis: T │ │
│ │ VEX statement: F (not affected) │ │
│ │ Result: T ∨ F = ⊤ (conflict!) │ │
│ │ │ │
│ │ Example 3: Multiple sources agree │ │
│ │ ────────────────────────────────── │ │
│ │ Static analysis: T │ │
│ │ Runtime observation: T │ │
│ │ Result: T ∨ T = T │ │
│ │ │ │
│ │ Example 4: Adding information to conflict │ │
│ │ ────────────────────────────────────────── │ │
│ │ Current: ⊤ (conflicting evidence) │ │
│ │ New source: T (yes, reachable) │ │
│ │ Result: ⊤ ∨ T = ⊤ (still conflicting) │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
MEET (∧) - Requiring Agreement
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ MEET OPERATION (∧) │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ MEET requires agreement between sources. │
│ It prefers "less information" - moves DOWN the information ordering. │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ MEET TRUTH TABLE │ │
│ │ │ │
│ │ ┌─────────┬─────────┬─────────┬─────────┬─────────┐ │ │
│ │ │ ∧ │ ⊥ │ T │ F │ ⊤ │ │ │
│ │ ├─────────┼─────────┼─────────┼─────────┼─────────┤ │ │
│ │ │ ⊥ │ ⊥ │ ⊥ │ ⊥ │ ⊥ │ │ │
│ │ │ T │ ⊥ │ T │ ⊥ │ T │ │ │
│ │ │ F │ ⊥ │ ⊥ │ F │ F │ │ │
│ │ │ ⊤ │ ⊥ │ T │ F │ ⊤ │ │ │
│ │ └─────────┴─────────┴─────────┴─────────┴─────────┘ │ │
│ │ │ │
│ │ Key insight: T ∧ F = ⊥ (unknown) │ │
│ │ When evidence disagrees, we have no consensus - result is unknown │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ EXAMPLES │ │
│ │ │ │
│ │ Example 1: Requiring both sources to confirm │ │
│ │ ───────────────────────────────────────────── │ │
│ │ Source A: T (reachable) │ │
│ │ Source B: T (reachable) │ │
│ │ Result: T ∧ T = T (confirmed by both) │ │
│ │ │ │
│ │ Example 2: One confirms, one unknown │ │
│ │ ──────────────────────────────────────── │ │
│ │ Source A: T (reachable) │ │
│ │ Source B: ⊥ (no data) │ │
│ │ Result: T ∧ ⊥ = ⊥ (can't confirm without both) │ │
│ │ │ │
│ │ Example 3: Sources disagree │ │
│ │ ───────────────────────────── │ │
│ │ Source A: T (yes) │ │
│ │ Source B: F (no) │ │
│ │ Result: T ∧ F = ⊥ (no consensus possible) │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
NEGATION (¬)
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ NEGATION OPERATION (¬) │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ Negation flips T↔F but preserves ⊤ and ⊥ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ NEGATION TABLE │ │
│ │ │ │
│ │ ┌─────────┬─────────┐ │ │
│ │ │ x │ ¬x │ │ │
│ │ ├─────────┼─────────┤ │ │
│ │ │ ⊥ │ ⊥ │ (unknown stays unknown) │ │
│ │ │ T │ F │ (true becomes false) │ │
│ │ │ F │ T │ (false becomes true) │ │
│ │ │ ⊤ │ ⊤ │ (both stays both) │ │
│ │ └─────────┴─────────┘ │ │
│ │ │ │
│ │ Key insight: ¬⊤ = ⊤ │ │
│ │ Conflict cannot be resolved by negation - "both yes and no" negated │ │
│ │ is still "both no and yes" │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
Application in Policy Engine
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ K4 IN POLICY EVALUATION │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ EVIDENCE AGGREGATION FLOW │ │
│ │ │ │
│ │ Question: "Is CVE-2021-23337 exploitable in this image?" │ │
│ │ │ │
│ │ ┌─────────────────────────────────────────────────────────────────────┐ │ │
│ │ │ Source │ Finding │ K4 Value │ │ │
│ │ │ ─────────────────────┼───────────────────┼────────────────────────│ │ │
│ │ │ Static analysis │ Path found │ T (True) │ │ │
│ │ │ Runtime observation │ Not observed │ ⊥ (Unknown) │ │ │
│ │ │ VEX (RedHat) │ Not affected │ F (False) │ │ │
│ │ │ VEX (Ubuntu) │ Not affected │ F (False) │ │ │
│ │ └─────────────────────────────────────────────────────────────────────┘ │ │
│ │ │ │
│ │ Aggregation using JOIN: │ │
│ │ │ │
│ │ Step 1: T ∨ ⊥ = T (static + runtime) │ │
│ │ Step 2: T ∨ F = ⊤ (add VEX RedHat → conflict!) │ │
│ │ Step 3: ⊤ ∨ F = ⊤ (add VEX Ubuntu → still conflict) │ │
│ │ │ │
│ │ Final K4 Value: ⊤ (Both/Conflict) │ │
│ │ │ │
│ │ Interpretation: We have conflicting evidence. Static analysis found │ │
│ │ a path, but vendors say it's not affected. This needs human review. │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ VERDICT MAPPING │ │
│ │ │ │
│ │ K4 Value │ Verdict │ Action │ │
│ │ ─────────┼──────────┼──────────────────────────────────────────────────────│ │
│ │ T (True) │ FAIL │ Evidence supports vulnerability is exploitable │ │
│ │ F (False)│ PASS │ Evidence supports vulnerability is not exploitable │ │
│ │ ⊥ (Unknown)│ WARN │ Insufficient data - conservative warning │ │
│ │ ⊤ (Both) │ REVIEW │ Conflicting evidence - requires human decision │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
Conceptual mapping.
PASS / WARN / FAIL / REVIEWabove are simplified labels for explanation. The live verdict enum is richer —PolicyVerdictStatusinsrc/Policy/__Libraries/StellaOps.Policy/PolicyVerdict.csdefinesPass, GuardedPass, Blocked, Ignored, Warned, Deferred, Escalated, RequiresVex. Use the source enum for exact verdict names, and see the Policy Engine Data Pipeline for how K4 values, EWS scoring, and gates combine into a verdict.
Policy Rule Evaluation
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ POLICY RULE EVALUATION │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ RULE STRUCTURE │ │
│ │ │ │
│ │ Policy rules are predicates that evaluate to K4 values: │ │
│ │ │ │
│ │ rule no_critical_reachable: │ │
│ │ condition: severity == CRITICAL AND reachable == TRUE │ │
│ │ action: FAIL │ │
│ │ │ │
│ │ The "AND" uses K4 meet (∧): │ │
│ │ │ │
│ │ ┌────────────────────────────────────────────────────────────────────┐ │ │
│ │ │ severity == CRITICAL │ │ │
│ │ │ │ │ │
│ │ │ If CVSS >= 9.0 → T │ │ │
│ │ │ If CVSS < 9.0 → F │ │ │
│ │ │ If CVSS unknown → ⊥ │ │ │
│ │ └────────────────────────────────────────────────────────────────────┘ │ │
│ │ │ │
│ │ ┌────────────────────────────────────────────────────────────────────┐ │ │
│ │ │ reachable == TRUE │ │ │
│ │ │ │ │ │
│ │ │ From K4 reachability evidence (as shown above) │ │ │
│ │ └────────────────────────────────────────────────────────────────────┘ │ │
│ │ │ │
│ │ Combined: severity_k4 ∧ reachable_k4 │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ EVALUATION EXAMPLES │ │
│ │ │ │
│ │ Example 1: Critical + definitely reachable │ │
│ │ ───────────────────────────────────────── │ │
│ │ severity: T (CVSS 9.8) │ │
│ │ reachable: T (static + runtime confirmed) │ │
│ │ Result: T ∧ T = T → FAIL │ │
│ │ │ │
│ │ Example 2: Critical + not reachable │ │
│ │ ──────────────────────────────────── │ │
│ │ severity: T (CVSS 9.8) │ │
│ │ reachable: F (static analysis proves no path) │ │
│ │ Result: T ∧ F = ⊥ → WARN (can't prove both conditions) │ │
│ │ │ │
│ │ Example 3: Critical + unknown reachability │ │
│ │ ─────────────────────────────────────────── │ │
│ │ severity: T (CVSS 9.8) │ │
│ │ reachable: ⊥ (no analysis done) │ │
│ │ Result: T ∧ ⊥ = ⊥ → WARN (missing reachability data) │ │
│ │ │ │
│ │ Example 4: Critical + conflicting reachability │ │
│ │ ─────────────────────────────────────────────── │ │
│ │ severity: T (CVSS 9.8) │ │
│ │ reachable: ⊤ (static says yes, VEX says no) │ │
│ │ Result: T ∧ ⊤ = T → REVIEW (conflict in reachability) │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
Conflict Resolution
┌─────────────────────────────────────────────────────────────────────────────────────┐
│ CONFLICT RESOLUTION │
├─────────────────────────────────────────────────────────────────────────────────────┤
│ │
│ When K4 evaluation results in ⊤ (Both/Conflict): │
│ │
│ ┌──────────────────────────────────────────────────────────────────────────────┐ │
│ │ RESOLUTION STRATEGIES │ │
│ │ │ │
│ │ 1. TRUST WEIGHTING │ │
│ │ ─────────────────── │ │
│ │ Weight sources by trust level and use weighted voting: │ │
│ │ │ │
│ │ Sources claiming T: │ │
│ │ • Static analysis (trust: 0.7) │ │
│ │ Total T weight: 0.7 │ │
│ │ │ │
│ │ Sources claiming F: │ │
│ │ • VEX RedHat (trust: 1.0) │ │
│ │ • VEX Ubuntu (trust: 1.0) │ │
│ │ Total F weight: 2.0 │ │
│ │ │ │
│ │ Resolution: F wins (2.0 > 0.7) → PASS with note │ │
│ │ │ │
│ │ 2. RECENCY PREFERENCE │ │
│ │ ───────────────────── │ │
│ │ Prefer more recent evidence: │ │
│ │ │ │
│ │ • Static analysis: 2024-12-01 → T │ │
│ │ • VEX RedHat: 2024-12-28 → F │ │
│ │ │ │
│ │ Resolution: F wins (more recent) → PASS │ │
│ │ │ │
│ │ 3. CONSERVATIVE DEFAULT │ │
│ │ ───────────────────────── │ │
│ │ When conflict cannot be resolved, default to safer option: │ │
│ │ │ │
│ │ • Conflict in reachability → assume reachable (T) │ │
│ │ • Conflict in exploitability → assume exploitable (T) │ │
│ │ │ │
│ │ 4. HUMAN ESCALATION │ │
│ │ ──────────────────── │ │
│ │ Flag for human review with all evidence: │ │
│ │ │ │
│ │ { │ │
│ │ "verdict": "REVIEW", │ │
│ │ "reason": "conflicting_evidence", │ │
│ │ "evidence": { │ │
│ │ "supporting_true": ["static_analysis"], │ │
│ │ "supporting_false": ["vex_redhat", "vex_ubuntu"] │ │
│ │ } │ │
│ │ } │ │
│ │ │ │
│ └──────────────────────────────────────────────────────────────────────────────┘ │
│ │
└─────────────────────────────────────────────────────────────────────────────────────┘
Implementation
Illustrative. The snippet below conveys the algebra; it is not a verbatim copy of source. The canonical implementation is
src/Policy/__Libraries/StellaOps.Policy/TrustLattice/K4Lattice.cs, where the enum members areUnknown(⊥),True,False, andConflict(⊤), andJoin/Meet/Negateuse explicit branching. Read that file for exact member names and the determinization variant (src/Policy/__Libraries/StellaOps.Policy.Determinization/Scoring/K4Lattice.cs).
// K4 value enumeration (illustrative names; source uses Unknown/Conflict)
public enum K4Value
{
Neither = 0, // ⊥ - Unknown
True = 1, // T
False = 2, // F
Both = 3 // ⊤ - Conflict
}
// K4 lattice operations
public static class K4Lattice
{
// JOIN (∨) - combines evidence
public static K4Value Join(K4Value a, K4Value b)
{
return (K4Value)((int)a | (int)b);
}
// MEET (∧) - requires agreement
public static K4Value Meet(K4Value a, K4Value b)
{
// Special handling for the bilattice structure
if (a == K4Value.Neither || b == K4Value.Neither)
return K4Value.Neither;
if (a == b)
return a;
if (a == K4Value.Both)
return b;
if (b == K4Value.Both)
return a;
// T meet F = Neither (no consensus)
return K4Value.Neither;
}
// Negation
public static K4Value Negate(K4Value x)
{
return x switch
{
K4Value.True => K4Value.False,
K4Value.False => K4Value.True,
_ => x // Neither and Both are self-dual
};
}
// Information ordering
public static bool LessOrEqualInfo(K4Value a, K4Value b)
{
// ⊥ ≤ T, ⊥ ≤ F, T ≤ ⊤, F ≤ ⊤
if (a == K4Value.Neither) return true;
if (b == K4Value.Both) return true;
return a == b;
}
}
// Evidence aggregation
public class EvidenceAggregator
{
public K4Value AggregateEvidence(IEnumerable<EvidenceSource> sources)
{
K4Value result = K4Value.Neither; // Start with no information
foreach (var source in sources)
{
K4Value sourceValue = EvaluateSource(source);
result = K4Lattice.Join(result, sourceValue);
}
return result;
}
private K4Value EvaluateSource(EvidenceSource source)
{
return source.Type switch
{
"static_reachable" => source.Finding ? K4Value.True : K4Value.False,
"runtime_observed" => source.Finding ? K4Value.True : K4Value.Neither,
"vex_not_affected" => K4Value.False,
"vex_affected" => K4Value.True,
_ => K4Value.Neither
};
}
}
Related Documentation
- Policy Engine Data Pipeline — how K4 values, EWS scoring, and gates produce a verdict.
- Policy Architecture — Policy module dossier (authoritative contracts).
- Call Graph Analysis — the 8-state reachability lattice that feeds the K4 reachability value.
- Policy Evaluation Flow — end-to-end evaluation sequence.
- Confidence Scoring — archived; superseded by the evidence-weighted scoring (EWS) model in the data-pipeline doc.