fix(checker): replay what the kernel proves in user programs - #215
Merged
the-homeless-god merged 7 commits intoOct 1, 2026
Merged
Conversation
On a set of 14 short user programs the kernel proves 28 places and the checker replayed 13; now it replays 26. Seven readings, all rules already in the ledger or evaluator equations: a goal closed by the checked promise of a called function, a result field of a written record, the any-case branch, a closed statement, the run line under a closed statement, N11, N7 with a length step, N3 for declared floors, a lower bound above zero. Adds the user-program probe plan with a CI step and 27 checker probes. Code lines 7711 -> 7788, ceiling raised by exactly that. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The checker now narrows a dependency set by the importers' "only" lists, so a hidden namesake no longer collides (tls, tls-handshake), looks up a type declared in a visible module of the set (hmac, postgres, redis) and declines instead of lying when no set is given. The share runner passes each record the transitive dependency set. With a set, stdlib code 1 goes from 5 of 49 to 0 of 49. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Measured counts follow the rebase onto the user-program checker work; its new probe files get their proved-share ledger lines and their English file name words, so the pre-push hook is green. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
The probes of tasks 2748 and 4573 are now rows of probes.tsv, and the forgery-probe ratchet follows the measured count, 572 to 596. Counts quoted in prose and the tree inventory are re-measured after the rebase onto dev. Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PNHrA3rG7FTWhB11E7pjDQ
the-homeless-god
force-pushed
the
a/4573-checker-reads-module-types-and-dependency-sets
branch
from
October 1, 2026 22:48
8949cbe to
be7b87e
Compare
the-homeless-god
deleted the
a/4573-checker-reads-module-types-and-dependency-sets
branch
October 1, 2026 22:59
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.
Verified on the tree of dev plus this branch (8949cbe): the checker test set passes, the provability verdict is green with all four checks, the proved-share ledger and the rule tables agree with the tree, pre-push is green, commit messages follow the convention.
🤖 Generated with Claude Code