Library mcertikos.mm.MPTCommonCodePTInitKern
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 MPTCOMMONCODEPTInitKern.
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 PTINITKERN.
Let L: compatlayer (cdata RData) := pt_init_comm ↦ gensem pt_init_comm_spec ⊕ set_PDE ↦ gensem setPDE_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 PTInitKernBody.
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 MPTCOMMONCODEPTInitKern.
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 PTINITKERN.
Let L: compatlayer (cdata RData) := pt_init_comm ↦ gensem pt_init_comm_spec ⊕ set_PDE ↦ gensem setPDE_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 PTInitKernBody.
Context `{Hwb: WritableBlockOps}.
Variable (sc: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches sc ge).
set_PDE
Variable bset_PDE: block.
Hypothesis hset_PDE1 : Genv.find_symbol ge set_PDE = Some bset_PDE.
Hypothesis hset_PDE2 : Genv.find_funct_ptr ge bset_PDE =
Some (External (EF_external set_PDE
(signature_of_type (Tcons tint (Tcons tint Tnil)) Tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) Tvoid cc_default).
pt_init_comm
Variable bptinitcomm: block.
Hypothesis hpt_init_comm1 : Genv.find_symbol ge pt_init_comm = Some bptinitcomm.
Hypothesis hpt_init_comm2 : Genv.find_funct_ptr ge bptinitcomm =
Some (External (EF_external pt_init_comm
(signature_of_type (Tcons tint Tnil) Tvoid cc_default))
(Tcons tint Tnil) Tvoid cc_default).
Definition pt_init_kern_mk_rdata adt (index: Z) := adt {ptpool: (Calculate_pt_kern (Z.to_nat (index - 256)) (ptpool adt))}.
Section pt_init_kern_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis init: init adt = true.
Hypothesis ipt: ipt adt = true.
Hypothesis pg: pg adt = false.
Hypothesis ihost: ihost adt = true.
Hypothesis ikern: ikern adt = true.
Definition pt_init_kern_loop_body_P (le: temp_env) (m: mem): Prop :=
PTree.get ti le = Some (Vint (Int.repr 256)) ∧
m = (minit, adt).
Definition pt_init_kern_loop_body_Q (le : temp_env) (m: mem): Prop :=
m = (minit, pt_init_kern_mk_rdata adt (960 - 1)).
Lemma pt_init_kern_loop_correct_aux : LoopProofSimpleWhile.t pt_init_kern_while_condition
pt_init_kern_while_body ge (PTree.empty _)
(pt_init_kern_loop_body_P) (pt_init_kern_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le (m: mem) w ⇒ ∃ i,
PTree.get ti le = Some (Vint i) ∧
256 ≤ Int.unsigned i ≤ 960 ∧
(Int.unsigned i = 256 ∧ m = (minit, adt) ∨ Int.unsigned i > 256 ∧
m =(minit, pt_init_kern_mk_rdata adt (Int.unsigned i - 1))) ∧
w = 960 - Int.unsigned i
) .
- apply Zwf_well_founded.
- intros.
unfold pt_init_kern_loop_body_P in H.
destruct H as [tile tmpH].
destruct tmpH as [pdtvalid msubst].
subst.
esplit. esplit.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [tile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [invar nval].
subst.
unfold pt_init_kern_while_condition.
unfold pt_init_kern_while_body.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
Caseeq ihigh.
+
intro ihigh.
destruct m.
case_eq invar;intros.
×
destruct a.
injection e0; intros; subst.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
∃ (960 - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split; try omega.
unfold pt_init_kern_mk_rdata.
f_equal.
f_equal; auto.
rewrite e in *; simpl.
unfold Calculate_pt_kern_at_i.
reflexivity.
×
destruct a as [ilo mval].
injection mval; intros; subst.
esplit. esplit.
repeat vcgen.
esplit. esplit.
repeat vcgen.
unfold setPDE_spec.
simpl.
rewrite ipt, pg, ihost, ikern, init.
unfold PDE_Arg.
unfold zle_lt, zle_le.
rewrite one_k_minus1.
repeat zdestruct.
∃ (960 - Int.unsigned i - 1).
repeat vcgen.
esplit.
repeat vcgen.
right.
split; try omega.
f_equal.
unfold pt_init_kern_mk_rdata.
replace (Int.unsigned i + 1 - 1 - 256) with (Z.succ (Int.unsigned i - 1 - 256)) by omega.
rewrite Z2Nat.inj_succ.
Opaque Z.of_nat.
simpl.
rewrite Nat2Z.inj_succ; try omega.
rewrite Z2Nat.id; try omega.
unfold Z.succ.
unfold Calculate_pt_kern_at_i.
assert(tmp2: (Int.unsigned i - 1 - 256 + 1 + 262144 / 1024) = Int.unsigned i).
{ change (262144 / 1024) with 256.
omega. }
rewrite tmp2.
reflexivity.
omega.
+
intro ival.
rewrite ival in ×.
esplit. esplit.
repeat vcgen.
unfold pt_init_kern_loop_body_Q.
Caseeq invar.
intro.
destruct H0.
omega.
intro tmpH.
destruct tmpH.
assumption.
Qed.
End pt_init_kern_loop_proof.
Lemma pt_init_kern_loop_correct: ∀ m adt adt´ le,
PTree.get ti le = Some (Vint (Int.repr 256)) →
init adt = true →
ipt adt = true →
pg adt = false →
ihost adt = true →
ikern adt = true →
adt´ = pt_init_kern_mk_rdata adt (960 - 1) →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, adt): mem)
(Swhile pt_init_kern_while_condition pt_init_kern_while_body) E0
le´ (m, adt´) Out_normal.
Proof.
intros.
generalize (pt_init_kern_loop_correct_aux m adt H0 H1 H2 H3 H4).
intro LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, adt) _)).
intro pre.
destruct pre as [le´´ pre].
destruct pre as [m´´ pre].
destruct pre as [pre1 pre2].
unfold pt_init_kern_loop_body_Q in pre2.
subst.
esplit; eassumption.
unfold pt_init_kern_loop_body_P.
repeat (split; auto).
Qed.
Require Import DeviceStateDataType.
Require Import CalRealPT.
Require Import CalRealPTPool.
Require Import ObjInterruptDriver.
Require Import CalTicketLock.
Require Import CalRealIDPDE.
Lemma same_num_div:
(983040 - 262144) / 1024 - 1 = 703.
Proof.
Transparent Z.sub.
xomega.
Opaque Z.sub.
Qed.
Lemma pt_init_kern_mk_rdata_eq_aux : ∀ d d´,
pt_init_kern_mk_rdata (d {ptpool : real_ptp (ptpool d´)}) (960 -1)
= d {ptpool : real_pt (ptpool d´)}.
Proof.
intros.
unfold pt_init_kern_mk_rdata. simpl.
unfold real_ptp, real_pt; simpl.
unfold real_ptp. simpl.
change (960 - 1 - 256) with 703.
change (64 - 1) with 63.
Opaque Calculate_pt_kern Calculate_pt_comm.
destruct d. destruct d´; simpl.
unfold update_ptpool. simpl. auto.
Qed.
Lemma pt_init_kern_mk_rdata_eq: ∀ d n,
pt_init_kern_mk_rdata
(((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d))
(Z.to_nat (n - 1))})
{ lapic
: (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ s : (ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))) { CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {ATC : real_ATC (ATC d)}) {nps : real_nps}) {AC : AC_init})
{init : true}) {multi_log : real_multi_log (multi_log d)})
{lock : real_lock (lock d)}) {idpde : real_idpde (idpde d)}) {ptpool : real_ptp (ptpool d)}
(960 - 1) =
(((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ lapic
: (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ s : (ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))) {CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {ATC : real_ATC (ATC d)}) {nps : real_nps}) {AC : AC_init})
{init : true}) {multi_log : real_multi_log (multi_log d)}) {lock : real_lock (lock d)})
{idpde : real_idpde (idpde d)}) {ptpool : real_pt (ptpool d)}.
Proof.
change (960 - 1 - 256) with 703.
replace (32 + 7) with 39 in *; try omega.
change (64 - 1) with 63.
intros.
remember
((((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ lapic
: (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ s : (ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))) {CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {ATC : real_ATC (ATC d)}) {nps : real_nps}) {AC : AC_init})
{init : true}) {multi_log : real_multi_log (multi_log d)}) {lock : real_lock (lock d)})
{idpde : real_idpde (idpde d)})) as adt.
rewrite pt_init_kern_mk_rdata_eq_aux.
reflexivity.
Qed.
Lemma pt_init_kern_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get tmbi_adr le = Some (Vint mbi_adr) →
pt_init_kern_spec (Int.unsigned mbi_adr) d = Some d´ →
∃ le´,
exec_stmt ge env le ((m, d): mem) pt_init_kern_body E0 le´ (m, d´) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
intros.
unfold pt_init_kern_body.
subst.
functional inversion H1.
simpl in ×.
exploit (pt_init_kern_loop_correct
m
((((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ lapic
: (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s: ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ s : (ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1)))
{ CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {ATC : real_ATC (ATC d)}) {nps : real_nps}) {AC : AC_init})
{init : true}) {multi_log : real_multi_log (multi_log d)}) {lock: real_lock (lock d)})
{idpde : real_idpde (idpde d)}) {ptpool : real_ptp (ptpool d)})
(pt_init_kern_mk_rdata
((((((((((((d { ioapic / s : ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ lapic
: (((mkLApicData
{| LapicEsr := 0;
LapicEoi := NoIntr;
LapicMaxLvt := LapicMaxLvt (s (lapic d));
LapicEnable := true;
LapicSpurious := 39;
LapicLint0Mask := true;
LapicLint1Mask := true;
LapicPcIntMask := true;
LapicLdr := 0;
LapicErrorIrq := 50;
LapicEsrClrPen := false;
LapicTpr := 0 |})
{ l1 : l1 (lapic d)}) { l2 : l2 (lapic d)}) { l3 : l3 (lapic d)}})
{ ioapic : ((ioapic d)
{ s: ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1))})
{ s : (ioapic_init_aux (s (ioapic d)) (Z.to_nat (n - 1)))
{ CurrentIrq : None}}})
{vmxinfo : real_vmxinfo}) {ATC : real_ATC (ATC d)}) {nps : real_nps}) {AC : AC_init})
{init : true}) {multi_log : real_multi_log (multi_log d)}) {lock: real_lock (lock d)})
{idpde : real_idpde (idpde d)}) {ptpool : real_ptp (ptpool d)})
(960 - 1))
(PTree.set ti (Vint (Int.repr 256)) (set_opttemp None Vundef le)));
try rewrite <- H; try assumption; try reflexivity; try (rewrite PTree.gss; reflexivity).
intro stmt.
destruct stmt as [le´ stmt].
esplit.
change E0 with (E0**E0).
econstructor.
Opaque Z.sub Z.add Z.mul Z.div.
Opaque ZMap.get ZMap.set Z.to_nat.
Opaque real_multi_log real_lock ioapic_init_aux real_idpde.
econstructor.
simpleproof.
d3 vcgen.
d3 vcgen.
d3 vcgen.
d3 vcgen.
vcgen.
vcgen.
vcgen.
unfold pt_init_comm_spec.
rewrite H2, H3, H4, H5, H6, H7.
fold n.
rewrite H8, H9.
unfold ret. unfold option_monad_ops. simpl. f_equal.
change E0 with (E0**E0).
econstructor.
vcgen.
repeat vcgen.
rewrite pt_init_kern_mk_rdata_eq in stmt.
apply stmt.
Qed.
End PTInitKernBody.
Theorem pt_init_kern_code_correct:
spec_le (pt_init_kern ↦ pt_init_kern_spec_low) (〚pt_init_kern ↦ f_pt_init_kern 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
fbigstep (pt_init_kern_body_correct s (Genv.globalenv p) makeglobalenv b1 Hb1fs Hb1fp b0 Hb0fs
Hb0fp m´0 labd labd´ (PTree.empty _)
(bind_parameter_temps´ (fn_params f_pt_init_kern)
(Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_pt_init_kern)))) H0.
Qed.
End PTINITKERN.
End WithPrimitives.
End MPTCOMMONCODEPTInitKern.