Library mcertikos.ticketlog.MTicketLockIntroCodeTicketLockInit
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 CommonTactic.
Require Import TacticsForTesting.
Require Import TicketLockOpGenSpec.
Require Import MTicketLockIntroCSource.
Require Import MTicketLockIntro.
Require Import CalTicketLock.
Require Import AbstractDataType.
Module MTICKETLOCKINTROTICKETLOCKINIT.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{fairness: WaitTime}.
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 TicketLOCKINIT.
Let L: compatlayer (cdata RData) := boot_loader ↦ gensem bootloader0_spec
⊕ init_ticket ↦ gensem init_ticket_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TicketLockInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bboot_loader: block.
Hypothesis hboot_loader1 : Genv.find_symbol ge boot_loader = Some bboot_loader.
Hypothesis hboot_loader2 :
Genv.find_funct_ptr ge bboot_loader =
Some (External (EF_external boot_loader
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable binit_ticket : block.
Hypothesis hinit_ticket1 : Genv.find_symbol ge init_ticket = Some binit_ticket.
Hypothesis hinit_ticket2 :
Genv.find_funct_ptr ge binit_ticket =
Some (External (EF_external init_ticket
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Section ticket_lock_init_loop_proof.
Section AuxLemmas.
Definition ticket_lock_init_mk_rdata adt index
:= adt {multi_log: real_multi_log_pb (Z.to_nat index) (multi_log adt)}.
Lemma real_multi_log_pb_exists:
∀ n (d: RData),
∃ d´, (d {multi_log : real_multi_log_pb n (multi_log d)}) = d´.
Proof.
clearAll.
induction n; intros.
∃ (d {multi_log
: real_multi_log_pb 0 (multi_log d)}); auto.
destruct IHn with d as (d´, H).
simpl.
∃
d {multi_log
: ZMap.set (Z.of_nat n) (MultiDef nil)
(multi_log d´)}.
Opaque real_multi_log_pb.
clear IHn. destruct d; destruct d´; simpl in ×.
inv H; simpl. repeat f_equal.
Transparent real_multi_log_pb.
Qed.
Lemma real_multi_log_pb_flags_same :
∀ n d d´,
ikern d = true ∧ ihost d = true ∧ init d = true →
d {multi_log: real_multi_log_pb n (multi_log d)} = d´ →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
Transparent real_multi_log_pb. clearAll.
induction n; intros.
unfold real_multi_log_pb in H0.
destruct d; destruct d´. inv H0; subst. simpl in ×. tauto.
destruct real_multi_log_pb_exists with (n := n) (d := d) as (d´´, H1).
eapply IHn with (2:= H1) in H.
simpl in H0.
clear IHn. destruct d; destruct d´; destruct d´´; simpl in ×.
inv H1; inv H0; auto.
Qed.
Lemma ticket_lock_mk_rdata_flags_same :
∀ n d d´, ikern d = true ∧ ihost d = true ∧ init d = true→
ticket_lock_init_mk_rdata d n = d´ →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
clearAll.
unfold ticket_lock_init_mk_rdata. intros.
eauto using real_multi_log_pb_flags_same.
Qed.
End AuxLemmas.
Section ticket_lock_init_fst_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iikern: ikern adt = true.
Hypothesis iihost: ihost adt = true.
Hypothesis iinit: init adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition ticket_lock_init_fst_loop_body_P (le: temp_env) (m:mem) : Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt lock_TCB_start).
Definition ticket_lock_init_fst_loop_body_Q (le: temp_env) (m: mem) : Prop :=
m = (minit, ticket_lock_init_mk_rdata adt lock_TCB_range).
Lemma ticket_lock_init_fst_loop_correct_aux :
LoopProofSimpleWhile.t f_ticket_lock_init_fst_while_condition
f_ticket_lock_init_fst_while_body
ge (PTree.empty _)
(ticket_lock_init_fst_loop_body_P)
(ticket_lock_init_fst_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
assert (lock_TCB_start_val0: lock_TCB_start = 1) by (unfold lock_TCB_start; reflexivity).
assert (ID_AT_range0: ID_AT_range = 1) by eauto.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (ID_TCB_range0: ID_TCB_range = num_chan) by (unfold ID_TCB_range; simpl; omega).
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ ID_TCB_range ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt (lock_TCB_start + (Int.unsigned i))) ∧
w = ID_TCB_range - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold ticket_lock_init_fst_loop_body_P in H.
destruct H as [_ile tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
subst.
esplit. esplit.
change (Int.zero) with (Int.repr 0) in _ile.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [_ile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
destruct tmpH as [mval H]; subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct hinv.
Caseeq ihigh; intros.
+
unfold f_ticket_lock_init_fst_while_body.
esplit. esplit.
repeat vcgen.
esplit. esplit.
Opaque Z.add Z.mul.
repeat vcgen.
{ unfold init_ticket_spec.
remember (ticket_lock_init_mk_rdata adt (lock_TCB_start + Int.unsigned i)) as r.
assert (ikern r= true ∧ ihost r = true ∧ init r = true)
by eauto using ticket_lock_mk_rdata_flags_same.
destruct H1 as (H1a, (H1b, H1c)).
rewrite H1a, H1b.
assert (index2Z 1 (Int.unsigned i) = Some (1 + (Int.unsigned i))).
{ clearAllExceptTwo ilow H. unfold index2Z; simpl.
destruct (zle_lt 0 (Int.unsigned i) ID_TCB_range); [ | try omega].
unfold ID_AT_range. reflexivity. }
rewrite H1. subst.
reflexivity. }
esplit.
repeat vcgen.
instantiate (1:= num_chan - (Int.unsigned i) - 1).
omega.
esplit; repeat vcgen.
unfold lock_TCB_start, ID_AT_range.
simpl.
f_equal.
unfold ticket_lock_init_mk_rdata.
assert(tmpeq´: 1 + (Int.unsigned i + 1) = 1 + Int.unsigned i + 1) by omega;
rewrite tmpeq´; clear tmpeq´.
change (1 + Int.unsigned i + 1) with (Z.succ (1 + Int.unsigned i)).
rewrite Z2Nat.inj_succ with (n:=(1 + Int.unsigned i)) in *; [ | omega].
simpl.
remember (1 + Int.unsigned i) as index.
assert (index ≥ 0) by omega.
destruct real_multi_log_pb_exists with (n:= (Z.to_nat index))
(d := adt) as (d´, H2).
rewrite H2.
inv H2.
rewrite Z2Nat.id; repeat vcgen.
+
unfold ticket_lock_init_fst_loop_body_Q.
esplit; esplit; repeat vcgen.
unfold lock_TCB_range. unfold ID_AT_range.
rewrite H. reflexivity.
Qed.
End ticket_lock_init_fst_loop_proof.
Lemma ticket_lock_init_fst_loop_correct:
∀ m d d´ d´´ le,
PTree.get _i le = Some (Vint (Int.repr 0)) →
ihost d = true →
ikern d = true →
init d = true →
high_level_invariant d →
d´ = ticket_lock_init_mk_rdata d ID_AT_range →
d´´ = ticket_lock_init_mk_rdata d lock_TCB_range →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d´): mem)
(Swhile f_ticket_lock_init_fst_while_condition
f_ticket_lock_init_fst_while_body) E0 le´ (m, d´´) Out_normal.
Proof.
intros m d d´ d´´ le tile iihost iikern iinit hinv m´val m´´val.
generalize (ticket_lock_init_fst_loop_correct_aux m d hinv).
unfold ticket_lock_init_fst_loop_body_P.
unfold ticket_lock_init_fst_loop_body_Q.
intros LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d´) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp lm_val].
∃ le´´; repeat vcgen.
destruct m´´. inv lm_val.
assert (lock_TCB_start_val0: lock_TCB_start = 1) by (unfold lock_TCB_start; reflexivity).
assert (ID_AT_range0: ID_AT_range = 1) by eauto.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (ID_TCB_range0: ID_TCB_range = num_chan) by (unfold ID_TCB_range; simpl; omega).
unfold f_ticket_lock_init_fst_while_condition, f_ticket_lock_init_fst_while_body in *;
repeat vcgen.
simpl.
repeat vcgen.
rewrite m´val. auto.
Qed.
Section ticket_lock_init_snd_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iikern: ikern adt = true.
Hypothesis iihost: ihost adt = true.
Hypothesis iinit: init adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition ticket_lock_init_snd_loop_body_P (le: temp_env) (m:mem) : Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt lock_SC_start).
Definition ticket_lock_init_snd_loop_body_Q (le: temp_env) (m: mem) : Prop :=
m = (minit, ticket_lock_init_mk_rdata adt lock_range).
Lemma ticket_lock_init_snd_loop_correct_aux :
LoopProofSimpleWhile.t f_ticket_lock_init_snd_while_condition
f_ticket_lock_init_snd_while_body
ge (PTree.empty _)
(ticket_lock_init_snd_loop_body_P)
(ticket_lock_init_snd_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
assert (lock_ST_start_val0: lock_SC_start = num_chan + 1) by (unfold lock_SC_start; unfold lock_TCB_range; reflexivity).
unfold lock_TCB_range. simpl.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (lock_range0: lock_range = num_chan + num_chan + 1) by (unfold lock_range; simpl; omega).
assert (ID_SC_range0: ID_SC_range = num_chan) by (unfold ID_SC_range; simpl; omega).
assert (num_chan_val0: num_chan = num_chan) by reflexivity.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ ID_SC_range ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt (lock_SC_start + (Int.unsigned i))) ∧
w = ID_SC_range - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold ticket_lock_init_snd_loop_body_P in H.
destruct H as [_ile tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
subst.
esplit. esplit.
change (Int.zero) with (Int.repr 0) in _ile.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [_ile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
destruct tmpH as [mval H]; subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct hinv.
Caseeq ihigh; intros.
+
unfold f_ticket_lock_init_snd_while_body.
esplit. esplit.
Opaque Z.add Z.mul.
repeat vcgen.
esplit. esplit.
repeat vcgen.
{
unfold init_ticket_spec.
remember (ticket_lock_init_mk_rdata adt (lock_SC_start + Int.unsigned i)) as r.
assert (ikern r= true ∧ ihost r = true ∧ init r = true)
by eauto using ticket_lock_mk_rdata_flags_same.
destruct H1 as (H1a, (H1b, H1c)).
rewrite H1a, H1b.
assert (index2Z 2 (Int.unsigned i) = Some (num_chan + 1 + (Int.unsigned i))).
{
clearAllExceptTwo ilow H. unfold index2Z; simpl.
destruct (zle_lt 0 (Int.unsigned i) ID_SC_range); [ | try omega].
unfold lock_SC_start. unfold lock_TCB_range.
reflexivity.
}
subst; vcgen.
}
esplit.
repeat vcgen.
instantiate (1:= num_chan - (Int.unsigned i) - 1).
omega.
esplit; repeat vcgen.
unfold lock_SC_start. unfold lock_TCB_range.
unfold ID_AT_range, ID_TCB_range.
simpl.
f_equal.
unfold ticket_lock_init_mk_rdata.
assert(tmpeq: 1 + num_chan + Int.unsigned i = num_chan + 1 + Int.unsigned i) by omega;
rewrite tmpeq; clear tmpeq.
assert(tmpeq´: 1 + num_chan + (Int.unsigned i + 1) = num_chan + 1 + Int.unsigned i + 1) by omega;
rewrite tmpeq´; clear tmpeq´.
change (num_chan + 1 + Int.unsigned i + 1) with (Z.succ (num_chan + 1 + Int.unsigned i)).
rewrite Z2Nat.inj_succ with (n:=(num_chan + 1 + Int.unsigned i)) in *; [ | omega].
simpl.
remember (num_chan + 1 + Int.unsigned i) as index.
assert (index ≥ 0) by omega.
destruct real_multi_log_pb_exists with (n:= (Z.to_nat index))
(d := adt) as (d´, H3).
rewrite H3.
inv H3.
rewrite Z2Nat.id; repeat vcgen.
+
unfold ticket_lock_init_snd_loop_body_Q.
esplit. esplit.
repeat vcgen.
simpl.
rewrite H.
unfold lock_range; auto.
Qed.
End ticket_lock_init_snd_loop_proof.
Lemma ticket_lock_init_snd_loop_correct:
∀ m d d´ d´´ le,
PTree.get _i le = Some (Vint (Int.repr 0)) →
ihost d = true →
ikern d = true →
init d = true →
high_level_invariant d →
d´ = ticket_lock_init_mk_rdata d lock_TCB_range →
d´´ = ticket_lock_init_mk_rdata d lock_range →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d´): mem)
(Swhile f_ticket_lock_init_snd_while_condition
f_ticket_lock_init_snd_while_body) E0 le´ (m, d´´) Out_normal.
Proof.
intros m d d´ d´´ le tile iihost iikern iinit hinv m´val m´´val.
generalize (ticket_lock_init_snd_loop_correct_aux m d hinv).
unfold ticket_lock_init_snd_loop_body_P.
unfold ticket_lock_init_snd_loop_body_Q.
intros LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d´) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp lm_val].
∃ le´´; repeat vcgen.
destruct m´´. inv lm_val.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (lock_range0: lock_range = num_chan + num_chan + 1) by (unfold lock_range; simpl; omega).
assert (ID_TCB_range0: ID_SC_range = num_chan) by (unfold ID_SC_range; simpl; omega).
unfold f_ticket_lock_init_snd_while_condition, f_ticket_lock_init_snd_while_body in *;
repeat vcgen.
simpl.
repeat vcgen.
rewrite m´val.
auto.
Qed.
End ticket_lock_init_loop_proof.
Lemma ticket_lock_init_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get _mbi_addr le = Some (Vint mbi_adr) →
PTree.get _i le = Some Vundef →
ticket_lock_init_spec (Int.unsigned mbi_adr) d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_ticket_lock_init_body E0
le´ (m, d´) Out_normal.
Proof.
assert (ID_AT_range0: ID_AT_range = 1) by auto.
assert (ID_TCB_range0: ID_TCB_range = num_chan) by auto.
assert (ID_SC_range0: ID_SC_range = num_chan) by auto.
assert (lock_TCB_start0: lock_TCB_start = 1) by (unfold lock_TCB_start; reflexivity).
assert (lock_SC_start0: lock_SC_start = num_chan + 1) by (unfold lock_SC_start; unfold lock_TCB_range; reflexivity).
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (lock_range0: lock_range = num_chan + num_chan + 1) by (unfold lock_range; simpl; omega).
generalize max_unsigned_val; intro muval.
intros.
subst.
functional inversion H2.
subst.
simpl in ×.
unfold f_ticket_lock_init_body.
unfold init_ticket_spec in ×.
set (di := (((((((d { ioapic / s
: ObjInterruptDriver.ioapic_init_aux
(DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1))}) {
lapic
: DeviceStateDataType.update_l3
(DeviceStateDataType.update_l2
(DeviceStateDataType.update_l1
(DeviceStateDataType.mkLApicData
{|
DeviceStateDataType.LapicEsr := 0;
DeviceStateDataType.LapicEoi := DeviceStateDataType.NoIntr;
DeviceStateDataType.LapicMaxLvt := DeviceStateDataType.LapicMaxLvt
(DeviceStateDataType.s
(lapic d));
DeviceStateDataType.LapicEnable := true;
DeviceStateDataType.LapicSpurious := 39;
DeviceStateDataType.LapicLint0Mask := true;
DeviceStateDataType.LapicLint1Mask := true;
DeviceStateDataType.LapicPcIntMask := true;
DeviceStateDataType.LapicLdr := 0;
DeviceStateDataType.LapicErrorIrq := 50;
DeviceStateDataType.LapicEsrClrPen := false;
DeviceStateDataType.LapicTpr := 0 |})
(DeviceStateDataType.l1 (lapic d)))
(DeviceStateDataType.l2 (lapic d)))
(DeviceStateDataType.l3 (lapic d))}) { ioapic
: DeviceStateDataType.update_s
(DeviceStateDataType.update_s (ioapic d)
(ObjInterruptDriver.ioapic_init_aux
(DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1))))
(DeviceStateDataType.update_CurrentIrq
(ObjInterruptDriver.ioapic_init_aux
(DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1)))
None)}) {MM : real_mm}) {MMSize : real_size})
{vmxinfo : real_vmxinfo}) {init : true})).
fold di in H2.
assert (di_flag: init di = true ∧ ihost di = true ∧ ikern di = true ∧ pg di = false).
{ unfold di; simpl; tauto. }
assert (di_hlinv: high_level_invariant di).
{ unfold di in H2; simpl in ×.
unfold di.
econstructor; inv H3; destruct d; destruct di; simpl in *; eauto. }
destruct di_flag as (di_f1 & di_f2 & di_f3 & di_f4).
Opaque Z.add Z.sub Z.mul Z.div.
exploit (ticket_lock_init_fst_loop_correct m di
(ticket_lock_init_mk_rdata di lock_TCB_start)
(ticket_lock_init_mk_rdata di lock_TCB_range)
(PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef (set_opttemp None Vundef le)))).
repeat vcgen.
assumption.
assumption.
assumption.
assumption.
reflexivity.
reflexivity.
intros H; destruct H as (le´, H).
exploit (ticket_lock_init_snd_loop_correct m di
(ticket_lock_init_mk_rdata di lock_SC_start)
(ticket_lock_init_mk_rdata di lock_range)
(PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef (set_opttemp None Vundef le´)))).
repeat vcgen.
assumption.
assumption.
assumption.
assumption.
reflexivity.
reflexivity.
intros H11.
unfold ticket_lock_init_mk_rdata in H, H11.
unfold real_multi_log.
destruct H11 as (le´´, H11).
∃ le´´.
change E0 with (E0 ** E0).
econstructor.
vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold bootloader0_spec.
rewrite H4, H5, H6, H7, H8, H9, H10.
instantiate (1:= di).
unfold di; repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
fold di.
repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
exact H.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
unfold lock_SC_start in H11.
exact H11.
Opaque Z.add Z.sub Z.mul Z.div.
Opaque CalTicketLock.
Qed.
End TicketLockInitBody.
Theorem ticket_lock_init_code_correct:
spec_le (ticket_lock_init ↦ ticket_lock_init_spec_low)
(〚ticket_lock_init ↦ f_ticket_lock_init 〛L).
Proof.
fbigstep_pre L.
fbigstep (ticket_lock_init_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_ticket_lock_init) (Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_ticket_lock_init))))
muval.
Qed.
End TicketLOCKINIT.
End WithPrimitives.
End MTICKETLOCKINTROTICKETLOCKINIT.
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 CommonTactic.
Require Import TacticsForTesting.
Require Import TicketLockOpGenSpec.
Require Import MTicketLockIntroCSource.
Require Import MTicketLockIntro.
Require Import CalTicketLock.
Require Import AbstractDataType.
Module MTICKETLOCKINTROTICKETLOCKINIT.
Section WithPrimitives.
Context `{real_params: RealParams}.
Context `{oracle_prop: MultiOracleProp}.
Context {memb} `{Hmemx: Mem.MemoryModelX memb}.
Context `{Hmwd: UseMemWithData memb}.
Context `{fairness: WaitTime}.
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 TicketLOCKINIT.
Let L: compatlayer (cdata RData) := boot_loader ↦ gensem bootloader0_spec
⊕ init_ticket ↦ gensem init_ticket_spec.
Local Instance: ExternalCallsOps mem :=
CompatExternalCalls.compatlayer_extcall_ops L.
Local Instance: CompilerConfigOps mem :=
CompatExternalCalls.compatlayer_compiler_config_ops L.
Section TicketLockInitBody.
Context `{Hwb: WritableBlockOps}.
Variable (s: stencil).
Variables (ge: genv)
(STENCIL_MATCHES : stencil_matches s ge).
Variable bboot_loader: block.
Hypothesis hboot_loader1 : Genv.find_symbol ge boot_loader = Some bboot_loader.
Hypothesis hboot_loader2 :
Genv.find_funct_ptr ge bboot_loader =
Some (External (EF_external boot_loader
(signature_of_type (Tcons tint Tnil) tvoid cc_default))
(Tcons tint Tnil) tvoid cc_default).
Variable binit_ticket : block.
Hypothesis hinit_ticket1 : Genv.find_symbol ge init_ticket = Some binit_ticket.
Hypothesis hinit_ticket2 :
Genv.find_funct_ptr ge binit_ticket =
Some (External (EF_external init_ticket
(signature_of_type (Tcons tint (Tcons tint Tnil)) tvoid cc_default))
(Tcons tint (Tcons tint Tnil)) tvoid cc_default).
Section ticket_lock_init_loop_proof.
Section AuxLemmas.
Definition ticket_lock_init_mk_rdata adt index
:= adt {multi_log: real_multi_log_pb (Z.to_nat index) (multi_log adt)}.
Lemma real_multi_log_pb_exists:
∀ n (d: RData),
∃ d´, (d {multi_log : real_multi_log_pb n (multi_log d)}) = d´.
Proof.
clearAll.
induction n; intros.
∃ (d {multi_log
: real_multi_log_pb 0 (multi_log d)}); auto.
destruct IHn with d as (d´, H).
simpl.
∃
d {multi_log
: ZMap.set (Z.of_nat n) (MultiDef nil)
(multi_log d´)}.
Opaque real_multi_log_pb.
clear IHn. destruct d; destruct d´; simpl in ×.
inv H; simpl. repeat f_equal.
Transparent real_multi_log_pb.
Qed.
Lemma real_multi_log_pb_flags_same :
∀ n d d´,
ikern d = true ∧ ihost d = true ∧ init d = true →
d {multi_log: real_multi_log_pb n (multi_log d)} = d´ →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
Transparent real_multi_log_pb. clearAll.
induction n; intros.
unfold real_multi_log_pb in H0.
destruct d; destruct d´. inv H0; subst. simpl in ×. tauto.
destruct real_multi_log_pb_exists with (n := n) (d := d) as (d´´, H1).
eapply IHn with (2:= H1) in H.
simpl in H0.
clear IHn. destruct d; destruct d´; destruct d´´; simpl in ×.
inv H1; inv H0; auto.
Qed.
Lemma ticket_lock_mk_rdata_flags_same :
∀ n d d´, ikern d = true ∧ ihost d = true ∧ init d = true→
ticket_lock_init_mk_rdata d n = d´ →
ikern d´ = true ∧ ihost d´ = true ∧ init d´ = true.
Proof.
clearAll.
unfold ticket_lock_init_mk_rdata. intros.
eauto using real_multi_log_pb_flags_same.
Qed.
End AuxLemmas.
Section ticket_lock_init_fst_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iikern: ikern adt = true.
Hypothesis iihost: ihost adt = true.
Hypothesis iinit: init adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition ticket_lock_init_fst_loop_body_P (le: temp_env) (m:mem) : Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt lock_TCB_start).
Definition ticket_lock_init_fst_loop_body_Q (le: temp_env) (m: mem) : Prop :=
m = (minit, ticket_lock_init_mk_rdata adt lock_TCB_range).
Lemma ticket_lock_init_fst_loop_correct_aux :
LoopProofSimpleWhile.t f_ticket_lock_init_fst_while_condition
f_ticket_lock_init_fst_while_body
ge (PTree.empty _)
(ticket_lock_init_fst_loop_body_P)
(ticket_lock_init_fst_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
assert (lock_TCB_start_val0: lock_TCB_start = 1) by (unfold lock_TCB_start; reflexivity).
assert (ID_AT_range0: ID_AT_range = 1) by eauto.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (ID_TCB_range0: ID_TCB_range = num_chan) by (unfold ID_TCB_range; simpl; omega).
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ ID_TCB_range ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt (lock_TCB_start + (Int.unsigned i))) ∧
w = ID_TCB_range - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold ticket_lock_init_fst_loop_body_P in H.
destruct H as [_ile tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
subst.
esplit. esplit.
change (Int.zero) with (Int.repr 0) in _ile.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [_ile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
destruct tmpH as [mval H]; subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct hinv.
Caseeq ihigh; intros.
+
unfold f_ticket_lock_init_fst_while_body.
esplit. esplit.
repeat vcgen.
esplit. esplit.
Opaque Z.add Z.mul.
repeat vcgen.
{ unfold init_ticket_spec.
remember (ticket_lock_init_mk_rdata adt (lock_TCB_start + Int.unsigned i)) as r.
assert (ikern r= true ∧ ihost r = true ∧ init r = true)
by eauto using ticket_lock_mk_rdata_flags_same.
destruct H1 as (H1a, (H1b, H1c)).
rewrite H1a, H1b.
assert (index2Z 1 (Int.unsigned i) = Some (1 + (Int.unsigned i))).
{ clearAllExceptTwo ilow H. unfold index2Z; simpl.
destruct (zle_lt 0 (Int.unsigned i) ID_TCB_range); [ | try omega].
unfold ID_AT_range. reflexivity. }
rewrite H1. subst.
reflexivity. }
esplit.
repeat vcgen.
instantiate (1:= num_chan - (Int.unsigned i) - 1).
omega.
esplit; repeat vcgen.
unfold lock_TCB_start, ID_AT_range.
simpl.
f_equal.
unfold ticket_lock_init_mk_rdata.
assert(tmpeq´: 1 + (Int.unsigned i + 1) = 1 + Int.unsigned i + 1) by omega;
rewrite tmpeq´; clear tmpeq´.
change (1 + Int.unsigned i + 1) with (Z.succ (1 + Int.unsigned i)).
rewrite Z2Nat.inj_succ with (n:=(1 + Int.unsigned i)) in *; [ | omega].
simpl.
remember (1 + Int.unsigned i) as index.
assert (index ≥ 0) by omega.
destruct real_multi_log_pb_exists with (n:= (Z.to_nat index))
(d := adt) as (d´, H2).
rewrite H2.
inv H2.
rewrite Z2Nat.id; repeat vcgen.
+
unfold ticket_lock_init_fst_loop_body_Q.
esplit; esplit; repeat vcgen.
unfold lock_TCB_range. unfold ID_AT_range.
rewrite H. reflexivity.
Qed.
End ticket_lock_init_fst_loop_proof.
Lemma ticket_lock_init_fst_loop_correct:
∀ m d d´ d´´ le,
PTree.get _i le = Some (Vint (Int.repr 0)) →
ihost d = true →
ikern d = true →
init d = true →
high_level_invariant d →
d´ = ticket_lock_init_mk_rdata d ID_AT_range →
d´´ = ticket_lock_init_mk_rdata d lock_TCB_range →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d´): mem)
(Swhile f_ticket_lock_init_fst_while_condition
f_ticket_lock_init_fst_while_body) E0 le´ (m, d´´) Out_normal.
Proof.
intros m d d´ d´´ le tile iihost iikern iinit hinv m´val m´´val.
generalize (ticket_lock_init_fst_loop_correct_aux m d hinv).
unfold ticket_lock_init_fst_loop_body_P.
unfold ticket_lock_init_fst_loop_body_Q.
intros LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d´) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp lm_val].
∃ le´´; repeat vcgen.
destruct m´´. inv lm_val.
assert (lock_TCB_start_val0: lock_TCB_start = 1) by (unfold lock_TCB_start; reflexivity).
assert (ID_AT_range0: ID_AT_range = 1) by eauto.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (ID_TCB_range0: ID_TCB_range = num_chan) by (unfold ID_TCB_range; simpl; omega).
unfold f_ticket_lock_init_fst_while_condition, f_ticket_lock_init_fst_while_body in *;
repeat vcgen.
simpl.
repeat vcgen.
rewrite m´val. auto.
Qed.
Section ticket_lock_init_snd_loop_proof.
Variable minit: memb.
Variable adt: RData.
Hypothesis iikern: ikern adt = true.
Hypothesis iihost: ihost adt = true.
Hypothesis iinit: init adt = true.
Hypothesis hinv: high_level_invariant adt.
Definition ticket_lock_init_snd_loop_body_P (le: temp_env) (m:mem) : Prop :=
PTree.get _i le = Some (Vint Int.zero) ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt lock_SC_start).
Definition ticket_lock_init_snd_loop_body_Q (le: temp_env) (m: mem) : Prop :=
m = (minit, ticket_lock_init_mk_rdata adt lock_range).
Lemma ticket_lock_init_snd_loop_correct_aux :
LoopProofSimpleWhile.t f_ticket_lock_init_snd_while_condition
f_ticket_lock_init_snd_while_body
ge (PTree.empty _)
(ticket_lock_init_snd_loop_body_P)
(ticket_lock_init_snd_loop_body_Q).
Proof.
generalize max_unsigned_val; intro muval.
assert (lock_ST_start_val0: lock_SC_start = num_chan + 1) by (unfold lock_SC_start; unfold lock_TCB_range; reflexivity).
unfold lock_TCB_range. simpl.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (lock_range0: lock_range = num_chan + num_chan + 1) by (unfold lock_range; simpl; omega).
assert (ID_SC_range0: ID_SC_range = num_chan) by (unfold ID_SC_range; simpl; omega).
assert (num_chan_val0: num_chan = num_chan) by reflexivity.
apply LoopProofSimpleWhile.make with
(W := Z)
(lt := fun z1 z2 ⇒ (0 ≤ z2 ∧ z1 < z2)%Z)
(I := fun le m w ⇒ ∃ i,
PTree.get _i le = Some (Vint i) ∧
0 ≤ Int.unsigned i ≤ ID_SC_range ∧
ikern adt = true ∧
ihost adt = true ∧
init adt = true ∧
m = (minit, ticket_lock_init_mk_rdata adt (lock_SC_start + (Int.unsigned i))) ∧
w = ID_SC_range - Int.unsigned i
).
- apply Zwf_well_founded.
- intros.
unfold ticket_lock_init_snd_loop_body_P in H.
destruct H as [_ile tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
subst.
esplit. esplit.
change (Int.zero) with (Int.repr 0) in _ile.
repeat vcgen.
- intros.
destruct H as [i tmpH].
destruct tmpH as [_ile tmpH].
destruct tmpH as [irange tmpH].
destruct tmpH as [iikern´ tmpH].
destruct tmpH as [iihost´ tmpH].
destruct tmpH as [iinit´ tmpH].
destruct tmpH as [mval H]; subst.
destruct irange as [ilow ihigh].
apply Zle_lt_or_eq in ihigh.
destruct hinv.
Caseeq ihigh; intros.
+
unfold f_ticket_lock_init_snd_while_body.
esplit. esplit.
Opaque Z.add Z.mul.
repeat vcgen.
esplit. esplit.
repeat vcgen.
{
unfold init_ticket_spec.
remember (ticket_lock_init_mk_rdata adt (lock_SC_start + Int.unsigned i)) as r.
assert (ikern r= true ∧ ihost r = true ∧ init r = true)
by eauto using ticket_lock_mk_rdata_flags_same.
destruct H1 as (H1a, (H1b, H1c)).
rewrite H1a, H1b.
assert (index2Z 2 (Int.unsigned i) = Some (num_chan + 1 + (Int.unsigned i))).
{
clearAllExceptTwo ilow H. unfold index2Z; simpl.
destruct (zle_lt 0 (Int.unsigned i) ID_SC_range); [ | try omega].
unfold lock_SC_start. unfold lock_TCB_range.
reflexivity.
}
subst; vcgen.
}
esplit.
repeat vcgen.
instantiate (1:= num_chan - (Int.unsigned i) - 1).
omega.
esplit; repeat vcgen.
unfold lock_SC_start. unfold lock_TCB_range.
unfold ID_AT_range, ID_TCB_range.
simpl.
f_equal.
unfold ticket_lock_init_mk_rdata.
assert(tmpeq: 1 + num_chan + Int.unsigned i = num_chan + 1 + Int.unsigned i) by omega;
rewrite tmpeq; clear tmpeq.
assert(tmpeq´: 1 + num_chan + (Int.unsigned i + 1) = num_chan + 1 + Int.unsigned i + 1) by omega;
rewrite tmpeq´; clear tmpeq´.
change (num_chan + 1 + Int.unsigned i + 1) with (Z.succ (num_chan + 1 + Int.unsigned i)).
rewrite Z2Nat.inj_succ with (n:=(num_chan + 1 + Int.unsigned i)) in *; [ | omega].
simpl.
remember (num_chan + 1 + Int.unsigned i) as index.
assert (index ≥ 0) by omega.
destruct real_multi_log_pb_exists with (n:= (Z.to_nat index))
(d := adt) as (d´, H3).
rewrite H3.
inv H3.
rewrite Z2Nat.id; repeat vcgen.
+
unfold ticket_lock_init_snd_loop_body_Q.
esplit. esplit.
repeat vcgen.
simpl.
rewrite H.
unfold lock_range; auto.
Qed.
End ticket_lock_init_snd_loop_proof.
Lemma ticket_lock_init_snd_loop_correct:
∀ m d d´ d´´ le,
PTree.get _i le = Some (Vint (Int.repr 0)) →
ihost d = true →
ikern d = true →
init d = true →
high_level_invariant d →
d´ = ticket_lock_init_mk_rdata d lock_TCB_range →
d´´ = ticket_lock_init_mk_rdata d lock_range →
∃ le´,
exec_stmt ge (PTree.empty _) le ((m, d´): mem)
(Swhile f_ticket_lock_init_snd_while_condition
f_ticket_lock_init_snd_while_body) E0 le´ (m, d´´) Out_normal.
Proof.
intros m d d´ d´´ le tile iihost iikern iinit hinv m´val m´´val.
generalize (ticket_lock_init_snd_loop_correct_aux m d hinv).
unfold ticket_lock_init_snd_loop_body_P.
unfold ticket_lock_init_snd_loop_body_Q.
intros LP.
refine (_ (LoopProofSimpleWhile.termination _ _ _ _ _ _ LP le (m, d´) _)).
intro pre.
destruct pre as [le´´ tmppre].
destruct tmppre as [m´´ tmppre].
destruct tmppre as [stmp lm_val].
∃ le´´; repeat vcgen.
destruct m´´. inv lm_val.
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (lock_range0: lock_range = num_chan + num_chan + 1) by (unfold lock_range; simpl; omega).
assert (ID_TCB_range0: ID_SC_range = num_chan) by (unfold ID_SC_range; simpl; omega).
unfold f_ticket_lock_init_snd_while_condition, f_ticket_lock_init_snd_while_body in *;
repeat vcgen.
simpl.
repeat vcgen.
rewrite m´val.
auto.
Qed.
End ticket_lock_init_loop_proof.
Lemma ticket_lock_init_body_correct: ∀ m d d´ env le mbi_adr,
env = PTree.empty _ →
PTree.get _mbi_addr le = Some (Vint mbi_adr) →
PTree.get _i le = Some Vundef →
ticket_lock_init_spec (Int.unsigned mbi_adr) d = Some d´ →
high_level_invariant d →
∃ le´,
exec_stmt ge env le ((m, d): mem) f_ticket_lock_init_body E0
le´ (m, d´) Out_normal.
Proof.
assert (ID_AT_range0: ID_AT_range = 1) by auto.
assert (ID_TCB_range0: ID_TCB_range = num_chan) by auto.
assert (ID_SC_range0: ID_SC_range = num_chan) by auto.
assert (lock_TCB_start0: lock_TCB_start = 1) by (unfold lock_TCB_start; reflexivity).
assert (lock_SC_start0: lock_SC_start = num_chan + 1) by (unfold lock_SC_start; unfold lock_TCB_range; reflexivity).
assert (lock_TCB_range0: lock_TCB_range = num_chan + 1) by (unfold lock_TCB_range; simpl; omega).
assert (lock_range0: lock_range = num_chan + num_chan + 1) by (unfold lock_range; simpl; omega).
generalize max_unsigned_val; intro muval.
intros.
subst.
functional inversion H2.
subst.
simpl in ×.
unfold f_ticket_lock_init_body.
unfold init_ticket_spec in ×.
set (di := (((((((d { ioapic / s
: ObjInterruptDriver.ioapic_init_aux
(DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1))}) {
lapic
: DeviceStateDataType.update_l3
(DeviceStateDataType.update_l2
(DeviceStateDataType.update_l1
(DeviceStateDataType.mkLApicData
{|
DeviceStateDataType.LapicEsr := 0;
DeviceStateDataType.LapicEoi := DeviceStateDataType.NoIntr;
DeviceStateDataType.LapicMaxLvt := DeviceStateDataType.LapicMaxLvt
(DeviceStateDataType.s
(lapic d));
DeviceStateDataType.LapicEnable := true;
DeviceStateDataType.LapicSpurious := 39;
DeviceStateDataType.LapicLint0Mask := true;
DeviceStateDataType.LapicLint1Mask := true;
DeviceStateDataType.LapicPcIntMask := true;
DeviceStateDataType.LapicLdr := 0;
DeviceStateDataType.LapicErrorIrq := 50;
DeviceStateDataType.LapicEsrClrPen := false;
DeviceStateDataType.LapicTpr := 0 |})
(DeviceStateDataType.l1 (lapic d)))
(DeviceStateDataType.l2 (lapic d)))
(DeviceStateDataType.l3 (lapic d))}) { ioapic
: DeviceStateDataType.update_s
(DeviceStateDataType.update_s (ioapic d)
(ObjInterruptDriver.ioapic_init_aux
(DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1))))
(DeviceStateDataType.update_CurrentIrq
(ObjInterruptDriver.ioapic_init_aux
(DeviceStateDataType.s (ioapic d))
(Z.to_nat
(DeviceStateDataType.IoApicMaxIntr
(DeviceStateDataType.s (ioapic d)) + 1 - 1)))
None)}) {MM : real_mm}) {MMSize : real_size})
{vmxinfo : real_vmxinfo}) {init : true})).
fold di in H2.
assert (di_flag: init di = true ∧ ihost di = true ∧ ikern di = true ∧ pg di = false).
{ unfold di; simpl; tauto. }
assert (di_hlinv: high_level_invariant di).
{ unfold di in H2; simpl in ×.
unfold di.
econstructor; inv H3; destruct d; destruct di; simpl in *; eauto. }
destruct di_flag as (di_f1 & di_f2 & di_f3 & di_f4).
Opaque Z.add Z.sub Z.mul Z.div.
exploit (ticket_lock_init_fst_loop_correct m di
(ticket_lock_init_mk_rdata di lock_TCB_start)
(ticket_lock_init_mk_rdata di lock_TCB_range)
(PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef (set_opttemp None Vundef le)))).
repeat vcgen.
assumption.
assumption.
assumption.
assumption.
reflexivity.
reflexivity.
intros H; destruct H as (le´, H).
exploit (ticket_lock_init_snd_loop_correct m di
(ticket_lock_init_mk_rdata di lock_SC_start)
(ticket_lock_init_mk_rdata di lock_range)
(PTree.set _i (Vint (Int.repr 0))
(set_opttemp None Vundef (set_opttemp None Vundef le´)))).
repeat vcgen.
assumption.
assumption.
assumption.
assumption.
reflexivity.
reflexivity.
intros H11.
unfold ticket_lock_init_mk_rdata in H, H11.
unfold real_multi_log.
destruct H11 as (le´´, H11).
∃ le´´.
change E0 with (E0 ** E0).
econstructor.
vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
repeat vcgen.
unfold bootloader0_spec.
rewrite H4, H5, H6, H7, H8, H9, H10.
instantiate (1:= di).
unfold di; repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
fold di.
repeat vcgen.
change E0 with (E0 ** E0).
econstructor.
exact H.
change E0 with (E0 ** E0).
econstructor.
repeat vcgen.
unfold lock_SC_start in H11.
exact H11.
Opaque Z.add Z.sub Z.mul Z.div.
Opaque CalTicketLock.
Qed.
End TicketLockInitBody.
Theorem ticket_lock_init_code_correct:
spec_le (ticket_lock_init ↦ ticket_lock_init_spec_low)
(〚ticket_lock_init ↦ f_ticket_lock_init 〛L).
Proof.
fbigstep_pre L.
fbigstep (ticket_lock_init_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_ticket_lock_init) (Vint mbi_adr::nil)
(create_undef_temps (fn_temps f_ticket_lock_init))))
muval.
Qed.
End TicketLOCKINIT.
End WithPrimitives.
End MTICKETLOCKINTROTICKETLOCKINIT.