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.