Adding a lemma for exec load propagation.

The commit also contains an incomplete proof for assert (BDYLENPOS: ((length li) < length (body bb))%nat).

1 files changed, 27 insertions, 25 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 8ac9684d..1699b5f1 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -1001,8 +1001,24 @@ Proof.
   + next_stuck_cong.
 Qed.
 
+Lemma exec_load_propag: forall sz rs2 m2 x a,
+  (Asm.exec_load tge Mint8unsigned
+    match sz with
+    | W => fun v : val => v
+    | X => Val.longofintu
+    end a x rs2 m2) =
+  (match sz with
+  | W => Asm.exec_load tge Mint8unsigned (fun v : val => v) a x rs2 m2
+  | X => Asm.exec_load tge Mint8unsigned Val.longofintu a x rs2 m2
+   end).
+Proof.
+  intros.
+  destruct sz; eauto.
+Qed.
+
 Lemma exec_basic_simulation:
   forall tf n rs1 m1 rs1' m1' rs2 m2 bi tbi
+  (BOUNDED: 0 <= n <= Ptrofs.max_unsigned)
   (BASIC: exec_basic lk ge bi rs1 m1 = Next rs1' m1')
   (MATCHI: match_internal n (State rs1 m1) (State rs2 m2))
   (TRANSBI: basic_to_instruction bi = OK tbi),
@@ -1013,30 +1029,8 @@ Proof.
   intros.
   destruct bi.
   2: {
-    simpl in*. destruct ld.
-    { monadInv TRANSBI. destruct rd as [[r|]|]; try congruence. inversion EQ; subst.
-
-      (*exploit load_preserved; eauto.*)
-
-      simpl in *. unfold exec_load, Asm.exec_load in *.
-      inversion MATCHI as [n0 r1 mx1 r2 mx2 EQM EQR EQPC]; subst.
-      rewrite <- (eval_addressing_preserved a rs1 rs2); auto.
-      destruct (Mem.loadv _ _ _).
-      + inversion BASIC; auto. repeat (econstructor; eauto).
-        * intros. unfold Asm.nextinstr. rewrite (Pregmap.gso (i := r) (j := PC)); auto.
-          destruct (PregEq.eq r x).
-          { subst. rewrite !Pregmap.gss; auto. }
-          { rewrite !Pregmap.gso; auto. }
-        * unfold Asm.nextinstr. rewrite Pregmap.gss. rewrite !Pregmap.gso; try congruence. admit.
-      + next_stuck_cong. }
-    all:admit.
-    
-  } all:admit.
-(*rs1 # x <- v r = Asm.nextinstr rs2 # x <- v r*)
-   (*Next (Asm.nextinstr rs2 # x <- v) m1' = Next rs2' m2*)
-  (*rs1 # x <- v r =*)
-(*(rs2 # x <- v) # PC <- (Val.offset_ptr (rs2 # x <- v PC) Ptrofs.one) r*)
-
+    simpl in*. destruct ld; monadInv TRANSBI; destruct rd as [[r|]|]; try congruence; inversion EQ; subst; exploit load_preserved; eauto.
+    - intros. simpl in *. rewrite exec_load_propag in H; eauto.
 Admitted.
 
 Lemma exec_body_simulation_star': forall
@@ -1175,7 +1169,15 @@ Lemma exec_body_simulation_plus_alt li: forall b ofs f bb rs m s2 rs' m'
 Proof.
   induction li as [|a li]; simpl; try congruence.
   intros.
-  assert (BDYLENPOS: ((length li) < length (body bb))%nat). { admit. (* TODO *) }
+  assert (BDYLENPOS: ((length li) < length (body bb))%nat). { 
+    (*apply is_tail_cons_left in BLI as BLI'.*)
+    (*apply is_tail_incl in BLI as INCLBLI.*)
+    (*apply NoDup_incl_length in INCLBLI as INCLBLILEN.*)
+    (* TODO -> The above statement requires a NoDup hyp... *)
+    (*econstructor.*)
+    (*assert (TAILLEN: ((length li) < (length (a :: li)))%nat). {*)
+      (*econstructor.*)
+    admit. }
   exploit internal_functions_unfold; eauto.
   intros (tc & FINDtf & TRANStf & _). 
   exploit find_basic_instructions; eauto.