rocq/backend/NfbTotal.v

NFB's Gallina reader is total and its fuel never runs out (docs/nfb.md, Relation to the term form and the Rocq model).

Every function of NfbTerm.v is a Gallina function, so decode returns on every list of words, a module or none. Where a reader recurses on more than the structure of its input it takes fuel, and each call site gives it the length of the words it reads. This file proves that length is enough: with any more fuel each reader gives the same answer, so no input is refused for want of fuel (sections_fuel, group_fuel, blocks_fuel, rest_fuel, side_term_fuel, name_recs_fuel). Each holds because every round of the reader takes at least one word.

From Stdlib Require Import String ZArith List Bool Lia

From Nanofil Require Import Term Maps Cfg

From Backend Require Import NfbTerm Nfb

Import ListNotations

Whether fuel f and every larger fuel give the reader the same answer.

21Definition enoughX : Type run : nat → optionX f : nat : Prop ≔

∀f′, f ≤ f′%nat → runf′ = runf

A reader whose answer is the same for the next fuel, from fuel f on, has enough fuel f.

26Lemma enough_step

∀ X : Type run : nat → optionX f

∀g, f ≤ g%nat → runSg = rung

enoughrun f

Proof 4 steps Qed

intros X run f H f′ Hf

induction Hf as | g Hg IH ; reflexivity |

rewrite H by lia

exact IH

Taking words

take_acc n leaves n fewer words.

36Lemma take_acc_length

∀ n xs acc a b

take_accn xs acc = Somea, b

lengthb + n = lengthxs%nat

Proof 7 steps Qed

induction n as | n IH ; intros xs acc a b H ; cbn [ take_acc ] in H

–injection H as _ ←

lia

–destruct xs as | x xs ; discriminate |

apply IH in H

simpl

lia

take n leaves n fewer words.

44Lemma take_length

∀ n xs a b

taken xs = Somea, b

lengthb + n = lengthxs%nat

Proof 2 steps Qed

intros n xs a b H

exact take_acc_lengthn xs [ ] a b H

Reading n of what a reader reads, where the reader never leaves more words than it was given, leaves no more.

49Lemma read_n_length

∀ X : Type r : readerX n ws v rest

∀ws v rest, rws = Somev, rest → lengthrest ≤ lengthws%nat

read_nn r ws = Somev, rest

lengthrest ≤ lengthws%nat

Proof 11 steps Qed

intros X r n

induction n as | n IH ; intros ws v rest Hr H ; simpl in H

–injection H as _ ←

lia

–destruct rws as a ws₁ | eqn: E1 ; | discriminate

simpl in H

destruct read_nn r ws1 as b ws₂ | eqn: E2 ; | discriminate

simpl in H

injection H as _ ←

apply Hr in E1

apply IH in E2 ; lia | exact Hr

As read_n_length, for a counted list, which also takes its count.

61Lemma read_counted_length

∀ X : Type r : readerX ws v rest

∀ws v rest, rws = Somev, rest → lengthrest ≤ lengthws%nat

read_countedr ws = Somev, rest

lengthrest < lengthws%nat

Proof 5 steps Qed

intros X r ws v rest Hr H

unfold read_counted in H

destruct ws as | n ws′ ; discriminate |

destruct negbat_leastZ.to_natn ws' ; discriminate |

apply read_n_length in H ; simpl ; lia | exact Hr

Two readers that agree on every list of at most L words, the first never leaving more words than it was given, read the same n of them from at most L words.

74Lemma read_n_ext

∀ X : Type r₁ r₂ : readerX L n ws

∀ws, lengthws ≤ L%nat → r₁ws = r₂ws

∀ws v rest, r₁ws = Somev, rest → lengthrest ≤ lengthws%nat

lengthws ≤ L%nat

read_nn r₁ ws = read_nn r₂ ws

Proof 7 steps Qed

intros X r₁ r₂ L n

induction n as | n IH ; intros ws Hext Hr Hws ; simpl ; reflexivity |

