Library mcertikos.ticketlog.MBootCode
Require Import Coqlib.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
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 MBootCSource.
Require Import MBoot.
Require Import CurIDGenSpec.
Require Import AbstractDataType.
Module MBOOTCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
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}.
Opaque PTree.get PTree.set.
Local Open Scope Z_scope.
Section GETCURID.
Let L: compatlayer (cdata RData) :=
CURID_LOC ↦ curid_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetCurIDBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches s ge).
Variables bcurid_loc : block.
Hypothesis bcurid_loc1 : Genv.find_symbol ge CURID_LOC = Some bcurid_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma get_curid_body_correct:
∀ m d env le curid,
env = PTree.empty _ →
ikern d = true →
ihost d = true →
high_level_invariant d →
Mem.loadv Mint32 ((m, d): mem) (Vptr bcurid_loc (Int.repr ((CPU_ID d × 4)))) = Some (Vint curid) →
∃ le´,
exec_stmt ge env le ((m, d): mem) get_curid_body E0 le´ (m, d) (Out_return (Some (Vint curid, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros; subst.
unfold get_curid_body.
inv H2.
esplit; repeat vcgen.
unfold get_CPU_ID_spec; simpl.
rewrite H0, H1 in ×.
instantiate (1:= Int.repr (CPU_ID d)).
repeat vcgen.
repeat vcgen.
rewrite tintsize.
rewrite Z.add_0_l.
rewrite Z.mul_comm.
apply H3.
repeat vcgen.
repeat vcgen.
Qed.
End GetCurIDBody.
Theorem get_curid_code_correct:
spec_le (get_curid ↦ get_curid_spec_low) (〚get_curid ↦ f_get_curid 〛L).
Proof.
fbigstep_pre L.
destruct H2.
generalize hinv; intro.
destruct m´; simpl in ×.
inv hinv.
assert (0 ≤ (CPU_ID l) × 4 ≤ Int.max_unsigned).
{ rewrite max_unsigned_val; omega. }
fbigsteptest (get_curid_body_correct s (Genv.globalenv p) makeglobalenv
b0 H b2 Hb2fs Hb2fp m l
(PTree.empty _) (bind_parameter_temps´
(fn_params f_get_curid)
nil
(create_undef_temps (fn_temps f_get_curid)))) muval.
reflexivity.
intro stmt; try (destruct stmt as [le´ stmt]).
repeat fbigstep_post.
Qed.
End GETCURID.
Section SETCURID.
Let L: compatlayer (cdata RData) :=
CURID_LOC ↦ curid_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetCurIDBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches s ge).
Variables bcurid_loc : block.
Hypothesis bcurid_loc1 : Genv.find_symbol ge CURID_LOC = Some bcurid_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma set_curid_body_correct:
∀ m m´ d env le curid,
env = PTree.empty _ →
PTree.get tcurid le = Some (Vint curid) →
ikern d = true →
ihost d = true →
high_level_invariant d →
Mem.storev Mint32 ((m, d): mem) (Vptr bcurid_loc (Int.repr ((CPU_ID d × 4)))) (Vint curid) = Some (m´, d)→
∃ le´,
exec_stmt ge env le ((m, d): mem) set_curid_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros; subst.
inv H3.
unfold set_curid_body.
esplit; repeat vcgen.
unfold get_CPU_ID_spec; simpl.
rewrite H1, H2 in ×.
instantiate (1:= Int.repr (CPU_ID d)).
repeat vcgen.
rewrite tintsize.
repeat vcgen.
rewrite Z.add_0_l.
rewrite Z.mul_comm.
apply H4.
repeat vcgen.
repeat vcgen.
Qed.
End SetCurIDBody.
Theorem set_curid_code_correct:
spec_le (set_curid ↦ set_curid_spec_low) (〚set_curid ↦ f_set_curid 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct H2.
destruct m; destruct m´; simpl in ×.
generalize hinv; intro.
inv hinv.
destruct H0; subst.
fbigstep (set_curid_body_correct s (Genv.globalenv p) makeglobalenv b0 H b2 Hb2fs Hb2fp m m0 l0
(PTree.empty _) (bind_parameter_temps´
(fn_params f_set_curid)
(Vint v::nil)
(create_undef_temps (fn_temps f_set_curid)))) H.
Qed.
End SETCURID.
Section SETCURIDINIT.
Let L: compatlayer (cdata RData) := CURID_LOC ↦ curid_loc_type.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetCurIDInitBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variables bcurid_loc : block.
Hypothesis bcurid_loc1 : Genv.find_symbol ge CURID_LOC = Some bcurid_loc.
Lemma set_curid_init_body_correct:
∀ m m´ d env le i,
env = PTree.empty _ →
PTree.get tindex le = Some (Vint i) →
ikern d = true →
ihost d = true →
high_level_invariant d →
0 ≤ Int.unsigned i < TOTAL_CPU →
Mem.storev Mint32 ((m, d): mem) (Vptr bcurid_loc (Int.repr ((Int.unsigned i) × 4))) (Vint (Int.repr (Int.unsigned i + 1))) = Some (m´, d)→
∃ le´,
exec_stmt ge env le ((m, d): mem) set_curid_init_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros; subst.
unfold set_curid_init_body.
inv H3.
esplit; repeat vcgen.
rewrite tintsize.
replace (0 + 4 × Int.unsigned i) with (Int.unsigned i × 4); try omega.
simpl.
rewrite Int.unsigned_repr; try omega.
simpl in H5.
rewrite Int.unsigned_repr in H5; try omega.
repeat vcgen.
Qed.
End SetCurIDInitBody.
Theorem set_curid_init_code_correct:
spec_le (set_curid_init ↦ set_curid_init_spec_low) (〚set_curid_init ↦ f_set_curid_init 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
destruct H2.
destruct m; destruct m´; simpl in ×.
destruct H0; subst.
generalize hinv; intro hinv0.
inv hinv.
assert (0 ≤ Int.unsigned i × 4 ≤ Int.max_unsigned).
{ rewrite muval; omega. }
fbigstep (set_curid_init_body_correct (Genv.globalenv p) b0 H m m0 l0
(PTree.empty _) (bind_parameter_temps´
(fn_params f_set_curid_init)
(Vint i::nil)
(create_undef_temps
(fn_temps f_set_curid_init)))) muval.
Qed.
End SETCURIDINIT.
End WithPrimitives.
End MBOOTCODE.
Require Import Maps.
Require Import AST.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import MemoryX.
Require Import MemWithData.
Require Import EventsX.
Require Import Globalenvs.
Require Import Locations.
Require Import LAsm.
Require Import Smallstep.
Require Import ClightBigstep.
Require Import Cop.
Require Import ZArith.Zwf.
Require Import LoopProof.
Require Import VCGen.
Require Import RealParams.
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 MBootCSource.
Require Import MBoot.
Require Import CurIDGenSpec.
Require Import AbstractDataType.
Module MBOOTCODE.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
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}.
Opaque PTree.get PTree.set.
Local Open Scope Z_scope.
Section GETCURID.
Let L: compatlayer (cdata RData) :=
CURID_LOC ↦ curid_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section GetCurIDBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches s ge).
Variables bcurid_loc : block.
Hypothesis bcurid_loc1 : Genv.find_symbol ge CURID_LOC = Some bcurid_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma get_curid_body_correct:
∀ m d env le curid,
env = PTree.empty _ →
ikern d = true →
ihost d = true →
high_level_invariant d →
Mem.loadv Mint32 ((m, d): mem) (Vptr bcurid_loc (Int.repr ((CPU_ID d × 4)))) = Some (Vint curid) →
∃ le´,
exec_stmt ge env le ((m, d): mem) get_curid_body E0 le´ (m, d) (Out_return (Some (Vint curid, tint))).
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros; subst.
unfold get_curid_body.
inv H2.
esplit; repeat vcgen.
unfold get_CPU_ID_spec; simpl.
rewrite H0, H1 in ×.
instantiate (1:= Int.repr (CPU_ID d)).
repeat vcgen.
repeat vcgen.
rewrite tintsize.
rewrite Z.add_0_l.
rewrite Z.mul_comm.
apply H3.
repeat vcgen.
repeat vcgen.
Qed.
End GetCurIDBody.
Theorem get_curid_code_correct:
spec_le (get_curid ↦ get_curid_spec_low) (〚get_curid ↦ f_get_curid 〛L).
Proof.
fbigstep_pre L.
destruct H2.
generalize hinv; intro.
destruct m´; simpl in ×.
inv hinv.
assert (0 ≤ (CPU_ID l) × 4 ≤ Int.max_unsigned).
{ rewrite max_unsigned_val; omega. }
fbigsteptest (get_curid_body_correct s (Genv.globalenv p) makeglobalenv
b0 H b2 Hb2fs Hb2fp m l
(PTree.empty _) (bind_parameter_temps´
(fn_params f_get_curid)
nil
(create_undef_temps (fn_temps f_get_curid)))) muval.
reflexivity.
intro stmt; try (destruct stmt as [le´ stmt]).
repeat fbigstep_post.
Qed.
End GETCURID.
Section SETCURID.
Let L: compatlayer (cdata RData) :=
CURID_LOC ↦ curid_loc_type
⊕ get_CPU_ID ↦ gensem get_CPU_ID_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetCurIDBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES: stencil_matches s ge).
Variables bcurid_loc : block.
Hypothesis bcurid_loc1 : Genv.find_symbol ge CURID_LOC = Some bcurid_loc.
Variable bget_CPU_ID: block.
Hypothesis hget_CPU_ID1 : Genv.find_symbol ge get_CPU_ID = Some bget_CPU_ID.
Hypothesis hget_CPU_ID2 :
Genv.find_funct_ptr ge bget_CPU_ID =
Some (External (EF_external get_CPU_ID
(signature_of_type Tnil tint cc_default))
Tnil tint cc_default).
Lemma set_curid_body_correct:
∀ m m´ d env le curid,
env = PTree.empty _ →
PTree.get tcurid le = Some (Vint curid) →
ikern d = true →
ihost d = true →
high_level_invariant d →
Mem.storev Mint32 ((m, d): mem) (Vptr bcurid_loc (Int.repr ((CPU_ID d × 4)))) (Vint curid) = Some (m´, d)→
∃ le´,
exec_stmt ge env le ((m, d): mem) set_curid_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros; subst.
inv H3.
unfold set_curid_body.
esplit; repeat vcgen.
unfold get_CPU_ID_spec; simpl.
rewrite H1, H2 in ×.
instantiate (1:= Int.repr (CPU_ID d)).
repeat vcgen.
rewrite tintsize.
repeat vcgen.
rewrite Z.add_0_l.
rewrite Z.mul_comm.
apply H4.
repeat vcgen.
repeat vcgen.
Qed.
End SetCurIDBody.
Theorem set_curid_code_correct:
spec_le (set_curid ↦ set_curid_spec_low) (〚set_curid ↦ f_set_curid 〛L).
Proof.
set (L´ := L) in ×. unfold L in ×.
fbigstep_pre L´.
destruct H2.
destruct m; destruct m´; simpl in ×.
generalize hinv; intro.
inv hinv.
destruct H0; subst.
fbigstep (set_curid_body_correct s (Genv.globalenv p) makeglobalenv b0 H b2 Hb2fs Hb2fp m m0 l0
(PTree.empty _) (bind_parameter_temps´
(fn_params f_set_curid)
(Vint v::nil)
(create_undef_temps (fn_temps f_set_curid)))) H.
Qed.
End SETCURID.
Section SETCURIDINIT.
Let L: compatlayer (cdata RData) := CURID_LOC ↦ curid_loc_type.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section SetCurIDInitBody.
Context `{Hwb: WritableBlockAllowGlobals}.
Variables (ge: genv).
Variables bcurid_loc : block.
Hypothesis bcurid_loc1 : Genv.find_symbol ge CURID_LOC = Some bcurid_loc.
Lemma set_curid_init_body_correct:
∀ m m´ d env le i,
env = PTree.empty _ →
PTree.get tindex le = Some (Vint i) →
ikern d = true →
ihost d = true →
high_level_invariant d →
0 ≤ Int.unsigned i < TOTAL_CPU →
Mem.storev Mint32 ((m, d): mem) (Vptr bcurid_loc (Int.repr ((Int.unsigned i) × 4))) (Vint (Int.repr (Int.unsigned i + 1))) = Some (m´, d)→
∃ le´,
exec_stmt ge env le ((m, d): mem) set_curid_init_body E0 le´ (m´, d) Out_normal.
Proof.
generalize max_unsigned_val; intro muval.
generalize tintsize; intro tintsize.
intros; subst.
unfold set_curid_init_body.
inv H3.
esplit; repeat vcgen.
rewrite tintsize.
replace (0 + 4 × Int.unsigned i) with (Int.unsigned i × 4); try omega.
simpl.
rewrite Int.unsigned_repr; try omega.
simpl in H5.
rewrite Int.unsigned_repr in H5; try omega.
repeat vcgen.
Qed.
End SetCurIDInitBody.
Theorem set_curid_init_code_correct:
spec_le (set_curid_init ↦ set_curid_init_spec_low) (〚set_curid_init ↦ f_set_curid_init 〛L).
Proof.
set (L´ := L) in ×.
unfold L in ×.
fbigstep_pre L´.
destruct H2.
destruct m; destruct m´; simpl in ×.
destruct H0; subst.
generalize hinv; intro hinv0.
inv hinv.
assert (0 ≤ Int.unsigned i × 4 ≤ Int.max_unsigned).
{ rewrite muval; omega. }
fbigstep (set_curid_init_body_correct (Genv.globalenv p) b0 H m m0 l0
(PTree.empty _) (bind_parameter_temps´
(fn_params f_set_curid_init)
(Vint i::nil)
(create_undef_temps
(fn_temps f_set_curid_init)))) muval.
Qed.
End SETCURIDINIT.
End WithPrimitives.
End MBOOTCODE.