diff options
Diffstat (limited to 'common/Memory.v')
| -rw-r--r-- | common/Memory.v | 54 |
1 files changed, 27 insertions, 27 deletions
diff --git a/common/Memory.v b/common/Memory.v index 764fdc26..8bb69c02 100644 --- a/common/Memory.v +++ b/common/Memory.v @@ -912,7 +912,7 @@ Proof. rewrite Ptrofs.add_unsigned. replace (Ptrofs.unsigned (Ptrofs.of_int (Int.repr 4))) with (Int.unsigned (Int.repr 4)) by (symmetry; apply Ptrofs.agree32_of_int; auto). - change (Int.unsigned (Int.repr 4)) with 4. + change (Int.unsigned (Int.repr 4)) with 4. apply Ptrofs.unsigned_repr. exploit (Zdivide_interval (Ptrofs.unsigned i) Ptrofs.modulus 8). omega. apply Ptrofs.unsigned_range. auto. @@ -934,7 +934,7 @@ Proof. exploit load_int64_split; eauto. intros (v1 & v2 & L1 & L2 & EQ). unfold Val.add; rewrite H0. assert (NV: Ptrofs.unsigned (Ptrofs.add i (Ptrofs.of_int (Int.repr 4))) = Ptrofs.unsigned i + 4). - { apply addressing_int64_split; auto. + { apply addressing_int64_split; auto. exploit load_valid_access. eexact H2. intros [P Q]. auto. } exists v1, v2. Opaque Ptrofs.repr. @@ -1519,7 +1519,7 @@ Qed. Theorem loadbytes_storebytes_same: loadbytes m2 b ofs (Z_of_nat (length bytes)) = Some bytes. Proof. - intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. + intros. assert (STORE2:=STORE). unfold storebytes in STORE2. unfold loadbytes. destruct (range_perm_dec m1 b ofs (ofs + Z_of_nat (length bytes)) Cur Writable); try discriminate. rewrite pred_dec_true. @@ -1829,7 +1829,7 @@ Proof. intros. exploit load_result; eauto. intro. rewrite H0. injection ALLOC; intros. rewrite <- H2; simpl. rewrite <- H1. rewrite PMap.gss. destruct (size_chunk_nat_pos chunk) as [n E]. rewrite E. simpl. - rewrite ZMap.gi. apply decode_val_undef. + rewrite ZMap.gi. apply decode_val_undef. Qed. Theorem load_alloc_same': @@ -2930,7 +2930,7 @@ Proof. rewrite (nextblock_store _ _ _ _ _ _ H0). auto. eapply store_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. - intros. eauto using perm_store_2. + intros. eauto using perm_store_2. Qed. Theorem storev_extends: @@ -2982,7 +2982,7 @@ Proof. rewrite (nextblock_storebytes _ _ _ _ _ H0). auto. eapply storebytes_outside_inj; eauto. unfold inject_id; intros. inv H2. eapply H1; eauto. omega. - intros. eauto using perm_storebytes_2. + intros. eauto using perm_storebytes_2. Qed. Theorem alloc_extends: @@ -3017,7 +3017,7 @@ Proof. intros. eapply perm_alloc_inv in H; eauto. generalize (perm_alloc_inv _ _ _ _ _ H0 b0 ofs Max Nonempty); intros PERM. destruct (eq_block b0 b). - subst b0. + subst b0. assert (EITHER: lo1 <= ofs < hi1 \/ ~(lo1 <= ofs < hi1)) by omega. destruct EITHER. left. apply perm_implies with Freeable; auto with mem. eapply perm_alloc_2; eauto. @@ -3034,7 +3034,7 @@ Proof. intros. inv H. constructor. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_left_inj; eauto. - intros. exploit mext_perm_inv0; eauto. intros [A|A]. + intros. exploit mext_perm_inv0; eauto. intros [A|A]. eapply perm_free_inv in A; eauto. destruct A as [[A B]|A]; auto. subst b0. right; eapply perm_free_2; eauto. intuition eauto using perm_free_3. @@ -3051,7 +3051,7 @@ Proof. rewrite (nextblock_free _ _ _ _ _ H0). auto. eapply free_right_inj; eauto. unfold inject_id; intros. inv H. eapply H1; eauto. omega. - intros. eauto using perm_free_3. + intros. eauto using perm_free_3. Qed. Theorem free_parallel_extends: @@ -3498,7 +3498,7 @@ Proof. intros. eapply mi_representable; try eassumption. destruct H4; eauto with mem. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_store_2. + intros. exploit mi_perm_inv0; eauto using perm_store_2. intuition eauto using perm_store_1, perm_store_2. Qed. @@ -3523,7 +3523,7 @@ Proof. intros. eapply mi_representable; try eassumption. destruct H3; eauto with mem. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_store_2. + intros. exploit mi_perm_inv0; eauto using perm_store_2. intuition eauto using perm_store_1, perm_store_2. Qed. @@ -3594,7 +3594,7 @@ Proof. intros. eapply mi_representable0; eauto. destruct H4; eauto using perm_storebytes_2. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. @@ -3668,7 +3668,7 @@ Proof. intros. eapply mi_representable0; eauto. destruct H3; eauto using perm_storebytes_2. (* perm inv *) - intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. + intros. exploit mi_perm_inv0; eauto using perm_storebytes_2. intuition eauto using perm_storebytes_1, perm_storebytes_2. Qed. @@ -3694,7 +3694,7 @@ Proof. auto. (* perm inv *) intros. eapply perm_alloc_inv in H2; eauto. destruct (eq_block b0 b2). - subst b0. eelim fresh_block_alloc; eauto. + subst b0. eelim fresh_block_alloc; eauto. eapply mi_perm_inv0; eauto. Qed. @@ -3741,7 +3741,7 @@ Proof. destruct H4; eauto using perm_alloc_4. (* perm inv *) intros. unfold f' in H3; destruct (eq_block b0 b1); try discriminate. - exploit mi_perm_inv0; eauto. + exploit mi_perm_inv0; eauto. intuition eauto using perm_alloc_1, perm_alloc_4. (* incr *) split. auto. @@ -3892,7 +3892,7 @@ Proof. (* perm inv *) intros. exploit mi_perm_inv0; eauto. intuition eauto using perm_free_3. eapply perm_free_inv in H4; eauto. destruct H4 as [[A B] | A]; auto. - subst b1. right; eapply perm_free_2; eauto. + subst b1. right; eapply perm_free_2; eauto. Qed. Lemma free_list_left_inject: @@ -4080,7 +4080,7 @@ Proof. destruct H0; eauto using perm_inj. rewrite H. omega. (* perm inv *) - intros. + intros. destruct (f b1) as [[b' delta'] |] eqn:?; try discriminate. destruct (f' b') as [[b'' delta''] |] eqn:?; try discriminate. inversion H; clear H; subst b'' delta. @@ -4163,7 +4163,7 @@ Proof. eapply mem_inj_compose; eauto. apply extensionality; intros. unfold compose_meminj, inject_id. auto. (* perm inv *) - exploit mext_perm_inv1; eauto. intros [A|A]. + exploit mext_perm_inv1; eauto. intros [A|A]. eapply mext_perm_inv0; eauto. right; red; intros; elim A. eapply perm_extends; eauto. Qed. @@ -4305,7 +4305,7 @@ Lemma perm_unchanged_on: unchanged_on m m' -> P b ofs -> perm m b ofs k p -> perm m' b ofs k p. Proof. - intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. + intros. destruct H. apply unchanged_on_perm0; auto. eapply perm_valid_block; eauto. Qed. Lemma perm_unchanged_on_2: @@ -4324,7 +4324,7 @@ Proof. - intros. transitivity (perm m2 b ofs k p); apply unchanged_on_perm; auto. eapply valid_block_unchanged_on; eauto. - intros. transitivity (ZMap.get ofs (mem_contents m2)#b); apply unchanged_on_contents; auto. - eapply perm_unchanged_on; eauto. + eapply perm_unchanged_on; eauto. Qed. Lemma loadbytes_unchanged_on_1: @@ -4462,13 +4462,13 @@ Proof. - rewrite (nextblock_drop _ _ _ _ _ _ H). apply Ple_refl. - split; intros. eapply perm_drop_3; eauto. destruct (eq_block b0 b); auto. - subst b0. + subst b0. assert (~ (lo <= ofs < hi)). { red; intros; eelim H0; eauto. } right; omega. - eapply perm_drop_4; eauto. -- unfold drop_perm in H. + eapply perm_drop_4; eauto. +- unfold drop_perm in H. destruct (range_perm_dec m b lo hi Cur Freeable); inv H; simpl. auto. -Qed. +Qed. End UNCHANGED_ON. @@ -4480,9 +4480,9 @@ Lemma unchanged_on_implies: Proof. intros. destruct H. constructor; intros. - auto. -- apply unchanged_on_perm0; auto. -- apply unchanged_on_contents0; auto. - apply H0; auto. eapply perm_valid_block; eauto. +- apply unchanged_on_perm0; auto. +- apply unchanged_on_contents0; auto. + apply H0; auto. eapply perm_valid_block; eauto. Qed. End Mem. |