Library mcertikos.trap.TTrapCode_syscall_dispatch

***********************************************************************
*                                                                     *
*            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 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 DispatchGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import XOmega.
Require Import TTrapCSource.
Require Import AbstractDataType.
Require Import ObjArg.
Require Import ObjTrap.
Require Import ObjSyncIPC.
Require Export TrapPrimSemantics.
Require Import CommonTactic.

Module TTRAPCODE.

  Section WithPrimitives.

    Context `{real_params: RealParams}.
    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}.

    Section SYSCALLDISPATCHC.

      Let L: compatlayer (cdata RData) := sys_proc_create trap_proccreate_compatsem trap_proc_create_spec
                                                            sys_get_quota gensem trap_get_quota_spec
                                                            sys_receive_chan gensem trap_receivechan_spec
                                                            sys_inject_event gensem trap_inject_event_spec
                                                            sys_check_int_shadow gensem trap_check_int_shadow_spec
                                                            sys_check_pending_event gensem trap_check_pending_event_spec
                                                            sys_intercept_int_window gensem trap_intercept_int_window_spec
                                                            sys_get_next_eip gensem trap_get_next_eip_spec
                                                            sys_get_reg gensem trap_get_reg_spec
                                                            sys_set_reg gensem trap_set_reg_spec
                                                            sys_set_seg gensem trap_set_seg_spec
                                                            sys_get_tsc_offset gensem trap_get_tsc_offset_spec
                                                            sys_set_tsc_offset gensem trap_set_tsc_offset_spec
                                                            sys_get_exitinfo gensem trap_get_exitinfo_spec
                                                            sys_handle_rdmsr gensem trap_handle_rdmsr_spec
                                                            sys_handle_wrmsr gensem trap_handle_wrmsr_spec
                                                            sys_mmap gensem trap_mmap_spec
                                                            sys_getc gensem sys_getc_spec
                                                            sys_putc gensem sys_putc_spec
                                                            uctx_arg1 gensem uctx_arg1_spec
                                                            uctx_set_errno gensem uctx_set_errno_spec.

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

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

      Section SyscallDispatchCBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

sys_proc_create
sys_get_quota
sys_receive_chan
sys_inject_event
sys_check_int_shadow
sys_check_pending_event
sys_intercept_int_window
sys_get_next_eip
sys_get_reg
sys_set_reg
sys_set_seg
sys_get_tsc_offset
sys_set_tsc_offset
sys_get_exitinfo
sys_handle_rdmsr
sys_handle_wrmsr
sys_mmap
sys_getc
sys_putc
uctx_arg1
uctx_set_errno

        Variable buctx_set_errno: block.

        Hypothesis huctx_set_errno1 : Genv.find_symbol ge uctx_set_errno = Some buctx_set_errno.

        Hypothesis huctx_set_errno2 : Genv.find_funct_ptr ge buctx_set_errno = Some (External (EF_external uctx_set_errno (signature_of_type (Tcons tint Tnil) tvoid cc_default)) (Tcons tint Tnil) tvoid cc_default).

        Lemma NSYS_NR_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            0 z Int.max_unsigned
            Syscall_Z2Num z = NSYS_NR
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H2.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          clear Hdestruct Hdestruct0 Hdestruct1 Hdestruct2 Hdestruct3 Hdestruct4 Hdestruct5 Hdestruct6 Hdestruct7 Hdestruct8 Hdestruct9 Hdestruct10 Hdestruct11 Hdestruct12 Hdestruct13 Hdestruct14 Hdestruct15 Hdestruct16 Hdestruct17 Hdestruct18 Hdestruct19 Hdestruct20 Hdestruct21 Hdestruct22 Hdestruct23 Hdestruct24 Hdestruct25 Hdestruct26.
          clear n3 n4 n8.
          change E0 with (E0 ** E0).
          econstructor.
          econstructor.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          change E0 with (E0 ** E0).
          econstructor.
          clear n26 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n26 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          econstructor.
          clear n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          econstructor.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n0 n.
          repeat vcgen.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n0 n.
          repeat vcgen.
          econstructor.
          clear n26 n25 n24 n23 n22 n21 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n26 n25 n24 n23 n22 n21 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          econstructor.
          clear n26 n25 n24 n23 n22 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n26 n25 n24 n23 n22 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          econstructor.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n11 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          econstructor.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n13 n12 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          econstructor.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n26 n25 n24 n23 n22 n21 n20 n19 n18 n17 n16 n15 n14 n12 n11 n10 n9 n7 n6 n5 n2 n1 n0 n.
          repeat vcgen.
          clear n0 n1 n5 n6 n9 n10 n11 n25 n26.
          repeat vcgen.
          assumption.
        Qed.

        Lemma NSYS_PUTS_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_PUTS
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_RING0_SPAWN_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_RING0_SPAWN
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_SPAWN_correct: m d le z,
            trap_proc_create_spec sc m d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_SPAWN
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_YIELD_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_YIELD
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_DISK_OP_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_DISK_OP
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_DISK_CAP_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_DISK_CAP
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GET_TSC_PER_MS_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GET_TSC_PER_MS
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GET_TSC_OFFSET_correct: m d le z,
            trap_get_tsc_offset_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GET_TSC_OFFSET
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_SET_TSC_OFFSET_correct: m d le z,
            trap_set_tsc_offset_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_SET_TSC_OFFSET
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_RUN_VM_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_RUN_VM
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GET_EXITINFO_correct: m d le z,
            trap_get_exitinfo_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GET_EXITINFO
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_MMAP_correct: m d le z,
            trap_mmap_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_MMAP
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_SET_REG_correct: m d le z,
            trap_set_reg_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_SET_REG
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GET_REG_correct: m d le z,
            trap_get_reg_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GET_REG
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_SET_SEG_correct: m d le z,
            trap_set_seg_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_SET_SEG
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GET_NEXT_EIP_correct: m d le z,
            trap_get_next_eip_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GET_NEXT_EIP
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_INJECT_EVENT_correct: m d le z,
            trap_inject_event_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_INJECT_EVENT
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_CHECK_PENDING_EVENT_correct: m d le z,
            trap_check_pending_event_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_CHECK_PENDING_EVENT
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_CHECK_INT_SHADOW_correct: m d le z,
            trap_check_int_shadow_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_CHECK_INT_SHADOW
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_INTERCEPT_INT_WINDOW_correct: m d le z,
            trap_intercept_int_window_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_INTERCEPT_INT_WINDOW
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_HANDLE_RDMSR_correct: m d le z,
            trap_handle_rdmsr_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_HANDLE_RDMSR
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_HANDLE_WRMSR_correct: m d le z,
            trap_handle_wrmsr_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_HANDLE_WRMSR
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GET_QUOTA_correct: m d le z,
            trap_get_quota_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GET_QUOTA
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_IS_CHAN_READY_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_IS_CHAN_READY
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_RECV_correct: m d le z,
            trap_receivechan_spec d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_RECV
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_SLEEP_correct: m d le z,
            uctx_set_errno_spec 3 d = Some
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_SLEEP
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          unfold Syscall_Z2Num in H1.
          subdestruct.
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_PUTC_correct: m d le z,
            sys_putc_spec d = ret
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_PUTC
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          assert (z = 28).
          {
            unfold Syscall_Z2Num in H1.
            subdestruct. assumption.
          }
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma NSYS_GETC_correct: m d le z,
            sys_getc_spec d = ret
            uctx_arg1_spec d = Some z
            Syscall_Z2Num z = NSYS_GETC
             le´,
              exec_stmt ge (PTree.empty _) le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          unfold syscall_dispatch_c_body.
          subst.
          assert (z = 27).
          {
            unfold Syscall_Z2Num in H1.
            subdestruct. assumption.
          }
          rewrite <- Int.unsigned_repr in H0 at 1.
          esplit.
          repeat vcgen.
          omega.
        Qed.

        Lemma syscall_dispatch_c_body_correct: m d env le,
            env = PTree.empty _
            sys_dispatch_c_spec sc m d = Some
            high_level_invariant d
             le´,
              exec_stmt ge env le ((m, d): mem) syscall_dispatch_c_body E0 le´ (m, ) Out_normal.
        Proof.
          generalize max_unsigned_val; intro muval.
          intros.
          subst.
          unfold sys_dispatch_c_spec in H0.
          case_eq (uctx_arg1_spec d); intros; rewrite H in H0; try discriminate H0.
          case_eq (zle_le 0 z Int.max_unsigned); intros; rewrite H2 in H0; try discriminate H0.
          case_eq (Syscall_Z2Num z); intros; rewrite H3 in H0.
          eapply NSYS_PUTS_correct; eauto.
          eapply NSYS_RING0_SPAWN_correct; eauto.
          eapply NSYS_SPAWN_correct; eauto.
          eapply NSYS_YIELD_correct; eauto.
          eapply NSYS_DISK_OP_correct; eauto.
          eapply NSYS_DISK_CAP_correct; eauto.
          eapply NSYS_GET_TSC_PER_MS_correct; eauto.
          eapply NSYS_GET_TSC_OFFSET_correct; eauto.
          eapply NSYS_SET_TSC_OFFSET_correct; eauto.
          eapply NSYS_RUN_VM_correct; eauto.
          eapply NSYS_GET_EXITINFO_correct; eauto.
          eapply NSYS_MMAP_correct; eauto.
          eapply NSYS_SET_REG_correct; eauto.
          eapply NSYS_GET_REG_correct; eauto.
          eapply NSYS_SET_SEG_correct; eauto.
          eapply NSYS_GET_NEXT_EIP_correct; eauto.
          eapply NSYS_INJECT_EVENT_correct; eauto.
          eapply NSYS_CHECK_PENDING_EVENT_correct; eauto.
          eapply NSYS_CHECK_INT_SHADOW_correct; eauto.
          eapply NSYS_INTERCEPT_INT_WINDOW_correct; eauto.
          eapply NSYS_HANDLE_RDMSR_correct; eauto.
          eapply NSYS_HANDLE_WRMSR_correct; eauto.
          eapply NSYS_GET_QUOTA_correct; eauto.
          eapply NSYS_IS_CHAN_READY_correct; eauto.
          eapply NSYS_RECV_correct; eauto.
          eapply NSYS_SLEEP_correct; eauto.
          eapply NSYS_PUTC_correct; eauto.
          eapply NSYS_GETC_correct; eauto.
          eapply NSYS_NR_correct; eauto.
        Qed.

      End SyscallDispatchCBody.

      Theorem syscall_dispatch_c_code_correct:
        spec_le (syscall_dispatch_C sys_dispatch_c_spec_low) (syscall_dispatch_C f_syscall_dispatch_c L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep (syscall_dispatch_c_body_correct s (Genv.globalenv p) makeglobalenv
        b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp
        b4 Hb4fs Hb4fp b5 Hb5fs Hb5fp b6 Hb6fs Hb6fp b7 Hb7fs Hb7fp
        b8 Hb8fs Hb8fp b9 Hb9fs Hb9fp b10 Hb10fs Hb10fp b11 Hb11fs Hb11fp
        b12 Hb12fs Hb12fp b13 Hb13fs Hb13fp b14 Hb14fs Hb14fp b15 Hb15fs Hb15fp
        b16 Hb16fs Hb16fp b17 Hb17fs Hb17fp b18 Hb18fs Hb18fp
        b19 Hb19fs Hb19fp b20 Hb20fs Hb20fp
        m´0 labd labd0 (PTree.empty _)
        (bind_parameter_temps´ (fn_params f_syscall_dispatch_c)
                               nil
                               (create_undef_temps (fn_temps f_syscall_dispatch_c)))) H0.
      Qed.

    End SYSCALLDISPATCHC.

    Section TRAPSENDTOCHANPRE.

      Let L: compatlayer (cdata RData) :=
                    uctx_arg2 gensem uctx_arg2_spec
                     uctx_arg3 gensem uctx_arg3_spec
                     uctx_arg4 gensem uctx_arg4_spec
                     syncsendto_chan_pre gensem syncsendto_chan_pre_spec.

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

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

      Section TrapSenToChanBody.

        Context `{Hwb: WritableBlockOps}.

        Variable (sc: stencil).

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

