Skip to content

Commit da35ff4

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
feat(proofs): extend type safety — or/sub/mul operators + capability preorder (#80)
## Summary Builds on the now-verified `WokeLang.lean` (#79) by **extending the type-safety proofs** — Tier 1 (base operators) + Tier 3 (capability lattice) from `AUDIT.md`. Every addition is machine-checked under Lean 4.30.0 by the `lean-proofs` CI gate, **still sorry-free, no axioms**. ## Tier 1 — base operators Each adds a `HasType` rule + `Step` rule and full `progress` / `preservation` coverage (including the congruence and error-propagation cases): - **`or`** (logical) — mirrors the proven `and`. - **`sub`, `mul`** (integer) — mirror the proven `add`. ## Tier 3 — capability lattice - **`capSubsumes_refl`**, **`capSubsumes_trans`** — capability subsumption is a **preorder**. This is deliberately the order shape echo-types' `DecorationStructure` requires (`≤-refl`/`≤-trans`), keeping WokeLang's capability lattice on-path for a future echo/loss layer. ## Echo-types design compatibility Per your request, I checked echo-types `main` before extending, and documented it in `AUDIT.md`. The precedent is `EchoEphapaxBridge`: **Ephapax** (a linear-typed language) ports `EchoLinear` + `EchoResidue` into its prover as a separate **L3 layer**. So the echo/loss layer is a `Mode`-indexed decoration *on top of* the base type system — these base-operator extensions are **orthogonal and compatible**, and the capability preorder is a stepping stone toward it. ## Verification ``` $ lean docs/proofs/verification/WokeLang.lean # exit 0, sorry-free ``` ## Still open in Tier 1 (next increment) Ordering comparisons (`lt`/`gt`/`le`/`ge`), `div`/`mod` (divide-by-zero → `error` panic, reusing the proven panic fragment), float variants, and `array` typing. 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 343867d commit da35ff4

2 files changed

Lines changed: 165 additions & 0 deletions

File tree

‎docs/proofs/verification/AUDIT.md‎

Lines changed: 32 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -114,6 +114,38 @@ the implementations toward it, or (b) build a *second* Lean model faithful to
114114
4. **Compiler/VM track** (the file's §8 TODO stubs: bytecode, compiler,
115115
VM semantics, compiler-correctness) remains open and is a larger effort.
116116

117+
## Echo-types design compatibility (checked 2026-06-14)
118+
119+
Checked against echo-types `main` before extending WokeLang's type system, so
120+
the extensions don't box out a future echo/loss layer. The precedent is
121+
`EchoEphapaxBridge`: **Ephapax** (a linear-typed language) ports
122+
`EchoLinear.agda` + `EchoResidue.agda` into its prover as an **L3 layer**
123+
(`formal/Echo.v`, 584 lines Coq, zero axioms), preserving the headline
124+
theorems (`weaken_collapses_distinction`, `affine_canonical`,
125+
`no_section_collapse_to_residue`, `degrade_mode_comp`).
126+
127+
- The echo/loss layer is a **`Mode`-indexed decoration** (`linear ⊑ affine`,
128+
`weaken : LEcho linear → LEcho affine`) sitting *on top of* a base type
129+
system as a **separate module** — not a change to `progress`/`preservation`.
130+
So the Tier-1 base-operator extensions (`or`/`sub`/`mul`/…) are **orthogonal
131+
and compatible** by construction.
132+
- echo-types' `DecorationStructure` is a **preorder** (`≤-refl`, `≤-trans`,
133+
`≤-prop`, `join`). WokeLang's **capability subsumption is that shape** — the
134+
`capSubsumes_refl` / `capSubsumes_trans` lemmas are deliberately on-path to
135+
host echo decorations later.
136+
- **Integration blueprint** (not yet started): a Lean port of `EchoLinear` +
137+
`EchoResidue` as a `WokeLang/Echo.lean` L3 module, à la Ephapax's Coq port,
138+
leaving the base type-safety proofs intact.
139+
140+
## Extensions landed (2026-06-14)
141+
142+
- **Tier 1 (base operators):** `or` (logical), `sub`/`mul` (integer) — each
143+
with `HasType` + `Step` rules and full `progress`/`preservation` coverage.
144+
- **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.
148+
117149
## Status
118150

