diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-24 09:58:50 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-24 09:58:50 +0200 |
| commit | ed989b948e34626d0e12b906abec1d17912da804 (patch) | |
| tree | 8a3d23e294a1dd434d01befedc916f4ac4c6b162 /aarch64/Asmgenproof.v | |
| parent | 8289c850a9e24406e8ce34cf3a0d53840ce02903 (diff) | |
| download | compcert-kvx-ed989b948e34626d0e12b906abec1d17912da804.tar.gz compcert-kvx-ed989b948e34626d0e12b906abec1d17912da804.zip | |
Complete bblock_size_aux_pos
Steal use of list_length_z_aux_increase from exec_header_simulation.
Diffstat (limited to 'aarch64/Asmgenproof.v')
| -rw-r--r-- | aarch64/Asmgenproof.v | 7 |
1 files changed, 6 insertions, 1 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 4a1f4de4..13aecf4d 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -494,7 +494,12 @@ Proof. Qed. Lemma bblock_size_aux_pos bb: list_length_z (body bb) + Z.of_nat (length_opt (exit bb)) >= 1. -Admitted. (* NB: from bblock_non_empty *) +Proof. + destruct (bblock_non_empty bb), (body bb) as [|hd tl], (exit bb); simpl; + try (congruence || omega); + unfold list_length_z; simpl; + generalize (list_length_z_aux_increase _ tl 1); omega. +Qed. Lemma bblock_size_aux bb: size bb = list_length_z (header bb) + list_length_z (body bb) + Z.of_nat (length_opt (exit bb)). Admitted. |