Merge harden/fuzz-miri: Invariant-1 no-panic fuzzer + Miri subset + generator fuel fix

Author: olwang

Makefile

@@ -0,0 +1,34 @@
+# Convenience targets for the RSScript dev container.
+#
+# Run everything inside the Docker dev environment (see docs/DOCKER.md):
+#   docker compose run --rm dev make <target>
+#
+# These are thin wrappers around the cargo invocations documented in
+# docs/DEVELOPMENT.md; they exist so CI and contributors invoke the *same*
+# command.
+
+.PHONY: miri fuzz-no-panic
+
+# Tier C (runtime hardening): run Miri over the largest pure-Rust subset it can
+# soundly interpret — the `rss-testgen` seed decoder (pure arithmetic / control
+# flow, no I/O, no FFI). Miri double-checks that subset for undefined behaviour
+# (out-of-bounds, use-after-free, invalid-value, data races).
+#
+# What Miri canNOT cover here, by construction:
+#   * the vm-jit tier — it executes generated *native machine code*, which Miri
+#     (a MIR interpreter) cannot run at all;
+#   * the FFI / syscall seams (native plugin cdylibs, process/network/filesystem
+#     in `rsscript-runtime` and `reir`) — Miri's isolation blocks real syscalls,
+#     so those test binaries abort under Miri rather than reporting UB.
+# Invariant 2 (`panic = "abort"`) is what keeps those out-of-Miri-scope seams
+# safe in production; Miri's job is the pure value/logic core.
+#
+# Requires a nightly toolchain with the `miri` component:
+#   rustup toolchain install nightly --component miri,rust-src
+miri:
+	cargo +nightly miri test -p rss-testgen --lib
+
+# Smoke-run the Invariant-1 no-panic fuzz target (requires `cargo install
+# cargo-fuzz` and a nightly toolchain). Bounded so it is CI-friendly.
+fuzz-no-panic:
+	cd fuzz && cargo +nightly fuzz run no_panic -- -runs=20000 -max_total_time=60

crates/rss-testgen/src/generator.rs

