Library mcertikos.objects.AbstractDataType


This file defines the raw abstract data and the primitives for the MBoot layer, which is also the bottom layer of memory management
Require Import Coqlib.
Require Import Maps.
Require Import AuxStateDataType.
Require Import DeviceStateDataType.
Require Import FlatMemory.
Require Import Values.
Require Import Memory.
Require Import AuxLemma.
Require Import Constant.
Require Import Integers.

Require Import liblayers.compat.CompatLayers.
Require Export GlobalOracle.
Require Export BigStepGlobalOracle.

Section ABDATA.

  Local Open Scope Z_scope.


Raw Abstract Data

  Record RData :=
    mkRData {

        CPU_ID: Z;
        MM: MMTable;
        MMSize: Z;
        vmxinfo: VMXInfo;

        CR3: globalpointer;
        ti: trapinfo;

        pg: bool;
        ikern: bool;
        ihost: bool;

        HP: flatmem;
        cid: ZMap.t Z;
        multi_log: MultiLogPool;
        multi_oracle: MultiOraclePool;
        lock: Lock;
        
        AC : ContainerPool;

        AT: ATable;
        ATC: ATCTable;
        nps: Z;
        init: bool;
        pperm: PPermT;

        PT: Z;
        ptpool: PMapPool;
        idpde: IDPDE;
        ipt: bool;
        LAT: LATCTable;
        smspool: SharedMemSTPool;

        kctxt: KContextPool;
        sleeper: Sleeper;
        tcb: TCBPool;
        tdq: TDQueuePool;
        abtcb: AbTCBPool;
        abq: AbQueuePool;
        syncchpool : SyncChanPool;
        buffer: PageBufferPool;

        big_log: BigLogType;
        big_oracle: BigOracle;

        uctxt : UContextPool;

        ept: EPTPool;
        vmcs: VMCSPool;

        vmx: VMXPool;

        ts: Z;

        com1: SerialData;
        drv_serial: SerialDriver;
        console_concrete: ConsoleDriverConcrete;
        console: ConsoleDriver;

        ioapic: IoApicData;
        lapic: LApicData;
        tf: TrapFrames;
        tf_reg: val;
temporary place to save an intermediate tf regiter
        curr_intr_num: Z;
        intr_flag: bool;
        saved_intr_flags: list bool;

        in_intr: bool;
        i_dev_serial: bool;

        kbd: KeyboardData;
        kbd_drv: KeyboardDriver

      }.

