Start Asmgenproof

- Define simulation relation as equality.
- Prove the easy cases, transf_initial_states, transf_final_states, and
  begin with the proof for the step simulation (external calls)

1 files changed, 69 insertions, 3 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 93899c72..97612601 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -45,11 +45,21 @@ Let tge := Genv.globalenv tprog.
 
 Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
 
-
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
 Proof (Genv.find_symbol_match TRANSF).
 
+Lemma symbol_addresses_preserved:
+  forall (s: ident) (ofs: ptrofs),
+  Genv.symbol_address tge s ofs = Genv.symbol_address ge s ofs.
+Proof.
+  intros; unfold Genv.symbol_address; rewrite symbols_preserved; reflexivity.
+Qed.
+
+Lemma senv_preserved:
+  Senv.equiv ge tge.
+Proof (Genv.senv_match TRANSF).
+
 Lemma symbol_high_low: forall (id: ident) (ofs: ptrofs),
   Val.addl (Asmblock.symbol_high lk id ofs) (Asmblock.symbol_low lk id ofs) = Genv.symbol_address ge id ofs.
 Proof.
@@ -57,9 +67,66 @@ Proof.
   rewrite symbols_preserved; reflexivity.
 Qed.
 
+Lemma functions_translated:
+  forall b f,
+  Genv.find_funct_ptr ge b = Some f ->
+  exists tf,
+  Genv.find_funct_ptr tge b = Some tf /\ transf_fundef f = OK tf.
+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.
+
+Lemma transf_initial_states:
+  forall s1, Asmblock.initial_state prog s1 ->
+  exists s2, Asm.initial_state tprog s2 /\ match_states s1 s2.
+Proof.
+  intros ? INIT_s1.
+  inversion INIT_s1 as (m, ?, ge0, rs). unfold ge0 in *.
+  econstructor; split.
+  - econstructor.
+    eapply (Genv.init_mem_transf_partial TRANSF); eauto.
+  - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved.
+    unfold rs; reflexivity.
+Qed.
+
+Lemma transf_final_states:
+  forall s1 s2 r,
+  match_states s1 s2 -> Asmblock.final_state s1 r -> Asm.final_state s2 r.
+Proof.
+  intros s1 s2 r MATCH FINAL_s1.
+  inv FINAL_s1; inv MATCH; constructor; assumption.
+Qed.
+
+Lemma step_simulation s1 t s1':
+  Asmblock.step lk ge s1 t s1' ->
+  forall s2, match_states s1 s2 ->
+  (exists s2', plus Asm.step tge s2 t s2' /\ match_states s1' s2').
+Proof.
+  intros STEP s2 MATCH.
+  inv STEP; simpl; exploit functions_translated; eauto;
+  intros (tf0 & FINDtf & TRANSf);
+  monadInv TRANSf.
+  - (* internal step *) admit.
+  - (* external step *)
+    eexists; split.
+    + apply plus_one.
+      rewrite <- MATCH.
+      exploit external_call_symbols_preserved; eauto. apply senv_preserved.
+      intros ?.
+      eapply Asm.exec_step_external; eauto.
+    + econstructor; eauto.
+Admitted.
+
 Lemma transf_program_correct:
   forward_simulation (Asmblock.semantics lk prog) (Asm.semantics tprog).
-Admitted. (* TODO *)
+Proof.
+  eapply forward_simulation_plus.
+  - apply senv_preserved.
+  - eexact transf_initial_states.
+  - eexact transf_final_states.
+  - (* TODO step_simulation *) admit.
+Admitted.
 
 End PRESERVATION.
 
@@ -140,4 +207,3 @@ Module Asmgenproof0.
 Definition return_address_offset := return_address_offset.
 
 End Asmgenproof0.
-