Add definition of match_internal

This relation will hold between Asmblock and Asm states while inside an
Asmblock block.

1 files changed, 18 insertions, 0 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 97612601..93a0ef66 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -77,6 +77,24 @@ Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 (* Asmblock and Asm share the same definition of state *)
 Definition match_states (s1 s2 : state) := s1 = s2.
 
+Inductive match_internal: forall n, state -> state -> Prop :=
+  | match_internal_intro n rs1 m1 rs2 m2
+    (MEM: m1 = m2)
+    (AG: forall r, r <> PC -> rs1 r = rs2 r)
+    (AGPC: Val.offset_ptr (rs1 PC) (Ptrofs.repr n) = rs2 PC)
+    : match_internal n (State rs1 m1) (State rs2 m2).
+
+(* match_internal from match_states *)
+Lemma mi_from_ms:
+  forall rs1 m1 rs2 m2 b ofs,
+  match_states (State rs1 m1) (State rs2 m2) ->
+  rs1#PC = Vptr b ofs ->
+  match_internal 0 (State rs1 m1) (State rs2 m2).
+Proof.
+  intros rs1 m1 rs2 m2 b ofs MS PCVAL.
+  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.