Val_cmp* -> Val.mxcmp*

1 files changed, 6 insertions, 60 deletions

diff --git a/aarch64/Asm.v b/aarch64/Asm.v
index 30bac2a4..dc1f025f 100644
--- a/aarch64/Asm.v
+++ b/aarch64/Asm.v
@@ -416,60 +416,6 @@ Definition outcome := option state.
 Definition Next rs m: outcome := Some (State rs m).
 Definition Stuck: outcome := None.
 
-
-(* a few lemma on comparisons of unsigned (e.g. pointers)
-
-TODO: these lemma are a copy/paste of kvx/Asmvliw.v (sharing to improve!)
-*)
-
-Definition Val_cmpu_bool cmp v1 v2: option bool :=
-  Val.cmpu_bool (fun _ _ => true) cmp v1 v2.
-
-Lemma Val_cmpu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmpu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmpu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmpu cmp v1 v2 := Val.of_optbool (Val_cmpu_bool cmp v1 v2).
-
-Lemma Val_cmpu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.cmpu (Mem.valid_pointer m) cmp v1 v2)
-               (Val_cmpu cmp v1 v2).
-Proof.
-  unfold Val.cmpu, Val_cmpu.
-  remember (Val.cmpu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob; simpl.
-  - erewrite Val_cmpu_bool_correct; eauto.
-    econstructor.
-  - econstructor.
-Qed.
-
-Definition Val_cmplu_bool (cmp: comparison) (v1 v2: val)
- := (Val.cmplu_bool (fun _ _ => true) cmp v1 v2).
-
-Lemma Val_cmplu_bool_correct (m:mem) (cmp: comparison) (v1 v2: val) b:
-   (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) = Some b
-   -> (Val_cmplu_bool cmp v1 v2) = Some b.
-Proof.
-  intros; eapply Val.cmplu_bool_lessdef; (econstructor 1 || eauto).
-Qed.
-
-Definition Val_cmplu cmp v1 v2 := Val.of_optbool (Val_cmplu_bool cmp v1 v2).
-
-Lemma Val_cmplu_correct (m:mem) (cmp: comparison) (v1 v2: val):
-   Val.lessdef (Val.maketotal (Val.cmplu (Mem.valid_pointer m) cmp v1 v2))
-               (Val_cmplu cmp v1 v2).
-Proof.
-  unfold Val.cmplu, Val_cmplu.
-  remember (Val.cmplu_bool (Mem.valid_pointer m) cmp v1 v2) as ob.
-  destruct ob as [b|]; simpl.
-  - erewrite Val_cmplu_bool_correct; eauto.
-    simpl. econstructor.
-  - econstructor.
-Qed.
-
 (** Testing a condition *)
 
 Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
@@ -540,8 +486,8 @@ Definition eval_testcond (c: testcond) (rs: regset) : option bool :=
 
 Definition eval_testzero (sz: isize) (v: val): option bool :=
   match sz with
-  | W => Val_cmpu_bool Ceq v (Vint Int.zero)
-  | X => Val_cmplu_bool Ceq v (Vlong Int64.zero)
+  | W => Val.mxcmpu_bool Ceq v (Vint Int.zero)
+  | X => Val.mxcmplu_bool Ceq v (Vlong Int64.zero)
   end.
 
 (** Integer "bit is set?" test *)
@@ -557,14 +503,14 @@ Definition eval_testbit (sz: isize) (v: val) (n: int): option bool :=
 
 Definition compare_int (rs: regset) (v1 v2: val) :=
   rs#CN <- (Val.negative (Val.sub v1 v2))
-    #CZ <- (Val_cmpu Ceq v1 v2)
-    #CC <- (Val_cmpu Cge v1 v2)
+    #CZ <- (Val.mxcmpu Ceq v1 v2)
+    #CC <- (Val.mxcmpu Cge v1 v2)
     #CV <- (Val.sub_overflow v1 v2).
 
 Definition compare_long (rs: regset) (v1 v2: val) :=
   rs#CN <- (Val.negativel (Val.subl v1 v2))
-    #CZ <- (Val_cmplu Ceq v1 v2)
-    #CC <- (Val_cmplu Cge v1 v2)
+    #CZ <- (Val.mxcmplu Ceq v1 v2)
+    #CC <- (Val.mxcmplu Cge v1 v2)
     #CV <- (Val.subl_overflow v1 v2).
 
 (** Semantics of [fcmp] instructions: