Less auto-generated names

1 files changed, 36 insertions, 36 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 29c746ba..6b73c5d6 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -228,31 +228,32 @@ Lemma cf_instruction_simulated:
                                   rs2 m2 = Next rs2' m2'
                    /\ match_states (State rs1' m1') (State rs2' m2').
 Proof.
-  intros. (* XXX auto-generated names *)
-  destruct cfi.
+  intros size_b f tf rs1 m1 rs1' m1' cfi SIZE_B_GE_1 STEP rs2 m2 MI.
+  destruct cfi; inv STEP; simpl in H0.
   - (* Pb *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
-      unfold incrPC, Asm.goto_label, goto_label.
-      inv H1. rewrite <- AGPC.
+    + rewrite <- H0;
+      unfold incrPC, Asm.goto_label, goto_label;
+      inv MI; rewrite <- AGPC.
       (* TODO: show that Asm.label_pos and label_pos behave the same *
        *       show that both Val.offset_ptr calculation return Vptr _ _ *)
       admit.
     + constructor.
   - (* Pbc *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
+      (* TODO see Pb *)
       admit.
     + constructor.
   - (* Pbl *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       rewrite symbol_addresses_preserved.
       unfold incrPC.
       assert ( Val.offset_ptr (rs2 PC) Ptrofs.one
              = Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)
              ) as EQPC. {
-        inv H1. rewrite <- AGPC.
+        inv MI. rewrite <- AGPC.
         rewrite Val.offset_ptr_assoc.
         unfold Ptrofs.one.
         rewrite Ptrofs.add_unsigned.
@@ -274,12 +275,12 @@ Proof.
         intros x. destruct (PregEq.eq x X30) as [X | X].
         - rewrite X. reflexivity.
         - destruct (PregEq.eq x PC) as [X' | X']; auto.
-        inv H1. rewrite AG; auto.
-      } rewrite EQRS. inv H1. reflexivity.
+        inv MI. rewrite AG; auto.
+      } rewrite EQRS. inv MI. reflexivity.
     + constructor.
   - (* Pbs *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       rewrite symbol_addresses_preserved.
       unfold incrPC.
       assert ( (rs2 # PC <- (Genv.symbol_address ge id Ptrofs.zero))
@@ -288,12 +289,12 @@ Proof.
              ) as EQRS. {
         unfold Pregmap.set; apply functional_extensionality. intros x.
         destruct (PregEq.eq x PC) as [X | X]; auto.
-        inv H1; rewrite AG; auto.
-      } rewrite EQRS; inv H1; auto.
+        inv MI; rewrite AG; auto.
+      } rewrite EQRS; inv MI; auto.
     + constructor.
   - (* Pblr *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       unfold incrPC. rewrite Pregmap.gss. rewrite Pregmap.gso; try discriminate.
       assert ( (rs2 # X30 <- (Val.offset_ptr (rs2 PC) Ptrofs.one)) # PC <- (rs2 r)
              = ((rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
@@ -302,51 +303,50 @@ Proof.
              ) as EQRS. {
         unfold Pregmap.set. apply functional_extensionality.
         intros x; destruct (PregEq.eq x PC) as [X | X].
-        - inv H1; rewrite AG; auto. discriminate.
+        - inv MI; rewrite AG; auto. discriminate.
         - destruct (PregEq.eq x X30) as [X' | X'].
-          + inv H1. rewrite <- AGPC.
+          + inv MI. rewrite <- AGPC.
             rewrite Val.offset_ptr_assoc. unfold Ptrofs.one.
             rewrite Ptrofs.add_unsigned. rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr.
             rewrite Z.sub_add; reflexivity.
             * split; try omega. apply one_le_max_unsigned.
             * split; try omega.
               (* TODO size_b - 1 <= Ptrofs.max_unsigned needs extra hypothesis *) admit.
-          + inv H1; rewrite AG; auto.
-      } rewrite EQRS. inv H1; auto.
+          + inv MI; rewrite AG; auto.
+      } rewrite EQRS. inv MI; auto.
     + constructor.
   - (* Pbr *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       unfold incrPC. rewrite Pregmap.gso; try discriminate.
-
       assert (  rs2 # PC <- (rs2 r)
              = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b)))
                     # PC <- (rs1 r)
              ) as EQRS. {
         unfold Pregmap.set; apply functional_extensionality.
         intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
-        - inv H1; rewrite AG; try discriminate. reflexivity.
-        - inv H1; rewrite AG; auto.
-      } rewrite EQRS; inv H1; auto.
+        - inv MI; rewrite AG; try discriminate. reflexivity.
+        - inv MI; rewrite AG; auto.
+      } rewrite EQRS; inv MI; auto.
     + constructor.
   - (* Pret *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3.
-      rewrite <- H3. unfold incrPC. rewrite Pregmap.gso; try discriminate.
+    + rewrite <- H0.
+      unfold incrPC. rewrite Pregmap.gso; try discriminate.
       assert (  rs2 # PC <- (rs2 r)
              = (rs1 # PC <- (Val.offset_ptr (rs1 PC) (Ptrofs.repr size_b))) # PC <- (rs1 r)
              ) as EQRS. {
         unfold Pregmap.set; apply functional_extensionality.
         intros x; destruct (PregEq.eq x PC) as [X | X]; try discriminate.
-        - inv H1; rewrite AG; try discriminate. reflexivity.
-        - inv H1; rewrite AG; auto.
-      } rewrite EQRS; inv H1; auto.
+        - inv MI; rewrite AG; try discriminate. reflexivity.
+        - inv MI; rewrite AG; auto.
+      } rewrite EQRS; inv MI; auto.
     + constructor.
   - (* Pcbnz *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       unfold eval_neg_branch. destruct sz.
-      * simpl. inv H1. rewrite <- AG; try discriminate.
+      * simpl. inv MI. rewrite <- AG; try discriminate.
         replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs1 r). 2: {
           symmetry. rewrite incrPC_agree_but_pc; try discriminate; auto.
         }
@@ -365,33 +365,33 @@ Proof.
     + constructor.
   - (* Pcbz *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       unfold eval_branch. (* TODO, will be very similar to Pcbnz *) admit.
     + constructor.
   - (* Pcbz *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       unfold eval_branch.
       replace (incrPC (Ptrofs.repr size_b) rs1 r) with (rs2 r). 2: {
           symmetry; rewrite incrPC_agree_but_pc; try discriminate; auto;
-          inv H1; rewrite AG; try discriminate; auto.
+          inv MI; rewrite AG; try discriminate; auto.
       } (* TODO, cf. Pcbnz *) admit.
     + constructor.
   - (* Ptbz *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       (* TODO, cf. Pcbz *) admit.
     + constructor.
   - (* Pbtbl *)
     simpl; eexists; eexists; split.
-    + inv H0. simpl in H3. rewrite <- H3.
+    + rewrite <- H0.
       assert (  rs2 # X16 <- Vundef r1
              = (incrPC (Ptrofs.repr size_b) rs1) # X16 <- Vundef r1
              ) as EQUNDEFX16. {
         unfold incrPC, Pregmap.set.
         destruct (PregEq.eq r1 X16) as [X16 | X16]; auto.
         destruct (PregEq.eq r1 PC) as [PC' | PC']; try discriminate.
-        inv H1; rewrite AG; auto.
+        inv MI; rewrite AG; auto.
       } rewrite <- EQUNDEFX16.
       (* TODO Asm.goto_label and goto_label *) admit.
     + constructor.