Revert back to original definition of match_states

(The simulation relation between aarch64's Asmblock and Asm as equality)

1 files changed, 8 insertions, 172 deletions

diff --git a/aarch64/Asmgenproof.v b/aarch64/Asmgenproof.v
index 23699f4a..97612601 100644
--- a/aarch64/Asmgenproof.v
+++ b/aarch64/Asmgenproof.v
@@ -44,12 +44,6 @@ Let ge := Genv.globalenv prog.
 Let tge := Genv.globalenv tprog.
 
 Definition lk :aarch64_linker := {| Asmblock.symbol_low:=Asm.symbol_low tge; Asmblock.symbol_high:=Asm.symbol_high tge|}.
-Record agree (rs1: regset) (rs2: regset) : Prop := mkagree {
-  agree_ir: forall r: iregsp, (rs1 r) = (rs2 r);
-  agree_fr: forall r: freg,   (rs1 r) = (rs2 r);
-  agree_cr: forall r: crbit,  (rs1 r) = (rs2 r);
-  agree_sp_def: (rs1 SP) <> Vundef;
-}.
 
 Lemma symbols_preserved:
   forall (s: ident), Genv.find_symbol tge s = Genv.find_symbol ge s.
@@ -81,11 +75,7 @@ Lemma functions_translated:
 Proof (Genv.find_funct_ptr_transf_partial TRANSF).
 
 (* Asmblock and Asm share the same definition of state *)
-Inductive match_states: state -> state -> Prop :=
-  | match_states_intro rs1 rs2 m
-    (AG: agree rs1 rs2)
-    (PC: rs1 PC = rs2 PC)
-    : match_states (State rs1 m) (State rs2 m).
+Definition match_states (s1 s2 : state) := s1 = s2.
 
 Lemma transf_initial_states:
   forall s1, Asmblock.initial_state prog s1 ->
@@ -97,9 +87,7 @@ Proof.
   - econstructor.
     eapply (Genv.init_mem_transf_partial TRANSF); eauto.
   - rewrite (match_program_main TRANSF); rewrite symbol_addresses_preserved.
-    unfold rs. unfold Vnullptr. unfold ge.
-    repeat (econstructor; eauto); simpl.
-    destruct Archi.ptr64; rewrite Pregmap.gss; discriminate.
+    unfold rs; reflexivity.
 Qed.
 
 Lemma transf_final_states:
@@ -107,151 +95,9 @@ Lemma transf_final_states:
   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.
-  inversion AG as (IR).
-  rewrite PC in *; rewrite IR in *;
-  constructor; trivial.
+  inv FINAL_s1; inv MATCH; constructor; assumption.
 Qed.
 
-Lemma agree_but_pc:
-  forall rs1 rs2 r,
-  r <> PC -> agree rs1 rs2 ->
-  (rs1 r) = (rs2 r).
-Proof.
-  intros rs1 rs2 r NOTPC AG.
-  inversion AG as (AGIR, AGFR, AGCR).
-  destruct r.
-  - apply AGIR.
-  - apply AGFR.
-  - apply AGCR.
-  - contradiction.
-Qed.
-
-Lemma agree_mregs:
-  forall (rs1 rs2 : regset) (r: mreg),
-  agree rs1 rs2 -> forall r: mreg, (rs1 (preg_of r)) = (rs2 (preg_of r)).
-Proof.
-  intros ? ? ? ? r. apply agree_but_pc; auto.
-  destruct r; discriminate.
-Qed.
-
-Lemma agree_iregs:
-  forall (rs1 rs2 : regset) (r: iregsp),
-  agree rs1 rs2 -> (rs1 r) = (rs2 r).
-Proof.
-  intros ? ? r. apply agree_but_pc; auto.
-  destruct r; discriminate.
-Qed.
-
-Lemma agree_fregs:
-  forall (rs1 rs2 : regset) (r: freg),
-  agree rs1 rs2 -> (rs1 r) = (rs2 r).
-Proof.
-  intros ? ? r. apply agree_but_pc; auto.
-  destruct r; discriminate.
-Qed.
-
-Lemma agree_sp:
-  forall (rs1 rs2 : regset),
-  agree rs1 rs2 -> (rs1 SP) = (rs2 SP).
-Proof.
-  intros ? ? r. apply agree_but_pc; auto.
-  discriminate.
-Qed.
-
-(* Copied and adapted from PseudoAsmblockproof *)
-Lemma extcall_arg_match ms rs m l v:
-  agree ms rs ->
-  extcall_arg ms m l v ->
-  extcall_arg rs m l v.
-Proof.
-  destruct 2.
-  - erewrite agree_mregs; eauto. constructor.
-  - econstructor; eauto. erewrite <- agree_sp; eauto.
-Qed.
-
-Local Hint Resolve extcall_arg_match: core.
-
-Lemma extcall_arg_pair_match:
-  forall ms rs m p v,
-  agree ms rs ->
-  extcall_arg_pair ms m p v ->
-  extcall_arg_pair rs m p v.
-Proof.
-  destruct 2; constructor; eauto.
-Qed.
-
-Local Hint Resolve extcall_arg_pair_match: core.
-
-Lemma extcall_args_match:
-  forall ms rs m, agree ms rs ->
-  forall ll vl,
-  list_forall2 (extcall_arg_pair ms m) ll vl ->
-  list_forall2 (extcall_arg_pair rs m) ll vl.
-Proof.
-  induction 2; constructor; eauto.
-Qed.
-
-Lemma extcall_arguments_match:
-  forall ms m rs sg args,
-  agree ms rs ->
-  extcall_arguments ms m sg args ->
-  extcall_arguments rs m sg args.
-Proof.
-  unfold extcall_arguments, extcall_arguments; intros.
-  eapply extcall_args_match; eauto.
-Qed.
-
-Lemma agree_undef_caller_save_regs_match:
-  forall rs1 rs2,
-  agree rs1 rs2 -> agree (undef_caller_save_regs rs1) (undef_caller_save_regs rs2).
-Proof.
-  intros rs1 rs2 AG.
-  unfold undef_caller_save_regs. split; auto; intros.
-  - erewrite agree_iregs; auto.
-  - erewrite agree_fregs; auto.
-  - simpl; inversion AG; assumption.
-Qed.
-
-Lemma agree_set_parallel:
-  forall rs1 rs2 r v,
-  agree rs1 rs2 ->
-  r <> SP \/ v <> Vundef -> (* TODO is the right case ever useful? *)
-  agree (rs1#r <- v) (rs2#r <- v).
-Proof.
-  intros rs1 rs2 r v AG H. split; auto.
-  (* TODO refactor repetitive proof *)
-  - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r).
-    + reflexivity.
-    + erewrite agree_but_pc; eauto. discriminate.
-  - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r).
-    + reflexivity.
-    + erewrite agree_but_pc; eauto. discriminate.
-  - intros. unfold Pregmap.set. destruct (PregEq.eq r0 r).
-    + reflexivity.
-    + erewrite agree_but_pc; eauto. discriminate.
-  - destruct H.
-    + rewrite Pregmap.gso; inv AG; auto.
-    + destruct (PregEq.eq SP r) as [SPr | SPnotr].
-      * rewrite SPr; rewrite Pregmap.gss; assumption.
-      * rewrite Pregmap.gso; auto. inv AG; auto.
-Qed.
-
-Lemma agree_set_pair:
-  forall rs1 rs2 p v,
-  agree rs1 rs2 ->
-  (* TODO assumption that pair does not include SP *)
-  agree (set_pair p v rs1) (set_pair p v rs2).
-Proof.
-  intros rs1 rs2 p v AG.
-  destruct p; simpl.
-  - assert (r <> SP) as NOTSP. { admit. }
-    apply agree_set_parallel; auto.
-  - assert (rlo <> SP /\ rhi <> SP) as NOTSP. { admit. } destruct NOTSP.
-    apply agree_set_parallel; auto.
-    + apply agree_set_parallel; auto.
-Admitted.
-
 Lemma step_simulation s1 t s1':
   Asmblock.step lk ge s1 t s1' ->
   forall s2, match_states s1 s2 ->
@@ -261,25 +107,15 @@ Proof.
   inv STEP; simpl; exploit functions_translated; eauto;
   intros (tf0 & FINDtf & TRANSf);
   monadInv TRANSf.
-  - (* internal step *)
-     destruct H2. (* exec_bblock *)
-     admit.
+  - (* internal step *) admit.
   - (* external step *)
-    inversion MATCH as (?, ?, ?, AG, AGPC).
-    exploit external_call_symbols_preserved; eauto. apply senv_preserved.
-    exploit extcall_arguments_match; eauto.
-    intros.
     eexists; split.
     + apply plus_one.
-      rewrite AGPC in *.
+      rewrite <- MATCH.
+      exploit external_call_symbols_preserved; eauto. apply senv_preserved.
+      intros ?.
       eapply Asm.exec_step_external; eauto.
-    + exploit agree_undef_caller_save_regs_match; eauto; intros AG'.
-      erewrite agree_iregs; eauto.
-      econstructor; auto.
-      apply agree_set_parallel.
-      apply agree_set_pair.
-      * apply agree_undef_caller_save_regs_match; auto.
-      * left. discriminate.
+    + econstructor; eauto.
 Admitted.
 
 Lemma transf_program_correct: