(* *************************************************************)
(*                                                             *)
(*             The Compcert verified compiler                  *)
(*                                                             *)
(*           Sylvain Boulmé     Grenoble-INP, VERIMAG          *)
(*           David Monniaux     CNRS, VERIMAG                  *)
(*           Cyril Six          Kalray                         *)
(*           Léo Gourdin        UGA, VERIMAG                   *)
(*                                                             *)
(*  Copyright Kalray. Copyright VERIMAG. All rights reserved.  *)
(*  This file is distributed under the terms of the INRIA      *)
(*  Non-Commercial License Agreement.                          *)
(*                                                             *)
(* *************************************************************)

Require Import Coqlib Errors.
Require Import Integers Floats AST Linking.
Require Import Values Memory Events Globalenvs Smallstep.
Require Import Op Locations Machblock Conventions Asmblock.
Require Import Asmblockprops.
Require Import PostpassScheduling.
Require Import Asmblockgenproof.
Require Import Axioms.
Require Import Lia.

Local Open Scope error_monad_scope.

Definition match_prog (p tp: program) :=
  match_program (fun _ f tf => transf_fundef f = OK tf) eq p tp.

Lemma transf_program_match:
  forall p tp, transf_program p = OK tp -> match_prog p tp.
Proof.
  intros. eapply match_transform_partial_program; eauto.
Qed.

Section PRESERVATION_ASMBLOCK.

Variables prog tprog: program.
Variable lk: aarch64_linker.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma symbols_preserved:
  forall id,
  Genv.find_symbol tge id = Genv.find_symbol ge id.
Proof (Genv.find_symbol_match TRANSL).

Lemma senv_preserved:
  Senv.equiv ge tge.
Proof (Genv.senv_match TRANSL).

Lemma function_ptr_translated:
  forall v f,
  Genv.find_funct_ptr ge v = Some f ->
  exists tf,
  Genv.find_funct_ptr tge v = Some tf /\ transf_fundef f = OK tf.
Proof (Genv.find_funct_ptr_transf_partial TRANSL).

Inductive match_states: state -> state -> Prop :=
  | match_states_intro:
      forall s1 s2, s1 = s2 -> match_states s1 s2.

Lemma prog_main_preserved:
  prog_main tprog = prog_main prog.
Proof (match_program_main TRANSL).

Lemma prog_main_address_preserved:
  (Genv.symbol_address (Genv.globalenv prog) (prog_main prog) Ptrofs.zero) =
  (Genv.symbol_address (Genv.globalenv tprog) (prog_main tprog) Ptrofs.zero).
Proof.
  unfold Genv.symbol_address. rewrite symbols_preserved.
  rewrite prog_main_preserved. auto.
Qed.

Lemma transf_initial_states:
  forall st1, initial_state prog st1 ->
  exists st2, initial_state tprog st2 /\ match_states st1 st2.
Proof.
  intros. inv H.
  econstructor; split.
  - eapply initial_state_intro.
    eapply (Genv.init_mem_transf_partial TRANSL); eauto.
  - econstructor; eauto. subst ge0. subst rs0. rewrite prog_main_address_preserved. auto.
Qed.

Lemma transf_final_states:
  forall st1 st2 r,
  match_states st1 st2 -> final_state st1 r -> final_state st2 r.
Proof.
  intros. inv H0. inv H. econstructor; eauto.
Qed.

Lemma transf_find_bblock:
  forall ofs f bb tf,
  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bb ->
  transf_function f = OK tf ->
  exists tbb,
     verified_schedule bb = OK tbb
     /\ find_bblock (Ptrofs.unsigned ofs) (fn_blocks tf) = Some tbb.
Proof.
  intros.
  monadInv H0. destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks x))); try (inv EQ0; fail). inv EQ0.
  monadInv EQ. simpl in *.
  generalize (Ptrofs.unsigned ofs) H x EQ0; clear ofs H x g EQ0.
  induction (fn_blocks f).
  - intros. simpl in *. discriminate.
  - intros. simpl in *.
    monadInv EQ0. simpl.
    destruct (zlt z 0); try discriminate.
    destruct (zeq z 0).
    + inv H. eauto.
    + monadInv EQ0.
      exploit IHb; eauto.
      intros (tbb & SCH & FIND).
      eexists; split; eauto.
      inv FIND.
      unfold verify_size in EQ0.
      destruct (size a =? size (stick_header (header a) x)) eqn:EQSIZE; try discriminate.
      rewrite Z.eqb_eq in EQSIZE; rewrite EQSIZE.
      reflexivity.
Qed.

