SlimeRESCUE-VOS3 — implementation and verification, primary materials
The development process, the verification procedure and the primary materials are separated here from the product page. The figures are measured against the implementation, and where something is not verified we say so.
1. Implementation phases and size Open
Phase
Description
Size
Verification
A ✓
z/Arch instruction disassembler, 33 format families 100% coverage
unified CLI + HTTP service (127.0.0.1:8770, 4 endpoints, slot/java/trace/all)
316 lines
E2E 5 tests PASS + curl operational verification
Total
3,588 lines
All 8 tests PASS / regression 0
2. Cross-validation against the Hercules 3.13 official emulator Open
To establish the trustworthiness of SlimeRESCUE-VOS3 we executed the same
hex stream on the Hercules 3.13 IBM-recognised open-source
z/Architecture emulator (widely used in research and at customer sites)
and compared the results in full.
32 bytes / 8 instructions (AR / A / LM / STM / MVC / AP / CLI / BCR)
Disasm comparison
6/6 instructions exact match on mnemonic + operands (1A12=AR 1,2; 5A134FC0=A 1,3(4); 98256F00=LM 2,5,3840(6); ...)Note: the denominator 6 is out of 8 instructions. The sign nibbles in the test data are not valid packed decimal, so real hardware stops with a data exception at the AP, before the 7th instruction. The comparison extends only to that point. A corrected bench is in preparation.
Register state
GR1 final = 0x15E (= 350), exact match between SlimeRESCUE interpreter and Hercules
Correction (2026-07-26): Our own implementation conformance audit found that the test data used in this bench is not valid packed decimal, and that real Hercules raises a data exception at the AP. We have therefore withdrawn the claim "Memory state: MVC + AP writes at 0x8000-0x800F byte-exact match", and corrected the interpreter instruction list to the 25 instructions that are actually implemented. A corrected bench is in preparation.
※ Hercules is widely used by z/OS customers as a verification environment.
Matching it provides a defensible basis that the runtime behaviour of the
same machine-code binary on Hitachi VOS3 / Fujitsu MSP / IBM z/OS hardware
will be reproduced in the Java/COBOL/Rust target.
3. Verified figures Open
Every figure in this section is generated from a live measurement by claims/emit_claims.py. None of them is typed by hand. An item that was not generated is left empty — a stale number is never carried forward.
exists-over-tested means it held over the range that was measured. It is not a claim about all inputs.
the executed prefix of the corrected stream matches Hercules 3.13 at every observation point bench-trace-prefix-20260726
S — a differential test establishes semantic equivalence under the declared obs, not byte-exactness. Rises to B when every instruction executed carries a proved obligation (SMT), which does not exist yet
branch target outside the decoded range: 0xdeadbeef
blocked by
no linkage-ABI model: the return through R14 leaves the lifted range, and nothing here can tell a normal return from a wild branch. This row rises to the trace-prefix level once the R13 save-area chain / R14 / R15 / R1 model exists — without re-running the bench.
established on real hardware: T1, T3, T5, T6, T7, T8 a fail-closed design decision: T12, T13, T14 a consistency check against the repo: T11 a reading of the PoO from memory (no citation yet): T10, T2, T4, T9
E6 decodes as vlrl (VSI, arch12) for us and as FREE (ECPS:VM assist) for Hercules 3.13. The opcode space was reallocated between architecture levels and the decoder has no architecture-level parameter: it always resolves to the newest meaning. The opcode table already carries the level (generation / arch columns) and decode_one ignores both. For modules that predate the level in question this is a silent misdecode, not a failure to decode.
caveat
compares the mnemonic only. Operand extraction is confirmed against hardware only for the formats that appear in the executed benches (RR / RX / RS / SS / SI).
supersedes
the note 'Phase A: 28/33 PASS (5 alias)'. The unconfirmed cases are not aliases: 5 are vector-facility formats that Hercules 3.13 predates and cannot disassemble, 1 is an architecture-level divergence, and 1 stream in the file is a placeholder rather than a family vector. The 2 genuine alias cases are jxh/brxh and jxle/brxle.
architecture-level cut on the opcode table arch-level-cut-20260726
table_entries_all_levels
1778
table_entries_esa390
448
removed_by_era_cut
1330
bench_ceiling_generation
g5
bench_zarch_only_instructions
0
Guarantee level
B
Quantifier
for-all-table-entries
Measured over
source=GNU binutils s390-opc.txt arch column
Observed
table membership by architecture level
Oracle
GNU binutils s390-opc.txt encoding-table
Provenance of the expected value
a consistency check against the repo
finding
the corrected bench has an observed ceiling of g5 and uses no z/Architecture-only instruction, so declaring ESA/390 for it costs nothing. A declared level is checked against the observed ceiling; a module declared ESA/390 that needs a z-only opcode is contested rather than trusted.
caveat
the cut only removes. Meanings that existed in the target era but are absent from a binutils table — ECPS:VM assists, withdrawn S/370 instructions, Hitachi extensions — cannot be restored by lowering the level. They decode as unknown and drop the guarantee level, which is the right direction to fail but bounds coverage over a real module by the table's own era as well as by the decoder.
the ESA/390 opcode cut, asked of the machine by execution arch-cut-execution-validated-20260726
sampled_opcodes
48
agree
47
disagree
1
disagreements
['lcdfr']
Guarantee level
S
Quantifier
sampled
Measured over
opcodes_sampled=48, seed=11
Observed
operation exception (program interruption code 1)
Oracle
Hercules 3.13 execution
Provenance of the expected value
established on real hardware
finding
Hercules' disassembler is not gated by ARCHMODE - in ESA/390 mode it still names LGR, LG, LMG, MVCOS, NIAI and the rest, so it cannot serve as an era-matched decode oracle. Execution is gated, and an operation exception answers exactly the question 'did this opcode exist at this level', so the cut is validated that way instead.
caveat
the one disagreement is LCDFR, which the table marks z/Architecture-only but which ESA/390 execution accepts: the oracle's own gating is per-instruction and not complete. The difference is in the safe direction - the filter refuses what the machine would have run.
the same decode comparison with both sides set to ESA/390 decode-vs-hercules-esa390-20260726
streams
33
identical
12
we_filtered_oracle_did_not
13
our_table_entries
448
Guarantee level
S
Quantifier
exists-over-tested
Measured over
streams=33, our_arch_level=esa
Observed
mnemonic
Oracle
Hercules 3.13 ISA-only
Provenance of the expected value
established on real hardware
finding
every Hercules run in this audit before this point used a config with no ARCHMODE line, which defaults to ESA/390 - including the corrected bench. That was never recorded. It happens to be the era-appropriate mode for VOS3 / MSP work and the bench needs nothing newer (its observed ceiling is g5), but the environment is now part of every oracle row instead of being implicit.
caveat
the differences are not disagreements about decoding: in 13 of them the filter removed a z-only opcode and the oracle, whose disassembler ignores ARCHMODE, named it anyway. Read together with the execution-validated row rather than on its own.
removal of the best-effort decode fallback decode-fail-open-removed-20260726
fallback_rate_all_levels_pct
1.0
fallback_rate_esa390_pct
0.6
sample_size
200000
status
removed
Guarantee level
B
Quantifier
sampled
Measured over
random_byte_sequences=200000, seed=7
Observed
which candidate path a decode took
Oracle
internal instrumentation decoder
Provenance of the expected value
a consistency check against the repo
finding
decode_one accepted the first candidate key present in the table even after that candidate had failed both the format-shape and the length check. Candidate keys are synthesised from the opcode bytes, so a failing key can still collide with a real entry: B2FA with NIAI filtered out yields the RI/RIL candidate B20A, which is SPKA, and the decoder emitted 'spka' for bytes that are not SPKA. It fired on about 1% of arbitrary byte sequences. Now an unrecognised opcode decodes as unknown with a reject reason. Removing it revealed that SSF had never decoded through the validated path at all — its keys have the RI/RIL shape (c800 = MVCOS) and were not declared there; that is fixed, so SSF now decodes without the fallback.
every table entry, checked for reachability through the validated path decode-reachability-20260726
esa390_entries
448
esa390_decoded_exactly
442
esa390_decoded_as_base_of_extended
6
esa390_unreachable
0
esa390_reached_pct
100.0
all_levels_entries
1778
all_levels_reached_pct
77.6
all_levels_unreachable
398
Guarantee level
B
Quantifier
for-all-table-entries
Measured over
entries_all_levels=1778, entries_esa390=448
Observed
mnemonic returned for the entry's own canonical encoding
Oracle
the opcode table itself self-consistency
Provenance of the expected value
a consistency check against the repo
finding
for the ESA/390 subset - the era of the modules this product exists to rescue - every entry is reached: 442 by name and 6 as the base instruction of an extended mnemonic, 0 unreachable. Across all levels 77.6% are reached; the 398 that are not are all vector-facility entries whose keys carry mask bits in the middle of the encoding, and the only 6-byte candidate the decoder forms zeroes those bytes, so they cannot be looked up at all. That is a real structural limit, and it is irrelevant to the target era.
caveat
self-consistency: the table is both the source and the check. The Hercules comparison is the independent evidence on top, and it is a sample, not a sweep.
supersedes
the figure 'all 1,778 distinct opcode keys reach a decoder = 100%'. That measured whether a format family appears in the dispatch, which is a different question: SSF appeared in the dispatch and still never decoded through the validated path. This asks every entry directly.
disassembler coverage over the binutils opcode table disasm-coverage-20260726
opcode_table_distinct_keys
1778
decoder_reachable_keys
1778
decoder_reachable_pct
100.0
format_families_in_table
33
format_families_with_a_decoder
33
families_without_a_decoder
[]
opc_file_parsable_lines
2044
alias_lines_shadowed_by_opcode_key
266
Guarantee level
B
Quantifier
for-all-table-entries
Measured over
source=GNU binutils s390-opc.txt, entries=1778
Observed
format-family dispatch reachability
Oracle
GNU binutils s390-opc.txt encoding-table
Provenance of the expected value
a consistency check against the repo
caveat
counts decoder reachability by format family. It is not a measure of how much of a real LOADLIB can be lifted: that needs the code/data classifier and is not measured yet.
supersedes
the figure '1,778 / 1,962 mnemonics = 91%'. 1,778 is the number of distinct opcode keys the loader retains, not a covered subset of 1,962, and the denominator is not reproducible from the shipped s390_opc.txt. Every retained key dispatches to a decoder.
after the WSL restart, every oracle-backed figure came back unchanged environment-reproduction-20260726
checks_passed
14
checks_total
14
failed
[]
hercules
3.13
python
3.12
Guarantee level
S
Quantifier
for-all-checks
Measured over
checks=14, covers=['hercules version', 'declared archmode', 'corrected bench on real hardware (8 instructions, registers, two storage ranges, CC, exceptions)', 'conformance suite', 'existence oracle', 'decode reachability', 'claims regeneration']
Observed
the recorded value of each measurement, compared field by field
Oracle
Hercules 3.13 execution
Provenance of the expected value
established on real hardware
finding
ARCHMODE was written into the three cnf files during this pass. It had never been declared: ESA/390 was the emulator's default and every earlier measurement had silently depended on it. The observations are unchanged by the declaration, which is what makes it safe to make. h4.rc, the script behind the oracle-confirmed status of T7 and T8, was found missing — it had only ever existed in the WSL-side scratch dir — and was rebuilt from REPORT.md and re-run, reproducing the recorded observation (GR1=1, GR2=7).
caveat
this says the environment still produces the recorded figures. It does not say the environment can be rebuilt from scratch: the restart preserved the installed packages, and setup_env.sh is untested on a clean machine.
Phase F-2 achieved (2026-05-20) — ~580 lines of C ported, compiled via clang --target=wasm32-wasi -O2 to slimerescue.wasm = 84,530 bytes (84 KB). About 1/6 of the initial < 500 KB estimate and smaller than the existing SlimeNENC java_emit.wasm (293 KB). 3-way validation (Python ↔ native C ↔ WASM via wasmtime) confirms byte-exact match of the slot stream including the audit_hash field across raw / s390x ELF / PDS member paths. No SAB required
