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.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
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 {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 SYSSETSEG1.
Let L: compatlayer (cdata RData) :=
vmx_set_desc1 ↦ gensem thread_vmx_set_desc1_spec
⊕ 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.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysSetSeg1Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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.
Require Import FutureTactic.
Require Import GlobalOracleProp.
Require Import SingleOracle.
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 {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 SYSSETSEG1.
Let L: compatlayer (cdata RData) :=
vmx_set_desc1 ↦ gensem thread_vmx_set_desc1_spec
⊕ 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.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysSetSeg1Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_set_seg1
Variable bvmx_set_desc: block.
Hypothesis hvmx_set_desc1 : Genv.find_symbol ge vmx_set_desc1 = Some bvmx_set_desc.
Hypothesis hvmx_set_desc2 : Genv.find_funct_ptr ge bvmx_set_desc =
let arg_type := Tcons tuint (Tcons tuint (Tcons tuint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_desc1 in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_set_desc1 : Genv.find_symbol ge vmx_set_desc1 = Some bvmx_set_desc.
Hypothesis hvmx_set_desc2 : Genv.find_funct_ptr ge bvmx_set_desc =
let arg_type := Tcons tuint (Tcons tuint (Tcons tuint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_desc1 in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
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).
Lemma sys_set_seg1_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_seg1_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_seg1_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst;
functional inversion H1; subst;
functional inversion H2; subst;
functional inversion H3; subst.
functional inversion H5; subst;
unfold sys_set_seg1_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
destruct _x;
unfold sys_set_seg1_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysSetSeg1Body.
Theorem sys_set_seg1_body_code_correct:
spec_le
(sys_set_seg1 ↦ trap_set_seg1_spec_low)
(〚sys_set_seg1 ↦ f_sys_set_seg1 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_seg1_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_set_seg1)
nil
(create_undef_temps (fn_temps f_sys_set_seg1)))) H.
Qed.
End SYSSETSEG1.
Section SYSSETSEG2.
Let L: compatlayer (cdata RData) :=
vmx_set_desc2 ↦ gensem thread_vmx_set_desc2_spec
⊕ 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.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysSetSeg2Body.
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).
Lemma sys_set_seg1_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_seg1_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_seg1_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst;
functional inversion H1; subst;
functional inversion H2; subst;
functional inversion H3; subst.
functional inversion H5; subst;
unfold sys_set_seg1_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
destruct _x;
unfold sys_set_seg1_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysSetSeg1Body.
Theorem sys_set_seg1_body_code_correct:
spec_le
(sys_set_seg1 ↦ trap_set_seg1_spec_low)
(〚sys_set_seg1 ↦ f_sys_set_seg1 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_seg1_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_set_seg1)
nil
(create_undef_temps (fn_temps f_sys_set_seg1)))) H.
Qed.
End SYSSETSEG1.
Section SYSSETSEG2.
Let L: compatlayer (cdata RData) :=
vmx_set_desc2 ↦ gensem thread_vmx_set_desc2_spec
⊕ 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.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysSetSeg2Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
vmx_set_seg2
Variable bvmx_set_desc: block.
Hypothesis hvmx_set_desc1 : Genv.find_symbol ge vmx_set_desc2 = Some bvmx_set_desc.
Hypothesis hvmx_set_desc2 : Genv.find_funct_ptr ge bvmx_set_desc =
let arg_type := Tcons tuint (Tcons tuint (Tcons tuint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_desc2 in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
Hypothesis hvmx_set_desc1 : Genv.find_symbol ge vmx_set_desc2 = Some bvmx_set_desc.
Hypothesis hvmx_set_desc2 : Genv.find_funct_ptr ge bvmx_set_desc =
let arg_type := Tcons tuint (Tcons tuint (Tcons tuint Tnil)) in
let ret_type := tvoid in
let cal_conv := cc_default in
let prim := vmx_set_desc2 in
Some (External (EF_external
prim
(signature_of_type arg_type ret_type cal_conv))
arg_type ret_type cal_conv).
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).
Lemma sys_set_seg2_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_seg2_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_seg2_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst;
functional inversion H1; subst;
functional inversion H2; subst;
functional inversion H3; subst.
functional inversion H5; subst;
unfold sys_set_seg2_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
destruct _x;
unfold sys_set_seg2_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysSetSeg2Body.
Theorem sys_set_seg2_body_code_correct:
spec_le
(sys_set_seg2 ↦ trap_set_seg2_spec_low)
(〚sys_set_seg2 ↦ f_sys_set_seg2 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_seg2_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_set_seg2)
nil
(create_undef_temps (fn_temps f_sys_set_seg2)))) H.
Qed.
End SYSSETSEG2.
Section SYSGETQUOTA.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
⊕ container_get_quota ↦ gensem thread_container_get_quota_spec
⊕ container_get_usage ↦ gensem thread_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).
Lemma sys_set_seg2_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_set_seg2_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_set_seg2_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
functional inversion H0; subst;
functional inversion H1; subst;
functional inversion H2; subst;
functional inversion H3; subst.
functional inversion H5; subst;
unfold sys_set_seg2_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
destruct _x;
unfold sys_set_seg2_body;
esplit;
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
repeat vcgen.
Qed.
End SysSetSeg2Body.
Theorem sys_set_seg2_body_code_correct:
spec_le
(sys_set_seg2 ↦ trap_set_seg2_spec_low)
(〚sys_set_seg2 ↦ f_sys_set_seg2 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_set_seg2_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_set_seg2)
nil
(create_undef_temps (fn_temps f_sys_set_seg2)))) H.
Qed.
End SYSSETSEG2.
Section SYSGETQUOTA.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
⊕ container_get_quota ↦ gensem thread_container_get_quota_spec
⊕ container_get_usage ↦ gensem thread_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.
functional inversion H6.
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; substx.
functional inversion H5; subst.
functional inversion H3; subst.
functional inversion H4; substx.
pose proof (INVLemmaThreadContainer.cvalid_quota _ (valid_container _ H1) (ZMap.get (CPU_ID d) (cid d)))
as valid_quota.
pose proof (INVLemmaThreadContainer.cvalid_usage _ (valid_container _ H1) (ZMap.get (CPU_ID d) (cid d)))
as valid_usage.
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 SYSRECEIVECHAN.
Lemma syncreceive_chan_prop:
∀ chanid vaddr rcount d d´ r,
thread_syncreceive_chan_spec chanid vaddr rcount d = Some (d´, r) →
ikern d´ = true ∧ ihost d´ = true.
Proof.
intros.
functional inversion H; subst.
functional inversion H7; subst; functional inversion H8; subst; functional inversion H0; subst.
- simpl; tauto.
- simpl in ×.
Require Import FutureTactic.
functional inversion H19; substx;
simpl in *;
tauto.
- substx.
simpl.
tauto.
Qed.
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 thread_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).
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.
functional inversion H6.
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; substx.
functional inversion H5; subst.
functional inversion H3; subst.
functional inversion H4; substx.
pose proof (INVLemmaThreadContainer.cvalid_quota _ (valid_container _ H1) (ZMap.get (CPU_ID d) (cid d)))
as valid_quota.
pose proof (INVLemmaThreadContainer.cvalid_usage _ (valid_container _ H1) (ZMap.get (CPU_ID d) (cid d)))
as valid_usage.
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 SYSRECEIVECHAN.
Lemma syncreceive_chan_prop:
∀ chanid vaddr rcount d d´ r,
thread_syncreceive_chan_spec chanid vaddr rcount d = Some (d´, r) →
ikern d´ = true ∧ ihost d´ = true.
Proof.
intros.
functional inversion H; subst.
functional inversion H7; subst; functional inversion H8; subst; functional inversion H0; subst.
- simpl; tauto.
- simpl in ×.
Require Import FutureTactic.
functional inversion H19; substx;
simpl in *;
tauto.
- substx.
simpl.
tauto.
Qed.
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 thread_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 (Hrange1: 0 ≤ chanid ≤ Int.max_unsigned).
{
functional inversion H1; subst.
repeat vcgen.
}
assert (Hrange2: 0 ≤ vaddr ≤ Int.max_unsigned).
{
functional inversion H2; subst.
repeat vcgen.
}
assert (Hrange3: 0 ≤ rcount ≤ Int.max_unsigned).
{
functional inversion H3; subst.
repeat vcgen.
}
assert(rrange: 0 ≤ r ≤ Int.max_unsigned).
{
functional inversion H4; try omega.
functional inversion H13; substx.
omega.
functional inversion H26; subst.
functional inversion H6; subst.
functional inversion H37; subst.
omega.
functional inversion H26; subst.
functional inversion H6; subst.
functional inversion H37; subst.
omega.
}
unfold sys_receive_chan_body.
rewrite <- (Int.unsigned_repr chanid) in H1; try assumption.
rewrite <- (Int.unsigned_repr vaddr) in H2; try assumption.
rewrite <- (Int.unsigned_repr rcount) in H3; try assumption.
rewrite <- Int.unsigned_repr with r in H4; try omega.
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.
Section SYSSENDTOCHAN.
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
⊕ syncsendto_chan_post ↦ gensem thread_syncsendto_chan_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysSendToChanBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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 (Hrange1: 0 ≤ chanid ≤ Int.max_unsigned).
{
functional inversion H1; subst.
repeat vcgen.
}
assert (Hrange2: 0 ≤ vaddr ≤ Int.max_unsigned).
{
functional inversion H2; subst.
repeat vcgen.
}
assert (Hrange3: 0 ≤ rcount ≤ Int.max_unsigned).
{
functional inversion H3; subst.
repeat vcgen.
}
assert(rrange: 0 ≤ r ≤ Int.max_unsigned).
{
functional inversion H4; try omega.
functional inversion H13; substx.
omega.
functional inversion H26; subst.
functional inversion H6; subst.
functional inversion H37; subst.
omega.
functional inversion H26; subst.
functional inversion H6; subst.
functional inversion H37; subst.
omega.
}
unfold sys_receive_chan_body.
rewrite <- (Int.unsigned_repr chanid) in H1; try assumption.
rewrite <- (Int.unsigned_repr vaddr) in H2; try assumption.
rewrite <- (Int.unsigned_repr rcount) in H3; try assumption.
rewrite <- Int.unsigned_repr with r in H4; try omega.
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.
Section SYSSENDTOCHAN.
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
⊕ syncsendto_chan_post ↦ gensem thread_syncsendto_chan_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysSendToChanBody.
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).
syncsendto_chan_post
Variable bsyncsendto_chan_post: block.
Hypothesis hsyncsendto_chan_post1 : Genv.find_symbol ge syncsendto_chan_post = Some bsyncsendto_chan_post.
Hypothesis hsyncsendto_chan_post2 : Genv.find_funct_ptr ge bsyncsendto_chan_post =
Some (External (EF_external syncsendto_chan_post
(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_sendto_chan_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
trap_sendtochan_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_sendto_chan_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold sys_sendto_chan_body.
functional inversion H0; subst.
functional inversion H1; subst;
unfold curid, cpu in *;
try omega.
functional inversion H2; subst;
unfold curid0, cpu0 in *;
try omega.
functional inversion H3; subst;
unfold curid1, cpu1 in *;
try omega.
assert(rrange: 0 ≤ r ≤ Int.max_unsigned).
{
functional inversion H4; subst; simpl; eauto.
functional inversion H30; subst; simpl; eauto.
functional inversion H6; subst; simpl; eauto.
rewrite Zmin_spec.
zdestruct.
}
rewrite <- Int.unsigned_repr with r in H4 by omega.
esplit; repeat vcgen.
Qed.
End SysSendToChanBody.
Theorem sys_sendto_chan_code_correct:
spec_le (sys_sendto_chan ↦ trap_sendtochan_spec_low)
(〚sys_sendto_chan ↦ f_sys_sendto_chan 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_sendto_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_sendto_chan)
nil
(create_undef_temps (fn_temps f_sys_sendto_chan)))) H.
Qed.
End SYSSENDTOCHAN.
End WithPrimitives.
End TTRAPARGCODE.
Hypothesis hsyncsendto_chan_post1 : Genv.find_symbol ge syncsendto_chan_post = Some bsyncsendto_chan_post.
Hypothesis hsyncsendto_chan_post2 : Genv.find_funct_ptr ge bsyncsendto_chan_post =
Some (External (EF_external syncsendto_chan_post
(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_sendto_chan_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
trap_sendtochan_spec d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_sendto_chan_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros; subst.
unfold sys_sendto_chan_body.
functional inversion H0; subst.
functional inversion H1; subst;
unfold curid, cpu in *;
try omega.
functional inversion H2; subst;
unfold curid0, cpu0 in *;
try omega.
functional inversion H3; subst;
unfold curid1, cpu1 in *;
try omega.
assert(rrange: 0 ≤ r ≤ Int.max_unsigned).
{
functional inversion H4; subst; simpl; eauto.
functional inversion H30; subst; simpl; eauto.
functional inversion H6; subst; simpl; eauto.
rewrite Zmin_spec.
zdestruct.
}
rewrite <- Int.unsigned_repr with r in H4 by omega.
esplit; repeat vcgen.
Qed.
End SysSendToChanBody.
Theorem sys_sendto_chan_code_correct:
spec_le (sys_sendto_chan ↦ trap_sendtochan_spec_low)
(〚sys_sendto_chan ↦ f_sys_sendto_chan 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep
(sys_sendto_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_sendto_chan)
nil
(create_undef_temps (fn_temps f_sys_sendto_chan)))) H.
Qed.
End SYSSENDTOCHAN.
End WithPrimitives.
End TTRAPARGCODE.