feat(proofs): statement typing judgment + metatheory (Lean + Coq)

claude · claude · commit facbf9ac2cf5 · 2026-06-18T11:23:59.000Z
Statements were declared (`Stmt`/`stmt`) but had no typing rules. This adds a context-threading statement typing judgment and its core metatheory, in both provers, at parity. Judgment (mutually inductive with the block form): - StmtWellTyped G s G' — single statement, threads the type context - StmtsWellTyped G ss G' — block, threads context left-to-right All nine forms: varDecl (extends context), assign (requires prior decl at the assigned type), return, if, loop, attempt, consent, expr, complain. Compound statements are block-scoped (they return the incoming context). Metatheorems (all proved, no new axioms): - ctxDomSub_{refl,trans,extend} - stmt_wellTyped_mono / stmts_wellTyped_mono — context monotonicity: a well-typed statement/block never undeclares a variable - stmts_wellTyped_append — sequencing composes - stmts_wellTyped_example — inhabitation smoke (`let x = 0; x`) Method: the single-statement metatheorems are non-recursive (blocks are scoped), which breaks the mutual dependency; the block versions then go by ordinary induction on the list, sidestepping a mutual-induction scheme. Verification: - Lean 4.30.0: `lean WokeLang.lean` exits 0, no warnings, sorry-free. - Coq 8.18.0: `coqc WokeLang.v` exits 0; `Print Assumptions` on all four statement lemmas reports "Closed under the global context" (axiom-free). Purely additive (new section 5b); existing theorems untouched. AUDIT.md updated; the dynamic story (execution + store-typing preservation, which needs open-term expression preservation) is recorded as the next step. Co-Authored-By: Claude Fable 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_013wg3Mtq2QFhYi4XVw1Z6z7
diff --git a/docs/proofs/verification/AUDIT.md b/docs/proofs/verification/AUDIT.md
@@ -65,7 +65,7 @@ the Rust type checker (`src/typechecker/mod.rs`).
 | Result type | `okay`/`oops`/`unwrap`/`error`, `tOkay…tUnwrap` | present in **Rust** typechecker (`Result(_, _)`); **absent** from `core/eval.ml` |
 | Unary | `neg` (int/float), `not` | + measured propagation |
 | Calls / arrays | `call` (no typing rule); **arrays typed + evaluated** (`tArray`/`tArrayVal`, `sArrayStep`/`sArrayVal`/`sArrayErr`) | builtins + user functions; arrays typed |
-| Statements | declared (`Stmt`), **no typing/exec** | full eval in `core/eval.ml` |
+| Statements | **typing judgment** (`StmtWellTyped`, context-threading) + monotonicity/append metatheorems; execution/preservation not yet | full eval in `core/eval.ml` |
 | Units of measure | **not modelled** | `EMeasured` / `VMeasured`, unit-match checking |
 | Pattern matching, workers, custom types | **not modelled** | present |
 | Consent | `consent_monotonicity/preservation` | matches **spec** `axiomatic-semantics.md` (consent Hoare logic) |
@@ -113,9 +113,17 @@ the implementations toward it, or (b) build a *second* Lean model faithful to
    **DONE (2026-06-18).** `tArray`/`tArrayVal` + `sArrayStep`/`sArrayVal`/
    `sArrayErr`, with full `progress`/`preservation` coverage (see
    "Extensions landed" below). This brings Lean to parity with Coq on arrays.
-3. **Decide the eval-correspondence question** (a) vs (b) above with the
+3. ~~Statement typing~~ — **DONE (2026-06-18):** `StmtWellTyped`/
+   `StmtsWellTyped` + monotonicity/append (see "Statement typing landed"
+   below). **Next on statements: a dynamic story** — a statement execution
+   relation + a store-typing *preservation* theorem. The prerequisite is
+   generalising the expression `preservation`/`type_safety` to **open** terms
+   (non-empty context + a store-typing agreement), since statement-embedded
+   expressions reference declared variables (the current expression proofs
+   assume the empty context, deriving a contradiction in the `var` case).
+4. **Decide the eval-correspondence question** (a) vs (b) above with the
    maintainer before attempting PROOF-NEEDS #2.
