Layer.v

Require Import LayerDeps.
Require Import Ident.
Require Import RData.
Require Import EventReplay.
Require Import MoverTypes.
Require Import Constants.
Require Import CommonLib.
Require Import AbsAccessor.Spec.
Require Import BaremoreHandler.Spec.
Require Import BaremoreSMC.Spec.
Require Import RmiAux.Spec.

Local Open Scope Z_scope.

Section Layer.

  Context `{real_params: RealParams}.

  Section InvDef.

    Record high_level_invariant (adt: RData) :=
      mkInvariants { }.

    Global Instance RmiAux_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 RmiAux_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 get_realm_params_inv: PreservesInvariants get_realm_params_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance validate_realm_params_inv: PreservesInvariants validate_realm_params_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance init_rec_sysregs_inv: PreservesInvariants init_rec_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance init_common_sysregs_inv: PreservesInvariants init_common_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance shiftl_inv: PreservesInvariants shiftl_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_par_base_inv: PreservesInvariants get_rd_par_base_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance addr_to_idx_inv: PreservesInvariants addr_to_idx_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance el3_sync_lel_inv: PreservesInvariants el3_sync_lel_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rvic_result_target_inv: PreservesInvariants set_rvic_result_target_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_sysregs_inv: PreservesInvariants set_rec_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_psci_call_inv: PreservesInvariants get_psci_result_forward_psci_call_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_refcount_inc_inv: PreservesInvariants granule_refcount_inc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_realm_params_measurement_algo_inv: PreservesInvariants get_realm_params_measurement_algo_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_read_rec_run_inv: PreservesInvariants ns_buffer_read_rec_run_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_put_inv: PreservesInvariants granule_put_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_mark_realm_inv: PreservesInvariants smc_mark_realm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rd_state_inv: PreservesInvariants set_rd_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance entry_is_table_inv: PreservesInvariants entry_is_table_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_pstate_inv: PreservesInvariants get_rec_pstate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_granule_put_release_inv: PreservesInvariants atomic_granule_put_release_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_run_gprs_inv: PreservesInvariants get_rec_run_gprs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_ptimer_asserted_inv: PreservesInvariants set_rec_ptimer_asserted_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_timer_asserted_inv: PreservesInvariants get_timer_asserted_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_rec_idx_inv: PreservesInvariants get_rec_rec_idx_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_run_is_emulated_mmio_inv: PreservesInvariants get_rec_run_is_emulated_mmio_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance read_reg_inv: PreservesInvariants read_reg_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_refcount_dec_inv: PreservesInvariants granule_refcount_dec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance interrupt_bitmap_dword_inv: PreservesInvariants interrupt_bitmap_dword_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_rec_pstate_inv: PreservesInvariants measurement_extend_rec_pstate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rd_measurement_algo_inv: PreservesInvariants set_rd_measurement_algo_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_ptimer_masked_inv: PreservesInvariants get_rec_ptimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_data_header_inv: PreservesInvariants measurement_extend_data_header_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_lock_inv: PreservesInvariants granule_lock_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_unmap_inv: PreservesInvariants ns_buffer_unmap_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_memzero_mapped_inv: PreservesInvariants granule_memzero_mapped_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ptr_eq_inv: PreservesInvariants ptr_eq_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_common_sysregs_inv: PreservesInvariants get_rec_common_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_addr_in_par_rec_inv: PreservesInvariants is_addr_in_par_rec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_state_inv: PreservesInvariants get_rd_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_par_base_inv: PreservesInvariants set_rec_par_base_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_sixty_four_inv: PreservesInvariants esr_sixty_four_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rvic_mask_bits_inv: PreservesInvariants get_rvic_mask_bits_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance run_realm_inv: PreservesInvariants run_realm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_params_flags_inv: PreservesInvariants get_rec_params_flags_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_timer_masked_inv: PreservesInvariants get_timer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_target_rec_inv: PreservesInvariants get_target_rec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_psci_result_forward_psci_call_inv: PreservesInvariants set_psci_result_forward_psci_call_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_g_rtt_refcount_inv: PreservesInvariants get_g_rtt_refcount_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_srt_inv: PreservesInvariants esr_srt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_rec_header_inv: PreservesInvariants measurement_extend_rec_header_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_pstate_inv: PreservesInvariants set_rec_pstate_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_rec_regs_inv: PreservesInvariants measurement_extend_rec_regs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_pc_inv: PreservesInvariants get_rec_pc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_par_end_inv: PreservesInvariants get_rd_par_end_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_rec_valid_inv: PreservesInvariants is_rec_valid_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_get_inv: PreservesInvariants granule_get_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rd_par_base_inv: PreservesInvariants set_rd_par_base_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_realm_params_par_size_inv: PreservesInvariants get_realm_params_par_size_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance buffer_unmap_inv: PreservesInvariants buffer_unmap_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance access_len_inv: PreservesInvariants access_len_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance enter_rmm_inv: PreservesInvariants enter_rmm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_g_rec_rd_inv: PreservesInvariants get_g_rec_rd_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_realm_params_rtt_addr_inv: PreservesInvariants get_realm_params_rtt_addr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_ptimer_masked_inv: PreservesInvariants set_rec_ptimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rd_g_rec_list_inv: PreservesInvariants set_rd_g_rec_list_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rd_par_end_inv: PreservesInvariants set_rd_par_end_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance sysreg_read_inv: PreservesInvariants sysreg_read_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_set_state_inv: PreservesInvariants granule_set_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance null_ptr_inv: PreservesInvariants null_ptr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance timer_is_masked_inv: PreservesInvariants timer_is_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rd_g_rtt_inv: PreservesInvariants set_rd_g_rtt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_ns_state_inv: PreservesInvariants get_ns_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_g_rec_rd_inv: PreservesInvariants set_g_rec_rd_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_vtimer_masked_inv: PreservesInvariants set_rec_vtimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_wi_g_llt_inv: PreservesInvariants get_wi_g_llt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_esr_inv: PreservesInvariants set_rec_run_esr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_map_inv: PreservesInvariants granule_map_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rvic_result_ns_notify_inv: PreservesInvariants set_rvic_result_ns_notify_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance realm_get_rec_entry_inv: PreservesInvariants realm_get_rec_entry_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_ns_state_inv: PreservesInvariants set_ns_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_g_rec_inv: PreservesInvariants get_rec_g_rec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_gprs_inv: PreservesInvariants set_rec_run_gprs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_hpfar_inv: PreservesInvariants set_rec_run_hpfar_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x0_inv: PreservesInvariants get_psci_result_x0_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_runnable_inv: PreservesInvariants set_rec_runnable_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x1_inv: PreservesInvariants get_psci_result_x1_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance interrupt_bit_inv: PreservesInvariants interrupt_bit_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x2_inv: PreservesInvariants get_psci_result_x2_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_lock_granule_inv: PreservesInvariants find_lock_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_null_inv: PreservesInvariants is_null_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_rvic_enabled_inv: PreservesInvariants get_rec_rvic_enabled_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance assert_cond_inv: PreservesInvariants assert_cond_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_target_rec_inv: PreservesInvariants set_target_rec_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance pgte_read_inv: PreservesInvariants pgte_read_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_g_rec_list_inv: PreservesInvariants get_rd_g_rec_list_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_vtimer_masked_inv: PreservesInvariants get_rec_vtimer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_wi_g_llt_inv: PreservesInvariants set_wi_g_llt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_last_run_info_esr_inv: PreservesInvariants get_rec_last_run_info_esr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_params_pc_inv: PreservesInvariants get_rec_params_pc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_finish_inv: PreservesInvariants measurement_finish_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_g_rec_list_inv: PreservesInvariants get_rec_g_rec_list_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_is_write_inv: PreservesInvariants esr_is_write_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_rec_sysregs_inv: PreservesInvariants measurement_extend_rec_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_x3_inv: PreservesInvariants get_psci_result_x3_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_wi_index_inv: PreservesInvariants get_wi_index_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_wi_index_inv: PreservesInvariants set_wi_index_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_timer_masked_inv: PreservesInvariants set_timer_masked_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance mpidr_to_rec_idx_inv: PreservesInvariants mpidr_to_rec_idx_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_unlock_inv: PreservesInvariants granule_unlock_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance emulate_timer_ctl_read_inv: PreservesInvariants emulate_timer_ctl_read_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_params_gprs_inv: PreservesInvariants get_rec_params_gprs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance exit_rmm_inv: PreservesInvariants exit_rmm_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_extend_data_inv: PreservesInvariants measurement_extend_data_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ESR_EL2_SYSREG_IS_WRITE_inv: PreservesInvariants ESR_EL2_SYSREG_IS_WRITE_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance barrier_inv: PreservesInvariants barrier_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance access_mask_inv: PreservesInvariants access_mask_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance esr_sign_extend_inv: PreservesInvariants esr_sign_extend_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_dispose_pending_inv: PreservesInvariants set_rec_dispose_pending_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rd_g_rtt_inv: PreservesInvariants get_rd_g_rtt_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_last_run_info_esr_inv: PreservesInvariants set_rec_last_run_info_esr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rvic_result_x0_inv: PreservesInvariants set_rvic_result_x0_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_memzero_inv: PreservesInvariants granule_memzero_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance test_bit_acquire_64_inv: PreservesInvariants test_bit_acquire_64_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_psci_result_forward_x1_inv: PreservesInvariants set_psci_result_forward_x1_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_regs_inv: PreservesInvariants get_rec_regs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_x3_inv: PreservesInvariants get_psci_result_forward_x3_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_rvic_inv: PreservesInvariants get_rec_rvic_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance realm_set_rec_entry_inv: PreservesInvariants realm_set_rec_entry_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_x2_inv: PreservesInvariants get_psci_result_forward_x2_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_psci_result_forward_x1_inv: PreservesInvariants get_psci_result_forward_x1_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_exit_reason_inv: PreservesInvariants set_rec_run_exit_reason_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ESR_EL2_SYSREG_ISS_RT_inv: PreservesInvariants ESR_EL2_SYSREG_ISS_RT_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_granule_put_inv: PreservesInvariants atomic_granule_put_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_read_rec_params_inv: PreservesInvariants ns_buffer_read_rec_params_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_lock_three_delegated_granules_inv: PreservesInvariants find_lock_three_delegated_granules_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_bit_set_release_64_inv: PreservesInvariants atomic_bit_set_release_64_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance read_idreg_inv: PreservesInvariants read_idreg_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_par_end_inv: PreservesInvariants get_rec_par_end_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_g_rd_inv: PreservesInvariants set_rec_g_rd_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_realm_params_par_base_inv: PreservesInvariants get_realm_params_par_base_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance measurement_start_inv: PreservesInvariants measurement_start_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_psci_result_x0_inv: PreservesInvariants set_psci_result_x0_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_mapping_inv: PreservesInvariants set_mapping_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_pc_inv: PreservesInvariants set_rec_pc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_regs_inv: PreservesInvariants set_rec_regs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_runnable_inv: PreservesInvariants get_rec_runnable_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_granule_map_inv: PreservesInvariants ns_granule_map_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_sysregs_inv: PreservesInvariants get_rec_sysregs_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_vtimer_asserted_inv: PreservesInvariants set_rec_vtimer_asserted_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_emulated_write_val_inv: PreservesInvariants set_rec_run_emulated_write_val_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_run_far_inv: PreservesInvariants set_rec_run_far_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance mpidr_is_valid_inv: PreservesInvariants mpidr_is_valid_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_run_emulated_read_val_inv: PreservesInvariants get_rec_run_emulated_read_val_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_g_rec_list_inv: PreservesInvariants set_rec_g_rec_list_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_vtimer_inv: PreservesInvariants get_rec_vtimer_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rec_par_end_inv: PreservesInvariants set_rec_par_end_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance granule_get_state_inv: PreservesInvariants granule_get_state_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_ptimer_inv: PreservesInvariants get_rec_ptimer_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_bitmap_loc_inv: PreservesInvariants get_bitmap_loc_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance smc_mark_nonsecure_inv: PreservesInvariants smc_mark_nonsecure_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_realm_params_rec_list_addr_inv: PreservesInvariants get_realm_params_rec_list_addr_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_g_rtt_rd_inv: PreservesInvariants set_g_rtt_rd_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_bit_clear_release_64_inv: PreservesInvariants atomic_bit_clear_release_64_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance ns_buffer_read_data_inv: PreservesInvariants ns_buffer_read_data_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance pgte_write_inv: PreservesInvariants pgte_write_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance is_addr_in_par_inv: PreservesInvariants is_addr_in_par_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance sysreg_write_inv: PreservesInvariants sysreg_write_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_granule_inv: PreservesInvariants find_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_par_base_inv: PreservesInvariants get_rec_par_base_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rec_g_rd_inv: PreservesInvariants get_rec_g_rd_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance init_rec_read_only_inv: PreservesInvariants init_rec_read_only_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_locked_granule_inv: PreservesInvariants get_locked_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance get_rvic_pending_bits_inv: PreservesInvariants get_rvic_pending_bits_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance find_lock_unused_granule_inv: PreservesInvariants find_lock_unused_granule_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance entry_to_phys_inv: PreservesInvariants entry_to_phys_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance stage2_tlbi_ipa_inv: PreservesInvariants stage2_tlbi_ipa_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance atomic_granule_get_inv: PreservesInvariants atomic_granule_get_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance user_step_inv: PreservesInvariants user_step_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance link_table_inv: PreservesInvariants link_table_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance set_rvic_mask_bits_inv: PreservesInvariants set_rvic_mask_bits_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance timer_condition_met_inv: PreservesInvariants timer_condition_met_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

    Global Instance addr_is_level_aligned_inv: PreservesInvariants addr_is_level_aligned_spec.
    Proof.
      constructor; intros; simpl; eauto.
      constructor.
    Qed.

  End InvProof.

  Section LayerDef.

    Definition RmiAux_fresh : compatlayer (cdata RData) :=
      _get_realm_params ↦ gensem get_realm_params_spec
        ⊕ _validate_realm_params ↦ gensem validate_realm_params_spec
        ⊕ _init_rec_sysregs ↦ gensem init_rec_sysregs_spec
        ⊕ _init_common_sysregs ↦ gensem init_common_sysregs_spec
      .

    Definition RmiAux_passthrough : compatlayer (cdata RData) :=
      _shiftl ↦ gensem shiftl_spec
        ⊕ _get_rd_par_base ↦ gensem get_rd_par_base_spec
        ⊕ _addr_to_idx ↦ gensem addr_to_idx_spec
        ⊕ _el3_sync_lel ↦ gensem el3_sync_lel_spec
        ⊕ _set_rvic_result_target ↦ gensem set_rvic_result_target_spec
        ⊕ _set_rec_sysregs ↦ gensem set_rec_sysregs_spec
        ⊕ _get_psci_result_forward_psci_call ↦ gensem get_psci_result_forward_psci_call_spec
        ⊕ _granule_refcount_inc ↦ gensem granule_refcount_inc_spec
        ⊕ _get_realm_params_measurement_algo ↦ gensem get_realm_params_measurement_algo_spec
        ⊕ _ns_buffer_read_rec_run ↦ gensem ns_buffer_read_rec_run_spec
        ⊕ _granule_put ↦ gensem granule_put_spec
        ⊕ _smc_mark_realm ↦ gensem smc_mark_realm_spec
        ⊕ _set_rd_state ↦ gensem set_rd_state_spec
        ⊕ _entry_is_table ↦ gensem entry_is_table_spec
        ⊕ _get_rec_pstate ↦ gensem get_rec_pstate_spec
        ⊕ _atomic_granule_put_release ↦ gensem atomic_granule_put_release_spec
        ⊕ _get_rec_run_gprs ↦ gensem get_rec_run_gprs_spec
        ⊕ _set_rec_ptimer_asserted ↦ gensem set_rec_ptimer_asserted_spec
        ⊕ _get_timer_asserted ↦ gensem get_timer_asserted_spec
        ⊕ _get_rec_rec_idx ↦ gensem get_rec_rec_idx_spec
        ⊕ _get_rec_run_is_emulated_mmio ↦ gensem get_rec_run_is_emulated_mmio_spec
        ⊕ _read_reg ↦ gensem read_reg_spec
        ⊕ _granule_refcount_dec ↦ gensem granule_refcount_dec_spec
        ⊕ _interrupt_bitmap_dword ↦ gensem interrupt_bitmap_dword_spec
        ⊕ _measurement_extend_rec_pstate ↦ gensem measurement_extend_rec_pstate_spec
        ⊕ _set_rd_measurement_algo ↦ gensem set_rd_measurement_algo_spec
        ⊕ _get_rec_ptimer_masked ↦ gensem get_rec_ptimer_masked_spec
        ⊕ _measurement_extend_data_header ↦ gensem measurement_extend_data_header_spec
        ⊕ _granule_lock ↦ gensem granule_lock_spec
        ⊕ _ns_buffer_unmap ↦ gensem ns_buffer_unmap_spec
        ⊕ _granule_memzero_mapped ↦ gensem granule_memzero_mapped_spec
        ⊕ _ptr_eq ↦ gensem ptr_eq_spec
        ⊕ _get_rec_common_sysregs ↦ gensem get_rec_common_sysregs_spec
        ⊕ _is_addr_in_par_rec ↦ gensem is_addr_in_par_rec_spec
        ⊕ _get_rd_state ↦ gensem get_rd_state_spec
        ⊕ _set_rec_par_base ↦ gensem set_rec_par_base_spec
        ⊕ _esr_sixty_four ↦ gensem esr_sixty_four_spec
        ⊕ _get_rvic_mask_bits ↦ gensem get_rvic_mask_bits_spec
        ⊕ _run_realm ↦ gensem run_realm_spec
        ⊕ _get_rec_params_flags ↦ gensem get_rec_params_flags_spec
        ⊕ _get_timer_masked ↦ gensem get_timer_masked_spec
        ⊕ _get_target_rec ↦ gensem get_target_rec_spec
        ⊕ _set_psci_result_forward_psci_call ↦ gensem set_psci_result_forward_psci_call_spec
        ⊕ _get_g_rtt_refcount ↦ gensem get_g_rtt_refcount_spec
        ⊕ _esr_srt ↦ gensem esr_srt_spec
        ⊕ _measurement_extend_rec_header ↦ gensem measurement_extend_rec_header_spec
        ⊕ _set_rec_pstate ↦ gensem set_rec_pstate_spec
        ⊕ _measurement_extend_rec_regs ↦ gensem measurement_extend_rec_regs_spec
        ⊕ _get_rec_pc ↦ gensem get_rec_pc_spec
        ⊕ _get_rd_par_end ↦ gensem get_rd_par_end_spec
        ⊕ _is_rec_valid ↦ gensem is_rec_valid_spec
        ⊕ _granule_get ↦ gensem granule_get_spec
        ⊕ _set_rd_par_base ↦ gensem set_rd_par_base_spec
        ⊕ _get_realm_params_par_size ↦ gensem get_realm_params_par_size_spec
        ⊕ _buffer_unmap ↦ gensem buffer_unmap_spec
        ⊕ _access_len ↦ gensem access_len_spec
        ⊕ _enter_rmm ↦ gensem enter_rmm_spec
        ⊕ _get_g_rec_rd ↦ gensem get_g_rec_rd_spec
        ⊕ _get_realm_params_rtt_addr ↦ gensem get_realm_params_rtt_addr_spec
        ⊕ _set_rec_ptimer_masked ↦ gensem set_rec_ptimer_masked_spec
        ⊕ _set_rd_g_rec_list ↦ gensem set_rd_g_rec_list_spec
        ⊕ _set_rd_par_end ↦ gensem set_rd_par_end_spec
        ⊕ _sysreg_read ↦ gensem sysreg_read_spec
        ⊕ _granule_set_state ↦ gensem granule_set_state_spec
        ⊕ _null_ptr ↦ gensem null_ptr_spec
        ⊕ _timer_is_masked ↦ gensem timer_is_masked_spec
        ⊕ _set_rd_g_rtt ↦ gensem set_rd_g_rtt_spec
        ⊕ _get_ns_state ↦ gensem get_ns_state_spec
        ⊕ _set_g_rec_rd ↦ gensem set_g_rec_rd_spec
        ⊕ _set_rec_vtimer_masked ↦ gensem set_rec_vtimer_masked_spec
        ⊕ _get_wi_g_llt ↦ gensem get_wi_g_llt_spec
        ⊕ _set_rec_run_esr ↦ gensem set_rec_run_esr_spec
        ⊕ _granule_map ↦ gensem granule_map_spec
        ⊕ _set_rvic_result_ns_notify ↦ gensem set_rvic_result_ns_notify_spec
        ⊕ _realm_get_rec_entry ↦ gensem realm_get_rec_entry_spec
        ⊕ _set_ns_state ↦ gensem set_ns_state_spec
        ⊕ _get_rec_g_rec ↦ gensem get_rec_g_rec_spec
        ⊕ _set_rec_run_gprs ↦ gensem set_rec_run_gprs_spec
        ⊕ _set_rec_run_hpfar ↦ gensem set_rec_run_hpfar_spec
        ⊕ _get_psci_result_x0 ↦ gensem get_psci_result_x0_spec
        ⊕ _set_rec_runnable ↦ gensem set_rec_runnable_spec
        ⊕ _get_psci_result_x1 ↦ gensem get_psci_result_x1_spec
        ⊕ _interrupt_bit ↦ gensem interrupt_bit_spec
        ⊕ _get_psci_result_x2 ↦ gensem get_psci_result_x2_spec
        ⊕ _find_lock_granule ↦ gensem find_lock_granule_spec
        ⊕ _is_null ↦ gensem is_null_spec
        ⊕ _get_rec_rvic_enabled ↦ gensem get_rec_rvic_enabled_spec
        ⊕ _assert_cond ↦ gensem assert_cond_spec
        ⊕ _set_target_rec ↦ gensem set_target_rec_spec
        ⊕ _pgte_read ↦ gensem pgte_read_spec
        ⊕ _get_rd_g_rec_list ↦ gensem get_rd_g_rec_list_spec
        ⊕ _get_rec_vtimer_masked ↦ gensem get_rec_vtimer_masked_spec
        ⊕ _set_wi_g_llt ↦ gensem set_wi_g_llt_spec
        ⊕ _get_rec_last_run_info_esr ↦ gensem get_rec_last_run_info_esr_spec
        ⊕ _get_rec_params_pc ↦ gensem get_rec_params_pc_spec
        ⊕ _measurement_finish ↦ gensem measurement_finish_spec
        ⊕ _get_rec_g_rec_list ↦ gensem get_rec_g_rec_list_spec
        ⊕ _esr_is_write ↦ gensem esr_is_write_spec
        ⊕ _measurement_extend_rec_sysregs ↦ gensem measurement_extend_rec_sysregs_spec
        ⊕ _get_psci_result_x3 ↦ gensem get_psci_result_x3_spec
        ⊕ _get_wi_index ↦ gensem get_wi_index_spec
        ⊕ _set_wi_index ↦ gensem set_wi_index_spec
        ⊕ _set_timer_masked ↦ gensem set_timer_masked_spec
        ⊕ _mpidr_to_rec_idx ↦ gensem mpidr_to_rec_idx_spec
        ⊕ _granule_unlock ↦ gensem granule_unlock_spec
        ⊕ _emulate_timer_ctl_read ↦ gensem emulate_timer_ctl_read_spec
        ⊕ _get_rec_params_gprs ↦ gensem get_rec_params_gprs_spec
        ⊕ _exit_rmm ↦ gensem exit_rmm_spec
        ⊕ _measurement_extend_data ↦ gensem measurement_extend_data_spec
        ⊕ _ESR_EL2_SYSREG_IS_WRITE ↦ gensem ESR_EL2_SYSREG_IS_WRITE_spec
        ⊕ _barrier ↦ gensem barrier_spec
        ⊕ _access_mask ↦ gensem access_mask_spec
        ⊕ _esr_sign_extend ↦ gensem esr_sign_extend_spec
        ⊕ _set_rec_dispose_pending ↦ gensem set_rec_dispose_pending_spec
        ⊕ _get_rd_g_rtt ↦ gensem get_rd_g_rtt_spec
        ⊕ _set_rec_last_run_info_esr ↦ gensem set_rec_last_run_info_esr_spec
        ⊕ _set_rvic_result_x0 ↦ gensem set_rvic_result_x0_spec
        ⊕ _granule_memzero ↦ gensem granule_memzero_spec
        ⊕ _test_bit_acquire_64 ↦ gensem test_bit_acquire_64_spec
        ⊕ _set_psci_result_forward_x1 ↦ gensem set_psci_result_forward_x1_spec
        ⊕ _get_rec_regs ↦ gensem get_rec_regs_spec
        ⊕ _get_psci_result_forward_x3 ↦ gensem get_psci_result_forward_x3_spec
        ⊕ _get_rec_rvic ↦ gensem get_rec_rvic_spec
        ⊕ _realm_set_rec_entry ↦ gensem realm_set_rec_entry_spec
        ⊕ _get_psci_result_forward_x2 ↦ gensem get_psci_result_forward_x2_spec
        ⊕ _get_psci_result_forward_x1 ↦ gensem get_psci_result_forward_x1_spec
        ⊕ _set_rec_run_exit_reason ↦ gensem set_rec_run_exit_reason_spec
        ⊕ _ESR_EL2_SYSREG_ISS_RT ↦ gensem ESR_EL2_SYSREG_ISS_RT_spec
        ⊕ _atomic_granule_put ↦ gensem atomic_granule_put_spec
        ⊕ _ns_buffer_read_rec_params ↦ gensem ns_buffer_read_rec_params_spec
        ⊕ _find_lock_three_delegated_granules ↦ gensem find_lock_three_delegated_granules_spec
        ⊕ _atomic_bit_set_release_64 ↦ gensem atomic_bit_set_release_64_spec
        ⊕ _read_idreg ↦ gensem read_idreg_spec
        ⊕ _get_rec_par_end ↦ gensem get_rec_par_end_spec
        ⊕ _set_rec_g_rd ↦ gensem set_rec_g_rd_spec
        ⊕ _get_realm_params_par_base ↦ gensem get_realm_params_par_base_spec
        ⊕ _measurement_start ↦ gensem measurement_start_spec
        ⊕ _set_psci_result_x0 ↦ gensem set_psci_result_x0_spec
        ⊕ _set_mapping ↦ gensem set_mapping_spec
        ⊕ _set_rec_pc ↦ gensem set_rec_pc_spec
        ⊕ _set_rec_regs ↦ gensem set_rec_regs_spec
        ⊕ _get_rec_runnable ↦ gensem get_rec_runnable_spec
        ⊕ _ns_granule_map ↦ gensem ns_granule_map_spec
        ⊕ _get_rec_sysregs ↦ gensem get_rec_sysregs_spec
        ⊕ _set_rec_vtimer_asserted ↦ gensem set_rec_vtimer_asserted_spec
        ⊕ _set_rec_run_emulated_write_val ↦ gensem set_rec_run_emulated_write_val_spec
        ⊕ _set_rec_run_far ↦ gensem set_rec_run_far_spec
        ⊕ _mpidr_is_valid ↦ gensem mpidr_is_valid_spec
        ⊕ _get_rec_run_emulated_read_val ↦ gensem get_rec_run_emulated_read_val_spec
        ⊕ _set_rec_g_rec_list ↦ gensem set_rec_g_rec_list_spec
        ⊕ _get_rec_vtimer ↦ gensem get_rec_vtimer_spec
        ⊕ _set_rec_par_end ↦ gensem set_rec_par_end_spec
        ⊕ _granule_get_state ↦ gensem granule_get_state_spec
        ⊕ _get_rec_ptimer ↦ gensem get_rec_ptimer_spec
        ⊕ _get_bitmap_loc ↦ gensem get_bitmap_loc_spec
        ⊕ _smc_mark_nonsecure ↦ gensem smc_mark_nonsecure_spec
        ⊕ _get_realm_params_rec_list_addr ↦ gensem get_realm_params_rec_list_addr_spec
        ⊕ _set_g_rtt_rd ↦ gensem set_g_rtt_rd_spec
        ⊕ _atomic_bit_clear_release_64 ↦ gensem atomic_bit_clear_release_64_spec
        ⊕ _ns_buffer_read_data ↦ gensem ns_buffer_read_data_spec
        ⊕ _pgte_write ↦ gensem pgte_write_spec
        ⊕ _is_addr_in_par ↦ gensem is_addr_in_par_spec
        ⊕ _sysreg_write ↦ gensem sysreg_write_spec
        ⊕ _find_granule ↦ gensem find_granule_spec
        ⊕ _get_rec_par_base ↦ gensem get_rec_par_base_spec
        ⊕ _get_rec_g_rd ↦ gensem get_rec_g_rd_spec
        ⊕ _init_rec_read_only ↦ gensem init_rec_read_only_spec
        ⊕ _get_locked_granule ↦ gensem get_locked_granule_spec
        ⊕ _get_rvic_pending_bits ↦ gensem get_rvic_pending_bits_spec
        ⊕ _find_lock_unused_granule ↦ gensem find_lock_unused_granule_spec
        ⊕ _entry_to_phys ↦ gensem entry_to_phys_spec
        ⊕ _stage2_tlbi_ipa ↦ gensem stage2_tlbi_ipa_spec
        ⊕ _atomic_granule_get ↦ gensem atomic_granule_get_spec
        ⊕ _user_step ↦ gensem user_step_spec
        ⊕ _link_table ↦ gensem link_table_spec
        ⊕ _set_rvic_mask_bits ↦ gensem set_rvic_mask_bits_spec
        ⊕ _timer_condition_met ↦ gensem timer_condition_met_spec
        ⊕ _addr_is_level_aligned ↦ gensem addr_is_level_aligned_spec
      .

    Definition RmiAux := RmiAux_fresh ⊕ RmiAux_passthrough.

  End LayerDef.

End Layer.