diff --git a/PLAN.md b/PLAN.md
index 26c725c4..66475af3 100644
--- a/PLAN.md
+++ b/PLAN.md
@@ -52,11 +52,16 @@ Design decisions baked into that statement:
     `Account.codeHash`; `blockHashOf` agrees with the header lookup;
   - halt: `st.halted` corresponds to `s.halt`/`s.hReturn`
     (`stop ↦ Success`, `return ↦ Returned+payload`, `revert ↦ Reverted+payload`,
-    `invalid ↦ Exception InvalidInstruction`; `none ↦ Running`);
-  - plus frame-level side conditions: `callStack = []`, `permitStateMutation = true`,
-    `codeAddr` is not a precompile, `fork = Osaka` (all supported ops are active
-    there; parameterizing over a range of compatible forks is a later
-    generalization).
+    `invalid ↦ Exception InvalidInstruction`,
+    `staticViolation ↦ Exception StaticModeViolation`; `none ↦ Running`);
+  - plus frame-level side conditions: `callStack = []`, `codeAddr` is not a
+    precompile, `fork = Osaka` (all supported ops are active there; parameterizing
+    over a range of compatible forks is a later generalization). The frame's
+    mutation permission is **not** constrained: `FrameOK` says nothing about
+    `permitStateMutation`, so both ordinary (`= true`) and static (`= false`)
+    frames are covered with no carve-out. In a static frame the state-modifying
+    built-ins the source forbids (`sstore`/`tstore`/`log0`–`log4`/`selfdestruct`,
+    value-bearing `call`, `create`/`create2`) halt with `StaticModeViolation`.
 * A Yul `.normal` outcome means the compiled code runs off the end of the bytecode;
   `Decode.decodeAt` yields an implicit `STOP` there (Yellow-Paper zero padding), so the
   target halts with `.Success` — i.e. straight-line Yul that falls through behaves
diff --git a/README.md b/README.md
index 07daf8ca..d109708e 100644
--- a/README.md
+++ b/README.md
@@ -194,6 +194,19 @@ created in the current transaction and pre-existing contracts. Actual account
 deletion is a transaction-finalization operation in evm-semantics and lies
 outside this frame-level compiler theorem.
 
+**Static-call context.** The theorem covers both ordinary and static
+(`STATICCALL`) frames with no carve-out — `FrameOK` no longer constrains
+`permitStateMutation` at all. In a static frame every state-modifying built-in
+that the source forbids halts with `Exception .StaticModeViolation`, matching
+the source's `.staticViolation`: the local writers
+`sstore`/`tstore`/`log0`–`log4`/`selfdestruct` fire the target's generic static
+gate, and the open-world `call` (value-bearing) / `create` / `create2` gates
+fire their dedicated target static rules. The value-free calls
+`callcode`/`delegatecall`/`staticcall` execute normally, propagating the static
+flag into the callee (a value-bearing `callcode` is a self-transfer — a
+world-state no-op — so, matching EIP-214 / the EVM, it is not rejected in a
+static frame).
+
 The headline theorems check with no `sorry`. Their `#print axioms` footprint is
 exactly the three standard classical axioms (`propext`, `Classical.choice`,
 `Quot.sound`) and nothing else — the `ByteArray` facts used by `MSTORE` are all
