Require Import Coqlib.
Require Import Maps.
Require Import ASTExtra.
Require Import Integers.
Require Import Floats.
Require Import Values.
Require Import Memory.
Require Import Events.
Require Import Stacklayout.
Require Import Globalenvs.
Require Import Smallstep.
Require Import AuxStateDataType.
Require Import CommonTactic.
Require Import AuxLemma.
Require Import RealParams.
Require Import PrimSemantics.
Require Import XOmega.
Require Import liblayers.logic.PTreeModules.
Require Import liblayers.logic.LayerLogicImpl.
Require Import liblayers.compat.CompatLayers.
Require Import liblayers.compat.CompatGenSem.
Require Import Constants.
Require Import AbsMachine.Spec.
Require Import MmioSPTWalk.Spec.
Require Import SmmuOps.Spec.
Require Import RData.
Require Import CtxtSwitch.Spec.
Require Import MemHandler.Spec.
Require Import NPTWalk.Spec.
Require Import FaultHandler.Spec.
Require Import Ident.
Require Import BootOps.Spec.
Require Import HypsecCommLib.
Local Open Scope Z_scope.
Section FaultHandlerLayer.
Context `{real_params: RealParams}.
Section InvDef.
Record high_level_invariant (adt: RData) :=
mkInvariants { }.
Global Instance FaultHandler_ops : CompatDataOps RData :=
{
empty_data := empty_adt;
high_level_invariant := high_level_invariant;
low_level_invariant := fun (b: block) (d: RData) => True;
kernel_mode adt := True
}.
End InvDef.
Section InvInit.
Global Instance FaultHandler_prf : CompatData RData.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
End InvInit.
Context `{Hstencil: Stencil}.
Context `{Hmem: Mem.MemoryModelX}.
Context `{Hmwd: UseMemWithData mem}.
Section InvProof.
Global Instance core_handle_pvops_inv: PreservesInvariants core_handle_pvops_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance handle_host_stage2_fault_inv: PreservesInvariants handle_host_stage2_fault_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance remap_vm_image_inv: PreservesInvariants remap_vm_image_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance set_boot_info_inv: PreservesInvariants set_boot_info_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance save_vm_inv: PreservesInvariants save_vm_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance panic_inv: PreservesInvariants panic_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance exit_populate_fault_inv: PreservesInvariants exit_populate_fault_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance core_to_host_inv: PreservesInvariants core_to_host_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance core_to_vm_inv: PreservesInvariants core_to_vm_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance get_cur_vmid_inv: PreservesInvariants get_cur_vmid_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance restore_host_inv: PreservesInvariants restore_host_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance get_cur_vcpuid_inv: PreservesInvariants get_cur_vcpuid_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance kvm_phys_addr_ioremap_inv: PreservesInvariants kvm_phys_addr_ioremap_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance mem_load_ref_inv: PreservesInvariants mem_load_ref_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance dev_load_ref_inv: PreservesInvariants dev_load_ref_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance dev_store_ref_inv: PreservesInvariants dev_store_ref_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance clear_vm_stage2_range_inv: PreservesInvariants clear_vm_stage2_range_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance get_shadow_ctxt_inv: PreservesInvariants get_shadow_ctxt_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance core_handle_sys64_inv: PreservesInvariants core_handle_sys64_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance save_host_inv: PreservesInvariants save_host_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance vm_to_core_inv: PreservesInvariants vm_to_core_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance timer_set_cntvoff_inv: PreservesInvariants timer_set_cntvoff_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance set_shadow_ctxt_inv: PreservesInvariants set_shadow_ctxt_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance el2_arm_lpae_clear_inv: PreservesInvariants el2_arm_lpae_clear_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance register_kvm_inv: PreservesInvariants register_kvm_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance restore_vm_inv: PreservesInvariants restore_vm_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance verify_and_load_images_inv: PreservesInvariants verify_and_load_images_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance el2_arm_lpae_iova_to_phys_inv: PreservesInvariants el2_arm_lpae_iova_to_phys_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance el2_alloc_smmu_pgd_inv: PreservesInvariants el2_alloc_smmu_pgd_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance register_vcpu_inv: PreservesInvariants register_vcpu_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance host_to_core_inv: PreservesInvariants host_to_core_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance el2_arm_lpae_map_inv: PreservesInvariants el2_arm_lpae_map_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance el2_free_smmu_pgd_inv: PreservesInvariants el2_free_smmu_pgd_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
Global Instance mem_store_ref_inv: PreservesInvariants mem_store_ref_spec.
Proof.
constructor; intros; simpl; eauto.
constructor.
Qed.
End InvProof.
Section LayerDef.
Definition FaultHandler_fresh : compatlayer (cdata RData) :=
core_handle_pvops ↦ gensem core_handle_pvops_spec
⊕ handle_host_stage2_fault ↦ gensem handle_host_stage2_fault_spec.
Definition FaultHandler_passthrough : compatlayer (cdata RData) :=
remap_vm_image ↦ gensem remap_vm_image_spec
⊕ set_boot_info ↦ gensem set_boot_info_spec
⊕ save_vm ↦ gensem save_vm_spec
⊕ panic ↦ gensem panic_spec
⊕ exit_populate_fault ↦ gensem exit_populate_fault_spec
⊕ core_to_host ↦ gensem core_to_host_spec
⊕ core_to_vm ↦ gensem core_to_vm_spec
⊕ get_cur_vmid ↦ gensem get_cur_vmid_spec
⊕ restore_host ↦ gensem restore_host_spec
⊕ get_cur_vcpuid ↦ gensem get_cur_vcpuid_spec
⊕ kvm_phys_addr_ioremap ↦ gensem kvm_phys_addr_ioremap_spec
⊕ mem_load_ref ↦ gensem mem_load_ref_spec
⊕ dev_load_ref ↦ gensem dev_load_ref_spec
⊕ dev_store_ref ↦ gensem dev_store_ref_spec
⊕ clear_vm_stage2_range ↦ gensem clear_vm_stage2_range_spec
⊕ get_shadow_ctxt ↦ gensem get_shadow_ctxt_spec
⊕ core_handle_sys64 ↦ gensem core_handle_sys64_spec
⊕ save_host ↦ gensem save_host_spec
⊕ vm_to_core ↦ gensem vm_to_core_spec
⊕ timer_set_cntvoff ↦ gensem timer_set_cntvoff_spec
⊕ set_shadow_ctxt ↦ gensem set_shadow_ctxt_spec
⊕ el2_arm_lpae_clear ↦ gensem el2_arm_lpae_clear_spec
⊕ register_kvm ↦ gensem register_kvm_spec
⊕ restore_vm ↦ gensem restore_vm_spec
⊕ verify_and_load_images ↦ gensem verify_and_load_images_spec
⊕ el2_arm_lpae_iova_to_phys ↦ gensem el2_arm_lpae_iova_to_phys_spec
⊕ el2_alloc_smmu_pgd ↦ gensem el2_alloc_smmu_pgd_spec
⊕ register_vcpu ↦ gensem register_vcpu_spec
⊕ host_to_core ↦ gensem host_to_core_spec
⊕ el2_arm_lpae_map ↦ gensem el2_arm_lpae_map_spec
⊕ el2_free_smmu_pgd ↦ gensem el2_free_smmu_pgd_spec
⊕ mem_store_ref ↦ gensem mem_store_ref_spec.
Definition FaultHandler := FaultHandler_fresh ⊕ FaultHandler_passthrough.
End LayerDef.
End FaultHandlerLayer.