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

lean_ctx_protocol/hive/
facts.rs
