Skip to content

feat(proofs): Tier 1 — comparisons (lt/gt/le/ge) + div/mod with panic #81

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
hyperpolymath merged 1 commit into from
Jun 14, 2026
Merged

feat(proofs): Tier 1 — comparisons (lt/gt/le/ge) + div/mod with panic #81

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
1 commit
Select commit
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
15 changes: 10 additions & 5 deletions docs/proofs/verification/AUDIT.md
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -139,12 +139,17 @@ theorems (`weaken_collapses_distinction`, `affine_canonical`,

## Extensions landed (2026-06-14)

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

## Status

Expand Down
238 changes: 238 additions & 0 deletions docs/proofs/verification/WokeLang.lean
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -183,6 +183,24 @@ inductive HasType : TypeEnv → Expr → WokeType → Prop where
| tMulInt : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .mul e₁ e₂) .int
| tLt : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .lt e₁ e₂) .bool
| tGt : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .gt e₁ e₂) .bool
| tLe : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .le e₁ e₂) .bool
| tGe : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .ge e₁ e₂) .bool
| tDivInt : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .div e₁ e₂) .int
| tModInt : ∀ Γ e₁ e₂,
HasType Γ e₁ .int → HasType Γ e₂ .int →
HasType Γ (.binOp .mod e₁ e₂) .int
| tNegInt : ∀ Γ e,
HasType Γ e .int →
HasType Γ (.unOp .neg e) .int
Expand Down Expand Up @@ -262,6 +280,30 @@ inductive Step : Expr → Env → Expr → Env → Prop where
| sMulInt : ∀ n₁ n₂ ρ,
Step (.binOp .mul (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vInt (n₁ * n₂))) ρ
| sLt : ∀ n₁ n₂ ρ,
Step (.binOp .lt (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vBool (decide (n₁ < n₂)))) ρ
| sGt : ∀ n₁ n₂ ρ,
Step (.binOp .gt (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vBool (decide (n₁ > n₂)))) ρ
| sLe : ∀ n₁ n₂ ρ,
Step (.binOp .le (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vBool (decide (n₁ ≤ n₂)))) ρ
| sGe : ∀ n₁ n₂ ρ,
Step (.binOp .ge (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vBool (decide (n₁ ≥ n₂)))) ρ
| sDivInt : ∀ n₁ n₂ ρ, n₂ ≠ 0 →
Step (.binOp .div (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vInt (n₁ / n₂))) ρ
| sDivZero : ∀ n₁ n₂ ρ, n₂ = 0 →
Step (.binOp .div (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.error "Division by zero") ρ
| sModInt : ∀ n₁ n₂ ρ, n₂ ≠ 0 →
Step (.binOp .mod (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.lit (.vInt (n₁ % n₂))) ρ
| sModZero : ∀ n₁ n₂ ρ, n₂ = 0 →
Step (.binOp .mod (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
(.error "Modulo by zero") ρ
| sUnOpCong : ∀ op e e' ρ ρ',
Step e ρ e' ρ' →
Step (.unOp op e) ρ (.unOp op e') ρ'
Expand Down Expand Up @@ -554,6 +596,154 @@ theorem progress : ∀ e t,
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .mul e₁' e₂, ρ', .sBinOpLeft .mul _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tLt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
right
cases ih₁ with
| inl hv₁ =>
cases hv₁ with
| lit v₁ =>
cases ih₂ with
| inl hv₂ =>
cases hv₂ with
| lit v₂ =>
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
subst hn₁; subst hn₂
exact ⟨.lit (.vBool (decide (n₁ < n₂))), emptyEnv, .sLt n₁ n₂ emptyEnv⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .lt v₁ msg emptyEnv⟩
| inr hstp =>
obtain ⟨e₂', ρ', hs₂⟩ := hstp
exact ⟨.binOp .lt (.lit v₁) e₂', ρ', .sBinOpRight .lt v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .lt msg e₂ emptyEnv⟩
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .lt e₁' e₂, ρ', .sBinOpLeft .lt _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tGt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
right
cases ih₁ with
| inl hv₁ =>
cases hv₁ with
| lit v₁ =>
cases ih₂ with
| inl hv₂ =>
cases hv₂ with
| lit v₂ =>
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
subst hn₁; subst hn₂
exact ⟨.lit (.vBool (decide (n₁ > n₂))), emptyEnv, .sGt n₁ n₂ emptyEnv⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .gt v₁ msg emptyEnv⟩
| inr hstp =>
obtain ⟨e₂', ρ', hs₂⟩ := hstp
exact ⟨.binOp .gt (.lit v₁) e₂', ρ', .sBinOpRight .gt v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .gt msg e₂ emptyEnv⟩
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .gt e₁' e₂, ρ', .sBinOpLeft .gt _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tLe e₁ e₂ h₁ h₂ ih₁ ih₂ =>
right
cases ih₁ with
| inl hv₁ =>
cases hv₁ with
| lit v₁ =>
cases ih₂ with
| inl hv₂ =>
cases hv₂ with
| lit v₂ =>
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
subst hn₁; subst hn₂
exact ⟨.lit (.vBool (decide (n₁ ≤ n₂))), emptyEnv, .sLe n₁ n₂ emptyEnv⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .le v₁ msg emptyEnv⟩
| inr hstp =>
obtain ⟨e₂', ρ', hs₂⟩ := hstp
exact ⟨.binOp .le (.lit v₁) e₂', ρ', .sBinOpRight .le v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .le msg e₂ emptyEnv⟩
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .le e₁' e₂, ρ', .sBinOpLeft .le _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tGe e₁ e₂ h₁ h₂ ih₁ ih₂ =>
right
cases ih₁ with
| inl hv₁ =>
cases hv₁ with
| lit v₁ =>
cases ih₂ with
| inl hv₂ =>
cases hv₂ with
| lit v₂ =>
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
subst hn₁; subst hn₂
exact ⟨.lit (.vBool (decide (n₁ ≥ n₂))), emptyEnv, .sGe n₁ n₂ emptyEnv⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .ge v₁ msg emptyEnv⟩
| inr hstp =>
obtain ⟨e₂', ρ', hs₂⟩ := hstp
exact ⟨.binOp .ge (.lit v₁) e₂', ρ', .sBinOpRight .ge v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .ge msg e₂ emptyEnv⟩
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .ge e₁' e₂, ρ', .sBinOpLeft .ge _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tDivInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
right
cases ih₁ with
| inl hv₁ =>
cases hv₁ with
| lit v₁ =>
cases ih₂ with
| inl hv₂ =>
cases hv₂ with
| lit v₂ =>
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
subst hn₁; subst hn₂
by_cases hz : n₂ = 0
· exact ⟨.error "Division by zero", emptyEnv, .sDivZero n₁ n₂ emptyEnv hz⟩
· exact ⟨.lit (.vInt (n₁ / n₂)), emptyEnv, .sDivInt n₁ n₂ emptyEnv hz⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .div v₁ msg emptyEnv⟩
| inr hstp =>
obtain ⟨e₂', ρ', hs₂⟩ := hstp
exact ⟨.binOp .div (.lit v₁) e₂', ρ', .sBinOpRight .div v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .div msg e₂ emptyEnv⟩
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .div e₁' e₂, ρ', .sBinOpLeft .div _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tModInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
right
cases ih₁ with
| inl hv₁ =>
cases hv₁ with
| lit v₁ =>
cases ih₂ with
| inl hv₂ =>
cases hv₂ with
| lit v₂ =>
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
subst hn₁; subst hn₂
by_cases hz : n₂ = 0
· exact ⟨.error "Modulo by zero", emptyEnv, .sModZero n₁ n₂ emptyEnv hz⟩
· exact ⟨.lit (.vInt (n₁ % n₂)), emptyEnv, .sModInt n₁ n₂ emptyEnv hz⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .mod v₁ msg emptyEnv⟩
| inr hstp =>
obtain ⟨e₂', ρ', hs₂⟩ := hstp
exact ⟨.binOp .mod (.lit v₁) e₂', ρ', .sBinOpRight .mod v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
| error msg =>
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .mod msg e₂ emptyEnv⟩
| inr hstp =>
obtain ⟨e₁', ρ', hs₁⟩ := hstp
exact ⟨.binOp .mod e₁' e₂, ρ', .sBinOpLeft .mod _ e₁' e₂ emptyEnv ρ' hs₁⟩
| tNegInt e h₁ ih =>
right
cases ih with
Expand Down Expand Up @@ -676,6 +866,12 @@ theorem preservation : ∀ e e' t ρ ρ',
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ (ih _ h₁) h₂
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ (ih _ h₁) h₂
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ (ih _ h₁) h₂
| tLt _ _ h₁ h₂ => exact .tLt _ _ _ (ih _ h₁) h₂
| tGt _ _ h₁ h₂ => exact .tGt _ _ _ (ih _ h₁) h₂
| tLe _ _ h₁ h₂ => exact .tLe _ _ _ (ih _ h₁) h₂
| tGe _ _ h₁ h₂ => exact .tGe _ _ _ (ih _ h₁) h₂
| tDivInt _ _ h₁ h₂ => exact .tDivInt _ _ _ (ih _ h₁) h₂
| tModInt _ _ h₁ h₂ => exact .tModInt _ _ _ (ih _ h₁) h₂
| sBinOpRight op v₁ e₂ e₂' ρ ρ' _hv hs₂ ih =>
cases ht with
| tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih _ h₂)
Expand All @@ -686,6 +882,12 @@ theorem preservation : ∀ e e' t ρ ρ',
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ h₁ (ih _ h₂)
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ h₁ (ih _ h₂)
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ h₁ (ih _ h₂)
| tLt _ _ h₁ h₂ => exact .tLt _ _ _ h₁ (ih _ h₂)
| tGt _ _ h₁ h₂ => exact .tGt _ _ _ h₁ (ih _ h₂)
| tLe _ _ h₁ h₂ => exact .tLe _ _ _ h₁ (ih _ h₂)
| tGe _ _ h₁ h₂ => exact .tGe _ _ _ h₁ (ih _ h₂)
| tDivInt _ _ h₁ h₂ => exact .tDivInt _ _ _ h₁ (ih _ h₂)
| tModInt _ _ h₁ h₂ => exact .tModInt _ _ _ h₁ (ih _ h₂)
| sAddInt n₁ n₂ _ =>
cases ht with
| tAddInt _ _ h₁ h₂ => exact .tInt _ _
Expand Down Expand Up @@ -719,6 +921,30 @@ theorem preservation : ∀ e e' t ρ ρ',
| sMulInt n₁ n₂ _ =>
cases ht with
| tMulInt _ _ h₁ h₂ => exact .tInt _ _
| sLt n₁ n₂ _ =>
cases ht with
| tLt _ _ h₁ h₂ => exact .tBool _ _
| sGt n₁ n₂ _ =>
cases ht with
| tGt _ _ h₁ h₂ => exact .tBool _ _
| sLe n₁ n₂ _ =>
cases ht with
| tLe _ _ h₁ h₂ => exact .tBool _ _
| sGe n₁ n₂ _ =>
cases ht with
| tGe _ _ h₁ h₂ => exact .tBool _ _
| sDivInt n₁ n₂ _ _ =>
cases ht with
| tDivInt _ _ h₁ h₂ => exact .tInt _ _
| sDivZero n₁ n₂ _ _ =>
cases ht with
| tDivInt _ _ h₁ h₂ => exact .tError _ _ _
| sModInt n₁ n₂ _ _ =>
cases ht with
| tModInt _ _ h₁ h₂ => exact .tInt _ _
| sModZero n₁ n₂ _ _ =>
cases ht with
| tModInt _ _ h₁ h₂ => exact .tError _ _ _
| sNegInt n _ =>
cases ht with
| tNegInt _ h₁ => exact .tInt _ _
Expand Down Expand Up @@ -774,6 +1000,12 @@ theorem preservation : ∀ e e' t ρ ρ',
| tOr _ _ h₁ h₂ => exact .tError _ msg _
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
| tLt _ _ h₁ h₂ => exact .tError _ msg _
| tGt _ _ h₁ h₂ => exact .tError _ msg _
| tLe _ _ h₁ h₂ => exact .tError _ msg _
| tGe _ _ h₁ h₂ => exact .tError _ msg _
| tDivInt _ _ h₁ h₂ => exact .tError _ msg _
| tModInt _ _ h₁ h₂ => exact .tError _ msg _
| sBinOpErrRight op v₁ msg _ =>
cases ht with
| tAddInt _ _ h₁ h₂ => exact .tError _ msg _
Expand All @@ -784,6 +1016,12 @@ theorem preservation : ∀ e e' t ρ ρ',
| tOr _ _ h₁ h₂ => exact .tError _ msg _
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
| tLt _ _ h₁ h₂ => exact .tError _ msg _
| tGt _ _ h₁ h₂ => exact .tError _ msg _
| tLe _ _ h₁ h₂ => exact .tError _ msg _
| tGe _ _ h₁ h₂ => exact .tError _ msg _
| tDivInt _ _ h₁ h₂ => exact .tError _ msg _
| tModInt _ _ h₁ h₂ => exact .tError _ msg _
| sUnOpErr op msg _ =>
cases ht with
| tNegInt _ h₁ => exact .tError _ msg _
Expand Down
Loading