uctx_arg2
        Variable buctx_arg2: block.
        Hypothesis huctx_arg21 : Genv.find_symbol ge uctx_arg2 = Some buctx_arg2.
        Hypothesis huctx_arg22 : Genv.find_funct_ptr ge buctx_arg2 =
                                 Some (External (EF_external uctx_arg2 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_arg3
        Variable buctx_arg3: block.
        Hypothesis huctx_arg31 : Genv.find_symbol ge uctx_arg3 = Some buctx_arg3.
        Hypothesis huctx_arg32 : Genv.find_funct_ptr ge buctx_arg3 =
                                 Some (External (EF_external uctx_arg3 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

uctx_arg4
        Variable buctx_arg4: block.
        Hypothesis huctx_arg41 : Genv.find_symbol ge uctx_arg4 = Some buctx_arg4.
        Hypothesis huctx_arg42 : Genv.find_funct_ptr ge buctx_arg4 =
                                 Some (External (EF_external uctx_arg4 (signature_of_type Tnil tuint cc_default))
                                                Tnil tint cc_default).

syncsendto_chan_pre
        Variable bsyncsendto_chan_pre: block.
        Hypothesis hsyncsendto_chan_pre1 : Genv.find_symbol ge syncsendto_chan_pre = Some bsyncsendto_chan_pre.
        Hypothesis hsyncsendto_chan_pre2 : Genv.find_funct_ptr ge bsyncsendto_chan_pre =
                                    Some (External (EF_external syncsendto_chan_pre
                                                                (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
                                                   (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).

        Lemma trap_sendtochan_pre_body_correct: m d env le val,
            env = PTree.empty _
            trap_sendtochan_pre_spec d = Some (, Int.unsigned val)
             le´,
              exec_stmt ge env le ((m, d): mem) trap_sendtochan_pre_body E0 le´ (m, ) (Out_return (Some (Vint val, tint))).
        Proof.
          generalize max_unsigned_val; intro muval.
          intros; subst.
          functional inversion H0; subst.
          functional inversion H1; try subst;
          functional inversion H2; try subst;
          functional inversion H3; try subst;
          unfold trap_sendtochan_pre_body;
          esplit;
          repeat vcgen.
        Qed.

      End TrapSenToChanBody.

      Theorem trap_sendtochan_pre_code_correct:
        spec_le
          (trap_sendtochan_pre trap_sendtochan_pre_spec_low)
          (trap_sendtochan_pre f_trap_sendtochan_pre L).
      Proof.
        set ( := L) in ×. unfold L in ×.
        fbigstep_pre .
        fbigstep
          (trap_sendtochan_pre_body_correct
             s (Genv.globalenv p) makeglobalenv
             b0 Hb0fs Hb0fp
             b1 Hb1fs Hb1fp
             b2 Hb2fs Hb2fp
             b3 Hb3fs Hb3fp
             m´0 labd labd0
             (PTree.empty _)
             (bind_parameter_temps´ (fn_params f_trap_sendtochan_pre)
                                    nil
                                    (create_undef_temps (fn_temps f_trap_sendtochan_pre)))) H0.
      Qed.

    End TRAPSENDTOCHANPRE.

  End WithPrimitives.

End TTRAPCODE.