uor-foundation 0.1.3

// @generated by uor-crate from uor-ontology — do not edit manually

//! `state/` namespace — Parameterized address spaces, context management, binding lifecycle, and state transitions. The user-space overlay onto the kernel's read-only ring substrate..
//!
//! Space: User

use crate::enums::SaturationPhase;
use crate::enums::SessionBoundaryType;
use crate::Primitives;

/// A bounded set of populated UOR addresses. The parameter space for a resolution cycle. Contexts hold bindings that map addresses to datum values.
/// Disjoint with: Binding, Frame, Transition.
pub trait Context<P: Primitives> {
    /// Associated type for `Binding`.
    type Binding: Binding<P>;
    /// A binding held in this context.
    fn binding(&self) -> &[Self::Binding];
    /// The maximum number of bindings this context can hold.
    fn capacity(&self) -> P::PositiveInteger;
    /// The content-derived address of this context, uniquely identifying its current state in the UOR address space.
    fn content_address(&self) -> &P::String;
    /// The quantum level of this context's address space.
    fn quantum(&self) -> P::PositiveInteger;
    /// The saturation degree σ ∈ \\[0, 1\\] of this context. Defined by SC_2: σ = (n − freeCount) / n.
    fn saturation_degree(&self) -> P::Decimal;
    /// The context temperature T_ctx ∈ \\[0, ln 2\\]. Defined by SC_1: T_ctx = freeCount × ln 2 / n. At σ = 1, T_ctx = 0.
    fn context_temperature(&self) -> P::Decimal;
    /// Whether this context has reached full saturation (σ = 1). Equivalent to freeCount = 0, S = 0, T_ctx = 0 per SC_4.
    fn is_saturated(&self) -> P::Boolean;
    /// The current saturation phase of this context: Unsaturated, PartialSaturation, or FullSaturation.
    fn saturation_phase(&self) -> SaturationPhase;
    /// The number of free (unbound) fibers remaining in this context. At saturation, residualFreeCount = 0.
    fn residual_free_count(&self) -> P::NonNegativeInteger;
}

/// The association of a datum value with an address in a context. The write primitive: creating a binding populates an address.
/// Disjoint with: Context, Frame, Transition.
pub trait Binding<P: Primitives> {
    /// Associated type for `Address`.
    type Address: crate::kernel::address::Address<P>;
    /// The UOR address being bound in this binding.
    fn address(&self) -> &Self::Address;
    /// Associated type for `Datum`.
    type Datum: crate::kernel::schema::Datum<P>;
    /// The datum value bound to the address in this binding.
    fn content(&self) -> &Self::Datum;
    /// Associated type for `TypeDefinition`.
    type TypeDefinition: crate::user::type_::TypeDefinition<P>;
    /// The type under which this binding's datum is resolved.
    fn bound_type(&self) -> &[Self::TypeDefinition];
    /// The time at which this binding was created.
    fn timestamp(&self) -> &P::String;
}

/// The visibility boundary determining which bindings are in scope for a given resolution. A frame is a view into a context: it selects which bindings the resolver sees.
/// Disjoint with: Context, Binding, Transition.
pub trait Frame<P: Primitives> {
    /// Associated type for `Binding`.
    type Binding: Binding<P>;
    /// The bindings currently in scope for this frame.
    fn active_bindings(&self) -> &[Self::Binding];
    /// Associated type for `Context`.
    type Context: Context<P>;
    /// The context this frame is a view of.
    fn context(&self) -> &Self::Context;
    /// Associated type for `Constraint`.
    type Constraint: crate::user::type_::Constraint<P>;
    /// The type:Constraint determining which bindings from the context are visible in this frame. The resolver applies this constraint to filter the context's binding set, producing the frame's active bindings. An absent constraint means all bindings are visible.
    fn constraint(&self) -> &Self::Constraint;
}

