{
  "finding_id": "DF-5586",
  "title": "vkernel exc_segfault() tail splz() unguarded: deferred IPIs/interrupts dispatched inside interrupted critical sections (pc64 doreti TD_CRITCOUNT gate divergence)",
  "verdict": "reproduced",
  "impact": "none (mechanism proven; in-vkernel corruption latent/timing-dependent; class memcorrupt)",
  "reproduce": {
    "build": "sh build.sh",
    "run": "./splzcrit vkernel; ./splzcrit pc64; in-vkernel: sh build_image.sh && sh run_vk.sh",
    "expected": "vkernel mode: INVARIANT_BROKEN callback_critcount=1 callback_torn=1; pc64 mode: INVARIANT_OK callback_critcount=0; vkernel storm: STORM_DONE/STORM_RC=0/ALIVE"
  },
  "kernel_refs": [
    "sys/platform/vkernel64/x86_64/exception.c:269",
    "sys/platform/vkernel64/platform/machintr.c:122",
    "sys/platform/pc64/x86_64/ipl.s:132",
    "sys/kern/lwkt_thread.c:1068"
  ],
  "artifacts": [
    "splzcrit.c", "storm.c", "build.sh", "run.sh", "build_image.sh",
    "run_vk.sh", "build_and_model.log", "run_vk.log", "fix.diff",
    "VERDICT.md", "README.md", "verdict.json", "manifest.json", "env.txt"
  ]
}