Skip to content

vms-cf5: consolidate vax drivers onto one crash-proof session-runner + exit-code contract - #581

Merged
baron-3dl merged 2 commits into
mainfrom
work/vms-cf5-retrofit
Aug 15, 2026
Merged

baron-3dl merged 2 commits into
mainfrom
work/vms-cf5-retrofit

Conversation

@baron-3dl

Copy link
Copy Markdown
Contributor

Summary

Retrofit tail for rd vms-cf5 (the vaxharness.py helper landed in #570).
Adds the canonical PROOF_FAILED/HARNESS_ERROR exit-code contract and a
shared run_captured() guest-session helper to tests/lab-vax/vaxharness.py,
then retrofits all seven vax SIMH drivers onto it, so the negctl-exit-code
bug class (access exiting 60, proctab/mbx exiting 16 -- a clean proof-fail
landing on a code the gate refused to invert) is structurally fixed instead
of re-fixed per driver.

  • vaxharness.py: Proof.exit_code() returns 0 or the single canonical
    PROOF_FAILED; negctl_gate()/negctl_gate.sh gain one carve-out --
    HARNESS_ERROR is never "the gate satisfied", in either mode -- additive
    to the existing zero-vs-nonzero table, not a rewrite (a not-yet-migrated
    legacy code still inverts exactly as before). New run_captured() encodes
    the redirect-to-file + Python-side-parse + always-dump-a-transcript
    convention (bug dcl: SHOW DEVICE row byte-exact + create_dir leak fix (vms-b9f round 5) #4: truncation on the lossy VAX/SIMH serial) once.
  • test_vaxharness.py: 16 new cases (48 total, all green) pin the new
    table (Python + bash mirror) and run_captured()'s contract.
  • All 7 drivers (drive_{access,proctab,mbx,boot,eflag,devvms,vmsfs}_vax.py)
    now return only {0, PROOF_FAILED, HARNESS_ERROR}; run-{eflag,devvms, vmsfs}.sh route negctl inversion through negctl_gate.sh instead of
    hand-rolling it. run-boot.sh is deliberately left un-routed (documented
    why: drive_boot_vax.py already computes final pass/fail per mode
    itself).
  • Behavior-preserving: no assertion/proof logic touched anywhere, only
    which integer a clean-fail/harness-error site returns.

Test plan

  • pytest tests/lab-vax/test_vaxharness.py -v -- 48 passed (32
    pre-existing + 16 new), no SIMH/container needed.
  • python3 -c "import ast; ast.parse(...)" on all 7 retrofitted
    drivers + a stubbed-import smoke test (fake anita/pexpect/
    netbsd_console modules) -- all import cleanly.
  • bash -n on every touched run-*.sh + negctl_gate.sh.
  • Nightly SIMH proofs (vax sysboot vms-d9c, event-flag, proctab, mbx,
    access -- positive + negctl-inverted) confirmed still PASS on the
    retrofitted drivers, by console evidence, not monitor-green alone.
    Triggered separately; conductor to attach run IDs before merge.

🤖 Generated with Claude Code

baron-3dl and others added 2 commits August 15, 2026 08:31
…+ exit-code contract

Retrofit tail for the vaxharness.py helper landed in #570: adds the
canonical PROOF_FAILED/HARNESS_ERROR exit-code contract and a shared
run_captured() guest-session helper, then retrofits all seven vax SIMH
drivers onto it so the recurring negctl-exit-code bug class (access
exiting 60, proctab/mbx exiting 16 -- a clean proof-fail landing on a
code the gate refused to invert) cannot recur in future facility proofs.

vaxharness.py:
- PROOF_FAILED/HARNESS_ERROR: Proof.exit_code() now returns 0 or the
  single canonical PROOF_FAILED, never a driver-invented ad hoc code.
- negctl_gate()/negctl_gate.sh gain one carve-out: HARNESS_ERROR is
  NEVER "the gate satisfied", in either mode (a harness crash during a
  negctl run is not evidence the negative control had teeth). Every
  other exit code keeps the existing zero-vs-nonzero table unchanged --
  additive, not a semantics rewrite, so a not-yet-migrated legacy code
  still inverts exactly as before.
- run_captured(run_fn, cmd, outfile, timeout): the shared
  redirect-to-file + Python-side-parse + always-dump-a-transcript
  helper (bug #4: a collapsed one-liner with $(...) + inline sed
  truncating on the lossy VAX/SIMH serial), so no future driver
  hand-rolls it.
- test_vaxharness.py: 16 new cases (48 total, all green) pin the
  PROOF_FAILED-inverts / HARNESS_ERROR-stays-red table (Python + bash
  mirror) and run_captured()'s never-raises/redirect-shape contract.

Driver retrofit (behavior-preserving -- only WHICH integer a
clean-fail/harness-error site returns changed, no assertion logic
touched):
- drive_access_vax.py / drive_proctab_vax.py / drive_mbx_vax.py
  (already on vaxharness.py): every return site now routes through
  proof.exit_code() or HARNESS_ERROR.
- drive_boot_vax.py / drive_eflag_vax.py / drive_devvms_vax.py /
  drive_vmsfs_vax.py (newly onto the exit-code contract): import
  PROOF_FAILED/HARNESS_ERROR, swap every ad hoc nonzero at a
  clean-proof-fail site for PROOF_FAILED and every
  pexpect.TIMEOUT/EOF/Exception handler for HARNESS_ERROR.
- run-eflag.sh / run-devvms.sh / run-vmsfs.sh: now source
  negctl_gate.sh and call vaxharness_negctl_gate() with the
  ||-protected run_session pattern, instead of hand-rolling
  `if run_session prove skip; then die "NO TEETH"; fi`.
- run-boot.sh: left un-routed through negctl_gate.sh by design
  (documented) -- drive_boot_vax.py already computes the final
  pass/fail verdict per mode itself, so there is no wrapper-side
  inversion to apply.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
…d vms-6d7 gate)

The two divider lines I added around the new
"rd vms-cf5's retrofit tail" test class comment were 70 dashes; every
other divider in this file (marker '#', char '-') is 74 -- the
divider_integrity_gate (ctest test_repo_source_tree_has_no_flagged_dividers,
rd vms-6d7) correctly flagged both as truncated-divider findings at
lines 316/318. Widened both to 74 dashes to match the file's existing
convention. This was introduced by my own retrofit edit (not a
pre-existing corruption inherited from a prior merge); no other file
in the tree is flagged.

Co-Authored-By: Claude Opus 4.8 (1M context) <noreply@anthropic.com>
@baron-3dl
baron-3dl force-pushed the work/vms-cf5-retrofit branch from 7a0652e to b090c06 Compare August 15, 2026 08:32
@baron-3dl
baron-3dl merged commit 5108e20 into main Aug 15, 2026
98 checks passed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

None yet

Projects

None yet

Development

Successfully merging this pull request may close these issues.

1 participant