Library mcertikos.mm.DAbsHandlerCode

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 Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
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 TacticsForTesting.
Require Import Ctypes.

Require Import DAbsHandlerCSource.
Require Import DAbsHandler.
Require Import ContainerIntroGenSpec.

Require Import AbstractDataType.

Module DAbsHandlerCode.

  Open Scope Z_scope.

  Definition QUOTA := 0.
  Definition USAGE := 4.
  Definition PARENT := 8.
  Definition NCHILDREN := 12.
  Definition USED := 16.
  Definition CSIZE := 20.

  Lemma convert_quota : i, Int.unsigned i < num_proc
    Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 0) = Int.unsigned i × CSIZE + QUOTA.
  Proof.
    intros i Hi.
    assert (Hrange:= Int.unsigned_range_2 i).
    rewrite Int.mul_signed.
    rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
    rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
  Qed.

  Lemma convert_usage : i, Int.unsigned i < num_proc
    Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 4) = Int.unsigned i × CSIZE + USAGE.
  Proof.
    intros i Hi.
    assert (Hrange:= Int.unsigned_range_2 i).
    rewrite Int.mul_signed.
    rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
    rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
  Qed.

  Lemma convert_parent : i, Int.unsigned i < num_proc
    Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 8) = Int.unsigned i × CSIZE + PARENT.
  Proof.
    intros i Hi.
    assert (Hrange:= Int.unsigned_range_2 i).
    rewrite Int.mul_signed.
    rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
    rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
  Qed.

  Lemma convert_nchildren : i, Int.unsigned i < num_proc
    Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 12) = Int.unsigned i × CSIZE + NCHILDREN.
  Proof.
    intros i Hi.
    assert (Hrange:= Int.unsigned_range_2 i).
    rewrite Int.mul_signed.
    rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
    rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
  Qed.

  Lemma convert_used : i, Int.unsigned i < num_proc
    Int.unsigned (Int.mul i (Int.repr 20)) + Int.unsigned (Int.repr 16) = Int.unsigned i × CSIZE + USED.
  Proof.
    intros i Hi.
    assert (Hrange:= Int.unsigned_range_2 i).
    rewrite Int.mul_signed.
    rewrite 2 Int.signed_eq_unsigned; try rewrite max_signed_val; try omega.
    rewrite 3 Int.unsigned_repr; eauto; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
    rewrite Int.unsigned_repr; try rewrite max_unsigned_val; try omega.
  Qed.

  Close Scope Z_scope.

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

    Opaque PTree.get PTree.set.

    Local Open Scope Z_scope.


    Section ContainerAlloc.

      Let L: compatlayer (cdata RData) := AC_LOC container_loc_type.

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

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

      Section AllocBody.

        Context `{Hwb: WritableBlockOps}.
        Context `{Hwbg: WritableBlockAllowGlobals WB}.

        Variable (s: stencil).

        Variables (ge: genv) (b_ac: block).

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_alloc_body_correct0:
           m d env i u,
            env = PTree.empty _
            0 Int.unsigned i < num_proc
            Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
            Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint u) →
            exec_stmt ge env (PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))
                      (m,d) container_alloc_body E0
                      (PTree.set t_q (Vint u) (PTree.set t_u (Vint u)
                         (PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))))
                      (m,d) (Out_return (Some (Vzero,tint))).
        Proof.
          intros m d env i u Henv Hi Hl1 Hl2; subst.
          assert (Hmax:= max_unsigned_val).
          replace E0 with (E0 ** E0 ** E0); auto.
          vcgen; vcgen; [|vcgen].
          {
            vcgen; vcgen; vcgen; try solve [vcgen].
            vcgen.
            vcgen; vcgen.
            vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            repeat vcgen.
            vcgen.
            apply deref_loc_copy; auto.
            eapply deref_loc_value; simpl; auto.
            unfold lift; unfold align; simpl; repeat vcgen.
            rewrite Z.mul_comm; apply Hl1. }
          {
            vcgen.
            vcgen; vcgen; vcgen; try solve [vcgen].
            vcgen.
            vcgen; vcgen.
            vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            repeat vcgen.
            vcgen.
            apply deref_loc_copy; auto.
            simpl; unfold lift; unfold align; simpl; repeat vcgen.
            rewrite Z.mul_comm; apply Hl2. }
          
          apply exec_Sseq_2; try discriminate; repeat vcgen.
        Qed.

        Lemma container_alloc_body_correct1:
           m d env i u q,
            env = PTree.empty _
            0 Int.unsigned i < num_proc
            Int.unsigned u < Int.unsigned q
            Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
            Mem.load Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint q) →
            Mem.store Mint32 (m,d) b_ac (Int.unsigned i × CSIZE + USAGE) (Vint (Int.add u Int.one)) = Some (,d)
            exec_stmt ge env (PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))
                      (m,d) container_alloc_body E0
                      (PTree.set t_q (Vint q) (PTree.set t_u (Vint u)
                         (PTree.set _id (Vint i) (create_undef_temps (fn_temps f_container_alloc)))))
                      (,d) (Out_return (Some (Vone,tint))).
        Proof.
          intros m d env i u q Henv Hi Hlt Hl1 Hl2 Hs; subst.
          assert (Hmax:= max_unsigned_val).
          replace E0 with (E0 ** E0 ** E0 ** E0 ** E0); auto.
          vcgen; vcgen; [|vcgen]; [| |vcgen]; [| | |vcgen].
          {
            vcgen; vcgen; vcgen; try solve [vcgen].
            vcgen.
            vcgen; vcgen.
            vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            vcgen.
            vcgen.
            apply deref_loc_copy; auto.
            eapply deref_loc_value; simpl; auto.
            unfold lift; unfold align; simpl; repeat vcgen.
            rewrite Z.mul_comm; apply Hl1. }
          {
            vcgen.
            vcgen; vcgen; vcgen; try solve [vcgen].
            vcgen.
            vcgen; vcgen.
            vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            repeat vcgen.
            vcgen.
            apply deref_loc_copy; auto.
            simpl; unfold lift; unfold align; simpl; repeat vcgen.
            rewrite Z.mul_comm; apply Hl2. }
          {
            repeat vcgen. }
          {
            vcgen.
            vcgen; vcgen; vcgen; vcgen; vcgen; vcgen; eauto; try discriminate.
            apply deref_loc_reference; auto.
            repeat vcgen.
            vcgen.
            repeat vcgen.
            vcgen.
            simpl; repeat vcgen.
            rewrite Z.mul_comm.
            simpl in *; unfold lift in *; simpl in ×.
            rewrite Int.unsigned_repr.
            rewrite <- Int.unsigned_one; rewrite <- Int.add_unsigned.
            unfold CSIZE, USAGE in Hs; rewrite Hs; eauto.
            omega. }
          
          repeat vcgen.
        Qed.

      End AllocBody.

      Theorem container_alloc_code_correct:
        spec_le (container_alloc container_alloc_spec_low)
                (container_alloc f_container_alloc L).
      Proof.
        fbigstep_pre L.
        { econstructor; eauto.
          simpl; unfold type_of_function; auto.
          simpl; auto.
          econstructor; eauto.
          repeat constructor; simpl; auto.
          intros a1 a2 Ha1 Ha2.
          inv Ha1.
          inv Ha2; try discriminate.
          inv H4; try discriminate.
          inv H5.
          inv H4.
          assert (Hexec:= container_alloc_body_correct0 _ _ H (fst ) (snd ) (PTree.empty _) i u).
          replace (fst , snd ) with in Hexec; [| destruct ; auto].
          simpl in *; apply Hexec; auto.
          simpl; split; auto; discriminate.
          simpl; auto. }
        { econstructor; eauto.
          simpl; unfold type_of_function; auto.
          simpl; auto.
          econstructor; eauto.
          repeat constructor; simpl; auto.
          intros a1 a2 Ha1 Ha2.
          inv Ha1.
          inv Ha2; try discriminate.
          inv H6; try discriminate.
          inv H7.
          inv H6.
          assert (Hexec:= container_alloc_body_correct1 _ _ H (fst m) (fst ) (snd m) (PTree.empty _) i u q).
          replace (fst m, snd m) with m in Hexec; [| destruct m; auto].
          simpl in *; apply Hexec; auto.
          unfold lift in *; simpl in ×.
          destruct H4 as [H4 _].
          destruct ; destruct m; simpl in ×.
          unfold ContainerIntroGenSpec.CSIZE in ×.
          unfold ContainerIntroGenSpec.USAGE in ×.
          unfold CSIZE, USAGE.
          rewrite H4; auto.
          simpl; split; auto; discriminate.
          simpl; destruct H4 as [_ H4].
          destruct ; simpl in *; subst; auto. }
      Qed.

    End ContainerAlloc.


    Section ContainerCanConsume.

      Let L: compatlayer (cdata RData) := AC_LOC container_loc_type.

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

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

      Section CanConsumeBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (s: stencil).

        Variables (ge: genv) (b_ac: block).

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_can_consume_body_correct:
           m d env le i n q u,
            env = PTree.empty _le ! _id = Some (Vint i) → le ! _n = Some (Vint n) →
            0 Int.unsigned i < num_proc
            Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint q) →
            Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint u) →
            exec_stmt ge env le (m, d) container_can_consume_body E0 le (m, d)
              (Out_return (Some (Vint
                 (match (Int.unsigned n <=? Int.unsigned q,
                         Int.unsigned u <=? Int.unsigned q - Int.unsigned n) with
                  | (true, true)Int.one
                  | _Int.zero end), tint))).
        Proof.
          intros; subst.

          assert (((Int.unsigned n <=? Int.unsigned q) = true
                   (Int.unsigned u <=? Int.unsigned q - Int.unsigned n) = true)
                  ((Int.unsigned n <=? Int.unsigned q) = true
                   (Int.unsigned u <=? Int.unsigned q - Int.unsigned n) = false)
                  (Int.unsigned n <=? Int.unsigned q) = false) as Hcases.
          destruct (Int.unsigned n <=? Int.unsigned q); auto.
          destruct (Int.unsigned u <=? Int.unsigned q - Int.unsigned n); auto.

          destruct Hcases as [Hcase1|Hcase2].
          destruct Hcase1 as [Hle1 Hle2].
          rewrite Hle1; rewrite Hle2.
          vcgen; vcgen; try discriminate.
          vcgen; simpl.
          { vcgen; vcgen; eauto.
            vcgen; vcgen.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            simpl; unfold sem_add; simpl; unfold align; simpl.
            rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
            apply deref_loc_copy; auto.
            apply deref_loc_value with (chunk := Mint32); auto.
            unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
            rewrite Int.add_unsigned.
            rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
              unfold CSIZE; unfold QUOTA; omega.
            vcgen. }
          { vcgen; simpl; unfold bool_val; simpl.
            destruct (zlt (Int.unsigned q) (Int.unsigned n)); simpl; unfold Int.eq.
            rewrite Z.leb_le in Hle1; omega.
            destruct (zeq (Int.unsigned Int.one) (Int.unsigned Int.zero)); simpl.
            inv e.
            eauto. }
          { vcgen; simpl.
            vcgen.
            vcgen.
            vcgen.
            vcgen; vcgen.
            vcgen.
            vcgen.
            vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            simpl; unfold sem_add; simpl; unfold align; simpl.
            rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
            apply deref_loc_copy; auto.
            vcgen.
            vcgen.
            apply deref_loc_value with (chunk := Mint32); auto.
            unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
            rewrite Int.add_unsigned.
            rewrite Int.unsigned_repr; rewrite convert_usage; try rewrite max_unsigned_val; eauto;
              unfold CSIZE; unfold USAGE; omega.
            vcgen.
            vcgen.
            vcgen.
            vcgen.
            vcgen; vcgen.
            vcgen.
            vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            simpl; unfold sem_add; simpl; unfold align; simpl.
            rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
            apply deref_loc_copy; auto.
            vcgen.
            vcgen.
            apply deref_loc_value with (chunk := Mint32); auto.
            unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
            rewrite Int.add_unsigned.
            rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
              unfold CSIZE; unfold QUOTA; omega.
            vcgen; eauto.
            vcgen.
            vcgen.
            simpl.
            rewrite Int.unsigned_repr.
            destruct (zlt (Int.unsigned q - Int.unsigned n) (Int.unsigned u)).
            rewrite Z.leb_le in Hle2; omega.
            vcgen.
            rewrite Z.leb_le in Hle1; assert (Hrange := Int.unsigned_range_2 q).
            rewrite max_unsigned_val in Hrange |- ×.
            split; try omega.
            apply Z.le_trans with (m := Int.unsigned q); try omega.
            assert (Hrange´ := Int.unsigned_range_2 n); omega.
            simpl; vcgen; vcgen. }

          
          replace E0 with (E0 ** E0).
          vcgen; vcgen.
          { destruct Hcase2 as [[Hle1 Hle2]|Hle].

            vcgen.
            {
              vcgen; vcgen; eauto.
              vcgen.
              vcgen.
              vcgen; vcgen.
              vcgen; vcgen; eauto.
              apply deref_loc_reference; auto.
              vcgen; eauto.
              simpl; unfold sem_add; simpl; unfold align; simpl.
              rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
              apply deref_loc_copy; auto.
              vcgen.
              vcgen.
              apply deref_loc_value with (chunk := Mint32); auto.
              unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
              rewrite Int.add_unsigned.
              rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
                unfold CSIZE; unfold QUOTA; omega.
              vcgen; eauto.
            }
            {
              simpl; destruct (zlt (Int.unsigned q) (Int.unsigned n)).
              rewrite Z.leb_le in Hle1; omega.
              vcgen.
            }
            {
              vcgen.
              vcgen; vcgen; eauto.
              vcgen.
              vcgen.
              vcgen; vcgen.
              vcgen; vcgen; eauto.
              apply deref_loc_reference; auto.
              vcgen; eauto.
              simpl; unfold sem_add; simpl; unfold align; simpl.
              rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
              apply deref_loc_copy; auto.
              vcgen.
              vcgen.
              apply deref_loc_value with (chunk := Mint32); auto.
              unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
              rewrite Int.add_unsigned.
              rewrite Int.unsigned_repr; rewrite convert_usage; try rewrite max_unsigned_val; eauto;
                unfold CSIZE; unfold USAGE; omega.
              vcgen; eauto.
              vcgen.
              vcgen.
              vcgen.
              vcgen.
              vcgen; vcgen.
              vcgen.
              vcgen; eauto.
              apply deref_loc_reference; auto.
              vcgen; eauto.
              simpl; unfold sem_add; simpl; unfold align; simpl.
              rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
              apply deref_loc_copy; auto.
              vcgen.
              vcgen.
              apply deref_loc_value with (chunk := Mint32); auto.
              unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
              rewrite Int.add_unsigned.
              rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
                unfold CSIZE; unfold QUOTA; omega.
              vcgen; eauto.
              vcgen.
              vcgen.
              simpl.
              rewrite Int.unsigned_repr.
              destruct (zlt (Int.unsigned q - Int.unsigned n) (Int.unsigned u)).
              vcgen.
              rewrite Z.leb_nle in Hle2; omega.
              rewrite Z.leb_le in Hle1; assert (Hrange := Int.unsigned_range_2 q).
              rewrite max_unsigned_val in Hrange |- ×.
              split; try omega.
              apply Z.le_trans with (m := Int.unsigned q); try omega.
              assert (Hrange´ := Int.unsigned_range_2 n); omega.
              simpl; vcgen. }

            
            vcgen.
            vcgen; vcgen; eauto.
            vcgen.
            vcgen.
            vcgen; vcgen.
            vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            simpl; unfold sem_add; simpl; unfold align; simpl.
            rewrite Int.add_zero_l; rewrite Int.mul_commut; auto.
            apply deref_loc_copy; auto.
            vcgen.
            vcgen.
            apply deref_loc_value with (chunk := Mint32); auto.
            unfold Mem.loadv; unfold align; simpl; unfold lift; simpl.
            rewrite Int.add_unsigned.
            rewrite Int.unsigned_repr; rewrite convert_quota; try rewrite max_unsigned_val; eauto;
              unfold CSIZE; unfold QUOTA; omega.
            vcgen; eauto.
            simpl.
            destruct (zlt (Int.unsigned q) (Int.unsigned n)).
            vcgen.
            rewrite Z.leb_nle in Hle; omega.
            simpl; vcgen. }
          { destruct Hcase2 as [[Hle1 Hle2]|Hle].
            rewrite Hle1; rewrite Hle2; vcgen; vcgen.
            rewrite Hle; vcgen; vcgen. }
          { simpl; auto. }
        Qed.

      End CanConsumeBody.

      Theorem container_can_consume_code_correct:
        spec_le (container_can_consume container_can_consume_spec_low)
                (container_can_consume f_container_can_consume L).
      Proof.
        fbigstep_pre L.
        fbigstep (container_can_consume_body_correct _ _ H (fst ) (snd ) (PTree.empty _)
                   (bind_parameter_temps´ (fn_params f_container_can_consume)
                   (Vint i :: Vint n :: nil) (PTree.empty _))) .
      Qed.

    End ContainerCanConsume.


    Section ContainerNodeInit.

      Let L: compatlayer (cdata RData) :=
        AC_LOC container_loc_type.

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

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

      Section InitBody.

        Context `{Hwb: WritableBlockAllowGlobals}.

        Variable (s: stencil).

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

        Variables b_ac : block.

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_node_init_body_correct:
           (d : cdata RData) env le i quota_v parent_v m m1 m2 m3 m4 ,
            env = PTree.empty _
            le ! _id = Some (Vint i) →
            le ! _q_val = Some (Vint quota_v) →
            le ! _p_val = Some (Vint parent_v) →
            0 Int.unsigned i < num_proc
            Mem.store Mint32 m b_ac (Int.unsigned i × CSIZE + QUOTA) (Vint quota_v) = Some m1
            Mem.store Mint32 m1 b_ac (Int.unsigned i × CSIZE + USAGE) (Vint Int.zero) = Some m2
            Mem.store Mint32 m2 b_ac (Int.unsigned i × CSIZE + PARENT) (Vint parent_v) = Some m3
            Mem.store Mint32 m3 b_ac (Int.unsigned i × CSIZE + NCHILDREN) (Vint Int.zero) = Some m4
            Mem.store Mint32 m4 b_ac (Int.unsigned i × CSIZE + USED) (Vint Int.one) = Some
            exec_stmt ge env le (m, d) container_set_values_body E0 le (, d) Out_normal.
        Proof.
          intros; subst.
          assert (Hmax:= max_unsigned_val).
          assert (AC_size : (sizeof t_struct_AC) = 20).
          { simpl; auto. }
          unfold Int.zero in *; unfold Int.one in ×.
          unfold container_set_values_body.
          unfold exec_stmt.
          replace E0 with (E0 ** E0); auto.
          econstructor.
          {
            vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold QUOTA, CSIZE in H4.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H4 by omega.
            rewrite H4.
            unfold set; simpl; auto.
            Transparent Z.mul. }
          replace E0 with (E0 ** E0); auto.
          vcgen.
          {
            vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold USAGE, CSIZE in H5.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H5 by omega.
            rewrite H5; simpl; auto.
            Transparent Z.mul. }
          replace E0 with (E0 ** E0); auto.
          vcgen.
          {
            vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold PARENT, CSIZE in H6.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H6 by omega.
            rewrite H6; simpl; auto.
            Transparent Z.mul. }
          replace E0 with (E0 ** E0); auto.
          vcgen.
          {
            vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold NCHILDREN, CSIZE in H7.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H7 by omega.
            rewrite H7; simpl; auto.
            Transparent Z.mul. }
          {
            vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold USED, CSIZE in H8.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H8 by omega.
            rewrite H8; simpl; auto.
            Transparent Z.mul. }
        Qed.

      End InitBody.

      Theorem container_node_init_code_correct:
        spec_le (container_node_init container_init_node_spec_low)
                (container_node_init f_container_set_values L).
      Proof.
        fbigstep_pre L.
        econstructor; eauto.
        simpl; unfold type_of_function; auto.
        simpl; auto.
        simpl.
        eapply eval_funcall_internal; eauto.
        constructor; eauto.
        simpl.
        constructor; eauto.
        simpl.
        constructor; eauto.
        intro contra.
        unfold _id, _p_val, _q_val in contra.
        simpl in contra.
        destruct contra; [ inv H7 | destruct H7; [inv H7 | auto]].
        econstructor; eauto.
        simpl.
        unfold _p_val, _q_val.
        intro contra.
        destruct contra; try inv H7; auto.
        econstructor; eauto.
        econstructor; eauto.
        simpl.
        unfold list_disjoint; intros.
        inv H8.
        econstructor.
        simpl.
        econstructor.
        assert (Hexec:= container_node_init_body_correct (Genv.globalenv p) b0 H labd
                                                         (PTree.empty _)
                                                         (PTree.set _p_val (Vint parent_val)
                                                         (PTree.set _q_val (Vint quota_val)
                                                                    (PTree.set _id (Vint i) (PTree.empty val))))
               i quota_val parent_val m0 m1 m2 m3 m4 m´0).
        unfold exec_stmt in Hexec.
        eapply Hexec; eauto.
        simpl; eauto.
        simpl; eauto.
      Qed.

    End ContainerNodeInit.


    Section ContainerSetUsage.

      Let L: compatlayer (cdata RData) :=
        AC_LOC container_loc_type.

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

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

      Section SETUSAGEBody.

        Context `{Hwb: WritableBlockAllowGlobals}.

        Variable (s: stencil).

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

        Variables b_ac : block.

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_set_usage_body_correct:
           (d : cdata RData) env le i usage_val m ,
            env = PTree.empty _
            le ! _id = Some (Vint i) →
            le ! _usage_val = Some (Vint usage_val) →
            0 Int.unsigned i < num_proc
            Mem.store Mint32 m b_ac (Int.unsigned i × CSIZE + USAGE) (Vint usage_val) = Some
            exec_stmt ge env le (m, d) container_set_usage_body E0 le (, d) Out_normal.
        Proof.
          intros; subst.
          assert (Hmax:= max_unsigned_val).
          assert (AC_size : (sizeof t_struct_AC) = 20).
          { simpl; auto. }
          unfold Int.zero in *; unfold Int.one in ×.
          unfold container_set_usage_body.
          unfold exec_stmt.
          {
            vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold USAGE, CSIZE in H3.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H3 by omega.
            rewrite H3.
            unfold set; simpl; auto.
            Transparent Z.mul. }
        Qed.

      End SETUSAGEBody.

      Theorem container_set_usage_code_correct:
        spec_le (container_set_usage container_set_usage_spec_low)
                (container_set_usage f_container_set_usage L).
      Proof.
        fbigstep_pre L.
        econstructor; eauto.
        simpl; unfold type_of_function; auto.
        simpl; auto.
        simpl.
        eapply eval_funcall_internal; eauto.
        constructor; eauto.
        simpl.
        constructor; eauto.
        simpl.
        constructor; eauto.
        unfold _id, _usage_val.
        intros contra.
        simpl in contra.
        destruct contra; [ inv H3 | auto].
        econstructor; eauto.
        simpl.
        econstructor; eauto.
        unfold list_disjoint; intros.
        simpl in H3, H4; contradiction.
        econstructor.
        simpl.
        econstructor.
        assert (Hexec:= container_set_usage_body_correct (Genv.globalenv p) b0 H labd
                                                         (PTree.empty _)
                                                         (PTree.set _usage_val (Vint usage_val)
                                                                    (PTree.set _id (Vint i) (PTree.empty val)))
                                                         i usage_val m0 m´0).
        unfold exec_stmt in Hexec.
        eapply Hexec; eauto.
        simpl; eauto.
        simpl; eauto.
      Qed.

    End ContainerSetUsage.

    Section ContainerSetNchildren.

      Let L: compatlayer (cdata RData) :=
        AC_LOC container_loc_type.

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

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

      Section SETNCHILDRENBody.

        Context `{Hwb: WritableBlockAllowGlobals}.

        Variable (s: stencil).

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

        Variables b_ac : block.

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_set_nchildren_body_correct:
           (d : cdata RData) env le i next_child cur_num m ,
            env = PTree.empty _
            PTree.get _id le = Some (Vint i) →
            PTree.get _next_child le = Some (Vint next_child) →
            0 Int.unsigned i < num_proc
            Mem.load Mint32 m b_ac (Int.unsigned i × CSIZE + NCHILDREN) = Some (Vint cur_num) →
            Mem.store Mint32 m b_ac (Int.unsigned i × CSIZE + NCHILDREN) (Vint (Int.add cur_num Int.one)) = Some
             le´, exec_stmt ge env le (m, d) container_set_nchildren_body E0 le´ (, d) Out_normal.
        Proof.
          intros; subst.
          assert (Hmax:= max_unsigned_val).
          assert (AC_size : (sizeof t_struct_AC) = 20).
          { simpl; auto. }
          unfold Int.zero in *; unfold Int.one in ×.
          unfold container_set_nchildren_body.
          esplit.
          unfold exec_stmt.
          replace E0 with (E0 ** E0); auto.
          econstructor.
          {
            vcgen; vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.loadv; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold CSIZE, NCHILDREN in H3.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H3 by omega.
            rewrite H3.
            unfold set; simpl; auto.
            Transparent Z.mul. }
          { vcgen; vcgen; vcgen; try eapply hac_loc1.
            vcgen; vcgen; vcgen; vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen.
            vcgen.
            rewrite AC_size.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            repeat vcgen.
            Opaque Z.mul.
            unfold Mem.storev; simpl; unfold lift; simpl.
            rewrite Int.unsigned_repr; try omega.
            unfold CSIZE, NCHILDREN in H4.
            replace (Int.unsigned i × 20) with (20 × Int.unsigned i) in H4 by omega.
            unfold Int.add in H4.
            rewrite Int.unsigned_repr in H4.
            rewrite H4; auto.
            omega. }
        Qed.

      End SETNCHILDRENBody.

      Theorem container_set_nchildren_code_correct:
        spec_le (container_set_nchildren container_set_nchildren_spec_low)
                (container_set_nchildren f_container_set_nchildren L).
      Proof.
        fbigstep_pre L.

        assert (Hexec:= container_set_nchildren_body_correct (Genv.globalenv p) b0 H labd
                                                             (PTree.empty _)
                                                             (bind_parameter_temps´
                                                                (fn_params f_container_set_nchildren)
                                                                (Vint i::(Vint next_child::nil))
                                                                (create_undef_temps (fn_temps f_container_set_nchildren)))
                                                             i next_child cur_num m0 m´0).
        edestruct Hexec as (le´ & Hexec´); eauto.
        unfold exec_stmt in Hexec.
        econstructor; eauto.
        simpl; unfold type_of_function; auto.
        simpl; auto.
        simpl.
        eapply eval_funcall_internal; eauto.
        constructor; eauto.
        simpl.
        constructor; eauto.
        simpl.
        constructor; eauto.
        unfold _next_child, _id.
        intros contra.
        simpl in contra.
        destruct contra; [ inv H4 | auto].
        econstructor; eauto.
        simpl.
        econstructor; eauto.
        unfold list_disjoint; intros.
        simpl in H4, H5.
        unfold _cur_num in H5.
        unfold _id in H4.
        unfold _next_child in H4.
        destruct H5; auto.
        destruct H4; auto.
        rewrite <- H4, <- H5; intro contra; inv contra.
        destruct H4; auto.
        rewrite <- H4, <- H5; intro contra; inv contra.
        econstructor.
        simpl; eauto.
      Qed.

    End ContainerSetNchildren.


    Section ContainerGetParent.

      Let L: compatlayer (cdata RData)
        := AC_LOC container_loc_type.

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

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

      Section GetParentBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (s: stencil).

        Variables (ge: genv) (b_ac: block).

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_get_parent_body_correct:
           m d env le v i,
            env = PTree.empty _le ! _id = Some (Vint i) →
            0 Int.unsigned i < num_proc
            Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + PARENT) = Some (Vint v) →
            exec_stmt ge env le (m, d) container_get_parent_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
        Proof.
          intros; subst.
          vcgen; vcgen; vcgen.
          vcgen; vcgen.
          { vcgen.
            vcgen.
            vcgen.
            vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            vcgen. }
          { assert (0 sizeof t_struct_AC Int.max_unsigned) as Hsize.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega.
            vcgen.
            apply deref_loc_copy; auto.
            rewrite Int.unsigned_repr; auto.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega. }
          { repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
            unfold Mem.loadv.
            rewrite Int.unsigned_repr.
            rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
            rewrite max_unsigned_val; omega. }
        Qed.

      End GetParentBody.

      Theorem container_get_parent_code_correct:
        spec_le (container_get_parent container_get_parent_spec_low)
                (container_get_parent f_container_get_parent L).
      Proof.
        fbigstep_pre L.
        fbigstep (container_get_parent_body_correct _ _ H (fst ) (snd ) (PTree.empty _)
                   (bind_parameter_temps´ (fn_params f_container_get_parent) (Vint i :: nil) (PTree.empty _))) .
      Qed.

    End ContainerGetParent.


    Section ContainerGetQuota.

      Let L: compatlayer (cdata RData) := AC_LOC container_loc_type.

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

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

      Section GetQuotaBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (s: stencil).

        Variables (ge: genv) (b_ac: block).

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_get_quota_body_correct:
           m d env le v i,
            env = PTree.empty _le ! _id = Some (Vint i) →
            0 Int.unsigned i < num_proc
            Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + QUOTA) = Some (Vint v) →
            exec_stmt ge env le (m, d) container_get_quota_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
        Proof.
          intros; subst.
          vcgen; vcgen; vcgen.
          vcgen; vcgen.
          { vcgen.
            vcgen.
            vcgen.
            vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            vcgen. }
          { assert (0 sizeof t_struct_AC Int.max_unsigned) as Hsize.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega.
            vcgen.
            apply deref_loc_copy; auto.
            rewrite Int.unsigned_repr; auto.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega. }
          { repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
            unfold Mem.loadv.
            rewrite Int.unsigned_repr.
            rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
            rewrite max_unsigned_val; omega. }
        Qed.

      End GetQuotaBody.

      Theorem container_get_quota_code_correct:
        spec_le (container_get_quota container_get_quota_spec_low)
                (container_get_quota f_container_get_quota L).
      Proof.
        fbigstep_pre L.
        fbigstep (container_get_quota_body_correct _ _ H (fst ) (snd ) (PTree.empty _)
                   (bind_parameter_temps´ (fn_params f_container_get_quota) (Vint i :: nil) (PTree.empty _))) .
      Qed.

    End ContainerGetQuota.


    Section ContainerGetUsage.

      Let L: compatlayer (cdata RData) := AC_LOC container_loc_type.

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

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

      Section GetUsageBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (s: stencil).

        Variables (ge: genv) (b_ac: block).

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_get_usage_body_correct:
           m d env le v i,
            env = PTree.empty _le ! _id = Some (Vint i) →
            0 Int.unsigned i < num_proc
            Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + USAGE) = Some (Vint v) →
            exec_stmt ge env le (m, d) container_get_usage_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
        Proof.
          intros; subst.
          vcgen; vcgen; vcgen.
          vcgen; vcgen.
          { vcgen.
            vcgen.
            vcgen.
            vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            vcgen. }
          { assert (0 sizeof t_struct_AC Int.max_unsigned) as Hsize.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega.
            vcgen.
            apply deref_loc_copy; auto.
            rewrite Int.unsigned_repr; auto.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega. }
          { repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
            unfold Mem.loadv.
            rewrite Int.unsigned_repr.
            rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
            rewrite max_unsigned_val; omega. }
        Qed.

      End GetUsageBody.

      Theorem container_get_usage_code_correct:
        spec_le (container_get_usage container_get_usage_spec_low)
                (container_get_usage f_container_get_usage L).
      Proof.
        fbigstep_pre L.
        fbigstep (container_get_usage_body_correct _ _ H (fst ) (snd ) (PTree.empty _)
                   (bind_parameter_temps´ (fn_params f_container_get_usage) (Vint i :: nil) (PTree.empty _))) .
      Qed.

    End ContainerGetUsage.


    Section ContainerGetNchildren.

      Let L: compatlayer (cdata RData) := AC_LOC container_loc_type.

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

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

      Section GetNchildrenBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (s: stencil).

        Variables (ge: genv) (b_ac: block).

        Hypothesis hac_loc1 : Genv.find_symbol ge AC_LOC = Some b_ac.

        Lemma container_get_nchildren_body_correct:
           m d env le v i,
            env = PTree.empty _le ! _id = Some (Vint i) →
            0 Int.unsigned i < num_proc
            Mem.load Mint32 (m, d) b_ac (Int.unsigned i × CSIZE + NCHILDREN) = Some (Vint v) →
            exec_stmt ge env le (m, d) container_get_nchildren_body E0 le (m, d) (Out_return (Some (Vint v, tint))).
        Proof.
          intros; subst.
          vcgen; vcgen; vcgen.
          vcgen; vcgen.
          { vcgen.
            vcgen.
            vcgen.
            vcgen; eauto.
            apply deref_loc_reference; auto.
            vcgen; eauto.
            vcgen. }
          { assert (0 sizeof t_struct_AC Int.max_unsigned) as Hsize.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega.
            vcgen.
            apply deref_loc_copy; auto.
            rewrite Int.unsigned_repr; auto.
            rewrite max_unsigned_val; rewrite sizeof_AC; omega. }
          { repeat vcgen; try rewrite sizeof_AC; try rewrite max_unsigned_val; try omega.
            unfold Mem.loadv.
            rewrite Int.unsigned_repr.
            rewrite Z.add_0_l; rewrite Z.mul_comm; auto.
            unfold CSIZE in H2. unfold NCHILDREN in H2.
            rewrite max_unsigned_val; omega. }
        Qed.

      End GetNchildrenBody.

      Theorem container_get_nchildren_code_correct:
        spec_le (container_get_nchildren container_get_nchildren_spec_low)
                (container_get_nchildren f_container_get_nchildren L).
      Proof.
        fbigstep_pre L.
        fbigstep (container_get_nchildren_body_correct _ _ H (fst ) (snd ) (PTree.empty _)
                   (bind_parameter_temps´ (fn_params f_container_get_nchildren) (Vint i :: nil) (PTree.empty _))) .
      Qed.

    End ContainerGetNchildren.



  End WithPrimitives.

End DAbsHandlerCode.