From ec47f7b92635952b7ae0f1901772ad4203b41f9b Mon Sep 17 00:00:00 2001
From: Léo Gourdin <leo.gourdin@univ-grenoble-alpes.fr>
Date: Wed, 14 Oct 2020 10:17:02 +0200
Subject: Draft commit on the PArithComparisonPP Proof

in exec_basic_simulation
---
 aarch64/Asmgenproof.v | 86 ++++++++++++++++++++++++++++++++++++++++++---------
 1 file changed, 72 insertions(+), 14 deletions(-)

(limited to 'aarch64/Asmgenproof.v')

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 718292f9..155114ef 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1024,18 +1024,6 @@ Proof.
     rewrite <- Ptrofs.add_unsigned. rewrite <- Val.offset_ptr_assoc. rewrite EQPC; eauto.
 Qed.
 
-(*Lemma arithp_preserved n rs1 m1 rs2 m2 rs2' rd i tf v: forall
-  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
-  (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
-  (rd': type_reg (arithp_args_type i))
-  (NEXTI: reg_of_preg (arithp_args_type i) rd = OK rd')
-  (RS2P: (Asm.nextinstr rs2 # rd <- v) = rs2')
-  (HV: (arith_eval_p lk i) = v),
-  Asm.exec_instr tge tf (arithp_to_instruction i rd') rs2 m2 = Next rs2' m2
-  /\ match_internal (n + 1) (State (rs1 # rd <- v) m1) (State rs2' m2).
-Proof.
-Admitted.*)
-
 Ltac inv_ok_eq :=
   repeat match goal with
   | [EQ: OK ?x = OK ?y |- _ ]
@@ -1055,6 +1043,7 @@ Ltac destruct_reg_inv :=
   end.
 
 Ltac destruct_reg_size :=
+  simpl in *;
   repeat match goal with
   | [ |- context [ match ?reg with _ => _ end = _ ] ]
       => destruct reg; try congruence
@@ -1072,6 +1061,12 @@ Ltac inv_matchi :=
       => inversion MATCHI; subst; find_rwrt_ag
   end.
 
+Ltac destruct_ir0_reg :=
+  match goal with
+  | [ |- context [ ir0 _ _ ?r ] ]
+      => unfold ir0 in *; destruct r; find_rwrt_ag; eauto
+  end.
+
 Lemma exec_basic_simulation:
   forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
   (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
@@ -1088,7 +1083,7 @@ Proof.
     simpl in *; destruct i.
     + (* PArithP *)
       destruct i;
-      monadInv TRANSBI;
+      try (monadInv TRANSBI);
       try (destruct_reg_inv);
       exploit next_inst_preserved; eauto;
       try (destruct_reg_size).
@@ -1108,8 +1103,71 @@ Proof.
       try (exploit next_inst_preserved; eauto);
       try (destruct_reg_size).
     + (* PArithRR0R *)
-
+      destruct i;
+      try (monadInv TRANSBI);
+      try (inv_matchi);
+      try (exploit next_inst_preserved; eauto);
+      try (destruct_reg_size);
+      try (destruct_ir0_reg).
+    + (* PArithRR0 *)
+      destruct i;
+      try (monadInv TRANSBI);
+      try (inv_matchi);
+      try (exploit next_inst_preserved; eauto);
+      try (destruct_reg_size);
+      try (destruct_ir0_reg).
+    + (* PArithARRRR0 *)
+      destruct i;
+      try (monadInv TRANSBI);
+      try (inv_matchi);
+      try (exploit next_inst_preserved; eauto);
+      try (destruct_reg_size);
+      try (destruct_ir0_reg).
+    + (* PArithComparisonPP *)
+      (*destruct i.*)
+
+      (*-- monadInv TRANSBI.*)
+         (*simpl in *. inversion MATCHI; subst.*)
+         (*inversion BASIC. repeat (econstructor; eauto).*)
+          (** intros. unfold Asm.nextinstr, compare_long.*)
+            (*rewrite (Pregmap.gso (i := r) (j := PC)); try congruence.*)
+            (*rewrite (Pregmap.gso (i := r) (j := CV)); try congruence.*)
+            (*destruct (PregEq.eq r CV).*)
+            (*{ *)
+              (*subst. rewrite !Pregmap.gss.*)
+              (*rewrite (Pregmap.gso (i := CV) (j := CC)).*)
+              (*destruct (PregEq.eq CV CC).*)
+              (*{ *)
+                (*rewrite Pregmap.gso.*)
+                (*destruct (PregEq.eq CV CC).*)
+                (*{*)
+                  (*rewrite Pregmap.gso.*)
+                  (*destruct (PregEq.eq CV CN).*)
+                  (*{*)
+                    (*unfold Val.subl_overflow.*)
+                    (*destruct (rs2 x0); try congruence.*)
+                  (*}*)
+                  (*{*)
+                    (*unfold Val.subl_overflow.*)
+                    (*destruct (rs2 x0); try congruence.*)
+                  (*}*)
+                  (*{ *)
+                    (*try congruence.*)
+                  (*}*)
+                (*}*)
+                (*{ rewrite !Pregmap.gso; try congruence. }*)
+                (*{ try congruence. }*)
+              (*}*)
+              (*{  }*)
+      all:admit.
+    + (* PArithComparisonR0R *)
       all:admit.
+    + (* PArithComparisonP *)
+      all:admit.
+    + (* Pcset *)
+      simpl in *.
+      all:admit.
+
     all:admit.
 
   (*
-- 
cgit