rocq/backend/NfbProof.v
What NFB's Gallina reader and writer (NfbTerm.v, Nfb.v) are proved to do (docs/nfb.md, Relation to the term form and the Rocq model).
- Canonical: the words
decodetakes are the wordsencode_withwrites for the module it gives, CONTEXT and tools' sections aside (decode_canonical). So two lists of words that decode to one module, with NAMES in both or in neither, are the same words (decode_identity): the words are the module's identity. - Round trip: a module that Transport.v's
decode_modulegives is read back from its words as itself (round_trip). Its two halves are that the term reader gives back what the term writer wrote (NfbRead.v,read_encode_term) and thatdecode_modulereadsenc_modulemas m (NfbTransport.v,decode_enc_module).
Canonical form
Whether the reader finds a NAMES section in ws.
The words decode takes are exactly the words encode_with writes for the module it gives, with NAMES if they have it: no other spelling of a module is read.
Proof 12 steps Qed
Two lists of words that decode reads as the same module, both with NAMES or both without, are the same words once CONTEXT and tools' sections are set aside: the module id the document defines over them is sound.
Proof 3 steps Qed
Round trip
A list of words is equal to itself by words_eqb.
Proof 3 steps Qed
A module that decode_module reads from a term, once written as words, is read back as itself, NAMES included.
Proof 10 steps Qed
decode_input, the reader without decode's check, reads a module back as itself too.