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 decode takes are the words encode_with writes 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: toward decodeencodem = Somem, the words of each kind of field read back as what was written: a signed 64-bit or 96-bit integer (i64_round_trip, wide_round_trip), an inline constant (inline_round_trip), and an enumeration's code (codes_round_trip).

From Stdlib Require Import String ZArith List Bool Lia

From Nanofil Require Import Term Syntax Transport Cfg

From Backend Require Import NfbTerm Nfb

Import ListNotations

Open Scope Z_scope

Canonical form

words_eqb is equality of word lists.

24Lemma words_eqb_eq

∀ xs ys

words_eqbxs ys = true

xs = ys

Proof 6 steps Qed

induction xs as | x xs IH ; intros | y ys H ; simpl in H ; try discriminate ; auto

apply andb_true_iff in H as H₁ H₂

apply Z.eqb_eq in H1

subst

f_equal

auto

Whether the reader finds a NAMES section in ws.

31Definition names_ofws : listZ : bool ≔

match read_termws with

Some_, b

⇒

None

⇒

false

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.

37Theorem decode_canonical

∀ ws m

decodews = Somem

encode_withnames_ofws m = module_wordsws

Proof 12 steps Qed

intros ws m H

unfold decode , names_of in *

destruct read_termws as t b | ; try discriminate

simpl in H

destruct decode_modulet as m₀ | ; try discriminate

destruct encode_withb m0 as ws₁ | eqn: E1 ; try discriminate

destruct module_wordsws as ws₂ | ; try discriminate

destruct words_eqbws1 ws2 eqn: E3 ; try discriminate

injection H as ←

apply words_eqb_eq in E3

subst

exact E1

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.

53Corollary decode_identity

∀ ws₁ ws₂ m

decodews₁ = Somem

decodews₂ = Somem

names_ofws₁ = names_ofws₂

module_wordsws₁ = module_wordsws₂

Proof 3 steps Qed

intros ws₁ ws₂ m H₁ H₂ E

rewrite <- decode_canonical_ _ H1 , <- decode_canonical_ _ H2 , E

reflexivity

Words read back

A signed 64-bit integer, written as two words, reads back.

64Lemma i64_round_trip

∀ n

i64okn = true

match i64_wordsn with

lo; hi

⇒

i64_oflo hi = n

⇒

False

Proof 18 steps Qed

intros n H

unfold i64ok in H

apply andb_true_iff in H as H₁ H₂

apply Z.leb_le in H1

apply Z.ltb_lt in H2

unfold i64_words , i64_of , two32 , two64 in *

change 18446744073709551616 / 2 with 9223372036854775808 in *

set u := n mod 18446744073709551616

assert Hu : u mod 4294967296 + u / 4294967296 × 4294967296 = u

