risc-v-gsp-rm-debugger: land docs 45-53 + harness/sim tool set with tests

rm_capture (chunked decode), launch_audit, state_seed/state_decode,
valprobe, rehost, contracts+run_contracts, host_traffic, gmmu_walk,
msgq_attach, libos_port, log_decode, server_snapshot; doc index updates
in the tool overview, operations pages and the repo README.

1 files changed, 15 insertions, 1 deletions

diff --git a/docs/05-operations/04-risc-v-gsp-rm-debugger-user-guide.md b/docs/05-operations/04-risc-v-gsp-rm-debugger-user-guide.md
index d16da23..7055f0e 100644
--- a/docs/05-operations/04-risc-v-gsp-rm-debugger-user-guide.md
+++ b/docs/05-operations/04-risc-v-gsp-rm-debugger-user-guide.md
@@ -167,6 +167,10 @@ Run everything from `open-iov/debug/risc-v-gsp-rm-vm/` unless stated.
 | `ci_release.py` | version_diff → matrix → mutation smoke, hashed into one bundle |
 | `port_driver_versions.py`, `port_new_device.py`, `package_sim.py` | porting/packaging scaffolds (dry-run default; pilot status and evaluation in [docs/28](../../debug/risc-v-gsp-rm-vm/docs/28-PORTING-AUTOMATION.md), [docs/29](../../debug/risc-v-gsp-rm-vm/docs/29-PACKAGING-AND-TRIALING.md)) |
 | `value_demos/run_all.py` | ten fixed scenarios s01–s10 with measured time-to-value |
+| `rm_capture.py` | real-client GSP RPC capture: decode, compare, replay prep ([docs/45](../../debug/risc-v-gsp-rm-vm/docs/45-RM-RPC-CAPTURE-AND-REPLAY.md)) |
+| `rehost.py` | run one bounded firmware function with crafted state and before/after snapshots ([docs/46](../../debug/risc-v-gsp-rm-vm/docs/46-SURGICAL-REHOST.md)) |
+| `valprobe.py` | run one firmware validation branch with crafted state and labelled outcome addresses (offline predicate probe; [docs/47](../../debug/risc-v-gsp-rm-vm/docs/47-VALIDATION-PREDICATE-PROBE.md)) |
+| `launch_audit.py` | audit a submission's engine-visible memory contract against captured page tables: `ok`/`pa_mismatch`/`unmapped`/`access_denied` per leg ([docs/48](../../debug/risc-v-gsp-rm-vm/docs/48-GMMU-WALK-AND-LAUNCH-AUDIT.md)) |
 | `common.py` | shared helpers (flat relocation, sessions, bounded log reads) |
 
 ### 4.3 Native simulator, plugins, host oracle, bridges
@@ -174,6 +178,7 @@ Run everything from `open-iov/debug/risc-v-gsp-rm-vm/` unless stated.
 | Tool | One-line purpose |
 |---|---|
 | `sim/` (`--backend native`, `--trace`) | deterministic RV64IMAC interpreter with exec/access trace and lenient MMIO |
+| `sim/gmmu_walk.py` | functional GMMU page-table walker over captured/constructed tables (VER2 4K/2M validated; 64K modelled) |
 | `python3 -m greeneye.device_map harvest\|show\|merge\|demo` | first-touch MMIO map: authoring, inspection, merge |
 | `qemu/greeneye_trace.c` (`make -C qemu`) | full TCG exec/access JSONL trace with `start=`/`end=` filters |
 | `plugins/example_plugin.py` | plugin authoring reference |
@@ -200,9 +205,18 @@ Run everything from `open-iov/debug/risc-v-gsp-rm-vm/` unless stated.
 | "Explore MMIO the firmware touches first" | `probe` → `python3 -m greeneye.device_map` | versioned JSON; feeds the device model |
 | "Triage a release end to end" | `harness/ci_release.py` | always `--dry-run` first |
 | "Let an agent monitor a run" | `plugins/mcp_server.py` | read/observe by default; writes gated |
+| **"Which control/entry shape does the firmware accept, and why?"** | `harness/valprobe.py` | offline predicate branch with crafted state + labelled outcomes; deterministic, seconds; [docs/47](../../debug/risc-v-gsp-rm-vm/docs/47-VALIDATION-PREDICATE-PROBE.md) |
+| **"A handler/function early-outs on state we don't have"** | `harness/rehost.py` | bounded call with crafted state; the first missing state is the finding; [docs/46](../../debug/risc-v-gsp-rm-vm/docs/46-SURGICAL-REHOST.md) |
+| "Decode/compare the real client's GSP RPCs" | `harness/rm_capture.py` | offline decode/stimulus; consumption awaits the message-injection rung; [docs/45](../../debug/risc-v-gsp-rm-vm/docs/45-RM-RPC-CAPTURE-AND-REPLAY.md) |
+| **"Where would the engine read/write this VA?"** | `sim/gmmu_walk.py`, `harness/launch_audit.py` | walk captured/constructed page tables offline; per-leg `ok`/`pa_mismatch`/`unmapped`/`access_denied`; [docs/48](../../debug/risc-v-gsp-rm-vm/docs/48-GMMU-WALK-AND-LAUNCH-AUDIT.md) |
 
 Decision rule: static reading is a hypothesis; a recorded session is evidence;
-at least an A/B pair is a conclusion.
+at least an A/B pair is a conclusion. If the question is "what will this
+firmware branch do with input/state X?", probe it offline first
+(`valprobe`/`rehost`, seconds, deterministic) and spend supervised cycles only
+on what the probe cannot see (engine/silicon behaviour); if it is "what does
+the silicon do?" or "does the run survive?", it is a hardware question and the
+simulator makes no L2/L3 claims.
 
 ## 6. Sessions as evidence