diff --git a/YulEvmCompiler/Correctness.lean b/YulEvmCompiler/Correctness.lean
index c31b56ad..0b7e104f 100644
--- a/YulEvmCompiler/Correctness.lean
+++ b/YulEvmCompiler/Correctness.lean
@@ -274,6 +274,10 @@ theorem compile_correct_eval (hexternal : ExternalsRealized model)
           have hhalt : s'.halt = .Exception .InvalidMemoryAccess := hhmatch
           exact ⟨by rw [hhalt]; simp, by
             rw [State.toResult_exception s' _ hhalt]; rfl⟩
+        | staticViolation =>
+          have hhalt : s'.halt = .Exception .StaticModeViolation := hhmatch
+          exact ⟨by rw [hhalt]; simp, by
+            rw [State.toResult_exception s' _ hhalt]; rfl⟩
         | selfdestruct =>
           obtain ⟨hhalt, _⟩ := hhmatch
           exact ⟨by rw [hhalt]; simp, by
diff --git a/YulEvmCompiler/LowerCorrect.lean b/YulEvmCompiler/LowerCorrect.lean
index 3754f1b8..7a0763ed 100644
--- a/YulEvmCompiler/LowerCorrect.lean
+++ b/YulEvmCompiler/LowerCorrect.lean
@@ -459,6 +459,87 @@ theorem astep_sim [model : ExternalModel] (hexternal : ExternalsRealized model)
       exact congrArg UInt256.ofNat (by omega)
     · rw [hstk2, hstk1]
 
+/-- **Phase B, open-world static halt**: a state-modifying external built-in
+attempted in a static frame. `call` (value-bearing) / `create` / `create2`
+halt with `Exception .StaticModeViolation` via their dedicated target static
+gates, matching the source's `.staticViolation`. `callcode` (value-bearing
+`callcode` is a self-transfer, a world-state no-op, so it is *not* rejected in
+a static frame — matching EIP-214 / the EVM), `delegatecall`, `staticcall`, and
+`gas` never produce a relational halt. -/
+theorem externalStaticHaltStep [model : ExternalModel]
+    {yop : Op} {o : Operation} (hop : opTable yop = some o)
+    (hexternal : IsExternalOp yop)
+    {args : List U256} {yst yst' : EvmState}
+    (hhalt : builtinWithExternal model.calls model.creates yop args yst (.halt yst'))
+    {code : ByteArray} {pre post : List UInt8} {σ : List UInt256} {s : State}
+    (hcode : code = mkCode (pre ++ (Instr.op o).bytes ++ post))
+    (hf : FrameOK code s) (hm : StateMatch yst s)
+    (hpc : s.pc = UInt256.ofNat pre.length)
+    (hstk : s.stack = args.map conv ++ σ) :
+    HaltStep s yst' := by
+  have hstatic : yst.env.static = true :=
+    builtinWithExternal_halt_external_imp_static hexternal hhalt
+  have hperm : s.executionEnv.permitStateMutation = false :=
+    hm.perm_of_static_true hstatic
+  obtain ⟨hb, hplain⟩ := opTable_roundtrip hop
+  have hdec : s.decodedOp = some o :=
+    decoded_op hf hcode hpc hb hplain (opTable_available hop)
+  cases yop
+  case call =>
+    obtain rfl : o = .CALL := by simpa [opTable] using hop.symm
+    rcases args with _|⟨g,_|⟨t,_|⟨val,_|⟨ao,_|⟨al,_|⟨ro,_|⟨rl,_|⟨e,rest⟩⟩⟩⟩⟩⟩⟩⟩ <;>
+      simp only [builtinWithExternal, hstatic, true_and] at hhalt
+    split at hhalt
+    · rename_i hval
+      obtain rfl : yst' = { yst with halted := some (.staticViolation, []) } := by
+        simpa using hhalt
+      have hstk7 : s.stack = conv g :: conv t :: conv val :: conv ao :: conv al ::
+          conv ro :: conv rl :: σ := by simpa using hstk
+      exact staticHaltStepGen hm hf.callStack
+        (EVM.Step.running hf.running hf.noPrecompile
+          (StepRunning.callStatic s (conv g) (conv t) (conv val) (conv ao) (conv al)
+            (conv ro) (conv rl) σ hdec hstk7 hperm
+            (by rw [conv_toNat]; intro h; exact hval (BitVec.toNat_injective (by simpa using h)))))
+    · exfalso
+      obtain ⟨resp, -, heq⟩ := hhalt
+      simp at heq
+  case callcode =>
+    exfalso
+    rcases args with _|⟨g,_|⟨t,_|⟨val,_|⟨ao,_|⟨al,_|⟨ro,_|⟨rl,_|⟨e,rest⟩⟩⟩⟩⟩⟩⟩⟩ <;>
+      simp [builtinWithExternal, YulSemantics.EVM.externalCall] at hhalt
+  case create =>
+    obtain rfl : o = .CREATE := by simpa [opTable] using hop.symm
+    rcases args with _|⟨val,_|⟨off,_|⟨sz,_|⟨e,rest⟩⟩⟩⟩ <;>
+      simp only [builtinWithExternal, hstatic, if_true] at hhalt
+    obtain rfl : yst' = { yst with halted := some (.staticViolation, []) } := by
+      simpa using hhalt
+    have hstk3 : s.stack = conv val :: conv off :: conv sz :: σ := by simpa using hstk
+    exact staticHaltStepGen hm hf.callStack
+      (EVM.Step.running hf.running hf.noPrecompile
+        (StepRunning.createStatic s (conv val) (conv off) (conv sz) σ hdec hstk3 hperm))
+  case create2 =>
+    obtain rfl : o = .CREATE2 := by simpa [opTable] using hop.symm
+    rcases args with _|⟨val,_|⟨off,_|⟨sz,_|⟨salt,_|⟨e,rest⟩⟩⟩⟩⟩ <;>
+      simp only [builtinWithExternal, hstatic, if_true] at hhalt
+    obtain rfl : yst' = { yst with halted := some (.staticViolation, []) } := by
+      simpa using hhalt
+    have hstk4 : s.stack = conv val :: conv off :: conv sz :: conv salt :: σ := by
+      simpa using hstk
+    exact staticHaltStepGen hm hf.callStack
+      (EVM.Step.running hf.running hf.noPrecompile
+        (StepRunning.create2Static s (conv val) (conv off) (conv sz) (conv salt) σ
+          hdec hstk4 hperm))
+  case delegatecall =>
+    exfalso
+    rcases args with _|⟨g,_|⟨t,_|⟨io,_|⟨isz,_|⟨oo,_|⟨ol,_|⟨e,rest⟩⟩⟩⟩⟩⟩⟩ <;>
+      simp [builtinWithExternal, YulSemantics.EVM.externalCall] at hhalt
+  case staticcall =>
+    exfalso
+    rcases args with _|⟨g,_|⟨t,_|⟨io,_|⟨isz,_|⟨oo,_|⟨ol,_|⟨e,rest⟩⟩⟩⟩⟩⟩⟩ <;>
+      simp [builtinWithExternal, YulSemantics.EVM.externalCall] at hhalt
+  case gas => simp [opTable] at hop
+  all_goals exact absurd hexternal (by decide)
+
 /-- **Phase B, halting step**: a halting built-in maps to one halting EVM
 step. -/
 theorem ahalt_sim [model : ExternalModel]
@@ -479,10 +560,17 @@ theorem ahalt_sim [model : ExternalModel]
     by_cases hexternal : IsExternalOp yop
     · refine ⟨0, ?_⟩
       intro s hm hgas
-      have hstatic := builtinWithExternal_halt_external_imp_static hexternal hstepOp
-      have hnotStatic : yst.env.static = false := by
-        simpa [hm.frame.perm] using hm.smatch.env.static
-      simp [hnotStatic] at hstatic
+      have hpos : codeSize prog - codeSize (Asm.op yop :: c) = codeSize pre := by
+        rw [codeSize_cons]
+        omega
+      have hhalt := externalStaticHaltStep hop hexternal hstepOp
+        (σ := mapStk prog σ)
+        (assembleWithPayload_at₁ hbytes payload)
+        hm.frame hm.smatch
+        (by rw [hm.pc, hpos, hlenPre])
+        (by rw [hm.stack, mapStk_words])
+      obtain ⟨s', hstep, hsm', hcs', hhm'⟩ := hhalt
+      exact ⟨s', .trans hstep (.refl _), hsm', hcs', hhm'⟩
     · have hstepLocal :=
         (builtinWithExternal_halt_iff_stepOp_of_not_external hexternal).mp hstepOp
       refine ⟨opBound yop args, ?_⟩
diff --git a/YulEvmCompiler/OpStep.lean b/YulEvmCompiler/OpStep.lean
index f9a99b33..89454747 100644
--- a/YulEvmCompiler/OpStep.lean
+++ b/YulEvmCompiler/OpStep.lean
@@ -282,7 +282,7 @@ theorem pushStepU {code : ByteArray} {pre post : List UInt8} {u : UInt256}
     omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.pushN s ⟨32, by decide⟩ u 32 (by decide) hdec hgas'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen,
@@ -354,7 +354,7 @@ theorem dupStep {code : ByteArray} {pre post : List UInt8} {n : Fin 16}
     omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.dup s n v hdec hgas' hget),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -389,7 +389,7 @@ theorem swapStep {code : ByteArray} {pre post : List UInt8} {n : Fin 16}
     omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.swap s n stk' hdec hgas' hswap),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -424,7 +424,7 @@ theorem popStep {code : ByteArray} {pre post : List UInt8}
     omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.pop s a rest hdec hgas' hstk),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -484,7 +484,7 @@ private theorem binPure
     rw [hfork]; omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (mk s (conv a) (conv b) σ hdec hgas' hstk'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -532,7 +532,7 @@ private theorem nullaryRead {yv : U256} {sv : UInt256}
   have hstk0 : s.stack = σ := by simpa using hstk
   have hgas' : Gas.baseCost s.fork o ≤ s.gasAvailable := by rw [hfork]; omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile (mk hdec hgas'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -583,7 +583,7 @@ private theorem unPure
     rw [hfork]; omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (mk s (conv a) σ hdec hgas' hstk'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -637,7 +637,7 @@ private theorem terPure
     rw [hfork]; omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (mk s (conv a) (conv b) (conv c) σ hdec hgas' hstk'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -672,6 +672,7 @@ private theorem logStep {yop : Op} {topicCount : Fin 5}
     {σ : List UInt256} {s : State}
     (hcode : code = mkCode (pre ++ (Instr.op (.Log ⟨topicCount⟩)).bytes ++ post))
     (hf : FrameOK code s) (hm : StateMatch yst s)
+    (hperm : s.executionEnv.permitStateMutation = true)
     (hpc : s.pc = UInt256.ofNat pre.length)
     (hstk : s.stack = (p :: n :: topics).map conv ++ σ)
     (hgas : opBound yop (p :: n :: topics) ≤ s.gasAvailable) :
@@ -696,8 +697,8 @@ private theorem logStep {yop : Op} {topicCount : Fin 5}
     le_trans hcost hgas
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.log s topicCount (conv p) (conv n) (topics.map conv) σ
-      hdec hf.perm (by simpa using htopics) hstk' hgas'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      hdec hperm (by simpa using htopics) hstk' hgas'),
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩, ?_, ?_, rfl, ?_⟩
   · constructor
     · exact hm.mem
@@ -740,6 +741,7 @@ theorem selfdestructStep {code : ByteArray} {pre post : List UInt8}
     {beneficiary : U256} {yst : EvmState} {σ : List UInt256} {s : State}
     (hcode : code = mkCode (pre ++ (Instr.op .SELFDESTRUCT).bytes ++ post))
     (hf : FrameOK code s) (hm : StateMatch yst s)
+    (hperm : s.executionEnv.permitStateMutation = true)
     (hpc : s.pc = UInt256.ofNat pre.length)
     (hstk : s.stack = [beneficiary].map conv ++ σ)
     (hgas : 40000 ≤ s.gasAvailable) :
@@ -766,13 +768,48 @@ theorem selfdestructStep {code : ByteArray} {pre post : List UInt8}
       hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩
   have hm' := hmGas.finishSelfdestruct beneficiary
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
-    (StepRunning.selfDestruct s (conv beneficiary) σ hdec hstk' hf.perm hgas'),
+    (StepRunning.selfDestruct s (conv beneficiary) σ hdec hstk' hperm hgas'),
     hm', ?_, ?_⟩
   · simpa [sGas, State.selfDestructTo] using hf.callStack
   · refine ⟨(.selfdestruct, []), ?_, ?_⟩
     · simp [YulSemantics.EVM.finishSelfdestruct]
     · simp [HaltMatch, State.selfDestructTo]
 
+/-- Package a target step that halts with `StaticModeViolation` (leaving all
+state fields untouched) into a `HaltStep` matching the source's
+`.staticViolation`. The source side only sets `halted` and the target gate
+halts before mutating, so the `StateMatch` carries over unchanged. -/
+theorem staticHaltStepGen {s : State} {yst : EvmState} (hm : StateMatch yst s)
+    (hcs : s.callStack = [])
+    (hstep : EVM.Step s { s with halt := .Exception .StaticModeViolation }) :
+    HaltStep s { yst with halted := some (.staticViolation, []) } :=
+  ⟨_, hstep,
+    ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
+      hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen,
+      hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩,
+    hcs, (.staticViolation, []), rfl, rfl⟩
+
+/-- A state-modifying built-in attempted in a static target frame
+(`permitStateMutation = false`) halts the frame with `StaticModeViolation`,
+matching the source's `.staticViolation`. Used by the local guarded ops
+(`sstore`/`tstore`/`log`/`selfdestruct`), all of which are `isStateMutating`
+and so fire the target's generic static gate. Neither side mutates world
+state: the source's `guardStatic` only sets `halted`, and the target gate
+halts before writing. -/
+theorem staticViolationStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
+    {code : ByteArray} {pre post : List UInt8} {s : State} {yst : EvmState}
+    (hcode : code = mkCode (pre ++ (Instr.op o).bytes ++ post))
+    (hf : FrameOK code s) (hm : StateMatch yst s)
+    (hpc : s.pc = UInt256.ofNat pre.length)
+    (hmut : o.isStateMutating = true)
+    (hperm : s.executionEnv.permitStateMutation = false) :
+    HaltStep s { yst with halted := some (.staticViolation, []) } := by
+  obtain ⟨hb, hplain⟩ := opTable_roundtrip hop
+  have hdec := decoded_op hf hcode hpc hb hplain (opTable_available hop)
+  exact staticHaltStepGen hm hf.callStack
+    (EVM.Step.running hf.running hf.noPrecompile
+      (StepRunning.staticModeViolation s o hdec hmut hperm))
+
 set_option maxHeartbeats 1600000 in
 open YulSemantics.EVM in
 /-- Executing the single compiled instruction of a supported built-in from a
@@ -793,11 +830,6 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
     | .halt yst' => HaltStep s yst' := by
   have hgas40 : 40000 ≤ s.gasAvailable := le_trans (le_opBound yop args) hgas
   have hfork : s.fork = .Osaka := hf.fork
-  have hstatic : yst.env.static = false := by
-    simpa [hf.perm] using hm.env.static
-  have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
-      YulSemantics.EVM.guardStatic yst act = some act := by
-    simp [YulSemantics.EVM.guardStatic, hstatic]
   -- common decode facts (only usable once `o` is concrete, but stated here
   -- for the bespoke cases)
   cases yop <;> simp only [opTable, Option.some.injEq, reduceCtorEq] at hop <;>
@@ -1068,7 +1100,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
         ≤ s.gasAvailable := by omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.exp s (conv a) (conv b) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -1110,7 +1142,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.keccak256 s (conv p) (conv n) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩,
@@ -1148,7 +1180,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.pop s (conv a) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1180,7 +1212,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.mload s (conv p) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -1219,7 +1251,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.mstore s (conv p) (conv v) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1262,7 +1294,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.mstore8 s (conv p) (conv v) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1314,7 +1346,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.mcopy s (conv d) (conv src) (conv n) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1363,7 +1395,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.calldataload s (conv p) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -1424,7 +1456,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.calldatacopy s (conv d) (conv s0) (conv nn) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1497,7 +1529,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
         (StepRunning.returndatacopy s (conv d) (conv s0) (conv nn) σ
           hdec hstk' hin hgas'),
-        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
           hf.running⟩,
         ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
           hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩,
@@ -1570,7 +1602,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       unfold Gas.codecopyTotal; rw [conv_toNat d, conv_toNat nn, h4]; omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.codecopy s (conv d) (conv s0) (conv nn) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1611,7 +1643,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       unfold Gas.codecopyTotal; rw [conv_toNat d, conv_toNat nn, h4]; omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.codecopy s (conv d) (conv s0) (conv nn) σ hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -1806,7 +1838,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       le_trans htotal hgas40
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.balance s (conv a) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -1848,7 +1880,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
         hm.externalCode.length a]
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.extcodesize s (conv a) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen,
@@ -1904,7 +1936,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.extcodecopy s (conv a) (conv d) (conv s0) (conv nn) σ
         hdec hstk' hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨?_, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, ?_, hm.retData, hm.retDataLen,
@@ -1955,7 +1987,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       le_trans htotal hgas40
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.extcodehash s (conv a) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen,
@@ -1992,7 +2024,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.blockhash s (conv n) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen,
@@ -2035,7 +2067,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       rw [hlookup] at hval
       refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
         (StepRunning.blobhash_oob s (conv i) σ hdec hgas' hstk' hlookup),
-        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
           hf.running⟩,
         ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
           hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -2056,7 +2088,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       rw [hlookup] at hval
       refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
         (StepRunning.blobhash s (conv i) σ h hdec hgas' hstk' hlookup),
-        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
           hf.running⟩,
         ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
           hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -2073,37 +2105,109 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
         have : Gas.baseCost s.fork .BLOBHASH ≤ 40000 := by rw [hfork]; decide
         omega
   case log0 =>
-    rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨extra, args⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    exact logStep (yop := .log0) (topicCount := 0) rfl rfl rfl
-      hcode hf hm hpc hstk hgas
+    cases hst : yst.env.static with
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨extra, args⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      exact logStep (yop := .log0) (topicCount := 0) rfl rfl rfl
+        hcode hf hm hperm hpc hstk hgas
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨extra, args⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .log0) rfl hcode hf hm hpc (by decide) hperm
   case log1 =>
-    rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨extra, args⟩⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    exact logStep (yop := .log1) (topicCount := 1) rfl rfl rfl
-      hcode hf hm hpc hstk hgas
+    cases hst : yst.env.static with
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨extra, args⟩⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      exact logStep (yop := .log1) (topicCount := 1) rfl rfl rfl
+        hcode hf hm hperm hpc hstk hgas
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨extra, args⟩⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .log1) rfl hcode hf hm hpc (by decide) hperm
   case log2 =>
-    rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨extra, args⟩⟩⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    exact logStep (yop := .log2) (topicCount := 2) rfl rfl rfl
-      hcode hf hm hpc hstk hgas
+    cases hst : yst.env.static with
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨extra, args⟩⟩⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      exact logStep (yop := .log2) (topicCount := 2) rfl rfl rfl
+        hcode hf hm hperm hpc hstk hgas
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨extra, args⟩⟩⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .log2) rfl hcode hf hm hpc (by decide) hperm
   case log3 =>
-    rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨t3,
-      _ | ⟨extra, args⟩⟩⟩⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    exact logStep (yop := .log3) (topicCount := 3) rfl rfl rfl
-      hcode hf hm hpc hstk hgas
+    cases hst : yst.env.static with
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨t3,
+        _ | ⟨extra, args⟩⟩⟩⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      exact logStep (yop := .log3) (topicCount := 3) rfl rfl rfl
+        hcode hf hm hperm hpc hstk hgas
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨t3,
+        _ | ⟨extra, args⟩⟩⟩⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .log3) rfl hcode hf hm hpc (by decide) hperm
   case log4 =>
