Library mcertikos.mcslock.MCSLockIntroGenAsmData

Require Import Coqlib.
Require Import Errors.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Op.
Require Import Locations.
Require Import AuxStateDataType.
Require Import Events.
Require Import Globalenvs.
Require Import Smallstep.
Require Import Values.
Require Import Memory.
Require Import Maps.
Require Import FlatMemory.
Require Import RefinementTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import Constant.
Require Import AsmImplLemma.
Require Import AsmImplTactic.
Require Import GlobIdent.
Require Import CommonTactic.

Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compcertx.MakeProgram.
Require Import LAsmModuleSem.
Require Import LAsm.
Require Import liblayers.compat.CompatGenSem.
Require Import PrimSemantics.
Require Import Conventions.

Require Import AbstractDataType.

Require Import MCSMCurID.
Require Import MCSLockIntroGenAsmSource.

Section ASM_DATA.

  Local Open Scope string_scope.
  Local Open Scope error_monad_scope.
  Local Open Scope Z_scope.

  Context `{real_params: RealParams}.
  Context `{mcs_oracle_prop: MCSOracleProp}.

  Notation LDATA := RData.
  Notation LDATAOps := (cdata (cdata_ops := mcurid_data_ops) LDATA).

  Section WITHMEM.

    Context `{Hstencil: Stencil}.
    Context `{Hmem: Mem.MemoryModelX}.
    Context `{Hmwd: UseMemWithData mem}.
    Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
    Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

    Lemma Hatomic_mcs_log:
      ∀ s ge,
        make_globalenv s (mcs_log ↦ mcs_log_function) mcurid = ret ge →
        (∃ b_atomic_mcs_log, Genv.find_symbol ge atomic_mcs_log = Some b_atomic_mcs_log
                                  ∧ Genv.find_funct_ptr ge b_atomic_mcs_log =
                                     Some (External (EF_external atomic_mcs_log atomic_mcs_log_sig)))
        ∧ get_layer_primitive atomic_mcs_log mcurid = OK (Some (primcall_atomic_mcs_log_compatsem atomic_mcs_log_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive atomic_mcs_log mcurid
                     = OK (Some (primcall_atomic_mcs_log_compatsem atomic_mcs_log_spec)))
        by (unfold mcurid; reflexivity).
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hmcs_log:
      ∀ ge s b,
        make_globalenv s (mcs_log ↦ mcs_log_function) mcurid = ret ge →
        find_symbol s mcs_log = Some b →
        stencil_matches s ge →
        Genv.find_funct_ptr ge b = Some (Internal mcs_log_function).
    Proof.
      intros.
      assert (Hmodule: get_module_function mcs_log (mcs_log ↦ mcs_log_function)
                       = OK (Some mcs_log_function))
        by apply get_module_function_mapsto.
      assert (HInternal: make_internal mcs_log_function = OK (AST.Internal mcs_log_function)) by reflexivity.
      eapply make_globalenv_get_module_function in H; eauto.
      destruct H as [?[Hsymbol ?]].
      inv H1.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H0 in Hsymbol. inv Hsymbol.
      assumption.
    Qed.

    Lemma Hatomic_mcs_CAS:
      ∀ s ge,
        make_globalenv s (mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function) mcurid = ret ge →
        (∃ b_atomic_mcs_CAS, Genv.find_symbol ge atomic_mcs_CAS = Some b_atomic_mcs_CAS
                                  ∧ Genv.find_funct_ptr ge b_atomic_mcs_CAS =
                                     Some (External (EF_external atomic_mcs_CAS atomic_mcs_CAS_sig)))
        ∧ get_layer_primitive atomic_mcs_CAS mcurid = OK (Some (primcall_atomic_mcs_CAS_compatsem atomic_mcs_CAS_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive atomic_mcs_CAS mcurid
                     = OK (Some (primcall_atomic_mcs_CAS_compatsem atomic_mcs_CAS_spec)))
        by (unfold mcurid; reflexivity).
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hmcs_CAS_TAIL:
      ∀ ge s b,
        make_globalenv s (mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function) mcurid = ret ge →
        find_symbol s mcs_CAS_TAIL = Some b →
        stencil_matches s ge →
        Genv.find_funct_ptr ge b = Some (Internal mcs_CAS_TAIL_function).
    Proof.
      intros.
      assert (Hmodule: get_module_function mcs_CAS_TAIL (mcs_CAS_TAIL ↦ mcs_CAS_TAIL_function)
                       = OK (Some mcs_CAS_TAIL_function))
        by apply get_module_function_mapsto.
      assert (HInternal: make_internal mcs_CAS_TAIL_function = OK (AST.Internal mcs_CAS_TAIL_function)) by reflexivity.
      eapply make_globalenv_get_module_function in H; eauto.
      destruct H as [?[Hsymbol ?]].
      inv H1.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H0 in Hsymbol. inv Hsymbol.
      assumption.
    Qed.

    Lemma Hatomic_mcs_SWAP:
      ∀ s ge,
        make_globalenv s (mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function) mcurid = ret ge →
        (∃ b_atomic_mcs_SWAP, Genv.find_symbol ge atomic_mcs_SWAP = Some b_atomic_mcs_SWAP
                                   ∧ Genv.find_funct_ptr ge b_atomic_mcs_SWAP =
                                      Some (External (EF_external atomic_mcs_SWAP atomic_mcs_SWAP_sig)))
        ∧ get_layer_primitive atomic_mcs_SWAP mcurid = OK (Some (primcall_atomic_mcs_SWAP_compatsem atomic_mcs_SWAP_spec)).
    Proof.
      intros.
      assert (Hprim: get_layer_primitive atomic_mcs_SWAP mcurid
                     = OK (Some (primcall_atomic_mcs_SWAP_compatsem atomic_mcs_SWAP_spec)))
        by (unfold mcurid; reflexivity).
      split; try assumption.
      eapply make_globalenv_get_layer_primitive; eauto.
    Qed.

    Lemma Hmcs_SWAP_TAIL:
      ∀ ge s b,
        make_globalenv s (mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function) mcurid = ret ge →
        find_symbol s mcs_SWAP_TAIL = Some b →
        stencil_matches s ge →
        Genv.find_funct_ptr ge b = Some (Internal mcs_SWAP_TAIL_function).
    Proof.
      intros.
      assert (Hmodule: get_module_function mcs_SWAP_TAIL (mcs_SWAP_TAIL ↦ mcs_SWAP_TAIL_function)
                       = OK (Some mcs_SWAP_TAIL_function))
        by apply get_module_function_mapsto.
      assert (HInternal: make_internal mcs_SWAP_TAIL_function = OK (AST.Internal mcs_SWAP_TAIL_function)) by reflexivity.
      eapply make_globalenv_get_module_function in H; eauto.
      destruct H as [?[Hsymbol ?]].
      inv H1.
      rewrite stencil_matches_symbols in Hsymbol.
      rewrite H0 in Hsymbol. inv Hsymbol.
      assumption.
    Qed.

  End WITHMEM.

End ASM_DATA.