diff --git a/Cargo.lock b/Cargo.lock index 4dbd4e39..ac44028e 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8189,6 +8189,8 @@ name = "praxis-core" version = "0.3.0" dependencies = [ "aios-protocol", + "blake3", + "chrono", "serde", "serde_json", "tempfile", @@ -8239,6 +8241,7 @@ dependencies = [ "arcan-sandbox", "async-trait", "blake3", + "chrono", "glob", "praxis-core", "regex", diff --git a/crates/praxis/CLAUDE.md b/crates/praxis/CLAUDE.md index 9bd19db5..acea3b2e 100644 --- a/crates/praxis/CLAUDE.md +++ b/crates/praxis/CLAUDE.md @@ -1,7 +1,7 @@ # Praxis — Canonical Tool Execution Engine -**Version**: 0.1.0 | **Date**: 2026-03-19 | **Status**: Active (Phase 4 — MCP server complete) -**Tests**: 90 passing | 4 crates | Rust 2024 Edition (MSRV 1.85) +**Version**: 0.1.0 | **Date**: 2026-07-17 | **Status**: Active (Phase 4 — MCP server complete) +**Tests**: 145 passing | 5 crates | Rust 2024 Edition (MSRV 1.85) Praxis is the canonical tool execution and sandbox engine for the Agent OS. It implements the `Tool` trait from `aios-protocol` and provides filesystem, editing, shell, memory, MCP server/client, and skill discovery tools. @@ -24,13 +24,17 @@ aios-protocol (Tool trait, ToolDefinition, ToolCall, ToolResult, ToolError) ## Crates -### praxis-core (12 tests) +### praxis-core (41 tests) - **SandboxPolicy**: cwd validation, env filtering, timeout enforcement, output truncation - **FsPolicy**: workspace boundary enforcement via canonicalize + starts_with - **CommandRunner**: trait + LocalCommandRunner implementation - **Error types**: PraxisError (thiserror) +- **belief** (BRO-1030): four-dimensional `BeliefWriteToken` types — `CapabilityId`, + `BeliefScope` + `ScopeQualifier` (Jaccard overlap), `BiTemporalStamp`, + `RevisionLink` + `BeliefRevisionAcknowledgment`, `ContentAddressedRef` (blake3), + `AnimaDid`, `BeliefClass`. Formation context as a typed, content-addressed write token. -### praxis-tools (24 tests) +### praxis-tools (54 tests) - **ReadFileTool**: reads files with hashline tags for content-addressed editing - **WriteFileTool**: writes files within workspace boundary - **ListDirTool**: lists directory contents with metadata @@ -39,6 +43,12 @@ aios-protocol (Tool trait, ToolDefinition, ToolCall, ToolResult, ToolError) - **EditFileTool**: hashline (Blake3) content-addressed line editing - **BashTool**: shell command execution within sandbox constraints - **ReadMemoryTool / WriteMemoryTool**: agent memory persistence (file-based markdown) +- **belief** (BRO-1030): `BeliefStore` + `write_belief` (six write-path checks, incl. + `MissingRevisionLink` on overlapping scope), `CapabilityGrant` registry, + `traverse_revisions` (revision-graph chain), `route_write` + `record_operational` + (normative/operational migration), `recent_supersessions` (Nous L2 read-model), + `revision_masks_contradiction` (bookkeeping contradiction gate). See + `docs/specs/bro-1030-belief-write-token.{md,html}`. ### praxis-skills (11 tests) - **SkillMetadata**: parsed from SKILL.md YAML frontmatter diff --git a/crates/praxis/praxis-core/Cargo.toml b/crates/praxis/praxis-core/Cargo.toml index f49ccec7..22b2a5fa 100644 --- a/crates/praxis/praxis-core/Cargo.toml +++ b/crates/praxis/praxis-core/Cargo.toml @@ -10,6 +10,8 @@ description = "Core sandbox policy, workspace enforcement, and command runner fo [dependencies] aios-protocol.workspace = true +blake3.workspace = true +chrono.workspace = true serde.workspace = true serde_json.workspace = true thiserror.workspace = true diff --git a/crates/praxis/praxis-core/src/belief.rs b/crates/praxis/praxis-core/src/belief.rs new file mode 100644 index 00000000..a2fa6e0c --- /dev/null +++ b/crates/praxis/praxis-core/src/belief.rs @@ -0,0 +1,788 @@ +//! # Belief formation context — the four-dimensional `BeliefWriteToken` +//! +//! A belief is not a bare proposition. Two agents can hold the *same* +//! proposition for entirely different reasons, at different times, about +//! different sub-domains, superseding different prior convictions. The +//! belief-contradiction problem (silent accumulation looking identical to +//! deliberate updating) is unsolvable without observing **how the belief was +//! formed**. This module makes formation context a first-class, typed write +//! token. +//! +//! ## The four dimensions +//! +//! | Dimension | Question answered | Field | +//! | -- | -- | -- | +//! | Capability | *Who authorized this belief?* | [`BeliefWriteToken::capability_id`] | +//! | Bi-temporal | *When in the world / when in the system?* | [`BeliefWriteToken::timestamp`] | +//! | Scope | *About what, precisely?* | [`BeliefWriteToken::scope`] + [`BeliefWriteToken::scope_qualifier`] | +//! | Revision | *What was superseded?* | [`BeliefWriteToken::revision_link`] | +//! +//! Without the fourth dimension — `revision_link` — even bi-temporal stamps +//! reduce to a *playback device*: two snapshots with timestamps but no causal +//! connection between them. A contradiction with a revision link is *visible +//! history* (a deliberate update); a contradiction *without* one is a genuine +//! failure of versioning. +//! +//! This crate owns the **types**. The write path, the belief store, the +//! revision-graph traversal, and the migration/routing logic live in +//! `praxis-tools` (`praxis_tools::belief`). + +use blake3::Hasher; +use chrono::{DateTime, Utc}; +use serde::{Deserialize, Serialize}; +use std::collections::{BTreeMap, BTreeSet}; +use std::fmt; + +// ── typed newtypes ─────────────────────────────────────────────────────── + +/// The capability grant that authorized a belief write. +/// +/// Answers khlo's question — *who authorized this belief?* A write with no +/// resolvable capability cannot be distinguished from silent accumulation, so +/// the write path rejects it. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +#[serde(transparent)] +pub struct CapabilityId(String); + +impl CapabilityId { + pub fn new(s: impl Into) -> Self { + Self(s.into()) + } + + pub fn as_str(&self) -> &str { + &self.0 + } + + /// A capability id is *present* when it is non-empty. + pub fn is_present(&self) -> bool { + !self.0.is_empty() + } +} + +impl fmt::Display for CapabilityId { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.0) + } +} + +impl From<&str> for CapabilityId { + fn from(s: &str) -> Self { + Self(s.to_owned()) + } +} + +/// The coarse domain a belief is about — e.g. `"self"`, `"market"`, `"user"`. +/// +/// A capability grant enumerates the scopes it authorizes; the write path +/// checks that the belief's scope is contained by the grant. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +#[serde(transparent)] +pub struct BeliefScope(String); + +impl BeliefScope { + pub fn new(s: impl Into) -> Self { + Self(s.into()) + } + + pub fn as_str(&self) -> &str { + &self.0 + } +} + +impl fmt::Display for BeliefScope { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.0) + } +} + +impl From<&str> for BeliefScope { + fn from(s: &str) -> Self { + Self(s.to_owned()) + } +} + +/// An agent's decentralised identifier (`did:key:z6Mk…`) — the principal that +/// signs the write. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +#[serde(transparent)] +pub struct AnimaDid(String); + +impl AnimaDid { + pub fn new(s: impl Into) -> Self { + Self(s.into()) + } + + pub fn as_str(&self) -> &str { + &self.0 + } +} + +impl fmt::Display for AnimaDid { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.0) + } +} + +impl From<&str> for AnimaDid { + fn from(s: &str) -> Self { + Self(s.to_owned()) + } +} + +// ── scope qualifier ────────────────────────────────────────────────────── + +/// A key within a [`ScopeQualifier`] — e.g. `"metric"`, `"regime"`, `"horizon"`. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +#[serde(transparent)] +pub struct QualifierKey(String); + +impl QualifierKey { + pub fn new(s: impl Into) -> Self { + Self(s.into()) + } + + pub fn as_str(&self) -> &str { + &self.0 + } +} + +impl From<&str> for QualifierKey { + fn from(s: &str) -> Self { + Self(s.to_owned()) + } +} + +/// A value within a [`ScopeQualifier`]. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +#[serde(transparent)] +pub struct QualifierValue(String); + +impl QualifierValue { + pub fn new(s: impl Into) -> Self { + Self(s.into()) + } + + pub fn as_str(&self) -> &str { + &self.0 + } +} + +impl From<&str> for QualifierValue { + fn from(s: &str) -> Self { + Self(s.to_owned()) + } +} + +/// Fine-grained scope conditions — Cornelius-Trinity's reframing that a belief +/// carries its *own* scope conditions ("reliable for X, unreliable for Y"). +/// +/// Two beliefs about the same coarse [`BeliefScope`] but disjoint qualifiers +/// are *parallel* beliefs, not contradictions. Overlap is measured with the +/// Jaccard index over the `(key, value)` pair set; the write path treats +/// overlap ≥ [`ScopeQualifier::OVERLAP_THRESHOLD`] as "the same belief slot", +/// requiring a revision link. +#[derive(Debug, Clone, Default, PartialEq, Eq, Serialize, Deserialize)] +pub struct ScopeQualifier { + /// Ordered map so the qualifier set has a canonical serialization + /// (required for stable content addressing). + pub qualifiers: BTreeMap, +} + +impl ScopeQualifier { + /// Jaccard overlap at or above this threshold ⇒ the two beliefs occupy the + /// same slot and a revision link is required (open question 2, PROVISIONAL). + pub const OVERLAP_THRESHOLD: f64 = 0.5; + + /// An empty qualifier — the belief makes no scope-narrowing claim. + pub fn empty() -> Self { + Self::default() + } + + /// Build from `(key, value)` string pairs. + pub fn from_pairs(pairs: impl IntoIterator) -> Self + where + K: Into, + V: Into, + { + Self { + qualifiers: pairs + .into_iter() + .map(|(k, v)| (QualifierKey::new(k), QualifierValue::new(v))) + .collect(), + } + } + + /// True when no qualifiers are set. + pub fn is_empty(&self) -> bool { + self.qualifiers.is_empty() + } + + fn pair_set(&self) -> BTreeSet<(&QualifierKey, &QualifierValue)> { + self.qualifiers.iter().collect() + } + + /// Jaccard index over the `(key, value)` pair sets, in `[0.0, 1.0]`. + /// + /// Two empty qualifiers overlap completely (`1.0`) — they name the same + /// unqualified slot. + pub fn jaccard(&self, other: &ScopeQualifier) -> f64 { + let a = self.pair_set(); + let b = other.pair_set(); + if a.is_empty() && b.is_empty() { + return 1.0; + } + let intersection = a.intersection(&b).count(); + let union = a.union(&b).count(); + if union == 0 { + 0.0 + } else { + intersection as f64 / union as f64 + } + } + + /// True when overlap is at or above [`Self::OVERLAP_THRESHOLD`] — the two + /// beliefs occupy the same slot, so a revision link is required to write + /// the second one. + pub fn overlaps(&self, other: &ScopeQualifier) -> bool { + self.jaccard(other) >= Self::OVERLAP_THRESHOLD + } +} + +// ── evidence + session context ─────────────────────────────────────────── + +/// A pointer to the evidence a belief cites. +/// +/// Kept structurally light: a `source` (where the evidence came from) plus an +/// optional `locator` (a URL, event id, line range…) and optional `digest` +/// (content hash of the cited artifact, for tamper evidence). +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct EvidenceRef { + /// Where the evidence came from — e.g. `"lago:event"`, `"observation"`, + /// `"user"`, `"tool:grep"`. + pub source: String, + /// Optional precise locator within the source. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub locator: Option, + /// Optional content digest of the cited artifact. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub digest: Option, +} + +impl EvidenceRef { + /// A minimal evidence reference carrying only a source label. + pub fn source(source: impl Into) -> Self { + Self { + source: source.into(), + locator: None, + digest: None, + } + } + + /// Attach a precise locator (URL, event id, line range). + pub fn with_locator(mut self, locator: impl Into) -> Self { + self.locator = Some(locator.into()); + self + } + + /// Attach a content digest of the cited artifact. + pub fn with_digest(mut self, digest: impl Into) -> Self { + self.digest = Some(digest.into()); + self + } +} + +/// The session in which a belief was formed — write-time provenance. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct SessionContext { + /// The session identifier. + pub session_id: String, + /// The run within the session, if known. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub run_id: Option, + /// The principal that formed the belief in this session. + pub principal: AnimaDid, + /// Optional free-form note about the formation context. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub summary: Option, +} + +impl SessionContext { + pub fn new(session_id: impl Into, principal: AnimaDid) -> Self { + Self { + session_id: session_id.into(), + run_id: None, + principal, + summary: None, + } + } + + pub fn with_run(mut self, run_id: impl Into) -> Self { + self.run_id = Some(run_id.into()); + self + } + + pub fn with_summary(mut self, summary: impl Into) -> Self { + self.summary = Some(summary.into()); + self + } +} + +// ── bi-temporal stamp ──────────────────────────────────────────────────── + +/// A bi-temporal stamp: *when in the world* the belief became valid +/// (`valid_from`) and *when in the system* it was recorded (`recorded_at`). +/// +/// Both fields are structurally required. The write path additionally checks +/// [`BiTemporalStamp::is_complete`] to reject sentinel/zero timestamps. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +pub struct BiTemporalStamp { + /// When the belief became true in the world being modelled. + pub valid_from: DateTime, + /// When the belief was written into the system. + pub recorded_at: DateTime, +} + +impl BiTemporalStamp { + pub fn new(valid_from: DateTime, recorded_at: DateTime) -> Self { + Self { + valid_from, + recorded_at, + } + } + + /// A stamp where the belief is valid from, and recorded at, the same + /// instant. + pub fn at(instant: DateTime) -> Self { + Self { + valid_from: instant, + recorded_at: instant, + } + } + + /// True when neither stamp was left at the zero/default (Unix epoch) + /// sentinel. + /// + /// `valid_from` is world time, so a belief about a pre-1970 fact is + /// legitimate: only the sentinel itself is rejected, not everything before + /// it. `recorded_at` is the system's own write time and cannot precede the + /// epoch, so it must be strictly after it. + pub fn is_complete(&self) -> bool { + let epoch = DateTime::::UNIX_EPOCH; + self.valid_from != epoch && self.recorded_at > epoch + } +} + +// ── content addressing ─────────────────────────────────────────────────── + +/// The bare claim a belief asserts — `subject` + `proposition`. +/// +/// Kept separate from the [`BeliefWriteToken`] envelope: the token carries +/// *authorization and provenance*, the claim carries *content*. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct BeliefClaim { + /// The entity or concept the belief is about (`"self"`, `"market"`, …). + pub subject: String, + /// The factual or evaluative proposition being asserted. + pub proposition: String, +} + +impl BeliefClaim { + pub fn new(subject: impl Into, proposition: impl Into) -> Self { + Self { + subject: subject.into(), + proposition: proposition.into(), + } + } +} + +/// A content-addressed reference to a prior belief — its content hash plus the +/// `valid_from` that disambiguates temporal versions of the same content. +/// +/// This is what a [`RevisionLink`] points *at*: the specific prior belief a new +/// write supersedes. +#[derive(Debug, Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Serialize, Deserialize)] +pub struct ContentAddressedRef { + /// Blake3 content hash of the superseded belief (hex). + pub content_hash: String, + /// The superseded belief's `valid_from`, disambiguating versions. + pub valid_from: DateTime, +} + +impl ContentAddressedRef { + pub fn new(content_hash: impl Into, valid_from: DateTime) -> Self { + Self { + content_hash: content_hash.into(), + valid_from, + } + } +} + +/// Length-prefix a variable-length field into the hasher: a domain tag, then +/// the field's byte length as u64 little-endian, then the field bytes. +/// +/// Length-prefixing (rather than delimiter framing) makes the encoding +/// unambiguous: no combination of field contents can be reinterpreted as a +/// different field boundary, because a byte inside a field can never be +/// mistaken for the length that precedes it. +fn hash_field(hasher: &mut Hasher, tag: &[u8], data: &[u8]) { + hasher.update(tag); + hasher.update(&(data.len() as u64).to_le_bytes()); + hasher.update(data); +} + +/// Compute the Blake3 content hash of a belief's *semantic identity*: +/// coarse scope, canonicalised qualifiers, subject, and proposition. +/// +/// Two writes with identical semantic identity hash to the same value +/// regardless of who wrote them or when — that is what makes supersession +/// referenceable. +/// +/// Every variable-length field is length-prefixed and the qualifier pair count +/// is written explicitly, so distinct inputs can never alias to the same hash: +/// e.g. the qualifier pairs `("a=b", "c")` and `("a", "b=c")` — which a naive +/// `key=value\0` concatenation would collide — produce distinct hashes here. +pub fn content_hash( + scope: &BeliefScope, + qualifier: &ScopeQualifier, + claim: &BeliefClaim, +) -> String { + let mut hasher = Hasher::new(); + hasher.update(b"praxis.belief.v1"); + hash_field(&mut hasher, b"scope", scope.as_str().as_bytes()); + // Explicit pair count, then each length-prefixed key/value. + // BTreeMap iterates in key order — canonical. + hasher.update(b"qualifiers"); + hasher.update(&(qualifier.qualifiers.len() as u64).to_le_bytes()); + for (k, v) in &qualifier.qualifiers { + hash_field(&mut hasher, b"qk", k.as_str().as_bytes()); + hash_field(&mut hasher, b"qv", v.as_str().as_bytes()); + } + hash_field(&mut hasher, b"subject", claim.subject.as_bytes()); + hash_field(&mut hasher, b"proposition", claim.proposition.as_bytes()); + hasher.finalize().to_hex().to_string() +} + +// ── revision link ──────────────────────────────────────────────────────── + +/// The structured trigger that prompted a revision. +/// +/// vina's framing: the past self is a series of discarded drafts. Naming *why* +/// a draft was discarded is what turns a contradiction into a lineage. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum RevisionTrigger { + /// New evidence arrived that the prior belief did not account for. + NewEvidence, + /// The scope was refined — the prior belief was over-broad. + ScopeRefinement, + /// The context shifted — the world changed under the prior belief. + ContextShift, +} + +impl RevisionTrigger { + /// The structured, query-stable label. + pub fn as_str(&self) -> &'static str { + match self { + RevisionTrigger::NewEvidence => "new evidence", + RevisionTrigger::ScopeRefinement => "scope refinement", + RevisionTrigger::ContextShift => "context shift", + } + } +} + +impl fmt::Display for RevisionTrigger { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.as_str()) + } +} + +/// The structured shape of the change a revision makes. +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum RevisionChange { + /// A polarity flip — `A` became `not-A`. + Negated, + /// A narrowing — `A` became `A` under an added qualifier. + Qualified, + /// A confidence change without a polarity flip. + Reweighted, +} + +impl RevisionChange { + /// The structured, query-stable label. + pub fn as_str(&self) -> &'static str { + match self { + RevisionChange::Negated => "from A to not-A", + RevisionChange::Qualified => "from A to A_qualified", + RevisionChange::Reweighted => "from A to A_reweighted", + } + } +} + +impl fmt::Display for RevisionChange { + fn fmt(&self, f: &mut fmt::Formatter<'_>) -> fmt::Result { + write!(f, "{}", self.as_str()) + } +} + +/// A belief-revision acknowledgment: structured fields for queryability plus a +/// free-form `rationale` addendum (open question 1, PROVISIONAL). +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct BeliefRevisionAcknowledgment { + /// Structured: what prompted the revision. + pub trigger: RevisionTrigger, + /// Structured: the shape of the change. + pub change: RevisionChange, + /// Free-form addendum explaining the revision in the agent's own words. + pub rationale: String, +} + +impl BeliefRevisionAcknowledgment { + pub fn new( + trigger: RevisionTrigger, + change: RevisionChange, + rationale: impl Into, + ) -> Self { + Self { + trigger, + change, + rationale: rationale.into(), + } + } +} + +/// The fourth dimension — what a belief supersedes. +/// +/// Without this, two contradictory beliefs are just two snapshots. With it, the +/// second belief *acknowledges* the first as its discarded draft: the +/// contradiction becomes visible history rather than a versioning failure. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct RevisionLink { + /// The prior belief this supersedes (content hash + `valid_from`). + pub superseded: ContentAddressedRef, + /// Which evidence triggered the revision. + pub triggered_by: Vec, + /// Structured + free-form acknowledgment of the change. + pub acknowledgment: BeliefRevisionAcknowledgment, +} + +impl RevisionLink { + pub fn new( + superseded: ContentAddressedRef, + triggered_by: Vec, + acknowledgment: BeliefRevisionAcknowledgment, + ) -> Self { + Self { + superseded, + triggered_by, + acknowledgment, + } + } +} + +// ── belief class ───────────────────────────────────────────────────────── + +/// The two belief classes with different survival criteria. +/// +/// | Class | Surface | All 4 dimensions required? | Survives on | +/// | -- | -- | -- | -- | +/// | Untested-normative | Praxis principal | **yes** | capability + scope + revision-link consistency | +/// | Tested-operational | Vigil (observed) | no | functional aliveness | +#[derive(Debug, Clone, Copy, PartialEq, Eq, Serialize, Deserialize)] +#[serde(rename_all = "snake_case")] +pub enum BeliefClass { + /// A normative belief written through the Praxis principal — must carry all + /// four formation dimensions. + UntestedNormative, + /// An operational belief observed by Vigil — survives on functional + /// aliveness, not on formation context. + TestedOperational, +} + +// ── the write token ────────────────────────────────────────────────────── + +/// The four-dimensional formation context accompanying a belief write. +/// +/// Field-for-field the spec of BRO-1030. The token is the *authorization and +/// provenance envelope*; the belief's [`BeliefClaim`] content is passed +/// alongside it to `praxis_tools::belief::write_belief`. +#[derive(Debug, Clone, PartialEq, Eq, Serialize, Deserialize)] +pub struct BeliefWriteToken { + /// **Who** authorized this belief. + pub capability_id: CapabilityId, + /// The coarse domain the belief is about. + pub scope: BeliefScope, + /// The fine-grained scope conditions. + pub scope_qualifier: ScopeQualifier, + /// The evidence the belief cites. + pub cited_evidence: Vec, + /// The session in which the belief was formed. + pub formation_context: SessionContext, + /// **What** this belief supersedes — the fourth dimension. `None` for a + /// first assertion in a slot. + #[serde(default, skip_serializing_if = "Option::is_none")] + pub revision_link: Option, + /// The principal that signs the write. + pub signed_by: AnimaDid, + /// **When** in the world / **when** in the system. + pub timestamp: BiTemporalStamp, +} + +impl BeliefWriteToken { + /// True when the token cites at least one piece of evidence. + pub fn has_evidence(&self) -> bool { + !self.cited_evidence.is_empty() + } + + /// Content hash of the belief this token describes, given its claim. + pub fn content_hash(&self, claim: &BeliefClaim) -> String { + content_hash(&self.scope, &self.scope_qualifier, claim) + } +} + +#[cfg(test)] +mod tests { + use super::*; + use chrono::TimeZone; + + fn ts(secs: i64) -> DateTime { + Utc.timestamp_opt(secs, 0).single().unwrap() + } + + #[test] + fn capability_presence() { + assert!(CapabilityId::new("cap-1").is_present()); + assert!(!CapabilityId::new("").is_present()); + } + + #[test] + fn jaccard_identical_qualifiers_is_one() { + let a = ScopeQualifier::from_pairs([("metric", "engagement"), ("regime", "bull")]); + let b = ScopeQualifier::from_pairs([("metric", "engagement"), ("regime", "bull")]); + assert_eq!(a.jaccard(&b), 1.0); + assert!(a.overlaps(&b)); + } + + #[test] + fn jaccard_disjoint_qualifiers_is_zero() { + let a = ScopeQualifier::from_pairs([("metric", "engagement")]); + let b = ScopeQualifier::from_pairs([("metric", "revenue")]); + assert_eq!(a.jaccard(&b), 0.0); + assert!(!a.overlaps(&b)); + } + + #[test] + fn jaccard_partial_overlap_at_threshold() { + // {A,B} vs {A,C}: intersection 1, union 3 => 1/3 < 0.5 => no overlap. + let a = ScopeQualifier::from_pairs([("k", "A"), ("k2", "B")]); + let b = ScopeQualifier::from_pairs([("k", "A"), ("k2", "C")]); + assert!((a.jaccard(&b) - 1.0 / 3.0).abs() < 1e-9); + assert!(!a.overlaps(&b)); + + // {A,B} vs {A,B,C}: intersection 2, union 3 => 2/3 >= 0.5 => overlap. + let c = ScopeQualifier::from_pairs([("k", "A"), ("k2", "B")]); + let d = ScopeQualifier::from_pairs([("k", "A"), ("k2", "B"), ("k3", "C")]); + assert!(c.overlaps(&d)); + } + + #[test] + fn empty_qualifiers_overlap_completely() { + let a = ScopeQualifier::empty(); + let b = ScopeQualifier::empty(); + assert_eq!(a.jaccard(&b), 1.0); + assert!(a.overlaps(&b)); + } + + #[test] + fn content_hash_is_stable_and_order_independent() { + let scope = BeliefScope::new("market"); + let q1 = ScopeQualifier::from_pairs([("metric", "engagement"), ("regime", "bull")]); + let q2 = ScopeQualifier::from_pairs([("regime", "bull"), ("metric", "engagement")]); + let claim = BeliefClaim::new("market", "engagement metrics are reliable"); + // Insertion order differs but BTreeMap canonicalises → same hash. + assert_eq!( + content_hash(&scope, &q1, &claim), + content_hash(&scope, &q2, &claim) + ); + } + + #[test] + fn content_hash_is_unambiguous_across_field_boundaries() { + // A naive `key=value\0` concatenation would collide these two qualifier + // pair sets (both flatten to "a=b=c"); length-prefixing keeps them + // distinct. + let scope = BeliefScope::new("market"); + let claim = BeliefClaim::new("market", "reliable"); + let q1 = ScopeQualifier::from_pairs([("a=b", "c")]); + let q2 = ScopeQualifier::from_pairs([("a", "b=c")]); + assert_ne!( + content_hash(&scope, &q1, &claim), + content_hash(&scope, &q2, &claim) + ); + + // Field boundaries between scope/subject/proposition are also + // unambiguous: shifting a byte across a boundary changes the hash. + let a = content_hash( + &BeliefScope::new("mark"), + &ScopeQualifier::empty(), + &BeliefClaim::new("etmarket", "reliable"), + ); + let b = content_hash( + &BeliefScope::new("market"), + &ScopeQualifier::empty(), + &BeliefClaim::new("market", "reliable"), + ); + assert_ne!(a, b); + } + + #[test] + fn content_hash_changes_with_proposition() { + let scope = BeliefScope::new("market"); + let q = ScopeQualifier::empty(); + let a = BeliefClaim::new("market", "reliable"); + let b = BeliefClaim::new("market", "unreliable"); + assert_ne!(content_hash(&scope, &q, &a), content_hash(&scope, &q, &b)); + } + + #[test] + fn bitemporal_completeness() { + assert!(BiTemporalStamp::new(ts(1000), ts(2000)).is_complete()); + assert!(!BiTemporalStamp::new(DateTime::::UNIX_EPOCH, ts(2000)).is_complete()); + // A historical belief (valid from 1965) is complete: only the epoch + // sentinel is rejected, not every pre-1970 instant. + assert!(BiTemporalStamp::new(ts(-157_766_400), ts(2000)).is_complete()); + assert!(!BiTemporalStamp::new(ts(1000), DateTime::::UNIX_EPOCH).is_complete()); + } + + #[test] + fn revision_trigger_and_change_labels() { + assert_eq!(RevisionTrigger::NewEvidence.as_str(), "new evidence"); + assert_eq!(RevisionChange::Negated.as_str(), "from A to not-A"); + } + + #[test] + fn token_roundtrips_through_json() { + let token = BeliefWriteToken { + capability_id: CapabilityId::new("cap-belief-write"), + scope: BeliefScope::new("market"), + scope_qualifier: ScopeQualifier::from_pairs([("metric", "engagement")]), + cited_evidence: vec![EvidenceRef::source("observation").with_locator("evt-42")], + formation_context: SessionContext::new("sess-1", AnimaDid::new("did:key:z6MkAlice")), + revision_link: Some(RevisionLink::new( + ContentAddressedRef::new("deadbeef", ts(500)), + vec![EvidenceRef::source("lago:event")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "engagement turned out to be gameable", + ), + )), + signed_by: AnimaDid::new("did:key:z6MkAlice"), + timestamp: BiTemporalStamp::new(ts(1000), ts(1000)), + }; + let json = serde_json::to_string(&token).unwrap(); + let back: BeliefWriteToken = serde_json::from_str(&json).unwrap(); + assert_eq!(token, back); + assert!(back.has_evidence()); + } +} diff --git a/crates/praxis/praxis-core/src/lib.rs b/crates/praxis/praxis-core/src/lib.rs index 6a942932..8a25c30c 100644 --- a/crates/praxis/praxis-core/src/lib.rs +++ b/crates/praxis/praxis-core/src/lib.rs @@ -4,11 +4,18 @@ //! Provides workspace boundary enforcement, sandbox policy, //! the command runner abstraction, and the filesystem port. +pub mod belief; pub mod error; pub mod fs_port; pub mod local_fs; pub mod sandbox; pub mod workspace; +pub use belief::{ + AnimaDid, BeliefClaim, BeliefClass, BeliefRevisionAcknowledgment, BeliefScope, + BeliefWriteToken, BiTemporalStamp, CapabilityId, ContentAddressedRef, EvidenceRef, + QualifierKey, QualifierValue, RevisionChange, RevisionLink, RevisionTrigger, ScopeQualifier, + SessionContext, content_hash, +}; pub use fs_port::{FsDirEntry, FsMetadata, FsPort}; pub use local_fs::LocalFs; diff --git a/crates/praxis/praxis-tools/Cargo.toml b/crates/praxis/praxis-tools/Cargo.toml index 263d4304..bef04da5 100644 --- a/crates/praxis/praxis-tools/Cargo.toml +++ b/crates/praxis/praxis-tools/Cargo.toml @@ -12,6 +12,7 @@ description = "Canonical tool implementations (filesystem, editing, shell, memor aios-protocol.workspace = true praxis-core.workspace = true blake3.workspace = true +chrono.workspace = true glob.workspace = true regex.workspace = true serde.workspace = true diff --git a/crates/praxis/praxis-tools/src/belief.rs b/crates/praxis/praxis-tools/src/belief.rs new file mode 100644 index 00000000..55980337 --- /dev/null +++ b/crates/praxis/praxis-tools/src/belief.rs @@ -0,0 +1,1310 @@ +//! # Belief write path, store, and revision-graph traversal +//! +//! This module is the runtime for the four-dimensional [`BeliefWriteToken`] +//! defined in `praxis_core::belief`. It provides: +//! +//! - [`BeliefStore`] — an in-memory reference store of belief records with a +//! capability-grant registry (mirroring the `praxis-skills` / +//! `nous-tools::lineage` in-memory-reference convention). A lago-backed +//! store lands separately. +//! - [`BeliefStore::write_belief`] — the write path enforcing the six checks, +//! including the new [`BeliefWriteError::MissingRevisionLink`] on overlapping +//! scope. +//! - [`BeliefStore::traverse_revisions`] — the revision-graph traversal API +//! returning the chain of supersession (immediate-predecessor links, +//! reconstructed transitively by walking). +//! - [`route_write`] / [`BeliefStore::record_operational`] — the migration: +//! token-less writes route to the Vigil-observed *tested-operational* class; +//! token writes take the Praxis *untested-normative* path. +//! - [`BeliefStore::recent_supersessions`] — the substrate read-model the Nous +//! L2 metacognitive surface projects as *"what did I supersede recently and +//! why"*. +//! - [`revision_masks_contradiction`] — the bookkeeping gate: a contradiction +//! covered by a revision link is *visible history*, not a contradiction. + +use chrono::{DateTime, Utc}; +use praxis_core::belief::{ + AnimaDid, BeliefClaim, BeliefClass, BeliefRevisionAcknowledgment, BeliefScope, + BeliefWriteToken, ContentAddressedRef, RevisionLink, ScopeQualifier, content_hash, +}; +use std::collections::{BTreeSet, HashMap}; +use thiserror::Error; + +/// A capability grant — which coarse [`BeliefScope`]s a capability authorizes a +/// principal to write beliefs about. +/// +/// The write path resolves [`BeliefWriteToken::capability_id`] against the +/// store's registry and checks scope containment. +#[derive(Debug, Clone)] +pub struct CapabilityGrant { + /// The capability id (matches [`BeliefWriteToken::capability_id`]). + pub id: praxis_core::belief::CapabilityId, + /// The scopes this capability authorizes belief writes about. + pub granted_scopes: BTreeSet, +} + +impl CapabilityGrant { + /// A grant for a single scope. + pub fn new(id: impl Into, scopes: impl IntoIterator) -> Self { + Self { + id: praxis_core::belief::CapabilityId::new(id), + granted_scopes: scopes.into_iter().collect(), + } + } + + /// Whether this grant authorizes writes about `scope`. + pub fn grants(&self, scope: &BeliefScope) -> bool { + self.granted_scopes.contains(scope) + } +} + +/// A stored belief record — the claim, its four-dimensional token, and derived +/// bookkeeping fields. +#[derive(Debug, Clone)] +pub struct BeliefRecord { + /// Store-assigned identifier (`blf-00000001`). + pub id: String, + /// Blake3 content hash of the belief's semantic identity. + pub content_hash: String, + /// The claim the belief asserts. + pub claim: BeliefClaim, + /// The four-dimensional formation token. + pub token: BeliefWriteToken, + /// Belief class — normative (Praxis) or operational (Vigil). + pub class: BeliefClass, + /// If a later belief has superseded this one, its id. + pub superseded_by: Option, +} + +impl BeliefRecord { + /// A content-addressed reference to *this* belief, for another belief to + /// supersede it. + pub fn as_ref(&self) -> ContentAddressedRef { + ContentAddressedRef::new(self.content_hash.clone(), self.token.timestamp.valid_from) + } + + /// True while no later belief supersedes this one. + pub fn is_live(&self) -> bool { + self.superseded_by.is_none() + } +} + +/// Errors returned by the belief write path. +#[derive(Debug, Clone, Error, PartialEq)] +pub enum BeliefWriteError { + /// Check 1 — no capability provided. + #[error("belief write rejected: no capability provided")] + MissingCapability, + + /// Check 1 — capability provided but not registered. + #[error("belief write rejected: capability '{capability}' is not registered")] + UnknownCapability { + /// The unresolved capability id. + capability: String, + }, + + /// Check 2 — the capability does not grant the belief's scope. + #[error("belief write rejected: capability '{capability}' does not grant scope '{scope}'")] + ScopeMismatch { + /// The capability id. + capability: String, + /// The scope that was not granted. + scope: String, + }, + + /// Check 3 — a normative belief must carry a scope qualifier. + #[error("belief write rejected: a normative belief requires a scope qualifier")] + MissingScopeQualifier, + + /// Check 4 — a normative belief must cite evidence. + #[error("belief write rejected: a normative belief must cite at least one evidence reference")] + MissingEvidence, + + /// Check 5 — an overlapping belief exists but no revision link was provided. + #[error( + "belief write rejected: a belief with overlapping scope (jaccard {jaccard:.2}) already \ + exists for this principal (id {existing_id}); either revise the existing belief or \ + specify a non-overlapping scope" + )] + MissingRevisionLink { + /// The id of the live overlapping belief the write must revise. + existing_id: String, + /// The measured qualifier overlap. + jaccard: f64, + }, + + /// Check 5 — a revision link was provided but its target does not exist. + #[error("belief write rejected: revision link supersedes {hash} but no such belief exists")] + RevisionTargetNotFound { + /// The dangling superseded content hash. + hash: String, + }, + + /// Check 5 — a revision link was provided but it does not target the live + /// belief it must revise. Either a live overlapping head exists and the + /// link points elsewhere (stale, cross-principal, or unrelated), or no + /// overlapping belief exists in this slot to revise at all. + #[error( + "belief write rejected: revision link must target the live overlapping belief for this \ + principal + scope{}", + match .expected_id { + Some(id) => format!(" (expected id {id})"), + None => " (no overlapping belief exists to revise — remove the revision link or narrow the scope)".to_string(), + } + )] + RevisionMustTargetHead { + /// The id of the live head the link must target, if one exists. + expected_id: Option, + }, + + /// Check 5 — more than one live belief overlaps the write's scope, so the + /// revision target is ambiguous. + #[error( + "belief write rejected: {count} live beliefs overlap this principal + scope; narrow the \ + scope_qualifier so the revision target is unambiguous" + )] + AmbiguousOverlap { + /// How many live beliefs overlap. + count: usize, + }, + + /// Check 6 — the bi-temporal stamp is incomplete. + #[error( + "belief write rejected: bi-temporal stamp is incomplete (valid_from and recorded_at must \ + both be set)" + )] + IncompleteBiTemporalStamp, +} + +/// Where a belief write is routed — the two-class migration. +#[derive(Debug, Clone, Copy, PartialEq, Eq)] +pub enum BeliefWriteRoute { + /// Token-bearing write → Praxis principal, untested-normative class, all + /// four formation dimensions enforced. + PraxisNormative, + /// Token-less write → Vigil-observed, tested-operational class, survives on + /// functional aliveness rather than formation context. + VigilOperational, +} + +/// The migration rule: a write carrying a formation token takes the Praxis +/// normative path; a legacy token-less write routes to the Vigil operational +/// surface. +pub fn route_write(has_token: bool) -> BeliefWriteRoute { + if has_token { + BeliefWriteRoute::PraxisNormative + } else { + BeliefWriteRoute::VigilOperational + } +} + +/// Whether a would-be contradiction between a newer token and an older belief +/// is *masked* — i.e. the newer belief carries a revision link that supersedes +/// exactly that older belief. When true, bookkeeping contradiction detection +/// must treat the pair as **visible history**, not a contradiction. +pub fn revision_masks_contradiction(newer: &BeliefWriteToken, older: &ContentAddressedRef) -> bool { + matches!(&newer.revision_link, Some(link) if &link.superseded == older) +} + +/// One entry in a revision chain returned by [`BeliefStore::traverse_revisions`]. +#[derive(Debug, Clone)] +pub struct RevisionChainEntry { + /// The belief record at this link. + pub record: BeliefRecord, + /// The acknowledgment that links this record to the *successor* which + /// superseded it — i.e. the revision that discarded this record as a draft. + /// `None` for the live head (nothing supersedes it). + pub via: Option, +} + +/// The substrate read-model behind the Nous L2 metacognitive surface — +/// *"what did I supersede recently and why"*. +#[derive(Debug, Clone)] +pub struct SupersessionView { + /// The superseding belief's id. + pub superseding_id: String, + /// The superseding belief's claim. + pub claim: BeliefClaim, + /// The coarse scope of the supersession. + pub scope: BeliefScope, + /// The prior belief that was superseded. + pub superseded: ContentAddressedRef, + /// The structured + free-form acknowledgment of the change. + pub acknowledgment: BeliefRevisionAcknowledgment, + /// When the supersession was recorded. + pub recorded_at: DateTime, +} + +/// In-memory reference store of belief records + capability grants. +/// +/// Append-only: records are never mutated except to stamp `superseded_by` when +/// a later belief supersedes them, preserving full history for traversal. +#[derive(Debug, Default)] +pub struct BeliefStore { + records: Vec, + by_id: HashMap, + capabilities: HashMap, + next_seq: u64, +} + +impl BeliefStore { + /// A fresh, empty store. + pub fn new() -> Self { + Self::default() + } + + /// Register a capability grant so writes citing it can be authorized. + pub fn register_capability(&mut self, grant: CapabilityGrant) { + self.capabilities.insert(grant.id.clone(), grant); + } + + /// All records, in recorded order. + pub fn records(&self) -> &[BeliefRecord] { + &self.records + } + + /// Look up a record by its store-assigned id. + pub fn get(&self, id: &str) -> Option<&BeliefRecord> { + self.by_id.get(id).map(|&i| &self.records[i]) + } + + /// Resolve a content-addressed reference to a stored record (matching both + /// content hash and `valid_from`). + pub fn resolve(&self, r: &ContentAddressedRef) -> Option<&BeliefRecord> { + self.records.iter().find(|rec| { + rec.content_hash == r.content_hash && rec.token.timestamp.valid_from == r.valid_from + }) + } + + fn resolve_index(&self, r: &ContentAddressedRef) -> Option { + self.records.iter().position(|rec| { + rec.content_hash == r.content_hash && rec.token.timestamp.valid_from == r.valid_from + }) + } + + /// Indices of every **live** (not-yet-superseded) belief for `principal` in + /// the same coarse `scope` whose qualifier overlaps `qualifier` at or above + /// the Jaccard threshold, each paired with the measured overlap. + /// + /// Returns *all* overlapping live heads (not just the strongest): more than + /// one means the revision target is ambiguous and the write must be + /// rejected rather than silently superseding one head while leaving another + /// conflicting belief live. + fn live_overlapping_indices( + &self, + principal: &AnimaDid, + scope: &BeliefScope, + qualifier: &ScopeQualifier, + ) -> Vec<(usize, f64)> { + self.records + .iter() + .enumerate() + .filter(|(_, rec)| rec.is_live()) + .filter(|(_, rec)| &rec.token.signed_by == principal) + .filter(|(_, rec)| &rec.token.scope == scope) + .map(|(i, rec)| (i, rec.token.scope_qualifier.jaccard(qualifier))) + .filter(|(_, j)| *j >= ScopeQualifier::OVERLAP_THRESHOLD) + .collect() + } + + /// Write a normative belief through the four-dimensional token, enforcing + /// the six write-path checks in order. On success the record is committed + /// and any superseded predecessor is stamped. + /// + /// See [`BeliefWriteError`] for the failure taxonomy. + pub fn write_belief( + &mut self, + claim: BeliefClaim, + token: BeliefWriteToken, + ) -> Result { + // Check 1 — capability presence. + if !token.capability_id.is_present() { + return Err(BeliefWriteError::MissingCapability); + } + let grant = self.capabilities.get(&token.capability_id).ok_or_else(|| { + BeliefWriteError::UnknownCapability { + capability: token.capability_id.to_string(), + } + })?; + + // Check 2 — scope match. + if !grant.grants(&token.scope) { + return Err(BeliefWriteError::ScopeMismatch { + capability: token.capability_id.to_string(), + scope: token.scope.to_string(), + }); + } + + // Check 6 — bi-temporal stamps both set. (Checked early: a malformed + // stamp is invalid regardless of the other dimensions.) + if !token.timestamp.is_complete() { + return Err(BeliefWriteError::IncompleteBiTemporalStamp); + } + + // Check 3 — scope qualifier presence (required for normative beliefs). + if token.scope_qualifier.is_empty() { + return Err(BeliefWriteError::MissingScopeQualifier); + } + + // Check 4 — evidence trace (required for normative beliefs). + if !token.has_evidence() { + return Err(BeliefWriteError::MissingEvidence); + } + + // Check 5 — revision link required when an overlapping live belief + // already exists for this principal, and it must target that exact live + // head. This prevents a write from superseding an unrelated, stale + // (already-superseded), or cross-principal record while leaving the + // conflicting live belief in place. + let principal = token.signed_by.clone(); + let overlaps = + self.live_overlapping_indices(&principal, &token.scope, &token.scope_qualifier); + + // More than one live overlapping head ⇒ the revision target is + // ambiguous. Reject rather than pick one arbitrarily. + if overlaps.len() > 1 { + return Err(BeliefWriteError::AmbiguousOverlap { + count: overlaps.len(), + }); + } + + let superseded_index = match (overlaps.first().copied(), &token.revision_link) { + // A live overlapping head exists but the write does not revise it. + (Some((head_idx, jaccard)), None) => { + return Err(BeliefWriteError::MissingRevisionLink { + existing_id: self.records[head_idx].id.clone(), + jaccard, + }); + } + // A live overlapping head exists and the write carries a revision + // link — it MUST target exactly that head (identity by content ref). + (Some((head_idx, _)), Some(link)) => { + let head_ref = self.records[head_idx].as_ref(); + if link.superseded != head_ref { + return Err(BeliefWriteError::RevisionMustTargetHead { + expected_id: Some(self.records[head_idx].id.clone()), + }); + } + Some(head_idx) + } + // No live overlapping head, but a revision link was supplied. There + // is nothing in this slot to revise: the target is either dangling + // (does not resolve) or points at a stale / cross-principal record. + (None, Some(link)) => match self.resolve_index(&link.superseded) { + None => { + return Err(BeliefWriteError::RevisionTargetNotFound { + hash: link.superseded.content_hash.clone(), + }); + } + Some(_) => { + return Err(BeliefWriteError::RevisionMustTargetHead { expected_id: None }); + } + }, + // Free slot, first assertion. + (None, None) => None, + }; + + // Commit. + let hash = content_hash(&token.scope, &token.scope_qualifier, &claim); + self.next_seq += 1; + let id = format!("blf-{:08}", self.next_seq); + let record = BeliefRecord { + id: id.clone(), + content_hash: hash, + claim, + token, + class: BeliefClass::UntestedNormative, + superseded_by: None, + }; + + if let Some(idx) = superseded_index { + self.records[idx].superseded_by = Some(id.clone()); + } + + let index = self.records.len(); + self.records.push(record.clone()); + self.by_id.insert(id, index); + Ok(record) + } + + /// Record a legacy, token-less belief as a *tested-operational* belief — + /// the Vigil-observed class. No formation dimensions are enforced; the + /// belief survives on functional aliveness, not on formation context. + /// + /// This is the migration target for pre-token writes (deliverable 3). + pub fn record_operational( + &mut self, + claim: BeliefClaim, + scope: BeliefScope, + observed_at: DateTime, + observer: AnimaDid, + ) -> BeliefRecord { + let token = BeliefWriteToken { + capability_id: praxis_core::belief::CapabilityId::new(""), + scope: scope.clone(), + scope_qualifier: ScopeQualifier::empty(), + cited_evidence: Vec::new(), + formation_context: praxis_core::belief::SessionContext::new( + "vigil:observed", + observer.clone(), + ), + revision_link: None, + signed_by: observer, + timestamp: praxis_core::belief::BiTemporalStamp::at(observed_at), + }; + let hash = content_hash(&scope, &token.scope_qualifier, &claim); + self.next_seq += 1; + let id = format!("blf-{:08}", self.next_seq); + let record = BeliefRecord { + id: id.clone(), + content_hash: hash, + claim, + token, + class: BeliefClass::TestedOperational, + superseded_by: None, + }; + let index = self.records.len(); + self.records.push(record.clone()); + self.by_id.insert(id, index); + record + } + + /// Walk the revision graph from `belief_id`, following immediate-predecessor + /// links up to `depth` supersessions. The returned chain starts with the + /// belief itself and proceeds to older, superseded beliefs. + /// + /// A `depth` of 0 returns just the starting belief. The chain is + /// reconstructed transitively — each belief links only to its immediate + /// predecessor (open question 3, PROVISIONAL). + pub fn traverse_revisions(&self, belief_id: &str, depth: usize) -> Vec { + let mut chain = Vec::new(); + let mut current = self.get(belief_id).cloned(); + let mut via: Option = None; + let mut steps = 0usize; + + while let Some(rec) = current { + let next_link: Option = rec.token.revision_link.clone(); + let rec_id = rec.id.clone(); + chain.push(RevisionChainEntry { + record: rec, + via: via.take(), + }); + if steps >= depth { + break; + } + match next_link { + Some(link) => { + via = Some(link.acknowledgment.clone()); + // Follow the store's own back-pointer, not the link's + // content-addressed ref. The write path stamps the exact + // record it superseded with `superseded_by`, so this is + // unique. `resolve(&link.superseded)` is not: the content + // hash is principal-agnostic by design and a revision may + // keep the same `valid_from`, so a first match can land on + // another principal's record or skip a version. + current = self + .records + .iter() + .find(|r| r.superseded_by.as_deref() == Some(rec_id.as_str())) + .cloned(); + steps += 1; + } + None => break, + } + } + chain + } + + /// The Nous L2 metacognitive read-model: the most recent supersessions by + /// `principal`, newest first, capped at `limit`. Each view answers *what + /// did I supersede, and why*. + pub fn recent_supersessions( + &self, + principal: &AnimaDid, + limit: usize, + ) -> Vec { + let mut views: Vec = self + .records + .iter() + .filter(|rec| &rec.token.signed_by == principal) + .filter_map(|rec| { + rec.token + .revision_link + .as_ref() + .map(|link| SupersessionView { + superseding_id: rec.id.clone(), + claim: rec.claim.clone(), + scope: rec.token.scope.clone(), + superseded: link.superseded.clone(), + acknowledgment: link.acknowledgment.clone(), + recorded_at: rec.token.timestamp.recorded_at, + }) + }) + .collect(); + // Newest first; break ties by superseding id (which is seq-ordered). + views.sort_by(|a, b| { + b.recorded_at + .cmp(&a.recorded_at) + .then_with(|| b.superseding_id.cmp(&a.superseding_id)) + }); + views.truncate(limit); + views + } +} + +#[cfg(test)] +mod tests { + use super::*; + use chrono::TimeZone; + use praxis_core::belief::{ + BiTemporalStamp, CapabilityId, EvidenceRef, RevisionChange, RevisionTrigger, SessionContext, + }; + + fn ts(secs: i64) -> DateTime { + Utc.timestamp_opt(secs, 0).single().unwrap() + } + + fn alice() -> AnimaDid { + AnimaDid::new("did:key:z6MkAlice") + } + + fn bob() -> AnimaDid { + AnimaDid::new("did:key:z6MkBob") + } + + fn store_with_cap() -> BeliefStore { + let mut store = BeliefStore::new(); + store.register_capability(CapabilityGrant::new( + "cap-belief-write", + [BeliefScope::new("market"), BeliefScope::new("self")], + )); + store + } + + /// Build a normative token for `market` with the given qualifier + optional + /// revision link. + fn token( + qualifier: ScopeQualifier, + revision: Option, + valid_from: i64, + recorded_at: i64, + ) -> BeliefWriteToken { + BeliefWriteToken { + capability_id: CapabilityId::new("cap-belief-write"), + scope: BeliefScope::new("market"), + scope_qualifier: qualifier, + cited_evidence: vec![EvidenceRef::source("observation")], + formation_context: SessionContext::new("sess-1", alice()), + revision_link: revision, + signed_by: alice(), + timestamp: BiTemporalStamp::new(ts(valid_from), ts(recorded_at)), + } + } + + #[test] + fn write_fails_without_capability() { + let mut store = store_with_cap(); + let mut t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ); + t.capability_id = CapabilityId::new(""); + let err = store + .write_belief(BeliefClaim::new("market", "reliable"), t) + .unwrap_err(); + assert_eq!(err, BeliefWriteError::MissingCapability); + } + + #[test] + fn write_fails_with_unregistered_capability() { + let mut store = BeliefStore::new(); // no grants registered + let t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ); + let err = store + .write_belief(BeliefClaim::new("market", "reliable"), t) + .unwrap_err(); + assert!(matches!(err, BeliefWriteError::UnknownCapability { .. })); + } + + #[test] + fn write_fails_on_scope_mismatch() { + let mut store = store_with_cap(); + let mut t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ); + t.scope = BeliefScope::new("weather"); // not granted + let err = store + .write_belief(BeliefClaim::new("weather", "sunny"), t) + .unwrap_err(); + assert!(matches!(err, BeliefWriteError::ScopeMismatch { .. })); + } + + #[test] + fn write_fails_without_scope_qualifier() { + let mut store = store_with_cap(); + let t = token(ScopeQualifier::empty(), None, 1000, 1000); + let err = store + .write_belief(BeliefClaim::new("market", "reliable"), t) + .unwrap_err(); + assert_eq!(err, BeliefWriteError::MissingScopeQualifier); + } + + #[test] + fn write_fails_without_evidence() { + let mut store = store_with_cap(); + let mut t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ); + t.cited_evidence.clear(); + let err = store + .write_belief(BeliefClaim::new("market", "reliable"), t) + .unwrap_err(); + assert_eq!(err, BeliefWriteError::MissingEvidence); + } + + #[test] + fn write_fails_on_incomplete_bitemporal() { + let mut store = store_with_cap(); + let mut t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ); + t.timestamp.valid_from = DateTime::::UNIX_EPOCH; + let err = store + .write_belief(BeliefClaim::new("market", "reliable"), t) + .unwrap_err(); + assert_eq!(err, BeliefWriteError::IncompleteBiTemporalStamp); + } + + #[test] + fn first_write_in_a_slot_succeeds() { + let mut store = store_with_cap(); + let t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ); + let rec = store + .write_belief(BeliefClaim::new("market", "reliable"), t) + .unwrap(); + assert_eq!(rec.class, BeliefClass::UntestedNormative); + assert!(rec.is_live()); + assert_eq!(store.records().len(), 1); + } + + #[test] + fn overlapping_write_without_revision_link_is_rejected() { + let mut store = store_with_cap(); + // First belief. + store + .write_belief( + BeliefClaim::new("market", "engagement is reliable"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + // Contradicting belief, same slot, no revision link → rejected. + let err = store + .write_belief( + BeliefClaim::new("market", "engagement is NOT reliable"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 2000, + 2000, + ), + ) + .unwrap_err(); + match err { + BeliefWriteError::MissingRevisionLink { + existing_id, + jaccard, + } => { + assert_eq!(existing_id, "blf-00000001"); + assert_eq!(jaccard, 1.0); + } + other => panic!("expected MissingRevisionLink, got {other:?}"), + } + } + + #[test] + fn disjoint_scope_qualifier_allows_parallel_beliefs() { + let mut store = store_with_cap(); + store + .write_belief( + BeliefClaim::new("market", "engagement is reliable"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + // Different metric → disjoint qualifier → parallel, no revision needed. + let rec = store + .write_belief( + BeliefClaim::new("market", "revenue is reliable"), + token( + ScopeQualifier::from_pairs([("metric", "revenue")]), + None, + 2000, + 2000, + ), + ) + .unwrap(); + assert!(rec.is_live()); + assert_eq!(store.records().iter().filter(|r| r.is_live()).count(), 2); + } + + #[test] + fn revision_link_supersedes_and_marks_predecessor() { + let mut store = store_with_cap(); + let first = store + .write_belief( + BeliefClaim::new("market", "engagement is reliable"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + let link = RevisionLink::new( + first.as_ref(), + vec![EvidenceRef::source("lago:event").with_locator("evt-99")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "engagement turned out to be gameable under adversarial load", + ), + ); + let second = store + .write_belief( + BeliefClaim::new("market", "engagement is NOT reliable"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(link), + 2000, + 2000, + ), + ) + .unwrap(); + // Predecessor now superseded; successor live. + assert_eq!( + store.get(&first.id).unwrap().superseded_by.as_deref(), + Some(second.id.as_str()) + ); + assert!(store.get(&second.id).unwrap().is_live()); + // The slot's only live belief is the successor. + assert_eq!(store.records().iter().filter(|r| r.is_live()).count(), 1); + } + + #[test] + fn dangling_revision_link_is_rejected() { + let mut store = store_with_cap(); + let bogus = ContentAddressedRef::new("nonexistent-hash", ts(5)); + let link = RevisionLink::new( + bogus, + vec![EvidenceRef::source("x")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "…", + ), + ); + let err = store + .write_belief( + BeliefClaim::new("market", "engagement is NOT reliable"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(link), + 2000, + 2000, + ), + ) + .unwrap_err(); + assert!(matches!( + err, + BeliefWriteError::RevisionTargetNotFound { .. } + )); + } + + fn ack(note: &str) -> BeliefRevisionAcknowledgment { + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + note, + ) + } + + #[test] + fn traverse_follows_its_own_principal_when_refs_collide() { + // Alice and Bob hold the SAME claim, scope, qualifier and valid_from, so + // their records carry identical content-addressed refs. Bob's revision + // chain must lead back to Bob's record, not to the first match. + let mut store = store_with_cap(); + let q = || ScopeQualifier::from_pairs([("metric", "engagement")]); + let alice_rec = store + .write_belief( + BeliefClaim::new("market", "same"), + token(q(), None, 1000, 1000), + ) + .unwrap(); + let mut bt = token(q(), None, 1000, 1001); + bt.signed_by = bob(); + bt.formation_context = SessionContext::new("sess-2", bob()); + let bob_rec = store + .write_belief(BeliefClaim::new("market", "same"), bt) + .unwrap(); + assert_eq!( + alice_rec.as_ref(), + bob_rec.as_ref(), + "precondition: refs collide" + ); + + let mut rt = token( + q(), + Some(RevisionLink::new( + bob_rec.as_ref(), + vec![EvidenceRef::source("e")], + ack("bob revises"), + )), + 2000, + 2000, + ); + rt.signed_by = bob(); + rt.formation_context = SessionContext::new("sess-2", bob()); + let bob_rev = store + .write_belief(BeliefClaim::new("market", "revised"), rt) + .unwrap(); + + let chain = store.traverse_revisions(&bob_rev.id, 10); + assert_eq!(chain.len(), 2); + assert_eq!( + chain[1].record.id, bob_rec.id, + "must not cross to Alice's record" + ); + } + + #[test] + fn traverse_does_not_skip_a_version_with_repeated_content() { + // Three versions with identical content and valid_from share one ref; + // v3's predecessor is v2, not the first record carrying that ref. + let mut store = store_with_cap(); + let q = || ScopeQualifier::from_pairs([("metric", "engagement")]); + let v1 = store + .write_belief( + BeliefClaim::new("market", "x"), + token(q(), None, 1000, 1000), + ) + .unwrap(); + let link = |r: &BeliefRecord| { + Some(RevisionLink::new( + r.as_ref(), + vec![EvidenceRef::source("e")], + ack("restated"), + )) + }; + let v2 = store + .write_belief( + BeliefClaim::new("market", "x"), + token(q(), link(&v1), 1000, 2000), + ) + .unwrap(); + let v3 = store + .write_belief( + BeliefClaim::new("market", "x"), + token(q(), link(&v2), 1000, 3000), + ) + .unwrap(); + + let ids: Vec<_> = store + .traverse_revisions(&v3.id, 10) + .into_iter() + .map(|e| e.record.id) + .collect(); + assert_eq!(ids, vec![v3.id, v2.id, v1.id]); + } + + #[test] + fn traverse_revisions_walks_the_chain() { + let mut store = store_with_cap(); + let a = store + .write_belief( + BeliefClaim::new("market", "A"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + let b = store + .write_belief( + BeliefClaim::new("market", "B"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + a.as_ref(), + vec![EvidenceRef::source("e1")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "A→B", + ), + )), + 2000, + 2000, + ), + ) + .unwrap(); + let c = store + .write_belief( + BeliefClaim::new("market", "C"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + b.as_ref(), + vec![EvidenceRef::source("e2")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::ContextShift, + RevisionChange::Qualified, + "B→C", + ), + )), + 3000, + 3000, + ), + ) + .unwrap(); + + // Full chain from the head. + let chain = store.traverse_revisions(&c.id, 10); + let ids: Vec<&str> = chain.iter().map(|e| e.record.id.as_str()).collect(); + assert_eq!(ids, vec![c.id.as_str(), b.id.as_str(), a.id.as_str()]); + // The head has no incoming ack; each older entry carries the ack that + // linked its successor to it. + assert!(chain[0].via.is_none()); + assert_eq!(chain[1].via.as_ref().unwrap().rationale, "B→C"); + assert_eq!(chain[2].via.as_ref().unwrap().rationale, "A→B"); + + // Depth-bounded traversal. + let shallow = store.traverse_revisions(&c.id, 1); + assert_eq!(shallow.len(), 2); + assert_eq!(shallow[0].record.id, c.id); + assert_eq!(shallow[1].record.id, b.id); + } + + #[test] + fn recent_supersessions_read_model() { + let mut store = store_with_cap(); + let a = store + .write_belief( + BeliefClaim::new("market", "A"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + let b = store + .write_belief( + BeliefClaim::new("market", "B"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + a.as_ref(), + vec![EvidenceRef::source("e1")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "A→B", + ), + )), + 2000, + 2000, + ), + ) + .unwrap(); + + let views = store.recent_supersessions(&alice(), 10); + assert_eq!(views.len(), 1); + assert_eq!(views[0].superseding_id, b.id); + assert_eq!(views[0].superseded, a.as_ref()); + assert_eq!( + views[0].acknowledgment.trigger, + RevisionTrigger::NewEvidence + ); + } + + #[test] + fn revision_masks_contradiction_gate() { + let a_ref = ContentAddressedRef::new("hash-a", ts(1000)); + // Token with a revision link superseding a_ref. + let mut t = token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + a_ref.clone(), + vec![EvidenceRef::source("e1")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "…", + ), + )), + 2000, + 2000, + ); + assert!(revision_masks_contradiction(&t, &a_ref)); + // A different older ref is NOT masked. + let other = ContentAddressedRef::new("hash-z", ts(1)); + assert!(!revision_masks_contradiction(&t, &other)); + // No revision link → never masks. + t.revision_link = None; + assert!(!revision_masks_contradiction(&t, &a_ref)); + } + + #[test] + fn migration_routing() { + assert_eq!(route_write(true), BeliefWriteRoute::PraxisNormative); + assert_eq!(route_write(false), BeliefWriteRoute::VigilOperational); + } + + #[test] + fn operational_write_bypasses_formation_checks() { + let mut store = store_with_cap(); + let rec = store.record_operational( + BeliefClaim::new("latency", "p99 under 200ms"), + BeliefScope::new("self"), + ts(1000), + alice(), + ); + assert_eq!(rec.class, BeliefClass::TestedOperational); + // Operational beliefs carry no capability and no evidence, yet persist. + assert!(!rec.token.capability_id.is_present()); + assert!(rec.token.cited_evidence.is_empty()); + } + + #[test] + fn third_write_must_revise_current_head_not_original() { + let mut store = store_with_cap(); + let a = store + .write_belief( + BeliefClaim::new("market", "A"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + let _b = store + .write_belief( + BeliefClaim::new("market", "B"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + a.as_ref(), + vec![EvidenceRef::source("e1")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "A→B", + ), + )), + 2000, + 2000, + ), + ) + .unwrap(); + // A third overlapping write with NO revision link is still rejected, + // now pointing at B (the live head), not the superseded A. + let err = store + .write_belief( + BeliefClaim::new("market", "C"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 3000, + 3000, + ), + ) + .unwrap_err(); + match err { + BeliefWriteError::MissingRevisionLink { existing_id, .. } => { + assert_eq!(existing_id, "blf-00000002"); // B, the live head + } + other => panic!("expected MissingRevisionLink, got {other:?}"), + } + } + + #[test] + fn revision_link_must_target_live_head_not_stale() { + let mut store = store_with_cap(); + let a = store + .write_belief( + BeliefClaim::new("market", "A"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + let b = store + .write_belief( + BeliefClaim::new("market", "B"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + a.as_ref(), + vec![EvidenceRef::source("e1")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "A→B", + ), + )), + 2000, + 2000, + ), + ) + .unwrap(); + // C tries to supersede the STALE A (already superseded by B) instead of + // the live head B — rejected; it must target B. + let err = store + .write_belief( + BeliefClaim::new("market", "C"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + Some(RevisionLink::new( + a.as_ref(), + vec![EvidenceRef::source("e2")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "C targets stale A", + ), + )), + 3000, + 3000, + ), + ) + .unwrap_err(); + match err { + BeliefWriteError::RevisionMustTargetHead { expected_id } => { + assert_eq!(expected_id.as_deref(), Some(b.id.as_str())); + } + other => panic!("expected RevisionMustTargetHead, got {other:?}"), + } + // The live head B is untouched. + assert!(store.get(&b.id).unwrap().is_live()); + } + + #[test] + fn revision_link_cannot_cross_principal() { + let mut store = store_with_cap(); + let a = store + .write_belief( + BeliefClaim::new("market", "A"), + token( + ScopeQualifier::from_pairs([("metric", "engagement")]), + None, + 1000, + 1000, + ), + ) + .unwrap(); + // Bob writes an overlapping belief and tries to supersede Alice's A. + // Bob has no live overlapping head of his own, so the link targets a + // record he does not own → rejected. + let bob_token = BeliefWriteToken { + capability_id: CapabilityId::new("cap-belief-write"), + scope: BeliefScope::new("market"), + scope_qualifier: ScopeQualifier::from_pairs([("metric", "engagement")]), + cited_evidence: vec![EvidenceRef::source("observation")], + formation_context: SessionContext::new("sess-b", bob()), + revision_link: Some(RevisionLink::new( + a.as_ref(), + vec![EvidenceRef::source("e")], + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + "bob supersedes alice", + ), + )), + signed_by: bob(), + timestamp: BiTemporalStamp::new(ts(2000), ts(2000)), + }; + let err = store + .write_belief(BeliefClaim::new("market", "B-bob"), bob_token) + .unwrap_err(); + assert!(matches!( + err, + BeliefWriteError::RevisionMustTargetHead { expected_id: None } + )); + // Alice's belief is untouched. + assert!(store.get(&a.id).unwrap().is_live()); + } + + #[test] + fn ambiguous_multi_head_overlap_is_rejected() { + let mut store = store_with_cap(); + // Two disjoint (hence both live) beliefs in the same coarse scope. + store + .write_belief( + BeliefClaim::new("market", "A"), + token(ScopeQualifier::from_pairs([("x", "1")]), None, 1000, 1000), + ) + .unwrap(); + store + .write_belief( + BeliefClaim::new("market", "B"), + token(ScopeQualifier::from_pairs([("y", "1")]), None, 1100, 1100), + ) + .unwrap(); + // C's qualifier {x:1, y:1} overlaps BOTH A and B at jaccard 0.5 → the + // revision target is ambiguous, so the write is rejected. + let err = store + .write_belief( + BeliefClaim::new("market", "C"), + token( + ScopeQualifier::from_pairs([("x", "1"), ("y", "1")]), + None, + 2000, + 2000, + ), + ) + .unwrap_err(); + match err { + BeliefWriteError::AmbiguousOverlap { count } => assert_eq!(count, 2), + other => panic!("expected AmbiguousOverlap, got {other:?}"), + } + } +} diff --git a/crates/praxis/praxis-tools/src/lib.rs b/crates/praxis/praxis-tools/src/lib.rs index 150695f5..d5f3bf84 100644 --- a/crates/praxis/praxis-tools/src/lib.rs +++ b/crates/praxis/praxis-tools/src/lib.rs @@ -7,11 +7,18 @@ //! - [`shell`] — Bash command execution //! - [`memory`] — Agent memory read/write (file-based) //! - [`remote`] — Remote command execution via [`arcan_sandbox::SandboxProvider`] +//! - [`belief`] — Four-dimensional [`belief::BeliefWriteToken`] write path, +//! belief store, and revision-graph traversal +pub mod belief; pub mod edit; pub mod fs; pub mod memory; pub mod remote; pub mod shell; +pub use belief::{ + BeliefRecord, BeliefStore, BeliefWriteError, BeliefWriteRoute, CapabilityGrant, + RevisionChainEntry, SupersessionView, revision_masks_contradiction, route_write, +}; pub use remote::RemoteCommandRunner; diff --git a/docs/specs/bro-1030-belief-write-token.html b/docs/specs/bro-1030-belief-write-token.html new file mode 100644 index 00000000..42731ed4 --- /dev/null +++ b/docs/specs/bro-1030-belief-write-token.html @@ -0,0 +1,232 @@ + + + + + + +BeliefWriteToken — Decision Matrix & Worked Examples · BRO-1030 + + + +
+
+
BRO-1030 · praxis · belief formation
+

The four-dimensional BeliefWriteToken

+

Silent accumulation of a belief cannot be distinguished from deliberate + updating unless the write records how the belief was formed. Four dimensions make + formation context first-class — and the fourth turns a contradiction from a versioning + failure into visible history.

+
+ +

The four dimensions

+
+
Who authorized this belief?

Capability

capability_id
+
When in the world / in the system?

Bi-temporal

timestamp
{ valid_from, recorded_at }
+
About what, precisely?

Scope

scope +
scope_qualifier
+
NEW
What was superseded?

Revision

revision_link
+
+ +
+ + + + + + + + + Prior belief "A" + content_hash + valid_from + + + revision_link + + + BeliefWriteToken (belief "not-A") + capability_id + timestamp + scope + qualifier + revision_link + signed_by · cited_evidence · formation_context + + + write_belief + + + Live head "not-A" + A stamped superseded_by + +
+ +

Write-path decision matrix

+

Each check runs in order. The first failure short-circuits with its typed error.

+
+
1 · Capability presence
capability resolves to a grant
MissingCapability / UnknownCapability
+
2 · Scope match
grant authorizes the scope
ScopeMismatch
+
3 · Bi-temporal
valid_from & recorded_at set
IncompleteBiTemporalStamp
+
4 · Scope qualifier
present for normative beliefs
MissingScopeQualifier
+
5 · Evidence trace
≥ 1 cited evidence
MissingEvidence
+
6 · Revision link
required on overlap ≥ 0.5; must target the live head
MissingRevisionLink / RevisionMustTargetHead / AmbiguousOverlap / RevisionTargetNotFound
+
+ +

Overlap → revision decision

+ + + + + + + + + + + +
Existing live belief in slot?Qualifier Jaccardrevision_linkOutcome
none—absentaccept first assertion
yes, same principal + scope< 0.5 (disjoint)absentaccept parallel belief
one live head, same principal + scope≥ 0.5 (overlap)absentreject MissingRevisionLink
one live head, same principal + scope≥ 0.5 (overlap)present → exactly the live headaccept supersede, becomes visible history
one live head, same principal + scope≥ 0.5 (overlap)present → stale / cross-principal / otherreject RevisionMustTargetHead
two or more live heads overlap≥ 0.5 eachanyreject AmbiguousOverlap — narrow scope
none—present → non-existent targetreject RevisionTargetNotFound
+ +

Two belief classes

+ + + + + + +
ClassSurfaceAll 4 dimensions?Survives on
Untested-normativePraxis principal · write_beliefyescapability + scope + revision-link consistency
Tested-operationalVigil-observed · record_operationalnofunctional aliveness
+

Migration: a write carrying a token → Praxis normative path; a legacy token-less +write → Vigil operational surface. New writes without a revision link on an overlapping +scope are rejected, never silently accepted.

+ +

Worked examples

+ +
+

accept First assertion in a fresh slot

+
write_belief(
+  claim   = { subject: "market", proposition: "engagement metrics are reliable" },
+  token   = { capability_id: "cap-belief-write", scope: "market",
+              scope_qualifier: { metric: "engagement" },
+              cited_evidence: [ { source: "observation" } ],
+              revision_link: None, timestamp: { valid_from, recorded_at } } )
+→ Ok(blf-00000001)   // live head, class = UntestedNormative
+
+ +
+

reject Contradiction with no acknowledgment

+
// slot already holds "engagement is reliable" (blf-00000001)
+write_belief(
+  claim = { subject: "market", proposition: "engagement is NOT reliable" },
+  token = { scope: "market", scope_qualifier: { metric: "engagement" },
+            revision_link: None, ... } )
+→ Err(MissingRevisionLink { existing_id: "blf-00000001", jaccard: 1.00 })
+// "either revise the existing belief or specify a non-overlapping scope"
+
+ +
+

visible history Same contradiction, acknowledged

+
write_belief(
+  claim = { subject: "market", proposition: "engagement is NOT reliable" },
+  token = { scope: "market", scope_qualifier: { metric: "engagement" },
+            revision_link: {
+              superseded: { content_hash: hash(blf-00000001), valid_from },
+              triggered_by: [ { source: "lago:event", locator: "evt-99" } ],
+              acknowledgment: {
+                trigger: NewEvidence, change: Negated,
+                rationale: "engagement turned out to be gameable under adversarial load" } },
+            ... } )
+→ Ok(blf-00000002)   // blf-00000001 stamped superseded_by = blf-00000002
+// bookkeeping: revision_masks_contradiction() ⇒ true ⇒ NOT flagged as a contradiction
+
+ +
+

accept Disjoint qualifier → parallel belief

+
// slot holds "engagement is reliable" under { metric: "engagement" }
+write_belief(
+  claim = { subject: "market", proposition: "revenue is reliable" },
+  token = { scope: "market", scope_qualifier: { metric: "revenue" },  // jaccard 0.0
+            revision_link: None, ... } )
+→ Ok(blf-00000002)   // two live beliefs coexist — no revision required
+
+ +

Revision-graph traversal & the Nous L2 surface

+
+

traverse_revisions(belief_id, depth) walks immediate-predecessor links from the +live head back through discarded drafts — C → B → A — each entry carrying the +acknowledgment that linked its successor to it.

+

recent_supersessions(principal, limit) is the substrate read-model the Nous L2 +metacognitive surface projects as "what did I supersede recently, and why". Praxis owns +the queryable substrate; Nous projects it — no praxis → nous dependency.

+
+ +
+

Canonical contract: docs/specs/bro-1030-belief-write-token.md · Implementation: + crates/praxis/praxis-core/src/belief.rs, crates/praxis/praxis-tools/src/belief.rs.

+

Origin: /loop runs 117 (khlo — capability), 118 (Cornelius-Trinity — scope), 119 (vina — revision). + The fourth dimension is what keeps bi-temporal stamps from being a mere playback device.

+
+
+ + diff --git a/docs/specs/bro-1030-belief-write-token.md b/docs/specs/bro-1030-belief-write-token.md new file mode 100644 index 00000000..e0a79ed7 --- /dev/null +++ b/docs/specs/bro-1030-belief-write-token.md @@ -0,0 +1,144 @@ +# BRO-1030 — `BeliefWriteToken`: four-dimensional belief formation context + +**Status:** implemented (praxis-core + praxis-tools) · **Crates:** `praxis-core::belief`, `praxis-tools::belief` + +A belief is not a bare proposition. The belief-contradiction problem — *silent +accumulation looking identical to deliberate updating* — is unsolvable without +observing **how a belief was formed**. This spec makes formation context a +first-class, typed write token with four dimensions. + +## The four dimensions + +| Dimension | Question answered | Field | Sourced from | +| -- | -- | -- | -- | +| Capability | *Who authorized this belief?* | `capability_id` | khlo — formation-context-as-write-time | +| Bi-temporal | *When in the world / when in the system?* | `timestamp: BiTemporalStamp` | bi-temporal stamps | +| Scope | *About what, precisely?* | `scope` + `scope_qualifier` | Cornelius-Trinity — beliefs carry their own scope conditions | +| **Revision** | ***What was superseded?*** | `revision_link` | **vina — the past self is a series of discarded drafts** | + +Without the fourth dimension, even bi-temporal stamps reduce to a *playback +device*: two snapshots with timestamps but no causal connection. A +contradiction **with** a revision link is *visible history* (a deliberate +update); a contradiction **without** one is a genuine failure of versioning. + +## Schema (`praxis-core::belief`) + +```rust +struct BeliefWriteToken { + capability_id: CapabilityId, + scope: BeliefScope, + scope_qualifier: ScopeQualifier, // BTreeMap + cited_evidence: Vec, + formation_context: SessionContext, // session + run + principal + revision_link: Option, // the fourth dimension + signed_by: AnimaDid, + timestamp: BiTemporalStamp, // { valid_from, recorded_at } +} + +struct RevisionLink { + superseded: ContentAddressedRef, // blake3 content hash + valid_from + triggered_by: Vec, + acknowledgment: BeliefRevisionAcknowledgment, +} + +struct BeliefRevisionAcknowledgment { + trigger: RevisionTrigger, // structured: NewEvidence | ScopeRefinement | ContextShift + change: RevisionChange, // structured: Negated | Qualified | Reweighted + rationale: String, // free-form addendum +} +``` + +The claim itself (`BeliefClaim { subject, proposition }`) is passed alongside +the token to `write_belief` — the token carries *authorization and provenance*, +the claim carries *content*. Content addressing hashes +`(scope, canonicalised scope_qualifier, subject, proposition)` with blake3. +Every variable-length field is **length-prefixed** (and the qualifier pair +count written explicitly), so distinct inputs can never alias to the same hash +— e.g. qualifier pairs `("a=b", "c")` and `("a", "b=c")`, which naive +`key=value\0` framing would collide, hash differently. + +## Write-path checks (`praxis-tools::belief::BeliefStore::write_belief`) + +Enforced in this order; each maps to a `BeliefWriteError` variant: + +1. **Capability presence** — empty `capability_id` ⇒ `MissingCapability`; an + unregistered id ⇒ `UnknownCapability`. +2. **Scope match** — the capability grant must authorize `token.scope` ⇒ else + `ScopeMismatch`. +3. **Bi-temporal completeness** — both `valid_from` and `recorded_at` set (not + the epoch sentinel) ⇒ else `IncompleteBiTemporalStamp`. +4. **Scope qualifier presence** — required for normative beliefs ⇒ else + `MissingScopeQualifier`. +5. **Evidence trace** — ≥ 1 cited evidence for normative beliefs ⇒ else + `MissingEvidence`. +6. **Revision link required, and it must target the live head** — if a **live** + belief for the same principal + coarse scope has a scope-qualifier Jaccard + overlap ≥ 0.5, the write **must** carry a `revision_link` ⇒ else + `MissingRevisionLink { existing_id, jaccard }`. When a link is supplied it + must target **exactly that live head** (identity by content hash + + `valid_from`); a link that points at a stale/superseded, cross-principal, or + otherwise non-head record ⇒ `RevisionMustTargetHead { expected_id }`. If more + than one live belief overlaps, the target is ambiguous ⇒ `AmbiguousOverlap` + (narrow the `scope_qualifier`). A link in a slot with no overlapping belief + whose target does not resolve ⇒ `RevisionTargetNotFound`. + +On success **only** the live head named by the revision link is stamped +`superseded_by`, so among the beliefs whose qualifier overlaps the new write +there is still exactly one **live** head. A belief with a disjoint qualifier is +a separate head in the same principal + scope and is left untouched, so the +slot as a whole may hold several live heads. Because the +target is resolved to the live head by index (not by a global hash lookup), a +write can never mutate another principal's record. + +## Two belief classes + +| Class | Surface | All 4 dimensions required? | Survives on | +| -- | -- | -- | -- | +| Untested-normative | Praxis principal (`write_belief`) | **yes** | capability + scope + revision-link consistency | +| Tested-operational | Vigil-observed (`record_operational`) | no | functional aliveness | + +**Migration** (`route_write`): a write carrying a formation token → Praxis +normative path; a legacy token-less write → Vigil operational surface +(tested-operational, no formation checks). New writes without a `revision_link` +on an overlapping scope are **rejected**, not silently accepted. + +## Revision-graph traversal + +`BeliefStore::traverse_revisions(belief_id, depth)` walks immediate-predecessor +links up to `depth` supersessions, returning `Vec` from the +live head back to older discarded drafts. Each entry carries the acknowledgment +that linked its successor to it. Multi-step chains are reconstructed by walking +(open question 3: each belief links only to its **immediate** predecessor). + +## Bookkeeping integration + +`revision_masks_contradiction(newer_token, older_ref)` is the gate: contradiction +detection fires **only** on Praxis writes *without* a revision link covering the +conflict. With a revision link pointing at the conflicting belief, the pair is +**visible history**, not a contradiction — bookkeeping treats it as a lineage +edge, not an alarm. + +## L2 metacognitive surface (Nous) + +`BeliefStore::recent_supersessions(principal, limit)` is the substrate +read-model behind the Nous L2 view *"what did I supersede recently, and why"*. +Each `SupersessionView` carries the superseding claim, the superseded reference, +the structured + free-form acknowledgment, and `recorded_at`. Praxis owns the +queryable substrate; the Nous daemon **projects** it as a metacognitive surface +(no praxis→nous dependency — Nous reads the read-model, consistent with how +autonomic/nous consult substrate through ports). + +## Resolved open questions + +1. **Acknowledgment granularity** — structured (`RevisionTrigger` + + `RevisionChange` enums) for queryability + a free-form `rationale` field. +2. **Revision vs `scope_qualifier`** — revision required only when qualifier + Jaccard overlap ≥ 0.5; disjoint qualifiers are *parallel* beliefs. +3. **Multi-step chains** — immediate predecessor only; chain reconstructed by + `traverse_revisions`. +4. **Cross-agent revision graphs** — composes with BRO-1029 (out of scope here). +5. **How L2 EGRI / Nous reads the graph** — via `recent_supersessions` / + `traverse_revisions` read-models (above). + +See `docs/specs/bro-1030-belief-write-token.html` for the visual decision matrix +and worked examples.