Library mcertikos.mm.MPTInitCode

***********************************************************************
*                                                                     *
*            The CertiKOS Certified Kit Operating System              *
*                                                                     *
*                   The FLINT Group, Yale University                  *
*                                                                     *
*  Copyright The FLINT Group, Yale University.  All rights reserved.  *
*  This file is distributed under the terms of the Yale University    *
*  Non-Commercial License Agreement.                                  *
*                                                                     *
*********************************************************************** 

Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import MPTInit.
Require Import ZArith.Zwf.
Require Import VCGen.
Require Import RealParams.
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 PTBitGenSpec.
Require Import MPTInitCSource.
Require Import AbstractDataType.

Module MPTINITCODE.

  Section WithPrimitives.

    Context `{real_params_ops: RealParamsOps}.
    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 SETBIT.

      Let L: compatlayer (cdata RData) := PTP_LOC ↦ ptp_loc_type.

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

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

      Section SetBitBody.

        Context `{Hwb: WritableBlockAllowGlobals}.

        Variable (s: stencil).

        Variable (ge: genv).

        Variable bptp_loc: block.
        Hypothesis hbptp_loc: Genv.find_symbol ge PTP_LOC = Some bptp_loc.

        Lemma set_bit_body_correct: ∀ m m´ d env le proc_index val,
                                      env = PTree.empty _ →
                                      PTree.get tproc_index le = Some (Vint proc_index) →
                                      PTree.get tval le = Some (Vint val) →
                                      Mem.store Mint32 ((m, d): mem) bptp_loc (Int.unsigned proc_index × 4) (Vint val) = Some (m´, d) →
                                      0 ≤ (Int.unsigned proc_index) < num_proc →
                                      exec_stmt ge env le ((m, d): mem) set_bit_body E0 le (m´, d) Out_normal.
        Proof.
          generalize tintsize; intro tintsize.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold set_bit_body.
          repeat vcgen.
          Opaque Z.mul.
          simpl.
          lift_unfold.
          rewrite Int.unsigned_repr.
          rewrite Z.mul_comm.
          rewrite H2.
          reflexivity.
          omega.
        Qed.

      End SetBitBody.

      Theorem set_bit_correct:
        spec_le (set_bit ↦ setbit_spec_low) (〚set_bit ↦ f_set_bit 〛L).
      Proof.
        fbigstep_pre L. destruct H0 as [H0 Heq].
        fbigstep (set_bit_body_correct (Genv.globalenv p) b0 H (fst m) (fst m´) (snd m) (PTree.empty _)
                                       (bind_parameter_temps´ (fn_params f_set_bit)
                                                              (Vint n::Vint v::nil)
                                                              (create_undef_temps (fn_temps f_set_bit)))) m.
        rewrite <- Heq.
        destruct m´; simpl in ×. congruence.
      Qed.

    End SETBIT.

    Section ISUSED.

      Let L: compatlayer (cdata RData) := PTP_LOC ↦ ptp_loc_type.

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

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

      Section IsUsedBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (s: stencil).

        Variable (ge: genv).

        Variable bptp_loc: block.
        Hypothesis hbptp_loc: Genv.find_symbol ge PTP_LOC = Some bptp_loc.

        Lemma is_used_body_correct: ∀ m d env le proc_index val,
                                      env = PTree.empty _ →
                                      PTree.get tproc_index le = Some (Vint proc_index) →
                                      Mem.load Mint32 (m, d) bptp_loc (Int.unsigned proc_index × 4) = Some (Vint val) →
                                      0 ≤ (Int.unsigned proc_index) < num_proc →
                                      ∃ le´,
                                        exec_stmt ge env le ((m, d): mem) is_used_body E0 le´ (m, d) (Out_return (Some (Vint val, tint))).
        Proof.
          generalize tintsize; intro tintsize.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold is_used_body.
          esplit.
          repeat vcgen.
          Opaque Z.mul.
          simpl.
          rewrite Int.unsigned_repr.
          rewrite Z.mul_comm.
          eassumption.
          omega.
        Qed.

      End IsUsedBody.

      Theorem is_used_correct:
        spec_le (is_used ↦ isused_spec_low) (〚is_used ↦ f_is_used 〛L).
      Proof.
        fbigstep_pre L.
        fbigstep (is_used_body_correct (Genv.globalenv p) b0 H (fst m´) (snd m´) (PTree.empty _) (bind_parameter_temps´ (fn_params f_is_used)
                                                                       (Vint n::nil)
                                                                       (create_undef_temps (fn_temps f_is_used)))) m´.
      Qed.

    End ISUSED.

  End WithPrimitives.

End MPTINITCODE.