Phase 1b substrate: expression-evaluation invariants under a store (#113)

## What

The layer the statement-execution relation sits on — three hole-free
lemmas
about how expression evaluation interacts with the runtime store.

| Lemma | Statement |
|---|---|
| `step_store_invariant` | a single expression step never mutates `ρ` |
| `multiStep_store_invariant` | the same for multi-step evaluation, by
transitivity |
| `hasType_lit_any` | literal typing is context-independent — a typing
for `.lit v` in one context holds in any context |

**Why these, in this order.** Per the agreed rule — *land the
lowest-complexity,
safe, **complete** unit first* — these are the substrate the next step
(statement
execution) rests on, strictly above the store-typing lemmas just merged
(#112):

- **Store invariance** is what lets statement execution compose: an
expression
sub-evaluation inside a statement cannot disturb the variable bindings
the
statement effect then acts on (base `Step` rules keep the store;
congruence
  rules thread it unchanged; transitivity lifts it to `MultiStep`).
- **`hasType_lit_any`** is the weakening that lifts `StoreWellTyped`'s
  `HasType emptyTypeEnv (.lit v) t` into the arbitrary context `Γ` that
statement-level expression typing lives in — needed for the `sVar` case
of the
  generalized, store-typed preservation that comes next.

## Correction to an earlier note

The roadmap previously said the expression `Step` is "closed-term-only,
so
variable resolution needs design." That was wrong: `Step` has an `sVar`
rule that
resolves variables from `ρ` directly. The closed-context restriction was
only ever
in the `emptyTypeEnv`-stated `progress`/`preservation`. The roadmap is
corrected,
and the remaining Phase 1b path is now: generalized store-typed
preservation
(`HasType Γ e t` under `StoreWellTyped Γ ρ`) → statement-execution
relation →
statement preservation.

## Verification

- `lean docs/proofs/verification/WokeLang.lean` exits 0 (Lean 4.30.0,
Mathlib-free, single-file).
- Hole-free: `step_store_invariant` / `multiStep_store_invariant` use
the classical
kernel base (`propext`, `Classical.choice`); **`hasType_lit_any` depends
on no axioms**.
  No `sorryAx`, no project-specific assumptions.

## Scope

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

@@ -141,10 +141,19 @@ unlock Phases 1c / 3a / 4a.
   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.
+  `varDecl` — preserves store typing). Hole-free (axiom `propext` only).
+- [~] **Phase 1b (substrate)** — **expression-evaluation invariants under a store**, the
+  layer the statement-execution relation sits on: `step_store_invariant` and
+  `multiStep_store_invariant` (expression evaluation never mutates `ρ` — so a sub-evaluation
+  inside a statement can't disturb the bindings the statement effect then acts on), and
+  `hasType_lit_any` (literal typing is context-independent — the weakening that lifts
+  `StoreWellTyped`'s `HasType emptyTypeEnv (.lit v) t` into the arbitrary `Γ` statement-level
+  typing uses). Hole-free (`hasType_lit_any` needs **no** axioms). *Correction to the prior
+  note:* the expression `Step` is **not** closed-term-only — it has an `sVar` rule that
+  resolves variables from `ρ`; the closed-context use was only in the `emptyTypeEnv`-stated
+  `progress`/`preservation`. So the remaining work is a generalized store-typed preservation
+  (`HasType Γ e t` under `StoreWellTyped Γ ρ`), then the statement-execution relation itself.
+- [ ] Phase 1 (cont.: `[T-Call]` after 1b), 1b (store-typed preservation → 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

@@ -1509,6 +1509,58 @@ theorem store_wellTyped_extend {Γ : TypeEnv} {ρ : Env} {x : String} {t : WokeT
     refine ⟨v', ?_, hvt⟩
     simp only [extendEnv]; rw [if_neg hxy]; exact hv'
 
+-- =========================================================================
+-- 7d. Expression-evaluation invariants under a store (Phase 1b substrate)
+-- =========================================================================
+
+/-- **Expression evaluation never mutates the store.** Every base reduction
+returns the store it was given, and every congruence rule threads the
+sub-step's store unchanged, so a single expression step leaves `ρ` fixed. This
+is what lets statement execution compose: an expression sub-evaluation inside a
+statement cannot disturb the variable bindings the statement effect then acts on. -/
+theorem step_store_invariant {e e' : Expr} {ρ ρ' : Env}
+    (h : Step e ρ e' ρ') : ρ' = ρ := by
+  induction h with
+  | sBinOpLeft _ _ _ _ _ _ _ ih => exact ih
+  | sBinOpRight _ _ _ _ _ _ _ _ ih => exact ih
+  | sUnOpCong _ _ _ _ _ _ ih => exact ih
+  | sOkayCong _ _ _ _ _ ih => exact ih
+  | sOopsCong _ _ _ _ _ ih => exact ih
+  | sUnwrapCong _ _ _ _ _ ih => exact ih
+  | sArrayStep _ _ _ _ _ _ _ ih => exact ih
+  | _ => rfl
+
+/-- Multi-step evaluation is store-preserving too, by transitivity. -/
+theorem multiStep_store_invariant {e e' : Expr} {ρ ρ' : Env}
+    (h : MultiStep e ρ e' ρ') : ρ' = ρ := by
+  induction h with
+  | refl => rfl
+  | step _ _ _ _ _ _ hs _ ih => rw [ih]; exact step_store_invariant hs
+
+/-- **Literal typing is context-independent.** A literal value's type is
+determined structurally and never consults the type context, so a typing for
+`.lit v` in one context holds in any context. This is the weakening that lifts
+`StoreWellTyped`'s `HasType emptyTypeEnv (.lit v) t` into the arbitrary context
+`Γ` that statement-level expression typing lives in. -/
+theorem hasType_lit_any {Γ Γ' : TypeEnv} {v : Value} {t : WokeType}
+    (h : HasType Γ (.lit v) t) : HasType Γ' (.lit v) t := by
+  -- Generalise to a same-expression form so the `vOkay`/`vArray` recursions get
+  -- usable induction hypotheses; the `∃ w, e = .lit w` guard rules out the
+  -- non-literal typing rules (which `induction` still enumerates).
+  have gen : ∀ {Δ e t'}, HasType Δ e t' → ∀ {Δ'}, (∃ w, e = .lit w) → HasType Δ' e t' := by
+    intro Δ e t' hh
+    induction hh with
+    | tInt n => intro _ _; exact .tInt _ _
+    | tFloat f => intro _ _; exact .tFloat _ _
+    | tString s => intro _ _; exact .tString _ _
+    | tBool b => intro _ _; exact .tBool _ _
+    | tUnit => intro _ _; exact .tUnit _
+    | tOkayVal w t'' _ ih => intro _ _; exact .tOkayVal _ _ _ (ih ⟨w, rfl⟩)
+    | tOopsVal s t'' => intro _ _; exact .tOopsVal _ _ _
+    | tArrayVal vs t'' _ ih => intro _ _; exact .tArrayVal _ _ _ (fun w hw => ih w hw ⟨w, rfl⟩)
+    | _ => intro _ hlit; obtain ⟨w, hw⟩ := hlit; nomatch hw
+  exact gen h ⟨v, rfl⟩
+
 -- =========================================================================
 -- 8. TODO Stubs
 -- =========================================================================