Skip to content
Merged
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
4 changes: 3 additions & 1 deletion docs/proposals/boot-profiles.md
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
---
type: Design Decision
title: "Boot Profiles — substrate vs agent execution gate"
description: "yuva.profile=substrate|agent runtime gate (default agent) skips/denies cognitive organs; stage A landed, compile-out deferred to stage B."
description: "yuva.profile=substrate|agent runtime gate (default agent) skips/denies cognitive organs; stage A landed; stage-B compile-out of every main.rs organ block landed (PR-1..4), the PR-5 image-split product step stays operator-gated."
tags: ["boot-profiles", "substrate", "micro-vmm", "tcb", "agent-agnostic", "sovereignty"]
timestamp: 2026-07-08T02:31:19+03:00
status: active
Expand All @@ -14,6 +14,8 @@ diataxis: explanation

> **STAGE-B PROOF-OF-CONCEPT LANDED (2026-07-09) — ONE ORGAN.** The compile-out MECHANISM (§11, §1.4 rung 3) is now proven end-to-end for exactly ONE organ, WITHOUT touching the other ~18. A kernel-crate-local Cargo feature `agent-organs` (DEFAULT-ON → every existing build/CI invocation byte-identical, SP#4 safe by construction) gates the M26 exit-telemetry `main.rs` block — BOTH the agent path AND the runtime substrate-skip `else` arm — behind `#[cfg(feature = "agent-organs")]`; `tb-encode`/`tb-hal` are untouched (the `exittel` leaf becomes unreferenced + DCE-eligible; the marker literals live only in the gated kernel block, so their image absence is by construction). A NEW additive lane (`scripts/run-compileout-poc-x86_64.sh` + the `compileout-poc-boot` ci.yml job, x86_64-only, 90s ceiling) builds `--no-default-features` and boots it under `yuva.profile=substrate`, asserting M26 is **ABSENT-BY-OMISSION** from BOTH the serial stream (no marker, no skip form, no `exittel:` witness) AND the compiled ELF (strict anchored byte-search), while the profile-scoped core RAN to the `PROFILE: substrate OK` tail and the neighbors M25/M28 stayed built in the stage-A skip form — the honest side-by-side contrast of rung-2 (skip form) vs rung-3 (absent-by-omission). Witness `bprof-poc: organ=M26-EXITTEL organs=NOT-BUILT scope=ONE-ORGAN-ONLY` — NO `tcb=`/minimal/secure/reduced claim (the other organs are STILL BUILT). The three required verifiers + the substrate lane + the census are ZERO lines changed. **STILL OPEN (full stage B):** every remaining organ + a measured image-size delta remain the named successor — the `mem/` engine/organ factorization itself LANDED separately as **#80** (`crates/tb-hal/src/mem/` split into `engine.rs` [substrate-side store] / `organ.rs` [agent-side organs], zero behavior change, verified line-multiset-conserving); this PoC proves only the mechanism, and full stage B lands as one reviewed, operator-gated product decision (§12).

> **STAGE-B COMPILE-OUT — EVERY main.rs ORGAN BLOCK LANDED (2026-07-10..12, PR-1..4).** The PoC's mechanism scaled to the whole kernel crate in four reviewed, 2×-green, SP#4-byte-identical steps: **#85 (PR-1)** the M20 persist untangle — `persist_selftest` moved ONTO the engine, driving `VirtioBlkStore`/`BackingStore` directly, `persist:` witness byte-identical; **#86 (PR-2)** the 14 SELF-CONTAINED organs (M13, M16, M17, M18, M18.1, M18.2 with its co-gated helper fn, M21-M24, M26, M33, M39, M40) each got the PoC's `#[cfg(feature = "agent-organs")]` on the whole `if/else`, and the lane became the table-driven `scripts/run-compileout-x86_64.sh`; **#87 (PR-3)** the M28/M29 ASYMMETRIC split — the one site where whole-gating would be WRONG (§3.3: khash is substrate-core): the M28 organ arm gates out while the M29 khash KAT hoisted to a standalone block guarded by a dual-cfg `let`, so with the feature OFF the KAT is unconditional and can never fall through a runtime check into absence; **#88 (PR-4)** the PIPELINE cluster (M25, M30, M31 both legs, M32-local, M38) via a contiguous data-flow span audit — the cross-block bindings (`m31_fold`, `m31_chan`, the M31 leg-1 tuple, the M32 tuple) co-gated with their producers/consumers, M38 gated by its OUTER statement only (the SP#4-computing interior untouched). The lane now asserts **20 organ families ABSENT** from stream AND ELF with witness `bprof: organs-not-built=20 scope=MAIN-RS-ORGAN-BLOCKS pipeline-organs=NONE-REMAINING` — deliberately scoped: it does NOT claim "zero agent code in the image" (tb-hal/tb-encode organ code may be linker-kept). **REMAINING (PR-5, the §12 operator gate):** the image-split product decision — the full-compile-out lane promotion, llvm-nm/objdump symbol-absence + measured size-delta, the `profile.rs` wire-witness `organs=NOT-BUILT` flip, census regeneration, and the explicit design choice (recommended: kernel-only gate + linker-DCE + post-link symbol verification; the alternative tb-hal/tb-encode mirrored features is strictly more coupling for no Kani benefit).

---


Expand Down
Loading