Library mcertikos.mm.ContainerIntroGenLink

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 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 I64Layer.
Require Import ContainerIntroGen.
Require Import MContainerIntro.
Require Import DAbsHandlerCSource.
Require Import DAbsHandlerCode.
Require Import ContainerIntroGenSpec.
Require Import LinkTactic.
Require Import ContainerIntroGenLinkSource.
Require Import CompCertiKOSproof.
Require Import AbstractDataType.
Require Import LinkTemplate.
Require Import FlatMemory.
Require Import Decision.
Require Import LAsmModuleSem.
Require Import Soundness.
Require Import CompatExternalCalls.
Require Import CommonTactic.
Require Import LayerCalculusLemma.
Require Import DAbsHandler.

Notation HDATA := RData.
Notation LDATA := RData.

Notation HDATAOps := (cdata (cdata_ops := mcontainerintro_data_ops) HDATA).
Notation LDATAOps := (cdata (cdata_ops := dabshandler_data_ops) LDATA).

Section WITHCOMPCERTIKOS.

  Context `{compcertikos_prf: CompCertiKOS} `{real_params_prf: RealParams}.
  Context `{oracle_prop: MultiOracleProp}.
  Lemma init_correct:
    init_correct_type MContainerIntro_module dabshandler mcontainerintro.
  Proof.
    init_correct.
    -
      intros i Hi.
      specialize (init_mem_characterization´ p b).
      unfold Genv.perm_globvar; simpl; intro Hperm.
      destruct (Hperm _ _ Hbvi Hm) as [Hperm1 [Hperm2 [Hperm3 Hperm4]]]; clear Hperm; simpl in ×.
      assert (Hwrite: ∀ ofs, (0 ≤ ofs < num_proc × CSIZE ∧ (4 | ofs)) →
                                  Mem.valid_access m2 Mint32 b ofs Writable).
      intros ofs [Hofs Hdiv].
      unfold Mem.valid_access; simpl; split; auto.
      intros ofs´ Hofs´.
      unfold Mem.range_perm, CSIZE in *; simpl in Hperm1.
      apply Hperm1.
      replace (Z.max 20480 0) with 20480; auto.
      destruct Hdiv as [n Hn]; omega.

      assert (Hquota: 0 ≤ i × CSIZE + QUOTA < num_proc × CSIZE ∧ (4 | i × CSIZE + QUOTA)).
      unfold CSIZE, QUOTA; split; try omega.
      ∃ (i×5); omega.
      assert (Husage: 0 ≤ i × CSIZE + USAGE < num_proc × CSIZE ∧ (4 | i × CSIZE + USAGE)).
      unfold CSIZE, USAGE; split; try omega.
      ∃ (i×5+1); omega.
      assert (Hparent: 0 ≤ i × CSIZE + PARENT < num_proc × CSIZE ∧ (4 | i × CSIZE + PARENT)).
      unfold CSIZE, PARENT; split; try omega.
      ∃ (i×5+2); omega.
      assert (Hnchildren: 0 ≤ i × CSIZE + NCHILDREN < num_proc × CSIZE ∧ (4 | i × CSIZE + NCHILDREN)).
      unfold CSIZE, NCHILDREN; split; try omega.
      ∃ (i×5+3); omega.
      assert (Hused: 0 ≤ i × CSIZE + USED < num_proc × CSIZE ∧ (4 | i × CSIZE + USED)).
      unfold CSIZE, USED; split; try omega.
      ∃ (i×5+4); omega.

      ∃ Int.zero, Int.zero, Int.zero, Int.zero, Int.zero.
      split.
      apply load_four_bytes_zero.
      destruct Hquota; auto.
      intros; apply (Hperm4 (eq_refl _)); unfold CSIZE, QUOTA; omega.
      split.
      apply load_four_bytes_zero.
      destruct Husage; auto.
      intros; apply (Hperm4 (eq_refl _)); unfold CSIZE, USAGE; omega.
      split.
      apply load_four_bytes_zero.
      destruct Hparent; auto.
      intros; apply (Hperm4 (eq_refl _)); unfold CSIZE, PARENT; omega.
      split.
      apply load_four_bytes_zero.
      destruct Hnchildren; auto.
      intros; apply (Hperm4 (eq_refl _)); unfold CSIZE, NCHILDREN; omega.
      split.
      apply load_four_bytes_zero.
      destruct Hused; auto.
      intros; apply (Hperm4 (eq_refl _)); unfold CSIZE, USED; omega.
      repeat (split; auto).
      rewrite ZMap.gi; constructor.
  Qed.

  Lemma link_correct_aux:
    link_correct_aux_type MContainerIntro_module dabshandler mcontainerintro.
  Proof.
    link_correct_aux.
    - link_cfunction container_node_init_spec_ref DAbsHandlerCode.container_node_init_code_correct.
    - link_cfunction container_set_nchildren_spec_ref DAbsHandlerCode.container_set_nchildren_code_correct.
    - link_cfunction container_set_usage_spec_ref DAbsHandlerCode.container_set_usage_code_correct.
    - link_cfunction container_get_parent_spec_intro_ref DAbsHandlerCode.container_get_parent_code_correct.
    - link_cfunction container_get_nchildren_spec_intro_ref DAbsHandlerCode.container_get_nchildren_code_correct.
    - link_cfunction container_get_quota_spec_intro_ref DAbsHandlerCode.container_get_quota_code_correct.
    - link_cfunction container_get_usage_spec_intro_ref DAbsHandlerCode.container_get_usage_code_correct.
    - link_cfunction container_can_consume_spec_intro_ref DAbsHandlerCode.container_can_consume_code_correct.
    - link_cfunction container_alloc_spec_intro_ref DAbsHandlerCode.container_alloc_code_correct.
    - apply passthrough_correct.
  Qed.

  Theorem cl_backward_simulation:
    cl_backward_simulation_type MContainerIntro_module dabshandler mcontainerintro.
  Proof.
    cl_backward_simulation init_correct link_correct_aux.
  Qed.

  Theorem make_program_exists:
    make_program_exist_type MContainerIntro_module dabshandler mcontainerintro.
  Proof.
    make_program_exists link_correct_aux.
  Qed.

End WITHCOMPCERTIKOS.