SlimeRESCUE-VOS3 — 実装・検証の一次資料
製品ページから開発過程・検証手続き・一次資料をこちらへ分離しています。数値は実装と突き合わせた実測値であり、検証できていない範囲は検証できていないと書きます。
1. 実装フェーズと規模 Open
| Phase | 内容 | 規模 | 検証 |
|---|---|---|---|
| A ✓ | z/Arch 命令 disassembler、33 format families 100% カバー | 757 行 | 28/33 PASS (5 alias)、18 format 20/20 PASS、cobol-like seq 8/8 PASS |
| B ✓ | s390x ELF64 BE parser (Linux file(1) が「IBM S/390」認識) | 260 行 | ELF roundtrip 8/8 PASS |
| C ✓ | Slot IR mapping (67 mnemonic 対応表、既存 SlimeNENC slot.c backend 互換) | 406 行 | Slot IR mapping 8/8 PASS |
| D ✓ | z/OS LOADLIB / PDS parser (256-byte directory blocks、EBCDIC member name、TTR ポインタ) | 275 行 | PDS roundtrip 3 member byte-exact + pipeline 8/8 PASS |
| E ✓ | Python z/Arch interpreter (25 命令 + packed BCD decimal + Hercules-style trace) | 342 行 | behavioural 6/6 PASS + Hercules 3.13 cross-validated 6/6 |
| F-1 ✓ | unified CLI + HTTP service (127.0.0.1:8770、4 endpoints、slot/java/trace/all) | 316 行 | E2E 5 test PASS + curl 動作確認 |
| 合計 | 3,588 行 | 全 8 test PASS / regression 0 | |
2. Hercules 3.13 official emulator との cross-validation Open
SlimeRESCUE-VOS3 の信頼性を担保するため、Hercules 3.13 (IBM 公認の open-source z/Architecture emulator、研究機関で標準的使用) と 同一 hex stream を実行した結果を完全比較しました。
| 環境 | Hercules 3.13 (Ubuntu apt-get)、CPUMODEL 3090、MAINSIZE 16MB |
|---|---|
| テスト stream | 32 bytes / 8 instructions (AR / A / LM / STM / MVC / AP / CLI / BCR) |
| Disasm 比較 | 6 / 6 命令で mnemonic + operand 完全一致 (1A12=AR 1,2、5A134FC0=A 1,3(4)、98256F00=LM 2,5,3840(6)、...)※ 分母 6 は 8 命令中。実機はテストデータの packed decimal 符号ニブルが不正なため、7 命令目の手前 (AP) でデータ例外により停止します。比較はその地点までです。修正版ベンチで差替予定。 |
| Register state | GR1 final = 0x15E (= 350)、SlimeRESCUE interpreter と Hercules で完全一致 |
訂正 (2026-07-26): 自社の実装適合性監査により、本ベンチのテストデータが packed decimal として不正であり、実機 Hercules では AP でデータ例外が発生することを確認しました。これに伴い「Memory state: 0x8000-0x800F の MVC + AP 書込み結果が byte-exact 一致」の記載を撤回し、interpreter 命令の列挙を実装どおり 25 命令に訂正しました。修正版ベンチを準備中です。
※ Hercules は z/OS 顧客の検証環境としても広く使用されており、これと一致するこ とで「同じ機械語 binary を Hitachi VOS3 / Fujitsu MSP / IBM z/OS 実機で実 行した結果」と同じ振る舞いを Java/COBOL/Rust 移植先で再現できる根拠となります。
3. 検証済みの数値 Open
この節の数字はすべて claims/emit_claims.py が実測から生成しています。手で書いた数字はありません。生成されなかった項目は空欄になります(古い数字が残ることはありません)。
exists-over-tested = 測定した範囲で成立した、という意味であり、全入力に対する主張ではありません。
the executed prefix of the corrected stream matches Hercules 3.13 at every observation point bench-trace-prefix-20260726
| GR1 | 350 |
|---|---|
| mem[0x8000..0x800F] | 444154415f464f525f4d564321212121 |
| mem[0x7800..0x7802] | 12355c |
| cc | 0 |
| exception | None |
| instructions_executed | 8 |
| オラクルと一致 | はい |
| 保証レベル | S |
| 量化 | exists-over-tested |
| 測定域 | streams=1, instructions_decoded=8, instructions_executed=8, prefix_terminates_at=0xdeadbeef, terminal_event=left-mapped-range |
| 観測対象 | GR0-15, mem[0x8000..0x800F], mem[0x7800..0x7802], cc, exception |
| オラクル | Hercules 3.13 ISA-only |
| 期待値の出所 | 実機で確定 |
| level cap | 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 |
| audit_hash | sha256:8391695c94e97bd80122e950f3e3e9761933ea251d827779002ec9cb1536eb4d |
the routine as a whole, including its return to the caller bench-routine-level-20260726
| オラクルと一致 | はい |
|---|---|
| 保証レベル | R |
| 量化 | exists-over-tested |
| 測定域 | streams=1, instructions_decoded=8 |
| 観測対象 | GR0-15, mem[0x8000..0x800F], mem[0x7800..0x7802], cc, exception |
| オラクル | Hercules 3.13 ISA-only |
| 期待値の出所 | 実機で確定 |
| 未モデル | 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. |
| audit_hash | sha256:8391695c94e97bd80122e950f3e3e9761933ea251d827779002ec9cb1536eb4d |
PoO conformance of the 25-instruction interpreter conformance-suite-20260726
| total | 13 |
|---|---|
| conform | 13 |
| 保証レベル | S |
| 量化 | exists-over-tested |
| 測定域 | tests=13, instruction_set=25 |
| 観測対象 | registers, storage, cc, exception, guarantee-level |
| オラクル | Hercules 3.13 ISA-only |
| 期待値の出所 | 混在(内訳は下表) |
| 内訳 | 実機で確定: T1, T3, T5, T6, T7, T8fail-closed の設計判断: T12, T13, T14リポジトリとの整合確認: T11PoO の記憶由来(章段引用未取得): T10, T2, T4, T9 |
| audit_hash | sha256:4124b5434b5cb0ac6ecb2ef213ef81b8909c7c84792ea07ec17fefe6107e264c |
decode of one instruction per format family, against Hercules 3.13 decode-vs-hercules-20260726
| format_families | 32 |
|---|---|
| oracle_confirmed | 26 |
| oracle_gap | 5 |
| arch_level_divergence | 1 |
| genuine_mismatches | 0 |
| streams_in_file | 33 |
| placeholders_excluded | 1 |
| 保証レベル | S |
| 量化 | exists-over-tested |
| 測定域 | format_families=32, instructions_per_family=1, generator=samples/test_33formats.py streams |
| 観測対象 | mnemonic |
| オラクル | Hercules 3.13 ISA-only |
| 期待値の出所 | 実機で確定 |
| 未モデル | e70000000056e70000000044e70000000013e70000000060e70000000036e60000000035 |
| finding | 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. |
| audit_hash | sha256:311b806f00347dc6ff1df3403875191b38465fae3b465c98465f0ebc0099d590 |
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 |
| 保証レベル | B |
| 量化 | for-all-table-entries |
| 測定域 | source=GNU binutils s390-opc.txt arch column |
| 観測対象 | table membership by architecture level |
| オラクル | GNU binutils s390-opc.txt encoding-table |
| 期待値の出所 | リポジトリとの整合確認 |
| 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. |
| audit_hash | sha256:75c252d858c338734b8c52171e28346d44d619be48613de025dddbab67c5730f |
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'] |
| 保証レベル | S |
| 量化 | sampled |
| 測定域 | opcodes_sampled=48, seed=11 |
| 観測対象 | operation exception (program interruption code 1) |
| オラクル | Hercules 3.13 execution |
| 期待値の出所 | 実機で確定 |
| 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. |
| audit_hash | sha256:5e26cc2cc00e17e793122c4ec01eceb4b50299eab59a281a2f883281bf932838 |
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 |
| 保証レベル | S |
| 量化 | exists-over-tested |
| 測定域 | streams=33, our_arch_level=esa |
| 観測対象 | mnemonic |
| オラクル | Hercules 3.13 ISA-only |
| 期待値の出所 | 実機で確定 |
| 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. |
| audit_hash | sha256:08ae8b3940d1336a1a83833f185070bb9d1efef24d24f20238d1a9c592b2993e |
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 |
| 保証レベル | B |
| 量化 | sampled |
| 測定域 | random_byte_sequences=200000, seed=7 |
| 観測対象 | which candidate path a decode took |
| オラクル | internal instrumentation decoder |
| 期待値の出所 | リポジトリとの整合確認 |
| 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. |
| audit_hash | sha256:bfb9d598cd4d9c2cd932a96c4eb19a4e5496b6d569e77d0b1944179eae473890 |
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 |
| 保証レベル | B |
| 量化 | for-all-table-entries |
| 測定域 | entries_all_levels=1778, entries_esa390=448 |
| 観測対象 | mnemonic returned for the entry's own canonical encoding |
| オラクル | the opcode table itself self-consistency |
| 期待値の出所 | リポジトリとの整合確認 |
| 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. |
| audit_hash | sha256:76b79d400d6af27f68d9d0e317cd374e2f814ffa93bddd5ac43e76accf8cf6f1 |
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 |
| 保証レベル | B |
| 量化 | for-all-table-entries |
| 測定域 | source=GNU binutils s390-opc.txt, entries=1778 |
| 観測対象 | format-family dispatch reachability |
| オラクル | GNU binutils s390-opc.txt encoding-table |
| 期待値の出所 | リポジトリとの整合確認 |
| 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. |
| audit_hash | sha256:f0d0a4cb470a0dd689d906f99c2c7491e02029a3358a2c81c4c72f9a9ab97fe7 |
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 |
| 保証レベル | S |
| 量化 | for-all-checks |
| 測定域 | 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'] |
| 観測対象 | the recorded value of each measurement, compared field by field |
| オラクル | Hercules 3.13 execution |
| 期待値の出所 | 実機で確定 |
| 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. |
| audit_hash | sha256:7abdc08b0faa9c58c69cf35760fd1eebdec886ca138a0526284f8a8a899fa6e9 |
the SKU generalisation of the claims apparatus changed no figure refactor-zero-diff-20260726
| rows_before | 10 |
|---|---|
| rows_after | 11 |
| identical | True |
| missing | [] |
| altered | [] |
| added_after_baseline | ['environment-reproduction-20260726'] |
| 保証レベル | B |
| 量化 | for-all-rows |
| 測定域 | rows_compared=10, baseline=claims.baseline-prerefactor.json |
| 観測対象 | every field of every row except generated_utc |
| オラクル | the pre-refactor document self-comparison |
| 期待値の出所 | リポジトリとの整合確認 |
| caveat | a refactor of the apparatus checked with the apparatus. It shows the rules did not move, not that they are right. |
| audit_hash | sha256:7dacd371609c647fa3a843936616e0bda00c627ddc62400418d93a2c0b1f9701 |
生成: 2026-07-26T13:09:38Z — asm_rev_to/claims/emit_claims.py
4. 実装インベントリ Open
| opcode source | GNU binutils s390-opc.txt (公式) を機械的に取り込み、独自取得を防止 |
|---|---|
| interpreter 命令 | 25 命令 (AR, A, AGR, AHI, SR, LR, LGR, L, LHI, LA, ST, LM, STM, MVC, MVI, CLI, CLC, CR, C, BCR, BC, AP, SP, CP, PR) |
| WASI port | Phase F-2 達成 (2026-05-20) ― C 移植 ~580 行 → clang --target=wasm32-wasi -O2 で slimerescue.wasm = 84,530 byte (84 KB)。当初推定 < 500 KB の 約 1/6、既存 SlimeNENC java_emit.wasm (293 KB) より小さい。3-way 検証 (Python ↔ native C ↔ WASM via wasmtime) で slot stream の audit_hash まで byte-exact 一致 (raw / s390x ELF / PDS member 全 path)、SAB 不要 |
5. 関連
- 製品ページ: SlimeRESCUE-VOS3 / SlimeRESCUE ファミリ
- 同系列: SlimeRESCUE-AS400
- 一覧: リソース