bedrock.prelude.interrupts

(*
 * Copyright (C) 2020 BlueRock Security, Inc.
 * All rights reserved.
 *
 * This software is distributed under the terms of the BedRock Open-Source License.
 * See the LICENSE-BedRock file in the repository root for details.
 *)

(* XXX Only temporarily here. *)

Require Import bedrock.prelude.base.
Require Import bedrock.prelude.hw_types.

Configurations of the interrupt lines attached to devices


Variant IntTrigger :=
| TriggerEdge
  (* ^ int is edge triggered *)
| TriggerLevel (active_low : bool).
  (* ^ int is low-level triggered active_low = true; otherwise, high-level triggered *)

#[global] Instance int_trigger_inhabited : Inhabited IntTrigger.
Proof. solve_inhabited. Qed.
#[global] Instance int_trigger_decision : EqDecision IntTrigger.
Proof. solve_decision. Defined.

Variant IntOwner :=
| HostInt
(* ^ int is host owned *)
| GuestInt.
(* ^ int is guest owned (VM passthrough) *)

#[global] Instance int_owner_inhabited : Inhabited IntOwner.
Proof. solve_inhabited. Qed.
#[global] Instance int_owner_decision : EqDecision IntOwner.
Proof. solve_decision. Defined.

Variant IntStatus : Set := IntMasked | IntEnabled.

#[global] Instance int_status_inhabited : Inhabited IntStatus.
Proof. solve_inhabited. Qed.
#[global] Instance int_status_decision : EqDecision IntStatus.
Proof. solve_decision. Defined.

Record IntConfig : Set :=
  { int_cpu : cpu
  ; int_trigger : IntTrigger
  ; int_owner : IntOwner
  ; int_status : IntStatus }.

The IntConfig value before the first assign_int

From NOVA IFSPEC 5.5.2 (assign_int): other than int_status := IntMasked, other values (CPU, trigger) are undefined for the initial interrupts. Furthermore, when the interrupt is masked, other values do not matter much, except when an EC requests a ctrl_sm DOWN on the interrupt sm, then NOVA checks that the EC's CPU matches the config's CPU.
Definition initialIntConfig :=
  {| int_cpu := cpu.of_N 0
  ; int_trigger := TriggerEdge
  ; int_owner := HostInt
  ; int_status := IntMasked
  |}.

Definition INT_config_of (c : cpuT) (edge active_low is_guest masked : bool)
    : IntConfig :=
  {| int_cpu := c
    ; int_trigger := if edge then TriggerEdge else TriggerLevel active_low
    ; int_owner := if is_guest then GuestInt else HostInt
    ; int_status := if masked then IntMasked else IntEnabled |}.

#[global] Instance int_config_inhabited : Inhabited IntConfig.
Proof. solve_inhabited. Qed.
#[global] Instance int_cfg_decision : EqDecision IntConfig.
Proof. solve_decision. Defined.

intline_of (x : T): The interrupt line attached to some value x : T
Class IntLines (T : Type) := intline_of : T -> int_line.
#[global] Hint Mode IntLines + : typeclass_instances.

Interrupt signals generated by devices


Variant InterruptSignal : Set :=
| LevelSig (_ : bool)
| EdgeSig.
  (* ^ note(gmm): it might not be possible to implement EdgeSig as successive
   * LevelSig true, LevelSig false because arbitrary scheduling can occur between
   * two events, so the LevelSig true might hide other interrupts.
   *)

#[global] Instance InterruptSignal_inhabited : Inhabited InterruptSignal.
Proof. solve_inhabited. Qed.
#[global] Instance InterruptSignal_eq_dec : EqDecision InterruptSignal.
Proof. solve_decision. Defined.

Definition int_trigger_match (sig : InterruptSignal) (trg : IntTrigger) : Prop :=
  match sig with
  | LevelSig high => trg = TriggerLevel (negb high)
    (* ^ high = true is a valid level trigger only if
         TriggerLevel false = active_low*). *)
  | EdgeSig => trg = TriggerEdge
  end.
#[global] Instance int_trigger_match_dec sig trg : Decision (int_trigger_match sig trg).
Proof. case: sig => /=; by apply: _. Defined.

Definition int_types_match (sig : InterruptSignal) (ty : IntConfig) : Prop :=
  int_trigger_match sig ty.(int_trigger).
#[global] Instance int_types_match_decision sig cfg : Decision (int_types_match sig cfg).
Proof. case: cfg => ?; by apply: _. Defined.

intcfg_valid cfg own sig means that cfg matches sig, the interrupt line was configured IntEnabled, and the owner is own (guest or host).
Definition intcfg_valid (cfg : IntConfig) (own : IntOwner) (sig : InterruptSignal) : Prop :=
    int_types_match sig cfg /\
    cfg.(int_owner) = own /\
    cfg.(int_status) = IntEnabled.

(* Confirm these instances are already derivable. *)
#[global] Instance intline_elem_of_dec :
  @RelDecision (int_line * IntConfig) (list (int_line * IntConfig)) elem_of.
Proof. apply _. Abort.

#[global] Instance intcfg_valid_decision cfg own sig : Decision (intcfg_valid cfg own sig).
Proof. apply _. Abort.

Record IntAction :=
{ line : int_line
; to : InterruptSignal
}.

#[global] Instance IntAction_inhabited : Inhabited IntAction.
Proof. solve_inhabited. Defined.
#[global] Instance IntAction_eq_dec : EqDecision IntAction.
Proof. solve_decision. Defined.