Library mcertikos.ticketlog.TicketLockIntroGenPassthrough
This file provide the contextual refinement proof between MBoot layer and MALInit layer
Section Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma IntUnsignedRange: ∀ i,
0 ≤ Int.unsigned i ≤ Int.max_unsigned.
Proof.
intros.
generalize (Int.unsigned_range i).
generalize max_unsigned_val; intro muval.
unfold Int.modulus, two_power_nat, shift_nat; simpl.
intro.
omega.
Qed.
Lemma CalTicketLockWraparoundRange: ∀ l l´ t n,
CalTicketLockWraparound l = Some (t, n, l´) →
(0 ≤ t ≤ Int.max_unsigned ∧
0 ≤ n ≤ Int.max_unsigned).
Proof.
generalize max_unsigned_val; intro muval.
intros.
destruct l.
simpl in H.
inv H.
split; omega.
simpl in H;
subdestruct; inv H; simpl in *;
split; eapply IntUnsignedRange.
Qed.
Lemma release_shared0_match:
∀ s i ofs e d d´ m f,
release_shared0_spec0 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared0_spec; intros. subdestruct.
inv H. inv H0; constructor; simpl.
inv Hlog. econstructor; eauto.
intros.
destruct (zeq z z0); subst.
- rewrite ZMap.gss.
specialize (Hticket _ _ _ Hdestruct2).
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
refine_split´; eauto.
rewrite Hdestruct3 in HM.
inv HM. econstructor; eauto.
Local Transparent CalTicketLock.
simpl. rewrite HCal. trivial.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
- rewrite ZMap.gso; auto.
eapply Hticket; eauto.
Qed.
Lemma release_shared0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared0_spec0))
(id ↦ primcall_release_lock_compatsem id (release_shared0_spec0)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit (release_shared0_exist (valid_arg:= Shared2ID0)); eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- econstructor; eauto.
+ econstructor; eauto.
eapply release_shared0_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
Section LOG_HOLD_SIM.
Lemma log_hold_match:
∀ s i ofs d d´ m f,
log_hold_spec i ofs d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold log_hold_spec; intros.
subdestruct; inv H.
inv H0. constructor. simpl.
inv Hlog. econstructor; eauto.
intros.
specialize (Hticket _ _ _ Hvalid).
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
refine_split´; eauto.
destruct (zeq z z0); subst.
- rewrite ZMap.gss. rewrite Hdestruct2 in HM. inv HM.
destruct tq.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
- rewrite ZMap.gso; auto.
Qed.
Lemma log_hold_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem log_hold_spec)
(id ↦ gensem log_hold_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit log_hold_exist; eauto 1. intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
- repeat econstructor; eauto ; try congruence.
-
eapply log_hold_match; eauto.
Qed.
End LOG_HOLD_SIM.
Section PAGE_COPY_SIM.
Lemma page_copy´´´_match:
∀ s d d´ m index i from f,
page_copy´´´_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy´´´_spec; intros.
subdestruct; inv H.
inv H0. constructor. simpl.
inv Hlog. econstructor; eauto.
intros.
specialize (Hticket _ _ _ Hvalid).
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
refine_split´; eauto.
destruct (zeq z z0); subst.
- rewrite ZMap.gss. rewrite Hdestruct5 in HM. inv HM.
destruct tq.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
- rewrite ZMap.gso; auto.
Qed.
Lemma page_copy´´´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy´´´_spec)
(id ↦ gensem page_copy´´´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy´´´_exist; eauto 1. intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
- repeat econstructor; eauto ; try congruence.
-
eapply page_copy´´´_match; eauto.
Qed.
End PAGE_COPY_SIM.
Lemma passthrough_correct:
sim (crel HDATA LDATA) mticketlockintro_passthrough mcurid.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´´´_sim.
- apply page_copy_back´_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply bootloader0_sim.
- apply get_CPU_ID_sim.
- apply release_shared0_sim.
- assert (Hp: match_impl_multi_log_one acquire_shared0_log_update_match).
{
constructor.
intros.
destruct H.
destruct Hlog.
constructor.
econstructor; eauto.
intros.
edestruct Hticket as (v1 & v2 & Hv1 & Hv2 & Hvi1 & Hvi2 & H); eauto.
∃ v1, v2.
repeat (apply conj; eauto).
simpl.
destruct (Decision.decide (z0 = z)); subst.
- rewrite ZMap.gss.
rewrite H0 in H; clear H0.
inversion H; clear H; subst.
eapply H1 in HCal.
edestruct HCal as (t´ & n´ & tq´ & Hl´ & Ht´ & Hn´).
rewrite <- Hn´.
rewrite <- Ht´.
econstructor; eauto.
- rewrite ZMap.gso by eauto.
assumption.
}
apply (acquire_shared0_sim (valid_id_args:= Shared2ID_valid0)).
intros. inv H. trivial. inv H0.
- apply log_hold_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply serial_irq_check_sim.
- apply iret_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_irq_current_sim.
- apply ic_intr_sim.
- apply save_context_sim.
- apply restore_context_sim.
- apply local_irq_save_sim.
- apply local_irq_restore_sim.
- apply serial_in_sim.
- apply serial_out_sim.
- apply serial_hw_intr_sim.
- apply ioapic_read_sim.
- apply ioapic_write_sim.
- apply lapic_read_sim.
- apply lapic_write_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End WITHMEM.
End Refinement.
Context `{real_params: RealParams}.
Context `{multi_oracle_prop: MultiOracleProp}.
Section WITHMEM.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Ltac pattern2_refinement_simpl:=
pattern2_refinement_simpl´ (@relate_AbData).
Global Instance: (LoadStoreProp (hflatmem_store:= flatmem_store´) (lflatmem_store:= flatmem_store´)).
Proof.
accessor_prop_tac.
- eapply flatmem_store´_exists; eauto.
Qed.
Lemma IntUnsignedRange: ∀ i,
0 ≤ Int.unsigned i ≤ Int.max_unsigned.
Proof.
intros.
generalize (Int.unsigned_range i).
generalize max_unsigned_val; intro muval.
unfold Int.modulus, two_power_nat, shift_nat; simpl.
intro.
omega.
Qed.
Lemma CalTicketLockWraparoundRange: ∀ l l´ t n,
CalTicketLockWraparound l = Some (t, n, l´) →
(0 ≤ t ≤ Int.max_unsigned ∧
0 ≤ n ≤ Int.max_unsigned).
Proof.
generalize max_unsigned_val; intro muval.
intros.
destruct l.
simpl in H.
inv H.
split; omega.
simpl in H;
subdestruct; inv H; simpl in *;
split; eapply IntUnsignedRange.
Qed.
Lemma release_shared0_match:
∀ s i ofs e d d´ m f,
release_shared0_spec0 i ofs e d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold release_shared0_spec; intros. subdestruct.
inv H. inv H0; constructor; simpl.
inv Hlog. econstructor; eauto.
intros.
destruct (zeq z z0); subst.
- rewrite ZMap.gss.
specialize (Hticket _ _ _ Hdestruct2).
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
refine_split´; eauto.
rewrite Hdestruct3 in HM.
inv HM. econstructor; eauto.
Local Transparent CalTicketLock.
simpl. rewrite HCal. trivial.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
- rewrite ZMap.gso; auto.
eapply Hticket; eauto.
Qed.
Lemma release_shared0_sim :
∀ id,
sim (crel RData RData) (id ↦ primcall_release_lock_compatsem id (release_shared0_spec0))
(id ↦ primcall_release_lock_compatsem id (release_shared0_spec0)).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData).
inv match_extcall_states.
exploit (release_shared0_exist (valid_arg:= Shared2ID0)); eauto 1; intros (labd´ & HP & HM).
eapply (extcall_args_with_data (D:= HDATAOps) d1) in H11.
exploit (extcall_args_inject (D1:= HDATAOps) (D2:= HDATAOps) d1 d2); eauto.
intros (varg´ & Hargs & Hlist).
eapply extcall_args_without_data in Hargs.
refine_split.
- econstructor; try eapply H7; eauto; try (eapply reg_symbol_inject; eassumption).
exploit Mem.loadbytes_inject; eauto.
{ eapply stencil_find_symbol_inject´; eauto. }
intros (bytes2 & HLD & Hlist).
eapply list_forall2_bytelist_inject_eq in Hlist. subst.
change (0 + 0) with 0 in HLD. trivial.
- econstructor; eauto.
+ econstructor; eauto.
eapply release_shared0_match; eauto.
+ subst rs´. val_inject_simpl.
Qed.
Section LOG_HOLD_SIM.
Lemma log_hold_match:
∀ s i ofs d d´ m f,
log_hold_spec i ofs d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold log_hold_spec; intros.
subdestruct; inv H.
inv H0. constructor. simpl.
inv Hlog. econstructor; eauto.
intros.
specialize (Hticket _ _ _ Hvalid).
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
refine_split´; eauto.
destruct (zeq z z0); subst.
- rewrite ZMap.gss. rewrite Hdestruct2 in HM. inv HM.
destruct tq.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
- rewrite ZMap.gso; auto.
Qed.
Lemma log_hold_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem log_hold_spec)
(id ↦ gensem log_hold_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit log_hold_exist; eauto 1. intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
- repeat econstructor; eauto ; try congruence.
-
eapply log_hold_match; eauto.
Qed.
End LOG_HOLD_SIM.
Section PAGE_COPY_SIM.
Lemma page_copy´´´_match:
∀ s d d´ m index i from f,
page_copy´´´_spec index i from d = Some d´
→ match_AbData s d m f
→ match_AbData s d´ m f.
Proof.
unfold page_copy´´´_spec; intros.
subdestruct; inv H.
inv H0. constructor. simpl.
inv Hlog. econstructor; eauto.
intros.
specialize (Hticket _ _ _ Hvalid).
destruct Hticket as (v1 & v2 & HLD1 & HLD2 & HV1 & HV2 & HM).
refine_split´; eauto.
destruct (zeq z z0); subst.
- rewrite ZMap.gss. rewrite Hdestruct5 in HM. inv HM.
destruct tq.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
+ econstructor; eauto.
simpl. rewrite HCal.
eapply CalTicketLockWraparoundRange in HCal.
destruct HCal.
repeat rewrite Int.unsigned_repr; eauto.
- rewrite ZMap.gso; auto.
Qed.
Lemma page_copy´´´_sim :
∀ id,
sim (crel RData RData) (id ↦ gensem page_copy´´´_spec)
(id ↦ gensem page_copy´´´_spec).
Proof.
intros. layer_sim_simpl. compatsim_simpl (@match_AbData). intros.
exploit page_copy´´´_exist; eauto 1. intros [labd´ [HP HM]].
refine_split;
match goal with
| |- inject_incr ?f ?f ⇒ apply inject_incr_refl
| _ ⇒ (econstructor; eauto ; try congruence)
end;
match goal with
| |- _ PC = Vptr _ _ ⇒ eapply reg_symbol_inject; eassumption
| |- _ → val_inject _ _ _ ⇒ val_inject_simpl
| _ ⇒ idtac
end.
- repeat econstructor; eauto ; try congruence.
-
eapply page_copy´´´_match; eauto.
Qed.
End PAGE_COPY_SIM.
Lemma passthrough_correct:
sim (crel HDATA LDATA) mticketlockintro_passthrough mcurid.
Proof.
sim_oplus.
- apply fload´_sim.
- apply fstore´_sim.
- apply page_copy´´´_sim.
- apply page_copy_back´_sim.
- apply vmxinfo_get_sim.
- apply setPG_sim.
- apply setCR3_sim.
- apply get_size_sim.
- apply is_mm_usable_sim.
- apply get_mm_s_sim.
- apply get_mm_l_sim.
- apply bootloader0_sim.
- apply get_CPU_ID_sim.
- apply release_shared0_sim.
- assert (Hp: match_impl_multi_log_one acquire_shared0_log_update_match).
{
constructor.
intros.
destruct H.
destruct Hlog.
constructor.
econstructor; eauto.
intros.
edestruct Hticket as (v1 & v2 & Hv1 & Hv2 & Hvi1 & Hvi2 & H); eauto.
∃ v1, v2.
repeat (apply conj; eauto).
simpl.
destruct (Decision.decide (z0 = z)); subst.
- rewrite ZMap.gss.
rewrite H0 in H; clear H0.
inversion H; clear H; subst.
eapply H1 in HCal.
edestruct HCal as (t´ & n´ & tq´ & Hl´ & Ht´ & Hn´).
rewrite <- Hn´.
rewrite <- Ht´.
econstructor; eauto.
- rewrite ZMap.gso by eauto.
assumption.
}
apply (acquire_shared0_sim (valid_id_args:= Shared2ID_valid0)).
intros. inv H. trivial. inv H0.
- apply log_hold_sim.
- apply get_curid_sim.
- apply set_curid_sim.
- apply set_curid_init_sim.
- apply trapin_sim.
- apply trapout´_sim.
- apply hostin_sim.
- apply hostout´_sim.
- apply proc_create_postinit_sim.
- apply trap_info_get_sim.
- apply trap_info_ret_sim.
- apply serial_irq_check_sim.
- apply iret_sim.
- apply cli_sim.
- apply sti_sim.
- apply serial_irq_current_sim.
- apply ic_intr_sim.
- apply save_context_sim.
- apply restore_context_sim.
- apply local_irq_save_sim.
- apply local_irq_restore_sim.
- apply serial_in_sim.
- apply serial_out_sim.
- apply serial_hw_intr_sim.
- apply ioapic_read_sim.
- apply ioapic_write_sim.
- apply lapic_read_sim.
- apply lapic_write_sim.
- layer_sim_simpl.
+ eapply load_correct1.
+ eapply store_correct1.
Qed.
End WITHMEM.
End Refinement.