Phase 1b foundation: store typing (StoreWellTyped + lemmas) (#112)

## What

Adds the **store-typing relation** that bridges the static `TypeEnv` and
the
runtime `Env` — the invariant every statement-execution preservation
theorem
is stated against — plus the three lemmas the statement dynamics rest
on.

```lean
def StoreWellTyped (Γ : TypeEnv) (ρ : Env) : Prop :=
  ∀ x t, Γ x = some t → ∃ v, ρ x = some v ∧ HasType emptyTypeEnv (.lit v) t
```

| Lemma | Statement |
|---|---|
| `store_wellTyped_empty` | the empty store types against the empty
context |
| `store_wellTyped_lookup` | a typed variable resolves to a value of its
type |
| `store_wellTyped_extend` | extending context+store in lockstep
(exactly a `varDecl`) preserves store typing |

## Why this, and why now

Per the agreed sequencing rule — *land the lowest-complexity, safe,
**complete**
unit first* — this is the foundational piece of **roadmap Phase 1b
(statement
dynamics)**. The statement-*execution* relation itself is the next,
higher-complexity
step: the expression `Step` is closed-term-only, so variable resolution
needs design.
That lands in a follow-up; this store-typing layer is the stable base it
builds on
(notably `store_wellTyped_extend` is the key step for `varDecl`
preservation).

## Verification

- `lean docs/proofs/verification/WokeLang.lean` exits 0 (Lean 4.30.0,
Mathlib-free, single-file).
- Hole-free: `#print axioms` reports **`propext`** only for
`store_wellTyped_empty`,
and **no axioms** for `store_wellTyped_lookup` /
`store_wellTyped_extend`.
  No `sorryAx`, no project-specific assumptions.

## Scope

`docs/proofs/verification/WokeLang.lean` (the three lemmas + the
`StoreWellTyped`
def) 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>

Author: hyperpolymath

docs/proofs/VERIFICATION-ROADMAP.md

@@ -136,7 +136,15 @@ unlock Phases 1c / 3a / 4a.
   reduction entangles with statement *execution* and belongs with **Phase 1b** (statement
   dynamics), not this step. There is also no `index` constructor, so `[T-Index]` requires an
   AST extension. Roadmap refined accordingly.
-- [ ] Phase 1 (cont.: `[T-Call]` after 1b), 1b, 1c — type-safety + operational metatheory.
+- [~] **Phase 1b (foundation)** — **store typing** (`StoreWellTyped`) bridging the
+  static `TypeEnv` and the runtime `Env`, with the three lemmas the statement-execution
+  preservation proofs rest on: `store_wellTyped_empty` (empty store types against the
+  empty context), `store_wellTyped_lookup` (a typed variable resolves to a value of its
+  type), and `store_wellTyped_extend` (extending context+store in lockstep — exactly a
+  `varDecl` — preserves store typing). Hole-free (axiom `propext` only). The statement
+  *execution* relation itself is the next, higher-complexity step (the expression `Step`
+  is closed-term-only, so variable resolution needs design); this foundation lands first.
+- [ ] Phase 1 (cont.: `[T-Call]` after 1b), 1b (exec relation + stmt preservation), 1c — type-safety + operational metatheory.
 - [ ] Phase 2b, 2c — consent + capability state machines.
 - [ ] Phase 3a (+3b) — HM inference.
 - [ ] Phase 4a–4c — compiler / parser / WASM.

docs/proofs/verification/WokeLang.lean

@@ -1473,6 +1473,42 @@ theorem subst_preserves_typing {x : String} {v : Value} {tx : WokeType} :
       simp only [subst]
       exact .tArrayVal _ _ _ (fun w hw => by simpa only [subst] using ih w hw hΔ hv)
 
+-- =========================================================================
+-- 7c. Store typing (roadmap Phase 1b foundation)
+-- =========================================================================
+
+/-- **Store typing.** The runtime store `ρ` agrees with the type context `Γ`:
+every variable `Γ` types is bound in `ρ` to a value of that type. This is the
+bridge between the static `TypeEnv` and the dynamic `Env`, and the invariant every
+statement-execution preservation theorem is stated against. -/
+def StoreWellTyped (Γ : TypeEnv) (ρ : Env) : Prop :=
+  ∀ x t, Γ x = some t → ∃ v, ρ x = some v ∧ HasType emptyTypeEnv (.lit v) t
+
+/-- The empty store is well typed against the empty context. -/
+theorem store_wellTyped_empty : StoreWellTyped emptyTypeEnv emptyEnv := by
+  intro x t h; simp [emptyTypeEnv] at h
+
+/-- Looking up a typed variable in a well-typed store yields a value of that type. -/
+theorem store_wellTyped_lookup {Γ : TypeEnv} {ρ : Env} {x : String} {t : WokeType}
+    (hs : StoreWellTyped Γ ρ) (hx : Γ x = some t) :
+    ∃ v, ρ x = some v ∧ HasType emptyTypeEnv (.lit v) t := hs x t hx
+
+/-- **Store-extension lemma.** Extending the context and the store in lockstep with
+a value of the declared type preserves store typing. This is exactly what a
+`varDecl` statement does to the runtime, and the key step for its preservation. -/
+theorem store_wellTyped_extend {Γ : TypeEnv} {ρ : Env} {x : String} {t : WokeType}
+    {v : Value} (hs : StoreWellTyped Γ ρ) (hv : HasType emptyTypeEnv (.lit v) t) :
+    StoreWellTyped (extendTypeEnv x t Γ) (extendEnv x v ρ) := by
+  intro y ty hy
+  simp only [extendTypeEnv] at hy
+  by_cases hxy : (x == y) = true
+  · rw [if_pos hxy] at hy; injection hy with hty; subst hty
+    exact ⟨v, by simp only [extendEnv]; rw [if_pos hxy], hv⟩
+  · rw [if_neg hxy] at hy
+    obtain ⟨v', hv', hvt⟩ := hs y ty hy
+    refine ⟨v', ?_, hvt⟩
+    simp only [extendEnv]; rw [if_neg hxy]; exact hv'
+
 -- =========================================================================
 -- 8. TODO Stubs
 -- =========================================================================