diff options
| author | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 20:27:07 +0200 |
|---|---|---|
| committer | Yann Herklotz <git@yannherklotz.com> | 2020-08-04 20:27:07 +0200 |
| commit | 4b433258deffec9207451fb30e4103462c704781 (patch) | |
| tree | 3fcda62ea8eb60ffff50fb1733310e500a7d053d | |
| parent | b1aff2a1a6d45a253d87c01b4c967376491597dc (diff) | |
| download | vericert-kvx-4b433258deffec9207451fb30e4103462c704781.tar.gz vericert-kvx-4b433258deffec9207451fb30e4103462c704781.zip | |
Remove last admits from istore
| -rw-r--r-- | src/translation/HTLgenproof.v | 5 |
1 files changed, 3 insertions, 2 deletions
diff --git a/src/translation/HTLgenproof.v b/src/translation/HTLgenproof.v index 5aa6628..7def187 100644 --- a/src/translation/HTLgenproof.v +++ b/src/translation/HTLgenproof.v @@ -1596,7 +1596,8 @@ Section CORRECTNESS. assert (Integers.Ptrofs.repr 0 = Integers.Ptrofs.zero) as ZERO by reflexivity. erewrite Mem.load_store_other with (m1 := m). 2: { exact H1. } - 2: { right. right. simpl. + 2: { rewrite HeqOFFSET in *. simplify_val. + right. right. simpl. rewrite ZERO. rewrite Integers.Ptrofs.add_zero_l. rewrite Integers.Ptrofs.unsigned_repr; crush; try lia. @@ -2143,7 +2144,7 @@ Section CORRECTNESS. exact (Values.Vint (Int.repr 0)). exact tt. exact (Values.Vint (Int.repr 0)). - Admitted. + Qed. Hint Resolve transl_istore_correct : htlproof. Lemma transl_icond_correct: |