From ad6e0974a93d2daf547eec53de8195621910853b Mon Sep 17 00:00:00 2001 From: kanon-vps Date: Fri, 17 Jul 2026 16:31:11 +0000 Subject: [PATCH 1/5] =?UTF-8?q?feat(praxis):=20BRO-1030=20four-dimensional?= =?UTF-8?q?=20BeliefWriteToken=20=E2=80=94=20capability=20+=20bi-temporal?= =?UTF-8?q?=20+=20scope=20+=20revision-link?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Formation context becomes a first-class, typed, content-addressed write token. The belief-contradiction problem (silent accumulation looking identical to deliberate updating) is unsolvable without observing HOW a belief was formed. Four dimensions: - capability_id — who authorized this belief (khlo, /loop 117) - timestamp: BiTemporalStamp — when in the world / when in the system - scope + scope_qualifier — about what, precisely (Cornelius-Trinity, /loop 118) - revision_link — what was superseded (vina, /loop 119; NEW fourth dimension) Without revision_link, bi-temporal stamps reduce to a playback device. With it, a contradiction becomes visible history rather than a versioning failure. praxis-core::belief (types): - BeliefWriteToken (spec-exact 8 fields), RevisionLink, BeliefRevisionAcknowledgment (structured RevisionTrigger + RevisionChange enums + free-form rationale), ScopeQualifier with Jaccard overlap (>=0.5 => same slot), ContentAddressedRef (blake3), BiTemporalStamp, CapabilityId, BeliefScope, AnimaDid, BeliefClass. praxis-tools::belief (runtime): - BeliefStore + write_belief: six write-path checks in order, new error class MissingRevisionLink when an overlapping live belief exists for the principal. - CapabilityGrant registry (scope-match check 2). - traverse_revisions(belief_id, depth): revision-graph chain (immediate- predecessor links, reconstructed by walking). - route_write + record_operational: normative (Praxis) vs tested-operational (Vigil) migration — token-less writes route to Vigil, unacknowledged overlapping writes are rejected. - recent_supersessions: substrate read-model behind the Nous L2 metacognitive surface ("what did I supersede recently, and why"). - revision_masks_contradiction: bookkeeping gate — a revision-linked contradiction is visible history, not an alarm. Docs: docs/specs/bro-1030-belief-write-token.{md (agent-read contract), html (P18 Category-C decision matrix + worked examples)}. Tests: praxis-core 40 (+10), praxis-tools 51 (+17). fmt + clippy -D warnings clean. Co-Authored-By: Claude Fable 5 --- Cargo.lock | 3 + crates/praxis/CLAUDE.md | 18 +- crates/praxis/praxis-core/Cargo.toml | 2 + crates/praxis/praxis-core/src/belief.rs | 733 +++++++++++++++ crates/praxis/praxis-core/src/lib.rs | 7 + crates/praxis/praxis-tools/Cargo.toml | 1 + crates/praxis/praxis-tools/src/belief.rs | 992 ++++++++++++++++++++ crates/praxis/praxis-tools/src/lib.rs | 7 + docs/specs/bro-1030-belief-write-token.html | 230 +++++ docs/specs/bro-1030-belief-write-token.md | 130 +++ 10 files changed, 2119 insertions(+), 4 deletions(-) create mode 100644 crates/praxis/praxis-core/src/belief.rs create mode 100644 crates/praxis/praxis-tools/src/belief.rs create mode 100644 docs/specs/bro-1030-belief-write-token.html create mode 100644 docs/specs/bro-1030-belief-write-token.md diff --git a/Cargo.lock b/Cargo.lock index 276e2784..bbafe32a 100644 --- a/Cargo.lock +++ b/Cargo.lock @@ -8252,6 +8252,8 @@ name = "praxis-core" version = "0.3.0" dependencies = [ "aios-protocol", + "blake3", + "chrono", "serde", "serde_json", "tempfile", @@ -8302,6 +8304,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..212d530b 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**: 141 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 (40 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 (51 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..eeac37bd --- /dev/null +++ b/crates/praxis/praxis-core/src/belief.rs @@ -0,0 +1,733 @@ +//! # 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 both stamps are past the Unix epoch sentinel — i.e. neither + /// was left at the zero/default value. + 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, + } + } +} + +/// Compute the Blake3 content hash of a belief's *semantic identity*: +/// coarse scope, canonicalised qualifiers, subject, and proposition. +/// +/// Two writes with identical content hash to the same value regardless of who +/// wrote them or when — that is what makes supersession referenceable. +pub fn content_hash( + scope: &BeliefScope, + qualifier: &ScopeQualifier, + claim: &BeliefClaim, +) -> String { + let mut hasher = Hasher::new(); + hasher.update(b"praxis.belief.v1\0"); + hasher.update(scope.as_str().as_bytes()); + hasher.update(b"\0scope_qualifier\0"); + // BTreeMap iterates in key order — canonical. + for (k, v) in &qualifier.qualifiers { + hasher.update(k.as_str().as_bytes()); + hasher.update(b"="); + hasher.update(v.as_str().as_bytes()); + hasher.update(b"\0"); + } + hasher.update(b"\0subject\0"); + hasher.update(claim.subject.as_bytes()); + hasher.update(b"\0proposition\0"); + hasher.update(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_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()); + } + + #[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..5590522d --- /dev/null +++ b/crates/praxis/praxis-tools/src/belief.rs @@ -0,0 +1,992 @@ +//! # 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 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 its predecessor, if this + /// record supersedes an earlier one. + 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 + }) + } + + /// The live (not-yet-superseded) belief for `principal` in the same coarse + /// `scope` whose qualifier overlaps `qualifier` at or above the Jaccard + /// threshold, plus the measured overlap. `None` when the slot is free. + fn find_overlapping( + &self, + principal: &AnimaDid, + scope: &BeliefScope, + qualifier: &ScopeQualifier, + ) -> Option<(&BeliefRecord, f64)> { + self.records + .iter() + .filter(|rec| rec.is_live()) + .filter(|rec| &rec.token.signed_by == principal) + .filter(|rec| &rec.token.scope == scope) + .map(|rec| (rec, rec.token.scope_qualifier.jaccard(qualifier))) + .filter(|(_, j)| *j >= ScopeQualifier::OVERLAP_THRESHOLD) + // Prefer the strongest overlap when several slots are close. + .max_by(|(_, a), (_, b)| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) + } + + /// 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. + let principal = token.signed_by.clone(); + let overlap = self + .find_overlapping(&principal, &token.scope, &token.scope_qualifier) + .map(|(rec, j)| (rec.id.clone(), j)); + + let superseded_index = match (&overlap, &token.revision_link) { + (Some((existing_id, jaccard)), None) => { + return Err(BeliefWriteError::MissingRevisionLink { + existing_id: existing_id.clone(), + jaccard: *jaccard, + }); + } + (_, Some(link)) => { + // A revision link — dangling or not — must point at a real + // belief, whether or not an overlap was detected. + let idx = self.resolve_index(&link.superseded).ok_or_else(|| { + BeliefWriteError::RevisionTargetNotFound { + hash: link.superseded.content_hash.clone(), + } + })?; + Some(idx) + } + (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(); + chain.push(RevisionChainEntry { + record: rec, + via: via.take(), + }); + if steps >= depth { + break; + } + match next_link { + Some(link) => { + via = Some(link.acknowledgment.clone()); + current = self.resolve(&link.superseded).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 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 { .. } + )); + } + + #[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:?}"), + } + } +} 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..0319ad3a --- /dev/null +++ b/docs/specs/bro-1030-belief-write-token.html @@ -0,0 +1,230 @@ + + + + + + +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
MissingRevisionLink / 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
yes, same principal + scope≥ 0.5 (overlap)absentreject MissingRevisionLink
yes, same principal + scope≥ 0.5 (overlap)present → live headaccept supersede, becomes visible history
anyanypresent → 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..a7c9431a --- /dev/null +++ b/docs/specs/bro-1030-belief-write-token.md @@ -0,0 +1,130 @@ +# 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. + +## 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 when applicable** — 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 }`. A revision link (dangling or + not) must resolve to a real stored belief ⇒ else `RevisionTargetNotFound`. + +On success the predecessor named by the revision link is stamped +`superseded_by`, so the slot has exactly one **live** head. + +## 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. From d22864a80e766537175cf2f0bb675a561ffe50f3 Mon Sep 17 00:00:00 2001 From: kanon-vps Date: Fri, 17 Jul 2026 17:21:18 +0000 Subject: [PATCH 2/5] fix(praxis): BRO-1030 harden belief write path per CodeRabbit review MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Two integrity fixes on the four-dimensional BeliefWriteToken write path, resolving the unresolved CodeRabbit review threads on PR #1785. 1. content_hash — unambiguous framing (Major). Variable-length fields were delimiter-framed (key=value\0), so ("a=b","c") and ("a","b=c") produced the same Blake3 input and thus the same belief identity. Now every field is length-prefixed and the qualifier pair count is written explicitly, so no distinct inputs can alias. Regression test added. 2. revision link must target the live overlapping head (Critical). The write path accepted any resolvable superseded ref, so a write could supersede an unrelated, stale (already-superseded), or cross-principal record while leaving the real conflicting live belief in place. Now: - live_overlapping_indices collects ALL live overlapping heads for the principal+scope; >1 => AmbiguousOverlap (narrow the scope). - with exactly one live head, a revision link MUST target that head by content ref (else RevisionMustTargetHead); the superseded record is resolved by index, never by a global hash lookup, so a write can never mutate another principal's record. - RevisionTargetNotFound retained for a dangling link in an empty slot. Tests added: stale/wrong-head, cross-principal, multi-head ambiguity. Also fixes the inverted doc on RevisionChainEntry.via (links to the SUCCESSOR that superseded the record, not its predecessor). Spec md + HTML decision matrix updated with the tightened check-5 semantics. Tests: praxis-core 41 (+1), praxis-tools 54 (+3). fmt + clippy -D warnings clean. Co-Authored-By: Claude Fable 5 --- crates/praxis/CLAUDE.md | 6 +- crates/praxis/praxis-core/src/belief.rs | 74 +++++- crates/praxis/praxis-tools/src/belief.rs | 269 +++++++++++++++++--- docs/specs/bro-1030-belief-write-token.html | 10 +- docs/specs/bro-1030-belief-write-token.md | 27 +- 5 files changed, 327 insertions(+), 59 deletions(-) diff --git a/crates/praxis/CLAUDE.md b/crates/praxis/CLAUDE.md index 212d530b..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-07-17 | **Status**: Active (Phase 4 — MCP server complete) -**Tests**: 141 passing | 5 crates | Rust 2024 Edition (MSRV 1.85) +**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,7 +24,7 @@ aios-protocol (Tool trait, ToolDefinition, ToolCall, ToolResult, ToolError) ## Crates -### praxis-core (40 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 @@ -34,7 +34,7 @@ aios-protocol (Tool trait, ToolDefinition, ToolCall, ToolResult, ToolError) `RevisionLink` + `BeliefRevisionAcknowledgment`, `ContentAddressedRef` (blake3), `AnimaDid`, `BeliefClass`. Formation context as a typed, content-addressed write token. -### praxis-tools (51 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 diff --git a/crates/praxis/praxis-core/src/belief.rs b/crates/praxis/praxis-core/src/belief.rs index eeac37bd..76b43db4 100644 --- a/crates/praxis/praxis-core/src/belief.rs +++ b/crates/praxis/praxis-core/src/belief.rs @@ -412,31 +412,48 @@ impl ContentAddressedRef { } } +/// 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 content hash to the same value regardless of who -/// wrote them or when — that is what makes supersession referenceable. +/// 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\0"); - hasher.update(scope.as_str().as_bytes()); - hasher.update(b"\0scope_qualifier\0"); + 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 { - hasher.update(k.as_str().as_bytes()); - hasher.update(b"="); - hasher.update(v.as_str().as_bytes()); - hasher.update(b"\0"); - } - hasher.update(b"\0subject\0"); - hasher.update(claim.subject.as_bytes()); - hasher.update(b"\0proposition\0"); - hasher.update(claim.proposition.as_bytes()); + 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() } @@ -684,6 +701,35 @@ mod tests { ); } + #[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"); diff --git a/crates/praxis/praxis-tools/src/belief.rs b/crates/praxis/praxis-tools/src/belief.rs index 5590522d..afb8e65b 100644 --- a/crates/praxis/praxis-tools/src/belief.rs +++ b/crates/praxis/praxis-tools/src/belief.rs @@ -140,6 +140,34 @@ pub enum BeliefWriteError { 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 \ @@ -183,8 +211,9 @@ pub fn revision_masks_contradiction(newer: &BeliefWriteToken, older: &ContentAdd pub struct RevisionChainEntry { /// The belief record at this link. pub record: BeliefRecord, - /// The acknowledgment that links this record to its predecessor, if this - /// record supersedes an earlier one. + /// 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, } @@ -253,24 +282,29 @@ impl BeliefStore { }) } - /// The live (not-yet-superseded) belief for `principal` in the same coarse - /// `scope` whose qualifier overlaps `qualifier` at or above the Jaccard - /// threshold, plus the measured overlap. `None` when the slot is free. - fn find_overlapping( + /// 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, - ) -> Option<(&BeliefRecord, f64)> { + ) -> Vec<(usize, f64)> { self.records .iter() - .filter(|rec| rec.is_live()) - .filter(|rec| &rec.token.signed_by == principal) - .filter(|rec| &rec.token.scope == scope) - .map(|rec| (rec, rec.token.scope_qualifier.jaccard(qualifier))) + .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) - // Prefer the strongest overlap when several slots are close. - .max_by(|(_, a), (_, b)| a.partial_cmp(b).unwrap_or(std::cmp::Ordering::Equal)) + .collect() } /// Write a normative belief through the four-dimensional token, enforcing @@ -318,29 +352,55 @@ impl BeliefStore { } // Check 5 — revision link required when an overlapping live belief - // already exists for this principal. + // 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 overlap = self - .find_overlapping(&principal, &token.scope, &token.scope_qualifier) - .map(|(rec, j)| (rec.id.clone(), j)); + 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 (&overlap, &token.revision_link) { - (Some((existing_id, jaccard)), None) => { + 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: existing_id.clone(), - jaccard: *jaccard, + existing_id: self.records[head_idx].id.clone(), + jaccard, }); } - (_, Some(link)) => { - // A revision link — dangling or not — must point at a real - // belief, whether or not an overlap was detected. - let idx = self.resolve_index(&link.superseded).ok_or_else(|| { - BeliefWriteError::RevisionTargetNotFound { - hash: link.superseded.content_hash.clone(), - } - })?; - Some(idx) + // 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, }; @@ -496,6 +556,10 @@ mod tests { 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( @@ -989,4 +1053,149 @@ mod tests { 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/docs/specs/bro-1030-belief-write-token.html b/docs/specs/bro-1030-belief-write-token.html index 0319ad3a..42731ed4 100644 --- a/docs/specs/bro-1030-belief-write-token.html +++ b/docs/specs/bro-1030-belief-write-token.html @@ -132,7 +132,7 @@

Write-path decision matrix

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
MissingRevisionLink / RevisionTargetNotFound
+
6 · Revision link
required on overlap ≥ 0.5; must target the live head
MissingRevisionLink / RevisionMustTargetHead / AmbiguousOverlap / RevisionTargetNotFound

Overlap → revision decision

@@ -141,9 +141,11 @@

Overlap → revision decision

none—absentaccept first assertion yes, same principal + scope< 0.5 (disjoint)absentaccept parallel belief - yes, same principal + scope≥ 0.5 (overlap)absentreject MissingRevisionLink - yes, same principal + scope≥ 0.5 (overlap)present → live headaccept supersede, becomes visible history - anyanypresent → non-existent targetreject RevisionTargetNotFound + 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 diff --git a/docs/specs/bro-1030-belief-write-token.md b/docs/specs/bro-1030-belief-write-token.md index a7c9431a..01fa0d0c 100644 --- a/docs/specs/bro-1030-belief-write-token.md +++ b/docs/specs/bro-1030-belief-write-token.md @@ -52,6 +52,10 @@ 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`) @@ -67,14 +71,21 @@ Enforced in this order; each maps to a `BeliefWriteError` variant: `MissingScopeQualifier`. 5. **Evidence trace** — ≥ 1 cited evidence for normative beliefs ⇒ else `MissingEvidence`. -6. **Revision link required when applicable** — 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 }`. A revision link (dangling or - not) must resolve to a real stored belief ⇒ else `RevisionTargetNotFound`. - -On success the predecessor named by the revision link is stamped -`superseded_by`, so the slot has exactly one **live** head. +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 the slot still has exactly one **live** head. 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 From 07e442d6b7f1ad075d34845a038e6501a51faa5a Mon Sep 17 00:00:00 2001 From: "Carlos D. Escobar-Valbuena" Date: Sun, 27 Sep 2026 01:59:37 -0500 Subject: [PATCH 3/5] fix(praxis): traverse revisions by back-pointer; a pre-1970 valid_from is complete Two review findings on #1785, both reproduced by new tests before the fix: - traverse_revisions resolved each link by (content_hash, valid_from) with first-match. content_hash is principal-agnostic by design and a revision may keep valid_from, so traversal could cross to another principal's record or skip a version. It now follows the superseded_by stamp the write path sets on exactly the record it superseded. Reverting fails 2 tests. - is_complete rejected every pre-epoch valid_from, not just the sentinel; valid_from is world time, so a 1965 belief is legitimate. Reverting fails 1. Co-Authored-By: Claude Opus 5.5 --- crates/praxis/praxis-core/src/belief.rs | 15 ++++- crates/praxis/praxis-tools/src/belief.rs | 80 +++++++++++++++++++++++- 2 files changed, 91 insertions(+), 4 deletions(-) diff --git a/crates/praxis/praxis-core/src/belief.rs b/crates/praxis/praxis-core/src/belief.rs index 76b43db4..a2fa6e0c 100644 --- a/crates/praxis/praxis-core/src/belief.rs +++ b/crates/praxis/praxis-core/src/belief.rs @@ -359,11 +359,16 @@ impl BiTemporalStamp { } } - /// True when both stamps are past the Unix epoch sentinel — i.e. neither - /// was left at the zero/default value. + /// 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 + self.valid_from != epoch && self.recorded_at > epoch } } @@ -743,6 +748,10 @@ mod tests { 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] diff --git a/crates/praxis/praxis-tools/src/belief.rs b/crates/praxis/praxis-tools/src/belief.rs index afb8e65b..e3958a1b 100644 --- a/crates/praxis/praxis-tools/src/belief.rs +++ b/crates/praxis/praxis-tools/src/belief.rs @@ -484,6 +484,7 @@ impl BeliefStore { 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(), @@ -494,7 +495,18 @@ impl BeliefStore { match next_link { Some(link) => { via = Some(link.acknowledgment.clone()); - current = self.resolve(&link.superseded).cloned(); + // 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, @@ -838,6 +850,72 @@ mod tests { )); } + 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(); From 1dce99782a7cc7c7d82ebb07b4c82ccd04f2e827 Mon Sep 17 00:00:00 2001 From: "Carlos D. Escobar-Valbuena" Date: Sun, 27 Sep 2026 02:15:44 -0500 Subject: [PATCH 4/5] style(praxis): rustfmt the new traversal tests Co-Authored-By: Claude Opus 5.5 --- crates/praxis/praxis-tools/src/belief.rs | 49 +++++++++++++++++++----- 1 file changed, 40 insertions(+), 9 deletions(-) diff --git a/crates/praxis/praxis-tools/src/belief.rs b/crates/praxis/praxis-tools/src/belief.rs index e3958a1b..55980337 100644 --- a/crates/praxis/praxis-tools/src/belief.rs +++ b/crates/praxis/praxis-tools/src/belief.rs @@ -851,7 +851,11 @@ mod tests { } fn ack(note: &str) -> BeliefRevisionAcknowledgment { - BeliefRevisionAcknowledgment::new(RevisionTrigger::NewEvidence, RevisionChange::Negated, note) + BeliefRevisionAcknowledgment::new( + RevisionTrigger::NewEvidence, + RevisionChange::Negated, + note, + ) } #[test] @@ -862,7 +866,10 @@ mod tests { 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)) + .write_belief( + BeliefClaim::new("market", "same"), + token(q(), None, 1000, 1000), + ) .unwrap(); let mut bt = token(q(), None, 1000, 1001); bt.signed_by = bob(); @@ -870,11 +877,19 @@ mod tests { 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"); + 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"))), + Some(RevisionLink::new( + bob_rec.as_ref(), + vec![EvidenceRef::source("e")], + ack("bob revises"), + )), 2000, 2000, ); @@ -886,7 +901,10 @@ mod tests { 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"); + assert_eq!( + chain[1].record.id, bob_rec.id, + "must not cross to Alice's record" + ); } #[test] @@ -896,16 +914,29 @@ mod tests { 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)) + .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"))) + 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)) + .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)) + .write_belief( + BeliefClaim::new("market", "x"), + token(q(), link(&v2), 1000, 3000), + ) .unwrap(); let ids: Vec<_> = store From ef1e95a940b42ca4f53c2f66b70213af1ad1b4be Mon Sep 17 00:00:00 2001 From: "Carlos D. Escobar-Valbuena" Date: Sun, 27 Sep 2026 02:45:49 -0500 Subject: [PATCH 5/5] docs(spec): one live head per overlapping set, not per slot Addresses review: disjoint qualifiers coexist as separate live heads in the same principal + coarse scope; a revision supersedes only its targeted head. Co-Authored-By: Claude Opus 5.5 --- docs/specs/bro-1030-belief-write-token.md | 5 ++++- 1 file changed, 4 insertions(+), 1 deletion(-) diff --git a/docs/specs/bro-1030-belief-write-token.md b/docs/specs/bro-1030-belief-write-token.md index 01fa0d0c..e0a79ed7 100644 --- a/docs/specs/bro-1030-belief-write-token.md +++ b/docs/specs/bro-1030-belief-write-token.md @@ -83,7 +83,10 @@ Enforced in this order; each maps to a `BeliefWriteError` variant: whose target does not resolve ⇒ `RevisionTargetNotFound`. On success **only** the live head named by the revision link is stamped -`superseded_by`, so the slot still has exactly one **live** head. Because the +`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.