Native MiniSat differential oracle harness for the ladder and corpus - #109
Merged
Conversation
Check each corpus/fixture and selected odd torus against native MiniSat's answer, then compare pinned v0.43.0 EMS-VM/AOT stdout byte for byte except the trailing timing field. Stage the AOT source/build under /tmp. Make missing reports, failed commands, timeouts and zero selections fail by name. Plant input corruption on the EMS arm, a wrong verdict, perturbed AOT bytes, zero instances, a timeout and empty output through the production checks. Removing each main comparator makes its own selftests MISS. Document the entry point and preserve the captured validation transcript. Measured validation (current default CDCL policies, regime C): SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20 SELFTEST ALL RED caught=6 expected=6 (intentional exit 1) MUTATION DONE control=1 disabled-comparators=3 CONFIG DONE checked=8 Search-gap table copied from the clean run (single-run counters): rung EMS_conflicts native_conflicts native_CPU_s native/EMS 3x3 592 731 0.004883 1.235x 4x4 9986 84150 0.22611 8.427x 5x5 EMS-VM hit the 120-second cap, so the default selects 3x3 and 4x4 and explicitly budget-skips the other standard rungs. Cold AOT build time also exceeds the brief's total fast-run target. Native MiniSat rejects SATLIB percent trailers; announce their removal and give identical temporary formula text to all three arms. Solver/emitter sources unchanged. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kpzyjv1SaLaqBf45FSFDhB
An emitter regression replacing the requested columns with 3 made the oracle report a 4x3 torus as 4x4 and exit 0. Verify each rung's full ordered DIMACS torus encoding, compare 3x3 directly to the existing CNF fixture, and preflight every ladder lane against full 3x3/4x4 regime-C output banks. Requested anchors reuse those solves; unrequested anchors are explicitly reported and excluded from the search-gap table. Under auto, a present but unbuildable AOT toolchain now emits a named skip and continues native MiniSat/EMS-VM checking with zero AOT passes. Explicit on still fails. Add the seventh resized-emitter plant and supporting controls for the independent fixture/regime checks, auto/on build failure, stale AOT state, and each coverage count. Keep solver/emitter code unchanged. Stage normalization output under /tmp even when controls read banked files. Reproduced before (exit 0): 4x4 4127 1565 0.005985 0.379x SUMMARY PASS selected=2 passed=2 native=2 VM=2 AOT=0 Same emitter regression after (exit 1): FAIL 4x4 [rung-identity]: expected p cnf 32 128; got p cnf 24 96 Clean run with fresh AOT build (exit 0): PREFLIGHT 3x3: PASS (regime C, byte-exact EMS-VM output excluding ms) PREFLIGHT 4x4: PASS (regime C, byte-exact EMS-VM output excluding ms) rung EMS_conflicts native_conflicts native_CPU_s native/EMS 3x3 592 731 0.00176 1.235x 4x4 9986 84150 0.223485 8.427x SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20 Final-source clean repeat with the freshly built binary (exit 0): rung EMS_conflicts native_conflicts native_CPU_s native/EMS 3x3 592 731 0.003798 1.235x 4x4 9986 84150 0.223714 8.427x SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20 Planted-fault verification: CONTROLS checked=15 expected=15 missed=0 SELFTEST ALL RED caught=7 expected=7 (intentional exit 1) MUTATION DONE control=1 mutations=7 EXTRA DONE identity-positive=7 identity-negative=1 configuration=7 isolated-coverage-mutation=1 Gutting each new comparator produces its own MISS and exit 2. Removing only the original coverage assertion makes passed/native/VM controls MISS while the separate AOT coverage control stays green. Auto/on also checked for build timeout and missing executable. Full commands and captured output are recorded in benchmarks/NATIVE_ORACLE_ROUND2.md. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kpzyjv1SaLaqBf45FSFDhB
Removing the production regime comparison previously left all selftests RED because controls called the helper directly. Each case now launches the current harness file through its normal CLI. Comparator fault probes select nonempty rungs and real file instances; a separate case tests an empty selection. Fault injection changes data, outputs, or accounting state; the production path must detect it. Distinct discovery/completion names prevent one vacuity check from concealing removal of the other. Filtered selftests are labeled partial; a zero-case selection fails. Anchor 4x4 to an ordered CNF captured from the unchanged EigenScript emitter, independently of the awk model, alongside the existing 3x3 fixture. Correct the ordering rationale: the measured 3x3 vertex-block swap leaves normalized VM output identical to the regime bank, while the identity gate rejects it. Input open/read/trailer failures now have separate names. Forward caller-supplied timeouts to selftest children. Solver, emitter, and existing regime banks remain unchanged. Ordering repro: reordered normalized-vs-bank=IDENTICAL FAIL 3x3 [rung-identity]: token 41: expected -2; got -3 Clean run, AOT_BINARY=/tmp/ems_aot, exit 0: IDENTITY 3x3: PASS (header, every ordered literal and clause, odd charge) IDENTITY 3x3: PASS (banked repository fixture, ordered DIMACS tokens) PREFLIGHT 3x3: PASS (regime C, byte-exact EMS-VM output excluding ms) IDENTITY 4x4: PASS (header, every ordered literal and clause, odd charge) IDENTITY 4x4: PASS (banked repository fixture, ordered DIMACS tokens) PREFLIGHT 4x4: PASS (regime C, byte-exact EMS-VM output excluding ms) rung EMS_conflicts native_conflicts native_CPU_s native/EMS 3x3 592 731 0.002613 1.235x 4x4 9986 84150 0.226566 8.427x SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20 Full --selftest, intentional exit 1: SELFTEST ALL RED checked=24 expected=24 caught=22 controls=2 (intentional exit 1) CALL-SITE MUTATIONS checked=13 missed=0 BOUNDARIES checked=13 unexpected=0 Each of the 13 production call-site deletions yielded its own MISS and exit 2, including the final-source regime deletion repeat. The 4x4 input anchor also rejects a resized emitter with the identity model disabled. chmod 000 now fails as input-open; actual trailer junk is input-trailer. The caller's --timeout 1 now reaches the child and yields a named rc=124 failure, never a completed control. Final default clean/full selftest were rerun after that correction. Commands, mutation driver, and captured output are in benchmarks/NATIVE_ORACLE_ROUND3.md. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kpzyjv1SaLaqBf45FSFDhB
Check prepared DIMACS against the source with an independent parser before any solver runs. Preserve ordered formula tokens modulo the documented SATLIB trailer/whitespace handling and validate header counts and literals. Derive production fail sites from the actual harness source. Require case enrollment in both directions and runtime witnesses for eligible sites. Cases now check the complete subject, class, evidence and printed diagnostic. Add real trailer controls, normalization corruption and uncovered/removed gate plants. Limit the 4x4 emitter capture claim to bank/model drift checks. Validation (sequential, AOT_BINARY=/tmp/ems_aot; no real AOT rebuild): AOT_BINARY=/tmp/ems_aot KEEP_WORK=1 benchmarks/run_native_oracle.sh SEARCH GAP (measurement only; native conflicts / EMS conflicts, not a speed ratio) rung EMS_conflicts native_conflicts native_CPU_s native/EMS 3x3 592 731 0.003254 1.235x 4x4 9986 84150 0.226753 8.427x SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20 EXIT=0 AOT_BINARY=/tmp/ems_aot KEEP_WORK=1 benchmarks/run_native_oracle.sh --selftest ENROLLMENT derived=48 enrolled=48 (actual production source) SELFTEST normalization-corruption: RED (production CLI rc=1; exact subject/class/evidence) FAIL tseitin-3x3-odd [input-preservation]: ordered DIMACS tokens changed during shared preparation CONTROL satlib-trailers: PASS (production CLI rc=0; exact report) SELFTEST enrollment: RED (production CLI rc=2; exact subject/class/evidence) FAIL harness [enrollment]: uncovered production sites: uncovered_gate:1 FAIL harness [enrollment]: cases reference absent production sites: execution_failed:1 WITNESSES observed=48 eligible=48 SELFTEST ALL RED checked=68 caught=65 controls=3 skipped=0 (intentional exit 1) EXIT=1 MUTATION AUDIT production-calls=28 failure-sites=48 all-MISS=yes all-exit=2 Mutations: deleting each of 48 derived failure expressions and 28 production calls gave MISS + exit 2. Wrong-name, class-swap and wrong-evidence mutations also gave MISS + exit 2. Gutting the normalization injection, rejecting all SATLIB trailers, and disabling either enrollment direction gave MISS + exit 2. ANCHOR SWEEP cases=1288 model-rejected=1160 model-accepted=128 accepted-only-0-to-minus0=yes bank-rejected-model-accepted=128 Full commands/output and mutation drivers: benchmarks/NATIVE_ORACLE_ROUND4.md. Solver, libraries, emitter and existing fixtures are untouched. Larger standard ladder rungs remain budget-skipped and opt-in. Python 3 stdlib is now required for input preservation and selftest enrollment. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kpzyjv1SaLaqBf45FSFDhB
Reject CNF preparation that moves a literal onto the header: require a four-token header and preserve ordered token tuples per LF-delimited data line. Add the exact header-line-merge plant and document the guarantee. Follow source/. edges recursively when deriving failure sites. Record the source filename in failure witnesses, enroll the existing unknown-plant guard, and add a two-edge sourced-gate plant. Both original enrollment membership directions remain tested. Measured sequentially with AOT_BINARY=/tmp/ems_aot, no AOT rebuild: SEARCH GAP (measurement only; native conflicts / EMS conflicts, not a speed ratio) rung EMS_conflicts native_conflicts native_CPU_s native/EMS 3x3 592 731 0.001778 1.235x 4x4 9986 84150 0.239762 8.427x SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20 clean exit=0 ENROLLMENT derived=49 enrolled=49 (production source graph) SELFTEST unknown-plant: RED (production CLI rc=1; exact subject/class/evidence) SELFTEST header-line-merge: RED (production CLI rc=1; exact subject/class/evidence) FAIL tseitin-3x3-odd [input-preservation]: prepared: DIMACS header must occupy its own four-token line SELFTEST enrollment: RED (production CLI rc=2; exact subject/class/evidence) SELFTEST enrollment-sourced: RED (production CLI rc=2; exact subject/class/evidence) WITNESSES observed=49 eligible=49 SELFTEST ALL RED checked=71 caught=68 controls=3 skipped=0 (intentional exit 1) selftest exit=1 (intentional) The production-awk header-merge repro exits 1 by [input-preservation]. The same merged CNF passes the baseline checker (rc=0) and fails the fixed checker (rc=1: prepared: DIMACS header must occupy its own four-token line). Restoring the flattened checker or disabling recursive source traversal makes the corresponding new case MISS, exit 2. Full commands and output: benchmarks/NATIVE_ORACLE_ROUND5.md. No solver, emitter, or fixture changes. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Kpzyjv1SaLaqBf45FSFDhB
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Adds
benchmarks/run_native_oracle.sh— a repeatable harness that checks EigenMiniSat against two independent oracles per instance, plus a planted-fault--selftest.What it checks
/usr/bin/minisat; EMS's verdict must agree. This is a cross-implementation answer oracle, not a self-comparison.ms=field).--aot autodegrades with a named SKIP if the toolchain is absent or unbuildable;--aot onhard-fails.[input-preservation]guards it without relying on agreement.Validation
Clean run:
SUMMARY PASS selected=20 passed=20 native=20 VM=20 AOT=20, exit 0.--selftestdrives every case through the production CLI and reds each planted fault; failure sites are derived from the production source graph (derived=49 enrolled=49), so a gate with no case, or a case naming an absent site, fails by construction. Mutation audit: deleting any production call site, gutting any injection, or altering a reported subject/class/evidence yields MISS + exit 2.Built over five blind-critic rounds (two model families). Findings that shaped it, each caught by a critic and fixed: a rung was never verified to be the instance it named (a one-line emitter regression passed at exit 0 with the search gap wrong by 22x); controls invoked helpers instead of production, so a check could be unplugged with the selftest still green; a rationale falsified by measurement; the preparation stage had no coverage and could silently strengthen the formula; and the post-condition's flattened comparison was blind to line structure (EMS's parser discards post-header tokens, native MiniSat does not).
Known scope: rungs above 4x4 are budget-skipped and opt-in. The 4x4 anchor is captured from the emitter it validates, so it detects drift and bank corruption, not initial emitter correctness — stated as such in the docs.
🤖 Generated with Claude Code
https://claude.ai/code/session_01Kpzyjv1SaLaqBf45FSFDhB