Fix proofs for ptr64vericert-kvx

5 files changed, 13 insertions, 64 deletions

diff --git a/verilog/Asmgenproof1.v b/verilog/Asmgenproof1.v
index 42ab8375..f37b85b4 100644
--- a/verilog/Asmgenproof1.v
+++ b/verilog/Asmgenproof1.v
@@ -728,9 +728,9 @@ Lemma transl_cond_int64s_correct:
 Proof.
   intros. destruct cmp; simpl. 
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+  split; intros; Simpl. destruct (rs###r1); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
-  split; intros; Simpl. destruct (rs###r1); auto. destruct (rs###r2); auto.
+  split; intros; Simpl. destruct (rs###r1); auto.
 - econstructor; split. apply exec_straight_one; [simpl; eauto|auto].
   split; intros; Simpl.
 - econstructor; split.
diff --git a/verilog/ConstpropOpproof.v b/verilog/ConstpropOpproof.v
index 74dc4a05..efeec6f6 100644
--- a/verilog/ConstpropOpproof.v
+++ b/verilog/ConstpropOpproof.v
@@ -17,6 +17,8 @@ Require Import Integers Floats Values Memory Globalenvs Events.
 Require Import Op Registers RTL ValueDomain.
 Require Import ConstpropOp.
 
+#[local] Opaque Archi.ptr64.
+
 Section STRENGTH_REDUCTION.
 
 Variable bc: block_classification.
@@ -201,7 +203,8 @@ Proof.
   predSpec Int.eq Int.eq_spec n Int.zero; intros.
   subst. exists (e#r); split; auto.
   destruct (e#r); simpl; auto; rewrite ?Int.add_zero, ?Ptrofs.add_zero; auto.
-  destruct Archi.ptr64; auto.
+  destruct Archi.ptr64 eqn:?; auto.
+  exists (Val.add e#r (Vint n)); split; auto.
   exists (Val.add e#r (Vint n)); split; auto.
 Qed.
 
@@ -406,7 +409,7 @@ Proof.
   predSpec Int64.eq Int64.eq_spec n Int64.zero; intros.
   subst. exists (e#r); split; auto.
   destruct (e#r); simpl; auto; rewrite ? Int64.add_zero, ? Ptrofs.add_zero; auto.
-  destruct Archi.ptr64; auto.
+  destruct Archi.ptr64 eqn:?; auto;
   exists (Val.addl e#r (Vlong n)); split; auto.
 Qed.
 
diff --git a/verilog/Op.v b/verilog/Op.v
index 9f94828f..87986f78 100644
--- a/verilog/Op.v
+++ b/verilog/Op.v
@@ -778,7 +778,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   (* addrsymbol *)
   - unfold Genv.symbol_address. destruct (Genv.find_symbol genv id)...
   (* addrstack *)
-  - destruct sp... apply Val.Vptr_has_type.
+  - destruct sp...
   (* castsigned *)
   - destruct v0...
   - destruct v0...
@@ -790,6 +790,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - unfold Val.sub. destruct v0; destruct v1... 
     unfold Val.has_type; destruct Archi.ptr64...
     destruct Archi.ptr64... destruct (eq_block b b0)...
+    destruct (eq_block b b0)...
   (* mul, mulhs, mulhu *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
@@ -839,9 +840,7 @@ Proof with (try exact I; try reflexivity; auto using Val.Vptr_has_type).
   - apply type_addl.
   (* negl, subl *)
   - destruct v0...
-  - unfold Val.subl. destruct v0; destruct v1... 
-    unfold Val.has_type; destruct Archi.ptr64...
-    destruct Archi.ptr64... destruct (eq_block b b0)...
+  - unfold Val.subl. destruct v0; destruct v1...
   (* mull, mullhs, mullhu *)
   - destruct v0; destruct v1...
   - destruct v0; destruct v1...
diff --git a/verilog/SelectLongproof.v b/verilog/SelectLongproof.v
index 0fc578bf..cd88911d 100644
--- a/verilog/SelectLongproof.v
+++ b/verilog/SelectLongproof.v
@@ -124,15 +124,12 @@ Proof.
   predSpec Int64.eq Int64.eq_spec n Int64.zero.
   subst. exists x; split; auto.
   destruct x; simpl; rewrite ?Int64.add_zero, ?Ptrofs.add_zero; auto.
-  destruct Archi.ptr64; auto.
   destruct (addlimm_match a); InvEval.
 - econstructor; split. apply eval_longconst. rewrite Int64.add_commut; auto.
 - econstructor; split. EvalOp. simpl; eauto. 
-  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto. 
-  destruct Archi.ptr64; auto. rewrite Ptrofs.add_commut; auto. 
+  unfold Genv.symbol_address. destruct (Genv.find_symbol ge s); simpl; auto.
 - econstructor; split. EvalOp. simpl; eauto. 
-  destruct sp; simpl; auto. destruct Archi.ptr64; auto. 
-  rewrite Ptrofs.add_assoc, (Ptrofs.add_commut m0). auto. 
+  destruct sp; simpl; auto.
 - subst x. rewrite Val.addl_assoc. rewrite Int64.add_commut. TrivialExists.
 - TrivialExists.
 Qed.
@@ -167,18 +164,10 @@ Proof.
     EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
     rewrite Val.addl_commut. destruct sp; simpl; auto.
     destruct v1; simpl; auto.
-    destruct Archi.ptr64 eqn:SF; auto. 
-    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. 
-    rewrite (Ptrofs.add_commut (Ptrofs.of_int64 n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst. econstructor; split.
     EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
     destruct sp; simpl; auto.
     destruct v1; simpl; auto.
-    destruct Archi.ptr64 eqn:SF; auto. 
-    apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
-    rewrite Ptrofs.add_commut. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst.
     replace (Val.addl (Val.addl v1 (Vlong n1)) y)
        with (Val.addl (Val.addl v1 y) (Vlong n1)).
@@ -347,7 +336,6 @@ Proof.
   subst x. destruct v1; simpl; auto.
   simpl in B2; inv B2. simpl in B3; inv B3. rewrite Int64.mul_add_distr_l.
   rewrite (Int64.mul_commut n). auto.
-  destruct Archi.ptr64; simpl; auto.
 - apply eval_mullimm_base; auto.
 Qed.
 
diff --git a/verilog/SelectOpproof.v b/verilog/SelectOpproof.v
index f450fe6c..789e38dc 100644
--- a/verilog/SelectOpproof.v
+++ b/verilog/SelectOpproof.v
@@ -172,7 +172,6 @@ Proof.
     destruct Archi.ptr64 eqn:SF; auto. 
     apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. 
     rewrite (Ptrofs.add_commut (Ptrofs.of_int n1)), Ptrofs.add_assoc. f_equal. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst. econstructor; split.
     EvalOp. constructor. EvalOp. simpl; eauto. constructor. eauto. constructor. simpl; eauto.
     destruct sp; simpl; auto.
@@ -180,7 +179,6 @@ Proof.
     destruct Archi.ptr64 eqn:SF; auto. 
     apply Val.lessdef_same. f_equal. rewrite ! Ptrofs.add_assoc. f_equal. f_equal.
     rewrite Ptrofs.add_commut. auto with ptrofs.
-    destruct Archi.ptr64 eqn:SF; auto.
   - subst.
     replace (Val.add (Val.add v1 (Vint n1)) y)
        with (Val.add (Val.add v1 y) (Vint n1)).
@@ -965,43 +963,6 @@ Proof.
   destruct Archi.ptr64 eqn:PTR64.
   2: discriminate.
   destruct ty; cbn in *; try discriminate.
-  - (* Tint *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true. apply normalize_low_long; assumption.
-      * rewrite ExtValues.select01_long_false. apply normalize_low_long; assumption.
-        
-  - (* Tfloat *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true.
-        apply ExtValues.float_bits_normalize.
-      * rewrite ExtValues.select01_long_false.
-        apply ExtValues.float_bits_normalize.
-
-  - (* Tlong *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true. reflexivity.
-      * rewrite ExtValues.select01_long_false. reflexivity.
-
-  - (* Tsingle *)
-    inv H. TrivialExists.
-    + cbn. repeat econstructor; eassumption.
-    + cbn. f_equal. rewrite ExtValues.normalize_select01.
-      rewrite H3. destruct b.
-      * rewrite ExtValues.select01_long_true.
-        rewrite normalize_low_long by assumption.
-        apply ExtValues.single_bits_normalize.
-      * rewrite ExtValues.select01_long_false.
-        rewrite normalize_low_long by assumption.
-        apply ExtValues.single_bits_normalize.
 Qed.
 
 Theorem eval_addressing:
@@ -1024,8 +985,7 @@ Proof.
     destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
     simpl. auto.
   - exists (v1 :: nil); split. eauto with evalexpr. simpl.
-    destruct v1; simpl in H; try discriminate. destruct Archi.ptr64 eqn:SF; inv H. 
-    simpl. auto.
+    destruct v1; simpl in H; try discriminate.
   - exists (v :: nil);  split. eauto with evalexpr. subst. simpl. rewrite Ptrofs.add_zero; auto.
 Qed.
 
@@ -1045,7 +1005,6 @@ Proof.
 + constructor; auto.
 + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vint n) else Val.add v1 (Vint n)).
   repeat constructor; auto.
-  rewrite SF; auto.
 - destruct Archi.ptr64 eqn:SF.
 + InvEval. replace v with (if Archi.ptr64 then Val.addl v1 (Vlong n) else Val.add v1 (Vlong n)).
   repeat constructor; auto.