Library mcertikos.layerlib.DeviceStateDataType
This file provide some data types that will be used in the layer definitions and refinement proofs
Require Import Coqlib.
Require Import Constant.
Require Import Values.
Require Import List.
Require Export AuxFunctions.
Require Import Maps.
Require Import Memory.
Section Device.
Section AbstractDevice.
Set Implicit Arguments.
Variable T: Type.
Record DeviceData :=
mkDevData {
s: T;
l1: Z;
l2: Z;
l3: Z
}.
Function update_s (a: DeviceData) x :=
mkDevData x (l1 a) (l2 a) (l3 a).
Function update_l1 (a: DeviceData) x :=
mkDevData (s a) x (l2 a) (l3 a).
Function update_l2 (a: DeviceData) x :=
mkDevData (s a) (l1 a) x (l3 a).
Function update_l3 (a: DeviceData) x :=
mkDevData (s a) (l1 a) (l2 a) x.
Inductive DeviceOp :=
| OpInput (addr: Z)
| OpOutput (addr value: Z).
Record Null :=
mkNull {}.
End AbstractDevice.
Inductive ParityType := pOdd | pEven | pHigh | pLow | pNone.
Section SerialDevice.
Record SerialState :=
mkSerialState {
Base: Z;
SerialOn: bool;
SerialIrq: bool;
RxIntEnable: bool;
TxBuf: list Z;
RxBuf: list Z;
DLAB: bool;
Baudrate: Z;
Databits: Z;
Stopbits: Z;
Parity: ParityType;
Fifo: Z;
Modem: Z
}.
Function update_Base (a: SerialState) x :=
mkSerialState x (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_SerialOn (a: SerialState) x :=
mkSerialState (Base a) x (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_SerialIrq (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) x (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_RxIntEnable (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) x (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_TxBuf (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) x (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_RxBuf (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) x
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_DLAB (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
x (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_Baudrate (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) x (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_Databits (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) x (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_Stopbits (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) x (Parity a) (Fifo a) (Modem a)
.
Function update_Parity (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) x (Fifo a) (Modem a)
.
Function update_Fifo (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) x (Modem a)
.
Function update_Modem (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) x
.
Definition SerialData := (DeviceData SerialState).
Definition mkSerialData (s: SerialState) :=
mkDevData s 0 0 0.
Definition com1_init : SerialData :=
mkSerialData
(mkSerialState PortCom1Base true false false nil nil false 0 0 0 pNone
0 0).
End SerialDevice.
Section SerialDriver.
Record SerialDriver :=
mkSerialDriver {
serial_exists: Z
}.
Function update_serial_exists (a: SerialDriver) x :=
mkSerialDriver x.
Definition serial_drv_init: SerialDriver :=
mkSerialDriver 0.
End SerialDriver.
Section ConsoleDriverConcrete.
Inductive ConsoleBufVal :=
| BufValUndef
| BufVal (val: Z).
Record ConsoleDriverConcrete :=
mkConsoleDrvierConcrete {
cons_buf_concrete: ZMap.t ConsoleBufVal;
rpos_concrete: Z;
wpos_concrete: Z
}.
Function update_cons_buf_concrete (a: ConsoleDriverConcrete) x :=
mkConsoleDrvierConcrete x (rpos_concrete a) (wpos_concrete a).
Function update_rpos_concrete (a: ConsoleDriverConcrete) x :=
mkConsoleDrvierConcrete (cons_buf_concrete a) x (wpos_concrete a).
Function update_wpos_concrete (a: ConsoleDriverConcrete) x :=
mkConsoleDrvierConcrete (cons_buf_concrete a) (rpos_concrete a) x.
Definition console_init_concrete: ConsoleDriverConcrete :=
mkConsoleDrvierConcrete (ZMap.init BufValUndef) 0 0.
Notation "a ´{´ ´cons_buf_concrete´ : x }" := (update_cons_buf_concrete a x) (at level 1).
Notation "a ´{´ ´rpos_concrete´ : x }" := (update_rpos_concrete a x) (at level 1).
Notation "a ´{´ ´wpos_concrete´ : x }" := (update_wpos_concrete a x) (at level 1).
Import List.ListNotations.
Function handle_cons_buf_write_concrete (s: ConsoleDriverConcrete) (c: Z) : ConsoleDriverConcrete :=
let buf := cons_buf_concrete s in
let wpos := wpos_concrete s in
s {cons_buf_concrete: ZMap.set wpos (BufVal c) buf} {wpos_concrete: (wpos + 1) mod CONSOLE_BUFFER_SIZE}.
End ConsoleDriverConcrete.
Section ConsoleDriver.
Record ConsoleDriver :=
mkConsoleDrvier {
cons_buf: list Z;
rpos: Z
}.
Function update_cons_buf (a: ConsoleDriver) x :=
mkConsoleDrvier x (rpos a).
Function update_rpos (a: ConsoleDriver) x :=
mkConsoleDrvier (cons_buf a) x.
Definition console_init_d: ConsoleDriver :=
mkConsoleDrvier nil 0.
Notation "a ´{´ ´cons_buf´ : x }" := (update_cons_buf a x) (at level 1).
Notation "a ´{´ ´rpos´ : x }" := (update_rpos a x) (at level 1).
Import List.ListNotations.
Function handle_cons_buf_write (s: ConsoleDriver) (c: Z) : ConsoleDriver :=
let b := cons_buf s in
if zlt (Zlength b) (CONSOLE_BUFFER_SIZE - 1)
then
s {cons_buf: (b ++ [c])}
else
s {cons_buf: skipn 1 (b ++ [c])} {rpos: ((rpos s) + 1) mod CONSOLE_BUFFER_SIZE}.
End ConsoleDriver.
Section KeyboardDevice.
Inductive KeyAction :=
| Press (k: Z)
| Release (k: Z)
.
Record KeyboardState :=
mkKeyboardState {
KbdIrq: bool;
KbdRxBuf: list Z
}.
Function update_KbdIrq (a: KeyboardState) x :=
mkKeyboardState x (KbdRxBuf a).
Function update_KbdRxBuf (a: KeyboardState) x :=
mkKeyboardState (KbdIrq a) x.
Definition KeyboardData := (DeviceData KeyboardState).
Definition mkKeyboardData (s: KeyboardState) :=
mkDevData s 0 0 0.
Definition kbd_init : KeyboardData :=
mkKeyboardData
(mkKeyboardState false nil).
End KeyboardDevice.
Section KeyboardDriver.
Record KeyboardDriver :=
mkKeyboardDriver {
shift_toggle: Z;
kbd_buf: list Z;
kbd_buf_concrete: ZMap.t ConsoleBufVal;
kbd_rpos_concrete: Z;
kbd_wpos_concrete: Z
}.
Function update_shift_toggle (a: KeyboardDriver) x :=
mkKeyboardDriver x (kbd_buf a) (kbd_buf_concrete a) (kbd_rpos_concrete a)
(kbd_wpos_concrete a).
Function update_kbd_buf (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) x (kbd_buf_concrete a) (kbd_rpos_concrete a)
(kbd_wpos_concrete a).
Function update_kbd_buf_concrete (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) (kbd_buf a) x (kbd_rpos_concrete a)
(kbd_wpos_concrete a).
Function update_kbd_rpos_concrete (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) (kbd_buf a) (kbd_buf_concrete a) x
(kbd_wpos_concrete a).
Function update_kbd_wpos_concrete (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) (kbd_buf a) (kbd_buf_concrete a) (kbd_rpos_concrete a)
x.
Definition kbd_drv_init: KeyboardDriver :=
mkKeyboardDriver 0 nil (ZMap.init BufValUndef) 0 0.
End KeyboardDriver.
Section IoApicDevice.
Inductive IntrOp :=
| IRQ (n: Z)
| EOI.
Inductive IntrMode :=
IntrFixed | IntrLow | SMI | NMI | INIT | ExtINT.
Function low32_to_irq (x: Z): Z :=
x mod 256.
Function low32_to_enable (x: Z): bool :=
x / 65536 mod 2 =? 0.
Inductive IoApicSelType :=
| SelId
| SelVer
| SelTblLow (idx: Z)
| SelTblHigh (idx: Z)
| SelInvalid.
Function reg_to_sel (x: Z) (max: Z) : IoApicSelType :=
match x with
| 0 ⇒ SelId
| 1 ⇒ SelVer
| _ ⇒
if zle_le 16 x max
then
let idx := (x - 16) / 2 in
if zeq (x mod 2) 0
then SelTblLow idx
else SelTblHigh idx
else
SelInvalid
end.
Record IoApicState :=
mkIoApicState {
IoApicInit: bool;
CurrentIrq: option (Z × Z);
IoApicBase: Z;
IoApicId: Z;
IoApicMaxIntr: Z;
IoApicIrqs: list Z;
IoApicEnables: list bool
}.
Function update_IoApicInit (a: IoApicState) x :=
mkIoApicState x (CurrentIrq a) (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_CurrentIrq (a: IoApicState) x :=
mkIoApicState (IoApicInit a) x (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicBase (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) x (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicId (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) x (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicMaxIntr (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) (IoApicId a) x
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicIrqs (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
x (IoApicEnables a).
Function update_IoApicEnables (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) x.
Definition IoApicStateInstance := mkIoApicState.
Inductive Word64 :=
| Low32 (x: Z)
| High32 (x: Z).
Function addr_to_idx (addr: Z) : Word64 :=
let idx := (addr - 16) / 2 in
if zeq (addr mod 2) 0
then Low32 idx
else High32 idx.
Definition IoApicData := (DeviceData IoApicState).
Function mkIoApicData (s: IoApicState) :=
mkDevData s 0 0 0.
Definition ioapic_init_d :=
mkIoApicData
(mkIoApicState false None 4273995776 1 23 (new_list 24 0) (new_list 24 false)).
End IoApicDevice.
Section LApicDevice.
Inductive LApicIntrType :=
| NoIntr
| IntrIoApic (n: Z)
| IntrException (n: Z)
| IntrSyscall (n: Z)
| IntrIpi (n: Z)
| IntrMsi (n: Z)
| IntrGuest (n: Z).
Record LApicState :=
mkLApicState {
LapicEsr: Z;
LapicEoi: LApicIntrType;
LapicMaxLvt: Z;
LapicEnable: bool;
LapicSpurious: Z;
LapicLint0Mask: bool;
LapicLint1Mask: bool;
LapicPcIntMask: bool;
LapicLdr: Z;
LapicErrorIrq: Z;
LapicEsrClrPen: bool;
LapicTpr: Z
}.
Function update_LapicEsr (a: LApicState) x :=
mkLApicState x (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicEoi (a: LApicState) x :=
mkLApicState (LapicEsr a) x (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicMaxLvt (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) x (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicEnable (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) x (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicSpurious (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) x
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicLint0Mask (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
x (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicLint1Mask (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) x (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicPcIntMask (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) x (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicLdr (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) x
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicErrorIrq (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
x (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicEsrClrPen (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) x (LapicTpr a).
Function update_LapicTpr (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) x.
Function lapic_reg_to_enable (reg: Z) :=
if zeq ((reg / 2^8) mod 2) 1 then true else false.
Function lapic_reg_to_spurious (reg: Z) :=
(reg mod 2^8) / 8 × 8 + 7.
Function lapic_reg_to_lvt_mask (reg: Z) :=
if zeq ((reg / 2^16) mod 2) 1 then true else false.
Definition LApicData := (DeviceData LApicState).
Function mkLApicData (s: LApicState) :=
mkDevData s 0 0 0.
Definition lapic_init_d :=
mkLApicData
(mkLApicState 0 NoIntr 5 false 7 false false false 0 0 false 0).
End LApicDevice.
Section CPU.
Require Import Asm.
Record TrapFrame :=
mkTrapFrame {
tf_regs: regset;
tf_trapno: Z;
tf_err: Z;
tf_esp: val
}.
Definition tf_init_d :=
mkTrapFrame
(Pregmap.init Vundef) 0 0 Vundef.
Function update_tf_regs (a: TrapFrame) x :=
mkTrapFrame x (tf_trapno a) (tf_err a) (tf_esp a).
Function update_tf_trapno (a: TrapFrame) x :=
mkTrapFrame (tf_regs a) x (tf_err a) (tf_esp a).
Function update_tf_err (a: TrapFrame) x :=
mkTrapFrame (tf_regs a) (tf_trapno a) x (tf_esp a).
Function update_tf_esp (a: TrapFrame) x :=
mkTrapFrame (tf_regs a) (tf_trapno a) (tf_err a) x.
Definition TrapFrames := list TrapFrame.
Definition tfs_init_d : TrapFrames := nil.
Definition tf_inj (f:meminj) (tf tf´: TrapFrame) :=
∀ r,
(
val_inject f (Pregmap.get r (tf_regs tf)) (Pregmap.get r (tf_regs tf´)) ∧
val_inject f (tf_esp tf) (tf_esp tf´) ∧
tf_err tf = tf_err tf´ ∧
tf_trapno tf = tf_trapno tf´
).
Fixpoint tfs_inj (f:meminj) (tfs tfs´: TrapFrames) :=
match (tfs, tfs´) with
| (nil, nil) ⇒ True
| (tf :: l, tf´ :: l´) ⇒ tf_inj f tf tf´ ∧ tfs_inj f l l´
| _ ⇒ False
end.
Definition tf_inject_neutral (n: block) (tf: TrapFrame) :=
let rs := tf_regs tf in
∀ r, Val.has_type (rs r) (typ_of_preg r)
∧ val_inject (Mem.flat_inj n) (rs r) (rs r).
Definition tfs_inject_neutral (tfs: TrapFrames) (n: block) :=
Forall (tf_inject_neutral n) tfs.
End CPU.
Require Import Clight.
Class IntrParamsOps : Type :=
{
f_serial_intr_disable: Clight.function;
f_serial_intr_enable: Clight.function
}.
End Device.
Notation "a ´{´ ´s´ : x }" := (update_s a x) (at level 1).
Notation "a ´{´ ´l1´ : x }" := (update_l1 a x) (at level 1).
Notation "a ´{´ ´l2´ : x }" := (update_l2 a x) (at level 1).
Notation "a ´{´ ´l3´ : x }" := (update_l3 a x) (at level 1).
Ltac unfold_DeviceData :=
try unfold update_s; simpl;
try unfold update_l1; simpl;
try unfold update_l2; simpl;
try unfold update_l3; simpl.
Notation "a ´{´ ´Base´ : x }" := (update_Base a x) (at level 1).
Notation "a ´{´ ´SerialOn´ : x }" := (update_SerialOn a x) (at level 1).
Notation "a ´{´ ´SerialIrq´ : x }" := (update_SerialIrq a x) (at level 1).
Notation "a ´{´ ´RxIntEnable´ : x }" := (update_RxIntEnable a x) (at level 1).
Notation "a ´{´ ´TxBuf´ : x }" := (update_TxBuf a x) (at level 1).
Notation "a ´{´ ´RxBuf´ : x }" := (update_RxBuf a x) (at level 1).
Notation "a ´{´ ´DLAB´ : x }" := (update_DLAB a x) (at level 1).
Notation "a ´{´ ´Baudrate´ : x }" := (update_Baudrate a x) (at level 1).
Notation "a ´{´ ´Databits´ : x }" := (update_Databits a x) (at level 1).
Notation "a ´{´ ´Stopbits´ : x }" := (update_Stopbits a x) (at level 1).
Notation "a ´{´ ´Parity´ : x }" := (update_Parity a x) (at level 1).
Notation "a ´{´ ´Fifo´ : x }" := (update_Fifo a x) (at level 1).
Notation "a ´{´ ´Modem´ : x }" := (update_Modem a x) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Base´ : x }" := (update_s a (update_Base (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´SerialOn´ : x }" := (update_s a (update_SerialOn (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´SerialIrq´ : x }" := (update_s a (update_SerialIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´RxIntEnable´ : x }" := (update_s a (update_RxIntEnable (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´TxBuf´ : x }" := (update_s a (update_TxBuf (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´RxBuf´ : x }" := (update_s a (update_RxBuf (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´DLAB´ : x }" := (update_s a (update_DLAB (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Baudrate´ : x }" := (update_s a (update_Baudrate (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Databits´ : x }" := (update_s a (update_Databits (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Stopbits´ : x }" := (update_s a (update_Stopbits (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Parity´ : x }" := (update_s a (update_Parity (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Fifo´ : x }" := (update_s a (update_Fifo (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Modem´ : x }" := (update_s a (update_Modem (s (a)) x)) (at level 1).
Ltac unfold_SerialState :=
try unfold update_Base; simpl;
try unfold update_SerialOn; simpl;
try unfold update_SerialIrq; simpl;
try unfold update_RxIntEnable; simpl;
try unfold update_TxBuf; simpl;
try unfold update_RxBuf; simpl;
try unfold update_DLAB; simpl;
try unfold update_Baudrate; simpl;
try unfold update_Databits; simpl;
try unfold update_Stopbits; simpl;
try unfold update_Parity; simpl;
try unfold update_Fifo; simpl;
try unfold update_Modem; simpl.
Tactic Notation "unfold_SerialState_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold update_Base in T; simpl in T;
try unfold update_SerialOn in T; simpl in T;
try unfold update_SerialIrq in T; simpl in T;
try unfold update_RxIntEnable in T; simpl in T;
try unfold update_TxBuf in T; simpl in T;
try unfold update_RxBuf in T; simpl in T;
try unfold update_DLAB in T; simpl in T;
try unfold update_Baudrate in T; simpl in T;
try unfold update_Databits in T; simpl in T;
try unfold update_Stopbits in T; simpl in T;
try unfold update_Parity in T; simpl in T;
try unfold update_Fifo in T; simpl in T;
try unfold update_Modem in T; simpl in T
end.
Notation "a ´{´ ´serial_exists´ : x }" := (update_serial_exists a x) (at level 1).
Notation "a ´{´ ´cons_buf_concrete´ : x }" := (update_cons_buf_concrete a x) (at level 1).
Notation "a ´{´ ´rpos_concrete´ : x }" := (update_rpos_concrete a x) (at level 1).
Notation "a ´{´ ´wpos_concrete´ : x }" := (update_wpos_concrete a x) (at level 1).
Notation "a ´{´ ´cons_buf´ : x }" := (update_cons_buf a x) (at level 1).
Notation "a ´{´ ´rpos´ : x }" := (update_rpos a x) (at level 1).
Ltac unfold_console :=
try unfold update_cons_buf; simpl;
try unfold update_rpos; simpl.
Notation "a ´{´ ´IoApicInit´ : x }" := (update_IoApicInit a x) (at level 1).
Notation "a ´{´ ´CurrentIrq´ : x }" := (update_CurrentIrq a x) (at level 1).
Notation "a ´{´ ´IoApicBase´ : x }" := (update_IoApicBase a x) (at level 1).
Notation "a ´{´ ´IoApicId´ : x }" := (update_IoApicId a x) (at level 1).
Notation "a ´{´ ´IoApicMaxIntr´ : x }" := (update_IoApicMaxIntr a x) (at level 1).
Notation "a ´{´ ´IoApicIrqs´ : x }" := (update_IoApicIrqs a x) (at level 1).
Notation "a ´{´ ´IoApicIrqs´ ´[´ n ´]´ : x }" := (update_IoApicIrqs a (replace x n (IoApicIrqs a))) (at level 1).
Notation "a ´{´ ´IoApicEnables´ : x }" := (update_IoApicEnables a x) (at level 1).
Notation "a ´{´ ´IoApicEnables´ ´[´ n ´]´ : x }" := (update_IoApicEnables a (replace x n (IoApicEnables a))) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´CurrentIrq´ : x }" := (update_s a (update_CurrentIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicBase´ : x }" := (update_s a (update_IoApicBase (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicId´ : x }" := (update_s a (update_IoApicId (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicMaxIntr´ : x }" := (update_s a (update_IoApicMaxIntr (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicIrqs´ : x }" := (update_s a (update_IoApicIrqs (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicIrqs´ ´[´ n ´]´ : x }" := (update_s a (update_IoApicIrqs (s (a)) (replace x n (IoApicIrqs (s a))))) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicEnables´ : x }" := (update_s a (update_IoApicEnables (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicEnables´ ´[´ n ´]´ : x }" := (update_s a (update_IoApicEnables (s (a)) (replace x n (IoApicEnables (s a))))) (at level 1).
Ltac unfold_IoApicState :=
try unfold update_IoApicInit; simpl;
try unfold update_CurrentIrq; simpl;
try unfold update_IoApicBase; simpl;
try unfold update_IoApicId; simpl;
try unfold update_IoApicMaxIntr; simpl;
try unfold update_IoApicIrqs; simpl;
try unfold update_IoApicEnables; simpl.
Tactic Notation "unfold_IoApicState_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold update_CurrentIrq in T; simpl in T;
try unfold update_IoApicBase in T; simpl in T;
try unfold update_IoApicId in T; simpl in T;
try unfold update_IoApicMaxIntr in T; simpl in T;
try unfold update_IoApicIrqs in T; simpl in T;
try unfold update_IoApicEnables in T; simpl in T
end.
Notation "a ´{´ ´LapicEsr´ : x }" := (update_LapicEsr a x) (at level 1).
Notation "a ´{´ ´LapicEoi´ : x }" := (update_LapicEoi a x) (at level 1).
Notation "a ´{´ ´LapicMaxLvt´ : x }" := (update_LapicMaxLvt a x) (at level 1).
Notation "a ´{´ ´LapicEnable´ : x }" := (update_LapicEnable a x) (at level 1).
Notation "a ´{´ ´LapicSpurious´ : x }" := (update_LapicSpurious a x) (at level 1).
Notation "a ´{´ ´LapicLint0Mask´ : x }" := (update_LapicLint0Mask a x) (at level 1).
Notation "a ´{´ ´LapicLint1Mask´ : x }" := (update_LapicLint1Mask a x) (at level 1).
Notation "a ´{´ ´LapicPcIntMask´ : x }" := (update_LapicPcIntMask a x) (at level 1).
Notation "a ´{´ ´LapicLdr´ : x }" := (update_LapicLdr a x) (at level 1).
Notation "a ´{´ ´LapicErrorIrq´ : x }" := (update_LapicErrorIrq a x) (at level 1).
Notation "a ´{´ ´LapicEsrClrPen´ : x }" := (update_LapicEsrClrPen a x) (at level 1).
Notation "a ´{´ ´LapicTpr´ : x }" := (update_LapicTpr a x) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEsr´ : x }" := (update_s a (update_LapicEsr (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEoi´ : x }" := (update_s a (update_LapicEoi (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicMaxLvt´ : x }" := (update_s a (update_LapicMaxLvt (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEnable´ : x }" := (update_s a (update_LapicEnable (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicSpurious´ : x }" := (update_s a (update_LapicSpurious (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicLint0Mask´ : x }" := (update_s a (update_LapicLint0Mask (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicLint1Mask´ : x }" := (update_s a (update_LapicLint1Mask (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicPcIntMask´ : x }" := (update_s a (update_LapicPcIntMask (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicLdr´ : x }" := (update_s a (update_LapicLdr (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicErrorIrq´ : x }" := (update_s a (update_LapicErrorIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEsrClrPen´ : x }" := (update_s a (update_LapicEsrClrPen (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicTpr´ : x }" := (update_s a (update_LapicTpr (s (a)) x)) (at level 1).
Ltac unfold_LApicState :=
try unfold update_LapicEsr; simpl;
try unfold update_LapicEoi; simpl;
try unfold update_LapicMaxLvt; simpl;
try unfold update_LapicEnable; simpl;
try unfold update_LapicSpurious; simpl;
try unfold update_LapicLint0Mask; simpl;
try unfold update_LapicLint1Mask; simpl;
try unfold update_LapicPcIntMask; simpl;
try unfold update_LapicLdr; simpl;
try unfold update_LapicErrorIrq; simpl;
try unfold update_LapicEsrClrPen; simpl;
try unfold update_LapicTpr; simpl.
Tactic Notation "unfold_LApicState_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold update_LapicEsr in T; simpl in T;
try unfold update_LapicEoi in T; simpl in T;
try unfold update_LapicMaxLvt in T; simpl in T;
try unfold update_LapicEnable in T; simpl in T;
try unfold update_LapicSpurious in T; simpl in T;
try unfold update_LapicLint0Mask in T; simpl in T;
try unfold update_LapicLint1Mask in T; simpl in T;
try unfold update_LapicPcIntMask in T; simpl in T;
try unfold update_LapicLdr in T; simpl in T;
try unfold update_LapicErrorIrq in T; simpl in T;
try unfold update_LapicEsrClrPen in T; simpl in T;
try unfold update_LapicTpr in T; simpl in T
end.
Notation "a ´{´ ´tf_regs´ : x }" := (update_tf_regs a x) (at level 1).
Notation "a ´{´ ´tf_trapno´ : x }" := (update_tf_trapno a x) (at level 1).
Notation "a ´{´ ´tf_err´ : x }" := (update_tf_err a x) (at level 1).
Notation "a ´{´ ´tf_esp´ : x }" := (update_tf_esp a x) (at level 1).
Ltac unfold_TrapFrame :=
try unfold update_tf_regs; simpl;
try unfold update_tf_trapno; simpl;
try unfold update_tf_err; simpl;
try unfold update_tf_esp; simpl.
Notation "a ´{´ ´KbdIrq´ : x }" := (update_KbdIrq a x) (at level 1).
Notation "a ´{´ ´KbdRxBuf´ : x }" := (update_KbdRxBuf a x) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´KbdIrq´ : x }" := (update_s a (update_KbdIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´KbdRxBuf´ : x }" := (update_s a (update_KbdRxBuf (s (a)) x)) (at level 1).
Ltac unfold_KeyboardState :=
try unfold update_KbdIrq; simpl;
try unfold update_KbdRxBuf; simpl.
Notation "a ´{´ ´shift_toggle´ : x }" := (update_shift_toggle a x) (at level 1).
Notation "a ´{´ ´kbd_buf´ : x }" := (update_kbd_buf a x) (at level 1).
Notation "a ´{´ ´kbd_buf_concrete´ : x }" := (update_kbd_buf_concrete a x) (at level 1).
Notation "a ´{´ ´kbd_rpos_concrete´ : x }" := (update_kbd_rpos_concrete a x) (at level 1).
Notation "a ´{´ ´kbd_wpos_concrete´ : x }" := (update_kbd_wpos_concrete a x) (at level 1).
Ltac unfold_KeyboardDriver :=
try unfold update_shift_toggle; simpl;
try unfold update_kbd_buf; simpl;
try unfold update_kbd_buf_concrete; simpl;
try unfold update_kbd_rpos_concrete; simpl;
try unfold update_kbd_wpos_concrete; simpl.
Require Import Constant.
Require Import Values.
Require Import List.
Require Export AuxFunctions.
Require Import Maps.
Require Import Memory.
Section Device.
Section AbstractDevice.
Set Implicit Arguments.
Variable T: Type.
Record DeviceData :=
mkDevData {
s: T;
l1: Z;
l2: Z;
l3: Z
}.
Function update_s (a: DeviceData) x :=
mkDevData x (l1 a) (l2 a) (l3 a).
Function update_l1 (a: DeviceData) x :=
mkDevData (s a) x (l2 a) (l3 a).
Function update_l2 (a: DeviceData) x :=
mkDevData (s a) (l1 a) x (l3 a).
Function update_l3 (a: DeviceData) x :=
mkDevData (s a) (l1 a) (l2 a) x.
Inductive DeviceOp :=
| OpInput (addr: Z)
| OpOutput (addr value: Z).
Record Null :=
mkNull {}.
End AbstractDevice.
Inductive ParityType := pOdd | pEven | pHigh | pLow | pNone.
Section SerialDevice.
Record SerialState :=
mkSerialState {
Base: Z;
SerialOn: bool;
SerialIrq: bool;
RxIntEnable: bool;
TxBuf: list Z;
RxBuf: list Z;
DLAB: bool;
Baudrate: Z;
Databits: Z;
Stopbits: Z;
Parity: ParityType;
Fifo: Z;
Modem: Z
}.
Function update_Base (a: SerialState) x :=
mkSerialState x (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_SerialOn (a: SerialState) x :=
mkSerialState (Base a) x (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_SerialIrq (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) x (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_RxIntEnable (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) x (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_TxBuf (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) x (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_RxBuf (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) x
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_DLAB (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
x (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_Baudrate (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) x (Databits a) (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_Databits (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) x (Stopbits a) (Parity a) (Fifo a) (Modem a)
.
Function update_Stopbits (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) x (Parity a) (Fifo a) (Modem a)
.
Function update_Parity (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) x (Fifo a) (Modem a)
.
Function update_Fifo (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) x (Modem a)
.
Function update_Modem (a: SerialState) x :=
mkSerialState (Base a) (SerialOn a) (SerialIrq a) (RxIntEnable a) (TxBuf a) (RxBuf a)
(DLAB a) (Baudrate a) (Databits a) (Stopbits a) (Parity a) (Fifo a) x
.
Definition SerialData := (DeviceData SerialState).
Definition mkSerialData (s: SerialState) :=
mkDevData s 0 0 0.
Definition com1_init : SerialData :=
mkSerialData
(mkSerialState PortCom1Base true false false nil nil false 0 0 0 pNone
0 0).
End SerialDevice.
Section SerialDriver.
Record SerialDriver :=
mkSerialDriver {
serial_exists: Z
}.
Function update_serial_exists (a: SerialDriver) x :=
mkSerialDriver x.
Definition serial_drv_init: SerialDriver :=
mkSerialDriver 0.
End SerialDriver.
Section ConsoleDriverConcrete.
Inductive ConsoleBufVal :=
| BufValUndef
| BufVal (val: Z).
Record ConsoleDriverConcrete :=
mkConsoleDrvierConcrete {
cons_buf_concrete: ZMap.t ConsoleBufVal;
rpos_concrete: Z;
wpos_concrete: Z
}.
Function update_cons_buf_concrete (a: ConsoleDriverConcrete) x :=
mkConsoleDrvierConcrete x (rpos_concrete a) (wpos_concrete a).
Function update_rpos_concrete (a: ConsoleDriverConcrete) x :=
mkConsoleDrvierConcrete (cons_buf_concrete a) x (wpos_concrete a).
Function update_wpos_concrete (a: ConsoleDriverConcrete) x :=
mkConsoleDrvierConcrete (cons_buf_concrete a) (rpos_concrete a) x.
Definition console_init_concrete: ConsoleDriverConcrete :=
mkConsoleDrvierConcrete (ZMap.init BufValUndef) 0 0.
Notation "a ´{´ ´cons_buf_concrete´ : x }" := (update_cons_buf_concrete a x) (at level 1).
Notation "a ´{´ ´rpos_concrete´ : x }" := (update_rpos_concrete a x) (at level 1).
Notation "a ´{´ ´wpos_concrete´ : x }" := (update_wpos_concrete a x) (at level 1).
Import List.ListNotations.
Function handle_cons_buf_write_concrete (s: ConsoleDriverConcrete) (c: Z) : ConsoleDriverConcrete :=
let buf := cons_buf_concrete s in
let wpos := wpos_concrete s in
s {cons_buf_concrete: ZMap.set wpos (BufVal c) buf} {wpos_concrete: (wpos + 1) mod CONSOLE_BUFFER_SIZE}.
End ConsoleDriverConcrete.
Section ConsoleDriver.
Record ConsoleDriver :=
mkConsoleDrvier {
cons_buf: list Z;
rpos: Z
}.
Function update_cons_buf (a: ConsoleDriver) x :=
mkConsoleDrvier x (rpos a).
Function update_rpos (a: ConsoleDriver) x :=
mkConsoleDrvier (cons_buf a) x.
Definition console_init_d: ConsoleDriver :=
mkConsoleDrvier nil 0.
Notation "a ´{´ ´cons_buf´ : x }" := (update_cons_buf a x) (at level 1).
Notation "a ´{´ ´rpos´ : x }" := (update_rpos a x) (at level 1).
Import List.ListNotations.
Function handle_cons_buf_write (s: ConsoleDriver) (c: Z) : ConsoleDriver :=
let b := cons_buf s in
if zlt (Zlength b) (CONSOLE_BUFFER_SIZE - 1)
then
s {cons_buf: (b ++ [c])}
else
s {cons_buf: skipn 1 (b ++ [c])} {rpos: ((rpos s) + 1) mod CONSOLE_BUFFER_SIZE}.
End ConsoleDriver.
Section KeyboardDevice.
Inductive KeyAction :=
| Press (k: Z)
| Release (k: Z)
.
Record KeyboardState :=
mkKeyboardState {
KbdIrq: bool;
KbdRxBuf: list Z
}.
Function update_KbdIrq (a: KeyboardState) x :=
mkKeyboardState x (KbdRxBuf a).
Function update_KbdRxBuf (a: KeyboardState) x :=
mkKeyboardState (KbdIrq a) x.
Definition KeyboardData := (DeviceData KeyboardState).
Definition mkKeyboardData (s: KeyboardState) :=
mkDevData s 0 0 0.
Definition kbd_init : KeyboardData :=
mkKeyboardData
(mkKeyboardState false nil).
End KeyboardDevice.
Section KeyboardDriver.
Record KeyboardDriver :=
mkKeyboardDriver {
shift_toggle: Z;
kbd_buf: list Z;
kbd_buf_concrete: ZMap.t ConsoleBufVal;
kbd_rpos_concrete: Z;
kbd_wpos_concrete: Z
}.
Function update_shift_toggle (a: KeyboardDriver) x :=
mkKeyboardDriver x (kbd_buf a) (kbd_buf_concrete a) (kbd_rpos_concrete a)
(kbd_wpos_concrete a).
Function update_kbd_buf (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) x (kbd_buf_concrete a) (kbd_rpos_concrete a)
(kbd_wpos_concrete a).
Function update_kbd_buf_concrete (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) (kbd_buf a) x (kbd_rpos_concrete a)
(kbd_wpos_concrete a).
Function update_kbd_rpos_concrete (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) (kbd_buf a) (kbd_buf_concrete a) x
(kbd_wpos_concrete a).
Function update_kbd_wpos_concrete (a: KeyboardDriver) x :=
mkKeyboardDriver (shift_toggle a) (kbd_buf a) (kbd_buf_concrete a) (kbd_rpos_concrete a)
x.
Definition kbd_drv_init: KeyboardDriver :=
mkKeyboardDriver 0 nil (ZMap.init BufValUndef) 0 0.
End KeyboardDriver.
Section IoApicDevice.
Inductive IntrOp :=
| IRQ (n: Z)
| EOI.
Inductive IntrMode :=
IntrFixed | IntrLow | SMI | NMI | INIT | ExtINT.
Function low32_to_irq (x: Z): Z :=
x mod 256.
Function low32_to_enable (x: Z): bool :=
x / 65536 mod 2 =? 0.
Inductive IoApicSelType :=
| SelId
| SelVer
| SelTblLow (idx: Z)
| SelTblHigh (idx: Z)
| SelInvalid.
Function reg_to_sel (x: Z) (max: Z) : IoApicSelType :=
match x with
| 0 ⇒ SelId
| 1 ⇒ SelVer
| _ ⇒
if zle_le 16 x max
then
let idx := (x - 16) / 2 in
if zeq (x mod 2) 0
then SelTblLow idx
else SelTblHigh idx
else
SelInvalid
end.
Record IoApicState :=
mkIoApicState {
IoApicInit: bool;
CurrentIrq: option (Z × Z);
IoApicBase: Z;
IoApicId: Z;
IoApicMaxIntr: Z;
IoApicIrqs: list Z;
IoApicEnables: list bool
}.
Function update_IoApicInit (a: IoApicState) x :=
mkIoApicState x (CurrentIrq a) (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_CurrentIrq (a: IoApicState) x :=
mkIoApicState (IoApicInit a) x (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicBase (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) x (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicId (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) x (IoApicMaxIntr a)
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicMaxIntr (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) (IoApicId a) x
(IoApicIrqs a) (IoApicEnables a).
Function update_IoApicIrqs (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
x (IoApicEnables a).
Function update_IoApicEnables (a: IoApicState) x :=
mkIoApicState (IoApicInit a) (CurrentIrq a) (IoApicBase a) (IoApicId a) (IoApicMaxIntr a)
(IoApicIrqs a) x.
Definition IoApicStateInstance := mkIoApicState.
Inductive Word64 :=
| Low32 (x: Z)
| High32 (x: Z).
Function addr_to_idx (addr: Z) : Word64 :=
let idx := (addr - 16) / 2 in
if zeq (addr mod 2) 0
then Low32 idx
else High32 idx.
Definition IoApicData := (DeviceData IoApicState).
Function mkIoApicData (s: IoApicState) :=
mkDevData s 0 0 0.
Definition ioapic_init_d :=
mkIoApicData
(mkIoApicState false None 4273995776 1 23 (new_list 24 0) (new_list 24 false)).
End IoApicDevice.
Section LApicDevice.
Inductive LApicIntrType :=
| NoIntr
| IntrIoApic (n: Z)
| IntrException (n: Z)
| IntrSyscall (n: Z)
| IntrIpi (n: Z)
| IntrMsi (n: Z)
| IntrGuest (n: Z).
Record LApicState :=
mkLApicState {
LapicEsr: Z;
LapicEoi: LApicIntrType;
LapicMaxLvt: Z;
LapicEnable: bool;
LapicSpurious: Z;
LapicLint0Mask: bool;
LapicLint1Mask: bool;
LapicPcIntMask: bool;
LapicLdr: Z;
LapicErrorIrq: Z;
LapicEsrClrPen: bool;
LapicTpr: Z
}.
Function update_LapicEsr (a: LApicState) x :=
mkLApicState x (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicEoi (a: LApicState) x :=
mkLApicState (LapicEsr a) x (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicMaxLvt (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) x (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicEnable (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) x (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicSpurious (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) x
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicLint0Mask (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
x (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicLint1Mask (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) x (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicPcIntMask (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) x (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicLdr (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) x
(LapicErrorIrq a) (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicErrorIrq (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
x (LapicEsrClrPen a) (LapicTpr a).
Function update_LapicEsrClrPen (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) x (LapicTpr a).
Function update_LapicTpr (a: LApicState) x :=
mkLApicState (LapicEsr a) (LapicEoi a) (LapicMaxLvt a) (LapicEnable a) (LapicSpurious a)
(LapicLint0Mask a) (LapicLint1Mask a) (LapicPcIntMask a) (LapicLdr a)
(LapicErrorIrq a) (LapicEsrClrPen a) x.
Function lapic_reg_to_enable (reg: Z) :=
if zeq ((reg / 2^8) mod 2) 1 then true else false.
Function lapic_reg_to_spurious (reg: Z) :=
(reg mod 2^8) / 8 × 8 + 7.
Function lapic_reg_to_lvt_mask (reg: Z) :=
if zeq ((reg / 2^16) mod 2) 1 then true else false.
Definition LApicData := (DeviceData LApicState).
Function mkLApicData (s: LApicState) :=
mkDevData s 0 0 0.
Definition lapic_init_d :=
mkLApicData
(mkLApicState 0 NoIntr 5 false 7 false false false 0 0 false 0).
End LApicDevice.
Section CPU.
Require Import Asm.
Record TrapFrame :=
mkTrapFrame {
tf_regs: regset;
tf_trapno: Z;
tf_err: Z;
tf_esp: val
}.
Definition tf_init_d :=
mkTrapFrame
(Pregmap.init Vundef) 0 0 Vundef.
Function update_tf_regs (a: TrapFrame) x :=
mkTrapFrame x (tf_trapno a) (tf_err a) (tf_esp a).
Function update_tf_trapno (a: TrapFrame) x :=
mkTrapFrame (tf_regs a) x (tf_err a) (tf_esp a).
Function update_tf_err (a: TrapFrame) x :=
mkTrapFrame (tf_regs a) (tf_trapno a) x (tf_esp a).
Function update_tf_esp (a: TrapFrame) x :=
mkTrapFrame (tf_regs a) (tf_trapno a) (tf_err a) x.
Definition TrapFrames := list TrapFrame.
Definition tfs_init_d : TrapFrames := nil.
Definition tf_inj (f:meminj) (tf tf´: TrapFrame) :=
∀ r,
(
val_inject f (Pregmap.get r (tf_regs tf)) (Pregmap.get r (tf_regs tf´)) ∧
val_inject f (tf_esp tf) (tf_esp tf´) ∧
tf_err tf = tf_err tf´ ∧
tf_trapno tf = tf_trapno tf´
).
Fixpoint tfs_inj (f:meminj) (tfs tfs´: TrapFrames) :=
match (tfs, tfs´) with
| (nil, nil) ⇒ True
| (tf :: l, tf´ :: l´) ⇒ tf_inj f tf tf´ ∧ tfs_inj f l l´
| _ ⇒ False
end.
Definition tf_inject_neutral (n: block) (tf: TrapFrame) :=
let rs := tf_regs tf in
∀ r, Val.has_type (rs r) (typ_of_preg r)
∧ val_inject (Mem.flat_inj n) (rs r) (rs r).
Definition tfs_inject_neutral (tfs: TrapFrames) (n: block) :=
Forall (tf_inject_neutral n) tfs.
End CPU.
Require Import Clight.
Class IntrParamsOps : Type :=
{
f_serial_intr_disable: Clight.function;
f_serial_intr_enable: Clight.function
}.
End Device.
Notation "a ´{´ ´s´ : x }" := (update_s a x) (at level 1).
Notation "a ´{´ ´l1´ : x }" := (update_l1 a x) (at level 1).
Notation "a ´{´ ´l2´ : x }" := (update_l2 a x) (at level 1).
Notation "a ´{´ ´l3´ : x }" := (update_l3 a x) (at level 1).
Ltac unfold_DeviceData :=
try unfold update_s; simpl;
try unfold update_l1; simpl;
try unfold update_l2; simpl;
try unfold update_l3; simpl.
Notation "a ´{´ ´Base´ : x }" := (update_Base a x) (at level 1).
Notation "a ´{´ ´SerialOn´ : x }" := (update_SerialOn a x) (at level 1).
Notation "a ´{´ ´SerialIrq´ : x }" := (update_SerialIrq a x) (at level 1).
Notation "a ´{´ ´RxIntEnable´ : x }" := (update_RxIntEnable a x) (at level 1).
Notation "a ´{´ ´TxBuf´ : x }" := (update_TxBuf a x) (at level 1).
Notation "a ´{´ ´RxBuf´ : x }" := (update_RxBuf a x) (at level 1).
Notation "a ´{´ ´DLAB´ : x }" := (update_DLAB a x) (at level 1).
Notation "a ´{´ ´Baudrate´ : x }" := (update_Baudrate a x) (at level 1).
Notation "a ´{´ ´Databits´ : x }" := (update_Databits a x) (at level 1).
Notation "a ´{´ ´Stopbits´ : x }" := (update_Stopbits a x) (at level 1).
Notation "a ´{´ ´Parity´ : x }" := (update_Parity a x) (at level 1).
Notation "a ´{´ ´Fifo´ : x }" := (update_Fifo a x) (at level 1).
Notation "a ´{´ ´Modem´ : x }" := (update_Modem a x) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Base´ : x }" := (update_s a (update_Base (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´SerialOn´ : x }" := (update_s a (update_SerialOn (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´SerialIrq´ : x }" := (update_s a (update_SerialIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´RxIntEnable´ : x }" := (update_s a (update_RxIntEnable (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´TxBuf´ : x }" := (update_s a (update_TxBuf (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´RxBuf´ : x }" := (update_s a (update_RxBuf (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´DLAB´ : x }" := (update_s a (update_DLAB (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Baudrate´ : x }" := (update_s a (update_Baudrate (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Databits´ : x }" := (update_s a (update_Databits (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Stopbits´ : x }" := (update_s a (update_Stopbits (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Parity´ : x }" := (update_s a (update_Parity (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Fifo´ : x }" := (update_s a (update_Fifo (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´Modem´ : x }" := (update_s a (update_Modem (s (a)) x)) (at level 1).
Ltac unfold_SerialState :=
try unfold update_Base; simpl;
try unfold update_SerialOn; simpl;
try unfold update_SerialIrq; simpl;
try unfold update_RxIntEnable; simpl;
try unfold update_TxBuf; simpl;
try unfold update_RxBuf; simpl;
try unfold update_DLAB; simpl;
try unfold update_Baudrate; simpl;
try unfold update_Databits; simpl;
try unfold update_Stopbits; simpl;
try unfold update_Parity; simpl;
try unfold update_Fifo; simpl;
try unfold update_Modem; simpl.
Tactic Notation "unfold_SerialState_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold update_Base in T; simpl in T;
try unfold update_SerialOn in T; simpl in T;
try unfold update_SerialIrq in T; simpl in T;
try unfold update_RxIntEnable in T; simpl in T;
try unfold update_TxBuf in T; simpl in T;
try unfold update_RxBuf in T; simpl in T;
try unfold update_DLAB in T; simpl in T;
try unfold update_Baudrate in T; simpl in T;
try unfold update_Databits in T; simpl in T;
try unfold update_Stopbits in T; simpl in T;
try unfold update_Parity in T; simpl in T;
try unfold update_Fifo in T; simpl in T;
try unfold update_Modem in T; simpl in T
end.
Notation "a ´{´ ´serial_exists´ : x }" := (update_serial_exists a x) (at level 1).
Notation "a ´{´ ´cons_buf_concrete´ : x }" := (update_cons_buf_concrete a x) (at level 1).
Notation "a ´{´ ´rpos_concrete´ : x }" := (update_rpos_concrete a x) (at level 1).
Notation "a ´{´ ´wpos_concrete´ : x }" := (update_wpos_concrete a x) (at level 1).
Notation "a ´{´ ´cons_buf´ : x }" := (update_cons_buf a x) (at level 1).
Notation "a ´{´ ´rpos´ : x }" := (update_rpos a x) (at level 1).
Ltac unfold_console :=
try unfold update_cons_buf; simpl;
try unfold update_rpos; simpl.
Notation "a ´{´ ´IoApicInit´ : x }" := (update_IoApicInit a x) (at level 1).
Notation "a ´{´ ´CurrentIrq´ : x }" := (update_CurrentIrq a x) (at level 1).
Notation "a ´{´ ´IoApicBase´ : x }" := (update_IoApicBase a x) (at level 1).
Notation "a ´{´ ´IoApicId´ : x }" := (update_IoApicId a x) (at level 1).
Notation "a ´{´ ´IoApicMaxIntr´ : x }" := (update_IoApicMaxIntr a x) (at level 1).
Notation "a ´{´ ´IoApicIrqs´ : x }" := (update_IoApicIrqs a x) (at level 1).
Notation "a ´{´ ´IoApicIrqs´ ´[´ n ´]´ : x }" := (update_IoApicIrqs a (replace x n (IoApicIrqs a))) (at level 1).
Notation "a ´{´ ´IoApicEnables´ : x }" := (update_IoApicEnables a x) (at level 1).
Notation "a ´{´ ´IoApicEnables´ ´[´ n ´]´ : x }" := (update_IoApicEnables a (replace x n (IoApicEnables a))) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´CurrentIrq´ : x }" := (update_s a (update_CurrentIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicBase´ : x }" := (update_s a (update_IoApicBase (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicId´ : x }" := (update_s a (update_IoApicId (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicMaxIntr´ : x }" := (update_s a (update_IoApicMaxIntr (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicIrqs´ : x }" := (update_s a (update_IoApicIrqs (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicIrqs´ ´[´ n ´]´ : x }" := (update_s a (update_IoApicIrqs (s (a)) (replace x n (IoApicIrqs (s a))))) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicEnables´ : x }" := (update_s a (update_IoApicEnables (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´IoApicEnables´ ´[´ n ´]´ : x }" := (update_s a (update_IoApicEnables (s (a)) (replace x n (IoApicEnables (s a))))) (at level 1).
Ltac unfold_IoApicState :=
try unfold update_IoApicInit; simpl;
try unfold update_CurrentIrq; simpl;
try unfold update_IoApicBase; simpl;
try unfold update_IoApicId; simpl;
try unfold update_IoApicMaxIntr; simpl;
try unfold update_IoApicIrqs; simpl;
try unfold update_IoApicEnables; simpl.
Tactic Notation "unfold_IoApicState_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold update_CurrentIrq in T; simpl in T;
try unfold update_IoApicBase in T; simpl in T;
try unfold update_IoApicId in T; simpl in T;
try unfold update_IoApicMaxIntr in T; simpl in T;
try unfold update_IoApicIrqs in T; simpl in T;
try unfold update_IoApicEnables in T; simpl in T
end.
Notation "a ´{´ ´LapicEsr´ : x }" := (update_LapicEsr a x) (at level 1).
Notation "a ´{´ ´LapicEoi´ : x }" := (update_LapicEoi a x) (at level 1).
Notation "a ´{´ ´LapicMaxLvt´ : x }" := (update_LapicMaxLvt a x) (at level 1).
Notation "a ´{´ ´LapicEnable´ : x }" := (update_LapicEnable a x) (at level 1).
Notation "a ´{´ ´LapicSpurious´ : x }" := (update_LapicSpurious a x) (at level 1).
Notation "a ´{´ ´LapicLint0Mask´ : x }" := (update_LapicLint0Mask a x) (at level 1).
Notation "a ´{´ ´LapicLint1Mask´ : x }" := (update_LapicLint1Mask a x) (at level 1).
Notation "a ´{´ ´LapicPcIntMask´ : x }" := (update_LapicPcIntMask a x) (at level 1).
Notation "a ´{´ ´LapicLdr´ : x }" := (update_LapicLdr a x) (at level 1).
Notation "a ´{´ ´LapicErrorIrq´ : x }" := (update_LapicErrorIrq a x) (at level 1).
Notation "a ´{´ ´LapicEsrClrPen´ : x }" := (update_LapicEsrClrPen a x) (at level 1).
Notation "a ´{´ ´LapicTpr´ : x }" := (update_LapicTpr a x) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEsr´ : x }" := (update_s a (update_LapicEsr (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEoi´ : x }" := (update_s a (update_LapicEoi (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicMaxLvt´ : x }" := (update_s a (update_LapicMaxLvt (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEnable´ : x }" := (update_s a (update_LapicEnable (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicSpurious´ : x }" := (update_s a (update_LapicSpurious (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicLint0Mask´ : x }" := (update_s a (update_LapicLint0Mask (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicLint1Mask´ : x }" := (update_s a (update_LapicLint1Mask (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicPcIntMask´ : x }" := (update_s a (update_LapicPcIntMask (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicLdr´ : x }" := (update_s a (update_LapicLdr (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicErrorIrq´ : x }" := (update_s a (update_LapicErrorIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicEsrClrPen´ : x }" := (update_s a (update_LapicEsrClrPen (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´LapicTpr´ : x }" := (update_s a (update_LapicTpr (s (a)) x)) (at level 1).
Ltac unfold_LApicState :=
try unfold update_LapicEsr; simpl;
try unfold update_LapicEoi; simpl;
try unfold update_LapicMaxLvt; simpl;
try unfold update_LapicEnable; simpl;
try unfold update_LapicSpurious; simpl;
try unfold update_LapicLint0Mask; simpl;
try unfold update_LapicLint1Mask; simpl;
try unfold update_LapicPcIntMask; simpl;
try unfold update_LapicLdr; simpl;
try unfold update_LapicErrorIrq; simpl;
try unfold update_LapicEsrClrPen; simpl;
try unfold update_LapicTpr; simpl.
Tactic Notation "unfold_LApicState_in" constr(T) :=
match goal with
| [T: _ |- _] ⇒
try unfold update_LapicEsr in T; simpl in T;
try unfold update_LapicEoi in T; simpl in T;
try unfold update_LapicMaxLvt in T; simpl in T;
try unfold update_LapicEnable in T; simpl in T;
try unfold update_LapicSpurious in T; simpl in T;
try unfold update_LapicLint0Mask in T; simpl in T;
try unfold update_LapicLint1Mask in T; simpl in T;
try unfold update_LapicPcIntMask in T; simpl in T;
try unfold update_LapicLdr in T; simpl in T;
try unfold update_LapicErrorIrq in T; simpl in T;
try unfold update_LapicEsrClrPen in T; simpl in T;
try unfold update_LapicTpr in T; simpl in T
end.
Notation "a ´{´ ´tf_regs´ : x }" := (update_tf_regs a x) (at level 1).
Notation "a ´{´ ´tf_trapno´ : x }" := (update_tf_trapno a x) (at level 1).
Notation "a ´{´ ´tf_err´ : x }" := (update_tf_err a x) (at level 1).
Notation "a ´{´ ´tf_esp´ : x }" := (update_tf_esp a x) (at level 1).
Ltac unfold_TrapFrame :=
try unfold update_tf_regs; simpl;
try unfold update_tf_trapno; simpl;
try unfold update_tf_err; simpl;
try unfold update_tf_esp; simpl.
Notation "a ´{´ ´KbdIrq´ : x }" := (update_KbdIrq a x) (at level 1).
Notation "a ´{´ ´KbdRxBuf´ : x }" := (update_KbdRxBuf a x) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´KbdIrq´ : x }" := (update_s a (update_KbdIrq (s (a)) x)) (at level 1).
Notation "a ´{´ ´s´ ´/´ ´KbdRxBuf´ : x }" := (update_s a (update_KbdRxBuf (s (a)) x)) (at level 1).
Ltac unfold_KeyboardState :=
try unfold update_KbdIrq; simpl;
try unfold update_KbdRxBuf; simpl.
Notation "a ´{´ ´shift_toggle´ : x }" := (update_shift_toggle a x) (at level 1).
Notation "a ´{´ ´kbd_buf´ : x }" := (update_kbd_buf a x) (at level 1).
Notation "a ´{´ ´kbd_buf_concrete´ : x }" := (update_kbd_buf_concrete a x) (at level 1).
Notation "a ´{´ ´kbd_rpos_concrete´ : x }" := (update_kbd_rpos_concrete a x) (at level 1).
Notation "a ´{´ ´kbd_wpos_concrete´ : x }" := (update_kbd_wpos_concrete a x) (at level 1).
Ltac unfold_KeyboardDriver :=
try unfold update_shift_toggle; simpl;
try unfold update_kbd_buf; simpl;
try unfold update_kbd_buf_concrete; simpl;
try unfold update_kbd_rpos_concrete; simpl;
try unfold update_kbd_wpos_concrete; simpl.