Skip to content

Commit 01f7329

Browse files
hyperpolymathclaude
hyperpolymath
and
claude
authored
Phase 1b: store-typed preservation (generalize preservation to an arbitrary context) (#114)
## What Adds **`store_step_preservation`** — the expression preservation theorem generalized from the empty type context to an arbitrary `Γ` under a store typing: ```lean StoreWellTyped Γ ρ → HasType Γ e t → Step e ρ e' ρ' → HasType Γ e' t ``` This is the form **statement execution** needs: expressions appearing inside a statement are typed in the *running* context, not in the empty one. ## How The proof mirrors the existing `preservation` (induction on the `Step` derivation, inversion on the typing). The **only** case that differs is `sVar`: - **Before** (`preservation`, empty context): `.var x` is untypable, so the case is a contradiction (`emptyTypeEnv x = none`). - **Now**: `store_wellTyped_lookup` gives the value `ρ` binds to `x` together with `HasType emptyTypeEnv (.lit v) t`, and `hasType_lit_any` lifts that to the running context `Γ`. Both lemmas landed in the two prior PRs (#112, #113). Every other case is context-polymorphic and textually identical to `preservation`. A **`preservation_via_store`** corollary confirms the generalization subsumes the closed theorem: the empty context is *vacuously* store-typed against any store (`emptyTypeEnv x = none` is never `some t`), so the old theorem is the `Γ := emptyTypeEnv` instance. ## Why this shape (and not a refactor) The cleaner design — make the general theorem primary and reduce `preservation` to a one-liner — would require moving `StoreWellTyped` / `hasType_lit_any` *above* `preservation` in the file, an invasive reorder of merged, CI-gated proofs. This PR is instead **purely additive (217 insertions, 0 deletions)**: the merged `preservation` and `type_safety` are left exactly as they are. ## Verification - `lean docs/proofs/verification/WokeLang.lean` exits 0 (Lean 4.30.0, Mathlib-free, single-file). - Hole-free: `store_step_preservation` and `preservation_via_store` depend only on the classical kernel base (`propext`, `Classical.choice`, `Quot.sound`). No `sorryAx`, no project-specific assumptions. ## Scope `docs/proofs/verification/WokeLang.lean` (the theorem + corollary) and a Progress entry in `docs/proofs/VERIFICATION-ROADMAP.md`. No changes to existing proofs or to the shipping implementation. 🤖 Generated with [Claude Code](https://claude.com/claude-code) https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL --- _Generated by [Claude Code](https://claude.ai/code/session_015oyMquf4daB6hMhmqB1wAL)_ Co-authored-by: Claude <noreply@anthropic.com>
1 parent 156455f commit 01f7329

2 files changed

Lines changed: 228 additions & 1 deletion

File tree

‎docs/proofs/VERIFICATION-ROADMAP.md‎

Lines changed: 11 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -153,7 +153,17 @@ unlock Phases 1c / 3a / 4a.
153153
resolves variables from `ρ`; the closed-context use was only in the `emptyTypeEnv`-stated
154154
`progress`/`preservation`. So the remaining work is a generalized store-typed preservation
155155
(`HasType Γ e t` under `StoreWellTyped Γ ρ`), then the statement-execution relation itself.
156-
- [ ] Phase 1 (cont.: `[T-Call]` after 1b), 1b (store-typed preservation → exec relation → stmt preservation), 1c — type-safety + operational metatheory.
156+
- [~] **Phase 1b (store-typed preservation)** — `store_step_preservation`: expression
157+
preservation generalized from the empty context to an arbitrary `Γ` under `StoreWellTyped Γ ρ`
158+
(`HasType Γ e t → Step e ρ e' ρ' → HasType Γ e' t`). This is the form statement execution
159+
needs — expressions inside a statement are typed in the *running* context, not the empty one.
160+
Mirrors `preservation`; the **only** case that differs is `sVar`, which discharges via
161+
`store_wellTyped_lookup` + `hasType_lit_any` (the runtime value bound to `x` has the type
162+
`Γ` assigns `x`) instead of the empty-context contradiction. A `preservation_via_store`
163+
corollary confirms it subsumes the closed theorem (empty context is vacuously store-typed).
164+
Hole-free (classical kernel base: `propext`, `Classical.choice`, `Quot.sound`). Purely
165+
additive — the merged `preservation`/`type_safety` are untouched.
166+
- [ ] Phase 1 (cont.: `[T-Call]` after 1b), 1b (statement-execution relation → stmt preservation), 1c — type-safety + operational metatheory.
157167
- [ ] Phase 2b, 2c — consent + capability state machines.
158168
- [ ] Phase 3a (+3b) — HM inference.
159169
- [ ] Phase 4a–4c — compiler / parser / WASM.

‎docs/proofs/verification/WokeLang.lean‎

Lines changed: 217 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1561,6 +1561,223 @@ theorem hasType_lit_any {Γ Γ' : TypeEnv} {v : Value} {t : WokeType}
15611561
| _ => intro _ hlit; obtain ⟨w, hw⟩ := hlit; nomatch hw
15621562
exact gen h ⟨v, rfl⟩
15631563

1564+
/-- **Store-typed preservation.** The expression preservation theorem
1565+
generalised from the empty context to an arbitrary type context `Γ`, under a
1566+
store typing `StoreWellTyped Γ ρ`. This is the form statement execution needs:
1567+
expressions inside a statement are typed in the running context, not in the
1568+
empty one. Mirrors `preservation`; the *only* case that differs is `sVar`,
1569+
which here discharges via `store_wellTyped_lookup` + `hasType_lit_any` (the
1570+
runtime value bound to `x` has the type `Γ` assigns `x`) instead of the
1571+
empty-context contradiction. -/
1572+
theorem store_step_preservation {Γ : TypeEnv} {e e' : Expr} {ρ ρ' : Env} {t : WokeType}
1573+
(hst : StoreWellTyped Γ ρ) (ht : HasType Γ e t) (hs : Step e ρ e' ρ') :
1574+
HasType Γ e' t := by
1575+
induction hs generalizing t with
1576+
| sVar x ρ₀ v hx =>
1577+
cases ht with
1578+
| tVar _ _ hxt =>
1579+
obtain ⟨v', hv', hvt⟩ := hst x t hxt
1580+
rw [hx] at hv'; injection hv' with hvv; subst hvv
1581+
exact hasType_lit_any hvt
1582+
| sBinOpLeft op e₁ e₁' e₂ ρ ρ' hs₁ ih =>
1583+
cases ht with
1584+
| tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ (ih hst h₁) h₂
1585+
| tAddFloat _ _ h₁ h₂ => exact .tAddFloat _ _ _ (ih hst h₁) h₂
1586+
| tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ (ih hst h₁) h₂
1587+
| tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ (ih hst h₁) h₂
1588+
| tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ (ih hst h₁) h₂
1589+
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ (ih hst h₁) h₂
1590+
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ (ih hst h₁) h₂
1591+
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ (ih hst h₁) h₂
1592+
| tLt _ _ h₁ h₂ => exact .tLt _ _ _ (ih hst h₁) h₂
1593+
| tGt _ _ h₁ h₂ => exact .tGt _ _ _ (ih hst h₁) h₂
1594+
| tLe _ _ h₁ h₂ => exact .tLe _ _ _ (ih hst h₁) h₂
1595+
| tGe _ _ h₁ h₂ => exact .tGe _ _ _ (ih hst h₁) h₂
1596+
| tDivInt _ _ h₁ h₂ => exact .tDivInt _ _ _ (ih hst h₁) h₂
1597+
| tModInt _ _ h₁ h₂ => exact .tModInt _ _ _ (ih hst h₁) h₂
1598+
| sBinOpRight op v₁ e₂ e₂' ρ ρ' _hv hs₂ ih =>
1599+
cases ht with
1600+
| tAddInt _ _ h₁ h₂ => exact .tAddInt _ _ _ h₁ (ih hst h₂)
1601+
| tAddFloat _ _ h₁ h₂ => exact .tAddFloat _ _ _ h₁ (ih hst h₂)
1602+
| tAddString _ _ h₁ h₂ => exact .tAddString _ _ _ h₁ (ih hst h₂)
1603+
| tEq _ _ _ h₁ h₂ => exact .tEq _ _ _ _ h₁ (ih hst h₂)
1604+
| tAnd _ _ h₁ h₂ => exact .tAnd _ _ _ h₁ (ih hst h₂)
1605+
| tOr _ _ h₁ h₂ => exact .tOr _ _ _ h₁ (ih hst h₂)
1606+
| tSubInt _ _ h₁ h₂ => exact .tSubInt _ _ _ h₁ (ih hst h₂)
1607+
| tMulInt _ _ h₁ h₂ => exact .tMulInt _ _ _ h₁ (ih hst h₂)
1608+
| tLt _ _ h₁ h₂ => exact .tLt _ _ _ h₁ (ih hst h₂)
1609+
| tGt _ _ h₁ h₂ => exact .tGt _ _ _ h₁ (ih hst h₂)
1610+
| tLe _ _ h₁ h₂ => exact .tLe _ _ _ h₁ (ih hst h₂)
1611+
| tGe _ _ h₁ h₂ => exact .tGe _ _ _ h₁ (ih hst h₂)
1612+
| tDivInt _ _ h₁ h₂ => exact .tDivInt _ _ _ h₁ (ih hst h₂)
1613+
| tModInt _ _ h₁ h₂ => exact .tModInt _ _ _ h₁ (ih hst h₂)
1614+
| sAddInt n₁ n₂ _ =>
1615+
cases ht with
1616+
| tAddInt _ _ h₁ h₂ => exact .tInt _ _
1617+
| tAddFloat _ _ h₁ _ => nomatch h₁
1618+
| tAddString _ _ h₁ _ => nomatch h₁
1619+
| sAddFloat f₁ f₂ _ =>
1620+
cases ht with
1621+
| tAddFloat _ _ h₁ h₂ => exact .tFloat _ _
1622+
| tAddInt _ _ h₁ _ => nomatch h₁
1623+
| tAddString _ _ h₁ _ => nomatch h₁
1624+
| sAddString s₁ s₂ _ =>
1625+
cases ht with
1626+
| tAddString _ _ h₁ h₂ => exact .tString _ _
1627+
| tAddInt _ _ h₁ _ => nomatch h₁
1628+
| tAddFloat _ _ h₁ _ => nomatch h₁
1629+
| sEqTrue v _ =>
1630+
cases ht with
1631+
| tEq _ _ _ h₁ h₂ => exact .tBool _ _
1632+
| sEqFalse v₁ v₂ _ hneq =>
1633+
cases ht with
1634+
| tEq _ _ _ h₁ h₂ => exact .tBool _ _
1635+
| sAnd b₁ b₂ _ =>
1636+
cases ht with
1637+
| tAnd _ _ h₁ h₂ => exact .tBool _ _
1638+
| sOr b₁ b₂ _ =>
1639+
cases ht with
1640+
| tOr _ _ h₁ h₂ => exact .tBool _ _
1641+
| sSubInt n₁ n₂ _ =>
1642+
cases ht with
1643+
| tSubInt _ _ h₁ h₂ => exact .tInt _ _
1644+
| sMulInt n₁ n₂ _ =>
1645+
cases ht with
1646+
| tMulInt _ _ h₁ h₂ => exact .tInt _ _
1647+
| sLt n₁ n₂ _ =>
1648+
cases ht with
1649+
| tLt _ _ h₁ h₂ => exact .tBool _ _
1650+
| sGt n₁ n₂ _ =>
1651+
cases ht with
1652+
| tGt _ _ h₁ h₂ => exact .tBool _ _
1653+
| sLe n₁ n₂ _ =>
1654+
cases ht with
1655+
| tLe _ _ h₁ h₂ => exact .tBool _ _
1656+
| sGe n₁ n₂ _ =>
1657+
cases ht with
1658+
| tGe _ _ h₁ h₂ => exact .tBool _ _
1659+
| sDivInt n₁ n₂ _ _ =>
1660+
cases ht with
1661+
| tDivInt _ _ h₁ h₂ => exact .tInt _ _
1662+
| sDivZero n₁ n₂ _ _ =>
1663+
cases ht with
1664+
| tDivInt _ _ h₁ h₂ => exact .tError _ _ _
1665+
| sModInt n₁ n₂ _ _ =>
1666+
cases ht with
1667+
| tModInt _ _ h₁ h₂ => exact .tInt _ _
1668+
| sModZero n₁ n₂ _ _ =>
1669+
cases ht with
1670+
| tModInt _ _ h₁ h₂ => exact .tError _ _ _
1671+
| sNegInt n _ =>
1672+
cases ht with
1673+
| tNegInt _ h₁ => exact .tInt _ _
1674+
| tNegFloat _ h₁ => nomatch h₁
1675+
| sNegFloat f _ =>
1676+
cases ht with
1677+
| tNegFloat _ h₁ => exact .tFloat _ _
1678+
| tNegInt _ h₁ => nomatch h₁
1679+
| sNot b _ =>
1680+
cases ht with
1681+
| tNot _ h₁ => exact .tBool _ _
1682+
| sUnOpCong op e e' ρ ρ' hs₁ ih =>
1683+
cases ht with
1684+
| tNegInt _ h₁ => exact .tNegInt _ _ (ih hst h₁)
1685+
| tNegFloat _ h₁ => exact .tNegFloat _ _ (ih hst h₁)
1686+
| tNot _ h₁ => exact .tNot _ _ (ih hst h₁)
1687+
| sOkay v _ _hv =>
1688+
cases ht with
1689+
| tOkay _ _ h₁ => exact .tOkayVal _ v _ h₁
1690+
| sOkayCong e e' ρ ρ' hs₁ ih =>
1691+
cases ht with
1692+
| tOkay _ _ h₁ => exact .tOkay _ _ _ (ih hst h₁)
1693+
| sOops s _ =>
1694+
cases ht with
1695+
| tOops _ _ h₁ => exact .tOopsVal _ s _
1696+
| sOopsCong e e' ρ ρ' hs₁ ih =>
1697+
cases ht with
1698+
| tOops _ _ h₁ => exact .tOops _ _ _ (ih hst h₁)
1699+
| sUnwrapOkay v _ =>
1700+
cases ht with
1701+
| tUnwrap _ tOk tErr h₁ =>
1702+
cases h₁ with
1703+
| tOkayVal _ _ hinner => exact hinner
1704+
| sUnwrapError s _ =>
1705+
cases ht with
1706+
| tUnwrap _ tOk tErr h₁ => exact .tError _ s t
1707+
| sUnwrapCong e e' ρ ρ' hs₁ ih =>
1708+
cases ht with
1709+
| tUnwrap _ _ tErr h₁ => exact .tUnwrap _ _ _ _ (ih hst h₁)
1710+
| sBinOpErrLeft op msg e₂ _ =>
1711+
cases ht with
1712+
| tAddInt _ _ h₁ h₂ => exact .tError _ msg _
1713+
| tAddFloat _ _ h₁ h₂ => exact .tError _ msg _
1714+
| tAddString _ _ h₁ h₂ => exact .tError _ msg _
1715+
| tEq _ _ _ h₁ h₂ => exact .tError _ msg _
1716+
| tAnd _ _ h₁ h₂ => exact .tError _ msg _
1717+
| tOr _ _ h₁ h₂ => exact .tError _ msg _
1718+
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
1719+
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
1720+
| tLt _ _ h₁ h₂ => exact .tError _ msg _
1721+
| tGt _ _ h₁ h₂ => exact .tError _ msg _
1722+
| tLe _ _ h₁ h₂ => exact .tError _ msg _
1723+
| tGe _ _ h₁ h₂ => exact .tError _ msg _
1724+
| tDivInt _ _ h₁ h₂ => exact .tError _ msg _
1725+
| tModInt _ _ h₁ h₂ => exact .tError _ msg _
1726+
| sBinOpErrRight op v₁ msg _ =>
1727+
cases ht with
1728+
| tAddInt _ _ h₁ h₂ => exact .tError _ msg _
1729+
| tAddFloat _ _ h₁ h₂ => exact .tError _ msg _
1730+
| tAddString _ _ h₁ h₂ => exact .tError _ msg _
1731+
| tEq _ _ _ h₁ h₂ => exact .tError _ msg _
1732+
| tAnd _ _ h₁ h₂ => exact .tError _ msg _
1733+
| tOr _ _ h₁ h₂ => exact .tError _ msg _
1734+
| tSubInt _ _ h₁ h₂ => exact .tError _ msg _
1735+
| tMulInt _ _ h₁ h₂ => exact .tError _ msg _
1736+
| tLt _ _ h₁ h₂ => exact .tError _ msg _
1737+
| tGt _ _ h₁ h₂ => exact .tError _ msg _
1738+
| tLe _ _ h₁ h₂ => exact .tError _ msg _
1739+
| tGe _ _ h₁ h₂ => exact .tError _ msg _
1740+
| tDivInt _ _ h₁ h₂ => exact .tError _ msg _
1741+
| tModInt _ _ h₁ h₂ => exact .tError _ msg _
1742+
| sUnOpErr op msg _ =>
1743+
cases ht with
1744+
| tNegInt _ h₁ => exact .tError _ msg _
1745+
| tNegFloat _ h₁ => exact .tError _ msg _
1746+
| tNot _ h₁ => exact .tError _ msg _
1747+
| sOkayErr msg _ =>
1748+
cases ht with
1749+
| tOkay _ _ h₁ => exact .tError _ msg _
1750+
| sOopsErr msg _ =>
1751+
cases ht with
1752+
| tOops _ _ h₁ => exact .tError _ msg _
1753+
| sUnwrapErr msg _ =>
1754+
cases ht with
1755+
| tUnwrap _ tOk tErr h₁ => exact .tError _ msg _
1756+
| sArrayStep vs e e' rest ρ ρ' hs ih =>
1757+
cases ht with
1758+
| tArray _ t' hall =>
1759+
refine .tArray _ _ t' (fun x hx => ?_)
1760+
rcases List.mem_append.1 hx with hpre | hcons
1761+
· exact hall x (List.mem_append.2 (Or.inl hpre))
1762+
· rcases List.mem_cons.1 hcons with rfl | htail
1763+
· exact ih hst (hall e (List.mem_append.2 (Or.inr List.mem_cons_self)))
1764+
· exact hall x (List.mem_append.2 (Or.inr (List.mem_cons_of_mem _ htail)))
1765+
| sArrayVal vs ρ =>
1766+
cases ht with
1767+
| tArray _ t' hall =>
1768+
exact .tArrayVal _ vs t' (fun v hv => hall (Expr.lit v) (List.mem_map.2 ⟨v, hv, rfl⟩))
1769+
| sArrayErr vs msg rest ρ =>
1770+
exact .tError _ msg _
1771+
1772+
/-- Faithfulness check: `store_step_preservation` subsumes the empty-context
1773+
`preservation`. The empty type context is *vacuously* store-typed against any
1774+
store (`emptyTypeEnv x = none` is never `some t`), so the closed theorem is the
1775+
`Γ := emptyTypeEnv` instance. -/
1776+
theorem preservation_via_store {e e' : Expr} {ρ ρ' : Env} {t : WokeType}
1777+
(ht : HasType emptyTypeEnv e t) (hs : Step e ρ e' ρ') :
1778+
HasType emptyTypeEnv e' t :=
1779+
store_step_preservation (fun x t h => by simp [emptyTypeEnv] at h) ht hs
1780+
15641781
-- =========================================================================
15651782
-- 8. TODO Stubs
15661783
-- =========================================================================

0 commit comments

Comments
 (0)