-4. **Compiler/VM track** (the file's §8 TODO stubs: bytecode, compiler,
+5. **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)
@@ -155,6 +163,38 @@ theorems (`weaken_collapses_distinction`, `affine_canonical`,
 - Still open in Tier 1: **float** arithmetic variants (`sub`/`mul`/`div` on
   `float`, mirroring `add` on float).
 
+## Statement typing landed (2026-06-18) — both provers, in parity
+
+Statements went from *declared datatype with no judgments* to a typed
+sub-language with machine-checked metatheory, in **both** Lean (`WokeLang.lean`)
+and Coq (`WokeLang.v`):
+
+- **Judgment** `StmtWellTyped Γ s Γ'` / `StmtsWellTyped Γ ss Γ'` — a
+  context-threading typing relation over all nine statement forms (`varDecl`,
+  `assign`, `return`, `if`, `loop`, `attempt`, `consent`, `expr`, `complain`),
+  mutually inductive (blocks contain statements). `varDecl` extends the
+  context; `assign` requires a prior declaration at the assigned type;
+  compound statements are block-scoped (they return the incoming context).
+  This is the statement-level analogue of the expression `has_type`/`HasType`.
+- **Metatheorems (all proved):**
+  - `ctxDomSub_{refl,trans,extend}` — the context-domain preorder + the
+    extension fact;
+  - `stmt_wellTyped_mono` / `stmts_wellTyped_mono` — **context monotonicity**:
+    a well-typed statement (or block) never undeclares a variable;
+  - `stmts_wellTyped_append` — **sequencing composes**: typing one block then
+    another from the resulting context types their concatenation;
+  - `stmts_wellTyped_example` — an inhabitation smoke (`let x = 0; x`).
+- **Method note:** the single-statement metatheorems are non-recursive (blocks
+  are scoped), which breaks the mutual dependency; the block versions then go
+  by ordinary induction on the *list* (sidestepping a mutual-induction scheme).
+- **Soundness:** Lean is `sorry`-free; in Coq `Print Assumptions` reports all
+  four statement lemmas **"Closed under the global context"** — i.e. axiom-free
+  (they do not touch the classical-reals axioms the float fragment needs).
+
+**Still open on statements:** the *dynamic* story — an execution relation +
+store-typing preservation — which first needs open-term expression
+preservation (see "Recommended next proof steps" #3).
+
 ## Arrays landed (2026-06-18) — Lean now at parity with Coq
 
 The one array-shaped Tier-1 gap is closed on the Lean side, mirroring Coq's
diff --git a/docs/proofs/verification/WokeLang.lean b/docs/proofs/verification/WokeLang.lean
@@ -1171,6 +1171,120 @@ theorem type_safety : ∀ e t v ρ,
   | step e₁ e₂ e₃ ρ₁ ρ₂ ρ₃ hs hms' ih =>
     exact ih (preservation e₁ e₂ t ρ₁ ρ₂ ht hs) hev
 
+-- =========================================================================
+-- 5b. Statement Typing
+-- =========================================================================
+
+/- Statement typing threads a type context: `StmtWellTyped Γ s Γ'` reads
+   "in context `Γ`, statement `s` is well-typed and yields context `Γ'`".
+   `varDecl` extends the context with the declared binding; `assign` requires
+   the variable to already be declared at the assigned type; compound
+   statements (`if`/`loop`/`attempt`/`consent`) are block-scoped, so they
+   return the incoming context. Mutually inductive with `StmtsWellTyped`,
+   which threads the context left-to-right through a block.
+
+   This is the statement-level analogue of the expression `HasType` judgment;
+   statements were previously declared (`Stmt`) but had no typing rules. The
+   dynamic story (a statement execution relation + a store-typing preservation
+   theorem) is the natural next step and is noted in AUDIT.md. -/
+mutual
+inductive StmtWellTyped : TypeEnv → Stmt → TypeEnv → Prop where
+  | varDecl : ∀ Γ x e t,
+      HasType Γ e t →
+      StmtWellTyped Γ (.varDecl x e) (extendTypeEnv x t Γ)
+  | assign : ∀ Γ x e t,
+      Γ x = some t → HasType Γ e t →
+      StmtWellTyped Γ (.assign x e) Γ
+  | return_ : ∀ Γ e t,
+      HasType Γ e t →
+      StmtWellTyped Γ (.return_ e) Γ
+  | if_ : ∀ Γ c thn els Γ₁ Γ₂,
+      HasType Γ c .bool → StmtsWellTyped Γ thn Γ₁ → StmtsWellTyped Γ els Γ₂ →
+      StmtWellTyped Γ (.if_ c thn els) Γ
+  | loop : ∀ Γ c body Γ₁,
+      HasType Γ c .bool → StmtsWellTyped Γ body Γ₁ →
+      StmtWellTyped Γ (.loop c body) Γ
+  | attempt : ∀ Γ body hname Γ₁,
+      StmtsWellTyped Γ body Γ₁ →
+      StmtWellTyped Γ (.attempt body hname) Γ
+  | consent : ∀ Γ p body Γ₁,
+      StmtsWellTyped Γ body Γ₁ →
+      StmtWellTyped Γ (.consent p body) Γ
+  | expr : ∀ Γ e t,
+      HasType Γ e t →
+      StmtWellTyped Γ (.expr e) Γ
+  | complain : ∀ Γ m,
+      StmtWellTyped Γ (.complain m) Γ
+inductive StmtsWellTyped : TypeEnv → List Stmt → TypeEnv → Prop where
+  | nil : ∀ Γ, StmtsWellTyped Γ [] Γ
+  | cons : ∀ Γ s ss Γ₁ Γ₂,
+      StmtWellTyped Γ s Γ₁ → StmtsWellTyped Γ₁ ss Γ₂ →
+      StmtsWellTyped Γ (s :: ss) Γ₂
+end
+
+/-- Domain containment on type contexts: every variable declared in `Γ` is
+    still declared (at some type) in `Γ'`. -/
+def CtxDomSub (Γ Γ' : TypeEnv) : Prop := ∀ x t, Γ x = some t → ∃ t', Γ' x = some t'
+
+theorem ctxDomSub_refl (Γ : TypeEnv) : CtxDomSub Γ Γ := fun _ t h => ⟨t, h⟩
+
+theorem ctxDomSub_trans {Γ₁ Γ₂ Γ₃ : TypeEnv}
+    (h₁₂ : CtxDomSub Γ₁ Γ₂) (h₂₃ : CtxDomSub Γ₂ Γ₃) : CtxDomSub Γ₁ Γ₃ :=
+  fun x t h => let ⟨t', h'⟩ := h₁₂ x t h; h₂₃ x t' h'
+
+theorem ctxDomSub_extend (Γ : TypeEnv) (x : String) (t : WokeType) :
+    CtxDomSub Γ (extendTypeEnv x t Γ) := by
+  intro y ty hy
+  by_cases hxy : x = y
+  · exact ⟨t, by simp [extendTypeEnv, hxy]⟩
+  · exact ⟨ty, by simp [extendTypeEnv, hxy, hy]⟩
+
+/-- Context monotonicity (single statement): a well-typed statement never
+    undeclares a variable. Non-recursive — compound statements are
+    block-scoped, which breaks the mutual dependency for the proof. -/
+theorem stmt_wellTyped_mono {Γ s Γ'} (h : StmtWellTyped Γ s Γ') : CtxDomSub Γ Γ' := by
+  cases h with
+  | varDecl Γ x e t _ => exact ctxDomSub_extend Γ x t
+  | assign => exact ctxDomSub_refl _
+  | return_ => exact ctxDomSub_refl _
+  | if_ => exact ctxDomSub_refl _
+  | loop => exact ctxDomSub_refl _
+  | attempt => exact ctxDomSub_refl _
+  | consent => exact ctxDomSub_refl _
+  | expr => exact ctxDomSub_refl _
+  | complain => exact ctxDomSub_refl _
+
+/-- Context monotonicity (statement block), by induction on the block. -/
+theorem stmts_wellTyped_mono {Γ ss Γ'} (h : StmtsWellTyped Γ ss Γ') : CtxDomSub Γ Γ' := by
+  induction ss generalizing Γ Γ' with
+  | nil => cases h; exact ctxDomSub_refl _
+  | cons s rest ih =>
+    cases h with
+    | cons _ _ _ Γ₁ _ hs hrest => exact ctxDomSub_trans (stmt_wellTyped_mono hs) (ih hrest)
+
+/-- Sequencing composes: typing a block then another block from the resulting
+    context types their concatenation. -/
+theorem stmts_wellTyped_append {Γ ss₁ Γ' ss₂ Γ''}
+    (h₁ : StmtsWellTyped Γ ss₁ Γ') (h₂ : StmtsWellTyped Γ' ss₂ Γ'') :
+    StmtsWellTyped Γ (ss₁ ++ ss₂) Γ'' := by
+  induction ss₁ generalizing Γ Γ' with
+  | nil => cases h₁; exact h₂
+  | cons s rest ih =>
+    cases h₁ with
+    | cons _ _ _ Γ₁ _ hs hrest => exact .cons _ _ _ _ _ hs (ih hrest h₂)
+
+/-- Inhabitation smoke: `let x = 0; x` is a well-typed block, yielding a
+    context in which `x : int`. -/
+theorem stmts_wellTyped_example :
+    StmtsWellTyped emptyTypeEnv
+      [Stmt.varDecl "x" (.lit (.vInt 0)), Stmt.expr (.var "x")]
+      (extendTypeEnv "x" .int emptyTypeEnv) :=
+  .cons _ _ _ _ _
+    (.varDecl _ "x" (.lit (.vInt 0)) .int (.tInt _ _))
+    (.cons _ _ _ _ _
+      (.expr _ (.var "x") .int (.tVar _ "x" .int (by simp [extendTypeEnv])))
+      (.nil _))
+
 -- =========================================================================
 -- 6. Consent System
 -- =========================================================================
diff --git a/docs/proofs/verification/WokeLang.v b/docs/proofs/verification/WokeLang.v
@@ -1398,6 +1398,130 @@ Proof.
     eapply preservation; eauto.
 Qed.
 
+(* ========================================================================= *)
+(* 5b. Statement Typing                                                       *)
+(* ========================================================================= *)
+
+(** Statement typing threads a type context: [StmtWellTyped G s G'] reads
+    "in context [G], statement [s] is well-typed and yields context [G']".
+    [SVarDecl] extends the context; [SAssign] requires the variable already
+    declared at the assigned type; compound statements ([SIf]/[SLoop]/
+    [SAttempt]/[SConsent]) are block-scoped, so they return the incoming
+    context. Mutually inductive with [StmtsWellTyped] for blocks. Mirrors
+    StmtWellTyped/StmtsWellTyped in WokeLang.lean (cross-prover parity).
+
+    This is the statement-level analogue of the [has_type] expression
+    judgment; statements were previously declared ([stmt]) but had no typing
+    rules. A statement execution relation + store-typing preservation is the
+    natural next step (see AUDIT.md). *)
+
+Inductive StmtWellTyped : type_env -> stmt -> type_env -> Prop :=
+  | SWT_VarDecl : forall G x e t,
+      has_type G e t ->
+      StmtWellTyped G (SVarDecl x e) (extend_type_env x t G)
+  | SWT_Assign : forall G x e t,
+      G x = Some t -> has_type G e t ->
+      StmtWellTyped G (SAssign x e) G
+  | SWT_Return : forall G e t,
+      has_type G e t ->
+      StmtWellTyped G (SReturn e) G
+  | SWT_If : forall G c thn els G1 G2,
+      has_type G c TBool ->
+      StmtsWellTyped G thn G1 -> StmtsWellTyped G els G2 ->
+      StmtWellTyped G (SIf c thn els) G
+  | SWT_Loop : forall G c body G1,
+      has_type G c TBool -> StmtsWellTyped G body G1 ->
+      StmtWellTyped G (SLoop c body) G
+  | SWT_Attempt : forall G body h G1,
+      StmtsWellTyped G body G1 ->
+      StmtWellTyped G (SAttempt body h) G
+  | SWT_Consent : forall G p body G1,
+      StmtsWellTyped G body G1 ->
+      StmtWellTyped G (SConsent p body) G
+  | SWT_Expr : forall G e t,
+      has_type G e t ->
+      StmtWellTyped G (SExpr e) G
+  | SWT_Complain : forall G m,
+      StmtWellTyped G (SComplain m) G
+
+with StmtsWellTyped : type_env -> list stmt -> type_env -> Prop :=
+  | SsWT_nil : forall G, StmtsWellTyped G nil G
+  | SsWT_cons : forall G s ss G1 G2,
+      StmtWellTyped G s G1 -> StmtsWellTyped G1 ss G2 ->
+      StmtsWellTyped G (s :: ss) G2.
+
+(** Domain containment: every variable declared in [G] is still declared
+    (at some type) in [G']. *)
+Definition CtxDomSub (G G' : type_env) : Prop :=
+  forall x t, G x = Some t -> exists t', G' x = Some t'.
+
+Lemma ctxDomSub_refl : forall G, CtxDomSub G G.
+Proof. intros G x t H. exists t. exact H. Qed.
+
+Lemma ctxDomSub_trans : forall G1 G2 G3,
+  CtxDomSub G1 G2 -> CtxDomSub G2 G3 -> CtxDomSub G1 G3.
+Proof.
+  intros G1 G2 G3 H12 H23 x t H.
+  destruct (H12 x t H) as [t' H']. exact (H23 x t' H').
+Qed.
+
+Lemma ctxDomSub_extend : forall G x t, CtxDomSub G (extend_type_env x t G).
+Proof.
+  intros G x t y ty Hy. unfold extend_type_env.
+  destruct (String.eqb x y) eqn:Hxy.
+  - exists t. reflexivity.
+  - exists ty. exact Hy.
+Qed.
+
+(** Context monotonicity (single statement): a well-typed statement never
+    undeclares a variable. *)
+Lemma stmt_wellTyped_mono : forall G s G',
+  StmtWellTyped G s G' -> CtxDomSub G G'.
+Proof.
+  intros G s G' H. inversion H; subst;
+    first [ apply ctxDomSub_refl | apply ctxDomSub_extend ].
+Qed.
+
+(** Context monotonicity (statement block), by induction on the block. *)
+Lemma stmts_wellTyped_mono : forall ss G G',
+  StmtsWellTyped G ss G' -> CtxDomSub G G'.
+Proof.
+  induction ss as [| s rest IH]; intros G G' H; inversion H; subst.
+  - apply ctxDomSub_refl.
+  - eapply ctxDomSub_trans.
+    + eapply stmt_wellTyped_mono; eassumption.
+    + eapply IH; eassumption.
+Qed.
+
+(** Sequencing composes: typing a block then another from the resulting
+    context types their concatenation. *)
+Lemma stmts_wellTyped_append : forall ss1 G G' ss2 G'',
+  StmtsWellTyped G ss1 G' -> StmtsWellTyped G' ss2 G'' ->
+  StmtsWellTyped G (ss1 ++ ss2) G''.
+Proof.
+  induction ss1 as [| s rest IH]; intros G G' ss2 G'' H1 H2;
+    inversion H1; subst; simpl.
+  - exact H2.
+  - eapply SsWT_cons.
+    + eassumption.
+    + eapply IH; eassumption.
+Qed.
+
+(** Inhabitation smoke: [let x = 0; x] is a well-typed block, yielding a
+    context in which [x : TInt]. *)
+Example stmts_wellTyped_example :
+  StmtsWellTyped empty_type_env
+    (SVarDecl "x"%string (ELit (VInt 0)) :: SExpr (EVar "x"%string) :: nil)
+    (extend_type_env "x"%string TInt empty_type_env).
+Proof.
+  eapply SsWT_cons.
+  - apply SWT_VarDecl with (t := TInt). apply T_Int.
+  - eapply SsWT_cons.
+    + apply SWT_Expr with (t := TInt). apply T_Var.
+      unfold extend_type_env. rewrite String.eqb_refl. reflexivity.
+    + apply SsWT_nil.
+Qed.
+
 (* ========================================================================= *)
 (* 6. Consent System                                                         *)
 (* ========================================================================= *)
