feat(proofs): Tier 1 — comparisons (lt/gt/le/ge) + div/mod with panic#81
Merged
Conversation
Extends the verified type safety (machine-checked under Lean 4.30.0 by the lean-proofs CI gate; sorry-free, no axioms; theorem statements unchanged). - Ordering comparisons `lt`/`gt`/`le`/`ge` (integer → bool, computed via `decide (n₁ < n₂)` etc.) — HasType + Step + full progress/preservation. - Integer `div`/`mod` with divide-by-zero PANIC: a zero divisor steps to `error` (reusing the proven unwrap-of-oops panic fragment); progress splits on `n₂ = 0` via `by_cases`, preservation types the `error` via `tError`. Integer arithmetic (add/sub/mul/div/mod), all comparisons (eq/lt/gt/le/ge), and logical (and/or) are now complete. Remaining Tier 1: float variants + arrays. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
hyperpolymath
marked this pull request as ready for review
June 14, 2026 10:55
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
2 participants
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.
Summary
Continues extending the verified WokeLang type-safety proofs (machine-checked under Lean 4.30.0 by the
lean-proofsCI gate; sorry-free, no axioms, theorem statements unchanged).Tier 1 — operators added
Each with a
HasTyperule +Steprule(s) and fullprogress/preservationcoverage:lt,gt,le,ge— integer →bool, computed viadecide (n₁ < n₂)etc. (noby_casesneeded).div/modwith divide-by-zero PANIC — a zero divisor steps toerror(reusing the provenunwrap-of-oopspanic fragment).progresssplits onn₂ = 0viaby_cases;preservationtypes the resultingerrorat any type viatError.With this, integer arithmetic (
add/sub/mul/div/mod), all comparisons (eq/lt/gt/le/ge), and logical (and/or) are complete.Verification
Remaining Tier 1
Float arithmetic variants (
sub/mul/divonfloat, mirroringadd) andarraytyping/evaluation — documented inAUDIT.md.https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
Generated by Claude Code