Library mcertikos.devdrivers.DAbsConsoleBuffIntroCode

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 AbstractDataType.
Require Import DAbsConsoleBuffIntroCSource.
Require Import SerialIntroGenSpec.
Require Import ObjMultiprocessor.

Module DABSCONSOLEBUFFINTROCODE.

  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 GETSERIALEXISTS.

      Let L: compatlayer (cdata RData) := serial_exists_LOC ↦ v_serial_exists.

      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 GetSerialExistsBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable (bserial_exists: block).

        Hypothesis hserial_exists_loc :
          Genv.find_symbol ge serial_exists_LOC = Some bserial_exists.

        Lemma get_serial_exists_body_correct:
          ∀ m d env le v,
            env = PTree.empty _ →
            Mem.loadv Mint32 (m, d) (Vptr bserial_exists Int.zero) = Some (Vint v) →
            exec_stmt ge env le ((m, d): mem) get_serial_exists_body E0 le (m, d)
                      (Out_return (Some (Vint v, tint))).
        Proof.
          intros m d env le z Henv Hmem. subst.
          unfold get_serial_exists_body.
          repeat vcgen.
        Qed.

      End GetSerialExistsBody.

      Theorem get_serial_exists_code_correct:
        spec_le
          (get_serial_exists ↦ get_serial_exists_spec_low)
          (〚get_serial_exists ↦ f_get_serial_exists 〛L).
      Proof.
        fbigstep_pre L.
        fbigstep
          (get_serial_exists_body_correct
             (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_get_serial_exists) nil
                                    (create_undef_temps (fn_temps f_get_serial_exists))
             )
          ) m´.
      Qed.
    End GETSERIALEXISTS.

    Section SETSERIALEXISTS.

      Let L: compatlayer (cdata RData) := serial_exists_LOC ↦ v_serial_exists.

      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 SetSerialExistsBody.

        Context `{Hwb: WritableBlockAllowGlobals}.

        Variable (sc: stencil).

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

        Variable (bserial_exists: block).

        Hypothesis hserial_exists_loc :
          Genv.find_symbol ge serial_exists_LOC = Some bserial_exists.

        Require Import Integers.
        Import DeviceStateDataType.
        Lemma set_serial_exists_body_correct:
          ∀ m m´ d env le ex,
            env = PTree.empty _ →
            high_level_invariant d →
            PTree.get _ex le = Some (Vint ex)->
            (0 < (Int.unsigned ex) ∧
              Mem.store Mint32 (m, d) bserial_exists 0 (Vint Int.one) = Some (m´, d))
              ∨
            (0 = Int.unsigned ex ∧
              Mem.store Mint32 (m, d) bserial_exists 0 (Vint Int.zero) = Some (m´, d)) →
            exec_stmt ge env le ((m, d): mem) set_serial_exists_body E0 le (m´, d)
                      Out_normal.
        Proof.
          intros. subst. unfold set_serial_exists_body.
          destruct H2 as [H | H]; destruct H as [Hexrange Hstore].
          - Case "ex <> 0".
            repeat vcgen.
          - Case "ex = 0".
            repeat vcgen.
        Qed.

      End SetSerialExistsBody.

      Theorem set_serial_exists_code_correct:
        spec_le
          (set_serial_exists ↦ set_serial_exists_spec_low)
          (〚set_serial_exists ↦ f_set_serial_exists 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´;
        destruct m; destruct m´;
        fbigstep
          (set_serial_exists_body_correct
             (Genv.globalenv p) b0 H m m0 l (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_set_serial_exists) (Vint v::nil)
                                    (create_undef_temps (fn_temps f_set_serial_exists))
             )
          ) H1.
      Qed.
    End SETSERIALEXISTS.

  End WithPrimitives.

End DABSCONSOLEBUFFINTROCODE.