Library mcertikos.mm.MPTCommonCode
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 TacticsForTesting.
Require Import XOmega.
Require Import AbstractDataType.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import MPTCommon.
Require Import MPTCommonCSource.
Require Import PTKernGenSpec.
Module MPTCOMMONCODE.
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}.
Section PTRMV.
Let L: compatlayer (cdata RData) := pt_read ↦ gensem ptRead_spec
⊕ pt_rmv_aux ↦ gensem ptRmvAux_spec
⊕ at_get_c ↦ gensem get_at_c_spec
⊕ at_set_c ↦ gensem set_at_c0_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 PTRmvBody.
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 TacticsForTesting.
Require Import XOmega.
Require Import AbstractDataType.
Require Import CalRealPTPool.
Require Import CalRealPT.
Require Import MPTCommon.
Require Import MPTCommonCSource.
Require Import PTKernGenSpec.
Module MPTCOMMONCODE.
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}.
Section PTRMV.
Let L: compatlayer (cdata RData) := pt_read ↦ gensem ptRead_spec
⊕ pt_rmv_aux ↦ gensem ptRmvAux_spec
⊕ at_get_c ↦ gensem get_at_c_spec
⊕ at_set_c ↦ gensem set_at_c0_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 PTRmvBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
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_rmv_aux
Variable bpt_rmv_aux: block.
Hypothesis hpt_rmv_aux1 : Genv.find_symbol ge pt_rmv_aux = Some bpt_rmv_aux.
Hypothesis hpt_rmv_aux2 : Genv.find_funct_ptr ge bpt_rmv_aux =
Some (External (EF_external pt_rmv_aux
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
at_get_c
Variable bat_get_c: block.
Hypothesis hat_get_c1 : Genv.find_symbol ge at_get_c = Some bat_get_c.
Hypothesis hat_get_c2 : Genv.find_funct_ptr ge bat_get_c =
Some (External (EF_external at_get_c
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
at_set_c
Variable bat_set_c: block.
Hypothesis hat_set_c1 : Genv.find_symbol ge at_set_c = Some bat_set_c.
Hypothesis hat_set_c2 : Genv.find_funct_ptr ge bat_set_c =
Some (External (EF_external at_set_c
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Lemma pt_rmv_body_correct: ∀ m d d´ env le proc_index vadr v,
env = PTree.empty _ →
PTree.get tproc_index le = Some (Vint proc_index) →
PTree.get tvadr le = Some (Vint vadr) →
ptRmv_spec (Int.unsigned proc_index) (Int.unsigned vadr) d = Some (d´, Int.unsigned v) →
∃ le´,
exec_stmt ge env le ((m, d): mem) pt_rmv_body E0
le´ (m, d´) (Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize one_k_minus1; intro one_k_minus1.
intros.
subst.
unfold pt_rmv_body.
functional inversion H2; subst.
{
unfold pt, pdi, pti, pdt´, pt´ in ×.
functional inversion H4.
assert(range: 0 < Int.unsigned v × 4096 + PermtoZ _x1 ≤ Int.max_unsigned).
{
unfold PermtoZ.
destruct _x1; try omega.
destruct b; omega.
}
assert(divval: (Int.unsigned v × 4096 + PermtoZ _x1) / 4096 = Int.unsigned v).
{
destruct _x1; simpl.
xomega.
xomega.
destruct b; xomega.
}
esplit.
repeat vcgen.
unfold ptRead_spec.
unfold getPTE_spec, getPDE_spec.
rewrite H6, H7, H8, H9.
unfold PTE_Arg.
unfold PDE_Arg.
rewrite zle_lt_true.
rewrite zle_le_true.
rewrite zle_le_true.
rewrite H11, H12, H13.
destruct (zeq pi 0); try omega.
instantiate (1:= (Int.repr (Int.unsigned v × 4096 + PermtoZ _x1))).
rewrite Int.unsigned_repr; try omega.
reflexivity.
unfold PTX.
assert (0 < one_k) by omega.
generalize (Z.mod_pos_bound (Int.unsigned vadr / 4096) one_k H17); intro.
change ((Int.max_unsigned / 4096) mod 1024) with 1023.
omega.
unfold PDX.
xomega.
omega.
discharge_cmp.
repeat vcgen.
unfold ptRmvAux_spec.
unfold rmvPTE_spec.
rewrite H6, H7, H8, H9.
unfold PTE_Arg.
unfold PDE_Arg.
rewrite zle_lt_true.
rewrite zle_le_true.
rewrite zle_le_true.
rewrite H10, H11.
reflexivity.
unfold PTX.
assert (0 < one_k) by omega.
generalize (Z.mod_pos_bound (Int.unsigned vadr / 4096) one_k H17); intro.
change ((Int.max_unsigned / 4096) mod 1024) with 1023.
omega.
unfold PDX.
xomega.
omega.
rewrite divval.
unfold get_at_c_spec.
simpl.
rewrite H8, H9, H15.
rewrite zle_lt_true.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr; try omega.
reflexivity.
omega.
discharge_cmp.
repeat vcgen.
rewrite divval.
unfold set_at_c0_spec.
simpl.
rewrite H8, H9, H15.
rewrite zle_lt_true.
reflexivity.
omega.
repeat vcgen.
simpl.
unfold sem_div.
unfold sem_binarith; simpl.
discharge_cmp.
rewrite divval.
rewrite Int.repr_unsigned.
reflexivity.
}
{
unfold pt, pdi, pti in ×.
functional inversion H4.
esplit.
repeat vcgen.
unfold ptRead_spec.
unfold getPTE_spec.
unfold getPDE_spec.
rewrite H6, H7, H8, H9.
unfold PTE_Arg.
unfold PDE_Arg.
rewrite zle_lt_true.
rewrite zle_le_true.
rewrite zle_le_true.
rewrite H11, H13.
destruct (zeq pi 0); try omega.
rewrite zlt_lt_true.
change 0 with (Int.unsigned Int.zero).
reflexivity.
omega.
unfold PTX.
assert (0 < one_k) by omega.
generalize (Z.mod_pos_bound (Int.unsigned vadr / 4096) one_k H15); intro.
change ((Int.max_unsigned / 4096) mod 1024) with 1023.
omega.
unfold PDX.
xomega.
omega.
discharge_cmp.
repeat vcgen.
simpl.
rewrite PTree.gss.
f_equal.
simpl.
unfold sem_div.
unfold sem_binarith; simpl.
discharge_cmp.
f_equal.
f_equal.
erewrite <- unsigned_inj.
reflexivity.
rewrite <- H3.
rewrite Int.unsigned_repr.
reflexivity.
xomega.
}
Qed.
End PTRmvBody.
Theorem pt_rmv_code_correct:
spec_le (pt_rmv ↦ ptRmv_spec_low) (〚pt_rmv ↦ f_pt_rmv 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pt_rmv_body_correct s (Genv.globalenv p) makeglobalenv b0 Hb0fs Hb0fp b1
Hb1fs Hb1fp b2 Hb2fs Hb2fp b3 Hb3fs Hb3fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_pt_rmv)
(Vint n::Vint vadr::nil)
(create_undef_temps (fn_temps f_pt_rmv)))) H0.
Qed.
End PTRMV.
Section PTINSERT.
Let L: compatlayer (cdata RData) := pt_read_pde ↦ gensem ptReadPDE_spec
⊕ pt_insert_aux ↦ gensem ptInsertAux_spec
⊕ pt_alloc_pde ↦ gensem ptAllocPDE_spec
⊕ at_get_c ↦ gensem get_at_c_spec
⊕ at_set_c ↦ gensem set_at_c0_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 PTInsertBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
pt_read_pde
Variable bpt_read_pde: block.
Hypothesis hpt_read_pde1 : Genv.find_symbol ge pt_read_pde = Some bpt_read_pde.
Hypothesis hpt_read_pde2 : Genv.find_funct_ptr ge bpt_read_pde =
Some (External (EF_external pt_read_pde
(signature_of_type (Tcons tint (Tcons tint Tnil)) tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
pt_insert_aux
Variable bpt_insert_aux: block.
Hypothesis hpt_insert_aux1 : Genv.find_symbol ge pt_insert_aux = Some bpt_insert_aux.
Hypothesis hpt_insert_aux2 : Genv.find_funct_ptr ge bpt_insert_aux =
Some (External (EF_external pt_insert_aux
(signature_of_type
(Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil))))
Tvoid cc_default))
(Tcons tint (Tcons tint (Tcons tint (Tcons tint Tnil)))) Tvoid cc_default).
pt_alloc_pde
Variable bpt_alloc_pde: block.
Hypothesis hpt_alloc_pde1 : Genv.find_symbol ge pt_alloc_pde = Some bpt_alloc_pde.
Hypothesis hpt_alloc_pde2 : Genv.find_funct_ptr ge bpt_alloc_pde =
Some (External (EF_external pt_alloc_pde
(signature_of_type (Tcons tint (Tcons tint Tnil))
tint cc_default))
(Tcons tint (Tcons tint Tnil)) tint cc_default).
at_get_c
Variable bat_get_c: block.
Hypothesis hat_get_c1 : Genv.find_symbol ge at_get_c = Some bat_get_c.
Hypothesis hat_get_c2 : Genv.find_funct_ptr ge bat_get_c =
Some (External (EF_external at_get_c
(signature_of_type (Tcons tint Tnil) tint cc_default))
(Tcons tint Tnil) tint cc_default).
at_set_c
Variable bat_set_c: block.
Hypothesis hat_set_c1 : Genv.find_symbol ge at_set_c = Some bat_set_c.
Hypothesis hat_set_c2 : Genv.find_funct_ptr ge bat_set_c =
Some (External (EF_external at_set_c
(signature_of_type (Tcons tint (Tcons tint Tnil))
Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
Require Import CommonTactic.
Lemma lpalloc_prop:
∀ n d d´ v,
lpalloc_spec n d = Some (d´, v) →
ipt d´ = ipt d
∧ PT d´ = PT d
∧ nps d´ = nps d
∧ ptpool d´ = ptpool d
∧ (v ≠ 0 →
0 < v < nps d).
Proof.
clear.
intros.
unfold lpalloc_spec in H.
subdestruct; simpl in ×.
- destruct a0.
inversion H; subst; simpl.
tauto.
- inv H; simpl.
tauto.
- inv H; simpl.
tauto.
Qed.
Lemma pt_insert_body_correct: ∀ m d d´ env le proc_index vadr padr perm v,
env = PTree.empty _ →
PTree.get tproc_index le = Some (Vint proc_index) →
PTree.get tvadr le = Some (Vint vadr) →
PTree.get tpadr le = Some (Vint padr) →
PTree.get tperm le = Some (Vint perm) →
ptInsert_spec (Int.unsigned proc_index) (Int.unsigned vadr)
(Int.unsigned padr) (Int.unsigned perm) d = Some (d´, Int.unsigned v) →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) pt_insert_body E0
le´ (m, d´) (Out_return (Some (Vint v, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize one_k_minus1; intro one_k_minus1.
intros.
subst.
unfold pt_insert_body.
destruct H5.
functional inversion H4; subst.
{
generalize (valid_nps H9); intro npsrange.
functional inversion H14; subst.
functional inversion H6; subst.
functional inversion H; subst.
unfold pt, pdi, pti, pt0, pdi0, pti0, pdt´, pt´ in ×.
esplit.
repeat vcgen.
- unfold ptReadPDE_spec.
unfold getPDE_spec.
rewrite H8, H9, H10, H11.
unfold PDE_Arg.
rewrite zle_lt_true.
rewrite zle_le_true.
rewrite H19.
instantiate (1:= Int.repr pi0).
rewrite Int.unsigned_repr.
reflexivity.
omega.
unfold PDX.
xomega.
omega.
- discharge_cmp.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
+ unfold ptInsertAux_spec.
unfold setPTE_spec.
subrewrite´.
unfold PTE_Arg.
unfold PDE_Arg.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
rewrite zle_le_true; try omega.
reflexivity.
unfold PTX.
assert (0 < one_k) by omega.
generalize (Z.mod_pos_bound (Int.unsigned vadr / 4096) one_k H27); intro.
change ((Int.max_unsigned / 4096) mod 1024) with 1023.
omega.
unfold PDX.
xomega.
+ unfold get_at_c_spec.
simpl.
subrewrite´.
rewrite zle_lt_true.
instantiate (1:= Int.repr c).
rewrite Int.unsigned_repr; try omega.
reflexivity.
omega.
+ unfold set_at_c0_spec.
simpl.
subrewrite´.
rewrite zle_lt_true.
rewrite Int.unsigned_repr.
reflexivity.
omega.
omega.
+ repeat vcgen.
- simpl.
rewrite H5.
rewrite Int.repr_unsigned.
repeat vcgen. }
{ generalize (valid_nps H9); intro npsrange.
unfold pt, pdi, pti in ×.
functional inversion H6; subst.
functional inversion H; subst.
esplit.
repeat vcgen.
- unfold ptReadPDE_spec.
unfold getPDE_spec.
rewrite H8, H9, H10, H11, H13.
unfold PDE_Arg.
rewrite zle_lt_true.
rewrite zle_le_true.
change 0 with (Int.unsigned Int.zero).
reflexivity.
unfold PDX.
xomega.
omega.
- discharge_cmp.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- repeat vcgen.
- simpl.
rewrite H5.
rewrite Int.repr_unsigned.
repeat vcgen. }
{ generalize (valid_nps H9); intro npsrange.
unfold pt, pdi, pti in ×.
functional inversion H6; subst.
functional inversion H; subst.
functional inversion H14.
- unfold pdi0 in ×.
functional inversion H16.
assert (v_val: v = Int.zero).
{ unfold Int.zero.
rewrite <- _x4.
rewrite Int.repr_unsigned.
auto. }
unfold pt0, pdi1, pti0, pdt´, pt´ in ×.
rewrite <- H19, <- H31 in *; simpl in ×.
destruct _x.
trivial.
- unfold pdi0 in ×.
functional inversion H16. idtac.
unfold pt0, pdi1, pti0, pdt´, pt´ in ×.
rewrite <- H19, <- H31 in *; simpl in ×.
simpl.
exploit lpalloc_prop; eauto.
intros (Hipt & HPT & Hnps & Hptpool & Hrange).
subrewrite´.
esplit.
repeat vcgen.
+ unfold ptReadPDE_spec.
unfold getPDE_spec.
subrewrite´.
unfold PDE_Arg.
rewrite zle_lt_true.
rewrite zle_le_true.
change 0 with (Int.unsigned Int.zero).
reflexivity.
unfold PDX.
xomega.
omega.
+ discharge_cmp.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ repeat vcgen.
+ simpl.
repeat vcgen.
× unfold ptInsertAux_spec.
unfold setPTE_spec.
simpl.
subrewrite´.
repeat rewrite ZMap.gss.
unfold PTE_Arg.
unfold PDE_Arg.
rewrite zle_lt_true; try omega.
rewrite zle_le_true; try omega.
rewrite zle_le_true; try omega.
reflexivity.
unfold PTX.
assert (0 < one_k) by omega.
generalize (Z.mod_pos_bound (Int.unsigned vadr / 4096) one_k H41); intro.
change ((Int.max_unsigned / 4096) mod 1024) with 1023.
omega.
unfold PDX.
xomega.
× unfold get_at_c_spec.
simpl. rewrite <- H19.
simpl.
subrewrite´.
rewrite zle_lt_true.
instantiate (1:= Int.repr c0).
rewrite Int.unsigned_repr; try omega.
reflexivity.
omega.
× unfold set_at_c0_spec.
simpl. rewrite <- H19.
simpl.
subrewrite´.
rewrite zle_lt_true.
repeat rewrite Int.unsigned_repr; try omega.
simpl.
unfold pdt´, pt0, pdi1 in ×.
rewrite <- H31.
rewrite <- H19.
simpl.
subrewrite´.
repeat rewrite ZMap.gss.
assert (HSpeed:
∀ d ptp a,
Some (d {ptpool: ptp} {ATC: a})
= ret (d {ATC: a} {ptpool: ptp})).
{ intros. reflexivity. }
apply HSpeed.
omega.
× repeat vcgen.
+ repeat vcgen.
}
Qed.
End PTInsertBody.
Theorem pt_insert_code_correct:
spec_le (pt_insert ↦ ptInsert_spec_low) (〚pt_insert ↦ f_pt_insert 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pt_insert_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 labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_pt_insert)
(Vint n::Vint vadr::Vint padr::Vint p0::nil)
(create_undef_temps (fn_temps f_pt_insert)))) H0.
Qed.
End PTINSERT.
End WithPrimitives.
End MPTCOMMONCODE.