Library mcertikos.mm.MPTInitCode
Require Import TacticsForTesting.
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import MPTInit.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import PTNewGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import XOmega.
Require Import AbstractDataType.
Require Import MPTInitCSource.
Module MPTINITCODE.
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 PTRESV2.
Let L: compatlayer (cdata RData) := container_alloc ↦ gensem alloc_spec
⊕ pt_insert ↦ gensem ptInsert0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTResv2Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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 MPTInit.
Require Import ZArith.Zwf.
Require Import RealParams.
Require Import LoopProof.
Require Import VCGen.
Require Import liblayers.compcertx.Stencil.
Require Import liblayers.compcertx.MakeProgram.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import CompatClightSem.
Require Import PrimSemantics.
Require Import PTNewGenSpec.
Require Import Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import XOmega.
Require Import AbstractDataType.
Require Import MPTInitCSource.
Module MPTINITCODE.
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 PTRESV2.
Let L: compatlayer (cdata RData) := container_alloc ↦ gensem alloc_spec
⊕ pt_insert ↦ gensem ptInsert0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTResv2Body.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
container_alloc
Variable balloc: block.
Hypothesis halloc1 : Genv.find_symbol ge container_alloc = Some balloc.
Hypothesis halloc2 : Genv.find_funct_ptr ge balloc = Some (External (EF_external container_alloc (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
pt_insert2
Variable bptinsert: block.
Hypothesis hpt_insert1 : Genv.find_symbol ge pt_insert = Some bptinsert.
Hypothesis hpt_insert2 : Genv.find_funct_ptr ge bptinsert = Some (External (EF_external pt_insert (signature_of_type (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default).
Lemma pt_resv2_body_correct: ∀ m d d' env le proc_index vaddr perm proc_index2 vaddr2 perm2 v,
env = PTree.empty _ →
PTree.get tproc_index le = Some (Vint proc_index) →
PTree.get tvaddr le = Some (Vint vaddr) →
PTree.get tperm le = Some (Vint perm) →
PTree.get tproc_index2 le = Some (Vint proc_index2) →
PTree.get tvaddr2 le = Some (Vint vaddr2) →
PTree.get tperm2 le = Some (Vint perm2) →
ptResv2_spec (Int.unsigned proc_index) (Int.unsigned vaddr) (Int.unsigned perm) (Int.unsigned proc_index2) (Int.unsigned vaddr2) (Int.unsigned perm2) d = Some (d', Int.unsigned v) →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) pt_resv2_body E0 le' (m, d') (Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold pt_resv2_body.
inversion H7.
functional inversion H6; subst.
{
rewrite <- Int.unsigned_repr with 1048577 in H8; try omega.
apply unsigned_inj in H8.
rewrite <- H8.
functional inversion H9; subst.
{
destruct _x.
omega.
}
{
change 0 with (Int.unsigned Int.zero) in H9.
esplit.
repeat vcgen.
}
}
{
rewrite <- Int.unsigned_repr with 1048577 in H8; try omega.
apply unsigned_inj in H8.
rewrite <- H8.
functional inversion H9;subst.
{
destruct _x0.
destruct a0.
generalize (valid_nps H17); intro npsrange.
esplit.
repeat vcgen.
}
{
omega.
}
}
{
functional inversion H8; subst.
{
destruct _x1.
destruct a0.
generalize (valid_nps H17); intro npsrange.
functional inversion H10; functional inversion H28; subst; esplit; repeat vcgen.
destruct _x2.
destruct a1.
simpl in a0.
instantiate (1:= v0).
repeat vcgen.
discharge_cmp.
omega.
destruct _x2.
destruct a1.
simpl in a0.
omega.
repeat vcgen.
repeat vcgen.
}
{
omega.
}
}
Grab Existential Variables.
apply le.
apply le.
apply le.
Qed.
End PTResv2Body.
Theorem pt_resv2_code_correct:
spec_le (pt_resv2 ↦ ptResv2_spec_low) (〚pt_resv2 ↦ f_pt_resv2 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep (pt_resv2_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m'0 labd labd' (PTree.empty _)
(bind_parameter_temps' (fn_params f_pt_resv2)
(Vint n::Vint vadr::Vint p0::Vint n'::Vint vadr'::Vint p'::nil)
(create_undef_temps (fn_temps f_pt_resv2)))) H0.
Qed.
End PTRESV2.
Section PTNEW.
Let L: compatlayer (cdata RData) := container_split ↦ gensem container_split_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTNewBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
Variables (id quota: int).
container_split
Variable bsplit: block.
Hypothesis hsplit1 : Genv.find_symbol ge container_split = Some bsplit.
Hypothesis hsplit2 :
Genv.find_funct_ptr ge bsplit = Some (External
(EF_external container_split (signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
Lemma pt_new_body_correct:
∀ m d d' env le n,
env = PTree.empty _ →
pt_new_spec (Int.unsigned id) (Int.unsigned quota) d = Some (d', Int.unsigned n) →
le ! tid = Some (Vint id) → le ! tquota = Some (Vint quota) →
∃ le',
exec_stmt ge env le ((m, d): mem) pt_new_body E0 le' (m, d') (Out_return (Some (Vint n, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold pt_new_body.
functional inversion H0.
unfold update_cusage, update_cchildren in *; rewrite ZMap.gss in *; simpl in ×.
∃ (PTree.set tchild (Vint n) le).
repeat vcgen.
subst; apply PTree.gempty.
unfold container_split_spec, update_cusage, update_cchildren; subst child c i.
repeat (match goal with
| [ H : ?a = _ |- context [if ?a then _ else _] ] ⇒ rewrite H
| [ |- context [if ?a then _ else _] ] ⇒ destruct a; try omega
end).
rewrite ZMap.gss; subst.
apply f_equal with (f:= Int.repr) in H4; rewrite Int.repr_unsigned in H4; subst.
repeat vcgen.
Qed.
End PTNewBody.
Theorem pt_new_code_correct:
spec_le (pt_new ↦ pt_new_spec_low) (〚pt_new ↦ f_pt_new 〛L).
Proof.
fbigstep_pre L.
fbigstep (pt_new_body_correct s (Genv.globalenv p) makeglobalenv id q b0 Hb0fs Hb0fp
m'0 labd labd' (PTree.empty _)
(bind_parameter_temps' (fn_params f_pt_new)
(Vint id :: Vint q :: nil)
(create_undef_temps (fn_temps f_pt_new)))) H0.
Qed.
End PTNEW.
Section PTRESV.
Let L: compatlayer (cdata RData) := container_alloc ↦ gensem alloc_spec
⊕ pt_insert ↦ gensem ptInsert0_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Section PTResvBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
container_alloc
Variable balloc: block.
Hypothesis halloc1 : Genv.find_symbol ge container_alloc = Some balloc.
Hypothesis halloc2 : Genv.find_funct_ptr ge balloc = Some (External (EF_external container_alloc (signature_of_type (Tcons tint Tnil) tint cc_default)) (Tcons tint Tnil) tint cc_default).
pt_insert2
Variable bptinsert: block.
Hypothesis hpt_insert1 : Genv.find_symbol ge pt_insert = Some bptinsert.
Hypothesis hpt_insert2 : Genv.find_funct_ptr ge bptinsert = Some (External (EF_external pt_insert (signature_of_type (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default)) (Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) tint cc_default).
Lemma pt_resv_body_correct: ∀ m d d' env le proc_index vaddr perm v,
env = PTree.empty _ →
PTree.get tproc_index le = Some (Vint proc_index) →
PTree.get tvaddr le = Some (Vint vaddr) →
PTree.get tperm le = Some (Vint perm) →
ptResv_spec (Int.unsigned proc_index)
(Int.unsigned vaddr) (Int.unsigned perm) d = Some (d', Int.unsigned v) →
high_level_invariant d →
∃ le',
exec_stmt ge env le ((m, d): mem) pt_resv_body E0 le' (m, d') (Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
intros.
subst.
unfold pt_resv_body.
inversion H4.
functional inversion H3; subst.
{
rewrite <- Int.unsigned_repr with 1048577 in H5; try omega.
apply unsigned_inj in H5.
rewrite <- H5.
functional inversion H6;subst.
{
destruct _x.
destruct a0.
generalize (valid_nps H12); intro npsrange.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H6.
esplit.
repeat vcgen.
}
}
{
functional inversion H5; subst.
{
destruct _x0.
destruct a0.
generalize (valid_nps H12); intro npsrange.
esplit.
repeat vcgen.
}
{
change 0 with (Int.unsigned Int.zero) in H5.
esplit.
repeat vcgen.
}
}
Grab Existential Variables.
apply le.
apply le.
Qed.
End PTResvBody.
Theorem pt_resv_code_correct:
spec_le (pt_resv ↦ ptResv_spec_low) (〚pt_resv ↦ f_pt_resv 〛L).
Proof.
set (L' := L) in ×. unfold L in ×.
fbigstep_pre L'.
fbigstep (pt_resv_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1 Hb1fs Hb1fp m'0 labd labd' (PTree.empty _)
(bind_parameter_temps' (fn_params f_pt_resv)
(Vint n::Vint vadr::Vint p0::nil)
(create_undef_temps (fn_temps f_pt_resv)))) H0.
Qed.
End PTRESV.
Section PMAPINIT.
Let L: compatlayer (cdata RData) := pt_init ↦ gensem pt_init_spec.
Local Instance: ExternalCallsOps mem := CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem := CompatExternalCalls.compatlayer_compiler_config_ops L.
Local Open Scope Z_scope.
Section PMapInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
pt_init
Variable bptinit: block.
Hypothesis hpt_init1 : Genv.find_symbol ge pt_init = Some bptinit.
Hypothesis hpt_init2 : Genv.find_funct_ptr ge bptinit = Some (External (EF_external pt_init (signature_of_type (Tcons tint Tnil) Tvoid cc_default)) (Tcons tint Tnil) Tvoid cc_default).
Lemma pmap_init_body_correct:
∀ m d d' env le mbi_adr,
env = PTree.empty _ →
PTree.get tmbi_adr le = Some (Vint mbi_adr) →
pmap_init_spec (Int.unsigned mbi_adr) d = Some d' →
exec_stmt ge env le ((m, d): mem) pmap_init_body E0 le (m, d') Out_normal.
Proof.
intros; unfold pmap_init_body.
functional inversion H1.
change le with (set_opttemp None Vundef le); repeat vcgen.
subst; apply PTree.gempty.
unfold pt_init_spec.
repeat (match goal with
| [ H : ?a = _ |- context[if ?a then _ else _] ] ⇒ rewrite H
end); auto.
Qed.
End PMapInitBody.
Theorem pmap_init_code_correct:
spec_le (pmap_init ↦ pmap_init_spec_low) (〚pmap_init ↦ f_pmap_init 〛L).
Proof.
fbigstep_pre L.
fbigstep (pmap_init_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp
m'0 labd labd' (PTree.empty _)
(bind_parameter_temps' (fn_params f_pmap_init)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_pmap_init)))) H0.
Qed.
End PMAPINIT.
End WithPrimitives.
End MPTINITCODE.