lean_ctx_protocol/hive/
facts.rs

1// SPDX-License-Identifier: Apache-2.0
2
3//! Fact states (C0 1.9, section 3).
4//!
5//! A fact is `current` until an engine finds a reason to doubt it: one of its
6//! anchors no longer matches the code (`anchor_changed`), the symbol moved
7//! to another path (`anchor_moved`), the anchored path or symbol is gone
8//! (`anchor_missing`), or another fact contradicts it (`contradiction`).
9//! The engine reports states with
10//! `POST /v1/vaults/{vault_id}/facts/states` ([`FactStateReportV1`],
11//! right `knowledge.read`); Hive answers [`FactStateAckV1`] and lists the
12//! non-current states with the revision ([`KnowledgeRevisionV1::fact_states`]).
13//! A report replaces the reporting engine's earlier states for that
14//! revision; a fact is `current` again when no engine reports it.
15//!
16//! A state never changes the document. Fixing a fact is a proposal; a
17//! `contradiction` with no proposal after 24 hours becomes a task (origin
18//! `contradiction`).
19//!
20//! [`KnowledgeRevisionV1::fact_states`]: super::knowledge::KnowledgeRevisionV1::fact_states
21
22use serde::{Deserialize, Serialize};
23
24use super::anchor::CodeAnchorV1;
25use super::knowledge::fact_id_ok;
26use super::require_schema;
27use crate::{UtcTimestamp, ValidationError};
28
29pub const FACT_STATE_REPORT_SCHEMA: &str = "leanctx.hive.fact-state-report/v1";
30pub const FACT_STATE_ACK_SCHEMA: &str = "leanctx.hive.fact-state-ack/v1";
31/// Facts per report (a document holds at most `MAX_FACTS`).
32pub const MAX_FACT_STATES: usize = super::knowledge::MAX_FACTS;
33pub const MAX_STATE_REASONS: usize = 4;
34pub const MAX_CONTRADICTED_BY: usize = 16;
35
36#[derive(Debug, Clone, Copy, PartialEq, Eq, Hash, Serialize, Deserialize)]
37#[serde(rename_all = "snake_case")]
38pub enum FactStateKind {
39    Current,
40    ToVerify,
41    Contradicted,
42    #[serde(other)]
43    Unknown,
44}
45
46#[derive(Debug, Clone, Copy, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)]
47#[serde(rename_all = "snake_case")]
48pub enum FactStateReason {
49    AnchorChanged,
50    AnchorMoved,
51    AnchorMissing,
52    Contradiction,
53    #[serde(other)]
54    Unknown,
55}
56
57/// The state of one fact, as an engine reports it.
58#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
59#[serde(deny_unknown_fields)]
60pub struct FactStateV1 {
61    pub fact: String,
62    /// `to_verify` or `contradicted`; a report never sends `current`.
63    pub state: FactStateKind,
64    /// Sorted, without repeats.
65    pub reasons: Vec<FactStateReason>,
66    /// With `anchor_moved`: where the symbol is now.
67    #[serde(default, skip_serializing_if = "Option::is_none")]
68    pub moved_to: Option<CodeAnchorV1>,
69    /// With `contradiction`: the facts that contradict this one.
70    #[serde(default, skip_serializing_if = "Vec::is_empty")]
71    pub contradicted_by: Vec<String>,
72    pub since: UtcTimestamp,
73}
74
75impl FactStateV1 {
76    pub fn validate(&self) -> Result<(), ValidationError> {
77        if !fact_id_ok(&self.fact) {
78            return Err(ValidationError::new("fact id is malformed"));
79        }
80        if self.reasons.is_empty()
81            || self.reasons.len() > MAX_STATE_REASONS
82            || self.reasons.windows(2).any(|pair| pair[0] >= pair[1])
83            || self.reasons.contains(&FactStateReason::Unknown)
84        {
85            return Err(ValidationError::new(
86                "reasons are 1-4 known reasons, sorted without repeats",
87            ));
88        }
89        let contradiction = self.reasons.contains(&FactStateReason::Contradiction);
90        match self.state {
91            FactStateKind::Contradicted if !contradiction => {
92                return Err(ValidationError::new(
93                    "a contradicted fact has the reason contradiction",
94                ));
95            }
96            FactStateKind::ToVerify if contradiction => {
97                return Err(ValidationError::new(
98                    "a contradiction makes the fact contradicted",
99                ));
100            }
101            FactStateKind::Current | FactStateKind::Unknown => {
102                return Err(ValidationError::new(
103                    "a report carries to_verify or contradicted",
104                ));
105            }
106            _ => {}
107        }
108        match (
109            self.reasons.contains(&FactStateReason::AnchorMoved),
110            &self.moved_to,
111        ) {
112            (true, Some(anchor)) => anchor.validate()?,
113            (false, None) => {}
114            _ => {
115                return Err(ValidationError::new(
116                    "moved_to comes exactly with anchor_moved",
117                ));
118            }
119        }
120        if contradiction == self.contradicted_by.is_empty()
121            || self.contradicted_by.len() > MAX_CONTRADICTED_BY
122            || self
123                .contradicted_by
124                .iter()
125                .any(|id| !fact_id_ok(id) || id == &self.fact)
126            || self
127                .contradicted_by
128                .windows(2)
129                .any(|pair| pair[0] >= pair[1])
130        {
131            return Err(ValidationError::new(
132                "contradicted_by lists 1-16 other facts, sorted, exactly with contradiction",
133            ));
134        }
135        Ok(())
136    }
137}
138
139/// `POST /v1/vaults/{vault_id}/facts/states`.
140#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
141#[serde(deny_unknown_fields)]
142pub struct FactStateReportV1 {
143    pub schema: String,
144    /// The released revision the engine checked.
145    pub revision: u64,
146    /// The facts in doubt, sorted by fact; empty: nothing in doubt.
147    pub states: Vec<FactStateV1>,
148}
149
150impl FactStateReportV1 {
151    pub fn validate(&self) -> Result<(), ValidationError> {
152        require_schema(&self.schema, FACT_STATE_REPORT_SCHEMA)?;
153        if self.revision == 0 {
154            return Err(ValidationError::new("revision 0 has no facts"));
155        }
156        if self.states.len() > MAX_FACT_STATES {
157            return Err(ValidationError::new(format!(
158                "at most {MAX_FACT_STATES} states"
159            )));
160        }
161        for (i, state) in self.states.iter().enumerate() {
162            state.validate()?;
163            if i > 0 && self.states[i - 1].fact >= state.fact {
164                return Err(ValidationError::new(
165                    "states must be sorted by fact without repeats",
166                ));
167            }
168        }
169        Ok(())
170    }
171}
172
173#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)]
174pub struct FactStateAckV1 {
175    pub schema: String,
176    pub revision: u64,
177    /// Facts not `current` across all engines' reports for that revision.
178    pub to_verify: u64,
179    pub contradicted: u64,
180}
181
182#[cfg(test)]
183mod tests {
184    use super::*;
185
186    fn state(reasons: Vec<FactStateReason>, kind: FactStateKind) -> FactStateV1 {
187        FactStateV1 {
188            fact: "retry.budget".into(),
189            state: kind,
190            reasons,
191            moved_to: None,
192            contradicted_by: Vec::new(),
193            since: "2026-10-22T08:00:00Z".parse().expect("time"),
194        }
195    }
196
197    #[test]
198    fn states_follow_their_reasons() {
199        assert!(
200            state(
201                vec![FactStateReason::AnchorChanged],
202                FactStateKind::ToVerify
203            )
204            .validate()
205            .is_ok()
206        );
207        let mut contradicted = state(
208            vec![FactStateReason::Contradiction],
209            FactStateKind::Contradicted,
210        );
211        assert!(
212            contradicted.validate().is_err(),
213            "names no contradicting fact"
214        );
215        contradicted.contradicted_by = vec!["retry.limit".into()];
216        assert!(contradicted.validate().is_ok());
217        assert!(
218            state(
219                vec![FactStateReason::Contradiction],
220                FactStateKind::ToVerify
221            )
222            .validate()
223            .is_err()
224        );
225        assert!(
226            state(vec![FactStateReason::AnchorMoved], FactStateKind::ToVerify)
227                .validate()
228                .is_err(),
229            "anchor_moved needs moved_to"
230        );
231        assert!(
232            state(vec![FactStateReason::AnchorChanged], FactStateKind::Current)
233                .validate()
234                .is_err()
235        );
236    }
237}
lean_ctx_protocol/hive/facts.rs

lean_ctx_protocol/hive/
facts.rs
