rocq/backend/NfbTransport.v
The term half of NFB's round trip (docs/nfb.md): a module that Transport.v's decode_module reads from any term is read back from the term Nfb.v's enc_module writes for it (decode_enc_module), and no item of that term is a context item (enc_module_no_context).
Most of the syntax is canonical: for every decoder of Transport.v but the data item's, what it reads from a term t is written back by its encoder as t itself (dinst_enc, dblock_enc, dfunc_enc and the others below). So enc_modulem would be t with its context items dropped, except for one construct: a string item whose character is an overlong two-byte UTF-8 atom, such as the atom of the bytes 0xC0 0x80. char_code reads it as the code 0, which code_char writes back as the one-byte atom. Then enc_modulem is not the term m was read from (strong_form_fails). The term is still read back as the same module, because char_code reads every code code_char writes (char_code_code_char), and that is all decode_enc_module needs.
Taking a decoder apart
Turn a fact E, that a decoder read a term, into the term itself, using one of the earlier lemmas in the context.
Split the hypothesis H on what blocks its match x: a variable, a string comparison, a list length, or a decoder's result.
One step of reading back a hypothesis H that a decoder gave Some: refute it, take apart what blocks it, or take its value.
Close a goal that the encoding is the term, rewriting with what the encoders of the parts gave back.
The head normal form of e.
Destruct the variable that blocks the match r, looking through the head of each scrutinee in turn.
Values and the small tables
An integer is read from the term TIntn only.
A class is read from its own atom only.
A temporary n is read from tmp(N) only.
A value is read from the term enc_value writes for it only.
Rights are read from their own atom only.
A bound is read from its own atom only.
A narrow type is read from its own atom only.
A load type is read from its own atom only.
Proof 5 steps Qed
A condition is read from its own atom only.
An effect is read from its own atom only.
A width is read from its own atom only.
If e writes back every term d reads, it writes back every list of terms that map_option d reads.
Proof 9 steps Qed
A list of effects is read from the list of their atoms only.
Proof 5 steps Qed
An op is read from the term enc_op writes for it only.
Proof 12 steps Qed
Instructions
A flight's argument is read from its own term only.
Proof 4 steps Qed
A flight's Lower is read from its own term only.
Proof 5 steps Qed
One result of a call is read from result(tmp(D), K) only.
Proof 6 steps Qed
A call's Res is read from its own term only.
Proof 6 steps Qed
A call's argument is read from arg(K, V) only.
Proof 6 steps Qed
A call's arguments are read from the list of their terms only.
Proof 5 steps Qed
An instruction is read from the term enc_inst writes for it only.
Proof 16 steps Qed
Jumps, phis, blocks and functions
A jump's target is read from its own term only.
A jump is read from the term enc_jump writes for it only.
Proof 7 steps Qed
One pair of a phi is read from Pred − Value only.
Proof 5 steps Qed
A phi is read from the term enc_phi writes for it only.
Proof 7 steps Qed
A block is read from the term enc_block writes for it only.
Proof 7 steps Qed
A function's Ret is read from its own term only.
Proof 6 steps Qed
A function's parameter is read from param(K, tmp(D)) only.
Proof 6 steps Qed
A function read from the arguments of a func term is written back as that term.
Proof 7 steps Qed
A data object's Linkage is read from its own term only.
Proof 4 steps Qed
Data
char_code reads only the codes 0 to 2047.
Proof 13 steps Qed
Proof 23 steps Qed
The codes of a string item are all from 0 to 2047.
Proof 7 steps Qed
Codes from 0 to 2047 are read back from the atoms code_char writes for them.
Proof 6 steps Qed
What is known of a data item x read from the term t: it is written back as t, or it is a string of codes from 0 to 2047.
Close a goal data_okt x.
A data item read from t is written back as t, or is a string of codes from 0 to 2047. The item's subterms on its second argument are taken apart once each, then stand for themselves, so that its first argument and its second are not taken apart together.
Proof 8 steps Qed
A data item read from any term is read back from the term enc_data_item writes for it.
Proof 7 steps Qed
If d reads back from e's term whatever it read from some term, the same holds of lists by map_option.
Proof 11 steps Qed
Items and the module
An item read from t is written back as t, unless it is a data object: then t is its data term, with its Linkage and items as read.
Proof 5 steps Qed
An item read from any term is read back from the term enc_item writes for it.
Proof 9 steps Qed
The items a module keeps of what ditem read: none for a context item.
Proof 11 steps Qed
Keeping every item of a list of items read as items gives the list.
Proof 1 step Qed
Every item of a module read from any term is read back, as that item, from the term enc_item writes for it.
Proof 6 steps Qed
The term half of NFB's round trip: a module read from any term is read back from the term enc_module writes for it.
Proof 8 steps Qed
Context items
Whether the term is not a context(_, _) item.
A term that ditem reads as an item is not a context item.
Proof 7 steps Qed
No item of the term enc_module writes for a module read from any term is a context item.
Proof 13 steps Qed
The strong form fails
The term t with its context items dropped, if it is a module.
A module of one data object whose string is the overlong UTF-8 sequence 0xC0 0x80, an atom of two characters.
overlong is read as the string of the one code 0, which is written back as a one-byte atom.
Proof 1 step Qed
So enc_modulem is not always the term m was read from with its context items dropped.