rewrite <- Hextws Hws

destruct r1ws as a ws₁ | eqn: E1 ; simpl ; | reflexivity

rewrite IH ; reflexivity | exact Hext | exact Hr |

apply Hr in E1

lia

As read_n_ext, for a counted list.

87Lemma read_counted_ext

∀ X : Type r₁ r₂ : readerX L ws

∀ws, lengthws ≤ L%nat → r₁ws = r₂ws

∀ws v rest, r₁ws = Somev, rest → lengthrest ≤ lengthws%nat

lengthws ≤ L%nat

read_countedr₁ ws = read_countedr₂ ws

Proof 7 steps Qed

intros X r₁ r₂ L ws Hext Hr Hws

unfold read_counted

destruct ws as | n ws′ ; reflexivity |

destruct negbat_leastZ.to_natn ws' ; reflexivity |

apply read_n_extr1 r2 L ; auto

simpl in Hws

lia

Sections

Splitting the words into sections, with fuel their length.

101Lemma sections_fuel

∀ ws

enoughλf ⇒ read_sectionsf ws lengthws

Proof 15 steps Qed

intros ws

apply enough_step

intros g Hg

revert ws Hg

induction g as | g IH ; intros ws Hg

–destruct ws as | a | b ws ; simpl in * ; try reflexivity ; lia

–destruct ws as | a | b ws ; try reflexivity

change read_sectionsSSg a :: b :: ws with let* p ≔ takeZ.to_natb ws in let* rest ≔ read_sectionsSg sndp in Somea, fstp :: rest

change read_sectionsSg a :: b :: ws with let* p ≔ takeZ.to_natb ws in let* rest ≔ read_sectionsg sndp in Somea, fstp :: rest

destruct takeZ.to_natb ws as c rest | eqn: E ; | reflexivity

cbn [ fst snd ]

apply take_length in E

simpl in Hg

rewrite IH by lia

reflexivity

Side sections

Case on every match in the hypotheses, dropping the cases where one says none is some, then on every pair, and take apart each hypothesis that says some is some.

122Ltac cases ≔

repeat match goal withH : context [match ?x with _ ⇒ _ end] |- _⇒destruct x eqn :? ; try discriminateend;repeat match goal withq : _ × _%type |- _⇒destruct qend;cbn [ fst snd ] in *;repeat match goal withH : Some_ = Some_ |- _⇒injection H as ; substend

A side section's term leaves fewer words than it was given.

130Lemma side_term_length

∀ pool f ws t rest

read_side_termpool f ws = Somet, rest

lengthrest < lengthws%nat

Proof 8 steps Qed

intros pool f

induction f as | f IH ; intros ws t rest H ; simpl in H ; discriminate |

assert Hr : ∀ws v rest, read_side_termpool f ws = Somev, rest → lengthrest ≤ lengthws%nat

