Library mcertikos.devdrivers.DHandlerSwAsmData

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 Op.
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 DHandlerSw.
Require Import DHandlerSwAsmSource.
Require Import AbstractDataType.

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 := dhandlerintro_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}.

      Section GENERATE.

        Require Import FutureTactic.

        Require Import CommonTactic.
        Lemma serial_intr_handler_asm_spec_inv´:
          ∀ rs rs´ d d´,
            serial_intr_handler_asm_spec rs d = Some (d´, rs´) →
            (ikern d = true ∧
             ihost d = true ∧
             init d = true ∧
             in_intr d = true ∧
             ∃ d1 d2 d3 d4 d5,
               save_context_spec rs d = d1 ∧
               d1 {ioapic / s / IoApicEnables [4%nat]: false} {intr_flag: true} = d2 ∧
               lapic_eoi_spec d2 = Some d3 ∧
               cons_intr_aux d3 = Some d4 ∧
               d4 {ioapic / s / IoApicEnables [4%nat]: true} = d5 ∧
               restore_context_spec d5 = (rs´, d´)).
        Proof.
          intros rs rs´ d d´.
          unfold serial_intr_handler_asm_spec.
          intros H.
          split; [subdestruct; auto|].
          split; [subdestruct; auto|].
          split; [subdestruct; auto|].
          split; [subdestruct; auto|].
          subdestruct.
          repeat esplit.
          eassumption.
          eassumption.
          inv H.
          assumption.
        Qed.

        Lemma serial_intr_handler_asm_generate:
          ∀ r´ (m0: mem) labd labd´ r´0,
            serial_intr_handler_asm_spec r´ labd = Some (labd´, r´0)
            → low_level_invariant (Mem.nextblock m0) labd
            → high_level_invariant labd
            → ∃ labd0 labd1,
                 save_context_spec r´ labd = labd0
                 ∧ serial_intr_handler_sw_spec labd0 = Some labd1
                 ∧ restore_context_spec labd1 = (r´0, labd´)
                 ∧ ikern labd = true
                 ∧ ihost labd = true
                 ∧ ikern labd0 = true
                 ∧ ihost labd0 = true
                 ∧ ikern labd1 = true
                 ∧ ihost labd1 = true.
        Proof.
          intros r´ m0 labd labd´ r´0 Hspec Hhigh Hlow.
          apply serial_intr_handler_asm_spec_inv´ in Hspec.
          blast Hspec.
          esplit. esplit.
          split. eapply Hex0.
          split. unfold serial_intr_handler_sw_spec.
          if_true. if_true. if_true. if_true.
          rewrite <- Hex2 in Hex1.
          change (Z.to_nat 4) with 4%nat.
          rewrite Hex1.
          rewrite H1.
          rewrite Hex4. reflexivity.
          - functional inversion Hex0; simpl; trivial.
          - functional inversion Hex0; simpl; trivial.
          - functional inversion Hex0; simpl; trivial.
          - functional inversion Hex0; simpl; trivial.
          - split. reflexivity.
            repeat (split; [trivial|]).
            + functional inversion Hex0; simpl; trivial.
            + functional inversion Hex0; simpl; trivial.
            + subst. functional inversion H1; simpl; functional inversion H0; simpl; trivial.
            + subst. functional inversion H1; simpl; functional inversion H0; simpl; trivial.
        Qed.

      End GENERATE.

      Lemma Hsave_context:
        ∀ s ge,
          make_globalenv s (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) dhandlersw = ret ge →
          (∃ b_save_context, Genv.find_symbol ge save_context = Some b_save_context
                             ∧ Genv.find_funct_ptr ge b_save_context =
                                Some (External (EF_external save_context null_signature)))
          ∧ get_layer_primitive save_context dhandlersw = OK (Some (primcall_save_context_compatsem save_context_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive save_context dhandlersw = OK (Some (primcall_save_context_compatsem save_context_spec)))
               by (unfold dhandlersw; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hrestore_context:
        ∀ s ge,
          make_globalenv s (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) dhandlersw = ret ge →
          (∃ b_restore_context, Genv.find_symbol ge restore_context = Some b_restore_context
                             ∧ Genv.find_funct_ptr ge b_restore_context =
                                Some (External (EF_external restore_context null_signature)))
          ∧ get_layer_primitive restore_context dhandlersw = OK (Some (primcall_restore_context_compatsem restore_context_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive restore_context dhandlersw = OK (Some (primcall_restore_context_compatsem restore_context_spec)))
               by (unfold dhandlersw; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

      Lemma Hserial_intr_handler_sw:
        ∀ s ge,
          make_globalenv s (serial_intr_handler_asm ↦ serial_intr_handler_asm_function) dhandlersw = ret ge →
          (∃ b_serial_intr_handler_sw, Genv.find_symbol ge serial_intr_handler_sw = Some b_serial_intr_handler_sw
                             ∧ Genv.find_funct_ptr ge b_serial_intr_handler_sw =
                                Some (External (EF_external serial_intr_handler_sw null_signature)))
          ∧get_layer_primitive serial_intr_handler_sw dhandlersw = OK (Some (gensem serial_intr_handler_sw_spec)).
      Proof.
        intros.
        assert (Hprim: get_layer_primitive serial_intr_handler_sw dhandlersw = OK (Some (gensem serial_intr_handler_sw_spec)))
               by (unfold dhandlersw; reflexivity).
        split; try assumption.
        eapply make_globalenv_get_layer_primitive; eauto.
      Qed.

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