# State-shortcut-laws


fx.experimental.desc-interp.effects.state-shortcut-laws: kernel-checked one-shot lemmas for handle_State on each canonical EffState op (get/put/modify). Each lemma discharges by `H.refl` — kernel conv decides reduction universally via ι on EffState.elim + Resp_State. Lemma RHSes match the `extract.Resume` emitter output, anchoring the shortcut path's soundness at the kernel layer.

## `getLemma`

_Proof of get-lemma: 3 lams + H.refl. Reduction at canonical `get` is by ι on `EffState.elim` plus β on the onGet branch; `Resp_State S (get S) ≡ S` by ι makes the resume payload `s` well-typed._

## `getLemmaTy`

_Π-type of get-lemma: `Π S A. Π s:S. handle_State S A (get S) s ≡ mkResumeAt S Op Resp (get S) A s s`._

## `modifyLemma`

_Proof of modify-lemma: 4 lams + H.refl. `Resp_State S (modify S fn) ≡ Unit` by ι; new state := `fn s`._

## `modifyLemmaTy`

_Π-type of modify-lemma: `Π S A. Π fn:S→S. Π s:S. handle_State S A (modify S fn) s ≡ mkResumeAt S Op Resp (modify S fn) A tt (fn s)`._

## `putLemma`

_Proof of put-lemma: 4 lams + H.refl. `Resp_State S (put S param) ≡ Unit` by ι; the prior state `s` is discarded and resume carries new state `param`._

## `putLemmaTy`

_Π-type of put-lemma: `Π S A. Π param s:S. handle_State S A (put S param) s ≡ mkResumeAt S Op Resp (put S param) A tt param`._