diff options
| author | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-17 17:27:50 +0200 |
|---|---|---|
| committer | Sylvain Boulmé <sylvain.boulme@univ-grenoble-alpes.fr> | 2020-10-17 17:27:50 +0200 |
| commit | eb61466b4b4ba3fbaf1832fcc59a0a036babff1b (patch) | |
| tree | 913f9b2c4345a35e2689eca86e2d9380093c9e68 /kvx | |
| parent | 41a97a2d5eace2a0b113d7da590df69f1cc0d763 (diff) | |
| download | compcert-kvx-eb61466b4b4ba3fbaf1832fcc59a0a036babff1b.tar.gz compcert-kvx-eb61466b4b4ba3fbaf1832fcc59a0a036babff1b.zip | |
update op_valid_pointer_eq proof on the KVX
Diffstat (limited to 'kvx')
| -rw-r--r-- | kvx/Op.v | 26 |
1 files changed, 4 insertions, 22 deletions
@@ -1238,24 +1238,6 @@ Proof. unfold Val.cmpu_bool, Val.cmplu_bool; rewrite SF; reflexivity. Qed. -Lemma Val_cmpu_bool_valid_pointer_eq m1 m2 c v1 v2: - (forall (b : block) (z : Z), Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> - Val.cmpu_bool( Mem.valid_pointer m1) c v1 v2 = Val.cmpu_bool (Mem.valid_pointer m2) c v1 v2. -Proof. - intros MEM; unfold Val.cmpu_bool; destruct v1; try congruence; - destruct v2; try congruence; - rewrite !MEM; auto. -Qed. - -Lemma Val_cmplu_bool_valid_pointer_eq m1 m2 c v1 v2: - (forall (b : block) (z : Z), Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> - Val.cmplu_bool( Mem.valid_pointer m1) c v1 v2 = Val.cmplu_bool (Mem.valid_pointer m2) c v1 v2. -Proof. - intros MEM; unfold Val.cmplu_bool; destruct v1; try congruence; - destruct v2; try congruence; - rewrite !MEM; auto. -Qed. - Lemma op_valid_pointer_eq: forall (F V: Type) (ge: Genv.t F V) sp op args m1 m2, (forall b z, Mem.valid_pointer m1 b z = Mem.valid_pointer m2 b z) -> @@ -1264,16 +1246,16 @@ Proof. intros until m2. destruct op; simpl; try congruence. - intros MEM; destruct cond; simpl; try congruence; repeat (destruct args; simpl; try congruence); - erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto. + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - intros MEM; destruct c0; simpl; try congruence; repeat (destruct args; simpl; try congruence); - erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto. + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - intros MEM; destruct c0; simpl; try congruence; repeat (destruct args; simpl; try congruence); - erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto. + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. - intros MEM; destruct c0; simpl; try congruence; repeat (destruct args; simpl; try congruence); - erewrite Val_cmpu_bool_valid_pointer_eq || erewrite Val_cmplu_bool_valid_pointer_eq; eauto. + erewrite cmpu_bool_valid_pointer_eq || erewrite cmplu_bool_valid_pointer_eq; eauto. Qed. |