{intros ws′ v rest′ H′

apply IH in H'

lia

unfold read_wide in H

cases ; simpl ; try lia;match goal withE : read_counted_ _ = Some_, _ |- _⇒apply read_counted_length in E ; simpl ; lia | exact Hrend

A side section's term, with fuel the length of its words: each level of the term takes a word.

145Lemma side_term_fuel

∀ pool ws

enoughλf ⇒ read_side_termpool f ws lengthws

Proof 17 steps Qed

intros pool ws

apply enough_step

intros g Hg

revert ws Hg

induction g as | g IH ; intros ws Hg

–destruct ws ; simpl in * ; reflexivity | lia

–assert Hext : ∀ws′, lengthws′ ≤ g%nat → read_side_termpool Sg ws′ = read_side_termpool g ws′ by auto

assert Hr : ∀ws v rest, read_side_termpool Sg ws = Somev, rest → lengthrest ≤ lengthws%nat

{intros ws′ v rest H

apply side_term_length in H

lia

destruct ws as | tag ws ; reflexivity |

simpl in Hg

change read_side_termpool SSg tag :: ws with match tag :: ws with 0 :: ws′ ⇒ let* p ≔ read_widews′ in SomeTIntfstp, sndp | 1 :: i :: ws′ ⇒ let* a ≔ ZMap.findi pool in Somea, ws′ | 2 :: i :: ws′ ⇒ let* fa ≔ ZMap.findi pool in let* fn ≔ atom_stringfa in let* p ≔ read_countedread_side_termpool Sg ws′ in match fstp with [ ] ⇒ None | _ ⇒ SomeTAppfn fstp, sndp end | 3 :: ws′ ⇒ let* p ≔ read_countedread_side_termpool Sg ws′ in SomeTListfstp, sndp | _ ⇒ None end

change read_side_termpool Sg tag :: ws with match tag :: ws with 0 :: ws′ ⇒ let* p ≔ read_widews′ in SomeTIntfstp, sndp | 1 :: i :: ws′ ⇒ let* a ≔ ZMap.findi pool in Somea, ws′ | 2 :: i :: ws′ ⇒ let* fa ≔ ZMap.findi pool in let* fn ≔ atom_stringfa in let* p ≔ read_countedread_side_termpool g ws′ in match fstp with [ ] ⇒ None | _ ⇒ SomeTAppfn fstp, sndp end | 3 :: ws′ ⇒ let* p ≔ read_countedread_side_termpool g ws′ in SomeTListfstp, sndp | _ ⇒ None end

cbv beta iota

repeat first|reflexivity|rewrite read_counted_extread_side_termpool Sg read_side_termpool g g _ Hext Hr by simpl in * ; lia|match goal with|- context [match ?x with _ ⇒ _ end]⇒destruct x eqn :?end

One round of reading NAMES, with fuel S f.

191Lemma name_recs_S

∀ pool d f w ws

read_name_recspool d Sf w :: ws

let rt ≔ read_side_termpool d in

let* a ≔ read_countedrt w :: ws in

let* b ≔ read_countedrt snda in

let* c ≔ read_countedrt sndb in

let* rest ≔ read_name_recspool d f sndc in

SomemkFnamesfsta fstb fstc :: rest

Proof 1 step Qed

reflexivity

NAMES, at any depth, with fuel the length of its words: each function's names take a word at least.

202Lemma name_recs_fuel

∀ pool d ws

enoughλf ⇒ read_name_recspool d f ws lengthws

Proof 23 steps Qed

intros pool d ws

apply enough_step

intros g Hg

revert ws Hg

induction g as | g IH ; intros ws Hg

–destruct ws ; simpl in * ; reflexivity | lia

–destruct ws as | w ws ; reflexivity |

rewrite ! name_recs_S

cbv zeta

set rt := read_side_termpool d

assert Hr : ∀ws v rest, rtws = Somev, rest → lengthrest ≤ lengthws%nat

{intros ws′ v rest H

apply side_term_length in H

lia

destruct read_countedrt w :: ws as a wa | eqn: Ea ; | reflexivity

cbn [ fst snd ]

destruct read_countedrt wa as b wb | eqn: Eb ; | reflexivity

cbn [ fst snd ]

destruct read_countedrt wb as c wc | eqn: Ec ; | reflexivity

cbn [ fst snd ]

apply read_counted_length in Ea , Eb , Ec ; try exact Hr

rewrite IH by simpl in * ; lia

reflexivity

Instructions and blocks

An instruction leaves fewer words than it was given: at least its header is read.

222Lemma inst_length

∀ r g n x ws t n′ x′ rest

read_instr g n x ws = Somet, n′, x′, rest

lengthrest < lengthws%nat

Proof 3 steps Qed

intros r g n x ws t n′ x′ rest H

unfold read_inst in H

cases;repeat match goal withE : take_ _ = Some_ |- _⇒apply take_length in Eend;simpl in *;lia

One round of reading a group, with fuel S f.

231Lemma group_S

∀ r g f n x ws

read_groupr g Sf n x ws

match next_opcodews with

Somec

⇒

Z.eqbgroupc g

→

let* p ≔ read_instr g n x ws in

let 't, n₁, x₁, ws₁ ≔ p in

let* q ≔ read_groupr g f n₁ x₁ ws₁ in

let 'ts, n₂, x₂, ws₂ ≔ q in

Somet :: ts, n₂, x₂, ws₂

else

Some[ ], n, x, ws

None

⇒

Some[ ], n, x, ws

Proof 1 step Qed

reflexivity

A group leaves no more words than it was given.

247Lemma group_length

∀ r g f n x ws ts n′ x′ rest

read_groupr g f n x ws = Somets, n′, x′, rest

lengthrest ≤ lengthws%nat

Proof 13 steps Qed

intros r g f

induction f as | f IH ; intros n x ws ts n′ x′ rest H

–simpl in H

destruct next_opcodews ; destruct Z.eqbgroupz g | ; try discriminate ; injection H as ; subst ; lia

–rewrite group_S in H

destruct next_opcodews as c | ; | injection H as ; subst ; lia

destruct Z.eqbgroupc g ; | injection H as ; subst ; lia

destruct read_instr g n x ws as t n₁ x₁ ws₁ | eqn: E1 ; | discriminate

destruct read_groupr g f n1 x1 ws1 as ts′ n₂ x₂ ws₂ | eqn: E2 ; | discriminate

injection H as ; subst

apply inst_length in E1

apply IH in E2

lia

A group of instructions, with fuel the length of its words: each instruction takes a word.

263Lemma group_fuel

∀ r g n x ws

enoughλf ⇒ read_groupr g f n x ws lengthws

Proof 14 steps Qed

intros r g n x ws

apply enough_step

intros f Hf

revert n x ws Hf

induction f as | f IH ; intros n x ws Hf

–destruct ws ; simpl in Hf ; | lia

reflexivity

–rewrite group_Sr g Sf , group_Sr g f

destruct next_opcodews as c | ; | reflexivity

destruct Z.eqbgroupc g ; | reflexivity

destruct read_instr g n x ws as t n₁ x₁ ws₁ | eqn: E1 ; | reflexivity

apply inst_length in E1

rewrite IH by lia

reflexivity

Blocks, with fuel the length of their words.

276Lemma blocks_fuel

∀ r k i n x ws

enoughλf ⇒ read_blocksr f i k n x ws lengthws

Proof 21 steps Qed

intros r k i n x ws f′ Hf

revert i n x ws f' Hf

induction k as | k IH ; intros i n x ws f′ Hf ; reflexivity |

simpl

destruct ZMap.findi r_labelsr as l | ; | reflexivity

rewrite group_fuelr 0 n x ws f' by lia

destruct read_groupr 0 lengthws n x ws as phis n₁ x₁ ws₁ | eqn: E1 ; | reflexivity

pose proof E1 as L₁

apply group_length in L1

destruct Z.eqbi 0 && negbNat.eqblengthphis 0 ; reflexivity |

rewrite group_fuelr 1 n1 x1 ws1 f' by lia

rewrite <- group_fuelr 1 n1 x1 ws1 lengthws by lia

destruct read_groupr 1 lengthws n1 x1 ws1 as insts n₂ x₂ ws₂ | eqn: E2 ; | reflexivity

pose proof E2 as L₂

apply group_length in L2

destruct read_instr 2 n2 x2 ws2 as j n₃ x₃ ws₃ | eqn: E3 ; | reflexivity

pose proof E3 as L₃

apply inst_length in L3

rewrite IHi + 1%Z n3 x3 ws3 f' by lia

rewrite IHi + 1%Z n3 x3 ws3 lengthws by lia

reflexivity

Elements of a list

Whether reading the field f takes a word: all fields but a definition's.

300Definition takes_wordf : field : bool ≔

match f with

FDef_ | FLocalDef_

⇒

false

⇒

true

Naming a definition reads no word.

304Lemma def_name_words

∀ r s t s′

def_namer s = Somet, s′

s_wordss′ = s_wordss

Proof 3 steps Qed

intros r s t s′ H

unfold def_name in H

cases ; reflexivity

The next word is one word.

308Lemma next_word_words

∀ s z s′

next_words = Somez, s′

Slengths_wordss′ = lengths_wordss%nat

Proof 4 steps Qed

intros ws rb n x z s′ H

unfold next_word in H

simpl in *

cases ; reflexivity

A field leaves no more words than it was given, and fewer if it takes a word.

314Lemma field_words

∀ r f e s e′ s′

read_fieldr f e s = Somee′, s′

lengths_wordss′

takes_wordf

→

else

≤

lengths_wordss

Proof 2 steps Qed

intros r f e s e′ s′ H

destruct f ; simpl in H |- * ; cases;repeat match goal withE : next_word_ = Some_ |- _⇒apply next_word_words in EE : def_name_ _ = Some_ |- _⇒apply def_name_words in EE : read_result_ _ _ = Some_ |- _⇒unfold read_result in Eend;cases;repeat match goal withE : next_word_ = Some_ |- _⇒apply next_word_words in EE : def_name_ _ = Some_ |- _⇒apply def_name_words in Eend;simpl in *;repeat match goal withE : s_words?a = s_words_ |- _⇒rewrite E in * ; clear Eend;lia

Fields leave no more words than they were given, and fewer if one of them takes a word.

336Lemma fields_words

∀ r fs e s e′ s′

read_fieldsr fs e s = Somee′, s′

lengths_wordss′

existsbtakes_word fs

→

else

≤

lengths_wordss

Proof 8 steps Qed

intros r fs

induction fs as | f fs IH ; intros e s e′ s′ H ; simpl in H |- *

–injection H as ← ←

lia

–destruct read_fieldr f e s as e₁ s₁ | eqn: E ; | discriminate

apply field_words in E

apply IH in H

destruct takes_wordf , existsbtakes_word fs ; simpl in * ; lia

One round of reading the rest, with fuel S f.

348Lemma rest_S

∀ r el fs f s

read_restr el fs Sf s

match s_wordss with

[ ]

⇒

Some[ ], s

⇒

let* p ≔ read_fieldsr fs [ ] s in

let* t ≔ fill_patel fstp in

let* q ≔ read_restr el fs f sndp in

Somet :: fstq, sndq

Proof 1 step Qed

reflexivity

The elements to the end of an instruction, with fuel the number of its words left, when each element takes a word.

359Lemma rest_fuel

∀ r el fs s

existsbtakes_word fs = true

enoughλf ⇒ read_restr el fs f s lengths_wordss

Proof 20 steps Qed

intros r el fs s Hfs

apply enough_step

intros g Hg

revert s Hg

induction g as | g IH ; intros s Hg

–destruct s_wordss eqn: E ; simpl in Hg ; | lia

rewrite rest_S

simpl

rewrite E

reflexivity

–rewrite rest_Sr el fs Sg , rest_Sr el fs g

destruct s_wordss as | w ws eqn: Ew ; reflexivity |

destruct read_fieldsr fs [ ] s as e s₁ | eqn: E ; | reflexivity

cbn [ fst snd ]

destruct fill_patel e ; | reflexivity

apply fields_words in E

rewrite Hfs , Ew in E

simpl in E , Hg

rewrite IH by lia

reflexivity

Every list of a form read to the end has elements that take a word, so rest_fuel covers each one the reader reads.

376Lemma forms_rest_take_words

forallb

λ f ⇒

forallb

λ lf ⇒

match lf with

FRest_ _ fs

⇒

existsbtakes_word fs

⇒

true

f_fieldsf

forms

true

Proof 2 steps Qed

vm_compute

reflexivity

The reader as a whole

decode gives every list of words a module or refuses it: it is a function, and by the lemmas above no refusal is for want of fuel.

388Theorem decode_total

∀ ws

decodews = None ∨ ∃m, decodews = Somem

Proof 2 steps Qed

intros ws

destruct decodews as m | ; right ; exists m | left ; reflexivity