Module state

The small step reduction (as defined in the file smallstep) is a binary relation between execution states. In this file we define execution states, of which we consider five variants: The above kinds of execution states are adapted from Compcert's Cmedium. Like CompCert, we capture undefined behavior by an explicit state for undefined behavior.
Undefined behavior is different from the reduction semantics getting stuck. For statically correct programs (i.e. those where all function names have a corresponding body, labels for gotos exist, etc) the reduction semantics should not get stuck, but might still end up in a state of undefined behavior.
Require Export statements memory.

Definitions

Execution of statements occurs by traversal through the program context in one of the following directions: down , up , to the top , or jump . When a return e statement is executed, and the expression e is evaluated to the value v, the direction is changed to v. The semantics then performs a traversal to the top of the statement, and returns from the called function. When a goto l statement is executed, the direction is changed to l, and the semantics performs a non-deterministic small step traversal through the zipper until the label l is found.
Inductive direction (K : Set) : Set :=
  | Down
  | Up
  | Top : val Kdirection K
  | Goto : labelnamedirection K
  | Throw : natdirection K
  | Switch : option Zdirection K.
Arguments Down {_}.
Arguments Up {_}.
Arguments Top {_} _.
Arguments Goto {_} _.
Arguments Throw {_} _.
Arguments Switch {_} _%Z.

Notation "↘" := Down : C_scope.
Notation "↗" := Up : C_scope.
Notation "⇈ v" := (Top v) (at level 20) : C_scope.
Notation "↷ l" := (Goto l) (at level 20) : C_scope.
Notation "↑ n" := (Throw n) (at level 20) : C_scope.
Notation "↓ mx" := (Switch mx) (at level 20) : C_scope.

Instance direction_eq_dec {K : Set} `{∀ k1 k2 : K, Decision (k1 = k2)}
  (d1 d2 : direction K) : Decision (d1 = d2).
Proof. solve_decision. Defined.

Definition direction_in {K} (d : direction K) (s : stmt K) : Prop :=
  match d with
  | ↘ => True | ↷ l => llabels s | ↓ mx => mxcases s | _ => False
  end.
Definition direction_out {K} (d : direction K) (s : stmt K) : Prop :=
  match d with
  | ↗ | ⇈ _ => True | ↷ l => llabels s | ↑ _ => True | _ => False
  end.
Arguments direction_in _ _ _ : simpl nomatch.
Arguments direction_out _ _ _ : simpl nomatch.
Hint Unfold direction_in direction_out.

Lemma direction_in_out {K} (d : direction K) s :
  direction_in d sdirection_out d sFalse.
Proof. by destruct d. Qed.

The data type focus describes the part of the program that is focused. An execution state state equips a focus with a program context and memory. These focuses correspond to the five variants of execution states as described above.
Inductive undef_state (K : Set) : Set :=
  | UndefExpr : ectx Kexpr Kundef_state K
  | UndefBranch : esctx_item Klocksetval Kundef_state K.
Inductive focus (K : Set) : Set :=
  | Stmt : direction Kstmt Kfocus K
  | Expr : expr Kfocus K
  | Call : funnamelist (val K) → focus K
  | Return : funnameval Kfocus K
  | Undef : undef_state Kfocus K.
Record state (K : Set) : Set :=
  State { SCtx : ctx K; SFoc : focus K; SMem : mem K }.
Add Printing Constructor state.

Arguments UndefExpr {_} _ _.
Arguments UndefBranch {_} _ _ _.
Arguments Stmt {_} _ _.
Arguments Expr {_} _.
Arguments Call {_} _ _.
Arguments Return {_} _ _.
Arguments Undef {_} _.
Arguments State {_} _ _ _.
Arguments SCtx {_} _.
Arguments SFoc {_} _.
Arguments SMem {_} _.

Instance undef_state_eq_dec {K : Set} `{∀ k1 k2 : K, Decision (k1 = k2)}
  (S1 S2 : undef_state K) : Decision (S1 = S2).
Proof. solve_decision. Defined.
Instance focus_eq_dec {K : Set} `{∀ k1 k2 : K, Decision (k1 = k2)}
  (φ1 φ2 : focus K) : Decision (φ1 = φ2).
Proof. solve_decision. Defined.
Instance state_eq_dec {K : Set} `{Env K}
  (S1 S2 : state K) : Decision (S1 = S2).
Proof. solve_decision. Defined.

Instance maybe_Call {K} : Maybe2 (@Call K) := λ S,
  match S with Call f vs => Some (f,vs) | _ => None end.
Instance maybe_Return {K} : Maybe2 (@Return K) := λ S,
  match S with Return f v => Some (f,v) | _ => None end.
Instance maybe_Undef {K} : Maybe (@Undef K) := λ S,
  match S with Undef Su => Some Su | _ => None end.

Definition initial_state {K} (m : mem K)
  (f : funname) (vs : list (val K)) : state K := State [] (Call f vs) m.
Definition is_final_state {K}
    (f : funname) (v : val K) (S : state K) : Prop :=
  maybe2 Return (SFoc S) = Some (f,v) ∧ SCtx S = [].
Arguments is_final_state _ _ _ !_ /.
Definition is_undef_state {K} (S : state K) : Prop :=
  is_Some (maybe Undef (SFoc S)).
Arguments is_undef_state _ !_ /.