missions/judge: heavy_certificates (Lean-kernel-only), swap for heavy shards, dispatch filter - #632
Merged
Merged
Conversation
…r heavy shards; dispatch filter #615 run 36076883673, shard judge rvm_bridge 2/4: with the stack limit raised (#625) nanoda no longer overflows on MM_weil_positivity_prime_free_window's exact LDL^T certificates -- it exhausts the 16 GB runner and the runner is killed ("received a shutdown signal") after five other nodes passed. - A node may declare `heavy_certificates = true`. The judge then writes its Comparator config with enable_nanoda = false (Lean kernel replay + axiom whitelist still run), `--configs` gains a sixth column nanoda|lean-kernel-only, MANIFEST.json records `nanoda` per node, the PASS line prints kernel=... - `mission comparator-record` refuses a plain record on such a node and requires --lean-kernel-only, which stores second_kernel = "none: heavy_certificates" in [comparator]; `provenance-report` prints those nodes as "Lean kernel only". Ordinary records are unchanged on disk. - Workflow: a swap step (8 GB on /mnt, 4 GB fallback) runs only in shards that contain a heavy node; MALLOC_ARENA_MAX=2 on the comparator step; a workflow_dispatch may be restricted to one island and shard (inputs island/shard) to re-judge a single node without the whole matrix. - Bundles regenerated (MANIFEST gains `nanoda: true` per node); docs. No node on main is flagged yet: the KWin nodes live on cl/kwin and cl/kwin2 and get `heavy_certificates = true` when this lands. 3 tests. conjecture1_proved = False. Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
…h inputs (job-level if cannot see matrix) Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
DrMurphyIsIn
marked this pull request as ready for review
September 25, 2026 14:24
DrMurphyIsIn
enabled auto-merge
September 25, 2026 14:30
DrMurphyIsIn
pushed a commit
that referenced
this pull request
Sep 25, 2026
…-only) `MM_weil_positivity_prime_free_window` declares `heavy_certificates = true`, so the Comparator judge writes its config with `enable_nanoda = false`: the Lean kernel replay and the export axiom whitelist still run, the second (nanoda) kernel does not. The KWin window certificates need ~16-19 GB per decide, which exhausted the 16 GB runner and killed the whole shard after five nodes (run 36076883673); with the flag, the shard's single heavy node is judged by the Lean kernel alone and the other twelve keep both kernels. Merged main in for the machinery this depends on: #632 (the flag, the swap step for shards containing a heavy node, the dispatch filter, and `comparator-record --lean-kernel-only`) and #625 (`ulimit -s unlimited`). Judge bundle regenerated; `judge --island rvm_bridge --check` matches the registry (53 challenges) and the node's config row now reads `lean-kernel-only`. `mission verify` is OK on all four campaigns. The record itself follows once the restricted shard dispatch passes, as `comparator-record --lean-kernel-only`, which stores `second_kernel = "none: heavy_certificates"` so provenance-report prints "Lean kernel only" rather than staying silent. No Lean source changes; no status change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
DrMurphyIsIn
pushed a commit
that referenced
this pull request
Sep 25, 2026
…l-only) `MM_weil_positivity_window_two_fifths` declares `heavy_certificates = true`, so the Comparator judge writes its config with `enable_nanoda = false`: the Lean kernel replay and the export axiom whitelist still run, the second (nanoda) kernel does not. The L = 1/2 window certificates are the heaviest in the registry (~1100 s and ~16 GB per decide in the local rebuild), well past what a 16 GB runner survives with two kernels. Merged cl/kwin in, which carries main (#632's flag, swap step and dispatch filter, #625's `ulimit -s unlimited`) and the same flag on the prime-free-window node. The two heavy nodes land in different shards -- prime-free in rvm_bridge 2/4, two-fifths in 3/4 -- so each shard has at most one heavy node and gets the swap step only where it is needed. Judge bundle regenerated; `judge --island rvm_bridge --check` matches the registry (54 challenges) and both heavy nodes' config rows read `lean-kernel-only`. `mission verify` is OK on all four campaigns. The records follow once the shards pass, as `comparator-record --lean-kernel-only`. No Lean source changes; no status change; conjecture1_proved = False. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
DrMurphyIsIn
pushed a commit
that referenced
this pull request
Sep 26, 2026
…marker means it Two problems behind the reviewer's messaging nit, one of them a latent trap. The console printed "second kernel: nanoda" and the report spoke of "the recorded second kernel" while the record contained no such field: `second_kernel` defaulted to "nanoda" and is only serialised when it differs, so a legacy record silently ASSERTED that nanoda replayed the export -- which is precisely what its log does not say. A legacy record now carries `second_kernel = "unstated (pre-#632 log)"`, written out, and the report says the log "does not state which second kernel ran" rather than implying someone read it. The trap: `lean_kernel_only` was computed as `second_kernel != "nanoda"`, so ANY other value read as the strong claim that the second kernel was skipped. Writing "unstated" would therefore have made all five legacy records announce themselves as "Lean kernel only (heavy_certificates: nanoda not run)" -- an overstatement of what was checked, in the exact direction this tooling exists to prevent. It now tests the heavy marker itself. Caught by looking at who consumes the field before changing it, not by a test; the new tests pin both halves so it cannot come back. conjecture1_proved = False (unchanged; provenance tooling only). Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU
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.
Follow-up to #625. On #615 run 36076883673 (shard
judge rvm_bridge 2/4), with the stack limit raised, nanoda no longer overflows onMM_weil_positivity_prime_free_window's exact LDL^T certificates: it exhausts the 16 GB runner and the runner is killed ("received a shutdown signal") 5.5 minutes after the fifth node of the shard passed.(1) Per-node second kernel. A node may declare
heavy_certificates = truein its toml. The judge then writes its Comparator config withenable_nanoda = false(the Lean-kernel replay and the export-level axiom whitelist still run),--configsgains a sixth columnnanoda|lean-kernel-only,MANIFEST.jsonrecordsnanodaper node, and the PASS line printskernel=....mission comparator-recordrefuses a plain record on such a node and requires--lean-kernel-only, which storessecond_kernel = "none: heavy_certificates"in[comparator];mission provenance-reportprints those nodes as Lean kernel only. One kernel is a weaker verdict and is labelled as such, never silently. Ordinary records are byte-identical to before.(2) Memory. A swap step (8 GB on
/mnt, 4 GB fallback, warning if neither) runs only in shards that contain a heavy node;MALLOC_ARENA_MAX=2on the comparator step for every shard (cheap). Ordinary shards are untouched.Dispatch filter.
workflow_dispatchtakesislandandshardinputs so one node's shard can be re-judged without the whole matrix.No node on main is flagged yet: the KWin nodes live on cl/kwin and cl/kwin2 and get
heavy_certificates = truethere once this lands (their bundles are regenerated bypython -m telperion.missions.judge --island rvm_bridge). Bundles on main regenerated (MANIFESTnanoda: trueper node). 3 new tests; missions battery 312 passed.conjecture1_proved = False.Test result. Throwaway branch
ci/judge-heavy-kwin-test(= cl/kwin + this branch +heavy_certificates = trueonMM_weil_positivity_prime_free_window, 53-node bundle regenerated), dispatched withisland=rvm_bridge shard=2/4: run 36138838236, conclusion success.planselected exactly one shard;judge rvm_bridge 2/4ran 13 nodes, 13/13 PASS, wall time 66m38s (13:09:54 to 14:16:32 UTC).extra swap enabled: /mnt/arda-judge.swap(swap total 3071 MB before, 11263 MB after);stack limit (KB): unlimited;MALLOC_ARENA_MAX=2.COMPARATOR PASS island=rvm_bridge node=MM_weil_positivity_prime_free_window theorem=weil_positivity_prime_free_window run=36138838236 kernel=lean-kernel-only, with "Lean default kernel accepts the solution"; the other 12 nodes reportkernel=nanodawith both kernels accepting.lakebwrapper's[res ...]lines would be the model if wanted).Compare the same shard on mirrormere: the full prime-free window (2L <= log 2) proved kernel-native, hypothesis-free, no Arb seam (draft; includes #606; grant after #607) #615's run 36076883673 before this change: 5 passes, then the runner was killed on this node.
🤖 Generated with Claude Code
https://claude.ai/code/session_017icTazCuXLgRx61VNRAZWU