3535 - preservation: stepping preserves types
3636 - type_safety: multi-step evaluation preserves types (by induction + preservation)
3737 - consent_monotonicity / consent_preservation: consent system properties
38+ - StmtExec / StmtsExec (§7e): a big-step statement-execution relation covering
39+ ALL nine statement forms — the simple statements (complain, expr, varDecl,
40+ assign, return_) and the control-flow forms (if_, loop, attempt, consent)
41+ with faithful lexical block scoping (restoreVars rolls block-local
42+ declarations back on exit; enclosing-variable mutations persist).
43+ - stmt_exec_preservation / stmts_exec_preservation: store-typing preservation
44+ for statement execution (a well-typed statement/block run in a well-typed
45+ store yields a store well-typed against its output context). This is a
46+ PRESERVATION-only result: there is no statement-progress or determinism claim.
47+
48+ ### Documented divergences (model vs. the real language)
49+ The execution model is faithful to the type system and to the parts of the
50+ interpreters it covers, but it deliberately abstracts/defers the following —
51+ none is hidden:
52+ - **loop is bool/while-guarded** , inheriting `StmtWellTyped.loop : … .bool`
53+ (the guard is re-evaluated each iteration), whereas the Rust/OCaml
54+ interpreters run a **counted-`int`** loop (`for _ in 0..n`). Making the model
55+ counted would edit the merged statics (`.bool` → `.int`); deferred.
56+ - **attempt** abstracts the result channel: `attemptOk`/`attemptErr` model only
57+ the STORE effect (success keeps outer mutations; error restores the entry
58+ store). Expression panics are not propagated through StmtExec (the simple
59+ rules require evaluation to a `.lit` value), so `attemptErr` is an
60+ abstraction of "an error occurred" rather than a derivation-driven catch; the
61+ `hname` handler binding and the Okay/Oops result wrapping are unmodeled.
62+ - **consent** abstracts the `#care` permission oracle: `consentGrant`/
63+ `consentDeny` are both always available (intentional non-determinism); the
64+ real capability/permission decision lives in the consent/capability theorems.
65+ - **early exit** (return/break/continue) is unmodeled — bodies run to
66+ completion; `return_` only evaluates its expression and keeps the store.
67+ - the `maybe` type constructor exists in `WokeType` but has no typing/eval
68+ rules yet (pre-existing; `result` is the supported option type).
3869
3970 ### Arrays (parity with Coq's WokeLang.v):
4071 `tArray` / `tArrayVal` type array expressions and array literal values
@@ -1779,22 +1810,30 @@ theorem preservation_via_store {e e' : Expr} {ρ ρ' : Env} {t : WokeType}
17791810 store_step_preservation (fun x t h => by simp [emptyTypeEnv] at h) ht hs
17801811
17811812-- =========================================================================
1782- -- 7e. Statement execution — simple-statement fragment (Phase 1b)
1813+ -- 7e. Statement execution — all forms, with block scoping (Phase 1b)
17831814-- =========================================================================
17841815
17851816/- A big-step statement-execution relation `StmtExec s ρ ρ'` ("statement `s`
17861817run in store `ρ` produces store `ρ'`"), with `StmtsExec` threading a block
1787- left-to-right. This increment covers the **simple** statements — those with no
1788- embedded sub-blocks: `complain`, `expr`, `varDecl`, `assign`, `return_`. Each
1789- evaluates its expression (if any) to a value via the closed-store `MultiStep`
1790- (the store is invariant under expression evaluation, `step_store_invariant`),
1791- then applies its store effect. `return_`'s value-propagation / block
1792- short-circuit and the control-flow forms (`if`/`loop`/`attempt`/`consent`,
1793- which introduce block scoping) are deliberately deferred to a later increment.
1794-
1795- The metatheorem is **store-typing preservation** : a well-typed statement run in
1796- a well-typed store yields a store well-typed against the statement's output
1797- context (`StmtWellTyped Γ s Γ'`). -/
1818+ left-to-right. It covers ALL nine statement forms:
1819+
1820+ - the **simple** statements — `complain`, `expr`, `varDecl`, `assign`,
1821+ `return_` — each of which evaluates its expression (if any) to a value via
1822+ the closed-store `MultiStep` (the store is invariant under expression
1823+ evaluation, `step_store_invariant`) then applies its store effect;
1824+ - the **control-flow** forms — `if`/`loop`/`attempt`/`consent` — which run a
1825+ sub-block and then RESTORE the names that block declared to their entry
1826+ values (`restoreVars` + `declaredVars`), faithful lexical scoping in which
1827+ block-local declarations vanish on exit while enclosing-variable mutations
1828+ persist (`loop` carries those mutations across iterations via the restored
1829+ store). See the file header's "Documented divergences" for what `loop`'s
1830+ bool guard, `attempt`'s error/result channel, and `consent`'s permission
1831+ oracle deliberately abstract or defer.
1832+
1833+ **store-typing preservation** : a well-typed statement (or
1834+ block) run in a well-typed store yields a store well-typed against its output
1835+ context (`StmtWellTyped Γ s Γ'`). It is preservation-only — there is no
1836+ statement-progress or determinism claim. -/
17981837
17991838/-- Multi-step store-typed preservation: evaluating a well-typed expression to
18001839completion in a well-typed store yields a value of the same type. The store is
@@ -1904,7 +1943,10 @@ theorem store_wellTyped_restore {Γ Γ₁ : TypeEnv} {ρ ρb : Env} {body : List
19041943 exact ⟨v, by simp only [restoreVars, if_neg hmem]; exact hv, hvt⟩
19051944
19061945mutual
1907- /-- Big-step execution of a single (simple) statement. -/
1946+ /-- Big-step execution of a single statement. Scoping (option A — the Rust
1947+ `Environment{bindings,parent}` discipline) is realized by `restoreVars`; see the
1948+ file header's "Documented divergences" for `loop`'s bool guard, `attempt`'s
1949+ abstracted error/result channel, and `consent`'s abstracted permission oracle. -/
19081950inductive StmtExec : Stmt → Env → Env → Prop where
19091951 | complain : ∀ m ρ, StmtExec (.complain m) ρ ρ
19101952 | expr : ∀ e v ρ, MultiStep e ρ (.lit v) ρ → StmtExec (.expr e) ρ ρ
@@ -1916,8 +1958,8 @@ inductive StmtExec : Stmt → Env → Env → Prop where
19161958 -- Control-flow forms. Each runs its body block, then RESTORES the names the
19171959 -- block declared to their entry values (faithful lexical scoping); outer-var
19181960 -- mutations survive. The bool guard inherits `StmtWellTyped.{if_,loop}`'s
1919- -- `HasType Γ c .bool` premise (see the divergence note : the interpreters use a
1920- -- counted-int `loop`; the merged statics fix `.bool`, deferred to a follow-up ).
1961+ -- `HasType Γ c .bool` premise — DIVERGENCE : the interpreters use a counted-int
1962+ -- `loop` (`for _ in 0..n`) ; the merged statics fix `.bool`, deferred (see header ).
19211963 | ifTrue : ∀ c thn els ρ ρb, MultiStep c ρ (.lit (.vBool true )) ρ → StmtsExec thn ρ ρb →
19221964 StmtExec (.if_ c thn els) ρ (restoreVars (declaredVars thn) ρ ρb)
19231965 | ifFalse : ∀ c thn els ρ ρb, MultiStep c ρ (.lit (.vBool false )) ρ → StmtsExec els ρ ρb →
@@ -1928,11 +1970,18 @@ inductive StmtExec : Stmt → Env → Env → Prop where
19281970 StmtExec (.loop c body) ρ ρ'
19291971 | attemptOk : ∀ body hname ρ ρb, StmtsExec body ρ ρb →
19301972 StmtExec (.attempt body hname) ρ (restoreVars (declaredVars body) ρ ρb)
1931- -- error mid-body: catch, restore the entry store (op-sem [ B-Attempt-Err ] ).
1973+ -- ABSTRACTION: `attemptErr` models the *store* effect of a caught error —
1974+ -- restore the entry store (op-sem [ B-Attempt-Err ] ). Expression panics are NOT
1975+ -- propagated through StmtExec (the simple rules require evaluation to a `.lit`
1976+ -- value), so this is an abstraction of "an error occurred mid-body" rather than
1977+ -- a derivation-driven catch; it is intentionally available non-deterministically
1978+ -- alongside `attemptOk`. The `hname` handler binding / Okay-Oops result are unmodeled.
19321979 | attemptErr : ∀ body hname ρ, StmtExec (.attempt body hname) ρ ρ
19331980 | consentGrant : ∀ p body ρ ρb, StmtsExec body ρ ρb →
19341981 StmtExec (.consent p body) ρ (restoreVars (declaredVars body) ρ ρb)
1935- -- permission denied: skip the body (op-sem [ B-Consent-Deny ] ).
1982+ -- ABSTRACTION: permission denied → skip the body (op-sem [ B-Consent-Deny ] ).
1983+ -- `consentGrant`/`consentDeny` are both always available (the real `#care`
1984+ -- permission oracle is unmodeled here — it lives in the consent/capability theorems).
19361985 | consentDeny : ∀ p body ρ, StmtExec (.consent p body) ρ ρ
19371986/-- Big-step execution of a block, threading the store left-to-right. -/
19381987inductive StmtsExec : List Stmt → Env → Env → Prop where
0 commit comments