The Synolon-to-Hyle producer (the direct fold; doc/synolon.md §7): the pure fragment translates per-construct (n-ary cases compile to if-chains over constructor tags; joins are lifted to definitions first), and each process folds to an explicit device: one definition per block (cells threaded as trailing parameters), one dispatch definition (an if-chain over the label tag), and register initials obtained by evaluating the entry block with the Hyle interpreter.

The machine-step record reproduces the retired purifier's bit layout exactly (so interpreter traces are unchanged): a step is halted | out | label-tag | pad | args | cells, where the halted bit is present only when a halt is reachable (the successor of the PuRe constructor tag), the label field mirrors the generic ADT layout of the retired R_ datatype (tag at the field's MSB, arguments LSB-aligned), and a halt step carries the retired A_ encoding (one tag per distinct answer type) in place of out | label.