@@ -742,40 +742,49 @@ impl<'a> Generator<'a> {
 
     fn gen_expr(&mut self, ty: &Ty, scope: &Scope, fuel: u32) -> String {
         if fuel == 0 {
-            return self.gen_atom(ty, scope);
+            return self.gen_atom(ty, scope, 0);
         }
         // Occasionally satisfy an `Int` target with a monomorphized generic call.
         if *ty == Ty::Int && !self.generic_fns.is_empty() && fuel > 0 && self.seed.choice(4) == 0 {
             return self.gen_generic_call(scope, fuel);
         }
         match self.seed.weighted(&[3, 2, 4]) {
-            0 => self.gen_atom(ty, scope),
+            0 => self.gen_atom(ty, scope, fuel),
             1 => self
                 .gen_call(ty, scope, fuel)
-                .unwrap_or_else(|| self.gen_atom(ty, scope)),
+                .unwrap_or_else(|| self.gen_atom(ty, scope, fuel)),
             _ => self.gen_compound(ty, scope, fuel),
         }
     }
 
-    /// A leaf: an in-scope variable, or a freshly constructed value.
-    fn gen_atom(&mut self, ty: &Ty, scope: &Scope) -> String {
+    /// A leaf: an in-scope variable, or a freshly constructed value. `fuel` is the
+    /// remaining recursion budget; construction of a compound payload consumes one
+    /// unit, so at `fuel == 0` only nullary literals/atoms are produced — this is
+    /// what guarantees termination even when a function returning `T` takes a
+    /// compound-of-`T` parameter (the `T -> Option<T> -> T -> …` cycle).
+    fn gen_atom(&mut self, ty: &Ty, scope: &Scope, fuel: u32) -> String {
         let vars = scope.bindings_of(ty);
         if !vars.is_empty() && self.seed.bool() {
             return vars[self.seed.choice(vars.len())].name.clone();
         }
-        self.gen_construct(ty, scope)
+        self.gen_construct(ty, scope, fuel)
     }
 
     /// Construct a value of `ty` (literal for scalars; constructor for compounds).
-    fn gen_construct(&mut self, ty: &Ty, scope: &Scope) -> String {
+    /// Compound payloads are generated with strictly-decreasing `fuel` so that
+    /// `Some`/`Ok` nesting cannot reset the recursion budget — at `fuel == 0` the
+    /// payload is a plain `gen_construct` (a literal/atom that never re-enters
+    /// `gen_expr`), which is what bounds generation.
+    fn gen_construct(&mut self, ty: &Ty, scope: &Scope, fuel: u32) -> String {
+        let payload_fuel = fuel.saturating_sub(1);
         match ty {
             Ty::Int | Ty::Bool | Ty::Float | Ty::String => self.gen_literal(ty),
             Ty::Option(inner) => {
-                let value = self.gen_expr(inner, scope, 1);
+                let value = self.gen_expr(inner, scope, payload_fuel);
                 format!("Some({value})")
             }
             Ty::Result(ok, _) => {
-                let value = self.gen_expr(ok, scope, 1);
+                let value = self.gen_expr(ok, scope, payload_fuel);
                 format!("Ok({value})")
             }
             Ty::Struct(name) => {
@@ -921,7 +930,7 @@ impl<'a> Generator<'a> {
             | Ty::List(_)
             | Ty::Map(_, _)
             | Ty::Set(_)
-            | Ty::Deque(_) => self.gen_construct(ty, scope),
+            | Ty::Deque(_) => self.gen_construct(ty, scope, fuel),
         }
     }
 

docs/hardening-todo.md

@@ -63,19 +63,43 @@ prefixes (the enum is intentionally minimal: `Diagnostics` / `Runtime`).
 
 ## Tier C — longevity (lower urgency)
 
-- [ ] **C5 Miri in CI** over a small test subset (we have none today) — also
-  double-checks the `unsafe` in `vm-jit`. Add a `cargo miri test` target/job;
-  if Miri flags `vm-jit`, document/fix.
+- [x] **C5 Miri in CI** over a small test subset (we had none) — landed as the
+  `make miri` target: `cargo +nightly miri test -p rss-testgen --lib`. That is
+  the largest subset Miri can *soundly* interpret here — the `rss-testgen` seed
+  decoder is pure arithmetic/control-flow with no I/O or FFI, so Miri can check
+  it for UB (it reports clean). **What Miri cannot cover, by construction:**
+  - the **vm-jit** tier executes generated *native machine code*; Miri is a MIR
+    interpreter and cannot run native code at all, so the JIT execute path is
+    permanently out of Miri's scope (this is why Invariant 2's `panic = "abort"`
+    carries the safety burden at the JIT/FFI seams instead);
+  - the **FFI / syscall** seams (`rsscript-runtime`'s tokio/reqwest/process/fs,
+    `reir`'s filesystem adapters, native plugin cdylibs) abort under Miri's
+    isolation — that is *unsupported I/O*, not detected UB, so those crates are
+    deliberately excluded rather than run-and-silenced.
+  Setup (offline-installable in the dev container):
+  `rustup toolchain install nightly --component miri,rust-src`.
 - [ ] **C6 Cycle/leak policy.** The value model makes accidental cycles unlikely;
   decide explicitly — document the weak-discipline + add leak tests, or plan a
   cycle collector for very-long-running apps.
 
 ## Meta — prove the invariant continuously
 
-- [ ] **M Invariant-1 fuzz target.** New `fuzz/fuzz_targets/no_panic.rs`: feed
-  random valid programs, assert the runtime only ever returns `Ok`/`EvalError`,
-  never panics. Converts "we hardened it" into "CI keeps it hardened" — the
-  natural extension of the existing `fail_closed`/`hostile.rs` ethos.
+- [x] **M Invariant-1 fuzz target.** Landed `fuzz/fuzz_targets/no_panic.rs`: a
+  seed decodes (via `rss-testgen`) to a well-typed program which, if the checker
+  accepts it, is evaluated on the reg-VM through
+  `reg_vm_eval_source_main_with_limits` under generous-but-finite `VmLimits`
+  (`max_depth: 16_384`, `step_budget: 50_000_000`, `mem_budget: 512 MiB`). The
+  result must be `Ok`/`EvalError`; any panic/abort is recorded by libFuzzer as a
+  crash. Converts "we hardened it" into "CI keeps it hardened" — the natural
+  extension of the `fail_closed`/`hostile.rs` ethos. Run it via
+  `make fuzz-no-panic` (or `cargo +nightly fuzz run no_panic`).
+  - *Bug it already caught:* the first smoke run surfaced a native stack
+    overflow — not in the runtime, but in the `rss-testgen` **generator** itself:
+    `gen_construct` reset the recursion `fuel` to a constant `1` for `Some`/`Ok`
+    payloads, so a generated `fn f(x: Result<Float,String>) -> Float` produced an
+    unbounded `Float → Result<Float> → Float → …` construction. Fixed by
+    threading strictly-decreasing fuel through `gen_atom`/`gen_construct` (this
+    bug latently affected the existing `differential`/`fail_closed` targets too).
 
 ## Verification discipline