# Extract


## Soundness layering

- **kernel-side (HOAS)**: per-canonical-op lemma
  `handle_X op s ≡_kernel mkResumeAt … r s` proved by `H.refl`
  + ι (mirrors `compose-laws.nix`).
- **emitter-side (Val)**: per-primitive conv test
  `eval (HOAS witness) ≡_Val extract (Primitive …)` shown via
  `fx.tc.conv.conv 0`. Sugar tests are consequences of the
  primitive tests + composition.
- **chain**: kernel-path Val ≡ shortcut-path Val at every
  canonical op.

## Algebra

- **Primitives** — `DescCon`, `BootInl`, `BootInr`, `Pair`,
  `Tt`, `BootRefl`. One-to-one mirrors of `V.vDescCon` /
  `vBootInl` / `vBootInr` / `vPair` / `vTt` / `vBootRefl`.
- **Sugars** — `Resume`, `Abort`, `PairRaw`. Folded shapes
  rewriting into nested primitive RF trees; no capability
  beyond the primitives.
- **Consumers** — `Project`, `OfElim`. Read a Val (or RF, via
  polymorphic `extract`) back into a Val; used by composed
  shortcuts.

Caller supplies `sumDescVal` / `leftSig` / `rightSig` once per
`atType` instance. `sumDescValOf leftSig rightSig` recovers
the VDescCon `.D` slot from a HOAS sum type by evaluating a
canonical `H.inl` skeleton.

## `Abort`

_Abort sumDescVal leftSig rightSig value state — UniRet right summand sugar. Folds to `DescCon sumDescVal Tt (BootInr leftSig rightSig (Pair (Pair value state) BootRefl))`. Used by error-strict (surrender), error-result (Sum-typed channel), and composed abort paths._

## `BootInl`

_BootInl left right val — primitive mirror of `V.vBootInl left right val`. Left-summand selector inside a `DescCon` for a plus-of-args description._

## `BootInr`

_BootInr left right val — primitive mirror of `V.vBootInr left right val`. Right-summand counterpart of `BootInl`._

## `BootRefl`

_BootRefl — primitive mirror of `V.vBootRefl`. Structural marker for the `ret` slot of descArg._

## `DescCon`

_DescCon D i d — primitive mirror of `V.vDescCon D i d`. `D` is a descriptor Val, `i` the index Val, `d` the constructor payload._

## `OfElim`

_OfElim scrutinee onResume onAbort — Val-side pattern match on a UniRet-shaped scrutinee. `onResume`/`onAbort` are Nix `Val → Val` functions receiving the bootInl/bootInr payload (a `(payload, state)` VPair). Used by composed shortcuts to dispatch on inner sub-handler results._

## `Pair`

_Pair fst_ snd_ — primitive mirror of `V.vPair fst snd`._

## `PairRaw`

_PairRaw fst_ snd_ — alias for `Pair`. Documents intent as a bare `H.pair _ _` residual (as opposed to UniRet-inner pair). Used by error's three strategies whose reduced RHS isn't UniRet-wrapped._

## `Project`

_Project side of_ — first or second projection of a VPair-typed Val. `side ∈ {"fst","snd"}`. Used by composed-shortcut state-slot repack._

## `Resume`

_Resume sumDescVal leftSig rightSig resp state — UniRet left summand sugar. Folds to `DescCon sumDescVal Tt (BootInl leftSig rightSig (Pair (Pair resp state) BootRefl))`. Mirrors `eval (mkResumeAt S Op Resp op A resp state)`._

## `Tt`

_Tt — primitive mirror of `V.vTt`. Unit Val constant._

## `extract`

_extract : ResidualForm → Val. Direct attrset construction targeting the VDescCon/VBootInl|VBootInr/VPair encoding produced by `eval` on the canonical mkResumeAt / mkAbortAt / fst_ / snd_ / sumElim spines. Per-constructor conv tests under `_self.tests` discharge emitter-side soundness._

## `sumDescValOf`

_sumDescValOf leftSigHoas rightSigHoas — recovers the VDescCon `.D` slot for a `H.sum leftSig rightSig` instantiation by evaluating a canonical `H.inl` skeleton and reading its `.D`. Caller-side helper for building `Resume`/`Abort` metadata Vals once per `atType` instance._