119151
- Repair to `sorry`-free under Lean 4.30.0: see CI / `lean` check.

‎docs/proofs/verification/WokeLang.lean‎

Lines changed: 133 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -174,6 +174,15 @@ inductive HasType : TypeEnv → Expr → WokeType → Prop where
174174
| tAnd : ∀ Γ e₁ e₂,
175175
HasType Γ e₁ .bool → HasType Γ e₂ .bool →
176176
HasType Γ (.binOp .and e₁ e₂) .bool
177+
| tOr : ∀ Γ e₁ e₂,
178+
HasType Γ e₁ .bool → HasType Γ e₂ .bool →
179+
HasType Γ (.binOp .or e₁ e₂) .bool
180+
| tSubInt : ∀ Γ e₁ e₂,
181+
HasType Γ e₁ .int → HasType Γ e₂ .int →
182+
HasType Γ (.binOp .sub e₁ e₂) .int
183+
| tMulInt : ∀ Γ e₁ e₂,
184+
HasType Γ e₁ .int → HasType Γ e₂ .int →
185+
HasType Γ (.binOp .mul e₁ e₂) .int
177186
| tNegInt : ∀ Γ e,
178187
HasType Γ e .int →
179188
HasType Γ (.unOp .neg e) .int
@@ -244,6 +253,15 @@ inductive Step : Expr → Env → Expr → Env → Prop where
244253
| sAnd : ∀ b₁ b₂ ρ,
245254
Step (.binOp .and (.lit (.vBool b₁)) (.lit (.vBool b₂))) ρ
246255
(.lit (.vBool (b₁ && b₂))) ρ
256+
| sOr : ∀ b₁ b₂ ρ,
257+
Step (.binOp .or (.lit (.vBool b₁)) (.lit (.vBool b₂))) ρ
258+
(.lit (.vBool (b₁ || b₂))) ρ
259+
| sSubInt : ∀ n₁ n₂ ρ,
260+
Step (.binOp .sub (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
261+
(.lit (.vInt (n₁ - n₂))) ρ
262+
| sMulInt : ∀ n₁ n₂ ρ,
263+
Step (.binOp .mul (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ
264+
(.lit (.vInt (n₁ * n₂))) ρ
247265
| sUnOpCong : ∀ op e e' ρ ρ',
248266
Step e ρ e' ρ' →
249267
Step (.unOp op e) ρ (.unOp op e') ρ'
@@ -464,6 +482,78 @@ theorem progress : ∀ e t,
464482
| inr hstp =>
465483
obtain ⟨e₁', ρ', hs₁⟩ := hstp
466484
exact ⟨.binOp .and e₁' e₂, ρ', .sBinOpLeft .and _ e₁' e₂ emptyEnv ρ' hs₁⟩
485+
| tOr e₁ e₂ h₁ h₂ ih₁ ih₂ =>
486+
right
487+
cases ih₁ with
488+
| inl hv₁ =>
489+
cases hv₁ with
490+
| lit v₁ =>
491+
cases ih₂ with
492+
| inl hv₂ =>
493+
cases hv₂ with
494+
| lit v₂ =>
495+
have ⟨b₁, hb₁⟩ := canonical_forms_bool v₁ h₁
496+
have ⟨b₂, hb₂⟩ := canonical_forms_bool v₂ h₂
497+
subst hb₁; subst hb₂
498+
exact ⟨.lit (.vBool (b₁ || b₂)), emptyEnv, .sOr b₁ b₂ emptyEnv⟩
499+
| error msg =>
500+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .or v₁ msg emptyEnv⟩
501+
| inr hstp =>
502+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
503+
exact ⟨.binOp .or (.lit v₁) e₂', ρ', .sBinOpRight .or v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
504+
| error msg =>
505+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .or msg e₂ emptyEnv⟩
506+
| inr hstp =>
507+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
508+
exact ⟨.binOp .or e₁' e₂, ρ', .sBinOpLeft .or _ e₁' e₂ emptyEnv ρ' hs₁⟩
509+
| tSubInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
510+
right
511+
cases ih₁ with
512+
| inl hv₁ =>
513+
cases hv₁ with
514+
| lit v₁ =>
515+
cases ih₂ with
516+
| inl hv₂ =>
517+
cases hv₂ with
518+
| lit v₂ =>
519+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
520+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
521+
subst hn₁; subst hn₂
522+
exact ⟨.lit (.vInt (n₁ - n₂)), emptyEnv, .sSubInt n₁ n₂ emptyEnv⟩
523+
| error msg =>
524+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .sub v₁ msg emptyEnv⟩
525+
| inr hstp =>
526+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
527+
exact ⟨.binOp .sub (.lit v₁) e₂', ρ', .sBinOpRight .sub v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
528+
| error msg =>
529+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .sub msg e₂ emptyEnv⟩
530+
| inr hstp =>
531+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
532+
exact ⟨.binOp .sub e₁' e₂, ρ', .sBinOpLeft .sub _ e₁' e₂ emptyEnv ρ' hs₁⟩
533+
| tMulInt e₁ e₂ h₁ h₂ ih₁ ih₂ =>
534+
right
535+
cases ih₁ with
536+
| inl hv₁ =>
537+
cases hv₁ with
538+
| lit v₁ =>
539+
cases ih₂ with
540+
| inl hv₂ =>
541+
cases hv₂ with
542+
| lit v₂ =>
543+
have ⟨n₁, hn₁⟩ := canonical_forms_int v₁ h₁
544+
have ⟨n₂, hn₂⟩ := canonical_forms_int v₂ h₂
545+
subst hn₁; subst hn₂
546+
exact ⟨.lit (.vInt (n₁ * n₂)), emptyEnv, .sMulInt n₁ n₂ emptyEnv⟩
547+
| error msg =>
548+
exact ⟨.error msg, emptyEnv, .sBinOpErrRight .mul v₁ msg emptyEnv⟩
549+
| inr hstp =>
550+
obtain ⟨e₂', ρ', hs₂⟩ := hstp
551+
exact ⟨.binOp .mul (.lit v₁) e₂', ρ', .sBinOpRight .mul v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩
552+
| error msg =>
553+
exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .mul msg e₂ emptyEnv⟩
554+
| inr hstp =>
555+
obtain ⟨e₁', ρ', hs₁⟩ := hstp
556+
exact ⟨.binOp .mul e₁' e₂, ρ', .sBinOpLeft .mul _ e₁' e₂ emptyEnv ρ' hs₁⟩
467557
| tNegInt e h₁ ih =>
468558
right
469559
cases ih with
@@ -583,13 +673,19 @@ theorem preservation : ∀ e e' t ρ ρ',
583673
| tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ (ih _ h₁) h₂
584674
| tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ (ih _ h₁) h₂
585675
| tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ (ih _ h₁) h₂
676+
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ (ih _ h₁) h₂
677+
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ (ih _ h₁) h₂
678+
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ (ih _ h₁) h₂
586679
| sBinOpRight op v₁ e₂ e₂' ρ ρ' _hv hs₂ ih =>
587680
cases ht with
588681
| tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih _ h₂)
589682
| tAddFloat _ _ h₁ h₂ => exact .tAddFloat _ _ _ h₁ (ih _ h₂)
590683
| tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ h₁ (ih _ h₂)
591684
| tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ h₁ (ih _ h₂)
592685
| tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ h₁ (ih _ h₂)
686+
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ h₁ (ih _ h₂)
687+
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ h₁ (ih _ h₂)
688+
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ h₁ (ih _ h₂)
593689
| sAddInt n₁ n₂ _ =>
594690
cases ht with
595691
| tAddInt _ _ h₁ h₂ => exact .tInt _ _
@@ -614,6 +710,15 @@ theorem preservation : ∀ e e' t ρ ρ',
614710
| sAnd b₁ b₂ _ =>
615711
cases ht with
616712
| tAnd _ _ h₁ h₂ => exact .tBool _ _
713+
| sOr b₁ b₂ _ =>
714+
cases ht with
715+
| tOr _ _ h₁ h₂ => exact .tBool _ _
716+
| sSubInt n₁ n₂ _ =>
717+
cases ht with
718+
| tSubInt _ _ h₁ h₂ => exact .tInt _ _
719+
| sMulInt n₁ n₂ _ =>
720+
cases ht with
721+
| tMulInt _ _ h₁ h₂ => exact .tInt _ _
617722
| sNegInt n _ =>
618723
cases ht with
619724
| tNegInt _ h₁ => exact .tInt _ _
@@ -666,13 +771,19 @@ theorem preservation : ∀ e e' t ρ ρ',
666771
| tAddString _ _ h₁ h₂ => exact .tError _ msg _
667772
| tEq _ _ _ h₁ h₂ => exact .tError _ msg _
668773
| tAnd _ _ h₁ h₂ => exact .tError _ msg _
774+
| tOr _ _ h₁ h₂ => exact .tError _ msg _
775+
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
776+
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
669777
| sBinOpErrRight op v₁ msg _ =>
670778
cases ht with
671779
| tAddInt _ _ h₁ h₂ => exact .tError _ msg _
672780
| tAddFloat _ _ h₁ h₂ => exact .tError _ msg _
673781
| tAddString _ _ h₁ h₂ => exact .tError _ msg _
674782
| tEq _ _ _ h₁ h₂ => exact .tError _ msg _
675783
| tAnd _ _ h₁ h₂ => exact .tError _ msg _
784+
| tOr _ _ h₁ h₂ => exact .tError _ msg _
785+
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
786+
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
676787
| sUnOpErr op msg _ =>
677788
cases ht with
678789
| tNegInt _ h₁ => exact .tError _ msg _
@@ -764,6 +875,28 @@ def capSubsumes (c₁ c₂ : Capability) : Bool :=
764875
def hasCapability (c : Capability) (cs : CapabilitySet) : Bool :=
765876
cs.any (fun c' => capSubsumes c' c)
766877

878+
-- Capability subsumption is a PREORDER (reflexive + transitive).
879+
-- This is the order shape that echo-types' `DecorationStructure` requires
880+
-- (`≤-refl`, `≤-trans`) to host echo decorations — see docs AUDIT.md
881+
-- "echo-types compatibility". Proving it here keeps WokeLang's capability
882+
-- lattice on-path for a future echo/loss layer (the Ephapax L3 precedent).
883+
884+
/-- Capability subsumption is reflexive. -/
885+
theorem capSubsumes_refl (c : Capability) : capSubsumes c c = true := by
886+
cases c with
887+
| fileRead o => cases o <;> simp [capSubsumes]
888+
| fileWrite o => cases o <;> simp [capSubsumes]
889+
| network o => cases o <;> simp [capSubsumes]
890+
| execute o => cases o <;> simp [capSubsumes]
891+
| process => simp [capSubsumes]
892+
| crypto => simp [capSubsumes]
893+
894+
/-- Capability subsumption is transitive. -/
895+
theorem capSubsumes_trans (c₁ c₂ c₃ : Capability) :
896+
capSubsumes c₁ c₂ = true → capSubsumes c₂ c₃ = true → capSubsumes c₁ c₃ = true := by
897+
cases c₁ <;> cases c₂ <;> cases c₃ <;> simp_all [capSubsumes]
898+
all_goals (rename_i a₁ a₂ a₃; cases a₁ <;> cases a₂ <;> cases a₃ <;> simp_all)
899+
767900
-- =========================================================================
768901
-- 8. TODO Stubs
769902
-- =========================================================================

0 commit comments

Comments
 (0)