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 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 Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import XOmega.
Require Import CommonTactic.
Require Import AbstractDataType.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import MPTInit.
Require Import MPTInitCSource.
Require Import PTNewGenSpec.
Module MPTINITCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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}.
Lemma palloc_prop´:
∀ i z d d´,
palloc_spec i d = Some (d´, z) →
pg d = true
∧ nps d´ = nps d
∧ (262144 ≤ nps d ≤ 1048576 →
0 ≤ z ≤ 1048577).
Proof.
intros.
unfold palloc_spec in H.
subdestruct;
inv H;
simpl.
destruct a0.
repeat (split; eauto); omega.
repeat (split; eauto); omega.
repeat (split; eauto); omega.
Qed.
Lemma ptInsert0_prop´:
∀ i v b p z d d´,
ptInsert0_spec i v b p d = Some (d´, z) →
262144 ≤ nps d ≤ 1048576 →
0 ≤ z ≤ 1048577.
Proof.
intros.
functional inversion H; try omega.
functional inversion H10.
- exploit palloc_prop´; eauto.
intros (_ & Hr). eapply Hr. auto.
- exploit palloc_prop´; eauto.
intros (_ & Hr). eapply Hr. auto.
Qed.
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).
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 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 Clight.
Require Import CDataTypes.
Require Import Ctypes.
Require Import XOmega.
Require Import CommonTactic.
Require Import AbstractDataType.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import MPTInit.
Require Import MPTInitCSource.
Require Import PTNewGenSpec.
Module MPTINITCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
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}.
Lemma palloc_prop´:
∀ i z d d´,
palloc_spec i d = Some (d´, z) →
pg d = true
∧ nps d´ = nps d
∧ (262144 ≤ nps d ≤ 1048576 →
0 ≤ z ≤ 1048577).
Proof.
intros.
unfold palloc_spec in H.
subdestruct;
inv H;
simpl.
destruct a0.
repeat (split; eauto); omega.
repeat (split; eauto); omega.
repeat (split; eauto); omega.
Qed.
Lemma ptInsert0_prop´:
∀ i v b p z d d´,
ptInsert0_spec i v b p d = Some (d´, z) →
262144 ≤ nps d ≤ 1048576 →
0 ≤ z ≤ 1048577.
Proof.
intros.
functional inversion H; try omega.
functional inversion H10.
- exploit palloc_prop´; eauto.
intros (_ & Hr). eapply Hr. auto.
- exploit palloc_prop´; eauto.
intros (_ & Hr). eapply Hr. auto.
Qed.
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 bpt_init: block.
Hypothesis hp_tinit1 : Genv.find_symbol ge pt_init = Some bpt_init.
Hypothesis hpt_init2 : Genv.find_funct_ptr ge bpt_init =
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´ →
kernel_mode d→
high_level_invariant d →
∃ le´,
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; subst.
esplit; repeat vcgen.
Qed.
End PMapInitBody.
Theorem pmap_init_code_correct:
spec_le (pmap_init ↦ pmap_init_spec_low) (〚pmap_init ↦ f_pmap_init 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
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.
Section PTRESV.
Let L: compatlayer (cdata RData) :=
palloc ↦ gensem palloc_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).
palloc
Variable bpalloc: block.
Hypothesis hpalloc1 : Genv.find_symbol ge palloc = Some bpalloc.
Hypothesis hpalloc2 : Genv.find_funct_ptr ge bpalloc =
Some (External (EF_external palloc
(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.
esplit.
rewrite <- Int.repr_unsigned with v.
rewrite <- H5.
repeat vcgen.
assert(hinv´: high_level_invariant abd´).
{
eapply palloc_high_level_inv; eauto.
}
assert(brange: 0 ≤ b ≤ Int.max_unsigned).
{
inv hinv´.
assert(pg´: pg abd´ = true).
{
functional inversion H; subst; eauto.
}
eapply valid_nps0 in pg´.
functional inversion H;
functional inversion H9; subst;
try omega.
}
esplit.
repeat vcgen.
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 PTRESV2.
Let L: compatlayer (cdata RData) :=
palloc ↦ gensem palloc_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).
palloc
Variable bpalloc: block.
Hypothesis hpalloc1 : Genv.find_symbol ge palloc = Some bpalloc.
Hypothesis hpalloc2 : Genv.find_funct_ptr ge bpalloc =
Some (External (EF_external palloc
(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.repr_unsigned with v.
rewrite <- H8.
esplit.
repeat vcgen.
assert(hinv´: high_level_invariant abd´).
{
eapply palloc_high_level_inv; eauto.
}
assert(brange: 0 ≤ b ≤ Int.max_unsigned).
{
inv hinv´.
assert(pg´: pg abd´ = true).
{
functional inversion H11; subst; eauto.
}
eapply valid_nps0 in pg´.
functional inversion H11;
try functional inversion H13; subst;
try omega.
functional inversion H14; subst;
omega.
}
rewrite <- Int.repr_unsigned with v.
rewrite <- H8.
esplit.
repeat vcgen.
assert(hinv´: high_level_invariant abd´).
{
eapply palloc_high_level_inv; eauto.
}
assert(brange: 0 ≤ b ≤ Int.max_unsigned).
{
inv hinv´.
assert(pg´: pg abd´ = true).
{
functional inversion H10; subst; eauto.
}
eapply valid_nps0 in pg´.
functional inversion H10;
try functional inversion H14; subst;
try omega.
}
assert(v0range: 0 ≤ v0 ≤ Int.max_unsigned).
{
assert(0 ≤ v0 ≤ 1048577).
{
eapply ptInsert0_prop´; eauto.
inv hinv´.
eapply valid_nps0.
functional inversion H10; subst; eauto.
}
omega.
}
esplit.
repeat vcgen.
rewrite <- Int.unsigned_repr with v0 in H10; eauto.
discharge_cmp.
omega.
omega.
repeat vcgen.
simpl.
ptreesolve.
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.
intros.
functional inversion H0; subst.
unfold pt_new_body.
esplit; repeat vcgen.
unfold container_split_spec.
fold c; fold parent.
rewrite H12, H11, H9, H8, H7, H6, H5.
unfold ret; unfold option_monad_ops.
repeat f_equal.
assumption.
Qed.
End PTNewBody.
Theorem pt_new_code_correct:
spec_le (pt_new ↦ pt_new_spec_low) (〚pt_new ↦ f_pt_new 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
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.
End WithPrimitives.
End MPTINITCODE.