Library mcertikos.trap.PIPCCode

Require Import TacticsForTesting.
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 Clight.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Ctypes.
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 TrapArgGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import XOmega.
Require Import PIPCCSource.
Require Import AbstractDataType.
Require Import PIPC.
Require Import ObjTrap.
Require Import ObjArg.
Require Import GlobalOracleProp.
Require Import SingleOracle.

Module PIPCCODE.

  Section WithPrimitives.

    Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
    Context `{Hmwd: UseMemWithData memb}.

    Context `{single_oracle_prop: SingleOracleProp}.
    Context `{real_params : RealParams}.
    Context `{multi_oracle_prop: MultiOracleProp}.

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


    Section UCTXARG1.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_get ↦ gensem thread_uctx_get_spec.

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

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

      Section UctxArg1Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_get: block.

        Hypothesis huctx_get1 : Genv.find_symbol ge uctx_get = Some buctx_get.

        Hypothesis huctx_get2 : Genv.find_funct_ptr ge buctx_get = Some (External (EF_external uctx_get (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default)) (Tcons tint (Tcons tint Tnil)) tint cc_default).

        Lemma uctx_arg1_body_correct: ∀ m d env le arg,
                                        env = PTree.empty _ →
                                        uctx_arg1_spec d = Some (Int.unsigned arg) →
                                        high_level_invariant d →
                                        ∃ le´,
                                          exec_stmt ge env le ((m, d): mem) uctx_arg1_body E0 le´ (m, d) (Out_return (Some (Vint arg, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H1; assumption).
          unfold uctx_arg1_body.
          functional inversion H0; subst.
          assert(ipt: ipt d = true).
            destruct H1.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H3, H5, H6.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          unfold thread_uctx_get_spec.
          rewrite zeq_true.
          rewrite H6.
          unfold ObjProc.uctx_get_spec.
          rewrite H3, H4, H5, ipt, H7, H8, H9.
          rewrite zle_lt_true; auto.
          unfold is_UCTXT_ptr.
          f_equal.
          f_equal.
          auto.
          omega.
          omega.
        Qed.

      End UctxArg1Body.

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

    End UCTXARG1.

    Section UCTXARG2.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_get ↦ gensem thread_uctx_get_spec.

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

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

      Section UctxArg2Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_get: block.

        Hypothesis huctx_get1 : Genv.find_symbol ge uctx_get = Some buctx_get.

        Hypothesis huctx_get2 : Genv.find_funct_ptr ge buctx_get = Some (External (EF_external uctx_get (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default)) (Tcons tint (Tcons tint Tnil)) tint cc_default).

        Lemma uctx_arg2_body_correct: ∀ m d env le arg,
                                        env = PTree.empty _ →
                                        uctx_arg2_spec d = Some (Int.unsigned arg) →
                                        high_level_invariant d →
                                        ∃ le´,
                                          exec_stmt ge env le ((m, d): mem) uctx_arg2_body E0 le´ (m, d) (Out_return (Some (Vint arg, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H1; assumption).
          unfold uctx_arg2_body.
          functional inversion H0; subst.
          assert(ipt: ipt d = true).
            destruct H1.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H3, H5, H6.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          unfold thread_uctx_get_spec.
          rewrite zeq_true.
          rewrite H6.
          unfold ObjProc.uctx_get_spec.
          rewrite H3, H5, ipt, H7, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite H4.
          rewrite zle_lt_true.
          f_equal.
          f_equal.
          assumption.
          omega.
          omega.
          omega.
        Qed.

      End UctxArg2Body.

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

    End UCTXARG2.

    Section UCTXARG3.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_get ↦ gensem thread_uctx_get_spec.

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

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

      Section UctxArg3Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_get: block.

        Hypothesis huctx_get1 : Genv.find_symbol ge uctx_get = Some buctx_get.

        Hypothesis huctx_get2 : Genv.find_funct_ptr ge buctx_get = Some (External (EF_external uctx_get (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default)) (Tcons tint (Tcons tint Tnil)) tint cc_default).

        Lemma uctx_arg3_body_correct: ∀ m d env le arg,
                                        env = PTree.empty _ →
                                        uctx_arg3_spec d = Some (Int.unsigned arg) →
                                        high_level_invariant d →
                                        ∃ le´,
                                          exec_stmt ge env le ((m, d): mem) uctx_arg3_body E0 le´ (m, d) (Out_return (Some (Vint arg, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H1; assumption).
          unfold uctx_arg3_body.
          functional inversion H0; subst.
          assert(ipt: ipt d = true).
            destruct H1.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H3, H5, H6.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          rewrite Int.unsigned_repr.
          unfold thread_uctx_get_spec.
          rewrite zeq_true.
          rewrite H6.
          unfold ObjProc.uctx_get_spec.
          rewrite H3, H4, H5, ipt, H7, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite zle_lt_true.
          f_equal.
          f_equal.
          assumption.
          omega.
          omega.
        Qed.

      End UctxArg3Body.

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

    End UCTXARG3.

    Section UCTXARG4.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_get ↦ gensem thread_uctx_get_spec.

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

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

      Section UctxArg4Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_get: block.

        Hypothesis huctx_get1 : Genv.find_symbol ge uctx_get = Some buctx_get.

        Hypothesis huctx_get2 : Genv.find_funct_ptr ge buctx_get = Some (External (EF_external uctx_get (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default)) (Tcons tint (Tcons tint Tnil)) tint cc_default).

        Lemma uctx_arg4_body_correct: ∀ m d env le arg,
                                        env = PTree.empty _ →
                                        uctx_arg4_spec d = Some (Int.unsigned arg) →
                                        high_level_invariant d →
                                        ∃ le´,
                                          exec_stmt ge env le ((m, d): mem) uctx_arg4_body E0 le´ (m, d) (Out_return (Some (Vint arg, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H1; assumption).
          unfold uctx_arg4_body.
          functional inversion H0; subst.
          assert(ipt: ipt d = true).
            destruct H1.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H3, H5, H6.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          rewrite Int.unsigned_repr.
          unfold thread_uctx_get_spec.
          rewrite zeq_true.
          rewrite H6.
          unfold ObjProc.uctx_get_spec.
          rewrite H3, H4, H5, ipt, H7, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite zle_lt_true.
          f_equal.
          f_equal.
          assumption.
          omega.
          omega.
        Qed.

      End UctxArg4Body.

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

    End UCTXARG4.

    Section UCTXSETERRNO.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_set ↦ gensem thread_uctx_set_spec.

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

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

      Section UctxSetErronoBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_set: block.

        Hypothesis huctx_set1 : Genv.find_symbol ge uctx_set = Some buctx_set.

        Hypothesis huctx_set2 : Genv.find_funct_ptr ge buctx_set = Some (External (EF_external uctx_set (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).

        Lemma uctx_set_errno_body_correct: ∀ m d d´ env le errno,
                                             env = PTree.empty _ →
                                             PTree.get terrno le = Some (Vint errno) →
                                             uctx_set_errno_spec (Int.unsigned errno) d = Some d´ →
                                             high_level_invariant d →
                                             ∃ le´,
                                               exec_stmt ge env le ((m, d): mem) uctx_set_errno_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H2; assumption).
          unfold uctx_set_errno_body.
          functional inversion H1; subst.
          assert(ipt: ipt d = true).
            destruct H2.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H4, H6, H7.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          unfold thread_uctx_set_spec.
          rewrite zeq_true.
          rewrite H7.
          unfold ObjProc.uctx_set_spec.
          rewrite H4, H5, H6, ipt, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite zle_lt_true.
          unfold uctx´.
          reflexivity.
          omega.
          omega.
          omega.
        Qed.

      End UctxSetErronoBody.

      Theorem uctx_set_errno_code_correct:
        spec_le (uctx_set_errno ↦ uctx_set_errno_spec_low) (〚uctx_set_errno ↦ f_uctx_set_errno 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (uctx_set_errno_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_uctx_set_errno)
                                                               (Vint arg::nil)
                                                               (create_undef_temps (fn_temps f_uctx_set_errno)))) H0.
      Qed.

    End UCTXSETERRNO.

    Section UCTXSETRETVAL1.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_set ↦ gensem thread_uctx_set_spec.

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

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

      Section UctxSetRetval1Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_set: block.

        Hypothesis huctx_set1 : Genv.find_symbol ge uctx_set = Some buctx_set.

        Hypothesis huctx_set2 : Genv.find_funct_ptr ge buctx_set = Some (External (EF_external uctx_set (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).

        Lemma uctx_set_retval1_body_correct: ∀ m d d´ env le retval,
                                               env = PTree.empty _ →
                                               PTree.get tretval le = Some (Vint retval) →
                                               uctx_set_retval1_spec (Int.unsigned retval) d = Some d´ →
                                               high_level_invariant d →
                                               ∃ le´,
                                                 exec_stmt ge env le ((m, d): mem) uctx_set_retval1_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H2; assumption).
          unfold uctx_set_retval1_body.
          functional inversion H1; subst.
          assert(ipt: ipt d = true).
            destruct H2.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H4, H6, H7.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          unfold thread_uctx_set_spec.
          rewrite zeq_true.
          rewrite H7.
          unfold ObjProc.uctx_set_spec.
          rewrite H4, H5, H6, ipt, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite zle_lt_true.
          unfold uctx´.
          reflexivity.
          omega.
          omega.
          omega.
        Qed.

      End UctxSetRetval1Body.

      Theorem uctx_set_retval1_code_correct:
        spec_le (uctx_set_retval1 ↦ uctx_set_retval1_spec_low) (〚uctx_set_retval1 ↦ f_uctx_set_retval1 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (uctx_set_retval1_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_uctx_set_retval1)
                                                               (Vint arg::nil)
                                                               (create_undef_temps (fn_temps f_uctx_set_retval1)))) H0.
      Qed.

    End UCTXSETRETVAL1.

    Section UCTXSETRETVAL2.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_set ↦ gensem thread_uctx_set_spec.

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

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

      Section UctxSetRetval2Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_set: block.

        Hypothesis huctx_set1 : Genv.find_symbol ge uctx_set = Some buctx_set.

        Hypothesis huctx_set2 : Genv.find_funct_ptr ge buctx_set = Some (External (EF_external uctx_set (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).

        Lemma uctx_set_retval2_body_correct: ∀ m d d´ env le retval,
                                               env = PTree.empty _ →
                                               PTree.get tretval le = Some (Vint retval) →
                                               uctx_set_retval2_spec (Int.unsigned retval) d = Some d´ →
                                               high_level_invariant d →
                                               ∃ le´,
                                                 exec_stmt ge env le ((m, d): mem) uctx_set_retval2_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H2; assumption).
          unfold uctx_set_retval2_body.
          functional inversion H1; subst.
          assert(ipt: ipt d = true).
            destruct H2.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H4, H6, H7.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          rewrite Int.unsigned_repr.
          unfold thread_uctx_set_spec.
          rewrite zeq_true.
          rewrite H7.
          unfold ObjProc.uctx_set_spec.
          rewrite H4, H5, H6, ipt, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite zle_lt_true.
          unfold uctx´.
          reflexivity.
          omega.
          omega.
        Qed.

      End UctxSetRetval2Body.

      Theorem uctx_set_retval2_code_correct:
        spec_le (uctx_set_retval2 ↦ uctx_set_retval2_spec_low) (〚uctx_set_retval2 ↦ f_uctx_set_retval2 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (uctx_set_retval2_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_uctx_set_retval1)
                                                               (Vint arg::nil)
                                                               (create_undef_temps (fn_temps f_uctx_set_retval2)))) H0.
      Qed.

    End UCTXSETRETVAL2.

    Section UCTXSETRETVAL3.

      Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
           ⊕ uctx_set ↦ gensem thread_uctx_set_spec.

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

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

      Section UctxSetRetval3Body.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

        Variable bget_curid: block.

        Hypothesis hget_curid1 : Genv.find_symbol ge get_curid = Some bget_curid.

        Hypothesis hget_curid2 : Genv.find_funct_ptr ge bget_curid = Some (External (EF_external get_curid (signature_of_type Tnil tint cc_default)) Tnil tint cc_default).

        Variable buctx_set: block.

        Hypothesis huctx_set1 : Genv.find_symbol ge uctx_set = Some buctx_set.

        Hypothesis huctx_set2 : Genv.find_funct_ptr ge buctx_set = Some (External (EF_external uctx_set (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) Tvoid cc_default).

        Lemma uctx_set_retval3_body_correct: ∀ m d d´ env le retval,
                                               env = PTree.empty _ →
                                               PTree.get tretval le = Some (Vint retval) →
                                               uctx_set_retval3_spec (Int.unsigned retval) d = Some d´ →
                                               high_level_invariant d →
                                               ∃ le´,
                                                 exec_stmt ge env le ((m, d): mem) uctx_set_retval3_body E0 le´ (m, d´) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          assert(cid_range: 0 ≤ ZMap.get (CPU_ID d) (cid d) < num_proc) by (destruct H2; assumption).
          unfold uctx_set_retval3_body.
          functional inversion H1; subst.
          assert(ipt: ipt d = true).
            destruct H2.
            rewrite <- valid_ikern_ipt0.
            assumption.
          unfold curid, cpu in ×.
          esplit.
          repeat vcgen.
          unfold thread_get_curid_spec.
          unfold ObjMultiprocessor.get_curid_spec.
          rewrite H4, H6, H7.
          rewrite Int.unsigned_repr.
          reflexivity.
          omega.
          rewrite Int.unsigned_repr.
          unfold thread_uctx_set_spec.
          rewrite zeq_true.
          rewrite H7.
          unfold ObjProc.uctx_set_spec.
          rewrite H4, H5, H6, ipt, H8, H9.
          unfold is_UCTXT_ptr.
          rewrite zle_lt_true.
          unfold uctx´.
          reflexivity.
          omega.
          omega.
        Qed.

      End UctxSetRetval3Body.

      Theorem uctx_set_retval3_code_correct:
        spec_le (uctx_set_retval3 ↦ uctx_set_retval3_spec_low) (〚uctx_set_retval3 ↦ f_uctx_set_retval3 〛L).
      Proof.
        set (L´ := L) in ×. unfold L in ×.
        fbigstep_pre L´.
        fbigstep (uctx_set_retval3_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_uctx_set_retval1)
                                                               (Vint arg::nil)
                                                               (create_undef_temps (fn_temps f_uctx_set_retval3)))) H0.
      Qed.

    End UCTXSETRETVAL3.

  End WithPrimitives.

End PIPCCODE.