From 29d4065c20d3eee80981316e05f329f34e9bba9c Mon Sep 17 00:00:00 2001 From: Claude Date: Sun, 14 Jun 2026 04:19:20 +0000 Subject: [PATCH] =?UTF-8?q?feat(proofs):=20extend=20type=20safety=20?= =?UTF-8?q?=E2=80=94=20or/sub/mul=20operators=20+=20capability=20preorder?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit Tier 1 + Tier 3 extensions on the now-verified WokeLang.lean, each machine- checked under Lean 4.30.0 (lean-proofs CI gate), still sorry-free, no axioms. Tier 1 (base operators) — HasType + Step rules + full progress/preservation: - `or` (logical, mirrors `and`) - `sub`, `mul` (integer, mirror `add`) Tier 3 (capability lattice): - `capSubsumes_refl`, `capSubsumes_trans` — capability subsumption is a preorder. Deliberately the order shape echo-types' `DecorationStructure` requires (≤-refl/≤-trans), keeping WokeLang on-path for a future echo layer. Also checked echo-types `main` for design compatibility (AUDIT.md): the echo layer is a Mode-indexed decoration ON TOP of the base type system (the Ephapax L3 precedent), so these base extensions are orthogonal/compatible. Still open in Tier 1: comparisons (lt/gt/le/ge), div/mod (panic), float, arrays. https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7 --- docs/proofs/verification/AUDIT.md | 32 ++++++ docs/proofs/verification/WokeLang.lean | 133 +++++++++++++++++++++++++ 2 files changed, 165 insertions(+) diff --git a/docs/proofs/verification/AUDIT.md b/docs/proofs/verification/AUDIT.md index 2a32a73..ef98dd5 100644 --- a/docs/proofs/verification/AUDIT.md +++ b/docs/proofs/verification/AUDIT.md @@ -114,6 +114,38 @@ the implementations toward it, or (b) build a *second* Lean model faithful to 4. **Compiler/VM track** (the file's §8 TODO stubs: bytecode, compiler, VM semantics, compiler-correctness) remains open and is a larger effort. +## Echo-types design compatibility (checked 2026-06-14) + +Checked against echo-types `main` before extending WokeLang's type system, so +the extensions don't box out a future echo/loss layer. The precedent is +`EchoEphapaxBridge`: **Ephapax** (a linear-typed language) ports +`EchoLinear.agda` + `EchoResidue.agda` into its prover as an **L3 layer** +(`formal/Echo.v`, 584 lines Coq, zero axioms), preserving the headline +theorems (`weaken_collapses_distinction`, `affine_canonical`, +`no_section_collapse_to_residue`, `degrade_mode_comp`). + +- The echo/loss layer is a **`Mode`-indexed decoration** (`linear ⊑ affine`, + `weaken : LEcho linear → LEcho affine`) sitting *on top of* a base type + system as a **separate module** — not a change to `progress`/`preservation`. + So the Tier-1 base-operator extensions (`or`/`sub`/`mul`/…) are **orthogonal + and compatible** by construction. +- echo-types' `DecorationStructure` is a **preorder** (`≤-refl`, `≤-trans`, + `≤-prop`, `join`). WokeLang's **capability subsumption is that shape** — the + `capSubsumes_refl` / `capSubsumes_trans` lemmas are deliberately on-path to + host echo decorations later. +- **Integration blueprint** (not yet started): a Lean port of `EchoLinear` + + `EchoResidue` as a `WokeLang/Echo.lean` L3 module, à la Ephapax's Coq port, + leaving the base type-safety proofs intact. + +## 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 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. + ## Status - Repair to `sorry`-free under Lean 4.30.0: see CI / `lean` check. diff --git a/docs/proofs/verification/WokeLang.lean b/docs/proofs/verification/WokeLang.lean index 325db2e..863fb6f 100644 --- a/docs/proofs/verification/WokeLang.lean +++ b/docs/proofs/verification/WokeLang.lean @@ -174,6 +174,15 @@ inductive HasType : TypeEnv → Expr → WokeType → Prop where | tAnd : ∀ Γ e₁ e₂, HasType Γ e₁ .bool → HasType Γ e₂ .bool → HasType Γ (.binOp .and e₁ e₂) .bool + | tOr : ∀ Γ e₁ e₂, + HasType Γ e₁ .bool → HasType Γ e₂ .bool → + HasType Γ (.binOp .or e₁ e₂) .bool + | tSubInt : ∀ Γ e₁ e₂, + HasType Γ e₁ .int → HasType Γ e₂ .int → + HasType Γ (.binOp .sub e₁ e₂) .int + | tMulInt : ∀ Γ e₁ e₂, + HasType Γ e₁ .int → HasType Γ e₂ .int → + HasType Γ (.binOp .mul e₁ e₂) .int | tNegInt : ∀ Γ e, HasType Γ e .int → HasType Γ (.unOp .neg e) .int @@ -244,6 +253,15 @@ inductive Step : Expr → Env → Expr → Env → Prop where | sAnd : ∀ b₁ b₂ ρ, Step (.binOp .and (.lit (.vBool b₁)) (.lit (.vBool b₂))) ρ (.lit (.vBool (b₁ && b₂))) ρ + | sOr : ∀ b₁ b₂ ρ, + Step (.binOp .or (.lit (.vBool b₁)) (.lit (.vBool b₂))) ρ + (.lit (.vBool (b₁ || b₂))) ρ + | sSubInt : ∀ n₁ n₂ ρ, + Step (.binOp .sub (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ + (.lit (.vInt (n₁ - n₂))) ρ + | sMulInt : ∀ n₁ n₂ ρ, + Step (.binOp .mul (.lit (.vInt n₁)) (.lit (.vInt n₂))) ρ + (.lit (.vInt (n₁ * n₂))) ρ | sUnOpCong : ∀ op e e' ρ ρ', Step e ρ e' ρ' → Step (.unOp op e) ρ (.unOp op e') ρ' @@ -464,6 +482,78 @@ theorem progress : ∀ e t, | inr hstp => obtain ⟨e₁', ρ', hs₁⟩ := hstp exact ⟨.binOp .and e₁' e₂, ρ', .sBinOpLeft .and _ e₁' e₂ emptyEnv ρ' hs₁⟩ + | tOr 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 ⟨b₁, hb₁⟩ := canonical_forms_bool v₁ h₁ + have ⟨b₂, hb₂⟩ := canonical_forms_bool v₂ h₂ + subst hb₁; subst hb₂ + exact ⟨.lit (.vBool (b₁ || b₂)), emptyEnv, .sOr b₁ b₂ emptyEnv⟩ + | error msg => + exact ⟨.error msg, emptyEnv, .sBinOpErrRight .or v₁ msg emptyEnv⟩ + | inr hstp => + obtain ⟨e₂', ρ', hs₂⟩ := hstp + exact ⟨.binOp .or (.lit v₁) e₂', ρ', .sBinOpRight .or v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩ + | error msg => + exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .or msg e₂ emptyEnv⟩ + | inr hstp => + obtain ⟨e₁', ρ', hs₁⟩ := hstp + exact ⟨.binOp .or e₁' e₂, ρ', .sBinOpLeft .or _ e₁' e₂ emptyEnv ρ' hs₁⟩ + | tSubInt 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 (.vInt (n₁ - n₂)), emptyEnv, .sSubInt n₁ n₂ emptyEnv⟩ + | error msg => + exact ⟨.error msg, emptyEnv, .sBinOpErrRight .sub v₁ msg emptyEnv⟩ + | inr hstp => + obtain ⟨e₂', ρ', hs₂⟩ := hstp + exact ⟨.binOp .sub (.lit v₁) e₂', ρ', .sBinOpRight .sub v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩ + | error msg => + exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .sub msg e₂ emptyEnv⟩ + | inr hstp => + obtain ⟨e₁', ρ', hs₁⟩ := hstp + exact ⟨.binOp .sub e₁' e₂, ρ', .sBinOpLeft .sub _ e₁' e₂ emptyEnv ρ' hs₁⟩ + | tMulInt 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 (.vInt (n₁ * n₂)), emptyEnv, .sMulInt n₁ n₂ emptyEnv⟩ + | error msg => + exact ⟨.error msg, emptyEnv, .sBinOpErrRight .mul v₁ msg emptyEnv⟩ + | inr hstp => + obtain ⟨e₂', ρ', hs₂⟩ := hstp + exact ⟨.binOp .mul (.lit v₁) e₂', ρ', .sBinOpRight .mul v₁ _ e₂' emptyEnv ρ' (.lit v₁) hs₂⟩ + | error msg => + exact ⟨.error msg, emptyEnv, .sBinOpErrLeft .mul msg e₂ emptyEnv⟩ + | inr hstp => + obtain ⟨e₁', ρ', hs₁⟩ := hstp + exact ⟨.binOp .mul e₁' e₂, ρ', .sBinOpLeft .mul _ e₁' e₂ emptyEnv ρ' hs₁⟩ | tNegInt e h₁ ih => right cases ih with @@ -583,6 +673,9 @@ theorem preservation : ∀ e e' t ρ ρ', | tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ (ih _ h₁) h₂ | tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ (ih _ h₁) h₂ | tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ (ih _ h₁) h₂ + | tOr _ _ h₁ h₂ => exact .tOr _ _ _ (ih _ h₁) h₂ + | tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ (ih _ h₁) h₂ + | tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ (ih _ h₁) h₂ | sBinOpRight op v₁ e₂ e₂' ρ ρ' _hv hs₂ ih => cases ht with | tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih _ h₂) @@ -590,6 +683,9 @@ theorem preservation : ∀ e e' t ρ ρ', | tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ h₁ (ih _ h₂) | tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ h₁ (ih _ h₂) | tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ h₁ (ih _ h₂) + | tOr _ _ h₁ h₂ => exact .tOr _ _ _ h₁ (ih _ h₂) + | tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ h₁ (ih _ h₂) + | tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ h₁ (ih _ h₂) | sAddInt n₁ n₂ _ => cases ht with | tAddInt _ _ h₁ h₂ => exact .tInt _ _ @@ -614,6 +710,15 @@ theorem preservation : ∀ e e' t ρ ρ', | sAnd b₁ b₂ _ => cases ht with | tAnd _ _ h₁ h₂ => exact .tBool _ _ + | sOr b₁ b₂ _ => + cases ht with + | tOr _ _ h₁ h₂ => exact .tBool _ _ + | sSubInt n₁ n₂ _ => + cases ht with + | tSubInt _ _ h₁ h₂ => exact .tInt _ _ + | sMulInt n₁ n₂ _ => + cases ht with + | tMulInt _ _ h₁ h₂ => exact .tInt _ _ | sNegInt n _ => cases ht with | tNegInt _ h₁ => exact .tInt _ _ @@ -666,6 +771,9 @@ theorem preservation : ∀ e e' t ρ ρ', | tAddString _ _ h₁ h₂ => exact .tError _ msg _ | tEq _ _ _ h₁ h₂ => exact .tError _ msg _ | tAnd _ _ h₁ h₂ => exact .tError _ msg _ + | tOr _ _ h₁ h₂ => exact .tError _ msg _ + | tSubInt _ _ h₁ h₂ => exact .tError _ msg _ + | tMulInt _ _ h₁ h₂ => exact .tError _ msg _ | sBinOpErrRight op v₁ msg _ => cases ht with | tAddInt _ _ h₁ h₂ => exact .tError _ msg _ @@ -673,6 +781,9 @@ theorem preservation : ∀ e e' t ρ ρ', | tAddString _ _ h₁ h₂ => exact .tError _ msg _ | tEq _ _ _ h₁ h₂ => exact .tError _ msg _ | tAnd _ _ h₁ h₂ => exact .tError _ msg _ + | tOr _ _ h₁ h₂ => exact .tError _ msg _ + | tSubInt _ _ h₁ h₂ => exact .tError _ msg _ + | tMulInt _ _ h₁ h₂ => exact .tError _ msg _ | sUnOpErr op msg _ => cases ht with | tNegInt _ h₁ => exact .tError _ msg _ @@ -764,6 +875,28 @@ def capSubsumes (c₁ c₂ : Capability) : Bool := def hasCapability (c : Capability) (cs : CapabilitySet) : Bool := cs.any (fun c' => capSubsumes c' c) +-- Capability subsumption is a PREORDER (reflexive + transitive). +-- This is the order shape that echo-types' `DecorationStructure` requires +-- (`≤-refl`, `≤-trans`) to host echo decorations — see docs AUDIT.md +-- "echo-types compatibility". Proving it here keeps WokeLang's capability +-- lattice on-path for a future echo/loss layer (the Ephapax L3 precedent). + +/-- Capability subsumption is reflexive. -/ +theorem capSubsumes_refl (c : Capability) : capSubsumes c c = true := by + cases c with + | fileRead o => cases o <;> simp [capSubsumes] + | fileWrite o => cases o <;> simp [capSubsumes] + | network o => cases o <;> simp [capSubsumes] + | execute o => cases o <;> simp [capSubsumes] + | process => simp [capSubsumes] + | crypto => simp [capSubsumes] + +/-- Capability subsumption is transitive. -/ +theorem capSubsumes_trans (c₁ c₂ c₃ : Capability) : + capSubsumes c₁ c₂ = true → capSubsumes c₂ c₃ = true → capSubsumes c₁ c₃ = true := by + cases c₁ <;> cases c₂ <;> cases c₃ <;> simp_all [capSubsumes] + all_goals (rename_i a₁ a₂ a₃; cases a₁ <;> cases a₂ <;> cases a₃ <;> simp_all) + -- ========================================================================= -- 8. TODO Stubs -- =========================================================================