Miscellaneous lemmas that I used at some point while experimenting

1 files changed, 84 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 93a0ef66..9f65dbc0 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -84,6 +84,41 @@ Inductive match_internal: forall n, state -> state -> Prop :=
     (AGPC: Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC)
     : match_internal n (State rs1 m1) (State rs2 m2).
 
+Lemma match_internal_set_parallel:
+  forall n rs1 m1 rs2 m2 r val,
+  match_internal n (State rs1 m1) (State rs2 m2) ->
+  r <> PC ->
+  match_internal n (State (rs1#r <- val) m1) (State (rs2#r <- val ) m2).
+Proof.
+  intros n rs1 m1 rs2 m2 r v MI.
+  inversion MI; constructor; auto.
+  - intros r' NOTPC.
+    unfold Pregmap.set; rewrite AG. reflexivity. assumption.
+  - unfold Pregmap.set; destruct (PregEq.eq PC r); congruence.
+Qed.
+
+Lemma agree_match_states:
+  forall rs1 m1 rs2 m2,
+  match_states (State rs1 m1) (State rs2 m2) ->
+  forall r : preg, rs1#r = rs2#r.
+Proof.
+  intros.
+  unfold match_states in *.
+  assert (rs1 = rs2) as EQ. { congruence. }
+  rewrite EQ. reflexivity.
+Qed.
+
+Lemma match_states_set_parallel:
+  forall rs1 m1 rs2 m2 r v,
+  match_states (State rs1 m1) (State rs2 m2) ->
+  match_states (State (rs1#r <- v) m1) (State (rs2#r <- v) m2).
+Proof.
+  intros; unfold match_states in *.
+  assert (rs1 = rs2) as RSEQ. { congruence. }
+  assert (m1 = m2) as MEQ. { congruence. }
+  rewrite RSEQ in *; rewrite MEQ in *; unfold Pregmap.set; reflexivity.
+Qed.
+
 (* match_internal from match_states *)
 Lemma mi_from_ms:
   forall rs1 m1 rs2 m2 b ofs,
@@ -95,6 +130,7 @@ Proof.
   inv MS; constructor; auto; unfold Val.offset_ptr;
   rewrite PCVAL; rewrite Ptrofs.add_zero; reflexivity.
 Qed.
+
 Lemma transf_initial_states:
   forall s1, Asmblock.initial_state prog s1 ->
   exists s2, Asm.initial_state tprog s2 /\ match_states s1 s2.
@@ -116,6 +152,54 @@ Proof.
   inv FINAL_s1; inv MATCH; constructor; assumption.
 Qed.
 
+Definition max_pos (f : Asm.function) := length f.(Asm.fn_code).
+
+Lemma functions_bound_max_pos: forall fb f tf,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transf_function f = OK tf ->
+  Z.of_nat (max_pos tf) <= Ptrofs.max_unsigned.
+Proof.
+  intros fb f tf FINDf TRANSf.
+  unfold transf_function in TRANSf.
+  apply bind_inversion in TRANSf.
+  destruct TRANSf as (c & TRANSf).
+  destruct TRANSf as (_ & TRANSf).
+  destruct (zlt Ptrofs.max_unsigned (Z.of_nat (length c))).
+  - inversion TRANSf.
+  - unfold max_pos.
+    assert (Asm.fn_code tf = c) as H. { inversion TRANSf as (H'); auto. }
+    rewrite H; omega.
+Qed.
+
+Lemma match_internal_exec_label:
+  forall n rs1 m1 rs2 m2 l fb f tf,
+  Genv.find_funct_ptr ge fb = Some (Internal f) ->
+  transf_function f = OK tf ->
+  match_internal n (State rs1 m1) (State rs2 m2) ->
+  n >= 0 ->
+  (* There is no step if n is already max_pos *)
+  n < Z.of_nat (max_pos tf) ->
+  exists rs2' m2', Asm.exec_instr tge tf (Asm.Plabel l) rs2 m2 = Next rs2' m2'
+                   /\ match_internal (n+1) (State rs1 m1) (State rs2' m2').
+Proof.
+  intros. (* XXX auto generated names *)
+  unfold Asm.exec_instr.
+  eexists; eexists; split; eauto.
+  inversion H1; constructor; auto.
+  - intros; unfold Asm.nextinstr; unfold Pregmap.set;
+    destruct (PregEq.eq r PC); auto; contradiction.
+  - unfold Asm.nextinstr; rewrite Pregmap.gss; unfold Ptrofs.one.
+    rewrite <- AGPC; rewrite Val.offset_ptr_assoc; unfold Ptrofs.add;
+    rewrite Ptrofs.unsigned_repr. rewrite Ptrofs.unsigned_repr; trivial.
+    + split.
+      * apply Z.le_0_1.
+      * unfold Ptrofs.max_unsigned; simpl; unfold Ptrofs.wordsize;
+        unfold Wordsize_Ptrofs.wordsize; destruct Archi.ptr64; simpl; omega.
+    + split.
+      * apply Z.ge_le; assumption.
+      * rewrite <- functions_bound_max_pos; eauto; omega.
+Qed.
+
 Lemma step_simulation s1 t s1':
   Asmblock.step lk ge s1 t s1' ->
   forall s2, match_states s1 s2 ->