Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
2 changes: 2 additions & 0 deletions bert-compose/src/export.rs
Original file line number Diff line number Diff line change
Expand Up @@ -262,6 +262,8 @@ pub fn to_world_model(circuit: &Circuit, name: &str) -> WorldModel {

WorldModel {
version: 1,
// Absent ≡ Full; compose exports carry the dynamical face.
mode: None,
environment,
systems,
interactions,
Expand Down
96 changes: 96 additions & 0 deletions bert-core/src/lib.rs
Original file line number Diff line number Diff line change
Expand Up @@ -598,6 +598,15 @@ pub struct WorldModel {
/// Older versions trigger migration logic during deserialization.
pub version: u32,

/// Authoring mode along the kernel ladder (Core/Structural/Operational/Full).
///
/// Absent ≡ [`Mode::Full`], so files written before SL v2.0 deserialize and
/// re-serialize byte-for-byte unchanged. Read it through [`WorldModel::mode`],
/// never directly. A mode is the lens an author committed to, not a constraint
/// on the data: every model is a valid Core model regardless of this field.
#[serde(default, skip_serializing_if = "Option::is_none")]
pub mode: Option<Mode>,

/// Environmental context containing external entities and root system information.
///
/// The environment represents the broader context in which the system
Expand Down Expand Up @@ -625,6 +634,93 @@ pub struct WorldModel {
pub hidden_entities: Vec<Id>,
}

/// A rung on the kernel ladder: how much structure an author has committed to.
///
/// Each mode is a faithful view the K ≅ 2 kernel generates (proven in
/// `systems-science-foundations/Systems/Klir/ViewGeneration.lean`). The rungs are
/// *parallel lenses* over one kernel, not a cumulative tower: `Structural` (Bunge)
/// and `Operational` (Mobus) each impose their own precondition independently —
/// neither inherits the other's. They share only `Core`'s on-ness. `Full` extends
/// `Operational` with the dynamical face. See [`validate::validate_mode`].
/// `Cybernetic` is deliberately absent: feedback-as-first-class is still an open
/// question (no faithful finite acyclic comparison yet), so it is not a buildable
/// mode here. `Full` is the default and richest view.
#[derive(Serialize, Deserialize, Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum Mode {
/// Klir's (things, dependency) — the kernel itself. Precondition: on-ness only.
Core,
/// Bunge CES: a bond between two distinct components. Precondition: `HasBond`.
Structural,
/// Mobus's structural face: typed flow networks, no self-dependency. Precondition: irreflexivity.
Operational,
/// The dynamical face populated (transformation, history, time constant). Extends `Operational`.
Full,
}

/// The K ≅ 2 kernel projected out of a [`WorldModel`]: a system *is* a morphism,
/// so the kernel is its relata (`things`) and its dependency graph (`dep`).
///
/// This is the Rust twin of the Lean `Kernel` (ViewGeneration.lean). It is a
/// derived projection, never stored: [`WorldModel::kernel`] computes it on demand,
/// and the round trip through any mode view returns the same `(things, dep)`.
#[derive(Debug, Clone, PartialEq, Eq)]
pub struct Kernel {
/// T: the relata — every system, the environment node, and every external source and sink.
pub things: Vec<Id>,
/// R: the dependency relation — each interaction as a `(source, sink)` arrow, on `things`.
///
/// A multiset, not a set: BERT is a multigraph, so two distinct interactions
/// between the same endpoints (e.g. an energy flow and a material flow A→B)
/// are kept as parallel edges. Dedup at the consumer if set semantics are needed.
pub dep: Vec<(Id, Id)>,
}

impl WorldModel {
/// The committed authoring mode, resolving an absent field to [`Mode::Full`].
pub fn mode(&self) -> Mode {
self.mode.unwrap_or(Mode::Full)
}

/// Project the kernel: forget every elaboration, keep `(things, dep)`.
///
/// Mirrors Lean `Kernel.toKlir`. `things` enumerates every declarable
/// relatum: the environment node, its sources and sinks, then each system
/// with its local sources and sinks. This is exactly the endpoint set
/// [`validate::validate`]'s `check_interaction_references` accepts (minus
/// interfaces, which are ports, not relata), so the Core on-ness rule and
/// this projection agree by construction. `dep` is each interaction's
/// `(source, sink)`. Pure and total — the relata of a dangling interaction
/// simply may not appear in `things` (the on-ness rule
/// [`validate::validate_mode`] checks at `Core`).
pub fn kernel(&self) -> Kernel {
let mut things = Vec::new();
things.push(self.environment.info.id.clone());
for source in &self.environment.sources {
things.push(source.info.id.clone());
}
for sink in &self.environment.sinks {
things.push(sink.info.id.clone());
}
for system in &self.systems {
things.push(system.info.id.clone());
for source in &system.sources {
things.push(source.info.id.clone());
}
for sink in &system.sinks {
things.push(sink.info.id.clone());
}
}

let dep = self
.interactions
.iter()
.map(|ix| (ix.source.clone(), ix.sink.clone()))
.collect();

Kernel { things, dep }
}
}

/// Hierarchical identifier system for all entities in the BERT data model.
///
/// The `Id` structure provides a unique, hierarchical addressing scheme that encodes
Expand Down
Loading
Loading