carlok — zsh — 88×30

cat _posts/2026-09-03-dratify-v0-1-3-tests-behind-the-differential-claim-and-untrusted-input-that-can-no-longer-ask-for-gigabytes.md

dratify v0.1.3: tests behind the differential claim, and untrusted input that can no longer ask for gigabytes

dratify is tagged v0.1.3: the docs said the Python checker and the Rust checker were compared against DRATChecker on acceptances and rejections, but the only two tests that did so had silently skipped on every run — an import-time guard — so that claim had never once been exercised. The new differential suite (2889df3) sweeps 150 random instances plus hand-written accept/reject cases, and CI installs the native checker and fails if the tests skip. The same release hardens the untrusted-input paths: header counts like p cnf 99999999999 0 that would have asked for hundreds of gigabytes are rejected outright, register_native validates the checker it is handed instead of unpacking a fixed tuple, and proof parsing reports the offending line and token. Tests go from 87 to 96 and coverage 84% to 87%, with each new guard confirmed to fail when its fix is reverted.