/// A state change: the transformation of one context into another through binding or unbinding. The sequence of transitions is the application's computation history.
/// Disjoint with: Context, Binding, Frame.
pub trait Transition<P: Primitives> {
    /// Associated type for `Context`.
    type Context: Context<P>;
    /// The context before this transition.
    fn from(&self) -> &Self::Context;
    /// The context after this transition.
    fn to(&self) -> &Self::Context;
    /// Associated type for `Binding`.
    type Binding: Binding<P>;
    /// Bindings added to the context in this transition.
    fn added_bindings(&self) -> &[Self::Binding];
    /// Bindings removed from the context in this transition.
    fn removed_bindings(&self) -> &[Self::Binding];
    /// Associated type for `ComputationTrace`.
    type ComputationTrace: crate::bridge::trace::ComputationTrace<P>;
    /// The computation trace recording the kernel operations that effected this state transition.
    fn trace(&self) -> &Self::ComputationTrace;
    /// Associated type for `TopologicalDelta`.
    type TopologicalDelta: crate::user::morphism::TopologicalDelta<P>;
    /// A snapshot of topological invariants at this transition point.
    fn topological_snapshot(&self) -> &Self::TopologicalDelta;
}

/// A bounded sequence of RelationQuery/response pairs sharing a common state:Context. Sessions are the unit of coherent multi-turn reasoning in Prism.
pub trait Session<P: Primitives> {
    /// Associated type for `Context`.
    type Context: Context<P>;
    /// The shared context holding all bindings accumulated across the queries in this session.
    fn session_bindings(&self) -> &Self::Context;
    /// The number of RelationQuery evaluations completed in this session.
    fn session_queries(&self) -> P::NonNegativeInteger;
}

/// The mutable accumulator that appends state:Binding instances to a state:Context as each RelationQuery resolves. Tracks monotonic reduction of aggregate free fiber space.
pub trait BindingAccumulator<P: Primitives> {
    /// Associated type for `FiberBudget`.
    type FiberBudget: crate::bridge::partition::FiberBudget<P>;
    /// The aggregate FiberBudget deficit across all accumulated bindings: the total remaining free fibers that have not yet been closed by resolution. Decreases monotonically as the session progresses.
    fn aggregate_fiber_deficit(&self) -> &Self::FiberBudget;
    /// Associated type for `Binding`.
    type Binding: Binding<P>;
    /// A binding accumulated by this accumulator from a resolved RelationQuery.
    fn accumulated_bindings(&self) -> &[Self::Binding];
}

/// Marks a context-reset event within a session stream. Records why the context was reset and provides a clean state:Context for subsequent queries.
pub trait SessionBoundary<P: Primitives> {
    /// A human-readable description of why this session boundary was triggered.
    fn boundary_reason(&self) -> &P::String;
    /// The typed reason category for this session boundary.
    fn boundary_type(&self) -> SessionBoundaryType;
    /// Associated type for `Context`.
    type Context: Context<P>;
    /// The state:Context that was active before this boundary reset.
    fn prior_context(&self) -> &Self::Context;
    /// The clean state:Context produced after this boundary reset, ready for subsequent queries.
    fn fresh_context(&self) -> &Self::Context;
}

/// A context that has reached full saturation: σ = 1, freeCount = 0, S = 0, T_ctx = 0 (SC_4). The ground state of the type system. All subsequent queries resolve in O(1) via SC_5.
pub trait SaturatedContext<P: Primitives>: Context<P> {
    /// Associated type for `SaturationCertificate`.
    type SaturationCertificate: crate::bridge::cert::SaturationCertificate<P>;
    /// The SaturationCertificate attesting that this context has reached full saturation.
    fn saturation_certificate(&self) -> &Self::SaturationCertificate;
}

/// Step-by-step evidence of the saturation process: records which bindings were applied, in what order, to reach full saturation.
pub trait SaturationWitness<P: Primitives> {
    /// Associated type for `Binding`.
    type Binding: Binding<P>;
    /// A binding that contributed to the saturation process, recorded in this SaturationWitness.
    fn witness_binding(&self) -> &[Self::Binding];
    /// The step index at which a particular binding was applied during the saturation process.
    fn witness_step(&self) -> P::NonNegativeInteger;
}

/// An informational/monitoring record tracking the saturation progress of a specific domain within a context. Carries no formal authority — purely observational.
pub trait DomainSaturationRecord<P: Primitives> {
    /// Associated type for `SaturatedContext`.
    type SaturatedContext: SaturatedContext<P>;
    /// The SaturatedContext that this DomainSaturationRecord monitors.
    fn saturated_context(&self) -> &Self::SaturatedContext;
    /// The domain within the context being tracked by this DomainSaturationRecord.
    fn saturated_domain(&self) -> &P::String;
    /// The number of free fibers remaining in the specific domain tracked by this DomainSaturationRecord.
    fn domain_free_count(&self) -> P::NonNegativeInteger;
}

