Library mcertikos.trap.TTrapArgCode2
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 GlobalOracleProp.
Require Import AuxLemma.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Opaque full_thread_list.
Module TTRAPARGCODE2.
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 PTFRESV.
Lemma palloc_range:
∀ d d´ re n,
big2_palloc_spec n d = Some (d´, re) →
262144 ≤ nps d ≤ 1048576 →
0 ≤ re ≤ Int.max_unsigned.
Proof.
intros. rewrite int_max.
unfold big2_palloc_spec in H; simpl; subdestruct; inv H;
try destruct a0;
omega.
Qed.
Lemma ptInsert0_range:
∀ p1 p2 v d d´ re n,
big2_ptInsert_spec p1 p2 v n d = Some (d´, re) →
262144 ≤ nps d ≤ 1048576 →
0 ≤ re ≤ Int.max_unsigned.
Proof.
intros. rewrite_omega.
functional inversion H; subst; try omega.
functional inversion H13; try subst; try omega.
functional inversion H11; try subst; try omega.
eapply palloc_range; eauto.
Qed.
Lemma ptInsert0_pg:
∀ p1 p2 v d d´ re n,
big2_ptInsert_spec p1 p2 v n d = Some (d´, re) →
pg d = true.
Proof.
intros.
functional inversion H; subst; eauto.
Qed.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
⊕ pt_resv ↦ gensem big2_ptResv_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PtfResvBody.
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 GlobalOracleProp.
Require Import AuxLemma.
Require Import GlobalOracleProp.
Require Import SingleOracle.
Opaque full_thread_list.
Module TTRAPARGCODE2.
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 PTFRESV.
Lemma palloc_range:
∀ d d´ re n,
big2_palloc_spec n d = Some (d´, re) →
262144 ≤ nps d ≤ 1048576 →
0 ≤ re ≤ Int.max_unsigned.
Proof.
intros. rewrite int_max.
unfold big2_palloc_spec in H; simpl; subdestruct; inv H;
try destruct a0;
omega.
Qed.
Lemma ptInsert0_range:
∀ p1 p2 v d d´ re n,
big2_ptInsert_spec p1 p2 v n d = Some (d´, re) →
262144 ≤ nps d ≤ 1048576 →
0 ≤ re ≤ Int.max_unsigned.
Proof.
intros. rewrite_omega.
functional inversion H; subst; try omega.
functional inversion H13; try subst; try omega.
functional inversion H11; try subst; try omega.
eapply palloc_range; eauto.
Qed.
Lemma ptInsert0_pg:
∀ p1 p2 v d d´ re n,
big2_ptInsert_spec p1 p2 v n d = Some (d´, re) →
pg d = true.
Proof.
intros.
functional inversion H; subst; eauto.
Qed.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
⊕ pt_resv ↦ gensem big2_ptResv_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PtfResvBody.
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 tint cc_default)) Tnil tint cc_default).
pt_resv
Variable bpt_resv: block.
Hypothesis hpt_resv1 : Genv.find_symbol ge pt_resv = Some bpt_resv.
Hypothesis hpt_resv2 : Genv.find_funct_ptr ge bpt_resv = Some (External (EF_external pt_resv (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
Lemma ptfault_resv_body_correct: ∀ m d d´ env le vaddr,
env = PTree.empty _ →
PTree.get _vaddr le = Some (Vint vaddr) →
ptfault_resv_spec (Int.unsigned vaddr) d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) ptfault_resv_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold ptfault_resv_body.
functional inversion H1; subst.
assert (flags: ikern d = true ∧ ihost d = true ∧ pg d = true ∧ ipt d = true ∧ init d = true).
{
functional inversion H4; subst.
unfold big2_palloc_spec in H6; subdestruct; simpl in *; eauto.
unfold big2_palloc_spec in H5; subdestruct; simpl in *; eauto.
}
destruct flags as (ikern & ihost & pg & ipt & iinit).
unfold curid, cpu in ×.
inv H2.
assert(0 ≤ _x ≤ Int.max_unsigned).
{
functional inversion H4; subst.
omega.
functional inversion H; subst.
omega.
omega.
functional inversion H16; subst.
omega.
unfold big2_palloc_spec in H26; subdestruct; inv H26; simpl in *; eauto; try omega.
destruct a0.
assert(npseq: nps abd´ = nps d).
{
unfold big2_palloc_spec in H3; subdestruct; unfold pt, c in *; inv H3; simpl in *; eauto.
}
specialize (valid_nps0 pg).
omega.
}
rewrite <- Int.unsigned_repr with _x in H4 by omega.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
subrewrite´.
rewrite Int.unsigned_repr.
reflexivity.
omega.
Qed.
End PtfResvBody.
Theorem ptfault_resv_code_correct:
spec_le (ptfault_resv ↦ ptf_resv_spec_low) (〚ptfault_resv ↦ f_ptfault_resv 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (ptfault_resv_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_ptfault_resv)
(Vint i::nil)
(create_undef_temps (fn_temps f_ptfault_resv)))) H1.
Qed.
End PTFRESV.
Section SYSMMAP.
Let L: compatlayer (cdata RData) := get_curid ↦ gensem thread_get_curid_spec
⊕ uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_arg4 ↦ gensem uctx_arg4_spec
⊕ pt_read ↦ gensem thread_ptRead_spec
⊕ pt_resv ↦ gensem big2_ptResv_spec
⊕ vmx_set_mmap ↦ gensem thread_vmx_set_mmap_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 SysMMapBody.
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 tint 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).
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 tint 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 tint cc_default)) Tnil tint cc_default).
pt_read
Variable bpt_read: block.
Hypothesis hpt_read1 : Genv.find_symbol ge pt_read = Some bpt_read.
Hypothesis hpt_read2 : Genv.find_funct_ptr ge bpt_read = Some (External (EF_external pt_read (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default)) (Tcons tint (Tcons tint Tnil)) tint cc_default).
pt_resv
Variable bpt_resv: block.
Hypothesis hpt_resv1 : Genv.find_symbol ge pt_resv = Some bpt_resv.
Hypothesis hpt_resv2 : Genv.find_funct_ptr ge bpt_resv = Some (External (EF_external pt_resv (signature_of_type (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint Tnil))) tint cc_default).
vmx_set_mmap
Variable bvmx_set_mmap: block.
Hypothesis hvmx_set_mmap1 : Genv.find_symbol ge vmx_set_mmap = Some bvmx_set_mmap.
Hypothesis hvmx_set_mmap2 : Genv.find_funct_ptr ge bvmx_set_mmap = Some (External (EF_external vmx_set_mmap (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).
Lemma sys_mmap_body_correct_aux1:
∀ hpa hpa´ d gpa hva mem_type abd0 _x1 abd1 _x3 d´ m le
(HINV: high_level_invariant d),
0 ≤ hpa ≤ Int.max_unsigned →
Z.land hpa 1 = 0 →
0 ≤ hpa´ ≤ Int.max_unsigned →
uctx_arg2_spec d = Some gpa →
uctx_arg3_spec d = Some hva →
uctx_arg4_spec d = Some mem_type →
Zdivide_dec 4096 hva AuxStateDataType.HPS &&
Zdivide_dec 4096 gpa AuxStateDataType.HPS &&
(zle_le 655360 hva (1703936 - 4096)
|| zle_le 1073741824 hva (4026531840 - 4096)) = true →
thread_ptRead_spec (ZMap.get (CPU_ID d) (cid d)) hva d = Some hpa →
big2_ptResv_spec (ZMap.get (CPU_ID d) (cid d)) hva 7 d =
Some (abd0, _x1) →
thread_ptRead_spec (ZMap.get (CPU_ID d) (cid d)) hva abd0 = Some hpa´ →
thread_vmx_set_mmap_spec gpa (Z.land hpa´ 4294963200 + hva mod 4096 : Z) mem_type abd0 = Some (abd1, _x3) →
uctx_set_errno_spec 0 abd1 = Some d´ →
∃ le´ : temp_env,
exec_stmt ge (PTree.empty (block × type)) le ((m, d):mem) sys_mmap_body E0 le´
(m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
assert(iflags: ikern d = true ∧ pg d = true ∧ ihost d = true).
{
functional inversion H2; subst.
eauto.
}
destruct iflags as [ikern iflags].
destruct iflags as [pg ihost].
destruct HINV.
assert(negval: Int.repr (-4096) = Int.repr (4294963200)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
assert(negval1: Int.repr (-268435456) = Int.repr (4026531840)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
functional inversion H2; subst.
functional inversion H3; subst.
functional inversion H4; subst.
unfold andb, orb in H5.
subdestruct.
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
destruct (Zdivide_dec 4096 (Int.unsigned n) AuxStateDataType.HPS).
unfold Z.divide in ×.
destruct d0.
destruct d1.
Focus 2.
simpl in ×.
discriminate Hdestruct0.
Focus 2.
simpl in ×.
discriminate Hdestruct.
exploit (Z.mod_unique_pos (Int.unsigned n0) 4096 x 0).
omega.
omega.
intro n0modval.
exploit (Z.mod_unique_pos (Int.unsigned n) 4096 x0 0).
omega.
omega.
intro nmodval.
destruct (zle_le 655360 (Int.unsigned n0) 1699840).
Focus 2.
simpl in ×.
discriminate Hdestruct1.
unfold sys_mmap_body.
rewrite negval.
assert(0 ≤ _x1 ≤ Int.max_unsigned).
{
functional inversion H7; try omega.
functional inversion H11; try omega.
subst.
unfold big2_ptAllocPDE_spec in H46; subdestruct; inv H46; simpl in*; try omega.
unfold big2_palloc_spec in Hdestruct9; subdestruct; inv Hdestruct9; simpl in ×.
destruct a1.
generalize (valid_nps0 pg); intro.
unfold big2_palloc_spec in H34; subdestruct; unfold pt in *; inv H34; simpl in ×.
omega.
omega.
omega.
omega.
omega.
}
assert(0 ≤ _x3 ≤ Int.max_unsigned).
{
functional inversion H9; try omega.
functional inversion H33; try omega.
functional inversion H43; subst; try omega.
}
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H22, ikern, ihost.
rewrite Int.unsigned_repr; try omega.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
discharge_cmp.
econstructor.
ptreesolve.
discharge_cmp.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
discharge_cmp.
omega.
omega.
omega.
omega.
omega.
repeat vcgenfull.
change (Z.lor (Z.lor 1 4) 2) with 7.
instantiate (1:= (Int.repr _x1)).
rewrite Int.unsigned_repr; try omega.
eassumption.
repeat vcgen.
instantiate (1:= (Int.repr hpa´)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat ptreesolve.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
simpl.
unfold sem_mod, sem_binarith.
simpl.
discharge_cmp.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgenfull.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
destruct (Zdivide_dec 4096 (Int.unsigned n) AuxStateDataType.HPS).
unfold Z.divide in ×.
destruct d0.
destruct d1.
Focus 2.
simpl in ×.
discriminate Hdestruct0.
Focus 2.
simpl in ×.
discriminate Hdestruct.
exploit (Z.mod_unique_pos (Int.unsigned n0) 4096 x 0).
omega.
omega.
intro n0modval.
exploit (Z.mod_unique_pos (Int.unsigned n) 4096 x0 0).
omega.
omega.
intro nmodval.
destruct (zle_le 1073741824 (Int.unsigned n0) 4026527744).
Focus 2.
simpl in ×.
discriminate H5.
destruct (zle_le 655360 (Int.unsigned n0) 1699840).
simpl in ×.
discriminate Hdestruct1.
unfold sys_mmap_body.
rewrite negval, negval1.
assert(0 ≤ _x1 ≤ Int.max_unsigned).
{
functional inversion H7; try omega.
functional inversion H11; try omega.
subst.
unfold big2_ptAllocPDE_spec in H46; subdestruct; inv H46; simpl in*; try omega.
unfold big2_palloc_spec in Hdestruct9; subdestruct; inv Hdestruct9; simpl in ×.
destruct a1.
generalize (valid_nps0 pg); intro.
unfold big2_palloc_spec in H34; subdestruct; unfold pt in *; inv H34; simpl in ×.
omega.
omega.
omega.
omega.
omega.
}
assert(0 ≤ _x3 ≤ Int.max_unsigned).
{
functional inversion H9; try omega.
functional inversion H33; try omega.
functional inversion H43; try omega.
}
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H15, ikern, ihost.
rewrite Int.unsigned_repr; try omega.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
discharge_cmp.
econstructor.
ptreesolve.
discharge_cmp.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
reflexivity.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
discharge_cmp.
omega.
omega.
omega.
omega.
omega.
repeat vcgenfull.
change (Z.lor (Z.lor 1 4) 2) with 7.
instantiate (1:= (Int.repr _x1)).
rewrite Int.unsigned_repr; try omega.
eassumption.
repeat vcgen.
instantiate (1:= (Int.repr hpa´)).
rewrite Int.unsigned_repr; try omega.
reflexivity.
repeat ptreesolve.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
simpl.
unfold sem_mod, sem_binarith.
simpl.
discharge_cmp.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgenfull.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
Qed.
Lemma sys_mmap_body_correct_aux2:
∀ hpa d gpa hva mem_type _x1 abd1 d´ m le
(HINV: high_level_invariant d),
0 ≤ hpa ≤ Int.max_unsigned →
Z.land hpa 1 ≠ 0 →
True →
uctx_arg2_spec d = Some gpa →
uctx_arg3_spec d = Some hva →
uctx_arg4_spec d = Some mem_type →
Zdivide_dec 4096 hva AuxStateDataType.HPS &&
Zdivide_dec 4096 gpa AuxStateDataType.HPS &&
(zle_le 655360 hva (1703936 - 4096)
|| zle_le 1073741824 hva (4026531840 - 4096)) = true →
thread_ptRead_spec (ZMap.get (CPU_ID d) (cid d)) hva d = Some hpa →
thread_vmx_set_mmap_spec gpa (Z.land hpa 4294963200 + hva mod 4096 : Z) mem_type d = Some (abd1, _x1) →
uctx_set_errno_spec 0 abd1 = Some d´ →
∃ le´ : temp_env,
exec_stmt ge (PTree.empty (block × type)) le ((m, d):mem) sys_mmap_body E0 le´
(m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
assert(iflags: ikern d = true ∧ pg d = true ∧ ihost d = true).
{
functional inversion H2; subst.
eauto.
}
destruct iflags as [ikern iflags].
destruct iflags as [pg ihost].
destruct HINV.
assert(negval: Int.repr (-4096) = Int.repr (4294963200)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
assert(negval1: Int.repr (-268435456) = Int.repr (4026531840)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
functional inversion H2; subst.
functional inversion H3; subst.
functional inversion H4; subst.
unfold andb, orb in H5.
subdestruct.
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
destruct (Zdivide_dec 4096 (Int.unsigned n) AuxStateDataType.HPS).
unfold Z.divide in ×.
destruct d0.
destruct d1.
Focus 2.
simpl in ×.
discriminate Hdestruct0.
Focus 2.
simpl in ×.
discriminate Hdestruct.
exploit (Z.mod_unique_pos (Int.unsigned n0) 4096 x 0).
omega.
omega.
intro n0modval.
exploit (Z.mod_unique_pos (Int.unsigned n) 4096 x0 0).
omega.
omega.
intro nmodval.
destruct (zle_le 655360 (Int.unsigned n0) 1699840).
Focus 2.
simpl in ×.
discriminate Hdestruct1.
unfold sys_mmap_body.
rewrite negval, negval1.
assert(0 ≤ _x1 ≤ Int.max_unsigned).
{
functional inversion H7; try omega.
functional inversion H9; try omega.
functional inversion H40; try omega.
}
subst.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H13, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
discharge_cmp.
econstructor.
ptreesolve.
discharge_cmp.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
omega.
omega.
omega.
omega.
repeat vcgenfull.
repeat ptreesolve.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
simpl.
unfold sem_mod, sem_binarith.
simpl.
discharge_cmp.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgenfull.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
destruct (Zdivide_dec 4096 (Int.unsigned n) AuxStateDataType.HPS).
unfold Z.divide in ×.
destruct d0.
destruct d1.
Focus 2.
simpl in ×.
discriminate Hdestruct0.
Focus 2.
simpl in ×.
discriminate Hdestruct.
exploit (Z.mod_unique_pos (Int.unsigned n0) 4096 x 0).
omega.
omega.
intro n0modval.
exploit (Z.mod_unique_pos (Int.unsigned n) 4096 x0 0).
omega.
omega.
intro nmodval.
destruct (zle_le 655360 (Int.unsigned n0) 1699840).
simpl in ×.
discriminate Hdestruct1.
destruct (zle_le 1073741824 (Int.unsigned n0) 4026527744).
Focus 2.
simpl in ×.
discriminate H5.
unfold sys_mmap_body.
rewrite negval, negval1.
assert(0 ≤ _x1 ≤ Int.max_unsigned).
{
functional inversion H7; try omega.
functional inversion H9; try omega.
functional inversion H40; try omega.
}
subst.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H13, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
econstructor.
discharge_cmp.
discharge_cmp.
econstructor.
ptreesolve.
discharge_cmp.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
omega.
omega.
omega.
omega.
repeat vcgenfull.
repeat ptreesolve.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
simpl.
unfold sem_mod, sem_binarith.
simpl.
discharge_cmp.
discharge_cmp.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
simpl.
repeat ptreesolve.
repeat vcgen.
repeat vcgenfull.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
rewrite <- n0modval.
rewrite Z.add_0_r.
repeat discharge_unsigned_range.
Qed.
Lemma sys_mmap_body_correct_aux3:
∀ d gpa hva mem_type d´ m le
(HINV: high_level_invariant d),
True →
True →
True →
uctx_arg2_spec d = Some gpa →
uctx_arg3_spec d = Some hva →
uctx_arg4_spec d = Some mem_type →
Zdivide_dec 4096 hva AuxStateDataType.HPS &&
Zdivide_dec 4096 gpa AuxStateDataType.HPS &&
(zle_le 655360 hva (1703936 - 4096)
|| zle_le 1073741824 hva (4026531840 - 4096)) = false →
uctx_set_errno_spec 4 d = Some d´ →
∃ le´ : temp_env,
exec_stmt ge (PTree.empty (block × type)) le ((m, d):mem) sys_mmap_body E0 le´
(m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
assert(iflags: ikern d = true ∧ pg d = true ∧ ihost d = true).
{
functional inversion H2; subst.
eauto.
}
destruct iflags as [ikern iflags].
destruct iflags as [pg ihost].
destruct HINV.
assert(negval: Int.repr (-4096) = Int.repr (4294963200)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
assert(negval1: Int.repr (-268435456) = Int.repr (4026531840)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
functional inversion H2; subst.
functional inversion H3; subst.
functional inversion H4; subst.
unfold andb, orb in H5.
subdestruct.
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
destruct (Zdivide_dec 4096 (Int.unsigned n) AuxStateDataType.HPS).
unfold Z.divide in ×.
destruct d0.
destruct d1.
Focus 2.
simpl in ×.
discriminate Hdestruct0.
Focus 2.
simpl in ×.
discriminate Hdestruct.
exploit (Z.mod_unique_pos (Int.unsigned n0) 4096 x 0).
omega.
omega.
intro n0modval.
exploit (Z.mod_unique_pos (Int.unsigned n) 4096 x0 0).
omega.
omega.
intro nmodval.
destruct (zle_le 655360 (Int.unsigned n0) 1699840).
simpl in ×.
discriminate Hdestruct1.
destruct (zle_le 1073741824 (Int.unsigned n0) 4026527744).
simpl in ×.
discriminate H5.
unfold sys_mmap_body.
rewrite negval, negval1.
destruct o.
{
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H25, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
}
destruct o0.
{
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H25, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
}
{
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H25, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
repeat vcgen.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat ptreesolve.
repeat vcgen.
repeat vcgen.
}
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
destruct (Zdivide_dec 4096 (Int.unsigned n) AuxStateDataType.HPS).
simpl in ×.
discriminate Hdestruct0.
Focus 2.
simpl in ×.
discriminate Hdestruct.
unfold Z.divide in d0.
destruct d0.
exploit (Z.mod_unique_pos (Int.unsigned n0) 4096 x 0).
omega.
omega.
intro n0modval.
assert(nmodneq0: 0 ≠ Int.unsigned n mod 4096).
{
intro.
symmetry in H7.
eapply Z.mod_divide in H7.
contradiction.
omega.
}
assert(0 ≤ Int.unsigned n mod 4096 < 4096).
{
apply Z.mod_bound_pos.
discharge_unsigned_range.
omega.
}
unfold sys_mmap_body.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H25, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
destruct (Zdivide_dec 4096 (Int.unsigned n0) AuxStateDataType.HPS).
simpl in ×.
discriminate Hdestruct.
assert(nmodneq0: 0 ≠ Int.unsigned n0 mod 4096).
{
intro.
symmetry in H7.
eapply Z.mod_divide in H7.
contradiction.
omega.
}
assert(0 ≤ Int.unsigned n0 mod 4096 < 4096).
{
apply Z.mod_bound_pos.
discharge_unsigned_range.
omega.
}
unfold sys_mmap_body.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
rewrite H25, ikern, ihost.
rewrite Int.unsigned_repr.
reflexivity.
omega.
repeat vcgen.
repeat vcgen.
repeat vcgen.
discharge_cmp.
discharge_unsigned_range.
discharge_unsigned_range.
repeat vcgen.
discharge_cmp.
discharge_cmp.
ptreesolve.
discharge_cmp.
repeat vcgen.
discharge_cmp.
repeat ptreesolve.
discharge_cmp.
repeat vcgen.
Qed.
Lemma sys_mmap_body_correct: ∀ m d d´ env le,
env = PTree.empty _ →
trap_mmap_spec d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_mmap_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
assert(iflags: ikern d = true ∧ pg d = true ∧ ihost d = true ∧ init d = true).
{
functional inversion H0; subst.
functional inversion H3; auto.
functional inversion H3; auto.
functional inversion H3; auto.
}
destruct iflags as [ikern iflags].
destruct iflags as [pg iflags].
destruct iflags as [ihost iinit].
rename H1 into HINV.
generalize HINV; intro tmp; destruct tmp.
assert(negval: Int.repr (-4096) = Int.repr (4294963200)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
assert(negval1: Int.repr (-268435456) = Int.repr (4026531840)).
{
apply Int.eqm_samerepr.
unfold Int.eqm.
unfold Int.eqmod.
∃ (-1).
repeat autounfold.
unfold two_power_nat, shift_nat.
simpl.
reflexivity.
}
functional inversion H0; subst.
{
unfold hpa0 in ×.
eapply (sys_mmap_body_correct_aux1 hpa hpa´); eauto.
}
{
unfold hpa0 in ×.
eapply (sys_mmap_body_correct_aux2 hpa); eauto.
}
{
eapply sys_mmap_body_correct_aux3; eauto.
}
Qed.
End SysMMapBody.
Theorem sys_mmap_code_correct:
spec_le (sys_mmap ↦ trap_mmap_spec_low) (〚sys_mmap ↦ f_sys_mmap 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sys_mmap_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 m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_mmap)
nil
(create_undef_temps (fn_temps f_sys_mmap)))) H1.
Qed.
End SYSMMAP.
Section SYSPROCCREATE.
Let L: compatlayer (cdata RData) := uctx_arg2 ↦ gensem uctx_arg2_spec
⊕ uctx_arg3 ↦ gensem uctx_arg3_spec
⊕ uctx_set_errno ↦ gensem uctx_set_errno_spec
⊕ uctx_set_retval1 ↦ gensem uctx_set_retval1_spec
⊕ get_curid ↦ gensem thread_get_curid_spec
⊕ container_can_consume ↦ gensem thread_container_can_consume_spec
⊕ proc_create ↦ proc_create_compatsem big2_proc_create_spec
⊕ proc_create_postinit ↦ gensem thread_proc_create_postinit_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SysProcCreateBody.
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 tint 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 tint 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).
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).
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 tint cc_default)) Tnil tint cc_default).
container_can_consume
Variable bcan_consume: block.
Hypothesis hcan_consume1 : Genv.find_symbol ge container_can_consume = Some bcan_consume.
Hypothesis hcan_consume2 : Genv.find_funct_ptr ge bcan_consume = Some (External (EF_external container_can_consume (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default)) (Tcons tint (Tcons tint Tnil)) tint cc_default).
proc_create
Variable bproc_create: block.
Hypothesis hproc_create1 : Genv.find_symbol ge proc_create = Some bproc_create.
Hypothesis hproc_create2 : Genv.find_funct_ptr ge bproc_create = Some (External (EF_external proc_create (signature_of_type (Tcons tint (Tcons (tptr tvoid) (Tcons tint Tnil))) tint cc_default)) (Tcons tint (Tcons (tptr tvoid) (Tcons tint Tnil))) tint cc_default).
proc_create_postinit
Variable bproc_create_postinit: block.
Hypothesis hproc_create_postinit1 : Genv.find_symbol ge proc_create_postinit = Some bproc_create_postinit.
Hypothesis hproc_create_postinit2 : Genv.find_funct_ptr ge bproc_create_postinit = Some (External (EF_external proc_create_postinit (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Lemma sys_proc_create_body_correct:
∀ m d d´ env le,
env = PTree.empty _ →
trap_proc_create_spec sc m d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) sys_proc_create_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize (tptrsize tvoid).
intros.
subst.
destruct H2.
destruct valid_container0.
rename H1 into Hspec; unfold trap_proc_create_spec in Hspec.
unfold thread_container_can_consume_spec.
unfold ObjContainer.container_can_consume_spec.
unfold sys_proc_create_body.
subdestruct; subst.
{ functional inversion Hspec; subst.
functional inversion Hdestruct1; subst.
functional inversion Hdestruct0; subst.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
subrewrite´.
rewrite Int.unsigned_repr; eauto; omega.
subrewrite´.
rewrite Int.unsigned_repr.
unfold thread_container_can_consume_spec.
rewrite zeq_true.
rewrite H14, H16, H17, H18.
unfold curid0, cpu1 in H19.
rewrite H19.
instantiate (1:= Int.zero); simpl.
unfold Int.zero; rewrite Int.unsigned_repr.
unfold c in H12.
rewrite H12.
reflexivity.
omega.
omega.
discharge_cmp.
repeat vcgen. }
{ functional inversion Hspec; subst.
functional inversion Hdestruct1; subst.
functional inversion Hdestruct0; subst.
unfold ELF_ident in Hdestruct6.
unfold Int.eq in Hdestruct14.
subdestruct.
injection Hdestruct6; intros; subst.
inv Hdestruct6.
rewrite Hdestruct8 in Hdestruct10.
injection Hdestruct10; intros; subst.
clear Hdestruct10.
clear Hdestruct2.
apply unsigned_inj in e.
generalize Hdestruct15; intro proc_create_inv.
unfold big2_proc_create_spec in proc_create_inv.
subdestruct.
inv proc_create_inv.
subst.
destruct a0.
specialize (cvalid_quota (ZMap.get (CPU_ID d) (cid d))); specialize (cvalid_usage (ZMap.get (CPU_ID d) (cid d))).
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
subrewrite´.
rewrite Int.unsigned_repr; eauto; omega.
subrewrite´.
unfold thread_container_can_consume_spec.
repeat rewrite Int.unsigned_repr; try omega.
subrewrite´.
omega.
discharge_cmp.
d2 vcgen.
repeat vcgen.
instantiate (1 := Int.zero).
unfold Int.zero.
rewrite Int.unsigned_repr; auto.
omega.
d2 vcgen.
d3 vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold thread_proc_create_postinit_spec.
subrewrite´.
repeat vcgen.
repeat vcgen.
erewrite stencil_matches_symbols; eauto.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold big2_proc_create_spec.
subrewrite´.
rewrite Int.unsigned_repr; eauto; omega.
rewrite Int.unsigned_repr; eauto; omega. }
{ functional inversion Hspec; subst.
functional inversion Hdestruct3; subst.
functional inversion Hdestruct2; subst.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
subrewrite´.
rewrite Int.unsigned_repr; eauto; omega.
subrewrite´.
rewrite Int.unsigned_repr.
unfold thread_container_can_consume_spec.
rewrite zeq_true.
rewrite H14, H16, H17, H18.
unfold curid0, cpu1 in H19.
rewrite H19.
instantiate (1:= Int.zero); simpl.
unfold Int.zero; rewrite Int.unsigned_repr.
unfold c in H12.
rewrite H12.
reflexivity.
omega.
omega.
discharge_cmp.
repeat vcgen. }
{ functional inversion Hspec; subst.
functional inversion Hdestruct3; subst.
functional inversion Hdestruct2; subst.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
subrewrite´.
rewrite Int.unsigned_repr; eauto; omega.
subrewrite´.
rewrite Int.unsigned_repr.
unfold thread_container_can_consume_spec.
rewrite zeq_true.
rewrite H14, H16, H17, H18.
unfold curid0, cpu1 in H19.
rewrite H19.
instantiate (1:= Int.zero); simpl.
unfold Int.zero; rewrite Int.unsigned_repr.
unfold c in H12.
rewrite H12.
reflexivity.
omega.
omega.
discharge_cmp.
repeat vcgen. }
{ functional inversion Hspec; subst.
functional inversion Hdestruct2; subst.
functional inversion Hdestruct1; subst.
esplit.
repeat vcgen.
unfold thread_get_curid_spec.
unfold ObjMultiprocessor.get_curid_spec.
subrewrite´.
rewrite Int.unsigned_repr; eauto; omega.
subrewrite´.
rewrite Int.unsigned_repr.
unfold thread_container_can_consume_spec.
rewrite zeq_true.
rewrite H14, H16, H17, H18.
unfold curid0, cpu1 in H19.
rewrite H19.
instantiate (1:= Int.zero); simpl.
unfold Int.zero; rewrite Int.unsigned_repr.
unfold c in H12.
rewrite H12.
reflexivity.
omega.
omega.
discharge_cmp.
repeat vcgen. }
Qed.
End SysProcCreateBody.
Theorem sys_proc_create_code_correct:
spec_le (sys_proc_create ↦ trap_proc_create_spec_low) (〚sys_proc_create ↦ f_sys_proc_create 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (sys_proc_create_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
m´0 labd labd0 (PTree.empty _)
(bind_parameter_temps´ (fn_params f_sys_proc_create) nil
(create_undef_temps (fn_temps f_sys_proc_create)))) H0.
Qed.
End SYSPROCCREATE.
End WithPrimitives.
End TTRAPARGCODE2.