docs(rivet): combined rivet-doc artifacts — no_std direction + memory-bounding + sigil trust chain (supersedes #416/#418/#422)

.gitignore

@@ -61,3 +61,6 @@ MODULE.bazel.lock
 /simple.wat
 /minimal.wat
 /file_ops_component.wat
+
+# Rivet external project cache
+.rivet/repos/

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

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