/// A Context visible to more than one Session simultaneously. Holds a set of ContextLease instances that partition its fiber coordinates among active sessions. Lease disjointness (SR_9) prevents concurrent write conflicts.
pub trait SharedContext<P: Primitives>: Context<P> {
    /// Associated type for `ContextLease`.
    type ContextLease: ContextLease<P>;
    /// A currently active ContextLease on this SharedContext.
    fn lease_set(&self) -> &[Self::ContextLease];
}

/// A bounded, exclusive claim on a set of fiber coordinates within a SharedContext, held by exactly one Session. When the session closes or hits a SessionBoundary, the lease is released and its fibers become available for re-leasing.
/// Disjoint with: Context, Binding, Frame, Transition.
pub trait ContextLease<P: Primitives> {
    /// Associated type for `FiberBudget`.
    type FiberBudget: crate::bridge::partition::FiberBudget<P>;
    /// The subset of fibers claimed by this lease. Must be disjoint from all other active leases on the same SharedContext (SR_9).
    fn leased_fibers(&self) -> &Self::FiberBudget;
    /// Associated type for `Session`.
    type Session: Session<P>;
    /// The Session that holds this lease.
    fn lease_holder(&self) -> &Self::Session;
}

/// Records that a Session was formed by merging the binding sets of two or more predecessor sessions. Valid only if all predecessor binding sets pass the cross-session consistency check (SR_8). An invalid composition attempt produces a ContradictionBoundary on the target session.
pub trait SessionComposition<P: Primitives> {
    /// Associated type for `Session`.
    type Session: Session<P>;
    /// A predecessor session contributing bindings to this composition. Non-functional: one composition may merge two or more sessions.
    fn composed_from(&self) -> &[Self::Session];
    /// Whether all predecessor binding sets passed the SR_8 consistency check. If false, the composition is invalid and must not be used as a session context.
    fn composition_compatible(&self) -> P::Boolean;
    /// Associated type for `Context`.
    type Context: Context<P>;
    /// The merged Context produced by a valid composition. Only present when compositionCompatible = true.
    fn composition_result(&self) -> &Self::Context;
    /// Whether the LiftChain tower consistency check (SR_8 parametric extension) was performed across all Q_0 through Q_k levels. Required for compositions involving sessions at Q_1 or higher.
    fn tower_consistency_verified(&self) -> P::Boolean;
}

/// The caller explicitly requested a context reset. All accumulated bindings are discarded.
pub mod explicit_reset {}

/// The session resolver determined that no further queries can reduce the aggregate fiber deficit.
pub mod convergence_boundary {}

/// A new query produced a type contradiction with an accumulated binding. Context must reset before resolution can continue.
pub mod contradiction_boundary {}

/// The context has σ = 0: no bindings accumulated, all fibers are free. The initial phase of every session.
pub mod unsaturated {}

/// The context has 0 < σ < 1: some fibers are pinned by accumulated bindings, but free fibers remain. The accumulation phase.
pub mod partial_saturation {}

/// The context has σ = 1: all fibers are pinned, freeCount = 0. The ground state. All subsequent queries resolve in O(1) via SC_5.
pub mod full_saturation {}

/// The canonical ground-state witness: a SaturatedContext at σ = 1, freeCount = 0, T_ctx = 0, S = 0 (SC_4). Demonstrates that full saturation is achievable and O(1) resolution (SC_5) is realized.
pub mod ground_state {
    /// `contextTemperature`
    pub const CONTEXT_TEMPERATURE: &str = "0.0";
    /// `isSaturated`
    pub const IS_SATURATED: bool = true;
    /// `residualFreeCount`
    pub const RESIDUAL_FREE_COUNT: i64 = 0;
    /// `saturationDegree`
    pub const SATURATION_DEGREE: &str = "1.0";
    /// `saturationPhase` -> `FullSaturation`
    pub const SATURATION_PHASE: &str = "https://uor.foundation/state/FullSaturation";
}