Library mcertikos.ticketlog.TicketLockOpGenLink

Require Import LinkTemplate.
Require Import MTicketLockOp.
Require Import TicketLockOpGen.
Require Import TicketLockOpGenLinkSource.
Require Import MTicketLockIntro.
Require Import MTicketLockIntroCSource.
Require Import MTicketLockIntroCode.
Require Import MTicketLockIntroCodeTicketLockInit.

Section WITHCOMPCERTIKOS.
  Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
  Context `{wait_time: WaitTime}.
  Context `{oracle_ops0: MultiOracleOps0}.
  Context `{oracle_ops: MultiOracleOps}.
  Context `{big_ops: BigOracleOps}.

  Lemma init_correct:
    init_correct_type MTicketLockOp_module mticketlockintro mticketlockop.
  Proof.
    init_correct.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type MTicketLockOp_module mticketlockintro mticketlockop.
  Proof.
    link_correct_aux.
    - link_cfunction ticket_lock_init_spec_ref MTICKETLOCKINTROTICKETLOCKINIT.ticket_lock_init_code_correct.
    - link_cfunction pass_lock_spec_ref MTICKETLOCKINTRO.pass_lock_code_correct.
    - link_cfunction wait_lock_spec_ref MTICKETLOCKINTRO.wait_lock_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type MTicketLockOp_module mticketlockintro mticketlockop.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type MTicketLockOp_module mticketlockintro mticketlockop.
  Proof.
    make_program_exists link_correct_aux.
  Qed.
End WITHCOMPCERTIKOS.