Library mcertikos.devdrivers.DLApicCode_cons_init

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import FutureTactic.
Require Import List.

Require Import AbstractDataType.
Require Import DLApicCSource.
Require Import ConsoleGenSpec.
Require Import ObjSerialDriver.
Require Import ObjConsole.
Require Import DLApic.
Require Import INVLemmaDevice.
Require Import DeviceStateDataType.

Require Import TacticsForTesting.
Require Import OracleInstances.

Module DLAPICCODE.

  Section WithPrimitives.

    Context `{real_params: RealParams}.
    Context `{oracle_prop: MultiOracleProp}.
    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.

    Let mem := mwd (cdata RData).

    Context `{Hstencil: Stencil}.
    Context `{make_program_ops: !MakeProgramOps Clight.function type Clight.fundef type}.
    Context `{Hmake_program: !MakeProgram Clight.function type Clight.fundef type}.

    Local Open Scope Z_scope.


    Section CONSINIT.
      Let L: compatlayer (cdata RData) :=
        cons_buf_init ↦ gensem cons_buf_init_spec
                          ⊕ serial_init ↦ gensem serial_init_spec.

      Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.

      Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.

      Local Open Scope Z_scope.

      Section ConsInitBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

        Variables (ge: genv)
                  (STENCIL_MATCHES: stencil_matches sc ge).

        Variable (bcons_buf_init: block).
        Hypothesis hcons_buf_init1 : Genv.find_symbol ge cons_buf_init = Some bcons_buf_init.
        Hypothesis hcons_buf_init2 : Genv.find_funct_ptr ge bcons_buf_init =
                                     Some (External (EF_external cons_buf_init
                                                                 (signature_of_type Tnil tvoid cc_default))
                                                    Tnil tvoid cc_default).

        Variable bserial_init: block.
        Hypothesis hserial_init1: Genv.find_symbol ge serial_init = Some bserial_init.
        Hypothesis hserial_init2: Genv.find_funct_ptr ge bserial_init =
                                  Some (External (EF_external serial_init
                                                              (signature_of_type Tnil tvoid cc_default))
                                                 Tnil tvoid cc_default).

        Function cons_init_spec_aux (abd: RData) : option RData :=
          match cons_buf_init_spec abd with
          | Some abd´ ⇒ serial_init_spec abd´
          | _ ⇒ None
          end.

        Lemma cons_init_body_correct_aux:
          ∀ m d d´ env le,
            env = PTree.empty _ →
            high_level_invariant d →
            cons_init_spec_aux d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) cons_init_body E0 le´ (m, d´)
                        Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros m d d´ env le Henv Hinv Hspec.
          functional inversion Hspec; subst.
          esplit.
          unfold cons_init_body.
          repeat vcgen.
        Qed.

        Lemma cons_init_body_correct_eq:
          ∀ d,
            high_level_invariant d →
            cons_init_spec d = cons_init_spec_aux d.
        Proof.
          intros.
          inversion H.
          unfold cons_init_spec_aux, cons_init_spec.
          unfold cons_buf_init_spec, serial_init_spec.
          destruct d; simpl.
          destruct ikern, init, ihost; simpl; reflexivity.
        Qed.


        Lemma cons_init_body_correct:
          ∀ m d d´ env le,
            env = PTree.empty _ →
            high_level_invariant d →
            cons_init_spec d = Some d´ →
            ∃ le´,
              exec_stmt ge env le ((m, d): mem) cons_init_body E0 le´ (m, d´)
                        Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros m d d´ env le Henv Hinv Hspec.
          rewrite cons_init_body_correct_eq in Hspec; auto.
          apply cons_init_body_correct_aux; assumption.
        Qed.

     End ConsInitBody.

     Theorem cons_init_code_correct:
        spec_le
          (cons_init ↦ cons_init_spec_low)
          (〚cons_init ↦ f_cons_init 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep
          (cons_init_body_correct
             s
             (Genv.globalenv p)
             makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m´0 labd labd´ (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_cons_init) (nil)
                                    (create_undef_temps (fn_temps f_cons_init))
             )
          ) H0.
      Qed.

    End CONSINIT.

  End WithPrimitives.

End DLAPICCODE.