rocq/backend/Nfb.v
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 subset 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.
A module as its term
As ir.pl writes a data object's Linkage.
As ir.pl writes a data item; a string's bytes as the term reader makes their characters.
As ir.pl writes a function's Ret.
As ir.pl writes a function.
As ir.pl writes an item; a function outside the core subset is its term.
The module as the term module(Items).
Words
The NFB of the module m, with its NAMES section when names is true; none for a module that has no encoding, such as one whose symbol is not an atom.
The NFB of the module m, NAMES included.
The module the NFB ws encode: the words must be what encode_with writes for it, NAMES if ws have it, CONTEXT and tools' sections aside.
The module the NFB ws encode, for a consumer that needs the module and not the words' identity, such as the backend: the reader, then decode_module, without decode's check that ws are the words encode_with writes for it. The round trip and totality hold for it as for decode (NfbProof.v, input_round_trip); only the canonical theorem needs the check, which costs as much again as the reading.