Skip to content

Commit b244755

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(proofs): Tier 1 — comparisons (lt/gt/le/ge) + div/mod with panic (#81)
## Summary Continues extending the verified WokeLang type-safety proofs (machine-checked under Lean 4.30.0 by the `lean-proofs` CI gate; **sorry-free, no axioms, theorem statements unchanged**). ## Tier 1 — operators added Each with a `HasType` rule + `Step` rule(s) and full `progress`/`preservation` coverage: - **Ordering comparisons** `lt`, `gt`, `le`, `ge` — integer → `bool`, computed via `decide (n₁ < n₂)` etc. (no `by_cases` needed). - **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 resulting `error` at any type via `tError`. With this, **integer arithmetic (`add/sub/mul/div/mod`), all comparisons (`eq/lt/gt/le/ge`), and logical (`and/or`)** are complete. ## Verification ``` $ lean docs/proofs/verification/WokeLang.lean # exit 0, sorry-free ``` ## Remaining Tier 1 Float arithmetic variants (`sub`/`mul`/`div` on `float`, mirroring `add`) and `array` typing/evaluation — documented in `AUDIT.md`. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7 --- _Generated by [Claude Code](https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent da35ff4 commit b244755

2 files changed

Lines changed: 248 additions & 5 deletions

File tree

‎docs/proofs/verification/AUDIT.md‎

Lines changed: 10 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -139,12 +139,17 @@ theorems (`weaken_collapses_distinction`, `affine_canonical`,
139139

140140
## Extensions landed (2026-06-14)
141141

142-
- **Tier 1 (base operators):** `or` (logical), `sub`/`mul` (integer) — each
143-
with `HasType` + `Step` rules and full `progress`/`preservation` coverage.
142+
- **Tier 1 (base operators)** — each with `HasType` + `Step` rules and full
143+
`progress`/`preservation` coverage:
144+
- logical: `or`;
145+
- integer arithmetic: `sub`, `mul`, `div`, `mod` — where `div`/`mod` panic on
146+
a zero divisor (step to `error`, reusing the proven `unwrap`-of-`oops`
147+
panic fragment);
148+
- ordering comparisons: `lt`, `gt`, `le`, `ge` (integer → `bool`, via
149+
`decide`).
144150
- **Tier 3 (capability):** `capSubsumes` is a preorder (`_refl`, `_trans`).
145-
- Still open in Tier 1: ordering comparisons (`lt`/`gt`/`le`/`ge`), `div`/`mod`
146-
(with divide-by-zero → `error` panic, reusing the proven panic fragment),
147-
float variants, and `array` typing.
151+
- Still open in Tier 1: **float** arithmetic variants (`sub`/`mul`/`div` on
152+
`float`, mirroring `add` on float) and **`array`** typing/evaluation.
148153

149154
## Status
150155

‎docs/proofs/verification/WokeLang.lean‎

Lines changed: 238 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -183,6 +183,24 @@ inductive HasType : TypeEnv → Expr → WokeType → Prop where
183183
| tMulInt : ∀ Γ e₁ e₂,
184184
HasType Γ e₁ .int → HasType Γ e₂ .int →
185185
HasType Γ (.binOp .mul e₁ e₂) .int
186+
| tLt : ∀ Γ e₁ e₂,
187+
HasType Γ e₁ .int → HasType Γ e₂ .int →
188+
HasType Γ (.binOp .lt e₁ e₂) .bool
189+
| tGt : ∀ Γ e₁ e₂,
190+
HasType Γ e₁ .int → HasType Γ e₂ .int →
191+
HasType Γ (.binOp .gt e₁ e₂) .bool
192+
| tLe : ∀ Γ e₁ e₂,
193+
HasType Γ e₁ .int → HasType Γ e₂ .int →
194+
HasType Γ (.binOp .le e₁ e₂) .bool
195+
| tGe : ∀ Γ e₁ e₂,
196+
HasType Γ e₁ .int → HasType Γ e₂ .int →
197+
HasType Γ (.binOp .ge e₁ e₂) .bool
198+
| tDivInt : ∀ Γ e₁ e₂,
199+
HasType Γ e₁ .int → HasType Γ e₂ .int →
200+
HasType Γ (.binOp .div e₁ e₂) .int
201+
| tModInt : ∀ Γ e₁ e₂,
202+
HasType Γ e₁ .int → HasType Γ e₂ .int →
203+
HasType Γ (.binOp .mod e₁ e₂) .int
186204
| tNegInt : ∀ Γ e,
187205
HasType Γ e .int →
188206
HasType Γ (.unOp .neg e) .int
@@ -262,6 +280,30 @@ inductive Step : Expr → Env → Expr → Env → Prop where
262280
| sMulInt : ∀ n₁ n₂ ρ,
263281
Step (.binOp .mul (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
264282
(.lit (.vInt (n₁ * n₂))) ρ
283+
| sLt : ∀ n₁ n₂ ρ,
284+
Step (.binOp .lt (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
285+
(.lit (.vBool (decide (n₁ < n₂)))) ρ
286+
| sGt : ∀ n₁ n₂ ρ,
287+
Step (.binOp .gt (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
288+
(.lit (.vBool (decide (n₁ > n₂)))) ρ
289+
| sLe : ∀ n₁ n₂ ρ,
290+
Step (.binOp .le (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
291+
(.lit (.vBool (decide (n₁ ≤ n₂)))) ρ
292+
| sGe : ∀ n₁ n₂ ρ,
293+
Step (.binOp .ge (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
294+
(.lit (.vBool (decide (n₁ ≥ n₂)))) ρ
295+
| sDivInt : ∀ n₁ n₂ ρ, n₂ ≠ 0 →
296+
Step (.binOp .div (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
297+
(.lit (.vInt (n₁ / n₂))) ρ
298+
| sDivZero : ∀ n₁ n₂ ρ, n₂ = 0 →
299+
Step (.binOp .div (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
300+
(.error "Division by zero") ρ
301+
| sModInt : ∀ n₁ n₂ ρ, n₂ ≠ 0 →
302+
Step (.binOp .mod (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
303+
(.lit (.vInt (n₁ % n₂))) ρ
304+
| sModZero : ∀ n₁ n₂ ρ, n₂ = 0 →
305+
Step (.binOp .mod (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
306+
(.error "Modulo by zero") ρ
265307
| sUnOpCong : ∀ op e e' ρ ρ',
266308
Step e ρ e' ρ' →
267309
Step (.unOp op e) ρ (.unOp op e') ρ'
@@ -554,6 +596,154 @@ theorem progress : ∀ e t,
554596
| inr hstp =>
555597
obtain ⟨e₁', ρ', hs₁⟩ := hstp
556598
exact ⟨.binOp .mul e₁' e₂, ρ', .sBinOpLeft .mul _ e₁' e₂ emptyEnv ρ' hs₁⟩
599+
| tLt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
600+
right
601+
cases ih₁ with
602+
| inl hv₁ =>
603+
cases hv₁ with
604+
| lit v₁ =>
605+
cases ih₂ with
606+
| inl hv₂ =>
607+
cases hv₂ with
608+
| lit v₂ =>
609+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
610+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
611+
subst hn₁; subst hn₂
612+
exact ⟨.lit (.vBool (decide (n₁ < n₂))), emptyEnv, .sLt n₁ n₂ emptyEnv⟩
613+
| error msg =>
614+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .lt v₁ msg emptyEnv⟩
615+
| inr hstp =>
616+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
617+
exact ⟨.binOp .lt (.lit v₁) e₂', ρ', .sBinOpRight .lt v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
618+
| error msg =>
619+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .lt msg e₂ emptyEnv⟩
620+
| inr hstp =>
621+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
622+
exact ⟨.binOp .lt e₁' e₂, ρ', .sBinOpLeft .lt _ e₁' e₂ emptyEnv ρ' hs₁⟩
623+
| tGt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
624+
right
625+
cases ih₁ with
626+
| inl hv₁ =>
627+
cases hv₁ with
628+
| lit v₁ =>
629+
cases ih₂ with
630+
| inl hv₂ =>
631+
cases hv₂ with
632+
| lit v₂ =>
633+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
634+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
635+
subst hn₁; subst hn₂
636+
exact ⟨.lit (.vBool (decide (n₁ > n₂))), emptyEnv, .sGt n₁ n₂ emptyEnv⟩
637+
| error msg =>
638+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .gt v₁ msg emptyEnv⟩
639+
| inr hstp =>
640+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
641+
exact ⟨.binOp .gt (.lit v₁) e₂', ρ', .sBinOpRight .gt v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
642+
| error msg =>
643+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .gt msg e₂ emptyEnv⟩
644+
| inr hstp =>
645+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
646+
exact ⟨.binOp .gt e₁' e₂, ρ', .sBinOpLeft .gt _ e₁' e₂ emptyEnv ρ' hs₁⟩
647+
| tLe e₁ e₂ h₁ h₂ ih₁ ih₂ =>
648+
right
649+
cases ih₁ with
650+
| inl hv₁ =>
651+
cases hv₁ with
652+
| lit v₁ =>
653+
cases ih₂ with
654+
| inl hv₂ =>
655+
cases hv₂ with
656+
| lit v₂ =>
657+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
658+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
659+
subst hn₁; subst hn₂
660+
exact ⟨.lit (.vBool (decide (n₁ ≤ n₂))), emptyEnv, .sLe n₁ n₂ emptyEnv⟩
661+
| error msg =>
662+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .le v₁ msg emptyEnv⟩
663+
| inr hstp =>
664+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
665+
exact ⟨.binOp .le (.lit v₁) e₂', ρ', .sBinOpRight .le v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
666+
| error msg =>
667+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .le msg e₂ emptyEnv⟩
668+
| inr hstp =>
669+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
670+
exact ⟨.binOp .le e₁' e₂, ρ', .sBinOpLeft .le _ e₁' e₂ emptyEnv ρ' hs₁⟩
671+
| tGe e₁ e₂ h₁ h₂ ih₁ ih₂ =>
672+
right
673+
cases ih₁ with
674+
| inl hv₁ =>
675+
cases hv₁ with
676+
| lit v₁ =>
677+
cases ih₂ with
678+
| inl hv₂ =>
679+
cases hv₂ with
680+
| lit v₂ =>
681+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
682+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
683+
subst hn₁; subst hn₂
684+
exact ⟨.lit (.vBool (decide (n₁ ≥ n₂))), emptyEnv, .sGe n₁ n₂ emptyEnv⟩
685+
| error msg =>
686+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .ge v₁ msg emptyEnv⟩
687+
| inr hstp =>
688+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
689+
exact ⟨.binOp .ge (.lit v₁) e₂', ρ', .sBinOpRight .ge v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
690+
| error msg =>
691+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .ge msg e₂ emptyEnv⟩
692+
| inr hstp =>
693+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
694+
exact ⟨.binOp .ge e₁' e₂, ρ', .sBinOpLeft .ge _ e₁' e₂ emptyEnv ρ' hs₁⟩
695+
| tDivInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
696+
right
697+
cases ih₁ with
698+
| inl hv₁ =>
699+
cases hv₁ with
700+
| lit v₁ =>
701+
cases ih₂ with
702+
| inl hv₂ =>
703+
cases hv₂ with
704+
| lit v₂ =>
705+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
706+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
707+
subst hn₁; subst hn₂
708+
by_cases hz : n₂ = 0
709+
· exact ⟨.error "Division by zero", emptyEnv, .sDivZero n₁ n₂ emptyEnv hz⟩
710+
· exact ⟨.lit (.vInt (n₁ / n₂)), emptyEnv, .sDivInt n₁ n₂ emptyEnv hz⟩
711+
| error msg =>
712+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .div v₁ msg emptyEnv⟩
713+
| inr hstp =>
714+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
715+
exact ⟨.binOp .div (.lit v₁) e₂', ρ', .sBinOpRight .div v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
716+
| error msg =>
717+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .div msg e₂ emptyEnv⟩
718+
| inr hstp =>
719+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
720+
exact ⟨.binOp .div e₁' e₂, ρ', .sBinOpLeft .div _ e₁' e₂ emptyEnv ρ' hs₁⟩
721+
| tModInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
722+
right
723+
cases ih₁ with
724+
| inl hv₁ =>
725+
cases hv₁ with
726+
| lit v₁ =>
727+
cases ih₂ with
728+
| inl hv₂ =>
729+
cases hv₂ with
730+
| lit v₂ =>
731+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
732+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
733+
subst hn₁; subst hn₂
734+
by_cases hz : n₂ = 0
735+
· exact ⟨.error "Modulo by zero", emptyEnv, .sModZero n₁ n₂ emptyEnv hz⟩
736+
· exact ⟨.lit (.vInt (n₁ % n₂)), emptyEnv, .sModInt n₁ n₂ emptyEnv hz⟩
737+
| error msg =>
738+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .mod v₁ msg emptyEnv⟩
739+
| inr hstp =>
740+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
741+
exact ⟨.binOp .mod (.lit v₁) e₂', ρ', .sBinOpRight .mod v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
742+
| error msg =>
743+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .mod msg e₂ emptyEnv⟩
744+
| inr hstp =>
745+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
746+
exact ⟨.binOp .mod e₁' e₂, ρ', .sBinOpLeft .mod _ e₁' e₂ emptyEnv ρ' hs₁⟩
557747
| tNegInt e h₁ ih =>
558748
right
559749
cases ih with
@@ -676,6 +866,12 @@ theorem preservation : ∀ e e' t ρ ρ',
676866
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ (ih _ h₁) h₂
677867
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ (ih _ h₁) h₂
678868
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ (ih _ h₁) h₂
869+
| tLt _ _ h₁ h₂ => exact .tLt _ _ _ (ih _ h₁) h₂
870+
| tGt _ _ h₁ h₂ => exact .tGt _ _ _ (ih _ h₁) h₂
871+
| tLe _ _ h₁ h₂ => exact .tLe _ _ _ (ih _ h₁) h₂
872+
| tGe _ _ h₁ h₂ => exact .tGe _ _ _ (ih _ h₁) h₂
873+
| tDivInt _ _ h₁ h₂ => exact .tDivInt _ _ _ (ih _ h₁) h₂
874+
| tModInt _ _ h₁ h₂ => exact .tModInt _ _ _ (ih _ h₁) h₂
679875
| sBinOpRight op v₁ e₂ e₂' ρ ρ' _hv hs₂ ih =>
680876
cases ht with
681877
| tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih _ h₂)
@@ -686,6 +882,12 @@ theorem preservation : ∀ e e' t ρ ρ',
686882
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ h₁ (ih _ h₂)
687883
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ h₁ (ih _ h₂)
688884
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ h₁ (ih _ h₂)
885+
| tLt _ _ h₁ h₂ => exact .tLt _ _ _ h₁ (ih _ h₂)
886+
| tGt _ _ h₁ h₂ => exact .tGt _ _ _ h₁ (ih _ h₂)
887+
| tLe _ _ h₁ h₂ => exact .tLe _ _ _ h₁ (ih _ h₂)
888+
| tGe _ _ h₁ h₂ => exact .tGe _ _ _ h₁ (ih _ h₂)
889+
| tDivInt _ _ h₁ h₂ => exact .tDivInt _ _ _ h₁ (ih _ h₂)
890+
| tModInt _ _ h₁ h₂ => exact .tModInt _ _ _ h₁ (ih _ h₂)
689891
| sAddInt n₁ n₂ _ =>
690892
cases ht with
691893
| tAddInt _ _ h₁ h₂ => exact .tInt _ _
@@ -719,6 +921,30 @@ theorem preservation : ∀ e e' t ρ ρ',
719921
| sMulInt n₁ n₂ _ =>
720922
cases ht with
721923
| tMulInt _ _ h₁ h₂ => exact .tInt _ _
924+
| sLt n₁ n₂ _ =>
925+
cases ht with
926+
| tLt _ _ h₁ h₂ => exact .tBool _ _
927+
| sGt n₁ n₂ _ =>
928+
cases ht with
929+
| tGt _ _ h₁ h₂ => exact .tBool _ _
930+
| sLe n₁ n₂ _ =>
931+
cases ht with
932+
| tLe _ _ h₁ h₂ => exact .tBool _ _
933+
| sGe n₁ n₂ _ =>
934+
cases ht with
935+
| tGe _ _ h₁ h₂ => exact .tBool _ _
936+
| sDivInt n₁ n₂ _ _ =>
937+
cases ht with
938+
| tDivInt _ _ h₁ h₂ => exact .tInt _ _
939+
| sDivZero n₁ n₂ _ _ =>
940+
cases ht with
941+
| tDivInt _ _ h₁ h₂ => exact .tError _ _ _
942+
| sModInt n₁ n₂ _ _ =>
943+
cases ht with
944+
| tModInt _ _ h₁ h₂ => exact .tInt _ _
945+
| sModZero n₁ n₂ _ _ =>
946+
cases ht with
947+
| tModInt _ _ h₁ h₂ => exact .tError _ _ _
722948
| sNegInt n _ =>
723949
cases ht with
724950
| tNegInt _ h₁ => exact .tInt _ _
@@ -774,6 +1000,12 @@ theorem preservation : ∀ e e' t ρ ρ',
7741000
| tOr _ _ h₁ h₂ => exact .tError _ msg _
7751001
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
7761002
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
1003+
| tLt _ _ h₁ h₂ => exact .tError _ msg _
1004+
| tGt _ _ h₁ h₂ => exact .tError _ msg _
1005+
| tLe _ _ h₁ h₂ => exact .tError _ msg _
1006+
| tGe _ _ h₁ h₂ => exact .tError _ msg _
1007+
| tDivInt _ _ h₁ h₂ => exact .tError _ msg _
1008+
| tModInt _ _ h₁ h₂ => exact .tError _ msg _
7771009
| sBinOpErrRight op v₁ msg _ =>
7781010
cases ht with
7791011
| tAddInt _ _ h₁ h₂ => exact .tError _ msg _
@@ -784,6 +1016,12 @@ theorem preservation : ∀ e e' t ρ ρ',
7841016
| tOr _ _ h₁ h₂ => exact .tError _ msg _
7851017
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
7861018
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
1019+
| tLt _ _ h₁ h₂ => exact .tError _ msg _
1020+
| tGt _ _ h₁ h₂ => exact .tError _ msg _
1021+
| tLe _ _ h₁ h₂ => exact .tError _ msg _
1022+
| tGe _ _ h₁ h₂ => exact .tError _ msg _
1023+
| tDivInt _ _ h₁ h₂ => exact .tError _ msg _
1024+
| tModInt _ _ h₁ h₂ => exact .tError _ msg _
7871025
| sUnOpErr op msg _ =>
7881026
cases ht with
7891027
| tNegInt _ h₁ => exact .tError _ msg _

0 commit comments

Comments
 (0)