Cryptol-to-Hyle translation: the engine behind rwc's Cryptol foreign-function interface. translate loads and typechecks a Cryptol module (with the Cryptol implementation itself -- the typechecker needs z3 on the PATH), elaborates the instantiation fn : ty (so Cryptol's own typechecker decides whether the use-site type is admissible), monomorphizes it with Cryptol's specializer, and translates the resulting closure of monomorphic definitions to Hyle.

The translation is the inverse of the width-preserving embedding the Cryptol backend uses (doc/hyle.md, section 8.4): a Cryptol word [n] is a Hyle bitvector of the same numeric value, sequence and tuple element zero sits at the most-significant end, and Bit is one bit. Cryptol's specializer erases the type arguments of primitive instances (a literal's value, an index operator's dimensions), so specialization runs through its lower-level S.withDeclGroups interface, whose name map recovers each primitive clone's instantiation types.

Supported fragment: combinational functions over Bit, words, vectors, tuples, records, newtypes, enums (case expressions), and Z n (modular arithmetic). if-then-else; local value and function bindings; higher-order functions applied to statically known functions; comprehensions, folds, and scans (unrolled); recursive finite comprehensions (the message-schedule/key-schedule/CBC idiom, unrolled element-wise); type-indexed recursion (unrolled per instantiation); infinite streams under statically bounded demand (a finite take or a constant index; see infPrefix); the scalar, slicing, sequence, indexing, rotate, update, and polynomial (pmult/pdiv/pmod, constant divisor) primitives. Records, enums, and Z n are interior-only: the entry point's type must be words/vectors/tuples (the rwc side has no counterpart). Enum values are laid out tag#pad#args with the tag at the most-significant end and the tag width nbits(#constructors) -- the same convention the Eidos fold uses for ReWire ADTs. error/undefined become a zero poison constant and trace the identity, both with warnings. Value recursion, unbounded-demand infinite streams, floating point, and Integer/Rational at runtime are rejected with (it is hoped) actionable messages.