{pose proof Z.div_modu 4294967296

lia

rewrite Hu

subst u

destruct Z_lt_le_decn 0 as Hn | Hn

–rewrite <- Z.mod_uniquen 18446744073709551616 −1 n + 18446744073709551616 by lia

destruct Z.ltb_specn + 18446744073709551616 9223372036854775808 ; lia

–rewrite Z.mod_small by lia

destruct Z.ltb_specn 9223372036854775808 ; lia

A signed 96-bit integer, written as three words, reads back.

83Lemma wide_round_trip

∀ n

wideokn = true

match wide_wordsn with

w₀; w₁; w₂

⇒

wide_ofw₀ w₁ w₂ = n

⇒

False

Proof 22 steps Qed

intros n H

unfold wideok in H

apply andb_true_iff in H as H₁ H₂

apply Z.leb_le in H1

apply Z.ltb_lt in H2

unfold wide_words , wide_of , two32 , two64 , two96 in *

change 79228162514264337593543950336 / 2 with 39614081257132168796771975168 in *

set u := n mod 79228162514264337593543950336

assert Hr : 0 ≤ u < 79228162514264337593543950336 by apply Z.mod_pos_bound ; lia

assert Hu : u mod 4294967296 + u / 4294967296 mod 4294967296 × 4294967296 + u / 18446744073709551616 × 18446744073709551616 = u

{pose proof Z.div_modu 4294967296 ltac:lia

pose proof Z.div_modu / 4294967296 4294967296 ltac:lia

rewrite Z.div_div in * by lia

change 4294967296 × 4294967296 with 18446744073709551616 in *

lia

rewrite Hu

subst u

destruct Z_lt_le_decn 0 as Hn | Hn

–rewrite <- Z.mod_uniquen 79228162514264337593543950336 −1 n + 79228162514264337593543950336 by lia

destruct Z.ltb_specn + 79228162514264337593543950336 39614081257132168796771975168 ; lia

–rewrite Z.mod_small by lia

destruct Z.ltb_specn 39614081257132168796771975168 ; lia

An inline constant's operand word reads back as the constant, whatever the tables: tag 1, the constant in the payload.

110Lemma inline_round_trip

∀ r c n

inlinen = true

∃z, const_wordc n = Somez ∧ const_ofr z = Somen

Proof 22 steps Qed

intros r c n H

unfold const_word

rewrite H

eexists

split ; reflexivity |

unfold inline , inline_bound in H

apply andb_true_iff in H as H₁ H₂

apply Z.leb_le in H1

apply Z.ltb_lt in H2

unfold const_of , inline_bound

set p := n mod 2 × 536870912

assert Hp : 0 ≤ p < 2 × 536870912 by apply Z.mod_pos_bound ; lia

replace p × 4 + 1 mod 4 with 1 by rewrite Z.add_comm , Z.mod_add ; reflexivity || lia

replace p × 4 + 1 / 4 with p by rewrite Z.add_comm , Z.div_add by lia ; reflexivity

simpl

f_equal

subst p

destruct Z_lt_le_decn 0 as Hn | Hn

–rewrite <- Z.mod_uniquen 2 × 536870912 −1 n + 2 × 536870912 by lia

destruct Z.ltb_specn + 2 × 536870912 536870912 ; lia

–rewrite Z.mod_small by lia

destruct Z.ltb_specn 536870912 ; lia

Whether each key and each value of the table xs occurs once.

129Definition table_okxs : liststring × Z : Prop ≔

NoDupmapfst xs ∧ NoDupmapsnd xs

A table whose keys and values each occur once gives back the key of the value of a key.

134Lemma assoc_round_trip

∀ xs s z

table_okxs

sassocs xs = Somez

srassocz xs = Somes

Proof 13 steps Qed

induction xs as | k v xs IH ; intros s z Hk Hv H ; simpl in * ; try discriminate

inversion Hk as [ |? ? Hk1 Hk2 ] ; inversion Hv as [ |? ? Hv1 Hv2 ] ; subst

destruct String.eqb_specs k as ← | Hne

–injection H as ←

rewrite Z.eqb_refl

reflexivity

–destruct Z.eqb_specz v as → | _

+exfalso

apply Hv1

clear - H

induction xs as | k′ v′ xs IHx ; simpl in * ; try discriminate

destruct String.eqbs k' ; injection H as → ; left ; reflexivity | right ; auto

+apply IH ; split | ; assumption

Every enumeration's table has each atom once and each code once.

148Lemma codes_ok

∀ e

table_okcodese

Proof 1 step Qed

intros e ; destruct e ; split ; simpl ; repeat constructor ; simpl ; intuition discriminate | ; constructor

The code of an atom in an enumeration reads back as the atom.

155Lemma codes_round_trip

∀ e t z

enc_codee t = Somez

dec_codee z = Somet

Proof 5 steps Qed

intros e t z H

destruct t as | s | | ; simpl in H ; try discriminate

unfold dec_code

rewrite assoc_round_trip_ _ _ codes_oke H

reflexivity