Library mcertikos.trap.TTrapArgCode
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 Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
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 TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource.
Require Import ObjTrap.
Require Import CommonTactic.
Lemma int_wrap:
Int.repr (-1) = Int.repr (Int.max_unsigned).
Proof.
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
reflexivity.
Qed.
Lemma unsigned_int_range:
∀ x: int,
0 ≤ Int.unsigned x ≤ Int64.max_unsigned.
Proof.
split.
apply Int.unsigned_range.
apply Z.le_trans with (m:=Int.max_unsigned);
( apply Int.unsigned_range_2 ||
unfold Int.max_unsigned, Int64.max_unsigned;
simpl; omega).
Qed.
Lemma cat_unsigned64_lor_range:
∀ lo hi,
0 ≤ Z.lor (Z.shiftl (Int.unsigned hi) 32) (Int.unsigned lo) ≤ Int64.max_unsigned.
Proof.
intros lo hi.
apply Z64_lor_range.
apply Z_shiftl_32_range.
apply Int.unsigned_range_2.
apply unsigned_int_range.
Qed.
Lemma unsigned_div_2pow32_eq_0:
∀ x, Int.unsigned x / 2 ^ 32 = 0.
Proof.
intro.
generalize (Int.unsigned_range x); intro.
repeat autounfold in H.
unfold two_power_nat, shift_nat in H.
simpl in H.
change (2 ^ 32) with 4294967296.
xomega.
Qed.
Lemma unsigned_shiftl_lor_shiftr_range:
∀ x y n,
0 ≤ n →
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) n) (Int.unsigned y)) n ≤ Int.max_unsigned.
Proof.
split.
- apply Z.shiftr_nonneg.
apply Z_lor_range_lo.
+ apply Z.shiftl_nonneg.
apply Int.unsigned_range.
+ apply Int.unsigned_range.
- rewrite Z.shiftr_lor.
rewrite Z.shiftr_shiftl_r.
+ rewrite Z.sub_diag with (n:=n).
rewrite Z.shiftr_0_r.
rewrite Z.shiftr_div_pow2.
apply Z_lor_range.
apply Int.unsigned_range_2.
split.
× change 0 with (0 / 2 ^ n).
apply Z_div_le.
apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
apply Int.unsigned_range.
× rewrite <- Z_div_mult_full with (a:=Int.max_unsigned)(b:=2^n).
{
apply Z_div_le.
- apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
- apply Z.le_trans with (m:=Int.max_unsigned).
+ apply Int.unsigned_range_2.
+ apply Z.le_mul_diag_r with (n:=Int.max_unsigned)(m:=2^n).
× repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
omega.
× apply Zle_lt_or_eq in H.
destruct H.
{
generalize (Z.pow_gt_1 2 n).
intro Hr.
destruct Hr.
- omega.
- apply H0 in H.
omega.
}
rewrite <- H.
simpl.
omega.
}
apply Z.pow_nonzero.
omega.
assumption.
× assumption.
+ assumption.
Qed.
Lemma unsigned_shiftl_lor_shiftr_32_range:
∀ x y,
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) 32) (Int.unsigned y)) 32 ≤ Int.max_unsigned.
Proof.
intros.
apply unsigned_shiftl_lor_shiftr_range with (n:=32).
omega.
Qed.
Lemma Z_mod_range:
∀ x n,
n > 0 →
0 ≤ x mod n ≤ n - 1.
Proof.
intros.
assert(0 ≤ x mod n < n).
apply Z_mod_lt.
omega.
omega.
Qed.
Ltac intomega :=
repeat autounfold; unfold two_power_nat, shift_nat; simpl; omega.
Hint Resolve Z_lor_range_lo.
Hint Resolve Z_land_range_lo.
Hint Resolve Z_shiftl_32_range.
Hint Resolve Int.unsigned_range_2.
Hint Resolve cat_unsigned64_lor_range.
Hint Resolve Z.shiftr_nonneg.
Hint Resolve unsigned_shiftl_lor_shiftr_range.
Hint Resolve unsigned_shiftl_lor_shiftr_32_range.
Module TTRAPARGCODE.
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 SYS_PRINT.
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 Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import compcert.lib.Integers.
Require Import ZArith.Zwf.
Require Import RealParams.
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 TacticsForTesting.
Require Import XOmega.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CLemmas.
Require Import AbstractDataType.
Require Import TTrapArg.
Require Import TrapGenSpec.
Require Import TTrapArgCSource.
Require Import ObjTrap.
Require Import CommonTactic.
Lemma int_wrap:
Int.repr (-1) = Int.repr (Int.max_unsigned).
Proof.
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
reflexivity.
Qed.
Lemma unsigned_int_range:
∀ x: int,
0 ≤ Int.unsigned x ≤ Int64.max_unsigned.
Proof.
split.
apply Int.unsigned_range.
apply Z.le_trans with (m:=Int.max_unsigned);
( apply Int.unsigned_range_2 ||
unfold Int.max_unsigned, Int64.max_unsigned;
simpl; omega).
Qed.
Lemma cat_unsigned64_lor_range:
∀ lo hi,
0 ≤ Z.lor (Z.shiftl (Int.unsigned hi) 32) (Int.unsigned lo) ≤ Int64.max_unsigned.
Proof.
intros lo hi.
apply Z64_lor_range.
apply Z_shiftl_32_range.
apply Int.unsigned_range_2.
apply unsigned_int_range.
Qed.
Lemma unsigned_div_2pow32_eq_0:
∀ x, Int.unsigned x / 2 ^ 32 = 0.
Proof.
intro.
generalize (Int.unsigned_range x); intro.
repeat autounfold in H.
unfold two_power_nat, shift_nat in H.
simpl in H.
change (2 ^ 32) with 4294967296.
xomega.
Qed.
Lemma unsigned_shiftl_lor_shiftr_range:
∀ x y n,
0 ≤ n →
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) n) (Int.unsigned y)) n ≤ Int.max_unsigned.
Proof.
split.
- apply Z.shiftr_nonneg.
apply Z_lor_range_lo.
+ apply Z.shiftl_nonneg.
apply Int.unsigned_range.
+ apply Int.unsigned_range.
- rewrite Z.shiftr_lor.
rewrite Z.shiftr_shiftl_r.
+ rewrite Z.sub_diag with (n:=n).
rewrite Z.shiftr_0_r.
rewrite Z.shiftr_div_pow2.
apply Z_lor_range.
apply Int.unsigned_range_2.
split.
× change 0 with (0 / 2 ^ n).
apply Z_div_le.
apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
apply Int.unsigned_range.
× rewrite <- Z_div_mult_full with (a:=Int.max_unsigned)(b:=2^n).
{
apply Z_div_le.
- apply Z.lt_gt.
apply Z.pow_pos_nonneg; omega.
- apply Z.le_trans with (m:=Int.max_unsigned).
+ apply Int.unsigned_range_2.
+ apply Z.le_mul_diag_r with (n:=Int.max_unsigned)(m:=2^n).
× repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
omega.
× apply Zle_lt_or_eq in H.
destruct H.
{
generalize (Z.pow_gt_1 2 n).
intro Hr.
destruct Hr.
- omega.
- apply H0 in H.
omega.
}
rewrite <- H.
simpl.
omega.
}
apply Z.pow_nonzero.
omega.
assumption.
× assumption.
+ assumption.
Qed.
Lemma unsigned_shiftl_lor_shiftr_32_range:
∀ x y,
0 ≤ Z.shiftr (Z.lor (Z.shiftl (Int.unsigned x) 32) (Int.unsigned y)) 32 ≤ Int.max_unsigned.
Proof.
intros.
apply unsigned_shiftl_lor_shiftr_range with (n:=32).
omega.
Qed.
Lemma Z_mod_range:
∀ x n,
n > 0 →
0 ≤ x mod n ≤ n - 1.
Proof.
intros.
assert(0 ≤ x mod n < n).
apply Z_mod_lt.
omega.
omega.
Qed.
Ltac intomega :=
repeat autounfold; unfold two_power_nat, shift_nat; simpl; omega.
Hint Resolve Z_lor_range_lo.
Hint Resolve Z_land_range_lo.
Hint Resolve Z_shiftl_32_range.
Hint Resolve Int.unsigned_range_2.
Hint Resolve cat_unsigned64_lor_range.
Hint Resolve Z.shiftr_nonneg.
Hint Resolve unsigned_shiftl_lor_shiftr_range.
Hint Resolve unsigned_shiftl_lor_shiftr_32_range.
Module TTRAPARGCODE.
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 SYS_PRINT.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem get_curid_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ device_output ↦ gensem device_output_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 PrintBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
get_curid
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 tuint cc_default))
Tnil tint cc_default).
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 tuint cc_default))
Tnil tint cc_default).
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 tint cc_default))
Tnil tint cc_default).
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 tint cc_default))
Tnil tint cc_default).
device_output
Variable bdevice_output: block.
Hypothesis hdevice_output1 : Genv.find_symbol ge device_output = Some bdevice_output.
Hypothesis hdevice_output2 : Genv.find_funct_ptr ge bdevice_output =
Some (External (EF_external device_output
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))
tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tvoid cc_default).
Hypothesis hdevice_output1 : Genv.find_symbol ge device_output = Some bdevice_output.
Hypothesis hdevice_output2 : Genv.find_funct_ptr ge bdevice_output =
Some (External (EF_external device_output
(signature_of_type (Tcons tuint (Tcons tuint (Tcons tuint Tnil)))
tvoid cc_default))
(Tcons tuint (Tcons tuint (Tcons tuint Tnil))) tvoid cc_default).
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).
Require Import AuxLemma.
Require Import CommonTactic.
Lemma print_correct:
∀ m d d' env le,
env = PTree.empty _ →
print_spec d = Some d' →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) print_body E0 le' (m, d') Out_normal.
Proof.
intros; subst.
unfold print_body.
functional inversion H0.
esplit.
assert (0 ≤ cid d ≤ Int.max_unsigned) as curid_range.
{ pose proof (valid_curid _ H1) as valid_curid.
rewrite_omega.
}
d3 vcgen.
{ repeat vcgen.
unfold get_curid_spec.
functional inversion H2; subst. subrewrite'.
instantiate (1 := Int.repr (cid d)).
rewrite Int.unsigned_repr; auto.
}
assert (0 ≤ content ≤ Int.max_unsigned)
as (content_range).
{ functional inversion H2; subst.
repeat discharge_unsigned_range.
}
repeat vcgen.
{
instantiate (1 := Int.repr content).
rewrite Int.unsigned_repr; auto.
}
rewrite Int.unsigned_repr; auto.
Qed.
End PrintBody.
Theorem print_code_correct:
spec_le (print ↦ print_spec_low)
(〚print ↦ f_print 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(print_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m'0 labd labd'
(PTree.empty _)
(bind_parameter_temps' (fn_params f_print)
nil
(create_undef_temps (fn_temps f_print)))) H.
Qed.
End SYS_PRINT.
Section SYSGETQUOTA.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem get_curid_spec
⊕ container_get_quota ↦ gensem container_get_quota_spec
⊕ container_get_usage ↦ gensem container_get_usage_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysGetQuotaBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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).
Require Import AuxLemma.
Require Import CommonTactic.
Lemma print_correct:
∀ m d d' env le,
env = PTree.empty _ →
print_spec d = Some d' →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) print_body E0 le' (m, d') Out_normal.
Proof.
intros; subst.
unfold print_body.
functional inversion H0.
esplit.
assert (0 ≤ cid d ≤ Int.max_unsigned) as curid_range.
{ pose proof (valid_curid _ H1) as valid_curid.
rewrite_omega.
}
d3 vcgen.
{ repeat vcgen.
unfold get_curid_spec.
functional inversion H2; subst. subrewrite'.
instantiate (1 := Int.repr (cid d)).
rewrite Int.unsigned_repr; auto.
}
assert (0 ≤ content ≤ Int.max_unsigned)
as (content_range).
{ functional inversion H2; subst.
repeat discharge_unsigned_range.
}
repeat vcgen.
{
instantiate (1 := Int.repr content).
rewrite Int.unsigned_repr; auto.
}
rewrite Int.unsigned_repr; auto.
Qed.
End PrintBody.
Theorem print_code_correct:
spec_le (print ↦ print_spec_low)
(〚print ↦ f_print 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(print_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
m'0 labd labd'
(PTree.empty _)
(bind_parameter_temps' (fn_params f_print)
nil
(create_undef_temps (fn_temps f_print)))) H.
Qed.
End SYS_PRINT.
Section SYSGETQUOTA.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem get_curid_spec
⊕ container_get_quota ↦ gensem container_get_quota_spec
⊕ container_get_usage ↦ gensem container_get_usage_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysGetQuotaBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
get_curid
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 tuint cc_default))
Tnil tint cc_default).
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 tuint cc_default))
Tnil tint cc_default).
container_get_quota
Variable bcontainer_get_quota: block.
Hypothesis hcontainer_get_quota1 : Genv.find_symbol ge container_get_quota = Some bcontainer_get_quota.
Hypothesis hcontainer_get_quota2 : Genv.find_funct_ptr ge bcontainer_get_quota =
Some (External (EF_external container_get_quota
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hcontainer_get_quota1 : Genv.find_symbol ge container_get_quota = Some bcontainer_get_quota.
Hypothesis hcontainer_get_quota2 : Genv.find_funct_ptr ge bcontainer_get_quota =
Some (External (EF_external container_get_quota
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
container_get_usage
Variable bcontainer_get_usage: block.
Hypothesis hcontainer_get_usage1 : Genv.find_symbol ge container_get_usage = Some bcontainer_get_usage.
Hypothesis hcontainer_get_usage2 : Genv.find_funct_ptr ge bcontainer_get_usage =
Some (External (EF_external container_get_usage
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
Hypothesis hcontainer_get_usage1 : Genv.find_symbol ge container_get_usage = Some bcontainer_get_usage.
Hypothesis hcontainer_get_usage2 : Genv.find_funct_ptr ge bcontainer_get_usage =
Some (External (EF_external container_get_usage
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
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).
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).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Lemma sys_get_quota_body_correct:
∀ m d d' env le,
env = PTree.empty _ →
trap_get_quota_spec d = Some d' →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) sys_get_quota_body E0 le' (m, d') Out_normal.
Proof.
intros; subst.
unfold sys_get_quota_body.
functional inversion H0.
assert (0 ≤ curid ≤ Int.max_unsigned) as curid_range.
{ functional inversion H2.
pose proof (valid_curid _ H1) as valid_curid.
intomega.
}
assert (0 ≤ quota ≤ Int.max_unsigned ∧
0 ≤ usage ≤ Int.max_unsigned ∧
0 ≤ quota - usage ≤ Int.max_unsigned)
as (quota_range & usage_range & remaining_quota_range).
{ functional inversion H3; subst.
functional inversion H4; subst.
pose proof (cvalid_quota _ (valid_container _ H1) _ H7) as valid_quota.
pose proof (cvalid_usage _ (valid_container _ H1) _ H7) as valid_usage.
unfold c, c0; omega.
}
esplit.
d3 vcgen.
{ repeat vcgen.
instantiate (1 := Int.repr curid).
rewrite Int.unsigned_repr; auto.
}
d3 vcgen; [ repeat vcgen.. |].
{ instantiate (1 := Int.repr quota).
rewrite Int.unsigned_repr; auto.
}
vcgen.
{ repeat vcgen.
instantiate (1 := Int.repr usage).
rewrite Int.unsigned_repr; auto.
}
repeat vcgen.
Qed.
End SysGetQuotaBody.
Theorem sys_get_quota_code_correct:
spec_le (sys_get_quota ↦ trap_get_quota_spec_low)
(〚sys_get_quota ↦ f_sys_get_quota 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(sys_get_quota_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m'0 labd labd0
(PTree.empty _)
(bind_parameter_temps' (fn_params f_sys_get_quota)
nil
(create_undef_temps (fn_temps f_sys_get_quota)))) H.
Qed.
End SYSGETQUOTA.
Section SYSOFFER_SHARED_MEM.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Lemma sys_get_quota_body_correct:
∀ m d d' env le,
env = PTree.empty _ →
trap_get_quota_spec d = Some d' →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) sys_get_quota_body E0 le' (m, d') Out_normal.
Proof.
intros; subst.
unfold sys_get_quota_body.
functional inversion H0.
assert (0 ≤ curid ≤ Int.max_unsigned) as curid_range.
{ functional inversion H2.
pose proof (valid_curid _ H1) as valid_curid.
intomega.
}
assert (0 ≤ quota ≤ Int.max_unsigned ∧
0 ≤ usage ≤ Int.max_unsigned ∧
0 ≤ quota - usage ≤ Int.max_unsigned)
as (quota_range & usage_range & remaining_quota_range).
{ functional inversion H3; subst.
functional inversion H4; subst.
pose proof (cvalid_quota _ (valid_container _ H1) _ H7) as valid_quota.
pose proof (cvalid_usage _ (valid_container _ H1) _ H7) as valid_usage.
unfold c, c0; omega.
}
esplit.
d3 vcgen.
{ repeat vcgen.
instantiate (1 := Int.repr curid).
rewrite Int.unsigned_repr; auto.
}
d3 vcgen; [ repeat vcgen.. |].
{ instantiate (1 := Int.repr quota).
rewrite Int.unsigned_repr; auto.
}
vcgen.
{ repeat vcgen.
instantiate (1 := Int.repr usage).
rewrite Int.unsigned_repr; auto.
}
repeat vcgen.
Qed.
End SysGetQuotaBody.
Theorem sys_get_quota_code_correct:
spec_le (sys_get_quota ↦ trap_get_quota_spec_low)
(〚sys_get_quota ↦ f_sys_get_quota 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(sys_get_quota_body_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m'0 labd labd0
(PTree.empty _)
(bind_parameter_temps' (fn_params f_sys_get_quota)
nil
(create_undef_temps (fn_temps f_sys_get_quota)))) H.
Qed.
End SYSGETQUOTA.
Section SYSOFFER_SHARED_MEM.
extern unsigned int get_curid(void);
extern unsigned int uctx_arg2(void);
extern unsigned int offer_shared_mem(unsigned int, unsigned int, unsigned int);
extern void uctx_set_errno(unsigned int);
extern void uctx_set_retval1(unsigned int);
void sys_offer_shared_mem()
{
unsigned int curid;
unsigned int vadr;
unsigned int res;
curid = get_curid();
if (curid == 1) {
vadr = uctx_arg2();
res = offer_shared_mem (1, 2, vadr);
uctx_set_retval1(res);
uctx_set_errno(0);
} {
uctx_set_errno(0);
}
}
Let L: compatlayer (cdata RData) := get_curid ↦ gensem get_curid_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ offer_shared_mem ↦ gensem offer_shared_mem_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysShareBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
get_curid
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 tuint cc_default))
Tnil tint cc_default).
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 tuint cc_default))
Tnil tint cc_default).
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 tint cc_default))
Tnil tint cc_default).
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 tint cc_default))
Tnil tint cc_default).
offer_shared_mem
Variable boffer_shared_mem: block.
Hypothesis hoffer_shared_mem1 : Genv.find_symbol ge offer_shared_mem = Some boffer_shared_mem.
Hypothesis hoffer_shared_mem2 : Genv.find_funct_ptr ge boffer_shared_mem =
Some (External (EF_external offer_shared_mem
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil)))
tint cc_default))
(Tcons tint(Tcons tint(Tcons tint Tnil))) tint cc_default).
Hypothesis hoffer_shared_mem1 : Genv.find_symbol ge offer_shared_mem = Some boffer_shared_mem.
Hypothesis hoffer_shared_mem2 : Genv.find_funct_ptr ge boffer_shared_mem =
Some (External (EF_external offer_shared_mem
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil)))
tint cc_default))
(Tcons tint(Tcons tint(Tcons tint Tnil))) tint cc_default).
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).
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).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Require Import AuxLemma.
Lemma sys_offer_shared_mem_correct:
∀ m d d' env le,
env = PTree.empty _ →
trap_offer_shared_mem_spec d = Some d' →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) sys_offer_shared_mem_body E0 le' (m, d') Out_normal.
Proof.
intros; subst.
unfold sys_offer_shared_mem_body.
functional inversion H0.
- esplit.
assert (0 ≤ vadr ≤ Int.max_unsigned ∧
0 ≤ res ≤ Int.max_unsigned)
as (vadr_range & res_range).
{ functional inversion H3; subst.
split.
repeat discharge_unsigned_range.
functional inversion H5; subst; rewrite_omega.
}
d3 vcgen.
{ repeat vcgen.
unfold get_curid_spec.
functional inversion H3; subst. subrewrite'.
instantiate (1 := Int.repr 1).
rewrite Int.unsigned_repr; auto.
rewrite_omega.
}
repeat vcgen.
{
rewrite Int.unsigned_repr; auto.
}
{
instantiate (1 := Int.repr res).
rewrite Int.unsigned_repr; auto.
rewrite Int.unsigned_repr; eauto.
}
{
rewrite_omega.
}
{
rewrite Int.unsigned_repr; eauto.
}
- esplit.
assert (0 ≤ n ≤ Int.max_unsigned) as curid_range.
{ pose proof (valid_curid _ H1) as valid_curid.
intomega.
}
d3 vcgen.
{ repeat vcgen.
unfold get_curid_spec.
functional inversion H3; subst. subrewrite'.
instantiate (1 := Int.repr n).
rewrite Int.unsigned_repr; auto.
}
repeat vcgen.
Qed.
End SysShareBody.
Theorem sys_offer_shared_mem_code_correct:
spec_le (sys_offer_shared_mem ↦ trap_offer_shared_mem_spec_low)
(〚sys_offer_shared_mem ↦ f_sys_offer_shared_mem 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(sys_offer_shared_mem_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m'0 labd labd0
(PTree.empty _)
(bind_parameter_temps' (fn_params f_sys_offer_shared_mem)
nil
(create_undef_temps (fn_temps f_sys_offer_shared_mem)))) H.
Qed.
End SYSOFFER_SHARED_MEM.
Section SYSRECEIVECHAN.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ syncreceive_chan ↦ gensem syncreceive_chan_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysReceiveChanBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Require Import AuxLemma.
Lemma sys_offer_shared_mem_correct:
∀ m d d' env le,
env = PTree.empty _ →
trap_offer_shared_mem_spec d = Some d' →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) sys_offer_shared_mem_body E0 le' (m, d') Out_normal.
Proof.
intros; subst.
unfold sys_offer_shared_mem_body.
functional inversion H0.
- esplit.
assert (0 ≤ vadr ≤ Int.max_unsigned ∧
0 ≤ res ≤ Int.max_unsigned)
as (vadr_range & res_range).
{ functional inversion H3; subst.
split.
repeat discharge_unsigned_range.
functional inversion H5; subst; rewrite_omega.
}
d3 vcgen.
{ repeat vcgen.
unfold get_curid_spec.
functional inversion H3; subst. subrewrite'.
instantiate (1 := Int.repr 1).
rewrite Int.unsigned_repr; auto.
rewrite_omega.
}
repeat vcgen.
{
rewrite Int.unsigned_repr; auto.
}
{
instantiate (1 := Int.repr res).
rewrite Int.unsigned_repr; auto.
rewrite Int.unsigned_repr; eauto.
}
{
rewrite_omega.
}
{
rewrite Int.unsigned_repr; eauto.
}
- esplit.
assert (0 ≤ n ≤ Int.max_unsigned) as curid_range.
{ pose proof (valid_curid _ H1) as valid_curid.
intomega.
}
d3 vcgen.
{ repeat vcgen.
unfold get_curid_spec.
functional inversion H3; subst. subrewrite'.
instantiate (1 := Int.repr n).
rewrite Int.unsigned_repr; auto.
}
repeat vcgen.
Qed.
End SysShareBody.
Theorem sys_offer_shared_mem_code_correct:
spec_le (sys_offer_shared_mem ↦ trap_offer_shared_mem_spec_low)
(〚sys_offer_shared_mem ↦ f_sys_offer_shared_mem 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(sys_offer_shared_mem_correct
s (Genv.globalenv p) makeglobalenv
b0 Hb0fs Hb0fp
b1 Hb1fs Hb1fp
b2 Hb2fs Hb2fp
b3 Hb3fs Hb3fp
b4 Hb4fs Hb4fp
m'0 labd labd0
(PTree.empty _)
(bind_parameter_temps' (fn_params f_sys_offer_shared_mem)
nil
(create_undef_temps (fn_temps f_sys_offer_shared_mem)))) H.
Qed.
End SYSOFFER_SHARED_MEM.
Section SYSRECEIVECHAN.
Let L: compatlayer (cdata RData) :=
uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ syncreceive_chan ↦ gensem syncreceive_chan_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysReceiveChanBody.
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).
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).
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).
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).
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).
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).
uctx_set_retval1
Variable buctx_set_retval1: block.
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Hypothesis huctx_set_retval11 : Genv.find_symbol ge uctx_set_retval1 = Some buctx_set_retval1.
Hypothesis huctx_set_retval12 : Genv.find_funct_ptr ge buctx_set_retval1 =
Some (External (EF_external uctx_set_retval1
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
syncreceive_chan
Variable bsyncreceive_chan: block.
Hypothesis hsyncreceive_chan1 : Genv.find_symbol ge syncreceive_chan = Some bsyncreceive_chan.
Hypothesis hsyncreceive_chan2 : Genv.find_funct_ptr ge bsyncreceive_chan =
Some (External (EF_external syncreceive_chan
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Lemma sys_receive_chan_body_correct: ∀ m d d' env le,
env = PTree.empty _ →
trap_receivechan_spec d = Some d' →
∃ le',
exec_stmt ge env le ((m, d): mem) sys_receive_chan_body E0 le' (m, d') Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
assert(rrange: 0 ≤ r ≤ Int.max_unsigned).
{
functional inversion H4; try omega.
unfold arecvcount.
functional inversion H3.
rewrite <- H20 in ×.
generalize (Z.min_spec (Int.unsigned scount) (Int.unsigned n)).
intro tmp.
destruct tmp; destruct H25; rewrite H26;
apply Int.unsigned_range_2.
}
rewrite <- Int.unsigned_repr with r in H4; try omega.
functional inversion H1; try subst;
functional inversion H2; try subst;
functional inversion H3; try subst;
unfold sys_receive_chan_body;
esplit;
repeat vcgen.
Qed.
End SysReceiveChanBody.
Theorem sys_receive_chan_code_correct:
spec_le
(sys_receive_chan ↦ trap_receivechan_spec_low)
(〚sys_receive_chan ↦ f_sys_receive_chan 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(sys_receive_chan_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
m'0 labd labd0
(PTree.empty _)
(bind_parameter_temps' (fn_params f_sys_receive_chan)
nil
(create_undef_temps (fn_temps f_sys_receive_chan)))) H0.
Qed.
End SYSRECEIVECHAN.
End WithPrimitives.
End TTRAPARGCODE.
Hypothesis hsyncreceive_chan1 : Genv.find_symbol ge syncreceive_chan = Some bsyncreceive_chan.
Hypothesis hsyncreceive_chan2 : Genv.find_funct_ptr ge bsyncreceive_chan =
Some (External (EF_external syncreceive_chan
(signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default))
(Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Lemma sys_receive_chan_body_correct: ∀ m d d' env le,
env = PTree.empty _ →
trap_receivechan_spec d = Some d' →
∃ le',
exec_stmt ge env le ((m, d): mem) sys_receive_chan_body E0 le' (m, d') Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst.
assert(rrange: 0 ≤ r ≤ Int.max_unsigned).
{
functional inversion H4; try omega.
unfold arecvcount.
functional inversion H3.
rewrite <- H20 in ×.
generalize (Z.min_spec (Int.unsigned scount) (Int.unsigned n)).
intro tmp.
destruct tmp; destruct H25; rewrite H26;
apply Int.unsigned_range_2.
}
rewrite <- Int.unsigned_repr with r in H4; try omega.
functional inversion H1; try subst;
functional inversion H2; try subst;
functional inversion H3; try subst;
unfold sys_receive_chan_body;
esplit;
repeat vcgen.
Qed.
End SysReceiveChanBody.
Theorem sys_receive_chan_code_correct:
spec_le
(sys_receive_chan ↦ trap_receivechan_spec_low)
(〚sys_receive_chan ↦ f_sys_receive_chan 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep
(sys_receive_chan_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
m'0 labd labd0
(PTree.empty _)
(bind_parameter_temps' (fn_params f_sys_receive_chan)
nil
(create_undef_temps (fn_temps f_sys_receive_chan)))) H0.
Qed.
End SYSRECEIVECHAN.
End WithPrimitives.
End TTRAPARGCODE.