The Cryptol backend on Hyle: the width-preserving embedding of doc/hyle.md, section 8.4. Every Hyle defn becomes a Cryptol function over bitvectors; the device becomes a step function rw_step (registers and inputs to outputs and next-register values, as one concatenated vector) wrapped in the standard Mealy stream idiom rw_device, matching the Hyle interpreter bit for bit.

Because Hyle widths are explicit and exact, no width reconstruction happens here: slices flip to Cryptol's MSB-first order, division gets the SMT-LIB division-by-zero guard (doc/hyle.md, section 5.2), and coercions and reductions map to small fixed helpers; everything else is a per-construct template.

Combinational externs without models become uninterpreted functions in a parameter block (generic arguments become leading 32-bit arguments); externs with models become ordinary calls to the model's function. Devices with instances (sequential externs) are rejected: a pure target has no equivalent.