conco/OpenMaidEngine
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases 3 Wiki Activity

feat: --verify execution-driven VM cross-check for SCJUMP decode (Task 4)

Browse Source 
Reworked from static-witness-only to execution-driven: ~99% of SCJUMP decisions
are gated by a native computed value (op 0x60), so witness-synthesis alone can't
cover them. Value-local tracking resolves load-then-compare guards to real globals;
native terms honestly marked opaque. Verify: static 3/3 exact + 279/279 execution-
driven consistent over 2000 seeds, 0 failures.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
This commit is contained in:
gamer147
2026-07-07 09:30:10 -04:00
parent 9862e29af0
commit fe23accfa2
2 changed files with 187 additions and 16 deletions
Download Patch File Download Diff File Expand all files Collapse all files

11
tools/test_scjump.py
View File

@@ -40,9 +40,20 @@ def test_emit_json_shape():
check(S.render_guard({"global": 0x3234, "op": "==", "value": 7}, {0x3234: "chapter_mode"}) == "chapter_mode==7",
"render_guard uses registry name")
def test_verify_sound_on_sample():
scr = S.load_scjump()
r = S.run_verify(scr, trials=1000)
# execution-driven check reaches many decision sites and agrees with the VM on all of them
check(r["rand_reached"] > 50, f"execution-driven check reaches decision sites (reached={r['rand_reached']})")
check(r["rand_ok"] == r["rand_reached"], f"every VM-realized decision agrees with the table (ok={r['rand_ok']}/{r['rand_reached']})")
# the fully-static decisions synthesize and match exactly
check(r["static_ok"] == r["static_n"], f"static-witness decisions all match (ok={r['static_ok']}/{r['static_n']})")
check(r["fails"] == [], f"0 verification failures (fails={r['fails'][:3]})")
if __name__ == "__main__":
test_cfg_acyclic_and_dispatch()
test_decode_anchor_and_count()
test_emit_json_shape()
test_verify_sound_on_sample()
print(f"\n{len(FAILS)} failures")
sys.exit(1 if FAILS else 0)