Library mcertikos.ticketlog.TicketLockIntroGenLink

Require Import LinkTemplate.
Require Import MTicketLockIntro.
Require Import TicketLockIntroGen.
Require Import TicketLockIntroGenLinkSource.
Require Import MCurID.
Require Import MCurIDCSource.
Require Import MCurIDCode.
Require Import TicketLockIntroGenAsm.

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

  Lemma lock_range_val : lock_range = num_chan + num_chan + 1.
  Proof. reflexivity. Qed.

  Lemma make_program_find_symbol (CTXT md : module)(m : mem) s :
    (p <- make_program s (CTXT ⊕ (md
                                    ⊕ TICKET_LOCK_LOC ↦ ticket_lock_type) ⊕ ∅) (mcurid ⊕ L64);
      ret (Genv.init_mem p) = OK (Some m))
    → ∃ b, find_symbol s TICKET_LOCK_LOC = Some b ∧
                 ∀ index, 0 ≤ index < lock_range →
                                   Mem.valid_access m Mint32 b (index × 8) Writable ∧
                                   Mem.valid_access m Mint32 b (index × 8 + 4) Writable.
  Proof.
    intros mkprog; inv_monad´ mkprog.
    assert (mkgenv := make_program_make_globalenv _ _ _ _ mkprog0).
    pose proof mkgenv as mkgenv´.
    eapply make_globalenv_stencil_matches in mkgenv´.
    inv_make_globalenv mkgenv. subst.
    rewrite (stencil_matches_symbols _ _ mkgenv´) in ×.
    inv mkgenv´.
    eexists; split; try eassumption.
    specialize (Genv.init_mem_characterization _ _ Hbvi H0); eauto.
    unfold Genv.perm_globvar; simpl; intros [Hperm _].
    change (Z.max 16648 0) with 16648 in Hperm.
    intros; subst.
    repeat split.
    - unfold Mem.range_perm; intros; apply Hperm.
      simpl in H1.
      rewrite lock_range_val in H.
      omega.
    - replace (index × 8) with ((index × 2) × 4) by omega.
      eexists; reflexivity.
    - unfold Mem.range_perm; intros; apply Hperm.
      simpl in H1.
      rewrite lock_range_val in H.
      omega.
    - replace (index × 8 + 4) with ((index × 2 + 1) × 4) by omega.
      eexists; reflexivity.
  Qed.

  Lemma init_correct:
    init_correct_type MTicketLockIntro_module mcurid mticketlockintro.
  Proof.
    init_correct.
    -
      exploit make_program_find_symbol; eauto.
      intros (b´ & find_symbol_TICKET_LOCK_LOC & access).
      assert (b´ = b1) by congruence; subst.
      econstructor; try eassumption; intros.
      assert (Hvalid´ : 0 ≤ z < lock_range).
      { unfold index2Z in Hvalid.
        assert (index = 0 ∨ index = 1 ∨ index = 2).
        { unfold index_range in Hvalid.
          case_eq (zeq index 0); intros.
          { subst; tauto. }
          case_eq (zeq index 1); intros.
          { subst; tauto. }
          case_eq (zeq index 2); intros.
          { subst; tauto. }
          subdestruct. }
        destruct H0 as [H1a | [H1b | H1c]].
        - subst.
          unfold index_range in Hvalid.
          unfold index_incrange in Hvalid.
          simpl.
          rewrite lock_range_val.
          unfold ID_AT_range in Hvalid.
          case_eq (zle_lt 0 ofs 1); intros; subst.
          × rewrite zle_lt_true in Hvalid; try omega.
            inv Hvalid; omega.
          × subdestruct.
        - subst.
          unfold index_range in Hvalid.
          unfold index_incrange in Hvalid.
          simpl.
          rewrite lock_range_val.
          unfold ID_TCB_range in Hvalid.
          case_eq (zle_lt 0 ofs num_chan); intros; subst.
          × rewrite zle_lt_true in Hvalid; try omega.
            Opaque Z.add.
            inv Hvalid; unfold ID_AT_range.
            omega.
          × subdestruct.
        - subst.
          unfold index_range in Hvalid.
          unfold index_incrange in Hvalid.
          simpl.
          rewrite lock_range_val.
          unfold ID_SC_range in Hvalid.
          case_eq (zle_lt 0 ofs num_chan); intros; subst.
          × rewrite zle_lt_true in Hvalid; try omega.
            Opaque Z.add.
            inv Hvalid; unfold lock_TCB_range.
            unfold ID_AT_range, ID_TCB_range.
            omega.
          × subdestruct. }
      specialize (access _ Hvalid´).
      destruct access as (acc_ti & acc_nw).
      assert (readable_ti : Mem.valid_access m2 Mint32 b1 (z × 8) Readable).
      { eapply Mem.valid_access_implies; try eassumption; econstructor. }
      assert (readable_nw : Mem.valid_access m2 Mint32 b1 (z × 8 + 4) Readable).
      { eapply Mem.valid_access_implies; try eassumption; econstructor. }
      destruct (Mem.valid_access_load _ _ _ _ readable_ti) as [v_ti load_ti].
      destruct (Mem.valid_access_load _ _ _ _ readable_nw) as [v_nw load_nw].
      ∃ v_ti, v_nw.
      repeat (split; [ eassumption|]).
      rewrite ZMap.gi.
      econstructor.
  Qed.

  Ltac link_cfunction refthm codethm :=
    eapply link_compiler;
    [ Decision.decision |
      Decision.decision |
      Decision.decision |
      eassumption |
      eapply refthm |
      link_nextblock |
      link_kernel_mode |
      eapply codethm |
      sim_oplus ].
  Lemma link_correct_aux:
    link_correct_aux_type MTicketLockIntro_module mcurid mticketlockintro.
  Proof.
    link_correct_aux.
    - link_cfunction incr_now_spec_ref MCURIDCODE.incr_now_code_correct.
    - link_cfunction init_ticket_spec_ref MCURIDCODE.init_ticket_code_correct.
    - link_asmfunction incr_ticket_spec_ref incr_ticket_code_correct.
    - link_asmfunction get_now_spec_ref get_now_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type MTicketLockIntro_module mcurid mticketlockintro.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type MTicketLockIntro_module mcurid mticketlockintro.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.