Library mcertikos.ticketlog.TicketLockIntroGenAsmData

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 MCurID.
Require Import TicketLockIntroGenAsmSource.
Require Import AbstractDataType.
Require Import MultiProcessorSemantics.

Section ASM_DATA.

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

  Context `{real_params: RealParams}.
  Context `{oracle_prop: MultiOracleProp}.

    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 `{fairness: WaitTime}.
      Context `{make_program_ops: !MakeProgramOps function Ctypes.type fundef unit}.
      Context `{make_program_prf: !MakeProgram function Ctypes.type fundef unit}.

      Lemma Hlog_get:
        ∀ s ge,
          make_globalenv s (get_now ↦ get_now_function) mcurid = ret ge →
          (∃ b_log_get, Genv.find_symbol ge log_get = Some b_log_get
                             ∧ Genv.find_funct_ptr ge b_log_get =
                                Some (External (EF_external log_get log_get_sig)))
          ∧ get_layer_primitive log_get mcurid = OK (Some (primcall_atomic_GET_compatsem log_get_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive log_get mcurid = OK (Some (primcall_atomic_GET_compatsem log_get_spec)))
          by (unfold mcurid; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hget_now:
        ∀ ge s b,
          make_globalenv s (get_now ↦ get_now_function) mcurid = ret ge →
          find_symbol s get_now = Some b →
          stencil_matches s ge →
          Genv.find_funct_ptr ge b = Some (Internal get_now_function).
      Proof.
        intros.
        assert (Hmodule: get_module_function get_now (get_now ↦ get_now_function) = OK (Some get_now_function))
          by apply get_module_function_mapsto.
        assert (HInternal: make_internal get_now_function = OK (AST.Internal get_now_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_FAI:
        ∀ s ge,
          make_globalenv s (incr_ticket ↦ incr_ticket_function) mcurid = ret ge →
          (∃ b_atomic_FAI, Genv.find_symbol ge atomic_FAI = Some b_atomic_FAI
                             ∧ Genv.find_funct_ptr ge b_atomic_FAI =
                                Some (External (EF_external atomic_FAI atomic_FAI_sig)))
          ∧ get_layer_primitive atomic_FAI mcurid = OK (Some (primcall_atomic_FAI_compatsem atomic_FAI_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive atomic_FAI mcurid = OK (Some (primcall_atomic_FAI_compatsem atomic_FAI_spec)))
               by (unfold mcurid; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hincr_ticket:
        ∀ ge s b,
          make_globalenv s (incr_ticket ↦ incr_ticket_function) mcurid = ret ge →
          find_symbol s incr_ticket = Some b →
          stencil_matches s ge →
          Genv.find_funct_ptr ge b = Some (Internal incr_ticket_function).
      Proof.
        intros.
        assert (Hmodule: get_module_function incr_ticket (incr_ticket ↦ incr_ticket_function) = OK (Some incr_ticket_function))
          by apply get_module_function_mapsto.
        assert (HInternal: make_internal incr_ticket_function = OK (AST.Internal incr_ticket_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.