# Composed-shortcut


Pipeline per Impure step on a composed op: read `op._side` /
`op._inner`, project the composed state with `extract.Project`,
recurse via the matching per-side shortcut, then `extract.OfElim`
on the sub-UniRet — Resume → composed Resume; Abort → composed
Abort — repacking the sibling state slot via `extract.PairRaw`.

Soundness: kernel-side `composedHandlerShortcutLemma`
(`composed-shortcut-laws.nix`) chains `composeHandlersInl/InrLemma`
with per-effect uniform-shortcut lemmas; emitter-side, the
`_self.tests` below conv-check kernel-composed vs shortcut-emitted
Vals at concrete canonical ops.

## `composedHandlerShortcut`

_composedHandlerShortcut H_short_A H_short_B metaFor op stateVal — composed UniRet Val mirroring `eval (composeHandlers … H_A H_B opVal stateVal)`. `op` carries `_side`/`_inner` sidecars from `composedInl`/`composedInr`; `metaFor` is the composed-UniRet metadata lookup keyed by inner-op tag; per-side shortcuts must return UniRet Vals. `null` propagates from any of the inputs (kernel fallback)._

## `composedInl`

_composedInl Op_A Op_B subOp — `H.inl Op_A Op_B subOp` with `_side = "composed-inl"`, `_inner = subOp`. Sidecars are ignored by elab and survive `K.send`'s `impureCon` wrap._

## `composedInr`

_composedInr Op_A Op_B subOp — `H.inr` counterpart of `composedInl`._

## `mkComposedMeta`

_mkComposedMeta { SigmaSHoas; A; respHoas; } — precompute `{ sumDescVal; leftSigVal; rightSigVal; }` for the composed UniRet at one canonical inner op (response type already ι-reduced)._