diff --git a/.gitignore b/.gitignore index 2a79f827..e17e9e39 100644 --- a/.gitignore +++ b/.gitignore @@ -61,3 +61,6 @@ MODULE.bazel.lock /simple.wat /minimal.wat /file_ops_component.wat + +# Rivet external project cache +.rivet/repos/ diff --git a/rivet.yaml b/rivet.yaml index 2d271d24..8b032520 100644 --- a/rivet.yaml +++ b/rivet.yaml @@ -74,8 +74,30 @@ externals: ref: main prefix: gale + gust: + # gust artifacts live in the gale repo (gale-gust is a gale checkout); distinct + # prefix for the OS/gust artifact set. + git: https://github.com/pulseengine/gale.git + path: /Volumes/Home/git/pulseengine/gale-gust + ref: main + prefix: gust + + loom: + git: https://github.com/pulseengine/loom.git + path: /Volumes/Home/git/pulseengine/loom + ref: main + prefix: loom + sigil: git: https://github.com/pulseengine/sigil.git path: /Volumes/Home/git/pulseengine/sigil ref: main prefix: sigil + + scry: + # Sound abstract interpretation for WebAssembly (DO-333 leg). Provides the + # worst-case shadow-stack / longest-path bounds that answer the hard half of + # "how much memory an arbitrary wasm can consume" (AD-WCMC-001). + git: https://github.com/pulseengine/scry.git + ref: main + prefix: scry diff --git a/safety/requirements/architecture-decisions.yaml b/safety/requirements/architecture-decisions.yaml index 9e8b28e7..9a789781 100644 --- a/safety/requirements/architecture-decisions.yaml +++ b/safety/requirements/architecture-decisions.yaml @@ -68,6 +68,94 @@ artifacts: previous-id: ARCH_DEC_DEPLOY_001 implementation: kiln-platform/src/ + - id: AD-NOSTD-INTERP-001 + type: design-decision + title: Hybrid embedded execution — a no_std interpreter mode alongside synth-AOT, deployed AS a wasm module via synth (amends RFC #46) + description: > + Kiln shall provide a no_std/no_alloc deployment of its WebAssembly + interpreter for on-board embedded execution (gale/gust), IN ADDITION TO the + synth-AOT native path — not instead of it — as the alternative for payloads + where AOT is not wanted or wished (dynamic / late-loaded modules, migrated + instances, untrusted code, or cert contexts that prefer an interpreter's + smaller TCB over a compiler's). + DEPLOYMENT MECHANISM (the elegant part): kiln itself (no_std/no_alloc) is + compiled TO a wasm module, and synth AOT-compiles THAT to native for the + target — the SAME pipeline as user code. So wasm is the universal IR, synth + is the single compiler in the TCB, and kiln-as-wasm is itself + verifiable/attestable (witness MC/DC on the kiln wasm, scry invariants, + sigil) like any other module — no separate no_std-Rust→native toolchain is + needed. The synth-compiled kiln then loads and interprets wasm on-board. + UNIQUE DIFFERENTIATOR: this on-board interpreter runs the FULL Component + Model (kiln's direct runtime hosting per AD-COMPONENT-HOST-001) — or plain + core wasm — whereas the safety-critical peers (spacewasm, DLR-FT) are + core-module-only. It EXTENDS AD-COMPONENT-HOST-001's direct-hosting path + from QM/std-reference-only to the embedded target, so embedded gets a + runtime-Component-Model option alongside meld-dissolve-to-core. meld + (build-time lowering) and synth (AOT hot path) are retained. + TIERED TCB (resolves the interpreter-vs-compiler-TCB tension): ship two + tiers, not one monolith — (i) a CORE-ONLY minimal interpreter with a small + auditable TCB that competes with spacewasm/DLR-FT on their own terms (and + beats them on verification evidence), and (ii) an OPT-IN Component-Model + layer (the differentiator, ~31k LOC) enabled only where the TCB budget and + cert context allow. This keeps the "smaller TCB than a compiler" claim and + the "Component Model on-board" claim from fighting each other — chosen per + deployment. + status: proposed + tags: [architecture, embedded, no-std, interpreter, deployment, rfc46-amendment] + links: + - type: satisfies + target: REQ_NOSTD_INTERP + - type: satisfies + target: REQ_FUNC_002 + fields: + rationale: > + Peer comparison (#413): NASA spacewasm and DLR-FT interpret ON-BOARD with + no AOT; DLR states they chose an interpreter because a compiler defies + DO-178C/DO-332 design principles. Putting synth (a compiler) in the + embedded cert TCB is a materially harder cert story than an interpreter — + the incumbents avoided it deliberately. Kiln already has the ingredients + (capability-bounded memory + per-instruction fuel; kiln-runtime is + categorized no-std with a std feature and a no-op no_std stub); the no_std + gate is a choice. Measured std-dependence is localized and portable: + ~90 Mutex/RwLock/thread hits (→ kiln-sync), ~55 std:: hits (→ alloc + collections), only ~5 std::fs/io (→ platform callbacks). A focused port, + not a rewrite; target shape is DLR-FT's "in-place, almost no deps". + Amends RFC #46 ("there is no no_std interpreter"; embedded = synth-AOT + only) — requires an RFC #46 doc update + BA sign-off, and touches + meld/synth positioning and gale/gust (new on-board target + live + migration). Also reconciles the record: REQ_FUNC_002 (baremetal) and + REQ_FUNC_033 (kilnd-nostd) are marked implemented but the no_std + interpreter is not actually delivered today; this decision is the path to + making those claims true. Direction chosen by the maintainer 2026-07-11 + (hybrid over stay-course / migration-only). + cross-repo-gale: > + Imposes a GALE (OS) requirement: gale must (a) load and run the + synth-compiled kiln image, and (b) support RUNTIME wasm loading on-target + (dynamic module/component load, since on-board interpretation means + loading payloads at runtime, not just at build). File a gale-side + requirement + confirm the loader/OS-service surface before Phase 3. + precedent: > + The no_std/no_alloc embedded deployment is NOT speculative — kiln-async + (REQ_ASYNC_SCHED) already proves it: it is no_std/no_alloc, forbid(unsafe), + and ships as a thumbv7em-none-eabi staticlib linked into gale (v0.3.2). So + the interpreter's no_std port follows an ESTABLISHED pattern, and a direct + no_std-Rust→native staticlib for gale is the PROVEN baseline deployment + (what kiln-async does today) — making this direction low-regret. synth-AOT + of wasm modules is separately proven via the jess pipeline (adopt → + meld_fuse → synth_compile → renode/QEMU, async-scheduler-plan.md). + open-questions: > + Only the ELEGANT variant (kiln-as-wasm→synth, vs the proven direct + no_std-Rust build) is unproven — the Phase-1 spike must answer: (1) does + synth accept + correctly AOT a module as large/complex as the kiln + interpreter; (2) interpreter-in-wasm-AOT'd-to-native perf vs the direct + no_std-Rust build and vs the peers; (3) bootstrapping/toolchain-trust of + compiling the interpreter through the same pipeline it runs. Fallback if + wasm→synth is impractical: the direct no_std-Rust build (kiln-async's + proven path) — the port work in REQ_NOSTD_INTERP is identical either way; + only the final codegen differs. So the port is committed; only the codegen + path is spike-gated. + upstream-ref: https://github.com/pulseengine/kiln/issues/415 + - id: AD-CRATE-001 type: design-decision title: Fine-grained crate organization @@ -476,3 +564,153 @@ artifacts: target: REQ_WITNESS_COV - type: derives-from target: REQ_WITNESS_COV + + - id: AD-WCMC-001 + type: design-decision + title: Bounding arbitrary-wasm memory (WCMC) — scry proves the hard half; kiln plumbs it; NO new companion + status: proposed + description: > + How much memory an arbitrary wasm module can consume (the crux for fixed + embedded RAM on gale/gust) is answered by COMPOSING existing PulseEngine + tools, NOT by building a new one. Decomposition (measured against + kiln-runtime): (a) DECLARED-LIMITS half — guest linear-memory min/max, + table min/max, global count, data/element bytes, per-function locals and + the static max operand-stack height — all exactly computable from the + module bytes in one decode pass (trivial, kiln already decodes it); + (b) STACK / longest-path half — worst-case call depth and shadow-stack + usage — the analytically hard, partly-undecidable part (recursion), which + is exactly what scry already does: "sound abstract interpretation for + WebAssembly (the DO-333 leg)", providing shadow-stack bounds + longest-path + attribution + budget_from_bound. So scry ALREADY answers the hard half; the + memory analog of WCET is scry(space) alongside spar's RTA(time). + tags: [memory, wcmc, bounding, embedded, scry, verification, direction] + links: + - type: satisfies + target: REQ_FUNC_003 + fields: + rationale: > + Two fable subagents (2026-07-11) analyzed this. The memory-bounding agent + recommended a companion analyzer; the maintainer's pointer that "scry + already answers a lot of the memory story" resolves it — scry IS that + analyzer for the stack half (the part the agent itself flagged as "where + a real tool adds value"; the declared-limits half is trivial). spar + already has the CONSUMER (a memory-budget pass, memory_budget.rs: Σ(code+ + data) ≤ memory_size) but lacks a source of truth for wasm component + sizes (hand-entered AADL today) — scry-derived bounds make that property + DERIVED + attested, exactly as WCET feeds RTA. Pipeline: meld → scry + (sound bounds) + kiln (declared-limits extraction) → the EXISTING + kiln.resource_limits custom section (kiln-decoder/src/ + resource_limits_section.rs; carries max_memory_usage, max_call_depth, + qualification_hash, ASIL) → {kilnd reject-at-load | synth sizes .bss/ + stack} → sigil co-signs module+manifest → spar closes the space leg, + RTA the time leg → rivet traces the fits verdict. Reject-at-load moves a + fixed-RAM overrun from "mid-mission trap in the field" to "integration + failure on the bench" — the whole reason WCET analysis exists, applied to + space. + implementation-plan: > + Kiln-side plumbing (concrete, near-term — the soundness gaps the analysis + found, all in the SR-41 family): (1) reject-at-load when a module's + declared memory `min` exceeds the --memory cap (today Memory::new + eagerly allocates `min` BEFORE the SR-41 grow cap applies — the cap is + set post-instantiate); (2) add a runtime element cap to Table mirroring + Memory::runtime_max_pages (table.grow is UNCAPPED today — same class of + bug SR-41 fixed for memory); (3) WIRE the dead kiln.resource_limits + section — capability_engine.rs:561 extracts it into _resource_config with + a literal `// TODO: Apply resource limits`, so the whole manifest pipe + exists but is disconnected; (4) restructure the 8 MiB HeapProvider that is + CLONED per-function/per-instruction (bounded_runtime_infra.rs:37 + + module.rs) so decoded-module RSS is O(|wasm|) not ~8 MiB × n_functions — + until then any interpreter WCMC is dominated by an artifact. These become + SR-43/44/45 + a perf fix once SR-41/42 (#417) land. + cross-repo: > + scry (producer of stack/longest-path bounds), spar (consumer: + memory-budget pass), synth (per-function native frame sizes for the + embedded WCSU), sigil (attests the manifest). Registered scry in rivet + externals for cross-linking. + embedded-trust-chain: > + scry runs HOST-side (build time) — it is NOT on the embedded path, so the + target cannot recompute the bounds; it must instead TRUST them, which + means they travel SIGNED and are VERIFIED ON-TARGET. Chain: scry computes + the bounds -> written into the kiln.resource_limits custom section -> + sigil signs the module INCLUDING that section (sigil embeds signatures in + the wasm and already has "verify image size before signing" precedent) -> + the embedded target verifies the signature OFFLINE, ON-TARGET, KEY-BASED, + then reject-at-loads off the SIGNATURE-VERIFIED size info (never the raw + unsigned claim). Two sigil ADJUSTMENTS are required and are the gap: (1) a + no_std sigil VERIFIER library (sigil is std-only today — grep finds no + no_std/#![no_std]; the verifier must compile for thumbv7em to run on + gale/gust), and (2) KEY-BASED offline verification only — sigil's own + recorded residual is "offline keyless verification impossible" (Sigstore/ + keyless needs network), so air-gapped embedded uses embedded public keys. + The size/WCMC manifest must be a SIGNED field of the attestation, not an + unsigned custom section. Tracked as a sigil coordination issue. + loader-integration: > + CRITICAL shape: the no_std sigil verifier is a LIBRARY compiled INTO + kiln's embedded LOADER — NOT a separate verifier component/tool that sits + next to the loader and is invoked by it. verify-signature + + check-signed-size-fits-budget + reject-at-load are ONE inseparable + admission step inside kiln's module-load path (the on-board interpreter's + load_module). Rationale: (a) verification is then NON-BYPASSABLE — you + physically cannot admit a module without verifying it, no code path loads + unverified bytes; (b) the TCB stays a SINGLE fused loader instead of + loader + separate verifier + IPC between them, which matters for the + minimal-TCB argument (gust: TCB = ~4-fn shim). So the sigil ask is a + no_std verify LIBRARY designed to be embedded into a host loader, and + kiln's embedded load path calls it inline before instantiation. + upstream-ref: https://github.com/pulseengine/kiln/issues/415 + provenance: + created-by: ai + model: claude-opus-4-8 + timestamp: 2026-07-11T09:00:00Z + release: v0.6.0 + - id: AD-LOADER-VERIFY-001 + type: design-decision + title: On-target admission — kiln's loader verifies a sigil signature before trusting kiln.resource_limits (fail-closed) + status: proposed + description: > + The kiln embedded loader shall VERIFY a module's sigil signature (via sigil's + no_std verify-core, compiled INTO the loader) BEFORE trusting the signed + kiln.resource_limits bounds it uses for reject-at-load — because scry's bounds + are computed host-side and the fixed-RAM target cannot recompute them, so it + must trust a signed, on-target-verified bound, never a forgeable raw claim. + FAIL-CLOSED contract (agreed with sigil, kiln#421 / sigil#187): the loader + REJECTS the module if (a) the signature is invalid, OR (b) the + kiln.resource_limits section is absent, OR (c) a signed bound + (max_memory_usage / max_call_depth / …) exceeds the provisioned RAM/stack + budget. This is the boot-admission gate; it composes with SR-43 (reject-at-load + on declared min) and SR-41/SR-44 (runtime caps). Implements the AD-WCMC-001 + embedded trust chain. + tags: [security, loader, embedded, sigil, attestation, reject-at-load, cross-repo, direction] + links: + - type: satisfies + target: REQ_FUNC_003 + fields: + rationale: > + Confirmed cross-repo (kiln#421): (1) the loader hook already exists — + extract_resource_limits_from_binary (kiln-foundation/src/execution.rs:144, + called at capability_engine.rs:559); wiring it to call sigil-verify-first IS + SR-45's kiln-side work, extended. (2) cargo-kiln embed-limits already exists + (cargo-kiln/src/commands/embed_limits.rs) and runs as a PRE-SIGN step so the + bounds land inside sigil's signed hash. (3) the existing ResourceLimitsSection + (v1, no_std/BoundedMap) is reused verbatim — sigil's whole-module signature + already covers it, no new manifest. sigil↔kiln boundary is a Rust staticlib + for thumbv7em (mirroring kiln-async), no C ABI. Verification is fused into + load_module (non-bypassable) — see AD-WCMC-001 loader-integration. + pipeline: > + meld -> cargo-kiln embed-limits (writes kiln.resource_limits) -> sigil sign + (embeds Ed25519 signature) -> [target] kiln loader { sigil no_std verify -> + trust bounds -> fit-check -> admit | reject } -> run. + cross-repo: > + sigil delivers: sigil:REQ-15 (no_std verify-core staticlib for thumbv7em, + v0.10.0), sigil:REQ-16 (signed reject-at-load of kiln.resource_limits, + v0.11.0), sigil:DD-8 (secure-boot verify profile: key-based Ed25519, + HW-preferred/SW-fallback), under sigil:FEAT-12. no_std crypto spike cleared + (ed25519-compact + ct-codecs build no_std for thumbv7em with pubkey verify). + Key-based only (keyless/Sigstore offline impossible). gale#164 covers HW + Ed25519 + trust-anchor provisioning. kiln#421 / sigil#187. + upstream-ref: https://github.com/pulseengine/kiln/issues/421 + provenance: + created-by: ai + model: claude-opus-4-8 + timestamp: 2026-07-11T11:00:00Z + release: v0.6.0 diff --git a/safety/requirements/roadmap-requirements.yaml b/safety/requirements/roadmap-requirements.yaml index a523bad6..9bcc8e11 100644 --- a/safety/requirements/roadmap-requirements.yaml +++ b/safety/requirements/roadmap-requirements.yaml @@ -544,6 +544,70 @@ artifacts: timestamp: 2026-07-08T22:48:04Z release: v0.7.0 + - id: REQ_NOSTD_INTERP + type: requirement + title: Kiln interpreter runs no_std for on-board embedded execution (hybrid with synth-AOT) + description: > + Kiln's interpreter shall build and run in a no_std/no_alloc environment on + embedded targets (thumbv7em / gale / gust), so kiln can interpret + WebAssembly ON-BOARD alongside the synth-AOT native path — the alternative + for payloads where AOT is not wanted (dynamic/late-loaded, migrated, + untrusted, or smaller-TCB cert contexts) — matching the deployment model of + the safety-critical interpreter field (NASA spacewasm, DLR-FT, #413) while + carrying kiln's verification evidence (Verus / Lean / witness MC/DC / scry / + sigil). DEPLOYMENT: kiln (no_std/no_alloc) is compiled TO a wasm module that + synth AOT-compiles to native for the target — the same pipeline as user + code (wasm = universal IR, synth = single compiler, kiln-as-wasm itself + attestable). UNIQUE SCOPE: the on-board interpreter runs the FULL Component + Model (direct hosting, AD-COMPONENT-HOST-001) or plain core wasm — peers are + core-only; this extends AD-COMPONENT-HOST-001's direct-hosting from + QM/std-only to embedded. meld + synth (AOT hot path) are RETAINED. Phased: + (1) feasibility spike — compile a minimal kiln interpreter to wasm, synth-AOT + it to native, interpret a core module under no_std+alloc on thumbv7em with + fuel + bounded memory intact; measure size + perf vs a direct no_std-Rust + build and vs the peers (go/no-go gate, incl. does synth accept a module this + large); (2) port sync primitives (~90 Mutex/RwLock/thread → kiln-sync) and + collections (std → alloc/bounded) behind the std-feature boundary; (3) host/ + WASI imports via the kiln-builtins platform-callback surface + a GALE OS + requirement for runtime wasm loading (dynamic module/component load) and for + running the synth-compiled kiln image; (4) Component-Model-on-embedded (bring + the direct-hosting path no_std); (5) live-instance migration (state serialize/ + restore — DLR-FT parity, gale/gust checkpoint-restart/failover; own track); + (6) cert-evidence parity with the std interpreter. Corrects the record: + REQ_FUNC_002 (baremetal) and REQ_FUNC_033 (kilnd-nostd) are marked + implemented, but RFC #46 routes embedded through synth-AOT only and + kiln-runtime is std-bound today — this delivers the actual no_std interpreter. + Amends RFC #46 (doc + BA sign-off). + status: proposed + release: v0.6.0 + tags: [interpreter, no-std, embedded, migration, rfc46-amendment, roadmap, direction] + links: + - type: derives-from + target: REQ_FUNC_002 + - type: depends-on + target: gust:SYSREQ-KILN-002 + fields: + upstream-ref: https://github.com/pulseengine/kiln/issues/415 + cross-repo: > + Aligns with existing sibling work (rivet externals synced): gust's whole + thesis is "kernel = verified wasm dissolved to native, TCB = ~4-fn shim", + and gust already tracks the wasm->native-toolchain-in-TCB trust argument + (my open-question #3 is gust's existing concern) and a phase-2 kiln + integration (gust:STKH-002 eliminate-C-FFI, gust:SYSREQ-KILN-002 + end-to-end verified compilation pipeline, gust:SWREQ-KILN-003 synth ARM + codegen). gale's north-star is "the dissolved CM composition runs on the + kiln/gust stack, kiln-async drives it bare metal" — confirming the + no_std/no_alloc embedded precedent. The kiln-as-wasm->synth idea is + PHILOSOPHICALLY IDENTICAL to gust's kernel-as-dissolved-wasm, so it fits + the existing architecture rather than fighting it. The genuinely-NEW ask + for gust is narrowly RUNTIME wasm loading (load a module/component + on-target at runtime for the interpreter path) — distinct from gust's + build-time dissolve — tracked as a gust gh issue for coordination. + provenance: + created-by: ai + model: claude-opus-4-8 + timestamp: 2026-07-11T00:00:00Z + - id: REQ_ENGINE_COMPARISON type: requirement title: Benchmark and differentially validate kiln against the safety-critical Rust interpreter field (NASA spacewasm, DLR-FT), not only wasmtime