-    rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨t3,
-      _ | ⟨t4, _ | ⟨extra, args⟩⟩⟩⟩⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    exact logStep (yop := .log4) (topicCount := 4) rfl rfl rfl
-      hcode hf hm hpc hstk hgas
+    cases hst : yst.env.static with
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨t3,
+        _ | ⟨t4, _ | ⟨extra, args⟩⟩⟩⟩⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      exact logStep (yop := .log4) (topicCount := 4) rfl rfl rfl
+        hcode hf hm hperm hpc hstk hgas
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨p, _ | ⟨n, _ | ⟨t1, _ | ⟨t2, _ | ⟨t3,
+        _ | ⟨t4, _ | ⟨extra, args⟩⟩⟩⟩⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .log4) rfl hcode hf hm hpc (by decide) hperm
   case sload =>
     rcases args with _ | ⟨k, _ | ⟨b, args⟩⟩ <;> simp [stepOp] at hyul
     subst hyul
@@ -2120,7 +2224,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.sload s (conv k) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -2140,98 +2244,112 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       unfold Gas.sloadTotal
       omega
   case sstore =>
-    rcases args with _ | ⟨k, _ | ⟨v, _ | ⟨c, args⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    show OkStep code s (opBound .sstore [k, v]) []
-      { yst with
-          storage := YulSemantics.EVM.upd yst.storage k v
-          env := { yst.env with storageOf :=
-            YulSemantics.EVM.updAccount yst.env.storageOf yst.env.address k v } }
-      pre.length 1 σ
-    obtain ⟨hb', hplain⟩ := opTable_roundtrip (yop := .sstore) rfl
-    have hdec := decoded_op hf hcode hpc hb' hplain
-      (opTable_available (yop := .sstore) rfl)
-    have hstk' : s.stack = conv k :: conv v :: σ := by simpa using hstk
-    have hsent : Gas.sstoreSentry s.fork
-        (s.gasAvailable - Gas.baseCost s.fork .SSTORE) = false := by
-      show Gas.sstoreSentry s.executionEnv.fork
-        (s.gasAvailable - Gas.baseCost s.executionEnv.fork Operation.SSTORE) = false
-      rw [hf.fork]
-      unfold Gas.sstoreSentry
-      rw [if_pos (by decide)]
-      apply decide_eq_false
-      have hb0 : Gas.baseCost Fork.Osaka Operation.SSTORE = 0 := by decide
-      omega
-    have hgas' : Gas.sstoreTotal s (conv k) (conv v) ≤ s.gasAvailable := by
-      unfold Gas.sstoreTotal
-      have h1 := sstoreCost_le s.executionEnv.fork
-        (s.substate.originalStorage s.executionEnv.address (conv k))
-        ((s.accountMap s.executionEnv.address).storage (conv k)) (conv v)
-      have h2 := sstoreCold_le s (conv k)
-      have hb0 : Gas.baseCost s.executionEnv.fork Operation.SSTORE = 0 := by
-        rw [hf.fork]; decide
-      omega
-    refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
-      (StepRunning.sstore s (conv k) (conv v) σ hdec hf.perm hstk' hsent hgas'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
-        hf.running⟩,
-      ?_, ?_, rfl, ?_⟩
-    · constructor
-      · exact hm.mem
-      · intro k'
-        show conv (YulSemantics.EVM.upd yst.storage k v k') = _
-        unfold YulSemantics.EVM.upd
-        rw [AccountMap.get_set_same]
-        by_cases hk : k' = k
-        · subst hk
-          rw [if_pos rfl]
-          exact (Storage.get_set_same _ _ _).symm
-        · rw [if_neg hk]
-          rw [Storage.get_set_other _ _ _ _ (by simpa [conv_inj] using hk)]
-          exact hm.stor k'
-      · intro k'
-        rw [AccountMap.get_set_same]
-        exact hm.tstor k'
-      · exact hm.cd
-      · exact hm.env.setStorageOf _
-      · exact hm.codeBytes
-      · exact hm.codeLen
-      · rw [AccountMap.get_set_same]
-        exact hm.selfBalance
-      · intro a
-        by_cases ha : AccountAddress.ofUInt256 (conv a) = s.executionEnv.address
-        · rw [ha, AccountMap.get_set_same]
-          have hba := hm.balanceOf a
-          rw [ha] at hba
-          simpa using hba
-        · rw [AccountMap.get_set_other _ _ _ _ ha]
-          exact hm.balanceOf a
-      · exact hm.activeWords
-      · exact hm.retData
-      · exact hm.retDataLen
-      · apply hm.externalCode.setStorage yst.env.address s.executionEnv.address k v
-        rw [hm.env.address]
-        exact accountAddress_ofUInt256_toUInt256 _
-      · exact hm.logs
-      · exact hm.selfdestructs
-      · exact hm.createdThisTx
-    · show s.pc.succ = _
-      rw [hpc]; apply succ_ofNat
-      have hsz : code.size = pre.length + 1 + post.length := by
-        subst hcode; simp [Instr.bytes]; omega
-      have := hf.codeSmall; omega
-    · show s.gasAvailable - Gas.sstoreTotal s (conv k) (conv v)
-        ≥ s.gasAvailable - opBound .sstore [k, v]
-      have h1 := sstoreCost_le s.executionEnv.fork
-        (s.substate.originalStorage s.executionEnv.address (conv k))
-        ((s.accountMap s.executionEnv.address).storage (conv k)) (conv v)
-      have h2 := sstoreCold_le s (conv k)
-      have h3 : opBound Op.sstore [k, v] = 40000 := rfl
-      have hb0 : Gas.baseCost s.executionEnv.fork Operation.SSTORE = 0 := by
-        rw [hf.fork]; decide
-      unfold Gas.sstoreTotal
-      omega
+    cases hst : yst.env.static with
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨k, _ | ⟨v, _ | ⟨c, args⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .sstore) rfl hcode hf hm hpc (by decide) hperm
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨k, _ | ⟨v, _ | ⟨c, args⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      show OkStep code s (opBound .sstore [k, v]) []
+        { yst with
+            storage := YulSemantics.EVM.upd yst.storage k v
+            env := { yst.env with storageOf :=
+              YulSemantics.EVM.updAccount yst.env.storageOf yst.env.address k v } }
+        pre.length 1 σ
+      obtain ⟨hb', hplain⟩ := opTable_roundtrip (yop := .sstore) rfl
+      have hdec := decoded_op hf hcode hpc hb' hplain
+        (opTable_available (yop := .sstore) rfl)
+      have hstk' : s.stack = conv k :: conv v :: σ := by simpa using hstk
+      have hsent : Gas.sstoreSentry s.fork
+          (s.gasAvailable - Gas.baseCost s.fork .SSTORE) = false := by
+        show Gas.sstoreSentry s.executionEnv.fork
+          (s.gasAvailable - Gas.baseCost s.executionEnv.fork Operation.SSTORE) = false
+        rw [hf.fork]
+        unfold Gas.sstoreSentry
+        rw [if_pos (by decide)]
+        apply decide_eq_false
+        have hb0 : Gas.baseCost Fork.Osaka Operation.SSTORE = 0 := by decide
+        omega
+      have hgas' : Gas.sstoreTotal s (conv k) (conv v) ≤ s.gasAvailable := by
+        unfold Gas.sstoreTotal
+        have h1 := sstoreCost_le s.executionEnv.fork
+          (s.substate.originalStorage s.executionEnv.address (conv k))
+          ((s.accountMap s.executionEnv.address).storage (conv k)) (conv v)
+        have h2 := sstoreCold_le s (conv k)
+        have hb0 : Gas.baseCost s.executionEnv.fork Operation.SSTORE = 0 := by
+          rw [hf.fork]; decide
+        omega
+      refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
+        (StepRunning.sstore s (conv k) (conv v) σ hdec hperm hstk' hsent hgas'),
+        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
+          hf.running⟩,
+        ?_, ?_, rfl, ?_⟩
+      · constructor
+        · exact hm.mem
+        · intro k'
+          show conv (YulSemantics.EVM.upd yst.storage k v k') = _
+          unfold YulSemantics.EVM.upd
+          rw [AccountMap.get_set_same]
+          by_cases hk : k' = k
+          · subst hk
+            rw [if_pos rfl]
+            exact (Storage.get_set_same _ _ _).symm
+          · rw [if_neg hk]
+            rw [Storage.get_set_other _ _ _ _ (by simpa [conv_inj] using hk)]
+            exact hm.stor k'
+        · intro k'
+          rw [AccountMap.get_set_same]
+          exact hm.tstor k'
+        · exact hm.cd
+        · exact hm.env.setStorageOf _
+        · exact hm.codeBytes
+        · exact hm.codeLen
+        · rw [AccountMap.get_set_same]
+          exact hm.selfBalance
+        · intro a
+          by_cases ha : AccountAddress.ofUInt256 (conv a) = s.executionEnv.address
+          · rw [ha, AccountMap.get_set_same]
+            have hba := hm.balanceOf a
+            rw [ha] at hba
+            simpa using hba
+          · rw [AccountMap.get_set_other _ _ _ _ ha]
+            exact hm.balanceOf a
+        · exact hm.activeWords
+        · exact hm.retData
+        · exact hm.retDataLen
+        · apply hm.externalCode.setStorage yst.env.address s.executionEnv.address k v
+          rw [hm.env.address]
+          exact accountAddress_ofUInt256_toUInt256 _
+        · exact hm.logs
+        · exact hm.selfdestructs
+        · exact hm.createdThisTx
+      · show s.pc.succ = _
+        rw [hpc]; apply succ_ofNat
+        have hsz : code.size = pre.length + 1 + post.length := by
+          subst hcode; simp [Instr.bytes]; omega
+        have := hf.codeSmall; omega
+      · show s.gasAvailable - Gas.sstoreTotal s (conv k) (conv v)
+          ≥ s.gasAvailable - opBound .sstore [k, v]
+        have h1 := sstoreCost_le s.executionEnv.fork
+          (s.substate.originalStorage s.executionEnv.address (conv k))
+          ((s.accountMap s.executionEnv.address).storage (conv k)) (conv v)
+        have h2 := sstoreCold_le s (conv k)
+        have h3 : opBound Op.sstore [k, v] = 40000 := rfl
+        have hb0 : Gas.baseCost s.executionEnv.fork Operation.SSTORE = 0 := by
+          rw [hf.fork]; decide
+        unfold Gas.sstoreTotal
+        omega
   case tload =>
     rcases args with _ | ⟨k, _ | ⟨b, args⟩⟩ <;> simp [stepOp] at hyul
     subst hyul
@@ -2246,7 +2364,7 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       omega
     refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
       (StepRunning.tload s (conv k) σ hdec hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
         hf.running⟩,
       ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, ?_, ?_⟩
@@ -2263,77 +2381,91 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
       have h3 : opBound Op.tload [k] = 40000 := rfl
       omega
   case tstore =>
-    rcases args with _ | ⟨k, _ | ⟨v, _ | ⟨c, args⟩⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    show OkStep code s (opBound .tstore [k, v]) []
-      { yst with
-          transient := YulSemantics.EVM.upd yst.transient k v
-          env := { yst.env with transientOf :=
-            YulSemantics.EVM.updAccount yst.env.transientOf yst.env.address k v } }
-      pre.length 1 σ
-    obtain ⟨hb', hplain⟩ := opTable_roundtrip (yop := .tstore) rfl
-    have hdec := decoded_op hf hcode hpc hb' hplain
-      (opTable_available (yop := .tstore) rfl)
-    have hstk' : s.stack = conv k :: conv v :: σ := by simpa using hstk
-    have hgas' : Gas.baseCost s.fork .TSTORE ≤ s.gasAvailable := by
-      rw [hfork]
-      have : Gas.baseCost .Osaka Operation.TSTORE ≤ 40000 := by decide
-      omega
-    refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
-      (StepRunning.tstore s (conv k) (conv v) σ hdec hf.perm hgas' hstk'),
-      ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
-        hf.running⟩,
-      ?_, ?_, rfl, ?_⟩
-    · constructor
-      · exact hm.mem
-      · intro k'
-        rw [AccountMap.get_set_same]
-        exact hm.stor k'
-      · intro k'
-        show conv (YulSemantics.EVM.upd yst.transient k v k') = _
-        unfold YulSemantics.EVM.upd
-        rw [AccountMap.get_set_same]
-        by_cases hk : k' = k
-        · subst hk
-          rw [if_pos rfl]
-          exact (Storage.get_set_same _ _ _).symm
-        · rw [if_neg hk]
-          rw [Storage.get_set_other _ _ _ _ (by simpa [conv_inj] using hk)]
-          exact hm.tstor k'
-      · exact hm.cd
-      · exact hm.env.setTransientOf _
-      · exact hm.codeBytes
-      · exact hm.codeLen
-      · rw [AccountMap.get_set_same]
-        exact hm.selfBalance
-      · intro a
-        by_cases ha : AccountAddress.ofUInt256 (conv a) = s.executionEnv.address
-        · rw [ha, AccountMap.get_set_same]
-          have hba := hm.balanceOf a
-          rw [ha] at hba
-          simpa using hba
-        · rw [AccountMap.get_set_other _ _ _ _ ha]
-          exact hm.balanceOf a
-      · exact hm.activeWords
-      · exact hm.retData
-      · exact hm.retDataLen
-      · apply hm.externalCode.setTransient yst.env.address s.executionEnv.address k v
-        rw [hm.env.address]
-        exact accountAddress_ofUInt256_toUInt256 _
-      · exact hm.logs
-      · exact hm.selfdestructs
-      · exact hm.createdThisTx
-    · show s.pc.succ = _
-      rw [hpc]; apply succ_ofNat
-      have hsz : code.size = pre.length + 1 + post.length := by
-        subst hcode; simp [Instr.bytes]; omega
-      have := hf.codeSmall; omega
-    · show s.gasAvailable - Gas.baseCost s.fork .TSTORE
-        ≥ s.gasAvailable - opBound .tstore [k, v]
-      have h1 : Gas.baseCost s.fork .TSTORE ≤ 100 := by rw [hfork]; decide
-      have h3 : opBound Op.tstore [k, v] = 40000 := rfl
-      omega
+    cases hst : yst.env.static with
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨k, _ | ⟨v, _ | ⟨c, args⟩⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .tstore) rfl hcode hf hm hpc (by decide) hperm
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨k, _ | ⟨v, _ | ⟨c, args⟩⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      show OkStep code s (opBound .tstore [k, v]) []
+        { yst with
+            transient := YulSemantics.EVM.upd yst.transient k v
+            env := { yst.env with transientOf :=
+              YulSemantics.EVM.updAccount yst.env.transientOf yst.env.address k v } }
+        pre.length 1 σ
+      obtain ⟨hb', hplain⟩ := opTable_roundtrip (yop := .tstore) rfl
+      have hdec := decoded_op hf hcode hpc hb' hplain
+        (opTable_available (yop := .tstore) rfl)
+      have hstk' : s.stack = conv k :: conv v :: σ := by simpa using hstk
+      have hgas' : Gas.baseCost s.fork .TSTORE ≤ s.gasAvailable := by
+        rw [hfork]
+        have : Gas.baseCost .Osaka Operation.TSTORE ≤ 40000 := by decide
+        omega
+      refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
+        (StepRunning.tstore s (conv k) (conv v) σ hdec hperm hgas' hstk'),
+        ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
+          hf.running⟩,
+        ?_, ?_, rfl, ?_⟩
+      · constructor
+        · exact hm.mem
+        · intro k'
+          rw [AccountMap.get_set_same]
+          exact hm.stor k'
+        · intro k'
+          show conv (YulSemantics.EVM.upd yst.transient k v k') = _
+          unfold YulSemantics.EVM.upd
+          rw [AccountMap.get_set_same]
+          by_cases hk : k' = k
+          · subst hk
+            rw [if_pos rfl]
+            exact (Storage.get_set_same _ _ _).symm
+          · rw [if_neg hk]
+            rw [Storage.get_set_other _ _ _ _ (by simpa [conv_inj] using hk)]
+            exact hm.tstor k'
+        · exact hm.cd
+        · exact hm.env.setTransientOf _
+        · exact hm.codeBytes
+        · exact hm.codeLen
+        · rw [AccountMap.get_set_same]
+          exact hm.selfBalance
+        · intro a
+          by_cases ha : AccountAddress.ofUInt256 (conv a) = s.executionEnv.address
+          · rw [ha, AccountMap.get_set_same]
+            have hba := hm.balanceOf a
+            rw [ha] at hba
+            simpa using hba
+          · rw [AccountMap.get_set_other _ _ _ _ ha]
+            exact hm.balanceOf a
+        · exact hm.activeWords
+        · exact hm.retData
+        · exact hm.retDataLen
+        · apply hm.externalCode.setTransient yst.env.address s.executionEnv.address k v
+          rw [hm.env.address]
+          exact accountAddress_ofUInt256_toUInt256 _
+        · exact hm.logs
+        · exact hm.selfdestructs
+        · exact hm.createdThisTx
+      · show s.pc.succ = _
+        rw [hpc]; apply succ_ofNat
+        have hsz : code.size = pre.length + 1 + post.length := by
+          subst hcode; simp [Instr.bytes]; omega
+        have := hf.codeSmall; omega
+      · show s.gasAvailable - Gas.baseCost s.fork .TSTORE
+          ≥ s.gasAvailable - opBound .tstore [k, v]
+        have h1 : Gas.baseCost s.fork .TSTORE ≤ 100 := by rw [hfork]; decide
+        have h3 : opBound Op.tstore [k, v] = 40000 := rfl
+        omega
   case call => simp [stepOp] at hyul
   case callcode => simp [stepOp] at hyul
   case delegatecall => simp [stepOp] at hyul
@@ -2341,10 +2473,25 @@ theorem opStep {yop : Op} {o : Operation} (hop : opTable yop = some o)
   case create => simp [stepOp] at hyul
   case create2 => simp [stepOp] at hyul
   case selfdestruct =>
-    rcases args with _ | ⟨beneficiary, _ | ⟨extra, args⟩⟩ <;>
-      simp [stepOp, hguard] at hyul
-    subst hyul
-    exact selfdestructStep hcode hf hm hpc hstk hgas40
+    cases hst : yst.env.static with
+    | true =>
+      have hperm : s.executionEnv.permitStateMutation = false :=
+        hm.perm_of_static_true hst
+      rcases args with _ | ⟨beneficiary, _ | ⟨extra, args⟩⟩ <;>
+        simp [stepOp, YulSemantics.EVM.guardStatic, hst] at hyul
+      subst hyul
+      exact staticViolationStep (yop := .selfdestruct) rfl hcode hf hm hpc
+        (by decide) hperm
+    | false =>
+      have hperm : s.executionEnv.permitStateMutation = true :=
+        hm.perm_of_static_false hst
+      have hguard (act : YulSemantics.BuiltinResult U256 EvmState) :
+          YulSemantics.EVM.guardStatic yst act = some act := by
+        simp [YulSemantics.EVM.guardStatic, hst]
+      rcases args with _ | ⟨beneficiary, _ | ⟨extra, args⟩⟩ <;>
+        simp [stepOp, hguard] at hyul
+      subst hyul
+      exact selfdestructStep hcode hf hm hperm hpc hstk hgas40
   case stop =>
     rcases args with _ | ⟨a, args⟩ <;> simp [stepOp] at hyul
     subst hyul
@@ -2436,7 +2583,7 @@ theorem jumpdestStep {code : ByteArray} {pre post : List UInt8}
     omega
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.jumpdest s hdec hgas'),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -2473,7 +2620,7 @@ theorem jumpStep {code : ByteArray} {pre post : List UInt8}
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.jump s dest rest hdec hgas' hstk
       (by rw [hf.hcode]; exact hvalid)),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, rfl, rfl, ?_⟩
@@ -2504,7 +2651,7 @@ theorem jumpiNotTakenStep {code : ByteArray} {pre post : List UInt8}
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.jumpi_notTaken s dest cond rest hdec hgas' hstk
       (by simp [UInt256.isTrue, hcond])),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, ?_, rfl, ?_⟩
@@ -2542,7 +2689,7 @@ theorem jumpiTakenStep {code : ByteArray} {pre post : List UInt8}
   refine ⟨_, EVM.Step.running hf.running hf.noPrecompile
     (StepRunning.jumpi_taken s dest cond rest hdec hgas' hstk hcond
       (by rw [hf.hcode]; exact hvalid)),
-    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.perm, hf.noPrecompile, hf.callStack,
+    ⟨hf.hcode, hf.codeSmall, hf.fork, hf.noPrecompile, hf.callStack,
       hf.running⟩,
     ⟨hm.mem, hm.stor, hm.tstor, hm.cd, hm.env, hm.codeBytes, hm.codeLen,
         hm.selfBalance, hm.balanceOf, hm.activeWords, hm.retData, hm.retDataLen, hm.externalCode, hm.logs, hm.selfdestructs, hm.createdThisTx⟩, rfl, rfl, ?_⟩
diff --git a/YulEvmCompiler/StateRel.lean b/YulEvmCompiler/StateRel.lean
index 4e5cd870..6fc67d12 100644
--- a/YulEvmCompiler/StateRel.lean
+++ b/YulEvmCompiler/StateRel.lean
@@ -1030,6 +1030,25 @@ structure StateMatch (yst : YulSemantics.EVM.EvmState) (s : EVM.State) : Prop wh
   createdThisTx : yst.env.createdThisTx =
     !(s.substate.originalAccountMap s.executionEnv.address).isContract
 
+/-- The target frame's mutation permission is the negation of the source
+static flag (a direct consequence of `EnvMatch.static`). -/
+theorem StateMatch.permitStateMutation_eq
+    {yst : YulSemantics.EVM.EvmState} {s : EVM.State} (hm : StateMatch yst s) :
+    s.executionEnv.permitStateMutation = !yst.env.static := by
+  rw [hm.env.static, Bool.not_not]
+
+/-- A non-static source frame corresponds to a mutation-permitting target frame. -/
+theorem StateMatch.perm_of_static_false
+    {yst : YulSemantics.EVM.EvmState} {s : EVM.State} (hm : StateMatch yst s)
+    (h : yst.env.static = false) : s.executionEnv.permitStateMutation = true := by
+  simp [hm.permitStateMutation_eq, h]
+
+/-- A static source frame corresponds to a mutation-forbidding target frame. -/
+theorem StateMatch.perm_of_static_true
+    {yst : YulSemantics.EVM.EvmState} {s : EVM.State} (hm : StateMatch yst s)
+    (h : yst.env.static = true) : s.executionEnv.permitStateMutation = false := by
+  simp [hm.permitStateMutation_eq, h]
+
 /-- Lift the balance/account-map facts specific to one `SELFDESTRUCT` branch into the complete
 machine-state correspondence. -/
 theorem StateMatch.finishSelfdestruct_of
@@ -1225,7 +1244,6 @@ structure FrameOK (code : ByteArray) (s : EVM.State) : Prop where
   /-- Positions in the code fit in a word, so `pc` arithmetic never wraps. -/
   codeSmall : code.size < 2 ^ 256
   fork : s.executionEnv.fork = .Osaka
-  perm : s.executionEnv.permitStateMutation = true
   noPrecompile : Precompile.isPrecompile s.executionEnv.fork s.executionEnv.codeAddr
     = false
   callStack : s.callStack = []
@@ -1240,6 +1258,7 @@ def HaltMatch (hk : YulSemantics.EVM.HaltKind × List UInt8) (s : EVM.State) : P
   | .revert  => s.halt = .Reverted ∧ s.hReturn.toList = hk.2
   | .invalid => s.halt = .Exception .InvalidInstruction
   | .invalidMemoryAccess => s.halt = .Exception .InvalidMemoryAccess
+  | .staticViolation => s.halt = .Exception .StaticModeViolation
   | .selfdestruct => s.halt = .Success ∧ s.hReturn = .empty
 
 /-- The `ExecutionResult` a yul-semantics halt corresponds to. -/
@@ -1250,6 +1269,7 @@ def resultOf (hk : YulSemantics.EVM.HaltKind × List UInt8) : ExecutionResult :=
   | .revert  => .reverted (mkCode hk.2)
   | .invalid => .exception .InvalidInstruction
   | .invalidMemoryAccess => .exception .InvalidMemoryAccess
+  | .staticViolation => .exception .StaticModeViolation
   | .selfdestruct => .success
 
 end YulEvmCompiler
diff --git a/lake-manifest.json b/lake-manifest.json
index 3e6e363a..d0280d40 100644
--- a/lake-manifest.json
+++ b/lake-manifest.json
@@ -15,10 +15,10 @@
    "type": "git",
    "subDir": null,
    "scope": "",
-   "rev": "5cfcdc8ea4ad891a8d669852fafe4bbb1e5ac506",
+   "rev": "0b1a2c0f981ce64c6dc262d7afe0756571e91b63",
    "name": "«yul-semantics»",
    "manifestFile": "lake-manifest.json",
-   "inputRev": "5cfcdc8ea4ad891a8d669852fafe4bbb1e5ac506",
+   "inputRev": "0b1a2c0f981ce64c6dc262d7afe0756571e91b63",
    "inherited": false,
    "configFile": "lakefile.toml"},
   {"url": "https://github.com/leanprover-community/mathlib4.git",
diff --git a/lakefile.toml b/lakefile.toml
index 2a81f6c4..932a4a23 100644
--- a/lakefile.toml
+++ b/lakefile.toml
@@ -6,7 +6,7 @@ defaultTargets = ["YulEvmCompiler", "YulParser", "YulEvmCompilerTests"]
 [[require]]
 name = "yul-semantics"
 git = "https://github.com/powdr-labs/yul-semantics"
-rev = "5cfcdc8ea4ad891a8d669852fafe4bbb1e5ac506"
+rev = "0b1a2c0f981ce64c6dc262d7afe0756571e91b63"
 
 # Target-language semantics: the EVM small-step/big-step relations.
 [[require]]