NFB (docs/nfb.md) for the modules of Syntax.v: encode writes a module's words and decode reads them back, in place of the term the Prolog compiler prints and Transport.v's decode_module reads.

A module of Syntax.v is written as the term ir.pl would print for it (enc_module, from IrTerm.v's encoders of instructions), and that term as words by NfbTerm.v. A function outside the core subsetcore subset nanofilThe core subset is the part of checked filc-mode IR that the Rocq model runs and validates: the integer, pointer and proof classes, floats, check and every reuse form, the raw accesses, flight, poll edges, direct calls, check_function with raw_call, free, named locals and variadics. A function that uses anything else decodes to IOutside. is already its term (IOutside), so it is written the same way. Reading is the converse: NfbTerm.v's reader gives the module term, decode_module the module, and the words are taken only if they are what encode writes for that module.