feat(bert-core): kernel projection + mode ladder (bert#88 Parts 1-3)

[rsthornton]

What

The implementation half of bert#88 — re-founds the data model on the K≅2 kernel. The proof (ViewGeneration.lean, 6/11) and spec (system-language-spec-v2-addendum.md, 6/11) are now realized in Rust. Part 0 (the feature/bert-core merge) landed in #90; this is Parts 1–3.

Three additive pieces:

1. WorldModel::kernel() — projects the kernel (things, dep), the Rust twin of Lean Kernel.toKlir. Pure, derived, never stored (the cheap path the spec left open in A6.1).
2. Mode field (Core/Structural/Operational/Full) — absent ≡ Full, so pre-v2.0 files deserialize and re-serialize byte-identical; the save path emits no mode key. Read via WorldModel::mode().
3. validate_mode(model, target) — a mode-entry gate. Each view checks its own precondition: Structural = a bond between distinct components (Bunge Def 1.1), Operational = no self-loop (Mobus §4.3, the one new rule), Full = dynamical face (warns, since Full is the default view).

Design notes

• Modes are parallel lenses, not a cumulative tower. Structural (Bunge/HasBond) and Operational (Mobus/Irreflexive) impose independent preconditions and share only Core's on-ness — matching the parallel toBunge/toMobus projections in the proof. A single-component model with external flows is a valid Operational/Full model but legitimately not Structural.
• Validators gate mode entry, never modeling. validate() is untouched and stays universal (orphans/dangling-refs/duplicates are errors in every mode) → zero breakage for existing callers (BERT app, bert-typedb, GSR). validate_mode borrows immutably, so a lens-switching UI can ask "can this enter Operational?" as a pure query.

Scope

+413 / −0, additive across 5 files. No struct rewrites, no migration, no storage change.

Out of scope (to be filed): presentation/semantic split (A6.2), typing the dynamical face (A6.3), mode-transition UI + §3.8 loss warnings (§A5, Wednesday's lenses prototype), GSR cross-substrate agreement test, Cybernetic mode.

Tests

cargo test -p bert-core → 27 pass. New: mode-boundary fixtures (aggregate passes Core / fails Structural; self-loop passes Structural / fails Operational; independent-lenses), byte-stability, all example models enter Full, kernel projection, read-only round-trip invariant.

Notes for reviewer

• Builds: bert-core, bert, bert-compose all cargo check clean. bert-tauri/bert-typedb fail to compile on a clean checkout due to the pre-existing parked typedb-driver 3.11.5 WIP (unrelated to this PR).
• Pre-existing clippy warning items_after_test_module at lib.rs:1844 (surfaces only under --all-targets) is untouched by this PR.

Refs bert#88 · proof: systems-science-foundations/Systems/Klir/ViewGeneration.lean

🤖 Generated with Claude Code

[claude]

Code Review

Overview: Additive PR (413 lines, 0 deletions) that realizes the K≅2 kernel spec in Rust across three pieces: WorldModel::kernel(), the Mode enum + field, and validate_mode. The design is clean and the backwards-compatibility story (absent ≡ Full, byte-stable serialization) is solid.

---

Strengths

• Purely additive. No struct rewrites, no migration path, zero risk of breaking existing callers (bert, bert-typedb, GSR all pass because validate() is untouched).
• Byte-stable serialization. #[serde(default, skip_serializing_if = "Option::is_none")] is exactly the right tool for this; the absent_mode_is_full_and_byte_stable test pin-points the invariant.
• validate_mode borrows immutably. This makes the mode-entry check a pure query, which is the right design for a future lens-switching UI.
• Test coverage is thorough. The independent-lenses test (structural_and_operational_are_independent_lenses) is particularly valuable — it encodes the parallel-not-tower invariant as a regression test. all_example_models_enter_full_mode gives real-world coverage for free.

---

Issues

1. serialize_id used for equality — should be == / != (minor, correctness-adjacent)

In check_bond and check_self_loops, ID identity is compared via:

serialize_id(&ix.source) != serialize_id(&ix.sink)   // check_bond
serialize_id(&ix.source) == serialize_id(&ix.sink)   // check_self_loops

Id derives PartialEq, Eq, and Hash (lib.rs:780), so this can and should be:

ix.source != ix.sink
ix.source == ix.sink

serialize_id was introduced elsewhere to key a HashSet<String> because it turns Id into a normalized string for set membership. Using it for a two-value equality check is both slower (serde round-trip per comparison, per interaction) and opaque to the reader. The existing code also means a hypothetical future change to the Id serialization format could silently change equality semantics here without touching the type.

2. kernel().things silently omits the environment node itself

WorldModel::kernel() collects systems, then environment.sources, then environment.sinks, then per-system sources and sinks. It never pushes self.environment.info.id. The docstring says "every system plus every external source and sink", which matches the code — but "external entity" in the BERT model usually refers to the Environment composite and its children.

This may be intentional per the Lean proof (only relata that appear as interaction endpoints are "on things"), but it is worth a comment or an assertion in the kernel projection test to make the invariant explicit. If an interaction targets the environment node directly (not one of its sources/sinks), that endpoint would not appear in things, and validate_mode(Mode::Core) would catch it via the existing check_interaction_references path — but the omission is currently undocumented.

3. check_dynamical_face warns on systems, not the root model

The warning says "Full mode shows the dynamical face, but '{name}' has no transformation, history, or time constant". This iterates model.systems, which includes every system at every nesting level. For deeply nested models that have the dynamical face populated at S0 but not at leaf subsystems, this will produce a warning per leaf. Is that the intended granularity? If the intent is "the model hasn't used the Full-mode slots at all", a model-level check (any system has a face) would be less noisy than a per-system check.

---

Nits

• is_system matches IdType::System | IdType::Subsystem. If a Processor or Composite variant is added to IdType later, this silently misclassifies it as "not a system component". Worth a #[non_exhaustive] note or at minimum a comment that this list must stay in sync with IdType.
• The mode_views_are_read_only_kernel_invariant test is correct but the comment ("enforced, not asserted") slightly overstates it — the Rust borrow checker enforces that validate_mode cannot mutate the model, but it doesn't prevent validate_mode from returning a result that causes a caller to mutate the model. The invariant is that validate_mode itself is read-only, which is true and compiler-enforced. Minor wording thing.
• cargo clippy --all-targets -- -D warnings is in CLAUDE.md's quality gates. The PR notes a pre-existing items_after_test_module warning at lib.rs:1844. Worth filing a follow-up rather than leaving it open indefinitely.

---

Summary

The design is sound and the implementation is clean. The one change I'd ask for before merging is replacing serialize_id comparisons with direct ==/!= in check_bond and check_self_loops — it's the idiomatic Rust approach and removes a subtle fragility. The kernel omission (#2) and dynamical-face granularity (#3) are worth a discussion comment or follow-up issue, but neither is a blocker.

27 tests passing, additive-only, backwards-compatible — good to go once the serialize_id nit is addressed.

[rsthornton]

Addressed the review in a4a3f31:

• serialize_id → ==/!= (Issue 1): done. Id: Eq, so direct comparison in check_bond/check_self_loops — no serde round-trip, clearer intent.
• kernel() omitted the environment node (Issue 2): fixed as a real consistency bug, not just docs. check_interaction_references accepts E-1 as an endpoint, so kernel().things now includes it — the Core on-ness rule and the projection agree by construction. Test asserts the env node is present.
• Per-leaf dynamical warnings (Issue 3): check_dynamical_face is now a single model-level warning (no system has a face) instead of one-per-leaf. Same signal, far less UI noise for the lens prototype.
• Nits: added an is_system/IdType-sync note, tightened the read-only test comment (the immutable borrow is the guarantee; the test pins the invariant), and filed the pre-existing items_after_test_module clippy warning as clippy: make the workspace pass --all-targets -D warnings #94 rather than touching unrelated code here.

27 tests still pass; clippy --all-targets clean except the pre-existing #94.

[claude]

Code Review: feat(bert-core): kernel projection + mode ladder (bert#88 Parts 1-3)

Overview

This PR introduces three additive pieces atop the feature/bert-core base: the Mode enum (Core/Structural/Operational/Full), the WorldModel::kernel() projection, and the validate_mode gate. The design is well-reasoned, the backward-compat story is solid, and the test suite is meaningfully structured. A few things worth looking at before merge.

---

Potential Bug: check_bond misses interface-mediated bonds

// bert-core/src/validate.rs
fn is_system(id: &Id) -> bool {
    matches!(id.ty, IdType::System | IdType::Subsystem)
}

fn check_bond(model: &WorldModel, issues: &mut Vec<ValidationIssue>) {
    let bonded = model
        .interactions
        .iter()
        .any(|ix| is_system(&ix.source) && is_system(&ix.sink) && ix.source != ix.sink);
    ...
}

Interaction.source and .sink can carry IdType::Interface endpoints (the struct accepts any Id). A model where two distinct systems are connected through their interfaces (source has IdType::Interface, sink has IdType::Interface) will fail check_bond and be blocked from Structural mode even though a bond clearly exists between distinct components. This could be a real scenario in practice.

Suggestion: Either extend is_system to also accept IdType::Interface (and verify the interface belongs to a different parent), or document a hard invariant that direct system-to-system Id assignment is the only valid encoding and enforce it elsewhere. At minimum, add a test that exercises interface-mediated interactions.

---

Missing test: kernel() with environment sources/sinks

The kernel_projects_things_and_dependencies test uses two_component_model(), which has no environment sources or sinks. The kernel doc says those are included in things, but there is no test verifying this path:

for source in &self.environment.sources {
    things.push(source.info.id.clone());
}
for sink in &self.environment.sinks {
    things.push(sink.info.id.clone());
}

Suggestion: Add a fixture with at least one environment source and one sink, and assert they appear in k.things.

---

Trivially-true test

mode_views_are_read_only_kernel_invariant cannot ever fail: validate_mode takes &WorldModel, so the compiler already proves immutability. The assertion before == after is always true by construction.

Fine to keep as documentation of intent, but worth noting so future readers do not treat it as a meaningful runtime guard.

---

Minor: redundant validate() cost when checking multiple modes

validate_mode calls validate(model) first on every invocation. A UI building a mode-availability matrix runs the universal pass once per mode even though the output is identical every time.

Suggestion (non-blocking): expose a validate_mode_only(model, target) that skips the universal pass, letting callers compose: run validate(model) once and extend with mode-specific results. Not urgent for the current use case.

---

Nit: is_system sync requirement is unenforceable

The comment "Keep this in sync with IdType" is a manual contract. An exhaustive match would make the compiler enforce it:

fn is_system(id: &Id) -> bool {
    match id.ty {
        IdType::System | IdType::Subsystem => true,
        IdType::Interface | IdType::Source | IdType::Sink
        | IdType::Environment | IdType::Flow | IdType::Boundary => false,
    }
}

A future IdType variant then becomes a compile error rather than a silent omission.

---

What is done well

• Byte-stability: #[serde(default, skip_serializing_if = "Option::is_none")] is exactly right; absent_mode_is_full_and_byte_stable pins it precisely.
• Pure immutable kernel projection: never stored, computed on demand, impossible to mutate through mode viewing — matches the Lean proof structure cleanly.
• Independent-lenses test: structural_and_operational_are_independent_lenses explicitly exercises the non-inheritance property the design section argues for.
• All-examples gate: all_example_models_enter_full_mode is an excellent regression guard.
• +413/-0: additive-only keeps blast radius at zero for all existing callers.

---

Summary

The main items before merge are the check_bond interface-mediated case (correctness question depending on whether the app generates interface-endpoint interactions) and the missing kernel test with environment entities. Everything else is non-blocking polish.

🤖 Generated with Claude Code

[rsthornton]

Round 2 addressed in latest push:

• check_bond / interface-mediated bonds — not a bug (verified, not assumed). Checked all example models: source/sink carry only System/Subsystem/Source/Sink Ids — never Interface. The interface lives in the separate source_interface/sink_interface field (per the struct contract). So a bond through interfaces is encoded as source = System, sink = System, and check_bond recognizes it. Added interface_mediated_bond_enters_structural to lock the invariant against regression.
• Missing kernel env-externals test: added kernel_includes_environment_externals exercising the environment.sources/sinks branch.
• is_system sync (nit): now an exhaustive IdType match — a new variant is a compile error, not a silent omission.
• Trivially-true read-only test: agreed — kept as intent documentation; the comment already says the immutable borrow is the compiler guarantee and the test pins the invariant.
• Redundant validate() per mode (non-blocking): filed as validate_mode: factor out validate_mode_only() for the lens-availability matrix #95 — expose validate_mode_only() when Wednesday's lens-availability matrix gives it a real caller.

29 tests pass; clippy --all-targets clean except the pre-existing #94.

[claude]

Code Review — feat(bert-core): kernel projection + mode ladder (bert#88 Parts 1-3)

Overview

Additive, well-scoped PR (+532/−0) that re-founds the data model on the K≅2 kernel from the Lean proof. Three independent pieces land together: WorldModel::kernel(), the Mode enum with serde round-trip stability, and validate_mode() as a pure immutable gate. The design decision to treat modes as parallel lenses rather than a cumulative tower is clearly motivated and correctly implemented.

---

What's Working Well

• Exhaustive is_system() match — using match over IdType instead of a wildcard arm means new IdType variants become a compile error rather than a silent misclassification. This is the right pattern for a safety-critical classifier.
• skip_serializing_if = "Option::is_none" for byte-stability — backward-compat round-trips are pinned by absent_mode_is_full_and_byte_stable. The test is a good regression anchor.
• Immutable borrow in validate_mode — the compiler enforces the read-only contract; the round-trip test in mode_views_are_read_only_kernel_invariant then pins the semantic invariant. Belt and suspenders.
• Test breadth — 10 targeted scenarios including the independent-lenses property, interface-mediated bond, and environment-external sources/sinks. The positive/negative pairing (e.g. aggregate_enters_core_but_not_structural / a_bond_enters_structural) is clean.

---

Issues

Minor — Missing test for check_dynamical_face warning path

check_dynamical_face emits a Warning (not an error) when no system has any dynamical-face fields populated. This is user-visible in the UI, but there is no test that exercises it. all_example_models_enter_full_mode only asserts !has_errors(), so a silently regressed warning would go undetected.

Suggested addition:

#[test]
fn empty_dynamical_face_warns_in_full_mode() {
    let m = two_component_model(); // no transformation/history/time_constant
    let r = validate_mode(&m, Mode::Full);
    assert!(!r.has_errors(), "missing dynamical face is a warning, not an error");
    assert!(
        r.has_warnings(),
        "Full mode should warn when no dynamical face is populated"
    );
    assert!(
        r.issues.iter().any(|i| i.message.contains("dynamical face")),
        "got: {:#?}", r.issues
    );
}

Nit — Mode missing Hash

Copy + Eq without Hash is an unusual combination in Rust — the standard library derives them together for a reason. Any caller that wants to use Mode as a HashMap key or in a HashSet will hit a compile error, and adding Hash later is a breaking change in some derives. Consider adding it now while the enum is new:

#[derive(Serialize, Deserialize, Clone, Copy, Debug, PartialEq, Eq, Hash)]
pub enum Mode { … }

Nit — read_dir bare .unwrap() in all_example_models_enter_full_mode

for entry in std::fs::read_dir(&dir).unwrap() {

A missing examples directory produces a generic panic. .expect("open examples dir") gives a much clearer failure message — especially useful in CI where the path may not match expectations.

Nit — kernel() makes two passes over self.systems

The function iterates self.systems once to collect system IDs, then again to collect per-system sources/sinks. A single pass would be equivalent and slightly cleaner:

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 }
}

This also puts the environment node first (relata naturally "include" the context), though ordering is currently unspecified.

---

Questions / Future Consideration

• dep can contain duplicate edges if the model has duplicate interactions. validate() catches duplicate IDs, but two interactions with the same source/sink but different IDs would produce duplicate pairs in dep. Worth documenting if Kernel consumers need a set-semantic dep relation.
• Cybernetic mode note in docs — the doc comment on Mode says cybernetic "is not a buildable mode here." Is there a tracking issue for this? A todo!/// TODO(bert#???) reference in the doc would help future contributors connect the dots.

---

Summary

The core logic is correct, the design is well-motivated, and the tests are genuinely useful. The one item worth addressing before merge is the missing warning test for check_dynamical_face — that path is user-visible and currently has zero coverage. The rest are nits.

[rsthornton]

Round 3 addressed:

• Missing check_dynamical_face warning test: added empty_dynamical_face_warns_in_full_mode. Note: the suggested snippet would have passed-then-failed — two_component_model() includes S0 with the default time_constant: "Second", so any_face is true and no warning fires. The test clears S0's time_constant first so no system has a face, asserts the warning, then restores it and asserts the warning clears.
• Mode missing Hash: added — Wednesday's mode-availability matrix may key by Mode.
• kernel() two passes: collapsed to a single pass over self.systems, environment node first. things is an unordered bag, so behavior-equivalent.
• dep duplicates: documented as intentional — dep is a multiset because BERT is a multigraph (an energy flow and a material flow A→B are distinct edges). Consumers dedup if they want set semantics.
• read_dir().unwrap(): .expect("open examples dir") on mine.
• Cybernetic tracking: the doc already explains why it is unbuildable (no faithful finite acyclic comparison yet); it is tracked as an SSF open question, not a code TODO, so no issue ref added.

30 tests pass; clippy --all-targets clean except pre-existing #94. Calling this the last polish round — merging rather than feeding the synchronize trigger another pass.

[claude]

Code Review — feat(bert-core): kernel projection + mode ladder (bert#88 Parts 1–3)

Overall this is a well-scoped, thoughtful PR. The design decisions are clearly articulated and match the systems-science intent. Below are specific findings ordered by severity.

---

Issues worth discussing

1. validate_mode always runs the full validate() — double-work for callers who already hold a ValidationResult

validate_mode unconditionally runs the universal validate() pass every time it's called. If a lens-switching UI asks "can this enter Operational? Structural? Core?" in rapid succession, it pays the full O(n) structural scan three times.

Consider accepting a pre-computed result or splitting into two functions:

pub fn validate_mode_from(base: ValidationResult, model: &WorldModel, target: Mode) -> ValidationResult
pub fn validate_mode(model: &WorldModel, target: Mode) -> ValidationResult {
    validate_mode_from(validate(model), model, target)
}

This keeps the ergonomic single-call API while letting callers amortize the base scan. Out-of-scope if the UI won't hot-path this, but worth noting.

2. mode field is pub despite the doc saying "never access directly"

lib.rs:608:

pub mode: Option<Mode>,

The doc comment says "Read it through WorldModel::mode(), never directly," but pub gives any downstream crate direct write access too. Since the field intentionally controls the serialization sentinel, accidental direct writes (e.g. model.mode = Some(Mode::Full) instead of None) would silently break the byte-stability guarantee.

Options: pub(crate) if no outside crates need it; otherwise keep pub but note this explicitly in the field-level doc.

3. kernel().things can contain duplicates if validate() hasn't been called first

The kernel() doc says:

"the relata of a dangling interaction simply may not appear in things"

But the inverse — a duplicate ID from two systems colliding — is only prevented if the caller ran validate() first (which catches it via check_duplicate_ids). The dep multiset comment is clear, but things has no analogous disclaimer. Worth a one-liner:

/// Duplicates are possible when the model has not been validated; call [`validate`] first
/// or dedup at the consumer if set semantics are needed.
pub things: Vec<Id>,

---

Minor observations

4. mode_views_are_read_only_kernel_invariant is a no-op test

validate_mode takes &WorldModel, so the compiler already guarantees immutability. The test can't observe anything the type system doesn't prevent. The comment acknowledges this ("the compiler already guarantees it"), so this is a documentation test rather than a correctness test — which is fine, but it's worth being explicit that this is intentional pinning rather than a runtime check.

5. check_dynamical_face uses .trim().is_empty() — minor style inconsistency

If transformation/history/time_constant are always stored pre-trimmed (which is the common pattern for UI-sourced strings in this codebase), .is_empty() is cheaper and clearer. If not, .trim().is_empty() is correct but worth a comment explaining the choice. Low priority.

6. Mode derives Hash — unnecessary for current use cases

Hash isn't needed to put a Mode in a HashMap or BTreeMap anywhere in this diff. It won't cause problems but adds a derived bound that future refactors need to be aware of. PartialEq + Eq + Copy + Clone + Debug is the practical minimum here.

---

What's done well

• The exhaustive match in is_system() is exactly right — a new IdType variant forces the author to classify it explicitly.
• #[serde(default, skip_serializing_if = "Option::is_none")] is the cleanest possible approach for the backward-compat requirement; the byte-stability test pins it.
• Mode validator ordering (validate() first, then mode checks) means universal errors always surface before mode-specific ones — no accidental false-positive mode passes on a broken model.
• validate_mode(model, Mode::Core) being equivalent to validate(model) is logically consistent with the spec and is clearly documented.
• Test coverage is comprehensive for a +413/-0 PR: boundary fixtures, byte stability, round-trip invariant, full example models suite.

---

Out-of-scope note

The PR description notes bert-tauri/bert-typedb fail to compile due to the pre-existing typedb-driver WIP — worth tracking in a separate issue to keep CI signals reliable.

🤖 Generated with Claude Code

[rsthornton]

Round 4 triaged — merging.

• Double-work / validate_mode_from (1): already tracked in validate_mode: factor out validate_mode_only() for the lens-availability matrix #95.
• pub mode sentinel + things dedup doc (2, 3): filed as bert#88 polish: protect the mode byte-stability sentinel + document kernel().things dedup #97. pub(crate) isn't viable (the bert/bert-compose crates build WorldModel via struct literal), so this wants a constructor/typestate — out of scope for this additive PR.
• bert-tauri/bert-typedb workspace build (out-of-scope note): filed as bert-tauri/bert-typedb don't compile against typedb-driver 3.11.5 (workspace build + release path) #96 — the pre-existing typedb-driver 3.11.5 WIP; blocks release.yml.
• No-op read-only test (4): intentional documentation test, as the comment states.
• Mode: Hash (6): keeping it — this is the direct opposite of round 3, which asked me to add it. It's harmless and Wednesday's mode matrix may key on it. The flip-flop is the signal the review has converged to noise, so I'm stopping the round-on-every-push loop here.

Everything actionable is resolved or filed (#93, #94, #95, #96, #97). 30 tests pass, clippy clean except pre-existing #94. Thanks for the reviews — rounds 1 and 3 caught real things.