functions to update each field of the record
  Section UPDATE_FUNCTION.

    Definition update_CPU_ID (a : RData) b :=
      mkRData b (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_MM (a : RData) b :=
      mkRData (CPU_ID a) b (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_MMSize (a : RData) b :=
      mkRData (CPU_ID a) (MM a) b (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_vmxinfo (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) b (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_CR3 (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) b (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ti (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) b (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_pg (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) b (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ikern (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) b (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ihost (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) b (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_HP (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) b
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_cid (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              b (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_multi_log (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) b (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_multi_oracle (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) b (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_lock (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) b (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_AC (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) b (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_AT (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) b (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ATC (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) b (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_nps (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) b (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_init (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) b
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_pperm (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              b (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_PT (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) b (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ptpool (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) b (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_idpde (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) b (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ipt (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) b (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_LAT (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) b (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_smspool (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) b (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_kctxt (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) b (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_sleeper (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) b
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_tcb (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              b (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_tdq (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) b (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_abtcb (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) b (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_abq (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) b (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_syncchpool (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) b (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_buffer (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) b (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_big_log (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) b (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_big_oracle (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) b (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_uctxt (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) b
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ept (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              b (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_vmcs (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) b (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_vmx (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) b (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ts (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) b (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_com1 (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) b (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_drv_serial (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) b (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_console_concrete (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) b (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_console (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) b (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_ioapic (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) b
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_lapic (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              b (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_tf (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) b (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_tf_reg (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) b (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_curr_intr_num (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) b (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_intr_flag (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) b (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_saved_intr_flags (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) b (in_intr a) (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_in_intr (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) b (i_dev_serial a) (kbd a)
              (kbd_drv a).

    Definition update_i_dev_serial (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) b (kbd a)
              (kbd_drv a).

    Definition update_kbd (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) b
              (kbd_drv a).

    Definition update_kbd_drv (a : RData) b :=
      mkRData (CPU_ID a) (MM a) (MMSize a) (vmxinfo a) (CR3 a) (ti a) (pg a) (ikern a) (ihost a) (HP a)
              (cid a) (multi_log a) (multi_oracle a) (lock a) (AC a) (AT a) (ATC a) (nps a) (init a)
              (pperm a) (PT a) (ptpool a) (idpde a) (ipt a) (LAT a) (smspool a) (kctxt a) (sleeper a)
              (tcb a) (tdq a) (abtcb a) (abq a) (syncchpool a) (buffer a) (big_log a) (big_oracle a) (uctxt a)
              (ept a) (vmcs a) (vmx a) (ts a) (com1 a) (drv_serial a) (console_concrete a) (console a) (ioapic a)
              (lapic a) (tf a) (tf_reg a) (curr_intr_num a) (intr_flag a) (saved_intr_flags a) (in_intr a) (i_dev_serial a) (kbd a)
              b.

  End UPDATE_FUNCTION.

  Context `{multi_oracle_ops: MultiOracleOps}.
  Context `{big_oracle_ops: BigOracleOps}.

  Fixpoint init_cal_cidpool (i: nat) (cidpool: ZMap.t Z) : ZMap.t Z :=
    match i with
      | O ⇒ ZMap.set 0 1 cidpool
      | S k ⇒ ZMap.set (Z.of_nat (S k)) (Z.of_nat (S k) + 1) (init_cal_cidpool k cidpool)
    end.

  Definition init_real_cidpool : ZMap.t Z :=
    init_cal_cidpool (Z.to_nat (TOTAL_CPU - 1)) (ZMap.init 0).

  Definition init_adt (o: MultiOraclePool) :=
    mkRData current_CPU_ID
            (ZMap.init MMUndef) 0 (ZMap.init 0)
            GLOBUndef init_trap_info false true true FlatMem.empty_flatmem
            (ZMap.init 0)
            (ZMap.init MultiUndef) o init_lock
            
            (ZMap.init Container_unused)
            (ZMap.init ATUndef) (ZMap.init ATCUndef) 0 false (ZMap.init PGUndef) (-1) (ZMap.init (ZMap.init PDEUndef))
            (ZMap.init (ZMap.init IDPTEUndef)) true (ZMap.init LATCUndef)
            (ZMap.init (ZMap.init SHRDUndef)) (ZMap.init (Pregmap.init Vundef)) init_sleeper
            (ZMap.init TCBUndef) (ZMap.init TDQUndef) (ZMap.init AbTCBUndef) (ZMap.init AbQUndef)
            
            
            
            
            (ZMap.init SyncChanUndef)
            page_buffer_init
            BigUndef
            big_oracle0
            (ZMap.init (ZMap.init Vundef)) (ZMap.init (ZMap.init EPML4EUndef))
            (ZMap.init (VMCSValid Vzero Vzero (ZMap.init Vundef))) (ZMap.init (ZMap.init Vundef)) 0 com1_init serial_drv_init
            console_init_concrete console_init_d ioapic_init_d lapic_init_d nil (Vint Int.zero) 256 true nil false false
            kbd_init kbd_drv_init.


End ABDATA.

the notation to update each field of the record
Notation "a {CPU_ID : b }" := (update_CPU_ID a b) (at level 1).
Notation "a {MM : b }" := (update_MM a b) (at level 1).
Notation "a {MMSize : b }" := (update_MMSize a b) (at level 1).
Notation "a {vmxinfo : b }" := (update_vmxinfo a b) (at level 1).
Notation "a {CR3 : b }" := (update_CR3 a b) (at level 1).
Notation "a {ti : b }" := (update_ti a b) (at level 1).
Notation "a {pg : b }" := (update_pg a b) (at level 1).
Notation "a {ikern : b }" := (update_ikern a b) (at level 1).
Notation "a {ihost : b }" := (update_ihost a b) (at level 1).
Notation "a {HP : b }" := (update_HP a b) (at level 1).
Notation "a {cid : b }" := (update_cid a b) (at level 1).
Notation "a {multi_log : b }" := (update_multi_log a b) (at level 1).
Notation "a {multi_oracle : b }" := (update_multi_oracle a b) (at level 1).
Notation "a {lock : b }" := (update_lock a b) (at level 1).
Notation "a {AC : b }" := (update_AC a b) (at level 1).
Notation "a {AT : b }" := (update_AT a b) (at level 1).
Notation "a {ATC : b }" := (update_ATC a b) (at level 1).
Notation "a {nps : b }" := (update_nps a b) (at level 1).
Notation "a {init : b }" := (update_init a b) (at level 1).
Notation "a {pperm : b }" := (update_pperm a b) (at level 1).
Notation "a {PT : b }" := (update_PT a b) (at level 1).
Notation "a {ptpool : b }" := (update_ptpool a b) (at level 1).
Notation "a {idpde : b }" := (update_idpde a b) (at level 1).
Notation "a {ipt : b }" := (update_ipt a b) (at level 1).
Notation "a {LAT : b }" := (update_LAT a b) (at level 1).
Notation "a {smspool : b }" := (update_smspool a b) (at level 1).
Notation "a {kctxt : b }" := (update_kctxt a b) (at level 1).
Notation "a {sleeper : b }" := (update_sleeper a b) (at level 1).
Notation "a {tcb : b }" := (update_tcb a b) (at level 1).
Notation "a {tdq : b }" := (update_tdq a b) (at level 1).
Notation "a {abtcb : b }" := (update_abtcb a b) (at level 1).
Notation "a {abq : b }" := (update_abq a b) (at level 1).
Notation "a {syncchpool : b }" := (update_syncchpool a b) (at level 1).
Notation "a {buffer : b }" := (update_buffer a b) (at level 1).
Notation "a {uctxt : b }" := (update_uctxt a b) (at level 1).
Notation "a {ept : b }" := (update_ept a b) (at level 1).
Notation "a {vmcs : b }" := (update_vmcs a b) (at level 1).
Notation "a {vmx : b }" := (update_vmx a b) (at level 1).
Notation "a {big_log : b }" := (update_big_log a b) (at level 1).
Notation "a {big_oracle : b }" := (update_big_oracle a b) (at level 1).

Notation "a ´{´ ´ts´ : x }" := (update_ts a x) (at level 1).
Notation "a ´{´ ´com1´ : x }" := (update_com1 a x) (at level 1).
Notation "a ´{´ ´drv_serial´ : x }" := (update_drv_serial a x) (at level 1).
Notation "a ´{´ ´console_concrete´ : x }" := (update_console_concrete a x) (at level 1).
Notation "a ´{´ ´console´ : x }" := (update_console a x) (at level 1).
Notation "a ´{´ ´ioapic´ : x }" := (update_ioapic a x) (at level 1).
Notation "a ´{´ ´lapic´ : x }" := (update_lapic a x) (at level 1).
Notation "a ´{´ ´tf´ : x }" := (update_tf a x) (at level 1).
Notation "a ´{´ ´tf_reg´ : x }" := (update_tf_reg a x) (at level 1).
Notation "a ´{´ ´curr_intr_num´ : x }" := (update_curr_intr_num a x) (at level 1).
Notation "a ´{´ ´intr_flag´ : x }" := (update_intr_flag a x) (at level 1).
Notation "a ´{´ ´saved_intr_flags´ : x }" := (update_saved_intr_flags a x) (at level 1).
Notation "a ´{´ ´in_intr´ : x }" := (update_in_intr a x) (at level 1).
Notation "a ´{´ ´i_dev_serial´ : x }" := (update_i_dev_serial a x) (at level 1).
Notation "a ´{´ ´kbd´ : x }" := (update_kbd a x) (at level 1).
Notation "a ´{´ ´kbd_drv´ : x }" := (update_kbd_drv a x) (at level 1).

Ltac unfold_RData :=
  try unfold update_CPU_ID; simpl;
  try unfold update_MM; simpl;
  try unfold update_MMSize; simpl;
  try unfold update_vmxinfo; simpl;
  try unfold update_CR3; simpl;
  try unfold update_ti; simpl;
  try unfold update_pg; simpl;
  try unfold update_ikern; simpl;
  try unfold update_ihost; simpl;
  try unfold update_HP; simpl;
  try unfold update_cid; simpl;
  try unfold update_multi_log; simpl;
  try unfold update_multi_oracle; simpl;
  try unfold update_big_log; simpl;
  try unfold update_big_oracle; simpl;
  try unfold update_lock; simpl;
  try unfold update_AC; simpl;
  try unfold update_AT; simpl;
  try unfold update_ATC; simpl;
  try unfold update_nps; simpl;
  try unfold update_init; simpl;
  try unfold update_pperm; simpl;
  try unfold update_PT; simpl;
  try unfold update_ptpool; simpl;
  try unfold update_idpde; simpl;
  try unfold update_ipt; simpl;
  try unfold update_LAT; simpl;
  try unfold update_smspool; simpl;
  try unfold update_kctxt; simpl;
  try unfold update_tcb; simpl;
  try unfold update_tdq; simpl;
  try unfold update_abtcb; simpl;
  try unfold update_abq; simpl;
  
  try unfold update_syncchpool; simpl;
  try unfold update_buffer; simpl;
  try unfold update_uctxt; simpl;
  try unfold update_ept; simpl;
  try unfold update_vmcs; simpl;
  try unfold update_vmx; simpl;
  try unfold update_ts; simpl;
  try unfold update_com1; simpl;
  try unfold update_drv_serial; simpl;
  try unfold update_console_concrete; simpl;
  try unfold update_console; simpl;
  try unfold update_ioapic; simpl;
  try unfold update_lapic; simpl;
  try unfold update_tf; simpl;
  try unfold update_curr_intr_num; simpl;
  try unfold update_intr_flag; simpl;
  try unfold update_saved_intr_flags; simpl;
  try unfold update_in_intr; simpl;
  try unfold update_i_dev_serial; simpl;
  try unfold update_kbd; simpl;
  try unfold update_kbd_drv; simpl.

Tactic Notation "unfold_RData_in" constr(T) :=
  match goal with
    | [T: _ |- _] ⇒
      try unfold update_CPU_ID in T; simpl in T;
      try unfold update_MM in T; simpl in T;
      try unfold update_MMSize in T; simpl in T;
      try unfold update_vmxinfo in T; simpl in T;
      try unfold update_CR3 in T; simpl in T;
      try unfold update_ti in T; simpl in T;
      try unfold update_pg in T; simpl in T;
      try unfold update_ikern in T; simpl in T;
      try unfold update_ihost in T; simpl in T;
      try unfold update_HP in T; simpl in T;
      try unfold update_cid in T; simpl in T;
      try unfold update_multi_log in T; simpl in T;
      try unfold update_multi_oracle in T; simpl in T;
      try unfold update_big_log in T; simpl in T;
      try unfold update_big_oracle in T; simpl in T;
      try unfold update_lock in T; simpl in T;
      try unfold update_AC in T; simpl in T;
      try unfold update_AT in T; simpl in T;
      try unfold update_ATC in T; simpl in T;
      try unfold update_nps in T; simpl in T;
      try unfold update_init in T; simpl in T;
      try unfold update_pperm in T; simpl in T;
      try unfold update_PT in T; simpl in T;
      try unfold update_ptpool in T; simpl in T;
      try unfold update_idpde in T; simpl in T;
      try unfold update_ipt in T; simpl in T;
      try unfold update_LAT in T; simpl in T;
      try unfold update_smspool in T; simpl in T;
      try unfold update_kctxt in T; simpl in T;
      try unfold update_tcb in T; simpl in T;
      try unfold update_tdq in T; simpl in T;
      try unfold update_abtcb in T; simpl in T;
      try unfold update_abq in T; simpl in T;
      
      try unfold update_syncchpool in T; simpl in T;
      try unfold update_buffer; simpl in T;
      try unfold update_uctxt in T; simpl in T;
      try unfold update_ept in T; simpl in T;
      try unfold update_vmcs in T; simpl in T;
      try unfold update_vmx in T; simpl in T;
      try unfold update_ts in T; simpl in T;
      try unfold update_com1 in T; simpl in T;
      try unfold update_drv_serial in T; simpl in T;
      try unfold update_console_concrete in T; simpl in T;
      try unfold update_console in T; simpl in T;
      try unfold update_ioapic in T; simpl in T;
      try unfold update_lapic in T; simpl in T;
      try unfold update_tf in T; simpl in T;
      try unfold update_curr_intr_num in T; simpl in T;
      try unfold update_intr_flag in T; simpl in T;
      try unfold update_saved_intr_flags in T; simpl in T;
      try unfold update_in_intr in T; simpl in T;
      try unfold update_i_dev_serial in T; simpl in T;
      try unfold update_kbd in T; simpl in T;
      try unfold update_kbd_drv; simpl in T
  end.

Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Base´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Base (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´SerialOn´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_SerialOn (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´SerialIrq´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_SerialIrq (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´RxIntEnable´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_RxIntEnable (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´TxBuf´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_TxBuf (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´RxBuf´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_RxBuf (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´DLAB´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_DLAB (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Baudrate´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Baudrate (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Databits´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Databits (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Stopbits´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Stopbits (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Parity´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Parity (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Fifo´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Fifo (s ((com1 (a)))) x))) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´s´ ´/´ ´Modem´ : x }"
  := (update_com1 a (update_s (com1 (a)) (update_Modem (s ((com1 (a)))) x))) (at level 1).

Notation "a ´{´ ´com1´ ´/´ ´s´ : x }" := (update_com1 a (update_s (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´l1´ : x }" := (update_com1 a (update_l1 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´l2´ : x }" := (update_com1 a (update_l2 (com1 (a)) x)) (at level 1).
Notation "a ´{´ ´com1´ ´/´ ´l3´ : x }" := (update_com1 a (update_l3 (com1 (a)) x)) (at level 1).

Notation "a ´{´ ´drv_serial´ ´/´ ´serial_exists´ : x }"
  := (update_drv_serial a (update_serial_exists (drv_serial (a)) x)) (at level 1).

Notation "a ´{´ ´console_concrete´ ´/´ ´cons_buf_concrete´ : x }"
  := (update_console_concrete a (update_cons_buf_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´console_concrete´ ´/´ ´rpos_concrete´ : x }"
  := (update_console_concrete a (update_rpos_concrete (console_concrete (a)) x)) (at level 1).
Notation "a ´{´ ´console_concrete´ ´/´ ´wpos_concrete´ : x }"
  := (update_console_concrete a (update_wpos_concrete (console_concrete (a)) x)) (at level 1).

Notation "a ´{´ ´console´ ´/´ ´cons_buf´ : x }" := (update_console a (update_cons_buf (console (a)) x)) (at level 1).
Notation "a ´{´ ´console´ ´/´ ´rpos´ : x }" := (update_console a (update_rpos (console (a)) x)) (at level 1).

Notation "a ´{´ ´ioapic´ ´/´ ´s´ : x }" := (update_ioapic a (update_s (ioapic (a)) x)) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicInit´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicInit (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´CurrentIrq´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_CurrentIrq (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicBase´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicBase (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicId´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicId (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicMaxIntr´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicMaxIntr (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicIrqs´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicIrqs (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicIrqs´ ´[´ n ´]´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicIrqs (s ((ioapic (a))))
                                                                (replace x n (IoApicIrqs (s (ioapic a))))))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicEnables´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicEnables (s ((ioapic (a)))) x))) (at level 1).
Notation "a ´{´ ´ioapic´ ´/´ ´s´ ´/´ ´IoApicEnables´ ´[´ n ´]´ : x }"
  := (update_ioapic a (update_s (ioapic (a)) (update_IoApicEnables (s ((ioapic (a))))
                                                                   (replace x n (IoApicEnables (s (ioapic a))))))) (at level 1).

Notation "a ´{´ ´lapic´ ´/´ ´s´ : x }" := (update_lapic a (update_s (lapic (a)) x)) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicEsr´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicEsr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicEoi´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicEoi (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicMaxLvt´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicMaxLvt (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicEnable´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicEnable (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicSpurious´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicSpurious (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicLint0Mask´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicLint0Mask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicLint1Mask´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicLint1Mask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicPcIntMask´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicPcIntMask (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicLdr´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicLdr (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicErrorIrq´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicErrorIrq (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicEsrClrPen´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicEsrClrPen (s ((lapic (a)))) x))) (at level 1).
Notation "a ´{´ ´lapic´ ´/´ ´s´ ´/´ ´LapicTpr´ : x }"
  := (update_lapic a (update_s (lapic (a)) (update_LapicTpr (s ((lapic (a)))) x))) (at level 1).

Notation "a ´{´ ´tf´ ´[´ n ´]´ ´/´ ´tf_regs´ : x }"
  := (update_tf a (replace (update_tf_regs (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´tf´ ´[´ n ´]´ ´/´ ´tf_trapno´ : x }"
  := (update_tf a (replace (update_tf_trapno (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´tf´ ´[´ n ´]´ ´/´ ´tf_err´ : x }"
  := (update_tf a (replace (update_tf_err (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).
Notation "a ´{´ ´tf´ ´[´ n ´]´ ´/´ ´tf_esp´ : x }"
  := (update_tf a (replace (update_tf_esp (nth n (tf (a)) tf_init_d) (x)) n (tf (a)))) (at level 1).

Notation "a ´{´ ´kbd´ ´/´ ´s´ ´/´ ´KbdIrq´ : x }"
  := (update_kbd a (update_s (kbd (a)) (update_KbdIrq (s ((kbd (a)))) x))) (at level 1).
Notation "a ´{´ ´kbd´ ´/´ ´s´ ´/´ ´KbdRxBuf´ : x }"
  := (update_kbd a (update_s (kbd (a)) (update_KbdRxBuf (s ((kbd (a)))) x))) (at level 1).

Notation "a ´{´ ´kbd_drv´ ´/´ ´shift_toggle´ : x }"
  := (update_kbd_drv a (update_shift_toggle (kbd_drv (a)) x)) (at level 1).
Notation "a ´{´ ´kbd_drv´ ´/´ ´kbd_buf´ : x }"
  := (update_kbd_drv a (update_kbd_buf (kbd_drv (a)) x)) (at level 1).
Notation "a ´{´ ´kbd_drv´ ´/´ ´kbd_buf_concrete´ : x }"
  := (update_kbd_drv a (update_kbd_buf_concrete (kbd_drv (a)) x)) (at level 1).
Notation "a ´{´ ´kbd_drv´ ´/´ ´kbd_rpos_concrete´ : x }"
  := (update_kbd_drv a (update_kbd_rpos_concrete (kbd_drv (a)) x)) (at level 1).
Notation "a ´{´ ´kbd_drv´ ´/´ ´kbd_wpos_concrete´ : x }"
  := (update_kbd_drv a (update_kbd_wpos_concrete (kbd_drv (a)) x)) (at level 1).

Section LOW_INV.

  Record low_level_invariant (n: block) (adt: RData) :=
    mkLowInv {
        CR2_INJECT: val_inject (Mem.flat_inj n) (snd (ti adt)) (snd (ti adt));
        CR2_Type: Val.has_type (snd (ti adt)) AST.Tint;
        kctxt_INJECT: kctxt_inject_neutral (kctxt adt) n;
        uctxt_INJECT: uctxt_inject_neutral (uctxt adt) n;
        VMCS_INJECT: VMCSPool_inject_neutral (vmcs adt) n;
        VMX_INJECT: VMXPool_inject_neutral (vmx adt) n;
        tf_INJECT: tfs_inject_neutral (tf adt) n
      }.

  Lemma low_level_invariant_incr:
    ∀ (n n´: positive) a,
      (n ≤ n´)%positive →
      low_level_invariant n a →
      low_level_invariant n´ a.
  Proof.
    inversion 2; subst.
    intros; constructor; trivial.
    - eapply val_inject_incr; [|eauto].
      apply flat_inj_inject_incr; trivial.
    - intros until 2. exploit kctxt_INJECT0; eauto.
      intros [? ?]. split; try assumption.
      eapply val_inject_incr; try eassumption.
      apply flat_inj_inject_incr; trivial.
    - intros until 2. exploit uctxt_INJECT0; eauto.
      intros [? ?]. split; try assumption.
      eapply val_inject_incr; try eassumption.
      apply flat_inj_inject_incr; trivial.
    - unfold VMCSPool_inject_neutral in ×.
      intros.
      specialize (VMCS_INJECT0 vmid vmcs0 H1 H2).
      inv VMCS_INJECT0. constructor; intros.
      destruct (H3 ofs) as (? & ?).
      split; try assumption.
      eapply val_inject_incr; try eassumption.
      apply flat_inj_inject_incr; trivial.
    - unfold VMXPool_inject_neutral in ×.
      intros.
      specialize (VMX_INJECT0 vmid vmx0 H1 H2).
      inv VMX_INJECT0. constructor; intros.
      destruct (H3 ofs) as (? & ?).
      split; try assumption.
      eapply val_inject_incr; try eassumption.
      apply flat_inj_inject_incr; trivial.
    - unfold tfs_inject_neutral in ×.
      induction (tf a).
      constructor.
      inv tf_INJECT0.
      constructor.
      unfold tf_inject_neutral in ×.
      intros.
      specialize (H3 r).
      destruct H3.
      split; try assumption.
      eapply val_inject_incr; try eassumption.
      apply flat_inj_inject_incr; trivial.
      eapply IHt; auto.
  Qed.

  Context `{multi_oracle_ops: MultiOracleOps}.
  Context `{big_oracle_ops: BigOracleOps}.

  Lemma empty_data_low_level_invariant:
    ∀ o n, low_level_invariant n (init_adt o).
  Proof.
    constructor; simpl; auto.
    - econstructor.
    - intros until 2. rewrite ZMap.gi. rewrite Pregmap.gi.
      split; constructor.
    - intros until 2. repeat rewrite ZMap.gi.
      split; constructor.
    - unfold VMCSPool_inject_neutral.
      intros.
      rewrite ZMap.gi in H0; subst.
      constructor. intros. subst v. repeat rewrite ZMap.gi.
      split; constructor.
    - unfold VMXPool_inject_neutral.
      intros.
      rewrite ZMap.gi in H0; subst.
      constructor. intros. subst v. repeat rewrite ZMap.gi.
      split; constructor.
    - constructor.
  Qed.


End LOW_INV.

Section InstanceT.

  Context `{data : CompatData RData}.
  Context `{data0 : CompatData RData}.

  Notation HDATAOps := (cdata (cdata_ops := data_ops) RData).
  Notation LDATAOps := (cdata (cdata_ops := data_ops0) RData).

  Context `{Hstencil: Stencil}.
  Context `{Hmem: Mem.MemoryModel}.

  Context `{rel_prf: CompatRel _ (memory_model_ops:= memory_model_ops) _
                               (stencil_ops:= stencil_ops) HDATAOps LDATAOps}.


  Section CLASS_IFLAGS.

    Record impl_iflags d1 d2 :=
      {
        ikern_eq : ikern d1 = ikern d2;

        ihost_eq: ihost d1 = ihost d2;

        pg_eq : pg d1 = pg d2
      }.

    Class relate_impl_iflags :=
      {
        relate_impl_iflags_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          impl_iflags d1 d2;

        
        relate_impl_ikern_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {ikern: b} d2 {ikern: b};

        relate_impl_ihost_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {ihost: b} d2 {ihost: b};

        relate_impl_pg_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {pg: b} d2 {pg: b}

      }.

    Class match_impl_iflags :=
      {
        match_impl_ikern_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {ikern: b} m f;

        match_impl_ihost_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {ihost: b} m f;

        match_impl_pg_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {pg: b} m f

      }.

  End CLASS_IFLAGS.

  Section CLASS_MM.

    Class relate_impl_MM :=
      {
        
        relate_impl_MM_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {MM: b} d2 {MM: b};

        relate_impl_MMSize_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {MMSize: b} d2 {MMSize: b}

      }.

    Class relate_impl_MM´ :=
      {
        relate_impl_MM_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (MM d1) = (MM d2);

        relate_impl_MMSize_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (MMSize d1) = (MMSize d2)
      }.

    Class match_impl_MM :=
      {
        match_impl_MM_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {MM: b} m f;

        match_impl_MMSize_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {MMSize: b} m f

      }.

  End CLASS_MM.

  Section CLASS_vmxinfo.

    Class relate_impl_vmxinfo :=
      {
        relate_impl_vmxinfo_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          vmxinfo d1 = vmxinfo d2;

        relate_impl_vmxinfo_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {vmxinfo: b} d2 {vmxinfo: b}
      }.

    Class match_impl_vmxinfo :=
      {
        match_impl_vmxinfo_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {vmxinfo: b} m f
      }.

  End CLASS_vmxinfo.

  Section CLASS_TI.

    Record impl_trapinfo f d1 d2 :=
      {
        ti_fst_eq : fst (ti d1) = fst (ti d2);

        ti_snd_eq: val_inject f (snd (ti d1)) (snd (ti d2))
      }.

    Class relate_impl_trapinfo :=
      {
        relate_impl_trapinfo_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          impl_trapinfo ι d1 d2
      }.

  End CLASS_TI.

  Section CLASS_HP.

    Class relate_impl_HP :=
      {
        relate_impl_HP_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          FlatMem.flatmem_inj (HP d1) (HP d2);

        
        relate_impl_HP_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b b´,
            FlatMem.flatmem_inj b b´ →
            relate_AbData s ι d1 {HP: b} d2 {HP: b´}
      }.

    Class match_impl_HP :=
      {
        match_impl_HP_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {HP: b} m f
      }.

  End CLASS_HP.

  Section CLASS_HP´.

    Class relate_impl_HP´ :=
      {
        relate_impl_HP´_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          FlatMem.flatmem_inj (HP d1) (HP d2)
      }.

  End CLASS_HP´.

  Section CLASS_NPS.

    Class relate_impl_nps :=
      {
        relate_impl_nps_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (nps d1) = (nps d2);

        
        relate_impl_nps_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {nps: b} d2 {nps: b}
      }.

    Class match_impl_nps :=
      {
        match_impl_nps_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {nps: b} m f
      }.

  End CLASS_NPS.

  Section CLASS_INIT.

    Class relate_impl_init :=
      {
        relate_impl_init_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (init d1) = (init d2);

        
        relate_impl_init_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {init: b} d2 {init: b}
      }.

    Class match_impl_init :=
      {
        match_impl_init_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {init: b} m f
      }.

  End CLASS_INIT.

  Section CLASS_AC.

    Class relate_impl_AC :=
      {
        relate_impl_AC_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          AC d1 = AC d2;

        relate_impl_AC_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {AC: b} d2 {AC: b}
      }.

    Class match_impl_AC :=
      {
        match_impl_AC_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {AC: b} m f
      }.

  End CLASS_AC.

  Section CLASS_AT.

    Class relate_impl_AT :=
      {
        relate_impl_AT_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (AT d1) = (AT d2);

        
        relate_impl_AT_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {AT: b} d2 {AT: b}
      }.

    Class match_impl_AT :=
      {
        match_impl_AT_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {AT: b} m f
      }.

  End CLASS_AT.

  Section CLASS_ATC.

    Class relate_impl_ATC :=
      {
        relate_impl_ATC_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (ATC d1) = (ATC d2);

        
        relate_impl_ATC_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {ATC: b} d2 {ATC: b}
      }.

    Class match_impl_ATC :=
      {
        match_impl_ATC_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {ATC: b} m f
      }.

  End CLASS_ATC.

  Section CLASS_CR3.

    Class relate_impl_CR3 :=
      {
        relate_impl_CR3_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (CR3 d1) = (CR3 d2);

        
        relate_impl_CR3_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {CR3: b} d2 {CR3: b}

      }.

    Class match_impl_CR3 :=
      {
        match_impl_CR3_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {CR3: b} m f
      }.

  End CLASS_CR3.

  Section CLASS_PPERM.

    Class relate_impl_pperm :=
      {
        relate_impl_pperm_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          pperm d1 = pperm d2;

        
        relate_impl_pperm_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {pperm: b} d2 {pperm: b}

      }.

    Class match_impl_pperm :=
      {
        match_impl_pperm_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {pperm: b} m f
      }.

  End CLASS_PPERM.

  Section CLASS_IPT.

    Class relate_impl_ipt :=
      {
        relate_impl_ipt_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ipt d1 = ipt d2;

        
        relate_impl_ipt_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {ipt: b} d2 {ipt: b}

      }.

    Class match_impl_ipt :=
      {
        match_impl_ipt_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {ipt: b} m f
      }.

  End CLASS_IPT.

  Section CLASS_syncchpool.

    Class relate_impl_syncchpool :=
      {
        relate_impl_syncchpool_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (syncchpool d1) = (syncchpool d2);

        relate_impl_syncchpool_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {syncchpool: b} d2 {syncchpool: b}
      }.

    Class match_impl_syncchpool :=
      {
        match_impl_syncchpool_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {syncchpool: b} m f
      }.
  End CLASS_syncchpool.


  Section CLASS_PTPOOL.

    Class relate_impl_ptpool :=
      {
        relate_impl_ptpool_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ptpool d1 = ptpool d2;

        
        relate_impl_ptpool_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {ptpool: b} d2 {ptpool: b}
      }.

    Class match_impl_ptpool :=
      {
        match_impl_ptpool_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {ptpool: b} m f
      }.

  End CLASS_PTPOOL.

  Section CLASS_PT.

    Class relate_impl_PT :=
      {
        relate_impl_PT_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          PT d1 = PT d2;

        
        relate_impl_PT_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {PT: b} d2 {PT: b}

      }.

    Class match_impl_PT :=
      {
        match_impl_PT_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {PT: b} m f
      }.

  End CLASS_PT.

  Section CLASS_idpde.

    Class relate_impl_idpde :=
      {
        relate_impl_idpde_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          idpde d1 = idpde d2;

        
        relate_impl_idpde_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {idpde: b} d2 {idpde: b}

      }.

    Class match_impl_idpde :=
      {
        match_impl_idpde_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {idpde: b} m f
      }.

  End CLASS_idpde.

  Section CLASS_LAT.

    Class relate_impl_LAT :=
      {
        relate_impl_LAT_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (LAT d1) = (LAT d2);

        
        relate_impl_LAT_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {LAT: b} d2 {LAT: b}
      }.

    Class match_impl_LAT :=
      {
        match_impl_LAT_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {LAT: b} m f
      }.

  End CLASS_LAT.

  Section CLASS_smspool.

    Class relate_impl_smspool :=
      {
        relate_impl_smspool_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (smspool d1) = (smspool d2);

        
        relate_impl_smspool_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {smspool: b} d2 {smspool: b}
      }.

    Class match_impl_smspool :=
      {
        match_impl_smspool_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {smspool: b} m f
      }.

  End CLASS_smspool.

  Section CLASS_kctxt.

    Class relate_impl_kctxt :=
      {
        relate_impl_kctxt_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          kctxt_inj ι num_proc (kctxt d1) (kctxt d2);

        
        relate_impl_kctxt_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b1 b2,
            kctxt_inj ι num_proc b1 b2 →
            relate_AbData s ι d1 {kctxt: b1} d2 {kctxt: b2}
      }.

    Class match_impl_kctxt :=
      {
        match_impl_kctxt_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {kctxt: b} m f
      }.

  End CLASS_kctxt.

  Section CLASS_tcb.

    Class relate_impl_tcb :=
      {
        relate_impl_tcb_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (tcb d1) = (tcb d2);

        
        relate_impl_tcb_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {tcb: b} d2 {tcb: b}
      }.

    Class match_impl_tcb :=
      {
        match_impl_tcb_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {tcb: b} m f
      }.

  End CLASS_tcb.

  Section CLASS_tdq.

    Class relate_impl_tdq :=
      {
        relate_impl_tdq_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (tdq d1) = (tdq d2);

        
        relate_impl_tdq_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {tdq: b} d2 {tdq: b}
      }.

    Class match_impl_tdq :=
      {
        match_impl_tdq_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {tdq: b} m f
      }.

  End CLASS_tdq.

  Section CLASS_abtcb.

    Class relate_impl_abtcb :=
      {
        relate_impl_abtcb_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (abtcb d1) = (abtcb d2);

        
        relate_impl_abtcb_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {abtcb: b} d2 {abtcb: b}
      }.

    Class match_impl_abtcb :=
      {
        match_impl_abtcb_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {abtcb: b} m f
      }.

  End CLASS_abtcb.

  Section CLASS_abq.

    Class relate_impl_abq :=
      {
        relate_impl_abq_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (abq d1) = (abq d2);

        
        relate_impl_abq_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {abq: b} d2 {abq: b}
      }.

    Class match_impl_abq :=
      {
        match_impl_abq_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {abq: b} m f
      }.

  End CLASS_abq.

  Section CLASS_cid.

    Class relate_impl_cid :=
      {
        relate_impl_cid_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (cid d1) = (cid d2);

        
        relate_impl_cid_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {cid: b} d2 {cid: b}
      }.

    Class match_impl_cid :=
      {
        match_impl_cid_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {cid: b} m f
      }.

  End CLASS_cid.


  Section CLASS_uctxt.

    Class relate_impl_uctxt :=
      {
        relate_impl_uctxt_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          uctxt_inj ι (uctxt d1) (uctxt d2);

        
        relate_impl_uctxt_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b1 b2,
            uctxt_inj ι b1 b2 →
            relate_AbData s ι d1 {uctxt: b1} d2 {uctxt: b2}
      }.

    Class match_impl_uctxt :=
      {
        match_impl_uctxt_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {uctxt: b} m f
      }.

  End CLASS_uctxt.

  Section CLASS_ept.

    Class relate_impl_ept :=
      {
        relate_impl_ept_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          (ept d1) = (ept d2);

        
        relate_impl_ept_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b,
            relate_AbData s ι d1 {ept: b} d2 {ept: b}
      }.

    Class match_impl_ept :=
      {
        match_impl_ept_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {ept: b} m f
      }.

  End CLASS_ept.

  Section CLASS_vmcs.

    Class relate_impl_vmcs :=
      {
        relate_impl_vmcs_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          VMCSPool_inj ι (vmcs d1) (vmcs d2);

        
        relate_impl_vmcs_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b b´,
            VMCSPool_inj ι b b´ →
            relate_AbData s ι d1 {vmcs: b} d2 {vmcs: b´}
      }.

    Class match_impl_vmcs :=
      {
        match_impl_vmcs_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {vmcs: b} m f
      }.

  End CLASS_vmcs.

  Section CLASS_vmx.

    Class relate_impl_vmx :=
      {
        relate_impl_vmx_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          VMXPool_inj ι (vmx d1) (vmx d2);

        
        relate_impl_vmx_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b b´,
            VMXPool_inj ι b b´ →
            relate_AbData s ι d1 {vmx: b} d2 {vmx: b´}
      }.

    Class match_impl_vmx :=
      {
        match_impl_vmx_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {vmx: b} m f
      }.

  End CLASS_vmx.

  Section CLASS_CPU_ID.

    Class relate_impl_CPU_ID :=
      {
        relate_impl_CPU_ID_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          CPU_ID d1 = CPU_ID d2;

        relate_impl_CPU_ID_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {CPU_ID: b} d2 {CPU_ID: b}
      }.

    Class match_impl_CPU_ID :=
      {
        match_impl_CPU_ID_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {CPU_ID: b} m f
      }.

  End CLASS_CPU_ID.

  Section CLASS_multi_log.

    Class relate_impl_multi_log :=
      {
        relate_impl_multi_log_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          multi_log d1 = multi_log d2;

        relate_impl_multi_log_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {multi_log: b} d2 {multi_log: b}
      }.

    Class match_impl_multi_log :=
      {
        match_impl_multi_log_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {multi_log: b} m f
      }.

    Class match_impl_multi_log_one R :=
      {
        match_impl_multi_log_one_update ι d m f z l l´:
          match_AbData ι d m f →
          ZMap.get z (multi_log d) = MultiDef l →
          R l l´ →
          match_AbData ι d {multi_log:ZMap.set z (MultiDef l´) (multi_log d)} m f
      }.

    Global Instance match_impl_multi_log_one_match_impl_multi_log R:
      match_impl_multi_log →
      match_impl_multi_log_one R.
    Proof.
      destruct 1;
      constructor;
      eauto.
    Qed.

  End CLASS_multi_log.

  Section CLASS_multi_oracle.

    Class relate_impl_multi_oracle :=
      {
        relate_impl_multi_oracle_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          multi_oracle d1 = multi_oracle d2;

        relate_impl_multi_oracle_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {multi_oracle: b} d2 {multi_oracle: b}
      }.

    Class match_impl_multi_oracle :=
      {
        match_impl_multi_oracle_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {multi_oracle: b} m f
      }.

  End CLASS_multi_oracle.

  Section CLASS_lock.

    Class relate_impl_lock :=
      {
        relate_impl_lock_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          lock d1 = lock d2;

        relate_impl_lock_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {lock: b} d2 {lock: b}
      }.

    Class match_impl_lock :=
      {
        match_impl_lock_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {lock: b} m f
      }.

  End CLASS_lock.


  Section CLASS_ts.

    Class relate_impl_ts :=
      {
        relate_impl_ts_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ts d1 = ts d2;

        relate_impl_ts_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {ts: b} d2 {ts: b}
      }.

    Class match_impl_ts :=
      {
        match_impl_ts_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {ts: b} m f
      }.

  End CLASS_ts.

  Section CLASS_com1.

    Class relate_impl_com1 :=
      {
        relate_impl_com1_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          com1 d1 = com1 d2;

        relate_impl_com1_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {com1: b} d2 {com1: b}
      }.

    Class match_impl_com1 :=
      {
        match_impl_com1_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {com1: b} m f
      }.

  End CLASS_com1.

  Section CLASS_drv_serial.

    Class relate_impl_drv_serial :=
      {
        relate_impl_drv_serial_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          drv_serial d1 = drv_serial d2;

        relate_impl_drv_serial_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {drv_serial: b} d2 {drv_serial: b}
      }.

    Class match_impl_drv_serial :=
      {
        match_impl_drv_serial_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {drv_serial: b} m f
      }.

  End CLASS_drv_serial.

  Section CLASS_console_concrete.

    Class relate_impl_console_concrete :=
      {
        relate_impl_console_concrete_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          console_concrete d1 = console_concrete d2;

        relate_impl_console_concrete_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {console_concrete: b} d2 {console_concrete: b}
      }.

    Class match_impl_console_concrete :=
      {
        match_impl_console_concrete_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {console_concrete: b} m f
      }.

  End CLASS_console_concrete.

  Section CLASS_console.

    Class relate_impl_console :=
      {
        relate_impl_console_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          console d1 = console d2;

        relate_impl_console_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {console: b} d2 {console: b}
      }.

    Class match_impl_console :=
      {
        match_impl_console_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {console: b} m f
      }.

  End CLASS_console.

  Section CLASS_ioapic.

    Class relate_impl_ioapic :=
      {
        relate_impl_ioapic_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ioapic d1 = ioapic d2;

        relate_impl_ioapic_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {ioapic: b} d2 {ioapic: b}
      }.

    Class match_impl_ioapic :=
      {
        match_impl_ioapic_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {ioapic: b} m f
      }.

  End CLASS_ioapic.

  Section CLASS_lapic.

    Class relate_impl_lapic :=
      {
        relate_impl_lapic_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          lapic d1 = lapic d2;

        relate_impl_lapic_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {lapic: b} d2 {lapic: b}
      }.

    Class match_impl_lapic :=
      {
        match_impl_lapic_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {lapic: b} m f
      }.

  End CLASS_lapic.

  Section CLASS_tf.

    Class relate_impl_tf :=
      {
        relate_impl_tf_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          tfs_inj ι (tf d1) (tf d2);

        
        relate_impl_tf_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b1 b2,
            tfs_inj ι b1 b2 →
            relate_AbData s ι d1 {tf: b1} d2 {tf: b2}
      }.

    Class match_impl_tf :=
      {
        match_impl_tf_update ι d m f:
          match_AbData ι d m f →
          ∀ b,
            match_AbData ι d {tf: b} m f
      }.

  End CLASS_tf.

  Section CLASS_tf´.

    Class relate_impl_tf´ :=
      {
        relate_impl_tf´_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          tf d1 = tf d2;

        relate_impl_tf´_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {tf: b} d2 {tf: b}
      }.

    Class match_impl_tf´ :=
      {
        match_impl_tf´_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {tf: b} m f
      }.

  End CLASS_tf´.

  Section CLASS_curr_intr_num.

    Class relate_impl_curr_intr_num :=
      {
        relate_impl_curr_intr_num_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          curr_intr_num d1 = curr_intr_num d2;

        relate_impl_curr_intr_num_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {curr_intr_num: b} d2 {curr_intr_num: b}
      }.

    Class match_impl_curr_intr_num :=
      {
        match_impl_curr_intr_num_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {curr_intr_num: b} m f
      }.

  End CLASS_curr_intr_num.

  Section CLASS_intr_flag.

    Class relate_impl_intr_flag :=
      {
        relate_impl_intr_flag_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          intr_flag d1 = intr_flag d2;

        relate_impl_intr_flag_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {intr_flag: b} d2 {intr_flag: b}
      }.

    Class match_impl_intr_flag :=
      {
        match_impl_intr_flag_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {intr_flag: b} m f
      }.
  End CLASS_intr_flag.

  Section CLASS_saved_intr_flags.

    Class relate_impl_saved_intr_flags :=
      {
        relate_impl_saved_intr_flags_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          saved_intr_flags d1 = saved_intr_flags d2;

        relate_impl_saved_intr_flags_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {saved_intr_flags: b} d2 {saved_intr_flags: b}
      }.

    Class match_impl_saved_intr_flags :=
      {
        match_impl_saved_intr_flags_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {saved_intr_flags: b} m f
      }.
  End CLASS_saved_intr_flags.


  Section CLASS_in_intr.

    Class relate_impl_in_intr :=
      {
        relate_impl_in_intr_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          in_intr d1 = in_intr d2;

        relate_impl_in_intr_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {in_intr: b} d2 {in_intr: b}
      }.

    Class match_impl_in_intr :=
      {
        match_impl_in_intr_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {in_intr: b} m f
      }.

  End CLASS_in_intr.

  Section CLASS_i_dev_serial.

    Class relate_impl_i_dev_serial :=
      {
        relate_impl_i_dev_serial_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          i_dev_serial d1 = i_dev_serial d2;

        relate_impl_i_dev_serial_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {i_dev_serial: b} d2 {i_dev_serial: b}
      }.

    Class match_impl_i_dev_serial :=
      {
        match_impl_i_dev_serial_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {i_dev_serial: b} m f
      }.

  End CLASS_i_dev_serial.

  Section CLASS_kbd.

    Class relate_impl_kbd :=
      {
        relate_impl_kbd_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          kbd d1 = kbd d2;

        relate_impl_kbd_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {kbd: b} d2 {kbd: b}
      }.

    Class match_impl_kbd :=
      {
        match_impl_kbd_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {kbd: b} m f
      }.

  End CLASS_kbd.

  Section CLASS_kbd_drv.

    Class relate_impl_kbd_drv :=
      {
        relate_impl_kbd_drv_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          kbd_drv d1 = kbd_drv d2;

        relate_impl_kbd_drv_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {kbd_drv: b} d2 {kbd_drv: b}
      }.

    Class match_impl_kbd_drv :=
      {
        match_impl_kbd_drv_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {kbd_drv: b} m f
      }.

  End CLASS_kbd_drv.

  Section CLASS_sleeper.

    Class relate_impl_sleeper :=
      {
        relate_impl_sleeper_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          sleeper d1 = sleeper d2;

        relate_impl_sleeper_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {sleeper: b} d2 {sleeper: b}
      }.

    Class match_impl_sleeper :=
      {
        match_impl_sleeper_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {sleeper: b} m f
      }.

  End CLASS_sleeper.

  Section CLASS_buffer.

    Class relate_impl_buffer :=
      {
        relate_impl_buffer_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          buffer d1 = buffer d2;

        relate_impl_buffer_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {buffer: b} d2 {buffer: b}
      }.

    Class match_impl_buffer :=
      {
        match_impl_buffer_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {buffer: b} m f
      }.

  End CLASS_buffer.

  Section CLASS_big_log.

    Class relate_impl_big_log :=
      {
        relate_impl_big_log_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          big_log d1 = big_log d2;

        relate_impl_big_log_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {big_log: b} d2 {big_log: b}
      }.

    Class match_impl_big_log :=
      {
        match_impl_big_log_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {big_log: b} m f
      }.

  End CLASS_big_log.

  Section CLASS_big_oracle.

    Class relate_impl_big_oracle :=
      {
        relate_impl_big_oracle_eq s ι d1 d2:
          relate_AbData s ι d1 d2 →
          big_oracle d1 = big_oracle d2;

        relate_impl_big_oracle_update s ι d1 d2:
          relate_AbData s ι d1 d2 →
          ∀ b, relate_AbData s ι d1 {big_oracle: b} d2 {big_oracle: b}
      }.

    Class match_impl_big_oracle :=
      {
        match_impl_big_oracle_update ι d m f:
          match_AbData ι d m f →
          ∀ b, match_AbData ι d {big_oracle: b} m f
      }.

  End CLASS_big_oracle.

  Class low_level_invariant_impl :=
    {
      low_level_invariant_impl_eq n d:
        CompatData.low_level_invariant n d →
        low_level_invariant n d
    }.

  Class high_level_invariant_impl_AbQCorrect_range :=
    {
      high_level_invariant_impl_AbQCorrect_range_eq d:
        CompatData.high_level_invariant d →
        pg d = true → AbQCorrect_range (abq d)
    }.

  Class high_level_invariant_impl_CPU_ID_range :=
    {
      high_level_invariant_impl_CPU_ID_range_eq d:
        CompatData.high_level_invariant d →
        (0 ≤ (CPU_ID d) < TOTAL_CPU)%Z
    }.

End InstanceT.

Ltac relate_match_instance_tac:=
  split; inversion 1; eauto 2; try econstructor; eauto 2.

Hint Extern 1 relate_impl_CPU_ID ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_CPU_ID ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_iflags ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_iflags ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_MM ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_MM´ ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_MM ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_trapinfo ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_HP ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_HP´ ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_HP ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_nps ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_nps ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_vmxinfo ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_vmxinfo ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_init ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_init ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_AC ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_AC ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_AT ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_AT ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_ATC ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_ATC ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_CR3 ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_CR3 ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_pperm ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_pperm ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_ipt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_ipt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_ptpool ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_ptpool ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_PT ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_PT ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_idpde ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_idpde ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_LAT ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_LAT ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_smspool ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_smspool ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_kctxt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_kctxt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_tcb ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_tcb ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_tdq ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_tdq ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_abtcb ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_abtcb ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_abq ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_abq ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_cid ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_cid ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_syncchpool ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_syncchpool ⇒
(relate_match_instance_tac): typeclass_instances.


Hint Extern 1 relate_impl_uctxt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_uctxt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_uctxt ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_ept ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_ept ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_vmcs ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_vmcs ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_vmx ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_vmx ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_ts ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_ts ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_com1 ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_com1 ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_drv_serial ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_drv_serial ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_console_concrete ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_console_concrete ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_console ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_console ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_ioapic ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_ioapic ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_lapic ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_lapic ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_tf ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_tf ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_tf´ ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_tf´ ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_curr_intr_num ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_curr_intr_num ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_intr_flag ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_intr_flag ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_saved_intr_flags ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_saved_intr_flags ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_in_intr ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_in_intr ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_i_dev_serial ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_i_dev_serial ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_kbd ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_kbd ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_kbd_drv ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_kbd_drv ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 low_level_invariant_impl ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 high_level_invariant_impl_AbQCorrect_range ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_multi_oracle ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_multi_oracle ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_multi_log ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_multi_log ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_big_log ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_big_log ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_big_oracle ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_big_oracle ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_lock ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_lock ⇒
(relate_match_instance_tac): typeclass_instances.


Hint Extern 1 relate_impl_sleeper ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_sleeper ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 relate_impl_buffer ⇒
(relate_match_instance_tac): typeclass_instances.

Hint Extern 1 match_impl_buffer ⇒
(relate_match_instance_tac): typeclass_instances.