Lemma stick_header_neutral: forall a,
  a = (stick_header (header a) (no_header a)).
Proof.
  intros.
  unfold stick_header. unfold Asmblock.stick_header_obligation_1. simpl. destruct a.
  simpl. reflexivity.
Qed.

Lemma symbol_address_preserved:
  forall l ofs, Genv.symbol_address ge l ofs = Genv.symbol_address tge l ofs.
Proof.
  intros. unfold Genv.symbol_address. repeat (rewrite symbols_preserved). reflexivity.
Qed.

Lemma verified_schedule_label:
  forall bb tbb l,
  verified_schedule bb = OK (tbb) ->
     is_label l bb = is_label l tbb.
Proof.
  intros.
  unfold is_label.
  monadInv H. simpl. auto.
Qed.

Remark label_pos_pvar_none_add:
  forall tc l p p' k,
  label_pos l (p+k) tc = None -> label_pos l (p'+k) tc = None.
Proof.
  induction tc.
  - intros. simpl. auto.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
    + discriminate.
    + pose (IHtc l p p' (k + size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.

Lemma label_pos_pvar_none:
  forall tc l p p',
  label_pos l p tc = None -> label_pos l p' tc = None.
Proof.
  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
  eapply label_pos_pvar_none_add; eauto.
Qed.

Remark label_pos_pvar_some_add_add:
  forall tc l p p' k k',
  label_pos l (p+k') tc = Some (p+k) -> label_pos l (p'+k') tc = Some (p'+k).
Proof.
  induction tc.
  - intros. simpl in H. discriminate.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
    + inv H. assert (k = k') by lia. subst. reflexivity.
    + pose (IHtc l p p' k (k' + size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.

Lemma label_pos_pvar_some_add:
  forall tc l p p' k,
  label_pos l p tc = Some (p+k) -> label_pos l p' tc = Some (p'+k).
Proof.
  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
  eapply label_pos_pvar_some_add_add; eauto.
Qed.

Remark label_pos_pvar_add:
  forall c tc l p p' k,
  label_pos l (p+k) c = label_pos l p tc ->
  label_pos l (p'+k) c = label_pos l p' tc.
Proof.
  induction c.
  - intros. simpl in *.
    exploit label_pos_pvar_none; eauto.
  - intros. simpl in *. destruct (is_label _ _) eqn:ISLBL.
    + exploit label_pos_pvar_some_add; eauto.
    + pose (IHc tc l p p' (k+size a)). repeat (rewrite Z.add_assoc in e). auto.
Qed.

Lemma label_pos_pvar:
  forall c tc l p p',
  label_pos l p c = label_pos l p tc ->
  label_pos l p' c = label_pos l p' tc.
Proof.
  intros. rewrite (Zplus_0_r_reverse p') at 1. rewrite (Zplus_0_r_reverse p) in H at 1.
  eapply label_pos_pvar_add; eauto.
Qed.

Lemma label_pos_head_cons:
  forall c bb tbb l tc p,
  verified_schedule bb = OK tbb ->
  label_pos l p c = label_pos l p tc ->
  label_pos l p (bb :: c) = label_pos l p (tbb :: tc).
Proof.
  intros. simpl.
  exploit verified_schedule_label; eauto. intros ISLBL.
  rewrite ISLBL.
  destruct (is_label l tbb) eqn:ISLBL'; simpl; auto.
  eapply label_pos_pvar in H0. erewrite H0.
  erewrite verified_schedule_size; eauto.
Qed.

Lemma label_pos_preserved:
  forall c tc l,
  transf_blocks c = OK tc -> label_pos l 0 c = label_pos l 0 tc.
Proof.
  induction c.
  - intros. simpl in *. inv H. reflexivity.
  - intros. unfold transf_blocks in H; fold transf_blocks in H. monadInv H.
    eapply IHc in EQ. eapply label_pos_head_cons; eauto.
Qed.

Lemma label_pos_preserved_blocks:
  forall l f tf,
  transf_function f = OK tf ->
  label_pos l 0 (fn_blocks f) = label_pos l 0 (fn_blocks tf).
Proof.
  intros. monadInv H. monadInv EQ.
  destruct (zlt Ptrofs.max_unsigned _); try discriminate.
  monadInv EQ0. simpl. eapply label_pos_preserved; eauto.
Qed.

Lemma transf_exec_basic:
  forall i rs m, exec_basic lk ge i rs m = exec_basic lk tge i rs m.
Proof.
  intros. pose symbol_address_preserved.
  unfold exec_basic. 
  destruct i; simpl; auto; try congruence.
Qed.

Lemma transf_exec_body:
  forall bdy rs m, exec_body lk ge bdy rs m = exec_body lk tge bdy rs m.
Proof.
  induction bdy; intros.
  - simpl. reflexivity.
  - simpl. rewrite transf_exec_basic.
    destruct (exec_basic _ _ _); auto.
Qed.

Lemma transf_exec_cfi: forall f tf cfi rs m,
  transf_function f = OK tf ->
  exec_cfi ge f cfi rs m = exec_cfi tge tf cfi rs m.
Proof.
  intros. destruct cfi; simpl; auto;
  assert (ge = Genv.globalenv prog); auto;
  assert (tge = Genv.globalenv tprog); auto;
  pose symbol_address_preserved.
  all: try unfold eval_branch; try unfold eval_neg_branch; try unfold goto_label;
       try erewrite label_pos_preserved_blocks; try rewrite e; eauto.
  destruct (rs # X16 <- Vundef r1); auto.
  destruct (list_nth_z tbl (Int.unsigned i)); auto.
  erewrite label_pos_preserved_blocks; eauto.
Qed.

Lemma transf_exec_exit:
  forall f tf sz ex t rs m rs' m',
  transf_function f = OK tf ->
  exec_exit ge f sz rs m ex t rs' m' ->
  exec_exit tge tf sz rs m ex t rs' m'.
Proof.
  intros. induction H0.
  - econstructor.
  - econstructor. erewrite <- transf_exec_cfi; eauto.
  - econstructor; eauto.
    eapply eval_builtin_args_preserved with (ge1 := ge); eauto. exact symbols_preserved.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
Qed.

Lemma transf_exec_bblock:
  forall f tf bb t rs m rs' m',
  transf_function f = OK tf ->
  exec_bblock lk ge f bb rs m t rs' m' ->
  exec_bblock lk tge tf bb rs m t rs' m'.
Proof.
  intros.
  destruct H0 as [rs1[m1[BDY EXIT]]].
  unfold exec_bblock.
  eexists; eexists; split.
  rewrite <- transf_exec_body; eauto.
  eapply transf_exec_exit; eauto.
Qed.

Theorem transf_step_correct:
  forall s1 t s2, step lk ge s1 t s2 ->
  forall s1' (MS: match_states s1 s1'),
  (exists s2', step lk tge s1' t s2' /\ match_states s2 s2').
Proof.
  induction 1; intros; inv MS.
  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
    exploit transf_find_bblock; eauto. intros (tbb & VES & FIND).
    exploit verified_schedule_correct; eauto. intros EBB.
    eapply transf_exec_bblock in EBB; eauto. 
    exists (State rs' m').
    split; try (econstructor; eauto).
  - exploit function_ptr_translated; eauto. intros (tf & FFP & TRANSF). monadInv TRANSF.
    remember (State _ m') as s'. exists s'. split; try constructor; auto.
    subst s'. eapply exec_step_external; eauto.
    eapply external_call_symbols_preserved; eauto. apply senv_preserved.
Qed.

Theorem transf_program_correct_Asmblock: 
  forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog).
Proof.
  eapply forward_simulation_step.
  - apply senv_preserved.
  - apply transf_initial_states.
  - apply transf_final_states.
  - apply transf_step_correct.
Qed.

End PRESERVATION_ASMBLOCK.

(*
Require Import Asm.

Lemma verified_par_checks_alls_bundles lb x: forall bundle,
  verify_par lb = OK x ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  induction lb; simpl; try tauto.
  intros bundle H; monadInv H.
  destruct 1; subst; eauto.
  destruct x0; auto.
Qed.

Lemma verified_schedule_nob_checks_alls_bundles bb lb bundle:
  verified_schedule_nob bb = OK lb ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  unfold verified_schedule_nob. intros H;
  monadInv H. destruct x4.
  intros; eapply verified_par_checks_alls_bundles; eauto.
Qed.

Lemma verify_par_bblock_PExpand bb i:
  exit bb = Some (PExpand i) -> verify_par_bblock bb = OK tt.
Proof.
  destruct bb as [h bdy ext H]; simpl.
  intros; subst. destruct i.
  generalize H.
  rewrite <- wf_bblock_refl in H.
  destruct H as [H H0].
  unfold builtin_alone in H0. erewrite H0; eauto.
Qed.

Local Hint Resolve verified_schedule_nob_checks_alls_bundles: core.

Lemma verified_schedule_checks_alls_bundles bb lb bundle:
  verified_schedule bb = OK lb ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  unfold verified_schedule. remember (exit bb) as exb.
  destruct exb as [c|]; eauto.
  destruct c as [i|]; eauto.
  destruct i; intros H. inversion_clear H; simpl.
  intuition subst.
  intros; eapply verify_par_bblock_PExpand; eauto.
Qed.

Lemma transf_blocks_checks_all_bundles lbb: forall lb bundle,
  transf_blocks lbb = OK lb ->
  List.In bundle lb -> verify_par_bblock bundle = OK tt.
Proof.
  induction lbb; simpl.
  - intros lb bundle H; inversion_clear H. simpl; try tauto.
  - intros lb bundle H0.
    monadInv H0.
    rewrite in_app. destruct 1; eauto.
    eapply verified_schedule_checks_alls_bundles; eauto.
Qed.

Lemma find_bblock_Some_in lb: 
  forall ofs b, find_bblock ofs lb = Some b -> List.In b lb.
Proof.
  induction lb; simpl; try congruence.
  intros ofs b.
  destruct (zlt ofs 0); try congruence.
  destruct (zeq ofs 0); eauto.
  intros X; inversion X; eauto.
Qed.*)

(*
Section PRESERVATION_ASMVLIW.

Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Lemma all_bundles_are_checked b ofs f bundle:
  Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) ->
  find_bblock ofs (fn_blocks f) = Some bundle ->
  verify_par_bblock bundle = OK tt. 
Proof.
  unfold match_prog, match_program in TRANSL.
  unfold Genv.find_funct_ptr; simpl; intros X.
  destruct (Genv.find_def_match_2 TRANSL b) as [|f0 y H]; try congruence.
  destruct y as [tf0|]; try congruence.
  inversion X as [H1]. subst. clear X.
  remember (@Gfun fundef unit (Internal f)) as f2.
  destruct H as [ctx' f1 f2 H0|]; try congruence.
  inversion Heqf2 as [H2]. subst; clear Heqf2.
  unfold transf_fundef, transf_partial_fundef in H.
  destruct f1 as [f1|f1]; try congruence.
  unfold transf_function, transl_function in H.
  monadInv H. monadInv EQ.
  destruct (zlt Ptrofs.max_unsigned (size_blocks (fn_blocks _))); simpl in *|-; try congruence.
  injection EQ1; intros; subst.
  monadInv EQ0. simpl in * |-.
  intros; exploit transf_blocks_checks_all_bundles; eauto.
  intros; eapply find_bblock_Some_in; eauto.
Qed.

Lemma checked_bundles_are_parexec_equiv f bundle rs rs' m m':
  exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' ->
  verify_par_bblock bundle = OK tt ->
  det_parexec (globalenv (semantics tprog)) f bundle rs m rs' m'.
Proof.
  intros. unfold verify_par_bblock in H0. destruct (Asmblockdeps.bblock_para_check _) eqn:BPC; try discriminate. clear H0.
  simpl in H.
  eapply Asmblockdeps.bblock_para_check_correct; eauto.
Qed.

Lemma seqexec_parexec_equiv b ofs f bundle rs rs' m m':
  Genv.find_funct_ptr (globalenv (Asmblock.semantics tprog)) b = Some (Internal f) ->
  find_bblock (Ptrofs.unsigned ofs) (fn_blocks f) = Some bundle ->
  exec_bblock (globalenv (Asmblock.semantics tprog)) f bundle rs m = Next rs' m' ->
  det_parexec (globalenv (semantics tprog)) f bundle rs m rs' m'.
Proof.
  intros; eapply checked_bundles_are_parexec_equiv; eauto.
  eapply all_bundles_are_checked; eauto.
Qed.

Theorem transf_program_correct_Asmvliw: 
  forward_simulation (Asmblock.semantics tprog) (Asmvliw.semantics tprog).
Proof.
  eapply forward_simulation_step with (match_states:=fun (s1:Asmvliw.state) s2 => s1=s2); eauto.
  - intros; subst; auto.
  - intros s1 t s1' H s2 H0; subst; inversion H; clear H; subst; eexists; split; eauto.
    + eapply exec_step_internal; eauto.
      intros; eapply seqexec_parexec_equiv; eauto.
    + eapply exec_step_builtin; eauto.
    + eapply exec_step_external; eauto.
Qed.

End PRESERVATION_ASMVLIW.*)

Section PRESERVATION.

Variable lk: aarch64_linker.
Variables prog tprog: program.
Hypothesis TRANSL: match_prog prog tprog.
Let ge := Genv.globalenv prog.
Let tge := Genv.globalenv tprog.

Theorem transf_program_correct: 
  forward_simulation (Asmblock.semantics lk prog) (Asmblock.semantics lk tprog).
Proof.
  eapply transf_program_correct_Asmblock; eauto.
Qed.

End PRESERVATION.