diff options
| author | Brian Campbell | 2018-11-19 13:17:17 +0000 |
|---|---|---|
| committer | Brian Campbell | 2018-11-19 13:21:42 +0000 |
| commit | 6e4cd778ab07aff67497d320e2e345ecdbace217 (patch) | |
| tree | 6ef411a208d1c7fbd2c69416a458afc74d8599a9 | |
| parent | 626c68dad5ea79da7776b4628e5ae22ca742669e (diff) | |
A few more constraint lemmas for aarch64
| -rw-r--r-- | aarch64/aarch64_extras.v | 33 |
1 files changed, 33 insertions, 0 deletions
diff --git a/aarch64/aarch64_extras.v b/aarch64/aarch64_extras.v index e095f4a2..7b89e454 100644 --- a/aarch64/aarch64_extras.v +++ b/aarch64/aarch64_extras.v @@ -214,3 +214,36 @@ intros [H|[H|[H|[H|[H|[]]]]]] H'; subst; reflexivity. Qed. Hint Resolve simdfp_register_lemma2 : sail. + +Lemma atomicops_st_lemma {datasize} : + 8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False -> + 8 * (datasize ÷ 8) > 0. +intros [H|[H|[H|[H|[H|[]]]]]]; subst; +reflexivity. +Qed. +Hint Resolve atomicops_st_lemma : sail. + +Lemma atomicops_cas_pair_lemma1 {datasize x0} : + 8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False -> + x0 = 2 * datasize ÷ 8 -> + 64 >= 0 /\ 8 * x0 >= 0. +intros [H|[H|[H|[H|[H|[]]]]]]; subst; +intro H; compute in H; subst; omega. +Qed. + +Lemma atomicops_cas_pair_lemma2 {datasize} : + 8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False -> + 2 * datasize = 8 * (2 * datasize ÷ 8). +intros [H|[H|[H|[H|[H|[]]]]]]; subst; reflexivity. +Qed. + +Lemma atomicops_cas_pair_lemma3 {datasize x0} : + 8 = datasize \/ 16 = datasize \/ 32 = datasize \/ 64 = datasize \/ 128 = datasize \/ False -> + x0 = 2 * datasize ÷ 8 -> + 2 * datasize = 8 * x0. +intros [H|[H|[H|[H|[H|[]]]]]]; subst; +intro H; compute in H; subst; omega. +Qed. + +Hint Resolve atomicops_cas_pair_lemma1 atomicops_cas_pair_lemma2 atomicops_cas_pair_lemma3 : sail. + |