Library mcertikos.ticketlog.QTicketLockGenAsmData

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 MHTicketLockOp.
Require Import QTicketLockGenAsmSource.
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 := mhticketlockop_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 Hacquire_shared:
        ∀ s ge,
          make_globalenv s (acquire_lock ↦ acquire_lock_function) mhticketlockop = ret ge →
          (∃ b_acquire_shared, Genv.find_symbol ge acquire_shared = Some b_acquire_shared
                                    ∧ Genv.find_funct_ptr ge b_acquire_shared =
                                       Some (External (EF_external acquire_shared acquire_shared_sig)))
          ∧ get_layer_primitive acquire_shared mhticketlockop
             = OK (Some (primcall_acquire_shared_compatsem acquire_shared_spec0)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive acquire_shared mhticketlockop
                       = OK (Some (primcall_acquire_shared_compatsem acquire_shared_spec0)))
          by (unfold mhticketlockop; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hwait_lock:
        ∀ s ge,
          make_globalenv s (acquire_lock ↦ acquire_lock_function) mhticketlockop = ret ge →
          (∃ b_wait_lock, Genv.find_symbol ge wait_lock = Some b_wait_lock
                               ∧ Genv.find_funct_ptr ge b_wait_lock =
                                  Some (External (EF_external wait_lock wait_lock_sig)))
          ∧ get_layer_primitive wait_lock mhticketlockop = OK (Some (gensem wait_hlock_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive wait_lock mhticketlockop = OK (Some (gensem wait_hlock_spec)))
          by (unfold wait_hlock_spec; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hacquire_lock:
        ∀ ge s b,
          make_globalenv s (acquire_lock ↦ acquire_lock_function) mhticketlockop = ret ge →
          find_symbol s acquire_lock = Some b →
          stencil_matches s ge →
          Genv.find_funct_ptr ge b = Some (Internal acquire_lock_function).
      Proof.
        intros.
        assert (Hmodule: get_module_function acquire_lock (acquire_lock ↦ acquire_lock_function)
                         = OK (Some acquire_lock_function))
          by apply get_module_function_mapsto.
        assert (HInternal: make_internal acquire_lock_function = OK (AST.Internal acquire_lock_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 Hrelease_shared:
        ∀ s ge,
          make_globalenv s (release_lock ↦ release_lock_function) mhticketlockop = ret ge →
          (∃ b_release_shared, Genv.find_symbol ge release_shared = Some b_release_shared
                                    ∧ Genv.find_funct_ptr ge b_release_shared =
                                       Some (External (EF_external release_shared release_shared_sig)))
          ∧ get_layer_primitive release_shared mhticketlockop
             = OK (Some (primcall_release_lock_compatsem release_shared release_shared_spec0)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive release_shared mhticketlockop
                       = OK (Some (primcall_release_lock_compatsem release_shared release_shared_spec0)))
          by (unfold mhticketlockop; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hpass_lock:
        ∀ s ge,
          make_globalenv s (release_lock ↦ release_lock_function) mhticketlockop = ret ge →
          (∃ b_pass_lock, Genv.find_symbol ge pass_lock = Some b_pass_lock
                             ∧ Genv.find_funct_ptr ge b_pass_lock =
                                Some (External (EF_external pass_lock pass_lock_sig)))
          ∧ get_layer_primitive pass_lock mhticketlockop = OK (Some (gensem pass_hlock_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive pass_lock mhticketlockop
                       = OK (Some (gensem pass_hlock_spec)))
               by (unfold mhticketlockop; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

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