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.