Library mcertikos.conlib.conmtlib.HAsmLinkTemplate

Require Export LinkTemplate.
Require Import SingleConfiguration.
Require Import HAsm.
Require Import AbstractDataType.

Section HASM.
  Context `{compcertikos_prf: CompCertiKOS}.
  Context `{real_params_prf : RealParams}.

  Context `{data1_ops: !CompatDataOps RData} `{Hdata1: !CompatData RData}.
  Context `{data2_ops: !CompatDataOps RData} `{Hdata2: !CompatData RData}.
  Context `{crel_ops: !CompatRelOps (stencil:=stencil) (cdata (cdata_ops := data1_ops) RData) (cdata (cdata_ops := data2_ops) RData)}.
  Context `{Hcrel: !CompatRel (stencil:=stencil) (cdata RData) (cdata RData)}.

  Let DH := cdata (cdata_ops := data1_ops) _.
  Let DL := cdata (cdata_ops := data2_ops) _.

  Definition cl_backward_simulation_type lm (LL: _ DL) (LH: _ DH) :=
    fun `{!LAsm.AccessorsDefined (LL ⊕ L64)}
        `{!LAsm.AccessorsDefined (LH ⊕ L64)} ⇒
    ∀ (s: stencil) (CTXT M: LAsm.module) pl ph
           (builtin_idents_norepet_prf: CompCertBuiltins.BuiltinIdentsNorepet),
      link_impl lm LL = OK M →
      ∀ `{Hsc : SingleConfiguration mem (spl_mem_ops := memory_model_ops)},
      make_program (D := cdata DH) s CTXT (LH ⊕ L64) = OK ph →
      make_program (D := cdata DL) s (CTXT ⊕ M) (LL ⊕ L64) = OK pl →
      backward_simulation
        (HAsm.semantics (LH ⊕ L64) ph)
        (HAsm.semantics (LL ⊕ L64) pl).
End HASM.

Ltac cl_backward_simulation init_correct lc :=
  let H := fresh in
  intros ? ? ? ? ? ? H;
  intros;
  eapply hasm_soundness;
  try eassumption;
  try decision;
  [ eapply lc; now eauto |
    eapply init_correct; [ | eapply make_program_oplus_right]; eassumption |
    inv_link_impl H; assumption ].