Library mcertikos.layerlib.RefinementTactic

Require Import Values.
Require Import AsmX.
Require Import Coqlib.
Require Import Integers.
Require Import LAsm.
Require Import Maps.
Require Import Memory.
Require Import CommonTactic.
Require Import Smallstep.
Require Import Errors.
Require Import Events.
Require Import AuxLemma.
Require Import Globalenvs.
Require Import AuxStateDataType.
Require Import liblayers.compat.CompatGenSem.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.



Ltac accessor_prop_tac :=
repeat match goal with
         | |- ∀ _, _ ⇒ idtac
         | _ ⇒ constructor
       end; try (inversion 2); try (inversion 1); intros; trivial; try (econstructor; simpl; eauto 2; fail).

Ltac exist_simpl :=
  intros HP HR; pose proof HR as HR´; inv HR; revert HP; simpl;
  subrewrite´; intros HQ; subdestruct; simpl;
  inv HQ; simpl; refine_split; eauto 1;
  simpl; try reflexivity; eauto;
  try constructor; simpl; try reflexivity; trivial
  ;try (inv HR´; assumption; fail).

Ltac compatsim_simpl´ :=
  match goal with
    | [ |- compatsim_def _ _ _ ] ⇒
      constructor; split; try reflexivity;
      match goal with
        | |- res_le ⊤%signature _ _ ⇒
          repeat constructor
        | _ ⇒
          idtac
      end;
      try (simpl; intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2 HWB _ Hlow Hhigh Hhigh´ H Hι Hmd;
           let Hmatch1 := fresh "Hmatch_ext" in
           pose proof Hmd as Hmatch1;
           inv_generic_sem H; inv Hmd)
    | _ ⇒ idtac
  end.

Ltac reduce_to_sim_step :=
  split; simpl in *; try reflexivity;
          match goal with
          | |- (_ → _ → true = true) ∧ _ ⇒ split; [ reflexivity | idtac ]
          | |- ∃ X, Some ?Y = Some X ∧ _ ⇒ ∃ Y; split; [ reflexivity |]
          | |- res_le ⊤ _ _ ⇒ repeat constructor
          | |- res_le (@rel_top _ _) _ _ ⇒ repeat constructor
          | |- option_le _ _ _ ⇒ repeat constructor
          | _ ⇒ idtac
          end.

Ltac compatsim_simpl_inv_match H Hmd match_D :=
     let Hmatch1 := fresh "Hmatch_ext" in
     pose proof Hmd as Hmatch1; inv_generic_sem H; inv Hmd;
     match goal with
     | Hmatch´:context [match_D]
       |- _ ⇒
           let Hmatch := fresh "Hmatch" in
           pose proof Hmatch´ as Hmatch; inv Hmatch
     | _ ⇒ idtac
     end.

Ltac compatsim_simpl match_D :=
  simpl;
   match goal with
   | |- compatsim_def _ _ _ ⇒
     constructor;
     match goal with
     | |- sextcall_sim _ _ _ ⇒
       reduce_to_sim_step;
       intros s WB1 WB2 ι vargs1 m1 d1 vres1 m1´ d1´ vargs2 m2 d2 HWB _
         Hlow Hhigh Hhigh´ H Hι Hmd;
       compatsim_simpl_inv_match H Hmd match_D
     | |- sprimcall_sim _ _ _ ⇒
       reduce_to_sim_step;
       intros s ι rs1 m1 d1 rs1´ m1´ d1´ rs2 m2 d2 _
         Hlow Hhigh Hhigh´ ? H Hmd;
       compatsim_simpl_inv_match H Hmd match_D
     | |- sextcall_sprimcall_sim _ _ _ ⇒
       reduce_to_sim_step;
       intros s b ι WB1 vargs1 vargs2 vres m1 d1 m1´ d1´ rs2 m2 d2 _
         Hlow Hhigh Hhigh´ H Hmd Hsi Hpc Hι;
       compatsim_simpl_inv_match H Hmd match_D
     end
   | _ ⇒ idtac
   end.

  Ltac rewrite_store_nextblock :=
    repeat progress
           match goal with
             | [HST: Mem.store _ _ _ _ _ = Some ?m2´ |- context[Mem.nextblock ?m2´]] ⇒
               rewrite (Mem.nextblock_store _ _ _ _ _ _ HST)
             | [HST: Mem.storebytes _ _ _ _ = Some ?m2´ |- context[Mem.nextblock ?m2´]] ⇒
               rewrite (Mem.nextblock_storebytes _ _ _ _ _ HST)
           end.

  Ltac rewrite_store_outside_inject :=
    repeat progress match goal with
                      | [HST: Mem.store _ ?m2 _ _ _ = Some ?m2´|-
                         Mem.inject ?ι _ ?m2´] ⇒
                        eapply Mem.store_outside_inject in HST; try eapply HST; intros;
                        match goal with
                          | [Hsome: ι _ = _, Hperm: context[¬ Mem.perm _ _ _ _ _] |- _] ⇒
                            eapply inject_forward_equal in Hsome; eauto; inv Hsome;
                            eapply Hperm; try eassumption; simpl; eauto
                          | _ ⇒ try eassumption
                        end
                    end.

  Ltac rewrite_storebytes_outside_inject :=
    repeat progress match goal with
                      | [HST: Mem.storebytes ?m2 _ _ _ = Some ?m2´|-
                         Mem.inject ?ι _ ?m2´] ⇒
                        eapply Mem.storebytes_outside_inject in HST; try eapply HST; intros;
                        match goal with
                          | [Hsome: ι _ = _, Hperm: context[¬ Mem.perm _ _ _ _ _] |- _] ⇒
                            eapply inject_forward_equal in Hsome; eauto; inv Hsome;
                            eapply Hperm; try eassumption; simpl; eauto
                          | _ ⇒ try eassumption
                        end
                    end.

  Ltac pattern2_refinement_simpl´ relate_D:=
    match goal with
      | [HST: Mem.store _ ?m2 _ _ _ = Some ?m2´|- Mem.inject ?ι _ ?m2´] ⇒ rewrite_store_outside_inject
      | [HST: Mem.storebytes ?m2 _ _ _ = Some ?m2´|- Mem.inject ?ι _ ?m2´] ⇒ rewrite_storebytes_outside_inject
      | [Hrelate: context[relate_D] |- context[relate_D]] ⇒
        inv Hrelate; simpl in *; split; simpl; try eassumption
      | [ |- (Mem.nextblock _ ≤ Mem.nextblock ?m2´)%positive] ⇒
        rewrite_store_nextblock; try xomega
      | _ ⇒ idtac
    end.

Ltac layer_sim_simpl :=
  match goal with
    | |- sim _ (accessors ↦ _) _ ⇒
      apply cl_accessors_sim_intro
    | _ ⇒ apply layer_sim_intro; simpl
  end.


          Ltac match_external_states_simpl :=
            refine_split;
            match goal with
              | |- inject_incr ?f ?f ⇒ apply inject_incr_refl
              | _ ⇒ repeat (econstructor; eauto; try congruence)
            end;
            match goal with
              | |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
              | |- ∀ _, val_inject _ _ _ ⇒ val_inject_simpl
              | _ ⇒ idtac
            end.

        Ltac kctxt_inj_simpl :=
          eapply kctxt_inj_set; eauto;
          intros; unfold Pregmap.get in *;
          repeat (rewrite Pregmap_Simpl);
          reg_destruct_simpl.