rocq/backend/NfbRead.v
NFB's term reader gives back what its writer wrote (NfbTerm.v, docs/nfb.md): for every module term t that encode_term writes with NAMES, read_term reads the words back as t itself, says whether they had NAMES, and those are words encode_term writes for t with that answer, which module_words keeps whole (read_encode_term).
The proof goes up in layers. First the words: integers written as two or three words, inline constants, codes, tables numbered by number and read by index_map, sorted string tables, bytes packed four to a word, and sections. Then one instruction: a term matched by its form's pattern is filled again from the holes its fields read back, given the reader's tables invert the writer's. The facts about the forms table, such as distinct opcodes and every hole read by a field, are checked once by computation. Then the groups of a block, the blocks and the body of a function, its temporaries named in the order of their first definitions; the data items, the side section of names, the items, and the module.
From Stdlib Require Import String ZArith List Bool Ascii Lia Sorted
From Nanofil Require Import Term Maps Cfg
From Backend Require Import Order NfbTerm
Import ListNotations
Open Scope string_scope
Open Scope list_scope
Open Scope Z_scope
Words
words_eqb is equality of word lists.
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 H1 H2
apply Z.eqb_eq in H1
subst
f_equal
auto
A signed 64-bit integer, written as two words, reads back.
Proof 18 steps Qed
intros n H
unfold i64ok in H
apply andb_true_iff in H as H1 H2
apply Z.leb_le in H1
apply Z.ltb_lt in H2
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.
Proof 22 steps Qed
intros n H
unfold wideok in H
apply andb_true_iff in H as H1 H2
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.
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 H1 H2
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.
A table whose keys and values each occur once gives back the key of the value of a key.
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.
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.
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
A class's code is from 1 to 8.
Proof 5 steps Qed
intros t z H
destruct t as | s | | ; simpl in H ; try discriminate
unfold sassoc , class_codes in H
repeat destruct String.eqbs _ ; injection H as ← ; lia |
discriminate
The two words of a signed 64-bit integer, read as two words.
Proof 4 steps Qed
intros n H
pose proof i64_round_tripn H as R
destruct i64_wordsn as | lo | hi | ; try contradiction
eauto
The three words of a signed 96-bit integer.
Proof 4 steps Qed
intros n H
pose proof wide_round_tripn H as R
destruct wide_wordsn as | a | b | c | ; try contradiction
eauto
Small facts
The arguments app_args finds are those of the compound.
Proof 7 steps Qed
intros f n t ts H
destruct t as | | g us | ; simpl in H ; try discriminate
destruct String.eqb_specf g ; | discriminate
destruct Nat.eqb_specn lengthus ; | discriminate
injection H as ←
subst
auto
The atom is_atom recognizes.
Proof 5 steps Qed
intros a t H
destruct t ; simpl in H ; try discriminate
apply String.eqb_eq in H
subst
reflexivity
mapo relates each element to its image.
Proof 8 steps Qed
intros X Y f
induction xs as | x xs IH ; intros ys H ; simpl in H
–injection H as ←
constructor
–destruct fx eqn: E ; | discriminate
destruct mapof xs eqn: E2 ; | discriminate
injection H as ←
constructor ; auto
mapo over two lists joined.
Proof 11 steps Qed
mapo gives as many images as elements.
Proof 4 steps Qed
take_acc the first part of two joined lists, after what it took.
Proof 7 steps Qed
induction xs as | x xs IH ; intros ys acc ; cbn [ length app take_acc ]
–rewrite rev_append_rev
reflexivity
–rewrite IH
cbn [ rev ]
rewrite <- app_assoc
reflexivity
take the first part of two joined lists.
Proof 4 steps Qed
An integer that take counts.
Proof 3 steps Qed
at_least n is whether there are n words or more.
Proof 1 step Qed
induction n as | n IH ; intros | x xs ; simpl ; auto
at_least of a count, as a comparison of integers.
Proof 3 steps Qed
intros n xs
rewrite at_least_len
destruct Nat.leb_specZ.to_natn lengthxs ; destruct Z.ltb_specZ.of_natlengthxs n ; simpl ; reflexivity || lia
A ZMap lookup after an add.
Proof 6 steps Qed
A lookup in the empty ZMap.
∀ A k
ZMap.findk ZMap.emptyA = None
Proof 2 steps Qed
intros
apply ZF.empty_o
Tables
index_map's fold leaves the keys below its start alone.
i < n
ZMap.findi fstfold_leftλp x ⇒ ZMap.addsndp x fstp, sndp + 1 xs m, n = ZMap.findi m
Proof 5 steps Qed
intros X xs
induction xs as | y ys IH ; intros m n i H ; simpl ; reflexivity |
rewrite IH by lia
rewrite zfind_add
destruct Z.eqb_specn i ; lia | reflexivity
index_map's fold maps the key n + k to the k-th element.
n ≤ i
nth_errorxs Z.to_nati − n = Somex
ZMap.findi fstfold_leftλp x ⇒ ZMap.addsndp x fstp, sndp + 1 xs m, n = Somex
Proof 13 steps Qed
intros X xs
induction xs as | y ys IH ; intros m n i x H1 H2 ; simpl
–destruct Z.to_nati − n ; discriminate
–destruct Z.eqb_speci n as [ ->| E ]
+rewrite Z.sub_diag in H2
simpl in H2
injection H2 as →
rewrite imap_below by lia
rewrite zfind_add , Z.eqb_refl
reflexivity
+apply IH ; lia |
replace Z.to_nati − n with SZ.to_nati − n + 1 in H2 by lia
exact H2
index_map maps i to the i-th element.
The table of wide constants maps a constant to an index of it.
∀ xs : listZ m n c i
ZMap.findc fstfold_leftλp c ⇒ ZMap.addc sndp fstp, sndp + 1 xs m, n = Somei
ZMap.findc m = Somei ∨ n ≤ i ∧ nth_errorxs Z.to_nati − n = Somec
Proof 15 steps Qed
induction xs as | y ys IH ; intros m n c i H ; simpl in H ; left ; exact H |
destruct IH_ _ _ _ H as H1 | H1 H2
–rewrite zfind_add in H1
destruct Z.eqb_specy c as [ <-| E ]
+injection H1 as ←
right
split ; lia |
rewrite Z.sub_diag
reflexivity
+left
exact H1
–right
split ; lia |
replace Z.to_nati − n with SZ.to_nati − n + 1 by lia
exact H2
number never renumbers a name.
Proof 9 steps Qed
induction xs as | y ys IH ; intros m n acc x i H ; simpl ; exact H |
rewrite nm_find_add
destruct name_eqbx y eqn: Exy ; | exact H
apply term_eqb_eq in Exy
subst
unfold nm_mem in E
rewrite H in E
discriminate
What number makes: the names newly numbered come after those numbered before, each name's number is its place in the list of both, and the count is that list's length.
n = Z.of_natlengthL0 ++ revacc
numberxs m n acc = m′, n′, F
Proof 74 steps Qed
induction xs as | y ys IH ; intros m n acc L0 Hm Hn m′ n′ F E ; simpl in E
–injection E as ← ← ←
exists [ ]
rewrite app_nil_r
split ; reflexivity |
split ; exact Hm |
split ; exact Hn |
split ; intros x |
split ; simpl ; lia | reflexivity
–pose proof number_keepys as K
–injection Hx as ←
apply term_eqb_eq in Exy
subst x
split ; lia |
rewrite Hn , Nat2Z.id , nth_error_app2 by apply Nat.le_refl
rewrite Nat.sub_diag
reflexivity
–destruct Hmx i Hx as H0 H1
split ; exact H0 |
rewrite nth_error_app1 ; exact H1 |
apply nth_error_Some
rewrite H1
discriminate
assert Hn′ : n + 1 = Z.of_natlengthL0 ++ revy :: acc
{simpl
rewrite app_assoc , length_app
simpl
lia
exists y :: nw
simpl in HF
rewrite <- app_assoc in HF
split ; exact HF |
split ; exact H1 |
split ; exact H2 |
split
∗intros x [ <-| Hx ] ; | auto
unfold nm_mem
rewrite nm_find_add in K
rewrite term_eqb_refl in K
rewrite E in K
simpl in K
rewrite K by reflexivity
reflexivity
number from nothing: each name's number is its place among the names newly numbered.
Proof 10 steps Qed
Names that differ are all numbered anew, in order.
Proof 16 steps Qed
induction xs as | y ys IH ; intros m n acc Hd Hm ; simpl
–rewrite app_nil_r
reflexivity
–rewrite Hmy or_introleq_refl
inversion Hd as [ |? ? Hy Hys ] ; subst
rewrite IH ; simpl ; rewrite <- app_assoc ; reflexivity | exact Hys |
intros x Hx
rewrite nm_mem_add
destruct name_eqbx y eqn: E
+simpl
apply Hm
right
exact Hx
Distinct names numbered from nothing: the number of each is its place in the list.
Proof 12 steps Qed
intros xs m n F Hd E
assert HF : F = xs
{pose proof number_nodupxs nm_empty 0 [ ] Hd as H
rewrite E in H
apply H
intros x _
unfold nm_mem
rewrite nm_find_empty
reflexivity
subst F
destruct number_fresh_ _ _ _ E as H1 & _
auto
Names numbered from nothing, as many as the names: they differ, and each one's number is its place.
Proof 5 steps Qed
intros xs m n F E Hn
destruct number_fresh_ _ _ _ E as H1 & H2 & H3 & H4 & H5
assert F = xs by apply H4 ; lia
subst
auto
The places that nth_error finds for two names in a list without duplicates differ when the names do.
Proof 6 steps Qed
intros X xs i j x Hd Hi Hj
eapply NoDup_nth_error ; eauto
apply nth_error_Some
rewrite Hi
discriminate
congruence
Sorted tables
One step of merge_uniq on two lists that are not empty.
∀ x xs y ys
Proof 1 step Qed
reflexivity
merge_uniq with an empty side.
∀ xs
merge_uniqlt eqb xs [ ] = xs ∧ merge_uniqlt eqb [ ] xs = xs
Proof 1 step Qed
intros | x xs ; split ; reflexivity
Every element of a merge is an element of one side.
Proof 11 steps Qed
induction xs as | x xs IHx ; intros ys z H
–rewrite proj2merge_uniq_nilys in H
auto
–induction ys as | y ys IHy
+rewrite proj1merge_uniq_nil_ in H
auto
+rewrite merge_uniq_cons in H
∗destruct IHx_ _ H ; auto
∗destruct IHx_ _ H ; auto
∗destruct IHyH as H1 | H1 ; simpl in H1 ; auto
The merge of two strictly sorted lists is strictly sorted.
Proof 28 steps Qed
induction xs as | x xs IHx ; intros ys Hx Hy
–rewrite proj2merge_uniq_nilys
exact Hy
–induction ys as | y ys IHy
+rewrite proj1merge_uniq_nil_
exact Hx
+apply StronglySorted_inv in Hx as Hx′
destruct Hx' as Hxs Fx
apply StronglySorted_inv in Hy as Hy′
destruct Hy' as Hys Fy
rewrite Forall_forall in Fx , Fy
rewrite merge_uniq_cons
∗apply eqb_true in E1
subst y
constructor ; auto |
apply Forall_forall
intros z Hz
destruct merge_in_ _ _ Hz ; auto
∗constructor ; auto |
apply Forall_forall
intros z Hz
destruct merge_in_ _ _ Hz as [ H | [ <-| H ] ] ; eauto
Merging the runs in pairs keeps each strictly sorted, and leaves fewer of them.
∀ rs
ForallStronglySortedλa b ⇒ lta b = true rs
ForallStronglySortedλa b ⇒ lta b = true merge_pairslt eqb rs ∧ 2 × lengthmerge_pairslt eqb rs ≤ lengthrs + 1%nat
Proof 6 steps Qed
fix IH 1
intros | r1 | r2 rs H ; simpl ; auto | split ; exact H | lia |
inversion H as [ |? ? H1 H' ] ; subst
inversion H' as [ |? ? H2 H'' ] ; subst
destruct IHrs H'' as A B
split ; constructor ; apply merge_sorted ; auto | exact A | lia
With enough rounds, merging leaves one strictly sorted run.
Proof 5 steps Qed
induction fuel as | f IH ; intros | r1 | r2 rs H Hl ; simpl in * ; try constructor ; try inversion H ; assumption ; try lia
destruct merge_pairs_sortedr1 :: r2 :: rs H as A B
apply IH ; exact A |
simpl in B |- *
lia
sort_uniq gives a strictly sorted list.
Proof 9 steps Qed
sort_uniq gives each element once.
Proof 8 steps Qed
intros xs
pose proof sort_uniq_sortedxs as H
induction H as | a l _ IH F ; constructor ; auto
intros Ha
rewrite Forall_forall in F
specialize Fa Ha
discriminate
Strings compare equal to themselves.
Proof 4 steps Qed
induction s as | c s IH ; simpl ; reflexivity |
unfold Ascii.compare
rewrite N.compare_refl
exact IH
The order of strings is transitive.
Proof 13 steps Qed
induction a as | x a IH ; intros | y b | z c ; cbn [ String.compare ] ; try discriminate ; auto
unfold Ascii.compare
destruct N.compare_specN_of_asciix N_of_asciiy as E1 | E1 | E1 ; try discriminate ; destruct N.compare_specN_of_asciiy N_of_asciiz as E2 | E2 | E2 ; try discriminate ; intros H1 H2
–rewrite E1 , E2 , N.compare_refl
eauto
–rewrite E1
rewrite proj2N.compare_lt_iff_ _ E2
reflexivity
–rewrite <- E2
rewrite proj2N.compare_lt_iff_ _ E1
reflexivity
–rewrite proj2N.compare_lt_iff_ _ N.lt_trans_ _ _ E1 E2
reflexivity
A sorted table of strings has each string once.
∀ xs
NoDupsort_uniqstr_lt String.eqb xs
Proof 20 steps Qed
apply sort_uniq_nodup
–apply String.eqb_eq
–unfold str_lt , atom_compare
intros x y z H1 H2
destruct String.comparex y eqn: E1 ; try discriminate
destruct String.comparey z eqn: E2 ; try discriminate
rewrite string_lt_trans_ _ _ E1 E2
reflexivity
–unfold str_lt , atom_compare
intros x y H1 H2
rewrite String.compare_antisym
destruct String.comparex y eqn: E ; try discriminate ; auto
apply String.compare_eq_iff in E
subst
rewrite String.eqb_refl in H1
discriminate
The atoms of distinct strings are distinct.
Proof 6 steps Qed
intros ss H
induction H as | a l Ha _ IH ; simpl ; constructor ; auto
intros Hin
apply in_map_iff in Hin as b & E & Hb
injection E as →
contradiction
Bytes
A byte: from 0 to 255.
0 ≤ b < 256
The four bytes of a packed word come back.
Proof 13 steps Qed
intros b0 b1 b2 b3 H0 H1 H2 H3
unfold byte in *
split ; | split ; | split
–symmetry
apply Z.mod_unique_ _ b1 + b2 × 256 + b3 × 65536 ; lia
–rewrite <- Z.div_unique_ 256 b1 + b2 × 256 + b3 × 65536 b0 by lia
symmetry
apply Z.mod_unique_ _ b2 + b3 × 256 ; lia
–rewrite <- Z.div_unique_ 65536 b2 + b3 × 256 b0 + b1 × 256 by lia
symmetry
apply Z.mod_unique_ _ b3 ; lia
–symmetry
apply Z.div_unique_ _ _ b0 + b1 × 256 + b2 × 65536 ; lia
Bytes packed and unpacked come back first, and the packed words are a quarter as many, rounded up.
Proof 25 steps Qed
fix IH 1
intros | b0 | b1 | b2 | b3 r H ; simpl ; split ; reflexivity | lia | | | | ; inversion H as [ |? ? Hb0 H1 ] ; subst ; try inversion H1 as [ |? ? Hb1 H2 ] ; subst ; try inversion H2 as [ |? ? Hb2 H3 ] ; subst ; try inversion H3 as [ |? ? Hb3 H4 ] ; subst
A byte string's words read back.
Proof 14 steps Qed
intros bs rest H
destruct unpack_packbs H as A B
unfold read_bytes , bytes_words
simpl app
cbv beta iota
The bytes of a string are bytes.
∀ s
Forallbyte string_bytess
Proof 9 steps Qed
intros s
unfold string_bytes
apply Forall_forall
intros b Hb
apply in_map_iff in Hb
destruct Hb as c & ← & _
pose proof nat_ascii_boundedc
unfold byte
lia
A string's bytes give the string back.
∀ s
Proof 8 steps Qed
intros s
unfold bytes_string , string_bytes
rewrite map_map
erewrite map_ext ; rewrite map_id ; apply string_of_list_ascii_of_string |
intros c
simpl
rewrite Nat2Z.id
apply ascii_nat_embedding
Readers
read_n reads back the elements whose words follow one another.
Proof 6 steps Qed
intros X r xs wss rest H
induction H as | x ws xs wss Hx _ IH ; simpl ; reflexivity |
rewrite <- app_assoc , Hx
simpl
rewrite IH
reflexivity
Elements whose words are not empty are fewer than their words.
Proof 6 steps Qed
intros X xs wss H
induction H as | x ws xs wss Hx _ IH ; simpl ; lia |
rewrite length_app
destruct ws ; congruence |
simpl
lia
read_counted reads back the count and the elements.
Forall2λx ws ⇒ ws ≠ [ ] ∧ ∀rest, rws ++ rest = Somex, rest xs wss
read_countedr Z.of_natlengthxs :: concatwss ++ rest = Somexs, rest
Proof 16 steps Qed
intros X r xs wss rest H
unfold read_counted
simpl app
cbv beta iota
assert L : lengthxs ≤ lengthconcatwss%nat
rewrite at_least_spec
replace Z.of_natlengthconcatwss ++ rest <? Z.of_natlengthxs with false by symmetry ; apply Z.ltb_ge ; rewrite length_app ; lia
rewrite Nat2Z.id
apply read_n_rt
eapply Forall2_impl ; | exact H
intros a b _ H2
exact H2
A Forall2 of a map.
Proof 2 steps Qed
intros X Y P f xs H
induction xs ; simpl ; constructor ; auto with datatypes
A string table's words read back.
∀ ss rest
read_stringsstrings_wordsss ++ rest = Somess, rest
Proof 12 steps Qed
intros ss rest
unfold read_strings , strings_words
rewrite flat_map_concat_map
apply read_counted_rt
apply forall2_map
intros s _
split ; unfold bytes_words ; discriminate |
intros rest′
rewrite read_bytes_rt by apply string_bytes_byte
simpl
rewrite bytes_string_rt
reflexivity
A table of wide constants reads back.
∀ cs rest
forallbwideok cs = true
read_countedread_wide Z.of_natlengthcs :: flat_mapwide_words cs ++ rest = Somecs, rest
Proof 13 steps Qed
intros cs rest H
rewrite flat_map_concat_map
apply read_counted_rt
apply forall2_map
intros c Hc
rewrite forallb_forall in H
destruct wide_words_rtc Hc Hc as a & b & d & E & R
rewrite E
split ; discriminate |
intros rest′
simpl
rewrite R
reflexivity
Sections
The sections' words split back into the sections.
Proof 13 steps Qed
induction ss as | id ws ss IH ; intros fuel H ; destruct fuel ; reflexivity |
unfold sections_words in *
cbn [ flat_map fst snd ] in *
destruct fuel as | f ; simpl in H ; lia |
cbn [ read_sections ]
simpl app
cbv iota
rewrite take_app_z
cbn [ fst snd ]
rewrite IH ; reflexivity |
simpl in H
rewrite length_app in H
lia
The sections of a module in their order: the core ones present, then NAMES if any.
c1
→
[ ]
else
1, a1
++
c2
→
[ ]
else
2, a2
++
c3
→
[ ]
else
3, a3
++
c4
→
[ ]
else
4, a4
++
c5
→
[ ]
else
5, a5
++
b
→
256, a6
else
[ ]
What the reader finds in a module's sections.
∀ c1 c2 c3 c4 c5 b a1 a2 a3 a4 a5 a6
Proof 3 steps Qed
intros
subst ss
destruct c1 , c2 , c3 , c4 , c5 , b ; split ; reflexivity || repeat split ; reflexivity
Patterns
The holes of a pattern, in order.
match_pat on the patterns ps and the terms ts in turn.
match ps, ts with
fill_pat on the patterns ps in turn.
match_pat, one level unfolded.
∀ p t e
Proof 1 step Qed
intros i | s | f ps | ps t e ; reflexivity
fill_pat, one level unfolded.
Proof 1 step Qed
intros i | s | f ps | ps e ; reflexivity
Induction on patterns, with the hypothesis on every pattern of a list.
Every key of the bindings nw is one of the holes hs.
Bindings in front of others do not hide a hole they do not bind.
Proof 4 steps Qed
induction nw as | j t nw IH ; intros e h H ; simpl in * ; reflexivity |
destruct Nat.eqb_spech j ; subst ; tauto |
apply IH
tauto
A list without duplicates, split in two.
Proof 9 steps Qed
intros X a b
induction a as | x a IH ; intros H ; simpl in *
–split ; constructor |
split ; exact H | intros h
What a pattern's match makes: bindings of its holes in front of the old ones; and the term, filled again from any bindings that agree on its holes, if the holes differ.
pat_ok for a list of patterns.
Proof 31 steps Qed
induction 1 as | p ps Hp Hps IH ; intros | t ts e0 e H ; simpl in H ; try discriminate
–injection H as ←
split ; exists [ ] ; split ; reflexivity | intros h | intros ; reflexivity
–destruct match_patp t e0 as e1 | eqn: E1 ; | discriminate
destruct Hp_ _ _ E1 as nw1 & → & K1 F1
destruct IH_ _ _ H as nw2 & → & K2 F2
split
+exists nw2 ++ nw1
rewrite app_assoc
split ; reflexivity |
intros h Hh
simpl
rewrite map_app in Hh
apply in_app_or in Hh as Hh | Hh ; apply in_or_app ; auto
+intros Hd e′ He
simpl in Hd
apply nodup_app_inv in Hd as D1 & D2 & D3
simpl
rewrite F1D1 e'
∗rewrite F2D2 e' ; reflexivity |
intros h Hh
apply He
simpl
apply in_or_app ; auto
∗intros h Hh
rewrite He by simpl ; apply in_or_app ; auto
apply env_get_app_out
intros Hk
apply D3h Hh
apply K2
exact Hk
Every pattern is pat_ok.
Proof 43 steps Qed
apply pat_rect2
–intros i t e0 e H
rewrite match_pat_eq in H
injection H as ←
split
+exists i, t
split ; reflexivity |
intros h H ; exact H
+intros _ e′ He
rewrite fill_pat_eq
rewrite He by left ; reflexivity
simpl
rewrite Nat.eqb_refl
reflexivity
–intros s t e0 e H
rewrite match_pat_eq in H
destruct is_atoms t eqn: E ; | discriminate
injection H as ←
apply is_atom_inv in E
subst
split
+exists [ ]
split ; reflexivity | intros h
+intros ; reflexivity
–intros f ps Hps t e0 e H
rewrite match_pat_eq in H
destruct t as | | g ts | ; try discriminate
destruct String.eqb_specf g as [ <-| ] ; | discriminate
split ; exact A |
intros Hd e′ He
rewrite fill_pat_eq
rewrite BHd e' He
reflexivity
–intros ps Hps t e0 e H
rewrite match_pat_eq in H
destruct t as | | g ts | ts ; try discriminate
split ; exact A |
intros Hd e′ He
rewrite fill_pat_eq
rewrite BHd e' He
reflexivity
The term a pattern matched is filled again from bindings that agree with the match on its holes, when they differ.
Proof 2 steps Qed
intros p t e H
exact proj2match_fill_okp t [ ] e H
Fields
The hole a field reads.
The hole an instruction's field reads.
The reader's tables invert the writer's: each id maps back to the name, string or constant it was written for.
| ok_syms | ||
| ok_strs | ||
| ok_consts | ||
| ok_temps | ||
| ok_labels | ||
| ok_locals |
Reading the definitions ds, the reader's rebind words and next id going from rb and n to rb' and n', names each in turn.
defs_read of two lists joined.
Proof 7 steps Qed
induction a as | d a IH ; intros b rb n rb′ n′ H ; simpl in *
–exists rb, n
auto
–destruct H as rb1 & n1 & H1 & H2
destruct IH_ _ _ _ _ H2 as rb2 & n2 & A & B
exists rb2, n2
split ; exists rb1, n1 ; auto | exact B
The reader's locals from the id x on are xs, up to the id x'.
match xs with
[ ]
⇒
x = x′
locals_read of two lists joined.
Proof 7 steps Qed
induction a as | v a IH ; intros b x x′ H ; simpl in *
–exists x
auto
–destruct H as H1 H2
destruct IH_ _ _ H2 as x1 & A & B
exists x1
auto
The local a field defines, if it is FLocalDef.
Bindings e1 that the bindings e agree with.
A binding env_get finds is in the list.
Proof 2 steps Qed
A bound key has a value.
Proof 3 steps Qed
An operand word reads back: tag 1 or 2 for a constant.
Proof 21 steps Qed
intros w r n z T H
destruct inlinen eqn: E
–destruct inline_round_tripr w_constsw n E as z′ & H1 & H2
rewrite H in H1
injection H1 as ←
split ; left | exact H2
unfold const_word in H
rewrite E in H
injection H as ←
rewrite Z.add_comm , Z.mod_add by lia
reflexivity
–unfold const_word in H
rewrite E in H
destruct ZMap.findn w_constsw as i | eqn: Ei ; | discriminate
injection H as ←
assert M : i × 4 + 2 mod 4 = 2 by rewrite Z.add_comm , Z.mod_add by lia ; reflexivity
assert D : i × 4 + 2 / 4 = i by rewrite Z.add_comm , Z.div_add by lia ; reflexivity
split ; right ; exact M |
unfold const_of
rewrite M , D
exact ok_consts_ _ T _ _ Ei
An operand reads back from its one word.
Proof 37 steps Qed
intros w r v o T H
destruct v as | | f | x | | ; try discriminate
cbv beta iota delta [ opnd_out ] in H
destruct String.eqb_specf "tmp" as [ ->| N1 ]
injection H as ←
split ; reflexivity |
exists i × 4
split ; reflexivity |
unfold value_of
rewrite Z.mod_mul , Z.div_mul by lia
cbn [ Z.eqb ]
rewrite ok_temps_ _ T _ _ Ei
reflexivity
–destruct String.eqb_specf "const" as [ ->| N2 ]
+destruct x as n | | | ; try discriminate
destruct const_wordw_constsw n as z | eqn: Ez ; | discriminate
injection H as ←
split ; reflexivity |
exists z
split ; reflexivity |
destruct const_rtw r n z T Ez as M C
unfold value_of
+destruct String.eqb_specf "global" as [ ->| N3 ] ; | discriminate
injection H as ←
split ; reflexivity |
exists i × 4 + 3
split ; reflexivity |
assert M : i × 4 + 3 mod 4 = 3 by rewrite Z.add_comm , Z.mod_add by lia ; reflexivity
assert D : i × 4 + 3 / 4 = i by rewrite Z.add_comm , Z.div_add by lia ; reflexivity
unfold value_of
rewrite M , D
cbn [ Z.eqb ]
rewrite ok_syms_ _ T _ _ Ei
reflexivity
The temporaries a call's result defines, and its one word, read back.
∀ r v o ws rb n x rb′ n′
result_outv = Someo
∃z, o_wordso = z ∧ read_resultr z mkRstws rb n x = Somev, mkRstws rb′ n′ x
Proof 66 steps Qed
intros r v o ws rb n x rb′ n′ H D
unfold result_out in H
destruct result_defsv as ds | eqn: Eds ; | discriminate
destruct is_atom"void" v eqn: Ev
–injection H as ←
apply is_atom_inv in Ev
subst v
simpl in D
destruct D as ← ←
exists 0
split ; reflexivity
–unfold result_defs in Eds
rewrite Ev in Eds
destruct app_args"result" 2 v as | d | k | | eqn: Er ; try apply app_args_inv in Er ; destruct Er as _ Er ; discriminate
injection H as ←
injection Eds as ←
apply app_args_inv in Et as → Lx
destruct xs as | y | ; try discriminate
apply app_args_inv in Er as → _
simpl in D
destruct D as rb1 & n1 & D1 & ← & ←
exists c
split ; reflexivity |
pose proof class_code_range_ _ Ec as R
unfold read_result
replace 256 ≤? c with false by symmetry ; apply Z.leb_gt ; lia
rewrite codes_round_trip_ _ _ Ec , D1
reflexivity
+destruct app_args"tuple" 1 v as | | | | rs | eqn: Et ; try discriminate
destruct rs as | r1 | r2 ; try discriminate
destruct app_args"result" 2 r1 as | d1 | k1 | | eqn: E1 ; try discriminate
destruct app_args"result" 2 r2 as | d2 | k2 | | eqn: E2 ; try discriminate
injection H as ←
cbn [ mapo ] in Eds
rewrite E1 , E2 in Eds
destruct app_args"tmp" 1 d1 as | x1 | eqn: Ed1 ; try discriminate
destruct app_args"tmp" 1 d2 as | x2 | eqn: Ed2 ; try discriminate
injection Eds as ←
apply app_args_inv in Ed1 as → _
apply app_args_inv in Ed2 as → _
apply app_args_inv in E1 as → _
apply app_args_inv in E2 as → _
apply app_args_inv in Et as → _
simpl in D
destruct D as rb1 & n1 & D1 & rb2 & n2 & D2 & ← & ←
exists 256 + 16 × c1 + c2
split ; reflexivity |
pose proof class_code_range_ _ Ec1
pose proof class_code_range_ _ Ec2
unfold read_result
replace Z.eqb256 + 16 × c1 + c2 0 with false by symmetry ; apply Z.eqb_neq ; lia
replace Z.eqb256 + 16 × c1 + c2 15 with false by symmetry ; apply Z.eqb_neq ; lia
replace 256 ≤? 256 + 16 × c1 + c2 with true by symmetry ; apply Z.leb_le ; lia
replace 256 + 16 × c1 + c2 − 256 / 16 with c1 by apply Z.div_unique_ _ _ c2 ; lia
replace 256 + 16 × c1 + c2 mod 16 with c2 by apply Z.mod_unique_ _ 16 + c1 ; lia
replace c1 <? 16 with true by symmetry ; apply Z.ltb_lt ; lia
rewrite codes_round_trip_ _ _ Ec1 , codes_round_trip_ _ _ Ec2
rewrite D1
cbn [ fst snd ]
rewrite D2
reflexivity
The next word of the reader's state.
Proof 1 step Qed
reflexivity
The hole of a local's definition, which writes no word, is bound.
One field reads back into its hole the value it was written from.
∀ w r e f o e0 ws rb n x rb′ n′ x′
∃v, env_getfield_holef e = Somev ∧ read_fieldr f e0 mkRsto_wordso ++ ws rb n x = Somefield_holef, v :: e0, mkRstws rb′ n′ x′
Proof 128 steps Qed
intros w r e f o e0 ws rb n x rb′ n′ x′ T H B D L
destruct f as i | i | en i | i | i | i | i | i | i | i | i | i | i | i ; cbn [ field_hole field_locals field_bound ] in * ; cbv beta iota delta [ field_out ] in H ; destruct env_geti e as v | eqn: Ev ; try discriminate ; try congruence ; exists v ; split ; try reflexivity ; cbn [ read_field ]
FDef
–injection H as ←
cbn [ o_words o_defs defs_read locals_read app ] in *
destruct D as rb1 & n1 & D1 & ← & ←
subst x'
rewrite D1
reflexivity
FClass
injection H as ←
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite next_word_cons
cbn [ fst snd ]
rewrite codes_round_trip_ _ _ Ez
reflexivity
FEnum
–destruct enc_codeen v as z | eqn: Ez ; | discriminate
injection H as ←
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite next_word_cons
cbn [ fst snd ]
rewrite codes_round_trip_ _ _ Ez
reflexivity
FU32
–destruct v as k | | | ; try discriminate
injection H as ←
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
reflexivity
FI64
–destruct v as k | | | ; try discriminate
injection H as ←
destruct i64_words_rtk Ek as lo & hi & Ew & R
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite Ew
cbn
rewrite R
reflexivity
FOpnd
–destruct opnd_rtw r v o T H as Hd & z & Hw & Hv
rewrite Hd in D
rewrite Hw
cbn [ defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite next_word_cons
cbn [ fst snd ]
rewrite Hv
reflexivity
FLabel
injection H as ←
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite next_word_cons
cbn [ fst snd ]
rewrite ok_labels_ _ T _ _ Ez
reflexivity
FTarget
–destruct app_args"poll" 1 v as | l | | eqn: Ep ; | destruct nm_findl w_labelsw as z | eqn: Ez ; | discriminate ; injection H as ← | | ; try destruct nm_findv w_labelsw as z | eqn: Ez ; | discriminate ; injection H as ← ; cbn [ o_words o_defs wwords defs_read locals_read app ] in * ; destruct D as ← ← ; subst x' ; rewrite next_word_cons ; cbn [ fst snd ] ; try replace z × 2 / 2 with z by symmetry ; apply Z.div_mul ; lia ; rewrite ok_labels_ _ T _ _ Ez ; rewrite Z.mod_mul by lia ; reflexivity
apply app_args_inv in Ep as → _
replace z × 2 + 1 / 2 with z by rewrite Z.add_comm , Z.div_add by lia ; reflexivity
replace z × 2 + 1 mod 2 with 1 by rewrite Z.add_comm , Z.mod_add by lia ; reflexivity
rewrite ok_labels_ _ T _ _ Ez
reflexivity
FLocal
injection H as ←
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite next_word_cons
cbn [ fst snd ]
rewrite ok_locals_ _ T _ _ Ez
reflexivity
FLocalDef
–injection H as ←
cbn [ o_words o_defs wnil defs_read locals_read app ] in *
destruct D as ← ←
destruct L as L1 ←
rewrite L1
reflexivity
FStr
–destruct v as | a | | ; try discriminate
injection H as ←
cbn [ o_words o_defs wwords defs_read locals_read app ] in *
destruct D as ← ←
subst x'
rewrite next_word_cons
cbn [ fst snd ]
rewrite ok_strs_ _ T _ _ Ez
reflexivity
FResult
–cbn [ locals_read ] in L
subst x'
destruct result_rtr v o ws rb n x rb' n' H D as z & Hw & R
rewrite Hw
cbn [ app ]
rewrite next_word_cons
cbn [ fst snd ]
rewrite R
reflexivity
FLower
–cbn [ locals_read ] in L
subst x'
destruct is_atom"none" v eqn: En
+destruct app_args"lower" 1 v as | p | | eqn: Ep ; try discriminate
destruct opnd_outw p as op | eqn: Eo ; | discriminate
injection H as ←
rewrite Hd , Hw in *
cbn [ app ] in *
destruct D as ← ←
apply app_args_inv in Ep as → _
cbn
rewrite Hv
reflexivity
FFlightArg
–cbn [ locals_read ] in L
subst x'
destruct app_args"address" 1 v as | p | | eqn: Ep ; | destruct opnd_outw p as op | eqn: Eo ; | discriminate ; injection H as ← ; destruct opnd_rtw r p op T Eo as Hd & z & Hw & Hv ; apply app_args_inv in Ep as → _ | | ; try destruct opnd_outw v as op | eqn: Eo ; | discriminate ; injection H as ← ; destruct opnd_rtw r v op T Eo as Hd & z & Hw & Hv ; cbn [ o_words o_defs wwords wapp defs_read app ] in * ; rewrite Hd , Hw in * ; cbn [ app ] in * ; destruct D as ← ← ; cbn ; rewrite Hv ; reflexivity
The fields fs read back into their holes the values they were written from.
∀ w r e fs o e0 ws rb n x rb′ n′ x′
∃e1, read_fieldsr fs e0 mkRsto_wordso ++ ws rb n x = Somee1 ++ e0, mkRstws rb′ n′ x′ ∧ env_ofe e1 ∧ ∀h, Inh mapfield_hole fs → Inh mapfst e1
Proof 32 steps Qed
intros w r e fs
induction fs as | f fs IH ; intros o e0 ws rb n x rb′ n′ x′ T H B D L ; simpl in H
–injection H as ←
cbn in D , L
destruct D as ← ←
subst x'
exists [ ]
split ; reflexivity |
split ; intros h v | intros h
destruct fields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
inversion B as [ |? ? B1 B2 ] ; subst
destruct defs_read_app_ _ _ _ _ _ _ D as rb1 & n1 & D1 & D2
cbn [ flat_map ] in L
destruct locals_read_app_ _ _ _ _ L as x1 & L1 & L2
destruct read_field_rtw r e f a e0 o_wordsb ++ ws rb n x rb1 n1 x1 T Ea B1 D1 L1 as v & Hv & R1
rewrite <- app_assoc
cbn [ read_fields ]
rewrite R1
cbn [ fst snd ]
destruct IHb field_holef, v :: e0 ws rb1 n1 x1 rb' n' x' T eq_refl B2 D2 L2 as e1 & R2 & E2 & K2
exists e1 ++ field_holef, v
rewrite <- app_assoc
split ; exact R2 |
split
+intros h [ <-| Hh ] ; rewrite map_app ; apply in_or_app ; right ; left ; reflexivity | left ; auto
Whether a field writes a word.
Whether a field defines a local.
Whether a field defines temporaries.
A field's temporaries defined less its words: at most this.
The sum of the fields' fcost.
An operand's word.
Proof 11 steps Qed
intros w v o H
destruct v as | | f | x | | ; try discriminate
cbv beta iota delta [ opnd_out ] in H
destruct String.eqbf "tmp" ; destruct nm_findx w_tempsw ; injection H as ← ; auto | discriminate |
destruct String.eqbf "const"
–destruct x as k | | | ; try discriminate
destruct const_wordw_constsw k ; | discriminate
injection H as ←
auto
–destruct String.eqbf "global" ; | discriminate
A call result's word and the temporaries it defines.
Proof 34 steps Qed
intros v o H
unfold result_out in H
destruct result_defsv as ds | eqn: Eds ; | discriminate
destruct is_atom"void" v eqn: Ev
–unfold result_defs in Eds
rewrite Ev in Eds
destruct app_args"result" 2 v as | d | k | | eqn: Er ; try apply app_args_inv in Er ; destruct Er as _ Er ; discriminate
injection H as ←
simpl
injection Eds as ←
apply app_args_inv in Et as _ Lx
split ; reflexivity |
split ; lia | reflexivity
+destruct app_args"tuple" 1 v as | | | | rs | ; try discriminate
destruct rs as | r1 | r2 ; try discriminate
destruct app_args"result" 2 r1 as | d1 | k1 | | ; try discriminate
destruct app_args"result" 2 r2 as | d2 | k2 | | ; try discriminate
injection H as ←
simpl
split ; reflexivity |
split ; | reflexivity
apply mapo_length in Eds
simpl in Eds
lia
A field defines at most its words plus its fcost.
Proof 35 steps Qed
intros w e f o H
destruct f as i | i | en i | i | i | i | i | i | i | i | i | i | i | i ; cbn [ fcost ] ; cbv beta iota delta [ field_out ] in H ; try destruct env_geti e as v | ; | discriminate
–injection H as ←
simpl
lia
–destruct enc_codeen v ; injection H as ← ; simpl ; lia | discriminate
–destruct v ; try discriminate
destruct u32okn ; injection H as ← ; simpl ; lia | discriminate
–destruct v ; try discriminate
destruct i64okn ; injection H as ← ; simpl ; lia | discriminate
–injection H as ←
simpl
lia
–destruct v ; try discriminate
–destruct result_shape_ _ H as A & B & _
lia
–destruct is_atom"none" v ; injection H as ← ; simpl ; lia |
destruct app_args"lower" 1 v as | p | | ; try discriminate
destruct opnd_outw p as op | eqn: Eo ; | discriminate
injection H as ←
destruct opnd_shape_ _ _ Eo as A B
rewrite ! length_app , A , B
simpl
lia
–destruct app_args"address" 1 v as | p | | ; | destruct opnd_outw p as op | eqn: Eo ; | discriminate ; injection H as ← ; destruct opnd_shape_ _ _ Eo as A B ; cbn [ o_words o_defs wapp wwords ] ; rewrite ! length_app , A , B ; simpl ; lia | | ; destruct opnd_outw v as op | eqn: Eo ; | discriminate ; injection H as ← ; destruct opnd_shape_ _ _ Eo as A B ; cbn [ o_words o_defs wapp wwords ] ; rewrite ! length_app , A , B ; simpl ; lia
A field that writes a word writes one at least.
Proof 7 steps Qed
intros w e f o H W
pose proof field_costw e f o H as C
destruct f ; cbn [ writes_word fcost ] in * ; try discriminate ; try lia
cbv beta iota delta [ field_out ] in H
destruct result_shape_ _ H as A & _
lia
The fields define at most their words plus their fscost.
∀ w e fs o
fields_outw e fs = Someo
Z.of_natlengtho_defso ≤ Z.of_natlengtho_wordso + fscostfs ∧ existsbwrites_word fs = true → 1 ≤ lengtho_wordso%nat
Proof 19 steps Qed
intros w e
induction fs as | f fs IH ; intros o H ; simpl in H
–injection H as ←
simpl
split ; lia | discriminate
destruct fields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
destruct IHb eq_refl as C1 W1
pose proof field_cost_ _ _ _ Ea as C0
rewrite ! length_app
split ; unfold fscost in C1 ; lia |
intros Hw
apply orb_true_iff in Hw as Hw | Hw
+pose proof field_words_ _ _ _ Ea Hw
lia
+specialize W1Hw
lia
The conditions on a list's element: its holes differ and are read by its fields, which define no local, write a word and define no more temporaries than words.
NoDuppat_holesel ∧ ∀h, Inh pat_holesel → Inh mapfield_hole fs ∧ Forallλf ⇒ is_localdeff = false fs ∧ existsbwrites_word fs = true ∧ fscostfs ≤ 0
The elements of a list define no more temporaries than their words, and write as many words as elements at least.
Proof 16 steps Qed
intros w el fs
induction ts as | t ts IH ; intros o Ok H ; simpl in H
–injection H as ←
simpl
lia
–destruct match_patel t [ ] as et | ; | discriminate
destruct fields_outw et fs as a | eqn: Ea ; | discriminate
destruct elems_outw el fs ts as b | eqn: Eb ; | discriminate
injection H as ←
destruct IHb Ok eq_refl as C1 L1
destruct fields_cost_ _ _ _ Ea as C0 W0
destruct Ok as _ & _ & _ & Wr & Cs
specialize W0Wr
rewrite ! length_app
split ; lia
Fields that define no local define none.
Proof 3 steps Qed
intros e fs H
induction H as | f fs Hf _ A B ; simpl ; split ; constructor |
destruct f ; simpl in Hf ; try discriminate ; split ; exact A | constructor ; exact I | exact B
The elements of a list read back, given their count.
Proof 30 steps Qed
intros w r el fs
induction ts as | t ts IH ; intros o ws rb n x rb′ n′ T Ok H D ; simpl in H
–injection H as ←
cbn in D |- *
destruct D as ← ←
reflexivity
–destruct match_patel t [ ] as et | eqn: Et ; | discriminate
destruct fields_outw et fs as a | eqn: Ea ; | discriminate
destruct elems_outw el fs ts as b | eqn: Eb ; | discriminate
injection H as ←
destruct defs_read_app_ _ _ _ _ _ _ D as rb1 & n1 & D1 & D2
destruct Ok as Nd & Cov & NoL & Wr & Cs eqn: Ok'
destruct no_localset fs NoL as Ln Bd
assert L0 : locals_readr flat_mapfield_localset fs x x by rewrite Ln ; reflexivity
destruct read_fields_rtw r et fs a [ ] o_wordsb ++ ws rb n x rb1 n1 x T Ea Bd D1 L0 as e1 & R1 & E1 & K1
cbn [ read_count length ]
rewrite <- app_assoc , R1
cbn [ fst snd ]
rewrite app_nil_r
rewrite match_fillel t et Et Nd e1
+rewrite IHb ws rb1 n1 x rb' n' T conjNd conjCov conjNoL conjWr Cs eq_refl D2
reflexivity
+intros h Hh
destruct env_get_keyh e1 K1h Covh Hh as v & Hv
rewrite Hv
symmetry
apply E1
apply env_get_in
exact Hv
The elements of a list read back to the end of its words.
Proof 36 steps Qed
intros w r el fs
induction ts as | t ts IH ; intros o rb n x rb′ n′ fuel T Ok H D F ; simpl in H
–injection H as ←
cbn in D |- *
destruct D as ← ←
destruct fuel ; reflexivity
–destruct match_patel t [ ] as et | eqn: Et ; | discriminate
destruct fields_outw et fs as a | eqn: Ea ; | discriminate
destruct elems_outw el fs ts as b | eqn: Eb ; | discriminate
injection H as ←
destruct defs_read_app_ _ _ _ _ _ _ D as rb1 & n1 & D1 & D2
destruct Ok as Nd & Cov & NoL & Wr & Cs eqn: Ok'
destruct no_localset fs NoL as Ln Bd
assert L0 : locals_readr flat_mapfield_localset fs x x by rewrite Ln ; reflexivity
destruct read_fields_rtw r et fs a [ ] o_wordsb rb n x rb1 n1 x T Ea Bd D1 L0 as e1 & R1 & E1 & K1
destruct fields_cost_ _ _ _ Ea as _ W0
specialize W0Wr
rewrite length_app in F
destruct fuel as | f ; lia |
destruct o_wordsa as | w0 aw eqn: Ew ; simpl in W0 ; lia |
rewrite R1
cbn [ fst snd ]
rewrite app_nil_r
rewrite match_fillel t et Et Nd e1
reflexivity
+intros h Hh
destruct env_get_keyh e1 K1h Covh Hh as v & Hv
rewrite Hv
symmetry
apply E1
apply env_get_in
exact Hv
The fields of an instruction that define locals.
flat_map
λ lf ⇒
match lf with
_
⇒
[ ]
fs
Whether a list to the end of the words comes last, if at all.
Whether no list goes to the end of the words.
The conditions on one field of an instruction.
match lf with
An instruction's fields read back into their holes the values they were written from.
∀ w r e fs o e0 ws rb n x rb′ n′ x′
tabs_okw r
rest_lastfs = true
Foralllfield_oke fs
lfields_outw e fs = Someo
ws = [ ] ∨ no_restfs = true
locals_readr lfields_localse fs x x′
∃e1, read_lfieldsr fs e0 mkRsto_wordso ++ ws rb n x = Somee1 ++ e0, mkRstws rb′ n′ x′ ∧ env_ofe e1 ∧ ∀h, Inh maplfield_hole fs → Inh mapfst e1
Proof 83 steps Qed
intros w r e fs
induction fs as | lf fs IH ; intros o e0 ws rb n x rb′ n′ x′ T RL Ok H Ws D L ; cbn [ lfields_out ] in H
–injection H as ←
cbn in D , L
destruct D as ← ←
subst x'
exists [ ]
split ; reflexivity |
split ; intros h v | intros h
–inversion Ok as [ |? ? Ok1 Ok2 ] ; subst
destruct lf as f | i el fs1 | i el fs1
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
destruct defs_read_app_ _ _ _ _ _ _ D as rb1 & n1 & D1 & D2
unfold lfields_locals in L
cbn [ flat_map ] in L
destruct locals_read_app_ _ _ _ _ L as x1 & L1 & L2
destruct read_field_rtw r e f a e0 o_wordsb ++ ws rb n x rb1 n1 x1 T Ea Ok1 D1 L1 as v & Hv & R1
rewrite <- app_assoc
cbn [ read_lfields ]
rewrite R1
cbn [ fst snd ]
destruct IHb field_holef, v :: e0 ws rb1 n1 x1 rb' n' x' T RL Ok2 eq_refl Ws D2 L2 as e1 & R2 & E2 & K2
exists e1 ++ field_holef, v
rewrite <- app_assoc
split ; exact R2 |
split
∗intros h [ <-| Hh ] ; rewrite map_app ; apply in_or_app ; right ; left ; reflexivity | left ; auto
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
destruct defs_read_app_ _ _ _ _ _ _ D as rb1 & n1 & D1 & D2
unfold lfields_locals in L
cbn [ flat_map app ] in L
destruct elems_costw el fs1 ts a Ok1 Ea as _ Lc
cbn [ read_lfields ]
rewrite next_word_cons
cbn [ fst snd s_words ]
replace Z.of_natlengthZ.of_natlengthts :: o_wordsa ++ o_wordsb ++ ws <? Z.of_natlengthts with false by symmetry ; apply Z.ltb_ge ; simpl ; rewrite ! length_app ; lia
rewrite Nat2Z.id , <- app_assoc
rewrite read_count_rtw r el fs1 ts a o_wordsb ++ ws rb n x rb1 n1 T Ok1 Ea D1
cbn [ fst snd ]
exists e1 ++ i, TListts
rewrite <- app_assoc
split ; exact R2 |
split
∗intros h [ <-| Hh ] ; rewrite map_app ; apply in_or_app ; right ; left ; reflexivity | left ; auto
+destruct fs as | lf′ fs ; | discriminate
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
cbn [ lfields_out ] in H
injection H as ←
rewrite ! app_nil_r in *
unfold lfields_locals in L
cbn [ flat_map app locals_read ] in L
subst x'
cbn [ read_lfields s_words ]
rewrite read_rest_rtw r el fs1 ts a rb n x rb' n' _ T Ok1 Ea D le_n_
cbn [ fst snd ]
exists i, TListts
split ; reflexivity |
split
∗intros h [ <-| [ ] ]
left
reflexivity
An instruction's fields define at most its words plus their costs; a list's elements cost nothing more.
The sum of an instruction's fields' lcost.
The cost bound of an instruction's fields.
∀ w e fs o
Foralllfield_oke fs
lfields_outw e fs = Someo
Proof 37 steps Qed
intros w e
induction fs as | lf fs IH ; intros o Ok H ; cbn [ lfields_out ] in H
–injection H as ←
simpl
lia
–inversion Ok as [ |? ? Ok1 Ok2 ] ; subst
destruct lf as f | i el fs1 | i el fs1
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
pose proof field_cost_ _ _ _ Ea
specialize IHb Ok2 eq_refl
unfold lscost in IH
rewrite ! length_app
lia
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
destruct elems_cost_ _ _ _ _ Ok1 Ea
specialize IHb Ok2 eq_refl
unfold lscost in IH
cbn [ length ]
rewrite ! length_app
lia
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
destruct elems_cost_ _ _ _ _ Ok1 Ea
specialize IHb Ok2 eq_refl
unfold lscost in IH
rewrite ! length_app
lia
What an instruction defines
The temporaries a field's words define.
match f with
_
⇒
[ ]
What a field writes defines its field_defs.
Proof 30 steps Qed
intros w e f o H
destruct f as i | i | en i | i | i | i | i | i | i | i | i | i | i | i ; cbn [ field_defs ] ; cbv beta iota delta [ field_out ] in H ; try destruct env_geti e as v | ; | discriminate
–injection H as ←
reflexivity
–destruct enc_codeen v ; injection H as ← ; reflexivity | discriminate
–destruct v ; try discriminate
destruct u32okn ; injection H as ← ; reflexivity | discriminate
–destruct v ; try discriminate
destruct i64okn ; injection H as ← ; reflexivity | discriminate
–apply opnd_shape_ _ _ H
–injection H as ←
reflexivity
–destruct v ; try discriminate
–destruct is_atom"none" v ; injection H as ← ; reflexivity |
destruct app_args"lower" 1 v as | p | | ; try discriminate
destruct opnd_outw p as op | eqn: Eo ; | discriminate
injection H as ←
destruct opnd_shape_ _ _ Eo as A _
rewrite A
reflexivity
–destruct app_args"address" 1 v as | p | | ; | destruct opnd_outw p as op | eqn: Eo ; | discriminate ; injection H as ← ; destruct opnd_shape_ _ _ Eo as A _ ; cbn [ o_defs wapp wwords ] ; rewrite A ; reflexivity | | ; destruct opnd_outw v as op | eqn: Eo ; | discriminate ; injection H as ← ; destruct opnd_shape_ _ _ Eo as A _ ; cbn [ o_defs wapp wwords ] ; rewrite A ; reflexivity
A value names no temporary it defines.
∀ v
p_defsvalue_partsv = [ ]
Proof 6 steps Qed
intros v
unfold value_parts
destruct v as | | f | x | ; try reflexivity
destruct String.eqbf "global" ; reflexivity |
destruct String.eqbf "const" ; | reflexivity
destruct x ; reflexivity
What a field holds defines its field_defs.
Proof 12 steps Qed
intros e f p H
destruct f as i | i | en i | i | i | i | i | i | i | i | i | i | i | i ; cbn [ field_defs ] ; cbv beta iota delta [ field_parts ] in H ; try injection H as ← ; reflexivity ; destruct env_geti e as v | ; try discriminate
–injection H as ←
reflexivity
–injection H as ←
apply value_parts_defs
–injection H as ←
reflexivity
–destruct result_defsv ; injection H as ← ; reflexivity | discriminate
–destruct app_args"lower" 1 v as | p′ | | ; injection H as ← ; try reflexivity
apply value_parts_defs
–destruct app_args"address" 1 v as | p′ | | ; injection H as ← ; apply value_parts_defs
The temporaries some fields define are the same whether their words or their parts say so.
Proof 16 steps Qed
intros w e fs
unfold fields_parts
induction fs as | f fs IH ; intros o p H P ; cbn [ mapo fields_out ] in *
–destruct field_partse f as pf | eqn: Ef ; | discriminate
destruct mapofield_partse fs as ps | eqn: Eps ; | discriminate
injection P as ←
destruct fields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
rewrite field_parts_defs_ _ _ Ef , field_out_defs_ _ _ _ Ea
reflexivity
The same for the elements of a list.
Proof 18 steps Qed
intros w el fs
unfold elems_parts
–destruct match_patel t [ ] as et | eqn: Et ; | discriminate
cbv beta iota in P , H
destruct fields_partset fs as pf | eqn: Ef ; | discriminate
destruct mapo_ ts as ps | eqn: Eps ; | discriminate
injection P as ←
destruct fields_outw et fs as a | eqn: Ea ; | discriminate
destruct elems_outw el fs ts as b | eqn: Eb ; | discriminate
injection H as ←
rewrite fields_parts_defs_ _ _ _ _ Ea Ef
reflexivity
The temporaries an instruction defines are the same whether its words or its parts say so.
Proof 41 steps Qed
intros w e fs
unfold inst_parts
induction fs as | lf fs IH ; intros o p H P ; cbn [ mapo lfields_out ] in *
–destruct lf as f | i el fs1 | i el fs1
+destruct field_partse f as pf | eqn: Ef ; | discriminate
destruct mapo_ fs as ps | eqn: Eps ; | discriminate
injection P as ←
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
rewrite field_parts_defs_ _ _ Ef , field_out_defs_ _ _ _ Ea
reflexivity
cbv beta iota in P , H
destruct elems_partsel fs1 ts as pf | eqn: Ef ; | discriminate
destruct mapo_ fs as ps | eqn: Eps ; | discriminate
injection P as ←
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
rewrite elems_parts_defs_ _ _ _ _ _ Ea Ef
reflexivity
cbv beta iota in P , H
destruct elems_partsel fs1 ts as pf | eqn: Ef ; | discriminate
destruct mapo_ fs as ps | eqn: Eps ; | discriminate
injection P as ←
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
rewrite elems_parts_defs_ _ _ _ _ _ Ea Ef
reflexivity
The table of forms
Whether the numbers of l differ.
nodupb is sound.
Proof 11 steps Qed
induction l as | x l IH ; simpl ; intros H ; constructor
–apply andb_true_iff in H as H _
intros Hx
apply negb_true_iff in H
rewrite <- not_true_iff_false in H
apply H
apply existsb_exists
exists x
split ; exact Hx | apply Nat.eqb_refl
–apply andb_true_iff in H as _ H
auto
Whether every number of hs is one of ks.
coveredb is sound.
Proof 8 steps Qed
elem_ok as a computation.
nodupbpat_holesel && coveredbpat_holesel mapfield_hole fs && forallbλf ⇒ negbis_localdeff fs && existsbwrites_word fs && fscostfs ≤? 0
elem_okb is sound.
Proof 13 steps Qed
intros el fs H
unfold elem_okb in H
repeat rewrite andb_true_iff in H
destruct H as A & B & C & D & E
split ; apply coveredb_ok ; exact B |
split ; | split ; exact D | apply Z.leb_le ; exact E
apply Forall_forall
intros f Hf
rewrite forallb_forall in C
specialize Cf Hf
apply negb_true_iff in C
exact C
Whether an instruction's field defines a local.
match lf with
Whether an instruction's field defines temporaries.
Whether a pattern can match a local_alloc/2.
match p with
The form of local_alloc(X, Size), the one that defines a local.
What every form satisfies, as a computation.
Whether the integers of cs differ.
match cs with
[ ]
⇒
true
The table of forms, checked: every form satisfies form_okb, the opcodes differ, and opcode 100 is local_form.
forallbform_okb forms = true ∧ codes_nodupbmapf_code forms = true ∧ form_of_codeforms 100 = Somelocal_form
Proof 1 step Qed
split ; | split ; vm_compute ; reflexivity
The form find_form picks is in the table and matches.
Proof 5 steps Qed
With distinct opcodes, a form is the form of its opcode.
Proof 12 steps Qed
What a form of the table satisfies.
| fo_nodup | ||
| fo_cover | : ∀h, Inh pat_holesf_patf → Inh maplfield_hole f_fieldsf | |
| fo_rest | ||
| fo_elems | ||
| fo_cost | ||
| fo_local | : f = local_form ∨ existsblf_localdef f_fieldsf = false ∧ top_localf_patf = false | |
| fo_jump | : groupf_codef = 2 → existsblf_defines f_fieldsf = false | |
| fo_code | : 2 ≤ f_codef < 65536 | |
| fo_of_code | : form_of_codeforms f_codef = Somef |
Every form of the table is form_ok.
Proof 41 steps Qed
intros f Hf
destruct forms_checked as A & B & C
pose proof form_of_code_in_ _ B Hf as Hc
rewrite forallb_forall in A
specialize Af Hf
repeat rewrite andb_true_iff in A
destruct A as A1 & A2 & A3 & A4 & A5 & A6 & A7 & A8 & A9
split
–apply nodupb_ok
exact A1
–apply coveredb_ok
exact A2
–exact A3
–rewrite forallb_forall in A4
apply Forall_forall
intros lf Hlf
specialize A4lf Hlf
destruct lf ; exact I | apply elem_okb_ok ; exact A4 | apply elem_okb_ok ; exact A4
–apply Z.leb_le
exact A5
–apply orb_true_iff in A6 as A6 | A6
+left
apply Z.eqb_eq in A6
rewrite A6 in Hc
rewrite C in Hc
injection Hc as ←
reflexivity
–intros G
rewrite G in A7
simpl in A7
apply negb_true_iff
exact A7
–apply Z.leb_le in A8
apply Z.ltb_lt in A9
lia
–exact Hc
The locals an instruction defines: one for local_alloc(X, _).
A list of patterns matches as many terms.
Proof 5 steps Qed
induction ps as | p ps IH ; intros | t ts e0 e H ; simpl in H ; try discriminate ; auto
destruct match_patp t e0 ; | discriminate
simpl
f_equal
eauto
The fields of a form that matched t define t's locals, and each is lfield_ok.
∀ f t e
lfields_localse f_fieldsf = inst_localst ∧ Foralllfield_oke f_fieldsf
Proof 55 steps Qed
intros f t e Hf Hm
destruct form_in_okf Hf as _ _ _ El _ Lo _ _ _
destruct Lo as [ ->| [ L1 L2 ] ]
–cbn [ f_pat local_form ] in Hm
rewrite match_pat_eq in Hm
destruct t as | | g ts | ; try discriminate
destruct String.eqb_spec"local_alloc" g as [ <-| ] ; | discriminate
destruct ts as | x | y ; cbn in Hm ; try discriminate
injection Hm as ←
split ; reflexivity |
repeat constructor
cbn
discriminate
–assert Hl : lfields_localse f_fieldsf = [ ]
{unfold lfields_locals
clear El
induction f_fieldsf as | lf fs IH ; reflexivity |
simpl in L1
apply orb_false_iff in L1 as L1 L3
simpl
rewrite IHL3
destruct lf as g | | ; destruct g ; simpl in L1 ; try discriminate | | ; reflexivity
split
+rewrite Hl
unfold inst_locals
rewrite match_pat_eq in Hm
destruct f_patf as i | s | g ps | ps ; simpl in L2 ; try discriminate
∗destruct t as | | h ts | ; try discriminate
apply match_pats_length in Hm
unfold app_args
destruct String.eqb_spec"local_alloc" g as [ <-| ] ; | reflexivity
destruct Nat.eqb_spec2 lengthts ; | reflexivity
destruct ps as | p1 | p2 | ; simpl in Hm ; try lia
simpl in L2
discriminate
∗destruct t ; try discriminate
reflexivity
+apply Forall_forall
intros lf Hlf
rewrite Forall_forall in El
specialize Ellf Hlf
destruct lf as g | | ; | exact El | exact El
cbn [ lfield_ok ]
assert G : lf_localdefFOneg = false
destruct g ; simpl in G ; try discriminate ; exact I
Temporaries
The writer's temporaries M and count N come from numbering, from the map m and the count n, the definitions q still to come; the numbers so far are below n.
The rebind words of definitions read back as the definitions, with the prefix or, if every word is 0, without it.
Proof 78 steps Qed
intros r M N
induction ds as | d ds IH ; intros n q rbw n′ Ok H I ; cbn [ rebinds ] in H
–injection H as ← ←
split ; exact I |
split ; intros ; cbn ; auto
destruct I as m & acc & IM & IN & Hn & Hm
cbn [ app number ] in IM , IN
+unfold nm_mem in Em
pose proof number_keepds ++ q m n acc d j Ej as K
rewrite IM , Ed in K
injection K as ←
destruct Hmd i Ej as Hi0 Hi
replace Z.eqbi n with false in H by symmetry ; apply Z.eqb_neq ; lia
cbv beta iota in H
injection H as ← ←
split ; exact I' |
split
∗intros more
cbn [ defs_read app fst snd ]
exists Somerbw1 ++ more, n
split ; | apply D1
intros ws x
unfold def_name
replace Z.eqbi + 1 0 with false by symmetry ; apply Z.eqb_neq ; lia
replace i + 1 − 1 <? n with true by symmetry ; apply Z.ltb_lt ; lia
replace i + 1 − 1 with i by lia
rewrite Ok_ _ Ed
reflexivity
∗cbn [ existsb fst snd ]
replace Z.eqbi + 1 0 with false by symmetry ; apply Z.eqb_neq ; lia
discriminate
rewrite nm_find_add in K
rewrite term_eqb_refl in K
specialize Keq_refl
rewrite IM , Ed in K
injection K as →
rewrite Z.eqb_refl in H
cbv beta iota in H
injection H as ← ←
split ; exact IM |
split ; exact IN |
split ; lia |
intros y j Hy
rewrite nm_find_add in Hy
destruct Hmy j Hy ; lia
destruct IHn + 1 q rbw1 n1 Ok Er I1 as I′ & D1 & D2
split ; exact I' |
split
One instruction
The reader's locals from the id x on are those of ql.
∀k v, nth_errorql k = Somev → ZMap.findx + Z.of_natk r_localsr = Somev
The first locals of ql read, and the rest after them.
∀ r a b x
locals_invr x a ++ b
locals_readr a x x + Z.of_natlengtha ∧ locals_invr x + Z.of_natlengtha b
Proof 21 steps Qed
intros r a
induction a as | v a IH ; intros b x H ; cbn [ locals_read length app ] in *
–split ; lia |
intros k u Hk
rewrite Z.add_0_r
apply H
exact Hk
–assert H1 : locals_invr x + 1 a ++ b
destruct IHb x + 1 H1 as A B
split ; split |
+rewrite <- Z.add_0_rx
apply H0%nat
reflexivity
+replace x + Z.of_natSlengtha with x + 1 + Z.of_natlengtha by lia
exact A
+replace x + Z.of_natSlengtha with x + 1 + Z.of_natlengtha by lia
exact B
The header word of an instruction of opcode c and length len.
∀ c len
0 ≤ c < 65536
0 ≤ len
c + len × 65536 mod 65536 = c ∧ c + len × 65536 / 65536 = len
Proof 8 steps Qed
intros c len Hc Hl
split
–rewrite Z.mod_add by lia
apply Z.mod_small
lia
–rewrite Z.div_add by lia
rewrite Z.div_small by lia
lia
An instruction without a rebind prefix reads back.
∀ r g n x c body rest f e′ t n2 x2
2 ≤ c < 65536
groupc = g
form_of_codeforms c = Somef
read_lfieldsr f_fieldsf [ ] mkRstbody None n x = Somee′, mkRst[ ] None n2 x2
read_instr g n x c + Z.of_natlengthbody + 1 × 65536 :: body ++ rest = Somet, n2, x2, rest
Proof 21 steps Qed
intros r g n x c body rest f e′ t n2 x2 Hc Hg Hf Hr Ht
destruct header_wordc Z.of_natlengthbody + 1 ltac:lia ltac:lia as M D
unfold read_inst
cbv beta iota zeta
rewrite M
unfold rebind_code
cbv beta iota zeta
rewrite M , D , Hg , Z.eqb_refl
replace Z.of_natlengthbody + 1 <? 1 with false by symmetry ; apply Z.ltb_ge ; lia
cbv beta iota
rewrite Hf
replace Z.to_natZ.of_natlengthbody + 1 − 1 with lengthbody by lia
rewrite take_app
cbv beta iota
cbn [ fst snd ]
rewrite Hr
cbv beta iota
rewrite Ht
reflexivity
An instruction with a rebind prefix reads back.
∀ r g n x c rbw body rest f e′ t n2 x2
2 ≤ c < 65536
groupc = g
form_of_codeforms c = Somef
rbw ≠ [ ]
read_lfieldsr f_fieldsf [ ] mkRstbody Somerbw n x = Somee′, mkRst[ ] Some[ ] n2 x2
read_instr g n x rebind_code + Z.of_natlengthrbw + 1 × 65536 :: rbw ++ c + Z.of_natlengthbody + 1 × 65536 :: body ++ rest = Somet, n2, x2, rest
Proof 32 steps Qed
intros r g n x c rbw body rest f e′ t n2 x2 Hc Hg Hf Hrb Hr Ht
destruct header_wordc Z.of_natlengthbody + 1 ltac:lia ltac:lia as M D
unfold rebind_code in *
destruct header_word1 Z.of_natlengthrbw + 1 ltac:lia ltac:lia as M1 D1
unfold read_inst
cbv beta iota zeta
rewrite M1
unfold rebind_code
rewrite Z.eqb_refl
cbv beta iota
rewrite D1
destruct rbw as | z rbw ; congruence |
cbn [ length ]
replace Z.of_natSlengthrbw + 1 <? 2 with false by symmetry ; apply Z.ltb_ge ; lia
cbv beta iota
replace Z.to_natZ.of_natSlengthrbw + 1 − 1 with lengthz :: rbw by cbn [ length ] ; lia
rewrite take_app
cbv beta iota
cbn [ fst snd ]
rewrite M , D , Hg , Z.eqb_refl
replace Z.of_natlengthbody + 1 <? 1 with false by symmetry ; apply Z.ltb_ge ; lia
cbv beta iota
rewrite Hf
replace Z.to_natZ.of_natlengthbody + 1 − 1 with lengthbody by lia
rewrite take_app
cbv beta iota
cbn [ fst snd ]
rewrite Hr
cbv beta iota
rewrite Ht
reflexivity
The words of an instruction: its form's fields' words, its opcode first, and words enough for the temporaries it defines.
∀ w g b n t ws n′ ord
inst_wordsw g b n t = Somews, n′, ord
∃f e o, find_formforms t = Somef, e ∧ groupf_codef = g ∧ lfields_outw e f_fieldsf = Someo ∧ lengtho_defso ≤ lengthws%nat ∧ ∀rest, next_opcodews ++ rest = Somef_codef
Proof 55 steps Qed
intros w g b n t ws n′ ord H
unfold inst_words in H
cbn [ fst snd ] in H
change negbtrue with false in H
cbv beta iota in H
destruct lfields_outw e f_fieldsf as o | eqn: Eo ; | discriminate
cbv zeta in H
try change fstrbw, n2 with rbw in H
try change sndrbw, n2 with n2 in H
destruct 65536 ≤? Z.of_natlengtho_wordso + 1 eqn: Elen ; discriminate |
remember rebind_code + Z.of_natlengthrbw + 1 × 65536 as h0 eqn: E0 in H
injection H as ← ← _
destruct find_form_in_ _ _ _ Ef as Hin Hm
pose proof form_in_okf Hin as Fo
destruct form_localsf t e Hin Hm as _ Lok
pose proof lfields_costw e _ o Lok Eo as C
pose proof fo_costf Fo as C1
pose proof fo_codef Fo as Hc
destruct header_wordf_codef Z.of_natlengtho_wordso + 1 ltac:lia ltac:lia as M D
exists f, e, o
split ; reflexivity |
split ; exact Eg |
split ; exact Eo |
split
–rewrite length_app
cbn [ length ]
lia
–intros rest
rewrite <- app_assoc
clear D
destruct existsbλz ⇒ negbZ.eqbz 0 rbw
+rewrite <- ! app_comm_cons
destruct header_wordrebind_code Z.of_natlengthrbw + 1 ltac:unfold rebind_code ; lia ltac:lia as M1 D1
rewrite <- E0 in M1 , D1
unfold next_opcode
cbv beta iota
rewrite M1 , Z.eqb_refl , D1
replace Z.to_natZ.of_natlengthrbw + 1 − 1 with lengthrbw by lia
rewrite nth_error_app2 by apply Nat.le_refl
rewrite Nat.sub_diag
cbn [ nth_error ]
cbv beta iota
rewrite M
reflexivity
+rewrite app_nil_l , <- app_comm_cons
unfold next_opcode
cbv beta iota
rewrite M
unfold rebind_code
reflexivity
One instruction reads back, its definitions named as the writer numbered them and its locals in turn.
∀ w r g b n t ws n′ ord x ds q ql rest N
tabs_okw r
inst_wordsw g b n t = Somews, n′, ord
∀f e o, find_formforms t = Somef, e → lfields_outw e f_fieldsf = Someo → o_defso = ds
locals_invr x inst_localst ++ ql
temps_invw_tempsw N n′ q ∧ locals_invr x + Z.of_natlengthinst_localst ql ∧ read_instr g n x ws ++ rest = Somet, n′, x + Z.of_natlengthinst_localst, rest
Proof 51 steps Qed
intros w r g b n t ws n′ ord x ds q ql rest N T H Hds TI LI
unfold inst_words in H
cbn [ fst snd ] in H
change negbtrue with false in H
cbv beta iota in H
destruct lfields_outw e f_fieldsf as o | eqn: Eo ; | discriminate
cbv zeta in H
try change fstrbw, n2 with rbw in H
try change sndrbw, n2 with n2 in H
destruct 65536 ≤? Z.of_natlengtho_wordso + 1 eqn: Elen ; discriminate |
remember rebind_code + Z.of_natlengthrbw + 1 × 65536 as h0 eqn: E0 in H
injection H as ← ← _
destruct find_form_in_ _ _ _ Ef as Hin Hm
pose proof form_in_okf Hin as Fo
destruct form_localsf t e Hin Hm as Lt Lok
rewrite <- Hdsf e o eq_refl Eo in TI
destruct rebinds_rtr w_tempsw N o_defso n q rbw n2 ok_temps_ _ T Erb TI as TI′ & D1 & D2
destruct locals_inv_splitr inst_localst ql x LI as LR LI′
rewrite <- Lt in LR
split ; exact TI' |
split ; exact LI' |
assert Fill : ∀e1, env_ofe e1 → ∀h, Inh maplfield_hole f_fieldsf → Inh mapfst e1 → fill_patf_patf e1 ++ [ ] = Somet
{intros e1 E1 K1
rewrite app_nil_r
apply match_fill_ _ _ Hm fo_nodupf Fo
intros h Hh
destruct env_get_keyh e1 K1h fo_coverf Fo h Hh as v & Hv
rewrite Hv
symmetry
apply E1
apply env_get_in
exact Hv
pose proof fo_codef Fo as Hc
pose proof fo_of_codef Fo as Hcode
destruct existsbλz ⇒ negbZ.eqbz 0 rbw eqn: Ex
–specialize D1[ ]
rewrite app_nil_r in D1
destruct read_lfields_rtw r e f_fieldsf o [ ] [ ] Somerbw n x Some[ ] n2 _ T fo_restf Fo Lok Eo or_introleq_refl D1 LR as e1 & R & E1 & K1
rewrite <- app_assoc , <- ! app_comm_cons
subst h0
apply read_inst_rebindr g n x f_codef rbw o_wordso rest f e1 ++ [ ] ; auto
destruct rbw ; discriminate | congruence
Groups and blocks
The temporaries a phi or an instruction defines, as body_words gathers them.
Somep_defsp
What defs_of gathers is what the instruction's words define.
Proof 8 steps Qed
intros w t d H f e o Ef Eo
unfold defs_of , term_parts in H
rewrite Ef in H
cbn [ fst snd ] in H
destruct inst_partse f_fieldsf as p | eqn: Ep ; | discriminate
injection H as ←
symmetry
apply lfields_parts_defsw e f_fieldsf o p Eo Ep
Fields that define no temporary define none.
Proof 51 steps Qed
intros w e
induction fs as | lf fs IH ; intros o Hd H ; cbn [ lfields_out ] in H
–injection H as ←
reflexivity
–cbn [ existsb ] in Hd
apply orb_false_iff in Hd as H1 H2
assert Hel : ∀el fs1 ts oe, existsbdefines fs1 = false → elems_outw el fs1 ts = Someoe → o_defsoe = [ ]
{intros el fs1
induction ts as | t ts IHt ; intros oe Hf He ; cbn [ elems_out ] in He
–injection He as ←
reflexivity
–destruct match_patel t [ ] as et | ; | discriminate
destruct fields_outw et fs1 as a | eqn: Ea ; | discriminate
destruct elems_outw el fs1 ts as b | eqn: Eb ; | discriminate
injection He as ←
rewrite IHtb Hf eq_refl , app_nil_r
clear - Ea Hf
revert a Ea
induction fs1 as | f fs1 IHf ; intros a Ea ; cbn [ fields_out ] in Ea
+injection Ea as ←
reflexivity
+cbn [ existsb ] in Hf
apply orb_false_iff in Hf as F1 F2
destruct field_outw et f as a1 | eqn: E1 ; | discriminate
destruct fields_outw et fs1 as a2 | eqn: E2 ; | discriminate
injection Ea as ←
rewrite IHfF2 a2 eq_refl , field_out_defs_ _ _ _ E1 , app_nil_r
destruct f ; simpl in F1 ; try discriminate ; reflexivity
destruct lf as f | i el fs1 | i el fs1
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
rewrite IHb H2 eq_refl , field_out_defs_ _ _ _ Ea , app_nil_r
destruct f ; simpl in H1 ; try discriminate ; reflexivity
destruct elems_outw el fs1 ts as a | eqn: Ea ; | discriminate
destruct lfields_outw e fs as b | eqn: Eb ; | discriminate
injection H as ←
rewrite IHb H2 eq_refl , Hel_ _ _ _ H1 Ea
reflexivity
A jump defines no temporary.
∀ w b n t ws n′ ord f e o
o_defso = [ ]
Proof 7 steps Qed
intros w b n t ws n′ ord H f e o Ef Eo
destruct inst_shape_ _ _ _ _ _ _ _ H as f1 & e1 & o1 & E1 & G & _
rewrite Ef in E1
injection E1 as ← ←
destruct find_form_in_ _ _ _ Ef as Hin _
apply no_definesw e f_fieldsf o ; | exact Eo
apply fo_jumpf form_in_okf Hin G
A phi or a jump defines no local.
Proof 15 steps Qed
intros w g b n t ws n′ ord H G
destruct inst_shape_ _ _ _ _ _ _ _ H as f & e & o & Ef & Eg & _
destruct find_form_in_ _ _ _ Ef as Hin Hm
pose proof form_in_okf Hin as Fo
destruct form_localsf t e Hin Hm as Lt _
rewrite <- Lt
destruct fo_localf Fo as [ ->| [ L1 _ ] ] ; cbn in Eg ; lia |
unfold lfields_locals
clear - L1
induction f_fieldsf as | lf fs IH ; reflexivity |
simpl in L1
apply orb_false_iff in L1 as L1 L3
simpl
rewrite IHL3
destruct lf as g | | ; destruct g ; simpl in L1 ; try discriminate | | ; reflexivity
The reader stops a group before the words ws.
None
⇒
True
The first opcode of a group's words that are not empty.
∀ w g b n ts ws n′ ord
insts_wordsw g b n ts = Somews, n′, ord
ts = [ ] ∧ ws = [ ] ∧ n′ = n ∨ ∀rest, ∃c, next_opcodews ++ rest = Somec ∧ groupc = g
Proof 13 steps Qed
intros w g b n | t ts ws n′ ord H ; cbn [ insts_words ] in H
–injection H as ← ← _
left
auto
–right
destruct inst_wordsw g b n t as ws1 n1 o1 | eqn: E1 ; | discriminate
destruct insts_wordsw g b n1 ts as ws2 n2 o2 | ; | discriminate
injection H as ← ← _
intros rest
destruct inst_shape_ _ _ _ _ _ _ _ E1 as f & e & o & _ & G & _ & _ & N
exists f_codef
rewrite <- app_assoc
auto
A group of instructions reads back, as many as its words hold.
∀ w r g b ts n ws n′ ord x dl q ql rest fuel N
tabs_okw r
insts_wordsw g b n ts = Somews, n′, ord
locals_invr x flat_mapinst_locals ts ++ ql
lengthws ≤ fuel%nat
stopsg rest
temps_invw_tempsw N n′ q ∧ locals_invr x + Z.of_natlengthflat_mapinst_locals ts ql ∧ read_groupr g fuel n x ws ++ rest = Somets, n′, x + Z.of_natlengthflat_mapinst_locals ts, rest ∧ lengthconcatdl ≤ lengthws%nat ∧ lengthts ≤ lengthws%nat ∧ lengthflat_mapinst_locals ts ≤ lengthws%nat
Proof 42 steps Qed
intros w r g b
induction ts as | t ts IH ; intros n ws n′ ord x dl q ql rest fuel N T H Hd TI LI F S ; cbn [ insts_words mapo ] in H , Hd
–injection H as ← ← _
injection Hd as ←
cbn in *
rewrite Z.add_0_r
split ; exact TI |
split ; exact LI |
split ; | lia
unfold stops in S
destruct fuel ; cbn [ read_group ] ; destruct next_opcoderest as c | ; try reflexivity ; replace Z.eqbgroupc g with false by symmetry ; apply Z.eqb_neq ; exact S ; reflexivity
–destruct inst_wordsw g b n t as ws1 n1 o1 | eqn: E1 ; | discriminate
destruct insts_wordsw g b n1 ts as ws2 n2 o2 | eqn: E2 ; | discriminate
injection H as ← ← _
destruct defs_oft as d | eqn: Ed ; | discriminate
injection Hd as ←
cbn [ concat flat_map ] in TI , LI |- *
rewrite <- app_assoc in TI , LI
destruct read_inst_rtw r g b n t ws1 n1 o1 x d concatdl' ++ q flat_mapinst_locals ts ++ ql ws2 ++ rest N T E1 defs_of_okw t d Ed TI LI as TI1 & LI1 & R1
destruct inst_shape_ _ _ _ _ _ _ _ E1 as f & e & o & Ef & G & Eo & Ld & Nx
rewrite defs_of_okw t d Ed f e o Ef Eo in Ld
assert Lt : lengthinst_localst ≤ 1%nat by unfold inst_locals ; destruct app_args_ _ _ as [ [ |? [ |? [ | ] ] ] | ] ; simpl ; lia
rewrite length_app in F
assert Ne : ws1 ≠ [ ] by intros → ; specialize Nx[ ] ; discriminate
destruct fuel as | fuel′ ; destruct ws1 ; congruence | simpl in F ; lia |
assert F′ : lengthws2 ≤ fuel'%nat by destruct ws1 ; congruence | simpl in F ; lia
destruct IHn1 ws2 n2 o2 _ dl' q ql rest fuel' N T E2 eq_refl TI1 LI1 F' S as TI2 & LI2 & R2 & L1 & L2 & L3
rewrite length_app , Nat2Z.inj_add , Z.add_assoc
split ; exact TI2 |
split ; exact LI2 |
split
+cbn [ read_group ]
rewrite <- app_assoc , Nx , G , Z.eqb_refl
rewrite R1
cbv beta iota
rewrite R2
reflexivity
+rewrite ! length_app
destruct ws1 as | z ws1 ; congruence |
cbn [ length ] in *
split ; | split ; lia
The locals a block's instructions define.
None
⇒
[ ]
The reader's labels from the index b on are those of the blocks.
match bs with
[ ]
⇒
True
bt :: bs′
⇒
∀l phis insts j, block_partsbt = Somel, phis, insts, j → ZMap.findb r_labelsr = Somel ∧ labels_atr b + 1 bs′
A block's parts make the block.
∀ bt l phis insts j
block_partsbt = Somel, phis, insts, j
Proof 6 steps Qed
intros bt l phis insts j H
unfold block_parts in H
destruct app_args"block" 4 bt as | l′ | | | | ps | | | | is | j′ | eqn: E ; try discriminate
injection H as ← ← ← ←
apply app_args_inv in E as → _
reflexivity
The phis of a group define no local.
Proof 9 steps Qed
intros w b n phis
revert n
induction phis as | t ts IH ; intros n ws n′ ord H ; reflexivity |
cbn [ insts_words ] in H
destruct inst_wordsw 0 b n t as a na oa | eqn: Ea ; | discriminate
destruct insts_wordsw 0 b na ts as c nc oc | eqn: Ec ; | discriminate
cbn [ flat_map ]
rewrite inst_locals_group_ _ _ _ _ _ _ _ Ea ltac:lia
exact IH_ _ _ _ Ec
The blocks read back from their index, the temporaries of their phis and instructions named in order of definition.
∀ w r bs b n ws n′ ord x dss q ql rest fuel N
tabs_okw r
blocks_wordsw b n bs = Somews, n′, ord
Forall2λbt ds ⇒ ∃l phis insts j, block_partsbt = Somel, phis, insts, j ∧ mapodefs_of phis ++ insts = Someds bs dss
locals_invr x flat_mapblock_locals bs ++ ql
labels_atr b bs
lengthws ≤ fuel%nat
temps_invw_tempsw N n′ q ∧ read_blocksr fuel b lengthbs n x ws ++ rest = Somebs, n′, x + Z.of_natlengthflat_mapblock_locals bs, rest ∧ lengthconcatconcatdss ≤ lengthws%nat ∧ lengthbs ≤ lengthws%nat ∧ lengthflat_mapblock_locals bs ≤ lengthws%nat
Proof 77 steps Qed
intros w r
induction bs as | bt bs IH ; intros b n ws n′ ord x dss q ql rest fuel N T H D TI LI La F ; cbn [ blocks_words ] in H ; inversion D as [ |? ds ? dss' Dh Dt ] ; subst
–injection H as ← ← _
cbn in *
split ; exact TI |
split ; rewrite Z.add_0_r ; reflexivity | lia
–destruct Dh as l & phis & insts & j & Eb & Ed
rewrite Eb in H
cbv beta iota in H
destruct insts_wordsw 0 b n phis as ws1 n1 o1 | eqn: E1 ; | discriminate
destruct insts_wordsw 1 b n1 insts as ws2 n2 o2 | eqn: E2 ; | discriminate
destruct inst_wordsw 2 b n2 j as ws3 n3 o3 | eqn: E3 ; | discriminate
destruct blocks_wordsw b + 1 n3 bs as ws4 n4 o4 | eqn: E4 ; | discriminate
injection H as ← ← _
destruct mapo_app_ _ _ _ Ed as dp & di & → & Edp & Edi
pose proof phis_locals_ _ _ _ _ _ _ E1 as Lp
pose proof inst_locals_group_ _ _ _ _ _ _ _ E3 ltac:lia as Lj
assert Bl : block_localsbt = flat_mapinst_locals insts by unfold block_locals ; rewrite Eb ; reflexivity
cbn [ flat_map concat ] in LI , TI |- *
rewrite Bl in LI |- *
rewrite ! concat_app in TI
rewrite <- ! app_assoc in TI
rewrite <- ! app_assoc in LI
destruct La as La1 La2
rewrite ! length_app in F
the phis
{unfold stops
destruct insts_next_ _ _ _ _ _ _ _ E2 as _ & → & _ | Nx
–destruct inst_shape_ _ _ _ _ _ _ _ E3 as f & e & o & _ & G & _ & _ & Nj
rewrite app_nil_l , Nj , G
lia
assert LI0 : locals_invr x flat_mapinst_locals phis ++ flat_mapinst_locals insts ++ flat_mapblock_locals bs ++ ql by rewrite Lp ; exact LI
destruct read_group_rtw r 0 b phis n ws1 n1 o1 x dp _ _ ws2 ++ ws3 ++ ws4 ++ rest fuel N T E1 Edp TI LI0 ltac:lia S0 as TI1 & LI1 & R1 & A1 & A2 & A3
rewrite Lp in LI1 , R1
cbn [ length Z.of_nat ] in LI1 , R1
rewrite Z.add_0_r in LI1 , R1
the instructions
{unfold stops
destruct inst_shape_ _ _ _ _ _ _ _ E3 as f & e & o & _ & G & _ & _ & Nj
rewrite Nj , G
lia
destruct read_group_rtw r 1 b insts n1 ws2 n2 o2 x di _ _ ws3 ++ ws4 ++ rest fuel N T E2 Edi TI1 LI1 ltac:lia S1 as TI2 & LI2 & R2 & B1 & B2 & B3
the jump
assert LI2′ : locals_invr x + Z.of_natlengthflat_mapinst_locals insts inst_localsj ++ flat_mapblock_locals bs ++ ql by rewrite Lj ; exact LI2
destruct read_inst_rtw r 2 b n2 j ws3 n3 o3 _ [ ] _ _ ws4 ++ rest N T E3 jump_defs_ _ _ _ _ _ _ E3 TI2' LI2' as TI3 & LI3 & R3
rewrite Lj in LI3 , R3
cbn [ length Z.of_nat ] in LI3 , R3
rewrite Z.add_0_r in LI3 , R3
destruct inst_shape_ _ _ _ _ _ _ _ E3 as fj & ej & oj & _ & _ & _ & _ & Nj
assert Ne3 : 1 ≤ lengthws3%nat by destruct ws3 ; specialize Nj[ ] ; discriminate | simpl ; lia
destruct IHb + 1 n3 ws4 n4 o4 _ dss' q ql rest fuel N T E4 Dt TI3 LI3 La2 ltac:lia as TI4 & R4 & C1 & C2 & C3
split ; exact TI4 |
split
+cbn [ read_blocks length ]
rewrite La1_ _ _ _ Eb
cbv beta iota
rewrite <- ! app_assoc , R1
cbv beta iota
rewrite E0
cbv beta iota
rewrite R2
cbv beta iota
rewrite R3
cbv beta iota
rewrite R4
cbv beta iota
rewrite block_parts_inv_ _ _ _ _ Eb
rewrite length_app , Nat2Z.inj_add , Z.add_assoc
reflexivity
+rewrite ! length_app , ! concat_app , ! length_app
cbn [ length ]
split ; lia |
split ; lia
A function's body
Some is injective; unlike injection, this leaves the terms as they are.
Proof 2 steps Qed
intros A a b H
congruence
A function's return type reads back from its word.
Proof 29 steps Qed
intros ret rw H
unfold ret_word in H
destruct is_atom"void" ret eqn: Ev
–destruct is_atom"data" ret eqn: Ed
destruct app_args"tuple" 1 ret as | | | | | k1 | k2 | eqn: Et ; try pose proof class_code_range_ _ H ; unfold read_ret ; replace Z.eqbrw 0 with false by symmetry ; apply Z.eqb_neq ; lia ; replace Z.eqbrw 15 with false by symmetry ; apply Z.eqb_neq ; lia ; replace 256 ≤? rw with false by symmetry ; apply Z.leb_gt ; lia ; apply codes_round_trip ; exact H
apply some_inj in H
subst rw
pose proof class_code_range_ _ E1
pose proof class_code_range_ _ E2
apply app_args_inv in Et as → _
unfold read_ret
replace Z.eqb256 + 16 × c1 + c2 0 with false by symmetry ; apply Z.eqb_neq ; lia
replace Z.eqb256 + 16 × c1 + c2 15 with false by symmetry ; apply Z.eqb_neq ; lia
replace 256 ≤? 256 + 16 × c1 + c2 with true by symmetry ; apply Z.leb_le ; lia
replace 256 + 16 × c1 + c2 − 256 / 16 with c1 by apply Z.div_unique_ _ _ c2 ; lia
replace 256 + 16 × c1 + c2 mod 16 with c2 by apply Z.mod_unique_ _ 16 + c1 ; lia
replace c1 <? 16 with true by symmetry ; apply Z.ltb_lt ; lia
rewrite codes_round_trip_ _ _ E1 , codes_round_trip_ _ _ E2
reflexivity
The class of a parameter, as the reader checks it.
A function's parameters read back from their classes and their temporaries.
∀ ps pps
mapoparam_parts ps = Somepps
∃pks, mapoparam_class mapsnd pps = Somepks ∧ lengthpks = lengthpps ∧ mapλq ⇒ TApp"param" fstq; TApp"tmp" sndq combinepks mapfst pps = ps
Proof 28 steps Qed
induction ps as | p ps IH ; intros pps H ; cbn [ mapo ] in H
–injection H as ←
exists [ ]
auto
–destruct param_partsp as x c | eqn: Ep ; | discriminate
destruct mapoparam_parts ps as pps′ | eqn: Eps ; | discriminate
injection H as ←
destruct IHpps' eq_refl as pks & A & B & C
unfold param_parts in Ep
destruct app_args"param" 2 p as | k | d | eqn: E1 ; try discriminate
injection Ep as ← ←
exists k :: pks
cbn [ map mapo fst snd ]
unfold param_class at 1
rewrite codes_round_trip_ _ _ E4
unfold class_in
rewrite E3
rewrite A
split ; reflexivity |
split ; simpl ; lia |
cbn [ combine map fst snd ]
rewrite C
apply app_args_inv in E1 as → _
apply app_args_inv in E2 as → _
reflexivity
Two Forall2 chained.
Proof 3 steps Qed
intros X Y W P Q R xs ys zs H1
revert zs
induction H1 as | x y xs ys H H1 IH ; intros zs H2 HR ; inversion H2 ; subst ; constructor ; eauto
The labels of the blocks, numbered from b.
Proof 14 steps Qed
The locals the writer numbers are the blocks' locals.
∀ bs bps
Forall2λbt bp ⇒ block_partsbt = Somebp bs bps
flat_map
λ bp ⇒
let '_, _, insts, _ ≔ bp in
flat_map
λ t ⇒
Somex; _
⇒
x
_
⇒
[ ]
insts
bps
=
flat_mapblock_locals bs
Proof 7 steps Qed
intros bs bps H
induction H as | bt l phis insts j bs bps H1 _ IH ; reflexivity |
cbn [ flat_map ]
rewrite IH
unfold block_locals
rewrite H1
reflexivity
The module's tables a function is written and read with: symbols, strings and constants.
A function's body reads back, its names from NAMES.
Proof 129 steps Qed
intros w r ret ps bs body ord nm name lk Ms Mt Mc H
unfold body_words in H
cbv zeta in H
destruct ret_wordret as rw | eqn: Er ; | discriminate
destruct mapoparam_parts ps as pps | eqn: Eps ; | discriminate
destruct mapoblock_parts bs as bps | eqn: Ebps ; | discriminate
cbv beta iota in H
destruct Z.eqb_specn0 Z.of_natlengthpps as Hn0 | ; | discriminate
cbv beta iota in H
destruct numberconcatconcatdss m0 n0 [ ] as temps nt firsts eqn: En
cbv beta iota in H
match type of H withcontext [number nm_empty 0 [ ]]⇒destruct numberxs nm_empty 0 [ ] as lmap nb lf eqn: Elend
cbv beta iota in H
match type of H withcontext [if negbZ.eqbnb then _ else _]⇒destruct Z.eqb_specnb k as Hnb | ; | discriminateend
cbv beta iota in H
match type of H withcontext [number nm_empty 0 [ ]]⇒destruct numberxs nm_empty 0 [ ] as xmap nl xf eqn: Exend
cbv beta iota in H
match type of H withcontext [if negbZ.eqbnl then _ else _]⇒destruct Z.eqb_specnl k as Hnl | ; | discriminateend
cbv beta iota in H
match type of H withcontext [blocks_words 0 _ bs]⇒destruct blocks_wordsw′ 0 Z.of_natlengthpps bs as stream n′ ord′ | eqn: Ebend;
cbv beta iota in H
injection H as ← _ ←
apply mapo_forall2 in Ebps as Fbp
rewrite locals_mapbs bps Fbp in Ex , Hnl |- *
set L := mapλbp ⇒ let 'l, _, _, _ ≔ bp in l bps in *
set XL := flat_mapblock_locals bs in *
destruct number_fresh_ _ _ _ En0 as P0 & P0n & _ & P0f & _
assert Hf0 : firsts0 = mapfst pps by apply P0f ; rewrite length_map ; lia
subst firsts0
assert Hm0 : ∀x : term i, nm_findx m0 = Somei → 0 ≤ i ∧ nth_errormapfst pps ++ rev[ ] Z.to_nati = Somex by intros x i Hx ; rewrite app_nil_r ; auto
assert Hn0′ : n0 = Z.of_natlengthmapfst pps ++ rev[ ] by cbn [ rev ] ; rewrite app_nil_r , length_map ; lia
destruct number_specconcatconcatdss m0 n0 [ ] mapfst pps Hm0 Hn0' temps nt firsts En as nw & HF & P1 & P1n & _ & P1l & _
cbn [ rev app ] in HF
subst nw
destruct number_count_ _ _ _ El ltac:unfold L in * ; lia as _ P2
destruct number_count_ _ _ _ Ex Hnl as _ P3
set w′ := w_syms ≔ w_symsw; w_strs ≔ w_strsw; w_consts ≔ w_constsw; w_temps ≔ temps; w_labels ≔ lmap; w_locals ≔ xmap in *
assert T′ : tabs_okw' r'
{unfold w' , r'
constructor ; cbn [ w_syms w_strs w_consts w_temps w_labels w_locals r_syms r_strs r_consts r_temps r_labels r_locals ]
–exact Ms
–exact Mt
–exact Mc
assert FD : Forall2λbt ds ⇒ ∃l phis insts j, block_partsbt = Somel, phis, insts, j ∧ mapodefs_of phis ++ insts = Someds bs dss
{apply forall2_compose_ _ _ bs bps dss Fbp mapo_forall2_ _ _ Edss
intros bt l phis insts j ds E1 E2
exists l, phis, insts, j
split ; exact E1 | exact E2
{exists m0, [ ]
rewrite app_nil_r , <- Hn0 , En
split ; reflexivity |
split ; reflexivity |
split ; lia |
intros y i Hy
destruct P0y i Hy as A B
split ; exact A |
assert B′ : Z.to_nati < lengthmapfst pps%nat by apply nth_error_Some ; rewrite B ; discriminate
rewrite length_map in B'
lia
assert LI : locals_invr' 0 XL ++ [ ]
{intros k v Hk
rewrite app_nil_r in Hk
unfold r'
cbn [ r_locals ]
apply index_map_nth ; lia |
rewrite Nat2Z.id
exact Hk
{apply labels_at_mapr' bs bps Fbp 0
intros k l Hk
unfold r'
cbn [ r_labels ]
apply index_map_nth ; lia |
rewrite Nat2Z.id
exact Hk
destruct read_blocks_rtw' r' bs 0 Z.of_natlengthpps stream n' ord' 0 dss [ ] [ ] [ ] lengthstream nt T' Eb FD TI LI LA le_n_ as TIe & R & C1 & C2 & C3
rewrite app_nil_r in R
change flat_mapblock_locals bs with XL in C3 , R
assert En′ : n' = nt by destruct TIe as m & acc & _ & E2 & _ ; exact E2
pose proof mapo_length_ _ _ Ebps as Lb
rewrite length_app in P1n
destruct params_rtps pps Eps as pks & Pk & Pl & Pe
unfold read_body
cbv beta iota
rewrite ret_rt_ _ Er
cbv beta iota
replace Z.to_natZ.of_natlengthpps with lengthmapsnd pps by rewrite length_map ; lia
rewrite take_app
cbv beta iota
cbn [ fst snd ]
replace Z.of_natlengthpps <? 0 with false by symmetry ; apply Z.ltb_ge ; lia
cbv beta iota
fold param_class
rewrite Pk
cbv beta iota zeta
assert Hchk : nb <? 0 || nt <? Z.of_natlengthpps || nl <? 0 || Z.of_natlengthstream <? nb || Z.of_natlengthstream <? nt − Z.of_natlengthpps || Z.of_natlengthstream <? nl = false
{assert Hnb′ : nb = Z.of_natlengthbs by rewrite Hnb , LL ; reflexivity
rewrite length_map in P1n
repeat rewrite orb_false_iff
repeat split ; apply Z.ltb_ge ; lia
rewrite Hchk
cbv beta iota
rewrite length_app , Hnb , Hnl , P1n , ! Z.eqb_refl
cbv beta iota zeta
rewrite LL , Nat2Z.id
unfold r' in R
rewrite R
cbv beta iota
rewrite En' , P1n , Z.add_0_l , ! Z.eqb_refl
cbv beta iota
rewrite Pl , <- length_mapfst pps , firstn_app , Nat.sub_diag , firstn_O , app_nil_r , firstn_all , Pe
reflexivity
Data
A character's code is not negative.
Proof 15 steps Qed
A signed 64-bit integer reads back.
Proof 6 steps Qed
The module's tables that data items are written with invert the reader's: symbols and constants.
∀x i, nm_findx m_symidst = Somei → ZMap.findi r_symsr = Somex ∧ ∀n i, ZMap.findn m_constidst = Somei → ZMap.findi r_constsr = Somen
The bytes of a string item's characters are bytes, and give the characters back.
Proof 17 steps Qed
induction cs as | c cs IH ; intros bs E ; cbn [ mapo ] in E
–injection E as ←
split ; constructor
cbv beta iota in E
destruct mapo_ cs as bs′ | eqn: E2 ; | discriminate
injection E as ←
apply andb_true_iff in Eb as B1 B2
apply Z.ltb_lt in B1
apply term_eqb_eq in B2
destruct IHbs' eq_refl as F M
split
+constructor ; unfold byte ; pose proof char_code_nonneg_ _ Ec ; lia | exact F
A data item reads back from its words, which are not empty.
∀ t r x ws
dtabs_okt r
data_item_wordst x = Somews
ws ≠ [ ] ∧ ∀rest, read_data_itemr ws ++ rest = Somex, rest
Proof 74 steps Qed
intros t r x ws Hs Hc H
unfold data_item_words in H
destruct app_args"item" 2 x as ts | eqn: Ex
–apply app_args_inv in Ex as → L
destruct ts as | wd | v | ; try discriminate L
clear L
destruct app_args"str" 1 v as us | eqn: Ev
+apply app_args_inv in Ev as → L
destruct us as | a | ; try discriminate L
clear L
destruct a as | | | cs ; cbn in H ; try discriminate
destruct is_atom"b" wd eqn: Eb ; | discriminate
destruct mapo_ cs as bs | eqn: Ebs ; | discriminate
injection H as ←
split ; discriminate |
intros rest
cbn [ app read_data_item ]
destruct str_bytes_rtcs bs Ebs as F M
rewrite read_bytes_rtbs rest F
cbv beta iota
cbn [ fst snd ]
rewrite M
apply is_atom_inv in Eb
subst wd
reflexivity
+destruct app_args"const" 1 v as us | eqn: Ec
∗apply app_args_inv in Ec as → L
destruct us as | a | ; try discriminate L
clear L
destruct a as k | | | ; cbn in H ; try discriminate
destruct const_wordm_constidst k as z | eqn: Ez ; | discriminate
injection H as ←
split ; discriminate |
intros rest
cbn [ app read_data_item ]
rewrite codes_round_trip_ _ _ Ew
cbv beta iota
rewrite C
reflexivity
∗destruct app_args"sym" 2 v as us | eqn: Es ; | discriminate
apply app_args_inv in Es as → L
destruct us as | s | a | ; try discriminate L
clear L
destruct a as k | | | ; try discriminate
injection H as ←
split ; discriminate |
intros rest
cbn [ app read_data_item ]
apply andb_true_iff in Eo as _ Eo
rewrite codes_round_trip_ _ _ Ew
cbv beta iota
rewrite Hs_ _ Ei
cbv beta iota
rewrite read_i64_rtk rest Eo
reflexivity
–destruct app_args"zero" 1 x as us | eqn: Ez ; | discriminate
apply app_args_inv in Ez as → L
destruct us as | a | ; try discriminate L
clear L
destruct a as k | | | ; try discriminate
injection H as ←
split ; discriminate |
intros rest
cbn [ app read_data_item ]
rewrite read_i64_rtk rest Ek
reflexivity
Names
Proof 4 steps Qed
intros xs m n F Hd E x i H
destruct number_ids_ _ _ _ Hd E as _ P
destruct Px i H as P1 P2
apply index_map_nth ; assumption
The words of a list of side terms, joined.
match ts with
[ ]
⇒
Some[ ]
ts
=
Somews
∃wss, Forall2λt w ⇒ side_term_wordsids t = Somew ts wss ∧ ws = concatwss
Proof 11 steps Qed
intros ids
induction ts as | t ts IH ; intros ws H
–injection H as ←
exists [ ]
split ; constructor
–destruct side_term_wordsids t as a | eqn: Ea ; | discriminate
match type of H withcontext [match ts with _ ⇒ _ end]⇒destruct gts as b | eqn: Ebend;
injection H as ←
destruct IHb eq_refl as wss & F & →
exists a :: wss
split ; constructor ; auto | reflexivity
A side term's words are not empty.
Proof 16 steps Qed
intros ids t ws H
destruct t as n | a | f ts | ts ; cbn [ side_term_words ] in H
–destruct Nat.eqb_ _ ; discriminate |
match type of H withcontext [match ts with _ ⇒ _ end]⇒destruct gtsend;
injection H as ←
discriminate
–match type of H withcontext [match ts with _ ⇒ _ end]⇒destruct gtsend;
injection H as ←
discriminate
One joined part's length bounds each part's.
∀ wss : listlistZ w
Inw wss
lengthw ≤ lengthconcatwss%nat
Proof 6 steps Qed
induction wss as | v wss IH ; intros w H ; contradiction |
simpl
rewrite length_app
destruct H as [ <-| H ] ; lia |
specialize IHw H
lia
A side term reads back from its words, given enough fuel and a pool that inverts the ids.
∀x i, nm_findx ids = Somei → ZMap.findi pool = Somex
side_term_wordsids t = Somews
lengthws ≤ fuel%nat
read_side_termpool fuel ws ++ rest = Somet, rest
Proof 54 steps Qed
intros ids pool fuel
induction fuel as | f IH ; intros t ws rest P H L
{destruct ws ; destruct side_nonempty_ _ _ H eq_refl | simpl in L ; lia
assert Hlist : ∀ts wss, Forall2λt w ⇒ side_term_wordsids t = Somew ts wss → lengthconcatwss < Sf%nat → Forall2λx ws ⇒ ws ≠ [ ] ∧ ∀rest, read_side_termpool f ws ++ rest = Somex, rest ts wss
{intros ts wss F Lc
induction F as | x w ts wss Hx F IHF ; constructor
–split ; exact side_nonempty_ _ _ Hx |
intros r′
apply IH ; exact P | exact Hx |
simpl in Lc
rewrite length_app in Lc
lia
–apply IHF
simpl in Lc
rewrite length_app in Lc
lia
destruct t as n | a | g ts | ts ; cbn [ side_term_words ] in H
–destruct wideokn eqn: Ew ; | discriminate
injection H as ←
destruct wide_words_rtn Ew as a & b & c & E & R
rewrite E
cbn
rewrite R
reflexivity
–destruct Nat.eqb_speclengthts 0 as | Hl ; discriminate |
match type of H withcontext [match ts with _ ⇒ _ end]⇒destruct gts as w | eqn: Egend;
cbv beta iota in H
injection H as ←
destruct side_go_ _ _ Eg as wss & F & →
simpl app
cbn [ read_side_term ]
rewrite P_ _ Ei
cbv beta iota
cbn [ atom_string ]
cbv beta iota
pose proof Forall2_lengthF as FL
replace Z.of_natlengthts :: concatwss ++ rest with Z.of_natlengthts :: concatwss ++ rest by reflexivity
rewrite read_counted_rt ; | apply Hlist ; exact F | simpl in L ; lia
cbn [ fst snd ]
destruct ts ; contradiction | reflexivity
–match type of H withcontext [match ts with _ ⇒ _ end]⇒destruct gts as w | eqn: Egend;
injection H as ←
destruct side_go_ _ _ Eg as wss & F & →
simpl app
cbn [ read_side_term ]
replace Z.of_natlengthts :: concatwss ++ rest with Z.of_natlengthts :: concatwss ++ rest by reflexivity
rewrite read_counted_rt ; reflexivity | apply Hlist ; exact F | simpl in L ; lia
A counted list of side terms reads back, given enough fuel.
∀x i, nm_findx ids = Somei → ZMap.findi pool = Somex
maposide_term_wordsids ts = Somewss
lengthconcatwss ≤ fuel%nat
read_countedread_side_termpool fuel Z.of_natlengthts :: concatwss ++ rest = Somets, rest
Proof 14 steps Qed
intros ids pool ts wss fuel rest P H L
apply read_counted_rt_ _ _ rest
apply mapo_forall2 in H
induction H as | t w ts wss Ht _ IH ; constructor
–split ; exact side_nonempty_ _ _ Ht |
intros r′
apply side_term_rtids ; exact P | exact Ht |
simpl in L
rewrite length_app in L
lia
The NAMES section reads back.
Proof 41 steps Qed
intros ns ws H
unfold names_words in H
set pool := sort_uniqstr_lt String.eqb _ in H
cbv beta iota zeta in H
injection H as ←
unfold read_names
rewrite read_strings_rtpool concatrecs : read_stringsZ.of_natlengthpool :: flat_map_ pool ++ concatrecs = _
cbv beta iota
cbn [ fst snd ]
pose proof number_indexmapTAtom pool _ _ _ nodup_atomspool sort_strings_nodup_ En as P
clearbody pool
clear En
apply mapo_forall2 in Er
cbv zeta
enough G : ∀d fuel, lengthconcatrecs ≤ d%nat → lengthconcatrecs ≤ fuel%nat → read_name_recsindex_mapmapTAtom pool d fuel concatrecs = Somens by apply G ; lia
induction Er as | f w ns recs Hf _ IH ; intros d fuel Ld L ; destruct fuel ; reflexivity |
destruct maposide_term_wordsids n_tempsf as wa | eqn: Ea ; | discriminate
cbv beta iota in Hf
destruct maposide_term_wordsids n_labelsf as wb | eqn: Eb ; | discriminate
cbv beta iota in Hf
destruct maposide_term_wordsids n_localsf as wc | eqn: Ec ; | discriminate
cbv beta iota in Hf
injection Hf as ←
cbn [ concat ] in *
destruct fuel as | fuel ; lia |
repeat rewrite <- app_assoc || progress cbn [ app ]
cbn [ read_name_recs ]
rewrite side_list_rtids ; | exact P | exact Ea | repeat rewrite length_app || progress cbn [ length ] ; lia
cbv beta iota
cbn [ fst snd ]
rewrite side_list_rtids ; | exact P | exact Eb | repeat rewrite length_app || progress cbn [ length ] ; lia
cbv beta iota
cbn [ fst snd ]
rewrite side_list_rtids ; | exact P | exact Ec | repeat rewrite length_app || progress cbn [ length ] ; lia
cbv beta iota
cbn [ fst snd ]
rewrite IH by lia
destruct f ; reflexivity
Items
A symbol's kind and linkage code come back out of its word.
∀ k c
0 ≤ k < 256
k + c × 256 mod 256 = k ∧ k + c × 256 / 256 = c
Proof 8 steps Qed
intros k c H
split
–rewrite Z.mod_add by lia
apply Z.mod_small
exact H
–rewrite Z.div_add by lia
rewrite Z.div_small by exact H
reflexivity
A function's linkage code reads back.
Proof 3 steps Qed
intros s c H
apply assoc_round_trip ; | exact H
split ; simpl ; repeat constructor ; simpl ; intuition discriminate | ; constructor
An alias's linkage code reads back.
Proof 3 steps Qed
intros s c H
apply assoc_round_trip ; | exact H
split ; simpl ; repeat constructor ; simpl ; intuition discriminate | ; constructor
A data linkage of the table reads back from its code.
Proof 5 steps Qed
intros lk z Et
unfold data_linkage_codes in Et
cbn [ tassoc ] in Et
repeat destruct term_eqblk _ eqn: E ; apply term_eqb_eq in E ; subst lk ; injection Et as ← ; reflexivity | clear E
discriminate
A data object's linkage reads back from its code and word.
Proof 18 steps Qed
intros lk c e H
unfold data_linkage_word in H
assert T : let* c ≔ tassoclk data_linkage_codes in Somec, 0 = Somec, e → read_data_linkagec e = Somelk
{intros H1
destruct tassoclk data_linkage_codes as z | eqn: Et ; | discriminate
injection H1 as ← ←
apply data_table_rt
exact Et
destruct app_args"init" 2 lk as us | eqn: Ei ; | exact TH
pose proof Ei as Ei′
apply app_args_inv in Ei' as Elk L
destruct us as | wh | p | ; try discriminate L
destruct p as p | | | ; try exact TH
subst lk
destruct u32okp ; | discriminate
destruct is_atom"ctor" wh eqn: Ec ; injection H as ← ← ; apply is_atom_inv in Ec ; subst ; reflexivity |
destruct is_atom"dtor" wh eqn: Ed ; injection H as ← ← ; apply is_atom_inv in Ed ; subst ; reflexivity |
discriminate
The function names a part of NAMES adds before the rest.
match o with
Somel
⇒
Somea ++ l
None
⇒
None
A function, data object or alias reads back from its symbol's words, its DATA words and its FUNCTIONS words, before the items after it.
∀ t r it n k sw dw fw o nmx
item_symbolit = Somen, k
symbol_wordst n, k, Someit = Somesw
data_wordst it = Somedw
func_wordst it = Somefw, o, nmx
∃sid kw extra, sw = sid; kw; extra ∧ nm_findn m_stridst = Somesid ∧ ∀syms dws fws nms rest, nms = None → nmx = [ ] → read_itemsr syms dws fws nms = Somerest → read_itemsr n, kw, extra :: syms dw ++ dws fw ++ fws nconsnmx nms = Someit :: rest
Proof 114 steps Qed
intros t r it n k sw dw fw o nmx M Hi Hs Hd Hf
destruct it as | | f args | ; try discriminate
destruct args as | n′ args ; try discriminate
cbn [ item_symbol ] in Hi
unfold symbol_words in Hs
cbv beta iota in Hs
destruct String.eqb_specf "func" as [ ->| Nf ] ; | destruct String.eqb_specf "data" as [ ->| Nd ] ; | destruct String.eqb_specf "alias" as [ ->| Na ] ; | discriminate ; injection Hi as ← ←
a function
–destruct args as | lk | ret | ps | bs | ; cbn - [ sassoc func_linkage_codes ] in Hs ; try discriminate
destruct lk as | s | | ; try discriminate
cbn [ atom_string ] in Hs
destruct sassocs func_linkage_codes as c | eqn: Ec ; | discriminate
injection Hs as ←
unfold func_words in Hf
cbn - [ body_words ] in Hf
destruct ps as | | | ps ; cbv beta iota in Hf ; try discriminate
destruct bs as | | | bs ; cbv beta iota in Hf ; try discriminate
match type of Hf withcontext [body_words ret ps bs]⇒destruct body_wordsw ret ps bs as body ord nm | eqn: Ebend;
injection Hf as ← ← ←
unfold data_words in Hd
cbn in Hd
injection Hd as ←
exists sid, 0 + c × 256, 0
split ; reflexivity |
split ; reflexivity |
intros syms dws fws nms rest Hn R
destruct nms as l | ; | specialize Hneq_refl ; discriminate
cbn [ read_items ]
rewrite K1 , K2
cbn [ Z.eqb ]
rewrite func_linkage_rt_ _ Ec
cbv beta iota
cbn [ negb app ncons ]
rewrite take_app_z
cbv beta iota
cbn [ fst snd ]
rewrite read_body_rt_ _ _ _ _ _ _ _ _ _ M Eb
cbv beta iota
rewrite R
reflexivity
a data object
–destruct args as | lk | al | its | ; cbn - [ data_linkage_word ] in Hs ; try discriminate
destruct data_linkage_wordlk as c e | eqn: El ; | discriminate
cbn [ fst snd ] in Hs
injection Hs as ←
unfold func_words in Hf
cbn in Hf
injection Hf as ← ← ←
unfold data_words in Hd
cbn - [ data_item_words mapo u32ok ] in Hd
destruct al as al | | | ; cbv beta iota in Hd ; try discriminate
destruct its as | | | its ; cbv beta iota in Hd ; try discriminate
destruct u32okal ; | discriminate
destruct mapodata_item_wordst its as wss | eqn: Ew ; | discriminate
injection Hd as ←
split ; reflexivity |
split ; reflexivity |
intros syms dws fws nms rest _ R
apply mapo_forall2 in Ew
assert F : Forall2λx w ⇒ w ≠ [ ] ∧ ∀rest, read_data_itemr w ++ rest = Somex, rest its wss
{induction Ew as | x w xs ws Hx _ IH ; constructor ; exact data_item_rt_ _ _ _ D Hx | exact IH
cbn [ read_items ]
rewrite K1 , K2
cbn [ Z.eqb ]
rewrite data_linkage_rt_ _ _ El
cbv beta iota
cbn [ app ]
assert L : lengthits ≤ lengthconcatwss ++ dws%nat
{rewrite length_app
pose proof concat_length_geits wss as G
assert Forall2λ_ ws ⇒ ws ≠ [ ] its wss by eapply Forall2_impl ; | exact F ; intros ? ? ; auto
specialize GH
lia
rewrite at_least_spec
destruct Z.ltb_specZ.of_natlengthconcatwss ++ dws Z.of_natlengthits ; lia |
rewrite Nat2Z.id
cbv beta iota
cbn [ fst snd ]
replace ncons[ ] nms with nms by destruct nms ; reflexivity
rewrite R
reflexivity
an alias
–destruct args as | lk | tg | ; cbn - [ sassoc alias_linkage_codes ] in Hs ; try discriminate
destruct lk as | s | | ; cbn [ atom_string ] in Hs ; try discriminate
destruct sassocs alias_linkage_codes as c | eqn: Ec ; | discriminate
cbv beta iota in Hs
injection Hs as ←
unfold func_words in Hf
cbn in Hf
injection Hf as ← ← ←
unfold data_words in Hd
cbn in Hd
injection Hd as ←
exists sid, 2 + c × 256, tid
split ; reflexivity |
split ; reflexivity |
intros syms dws fws nms rest _ R
cbn [ read_items ]
rewrite K1 , K2
cbn [ Z.eqb ]
rewrite alias_linkage_rt_ _ Ec
cbv beta iota
destruct M as M1 & _
rewrite M1_ _ Et
cbv beta iota
cbn [ app ]
replace ncons[ ] nms with nms by destruct nms ; reflexivity
rewrite R
reflexivity
The reader's view of a symbol: its words hold the string id of its name, then its kind word and extra word.
∃sid, w = sid; sndfsty; sndy ∧ ZMap.findsid r_strsr = Somefstfsty
The items read back from their symbols, DATA words and FUNCTIONS words, before the items after them.
∀ t r items defined sd datas fs
∃ ys ,
Forall2sym_readr sd ys
∧
map
λ y ⇒
let 'n, _, _ ≔ y in
n
ys
=
map
λ d ⇒
let 'n, _, _ ≔ d in
n
defined
∧
∀ syms dws fws nms rest ,
nms = None
→
concat
map
λ x ⇒
let '_, _, n ≔ x in
n
fs
=
[ ]
→
read_itemsr syms dws fws nms = Somerest
→
read_itemsr ys ++ syms concatdatas ++ dws
concat
map
λ x ⇒
let 'ws, _, _ ≔ x in
ws
fs
++
fws
concat
map
λ x ⇒
let '_, _, n ≔ x in
n
fs
nms
=
Someitems ++ rest
Proof 56 steps Qed
intros t r items
induction items as | it items IH ; intros defined sd datas fs M Hdef Hsd Hd Hf
–cbn [ mapo ] in *
injection Hdef as ←
cbn [ mapo ] in Hsd
injection Hsd as ←
injection Hd as ←
injection Hf as ←
exists [ ]
split ; constructor |
split ; reflexivity |
intros syms dws fws nms rest _ R
cbn
destruct nms ; exact R
–cbn [ mapo ] in Hdef , Hd , Hf
destruct item_symbolit as n k | eqn: Ei ; | discriminate
cbv beta iota in Hdef
cbn [ fst snd ] in Hdef
injection Hdef as ←
cbn [ mapo ] in Hsd
destruct symbol_wordst n, k, Someit as sw | eqn: Es ; | discriminate
destruct maposymbol_wordst defs as sds | eqn: Esds ; | discriminate
injection Hsd as ←
destruct data_wordst it as dw | eqn: Edw ; | discriminate
destruct mapodata_wordst items as dws′ | eqn: Edws ; | discriminate
injection Hd as ←
destruct func_wordst it as fw o nmx | eqn: Efw ; | discriminate
destruct mapofunc_wordst items as fs′ | eqn: Efs ; | discriminate
injection Hf as ←
destruct IHdefs sds dws' fs' M eq_refl Esds eq_refl eq_refl as ys & F & Nm & Hrest
exists n, kw, extra :: ys
split ; | split ; cbn [ map ] ; rewrite Nm ; reflexivity |
+intros syms dws fws nms rest Hn R
cbn [ map concat app ]
rewrite <- ! app_assoc
replace nconsnmx ++ concatmapλx ⇒ let '_, _, n ≔ x in n fs' nms with nconsnmx nconsconcatmapλx ⇒ let '_, _, n ≔ x in n fs' nms by destruct nms ; cbn ; rewrite app_assoc | ; reflexivity
apply Hit
∗intros E
destruct nms ; discriminate |
specialize Hneq_refl
cbn in Hn
apply app_eq_nil in Hn as Hn _
exact Hn
∗apply Hrest ; | exact R
intros E
specialize HnE
cbn in Hn
apply app_eq_nil in Hn as _ Hn
exact Hn
The symbols a module names without defining read back, and the reader skips them.
∀ t r named sn
maposymbol_wordst mapλs ⇒ TAtoms, 3, @Noneterm named = Somesn
∃ ys ,
Proof 25 steps Qed
intros t r named
induction named as | s named IH ; intros sn M H
–injection H as ←
exists [ ]
split ; constructor |
split ; reflexivity
–cbn [ map mapo ] in H
destruct symbol_wordst TAtoms, 3, None as w | eqn: Ew ; | discriminate
destruct maposymbol_wordst map_ named as ws | eqn: Ews ; | discriminate
injection H as ←
destruct IHws M eq_refl as ys & F & Nm & R
unfold symbol_words in Ew
cbv beta iota in Ew
injection Ew as ←
exists TAtoms, 3, 0 :: ys
split ; | split ; cbn [ map ] ; rewrite Nm ; reflexivity |
+intros dws fws nms
rewrite <- R
reflexivity
A name first_ids numbers is at its place in the names, or was already in the map it started from.
Proof 16 steps Qed
destruct IH_ _ _ _ H as H1 | H1 H2
rewrite nm_find_add in H1
destruct name_eqbx y eqn: E ; | left ; exact H1
injection H1 as ←
apply term_eqb_eq in E
subst
right
split ; lia |
rewrite Z.sub_diag
reflexivity
–right
split ; lia |
replace Z.to_natj − i with SZ.to_natj − i + 1 by lia
exact H2
The reader's tables of a module invert the writer's: symbols, strings and constants.
Proof 40 steps Qed
intros items t H
unfold module_tables in H
cbv beta iota in H
destruct mapoitem_parts items as pss | eqn: Ep ; | discriminate
cbv beta iota zeta in H
cbv beta iota in H
match type of H withcontext [mapoatom_string ]⇒destruct mapoatom_string l as named | eqn: Enend;
cbv beta iota in H
match type of H withcontext [mapoatom_string ]⇒destruct mapoatom_string l as files | eqn: Efend;
cbv beta iota in H
match type of H withcontext [numbermapTAtom nm_empty 0 [ ]]⇒destruct numbermapTAtom xs nm_empty 0 [ ] as strids k2 F2 eqn: E2end
cbv beta iota in H
cbv beta iota in H
injection H as ←
split ; eauto |
split ; exact Ew |
split ; | split
intros x i Hx
exact number_index_ _ _ _ nodup_atoms_ sort_strings_nodup_ E2 x i Hx
The module
The SYMBOLS words read back as the reader's symbols.
∀ r sws ys rest
Forall2sym_readr sws ys
∃ trips ,
λ ws ⇒
match ws with
a :: b :: c :: ws′
⇒
Somea, b, c, ws′
_
⇒
None
Z.of_natlengthsws :: concatsws ++ rest
=
Sometrips, rest
∧
Proof 15 steps Qed
intros r sws ys rest F
exists mapλw ⇒ match w with a; b; c ⇒ a, b, c _ ⇒ 0, 0, 0 end sws
split
–rewrite <- length_mapλw ⇒ match w with a; b; c ⇒ a, b, c _ ⇒ 0, 0, 0 end sws
apply read_counted_rt
induction F as | w y sws ys sid & → & _ _ IH ; constructor ; | exact IH
split ; discriminate |
intros rest′
reflexivity
A section's payload, or the words of an empty table when the section is absent because the table is empty.
∀ c : bool a d : listZ
c = true → a = d
match if c then None else Somea with
Somex
⇒
x
None
⇒
d
=
a
Proof 1 step Qed
intros | a d H ; symmetry ; apply H | ; reflexivity
The words encode_term writes read back as the module, with NAMES exactly when the module has functions; they are also what encode_term writes without NAMES in that case, and module_words keeps them all.
∀ t ws
encode_termtrue t = Somews
∃b, read_termws = Somet, b ∧ encode_termb t = Somews ∧ module_wordsws = Somews
Proof 121 steps Qed
intros m ws H
pose proof H as H0
unfold encode_term in H
cbv beta iota in H
apply app_args_inv in Em as → _
destruct xs as | x | ; try discriminate
destruct x as | | | items ; try discriminate
destruct module_tablesitems as t | eqn: Et ; | discriminate
cbv beta iota in H
destruct maposymbol_wordst m_symst as syms | eqn: Es ; | discriminate
cbv beta iota in H
destruct mapodata_wordst items as datas | eqn: Ed ; | discriminate
cbv beta iota in H
destruct mapofunc_wordst items as fs | eqn: Ef ; | discriminate
cbv beta iota zeta in H
set R0 := mkRtab_ _ _ _ _ _ in Mt
pose proof Es as Es′
rewrite Hsyms in Es'
apply mapo_app in Es' as sd & sn & Esyms & Esd & Esn
destruct named_rtt R0 _ sn Mt Esn as yn & Fn & Nn & Hn
destruct syms_read_rtR0 sd ++ sn yd ++ yn [ ] Forall2_appFd Fn as trips & Rc & Rm
cbn [ r_strs R0 ] in Rm
set FWS := concatmapλx ⇒ let 'ws, _, _ ≔ x in ws fs in *
set FN := concatmapλx ⇒ let '_, _, n ≔ x in n fs in *
set fl := if module_checkeditems then 1 else 0 + if module_filcitems then 2 else 0 + if forallbλx ⇒ let '_, o, _ ≔ x in o fs then 4 else 0 in *
assert Hfl : 0 ≤? fl = true ∧ fl <? 8 = true
{unfold fl
destruct module_checkeditems , module_filcitems , forallb_ fs ; split ; reflexivity
assert Main : ∀b : bool nw, if b then names_wordsFN = Somenw else FN = [ ] → ws = magic; version; fl; Z.of_natlengthmsecslengthm_strst =? 0%nat lengthm_constst =? 0%nat lengthm_symst =? 0%nat lengthconcatdatas =? 0%nat lengthFWS =? 0%nat b strings_wordsm_strst Z.of_natlengthm_constst :: flat_mapwide_words m_constst Z.of_natlengthm_symst :: concatsyms concatdatas FWS nw ++ sections_wordsmsecslengthm_strst =? 0%nat lengthm_constst =? 0%nat lengthm_symst =? 0%nat lengthconcatdatas =? 0%nat lengthFWS =? 0%nat b strings_wordsm_strst Z.of_natlengthm_constst :: flat_mapwide_words m_constst Z.of_natlengthm_symst :: concatsyms concatdatas FWS nw → read_termws = SomeTApp"module" TListitems, b ∧ module_wordsws = Somews
{intros b nw Hb Hws
subst ws
pose proof msecs_speclengthm_strst =? 0%nat lengthm_constst =? 0%nat lengthm_symst =? 0%nat lengthconcatdatas =? 0%nat lengthFWS =? 0%nat b strings_wordsm_strst Z.of_natlengthm_constst :: flat_mapwide_words m_constst Z.of_natlengthm_symst :: concatsyms concatdatas FWS nw as MS
cbv zeta in MS
set ss := msecs_ _ _ _ _ _ _ _ _ _ _ _ in *
destruct MS as Sid & Sf & S1 & S2 & S3 & S4 & S5 & S6
split
–unfold read_term
cbn [ app ]
rewrite ! Z.eqb_refl
destruct Hfl as F1 F2
rewrite F1 , F2
cbn [ andb negb ]
rewrite read_sections_rt by lia
cbv beta iota
rewrite Z.eqb_refl , Sid
cbn [ andb negb ]
rewrite S1 , S2 , S3 , S4 , S5 , S6
rewrite or_empty_eq_ strings_wordsm_strst 0 by intros E ; apply Nat.eqb_eq , length_zero_iff_nil in E ; rewrite E ; reflexivity
rewrite <- app_nil_rstrings_wordsm_strst , read_strings_rt
cbv beta iota
rewrite or_empty_eq_ Z.of_natlengthm_constst :: flat_mapwide_words m_constst 0 by intros E ; apply Nat.eqb_eq , length_zero_iff_nil in E ; rewrite E ; reflexivity
rewrite <- app_nil_rZ.of_natlengthm_constst :: flat_mapwide_words m_constst
rewrite read_wides_rt_ _ Wk
cbv beta iota
rewrite or_empty_eq_ Z.of_natlengthm_symst :: concatsyms 0 by intros E ; apply Nat.eqb_eq , length_zero_iff_nil in E ; rewrite E in Es ; injection Es as ← ; rewrite E ; reflexivity
rewrite <- mapo_length_ _ _ Es , Esyms
rewrite <- app_nil_rZ.of_natlengthsd ++ sn :: concatsd ++ sn , Rc
cbv beta iota
cbn [ fst snd ]
rewrite Rm
cbv beta iota
rewrite map_app , Nd , Nn , <- map_app , <- Hsyms
rewrite or_empty_eq_ concatdatas [ ] by intros E ; apply Nat.eqb_eq , length_zero_iff_nil in E ; exact E
rewrite or_empty_eq_ FWS [ ] by intros E ; apply Nat.eqb_eq , length_zero_iff_nil in E ; exact E
destruct b
+rewrite read_names_rt_ _ Hb
cbv beta iota
pose proof Hitemsyn [ ] [ ] Some[ ] [ ] ltac:discriminate ltac:rewrite Hn ; reflexivity as RI
cbn [ ncons ] in RI
rewrite ! app_nil_r in RI
unfold R0 in RI
rewrite RI
reflexivity
+cbv beta iota
pose proof Hitemsyn [ ] [ ] None [ ] ltac:intros _ ; exact Hb ltac:rewrite Hn ; reflexivity as RI
cbn [ ncons ] in RI
rewrite ! app_nil_r in RI
unfold R0 in RI
rewrite RI
reflexivity
destruct Nat.eqb_speclengthFN 0 as Hz | Hz
–replace lengthFN =? 0%nat with true in H by symmetry ; apply Nat.eqb_eq ; exact Hz
cbn [ andb negb ] in H
cbv beta iota in H
injection H as Hws
exists false
destruct Mainfalse [ ] ltac:apply length_zero_iff_nil ; exact Hz eq_symHws as R W
split ; exact R |
split ; | exact W
unfold encode_term
cbn [ app_args String.eqb Ascii.eqb Bool.eqb andb length Nat.eqb ]
cbv beta iota
rewrite Et
cbv beta iota
rewrite Es
cbv beta iota
rewrite Ed
cbv beta iota
rewrite Ef
cbv beta iota zeta
cbn [ andb ]
cbv beta iota
rewrite <- Hws
reflexivity
–replace lengthFN =? 0%nat with false in H by symmetry ; apply Nat.eqb_neq ; exact Hz
cbn [ andb negb ] in H
destruct names_wordsFN as nw | eqn: Enw ; | discriminate
cbv beta iota in H
injection H as Hws
exists true
destruct Maintrue nw eq_refl ltac:rewrite <- Hws ; reflexivity as R W
auto