diff options
| author | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-15 14:26:26 +0200 |
|---|---|---|
| committer | Justus Fasse <justus.fasse@etu.univ-grenoble-alpes.fr> | 2020-07-15 14:26:57 +0200 |
| commit | 502ae351b0f65601e5f023bb37fd4db7929e1075 (patch) | |
| tree | 774f18af9c6a585d7281ae1c5d1a1e1fbffd7900 /aarch64 | |
| parent | 2274a38371299cdf65f92bc88dfd78af99dd796a (diff) | |
| download | compcert-kvx-502ae351b0f65601e5f023bb37fd4db7929e1075.tar.gz compcert-kvx-502ae351b0f65601e5f023bb37fd4db7929e1075.zip | |
Add lemma showing 1 <= Ptrofs.max_unsigned
Diffstat (limited to 'aarch64')
| -rw-r--r-- | aarch64/Asmgenproof.v | 10 |
1 files changed, 8 insertions, 2 deletions
diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v index 9f65dbc0..10586f0e 100644 --- a/aarch64/Asmgenproof.v +++ b/aarch64/Asmgenproof.v @@ -171,6 +171,13 @@ Proof. rewrite H; omega. Qed. +Lemma one_le_max_unsigned: + 1 <= Ptrofs.max_unsigned. +Proof. + unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize; + unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega. +Qed. + Lemma match_internal_exec_label: forall n rs1 m1 rs2 m2 l fb f tf, Genv.find_funct_ptr ge fb = Some (Internal f) -> @@ -193,8 +200,7 @@ Proof. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; trivial. + split. * apply Z.le_0_1. - * unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize; - unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega. + * apply one_le_max_unsigned. + split. * apply Z.ge_le; assumption. * rewrite <- functions_bound_max_pos; eauto; omega. |