(* Copyright (c) 2017, the Dart project authors.  Please see the AUTHORS file
 * for details. All rights reserved. Use of this source code is governed by a
 * BSD-style license that can be found in the LICENSE file. *)


Require Import Coq.Lists.List.
Require Import Common.
Require Import Syntax.
Require Import ObjectModel.


Import ObjectModel.Subtyping.

Notation "s <: t" := (subtype (s, t) = true) (at level 70, no associativity).


Section OperationalSemantics.


(** The well-formedness hypothesis is that the environments are built via
  [lib_to_env] function from the object model module.  [program_wf] theorem
  defined there provides the rest of the well-formedness properties.  In
  [OperationalSemantics] sections we don't need the hypothesis itself, just the
  environments. *)
Variable CE : class_env.
Variable ME : member_env.


(** [runtime_value] represents the runtime values used in the abstract machine
  during program execution.  The values are typed and have some relation to
  syntactic types and internal representation of their interfaces. Currently a
  runtime value doesn't have a state, it only has a type.  It should have a
  state when a broader subset of Kernel is formalized. *)
Record runtime_value := mk_runtime_value {

  (** Null is currently modelled using None as the value of [runtime_type].
    It may change in future once [dart_type] includes a constructor for Null
    or Bottom.  Also, in the current subset of Kernel type Null can't be
    expressed syntactically; therefore, it can't be a declared type of a method
    parameter, a declared type of a variable, etc.  The only use of Null in the
    current subset of Kernel is that of a runtime type of a runtime value.  In
    that case the declared type of the variable holding such value and the
    runtime type of the value do not match.  *)
  runtime_type : option dart_type;
}.


(** [value_of_type] defines the meaning of statement "the runtime value has the
  given interface and the given type". *)
Inductive value_of_type :
    runtime_value -> interface -> option dart_type -> Prop :=

  (** If the type of the runtime value is an interface type, then the
    corresponding interface should be in the global class environment. *)
  | RFS_Interface_Type :
    forall val intf type class_id,
    type = DT_Interface_Type (Interface_Type class_id) ->
    NatMap.find class_id CE = Some intf ->
    (runtime_type val) = Some type ->
    value_of_type val intf (Some type)

  (** If the type of the runtime value is a function type, then the
    corresponding interface may or may not be in the global class environment,
    but should have a particular shape. *)
  | RFS_Function_Type :
    forall val intf ftype memb_id proc,
    (procedures intf) = (mk_procedure_desc "call" memb_id ftype) :: nil ->
    (getters intf) =
      (mk_getter_desc "call" memb_id (DT_Function_Type ftype)) :: nil ->
    NatMap.MapsTo memb_id (M_Procedure proc) ME ->
    (runtime_type val) = Some (DT_Function_Type ftype) ->
    value_of_type val intf (Some (DT_Function_Type ftype))

  (** Null values are currently represented as runtime values that have [None]
    in place of their type.  In future, for example when the Bottom type or
    explicit Null type are added to the syntax of dart types, the
    representation may change. *)
  | RFS_Null_Type :
    forall val intf,
    (procedures intf) = nil ->
    (getters intf) = nil ->
    (runtime_type val) = None ->
    value_of_type val intf None.


(** Describes that the given dart type has a method with the given name.  The
  predicate can be applied to runtime types of values, so it should accept None
  as the first parameter to account for `null` values.

  Currently, values of function type only have "call" methods, and null doesn't
  have any methods. *)
Inductive method_exists : option dart_type -> string -> Prop :=

  | ME_Interface_Type :
    forall name intf desc class_id type,
    type = (DT_Interface_Type (Interface_Type class_id)) ->
    (* TODO(dmitryas): Replace `value_of_type` here with a relation that binds
      together the interface and the type, avoiding the construction of the
      value. *)
    value_of_type (mk_runtime_value (Some type)) intf (Some type) ->
    List.In desc (procedures intf) ->
    ((pr_name desc) = name)%string ->
    method_exists (Some type) name

  | ME_Function_Type :
    forall type intf desc ftype,
    type = (DT_Function_Type ftype) ->
    (* TODO(dmitryas): Replace `value_of_type` here with a relation that binds
      together the interface and the type, avoiding the construction of the
      value. *)
    value_of_type (mk_runtime_value (Some type)) intf (Some type) ->
    List.In desc (procedures intf) ->
    ((pr_name desc) = "call")%string ->
    method_exists (Some type) "call".


(** Describes that the method with the given name of the given dart type
  accepts arguments of the given type.  The predicate can be applied to runtime
  types of values, so it should accept None as the first parameter to account
  for `null` values.

  Currently, values of function type only have "call" methods, and null doesn't
  have any methods. *)
Inductive method_accepts :
    option dart_type -> string -> option dart_type -> Prop :=

  | MA_Non_Null :
    forall name intf desc rcvr_type arg_type par_type ret_type,
    method_exists (Some rcvr_type) name ->
    (* TODO(dmitryas): Replace `value_of_type` here with a relation that binds
      together the interface and the type, avoiding the construction of the
      value. *)
    value_of_type (mk_runtime_value (Some rcvr_type)) intf (Some rcvr_type) ->
    List.In desc (procedures intf) ->
    ((pr_name desc) = name)%string ->
    (pr_type desc) = Function_Type par_type ret_type ->
    arg_type <: par_type ->
    method_accepts (Some rcvr_type) name (Some arg_type)

  | MA_Null :
    forall rcvr_type_opt name,
    method_exists rcvr_type_opt name ->
    method_accepts rcvr_type_opt name None.


(** Describes that the method with the given name of the given dart type
  returns a value of the given type.  The predicate can be applied to runtime
  types of values, so it should accept None as the first parameter to account
  for `null` values.

  Currently, values of function type only have "call" methods, and null doesn't
  have any methods. *)
Inductive method_returns :
    option dart_type -> string -> dart_type -> Prop :=

  | Method_Returns :
    forall name intf desc rcvr_type par_type ret_type,
    method_exists (Some rcvr_type) name ->
    (* TODO(dmitryas): Replace `value_of_type` here with a relation that binds
      together the interface and the type, avoiding the construction of the
      value. *)
    value_of_type (mk_runtime_value (Some rcvr_type)) intf (Some rcvr_type) ->
    List.In desc (procedures intf) ->
    ((pr_name desc) = name)%string ->
    (pr_type desc) = Function_Type par_type ret_type ->
    method_returns (Some rcvr_type) name ret_type.


(** Describes that the given dart type has a getter with the given name.  The
  predicate can be applied to runtime types of values, so it should accept None
  as the first parameter to account for `null` values.

  Currently, values of function type only have "call" getters, and null doesn't
  have any getters. *)
Inductive getter_exists : option dart_type -> string -> Prop :=

  | GE_Interface_Type :
    forall name intf desc class_id type,
    type = (DT_Interface_Type (Interface_Type class_id)) ->
    (* TODO(dmitryas): Replace `value_of_type` here with a relation that binds
      together the interface and the type, avoiding the construction of the
      value. *)
    value_of_type (mk_runtime_value (Some type)) intf (Some type) ->
    List.In desc (getters intf) ->
    ((gt_name desc) = name)%string ->
    getter_exists (Some type) name

  | GE_Function_Type :
    forall type intf desc ftype,
    type = (DT_Function_Type ftype) ->
    (* TODO(dmitryas): Replace `value_of_type` here with a relation that binds
      together the interface and the type, avoiding the construction of the
      value. *)
    value_of_type (mk_runtime_value (Some type)) intf (Some type) ->
    List.In desc (getters intf) ->
    ((gt_name desc) = "call")%string ->
    getter_exists (Some type) "call".


(** Describes that the getter with the given name of the given dart type
  returns a value of the given type.  The predicate can be applied to runtime
  types of values, so it should accept None as the first parameter to account
  for `null` values.

  Currently, values of function type only have "call" getters, and null doesn't
  have any getters. *)
Inductive getter_returns :
    option dart_type -> string -> dart_type -> Prop :=

  | Getter_Returns :
    forall name intf desc rcvr_type,
    getter_exists (Some rcvr_type) name ->
    value_of_type (mk_runtime_value (Some rcvr_type)) intf (Some rcvr_type) ->
    List.In desc (getters intf) ->
    ((gt_name desc) = name)%string ->
    getter_returns (Some rcvr_type) name (gt_type desc).


(** The environment that is used by the abstract machine to map the currently
  visible set of variables to their types and runtime values is represented as
  a list of records.

  [var_type] represents the declared type of the variable and may not match
  the runtime type of the [value] in case the latter is Null.  This is because
  in the current subset of Kernel Null can't be represented syntactically. *)
Record env_entry := mk_env_entry {
  var_ref   : nat;
  var_type  : dart_type;
  value     : runtime_value;
}.

Definition environment := list env_entry.

Definition env_get
      (var : nat)
      (env : environment)
    : option env_entry :=
  List.find (fun entry => Nat.eqb var (var_ref entry)) env.

Definition env_extend
      (var  : nat)
      (type : dart_type)
      (val  : runtime_value)
      (env  : environment)
    : environment :=
  (mk_env_entry var type val) :: env.

Definition env_in
      (var : nat)
      (env : environment)
    : Prop :=
  match List.find (fun entry => Nat.eqb var (var_ref entry)) env with
  | None    => False
  | Some _  => True
  end.

Definition empty_env : environment := nil.

Definition env_to_type_env : environment -> type_env :=
  fun env => List.fold_left
    (fun TE entry => NatMap.add (var_ref entry) (var_type entry) TE)
    env
    (NatMap.empty dart_type).


(** TODO(dmitryas): Write descriptive comments.

  First, [untyped_expression_continuation] is defined.  Its only difference
  from [expression_continuation] is that the value expected by the continuation
  is untyped; [expression_continuation] pairs an
  [untyped_expression_continuation] and a [dart_type], giving the expected
  value a type.  It is done to simplify the extraction of the type from an
  expression continuation in predicates. *)
Inductive untyped_expression_continuation : Set :=

  (** The constructor receives the following parameters:

    - an [environment]
    - a [expression_continuation]
    - a [statement_continuation] *)
  | Expression_Ek :
       environment
    -> expression_continuation
    -> statement_continuation
    -> untyped_expression_continuation

  (** The constructor receives the following parameters:

    - a [string]
    - an [expression]
    - an [environment]
    - a [expression_continuation] *)
  | Method_Invocation_Ek :
       string
    -> expression
    -> environment
    -> expression_continuation
    -> untyped_expression_continuation

  (** The constructor receives the following parameters:

    - a [runtime_value]
    - a [string]
    - an [environment]
    - a [expression_continuation] *)
  | Invocation_Ek :
       runtime_value
    -> string
    -> environment
    -> expression_continuation
    -> untyped_expression_continuation

  (** The constructor receives the following parameters:

    - a [string]
    - a [expression_continuation] *)
  | Property_Get_Ek :
       string
    -> expression_continuation
    -> untyped_expression_continuation

  (** The constructor receives the following parameters:

    - a [nat]
    - a [dart_type]
    - an [environment]
    - a [statement_continuation] *)
  | Var_Declaration_Ek :
       nat
    -> dart_type
    -> environment
    -> statement_continuation
    -> untyped_expression_continuation

  (** [Halt_Ek] represents the end of program execution.  The main procedure
    returns a value (or null) to this expression continuation.  The value is
    then ignored, and the program execution halts.  The constructor doesn't
    receive any parameters. *)
  | Halt_Ek :
    untyped_expression_continuation

(** TODO(dmitryas): Write descriptive comments. *)
with statement_continuation : Set :=

  (** The constructor receives the following parameters:

    - a [expression_continuation]
    - a [runtime_value] *)
  | Exit_Sk :
       expression_continuation
    -> runtime_value
    -> statement_continuation

  (** The constructor receives the following parameters:

    - a list of [statement]s
    - an [environment]
    - a [expression_continuation]
    - a [statement_continuation] *)
  | Block_Sk :
       list statement
    -> environment
    -> expression_continuation
    -> statement_continuation
    -> statement_continuation

(** A [expression_continuation] encapsulates a [dart_type] that signifies
  the type of the value expected by the expression continuation as the
  input.

  In the current subset of Kernel the Null type can't be described
  syntactically, so it can't be a type of a typed expression or statement.
  Therefore, the type of the value expected by the expression continuation
  can't be Null, and it's expressed as [dart_type], not [option dart_type]. *)
with expression_continuation : Set :=

  | Expression_Continuation :
       untyped_expression_continuation
    -> dart_type
    -> expression_continuation.


(** [configuration] represents configurations of the CESK abstract machine that
  is used for defining the operational semantics.  A transition of the machine
  represents a small step of the small-step operational semantics.  There are
  the following types of configurations:

  - [Eval_Configuration] — encapsulates a syntactic expression and an
    expression continuation.  After evaluation of the expression the resulting
    value is passed to the expression configuration.
  - [Exec_Configuration] — encapsulates a syntactic statement.  Represents the
    execution of the statement.
  - [Value_Passing_Configuration] — encapsulates a value and an expression
    continuation.  The value is passed to the expression continuation.
  - [Forward_Configuration] — encapsulates a statement continuation.
    The execution of the program proceeds to the associated statement. *)
Inductive configuration : Set :=

  (** [Eval_Configuration] represents the beginning of an expression
    evaluation.  The constructor receives the following parameters:

    - an [expression] — the expression to be evaluated;
    - an [environment] — the mapping from variables to values that is to be
      used during the expression evaluation;
    - a [expression_continuation] — the continuation that will receive
      the value of the expression after its evaluation. *)
  | Eval_Configuration :
       expression
    -> environment
    -> expression_continuation
    -> configuration

  (** [Exec_Configuration] represents the beginning of a statement execution.
    The constructor receives the following parameters:

    - a [statement] — the statement to be executed;
    - an [environment] — the mapping from variables to values that is to be
      used during the statement execution;
    - a [expression_continuation] — in case the executed statement
      returns a value, this continuation will receive this value;
    - a [statement_continuation] — in case the executed statement
      doesn't return a value, this continuation represents the rest of the
      program execution. *)
  | Exec_Configuration :
       statement
    -> environment
    -> expression_continuation
    -> statement_continuation
    -> configuration

  (** [Value_Passing_Configuration] represents the end of an expression
    evaluation.  The constructor receives the following parameters:

    - a [expression_continuation] — the continuation that receives the
      value which is the result of the expression evaluation;
    - a [value] — the result of the expression evaluation. *)
  | Value_Passing_Configuration :
       expression_continuation
    -> runtime_value
    -> configuration

  (** [Forward_Configuration] represents the rest of the program execution.
    The constructor receives the following parameters:

    - a [statement_continuation] — represents the rest of the program
      execution;
    - an [environment] — the mapping from variables to values that is to be
      used during the execution of the rest of the program. *)
  | Forward_Configuration :
       statement_continuation
    -> environment
    -> configuration.


(** Represents steps (a.k.a. transitions) of the abstract machine. *)
Inductive step : configuration -> configuration -> Prop :=

  (** <Block(stmt :: stmts), ρ, κE, κS>exec ==>
        <stmt, ρ, κE, BlockSK(stmts, ρ, κE, κS)>exec *)
  | Exec_Block :
    forall stmt stmts env ret_cont next_cont,
    step (Exec_Configuration
            (S_Block (Block (stmt :: stmts)))
            env ret_cont next_cont)
         (Exec_Configuration
            stmt env ret_cont
            (Block_Sk stmts env ret_cont next_cont))

  (** <Block(#[]#), ρ, κE, κS>exec ==> <κS, ρ>forward *)
  | Exec_Block_Empty :
    forall env ret_cont next_cont,
    step (Exec_Configuration
            (S_Block (Block nil)) env ret_cont next_cont)
         (Forward_Configuration next_cont env)

  (** <BlockSK(stmt :: stmts, ρ, κE, κS), ρ'>forward ==>
        <stmt, ρ', κE, BlockSK(stmts, ρ, κE, κS)>exec *)
  | Forward_Block_Sk :
    forall stmt stmts env ret_cont next_cont env',
    step (Forward_Configuration
            (Block_Sk (stmt :: stmts) env ret_cont next_cont)
            env')
         (Exec_Configuration
            stmt env' ret_cont
            (Block_Sk stmts env ret_cont next_cont))

  (** <BlockSK(#[]#, ρ, κE, κS), ρ'>forward ==> <κS, ρ>forward *)
  | Forward_Block_Sk_Empty :
    forall env ret_cont next_cont env',
    step (Forward_Configuration
            (Block_Sk nil env ret_cont next_cont)
            env')
         (Forward_Configuration next_cont env)

  (** <ExpressionStatement(expr), ρ, κE, κS>exec ==>
        <expr, ρ, ExpressionEK(ρ, κE, κS)>eval *)
  | Exec_Expression_Statement :
    forall expr env ret_cont next_cont ret_type,
    expression_type CE (env_to_type_env env) expr = Some ret_type ->
    step (Exec_Configuration
            (S_Expression_Statement (Expression_Statement expr))
            env ret_cont next_cont)
         (Eval_Configuration
            expr env
            (Expression_Continuation
              (Expression_Ek env ret_cont next_cont)
              ret_type))

  (** <ReturnStatement(expr), ρ, κE, κS>exec ==> <expr, ρ, κE>eval *)
  | Exec_Return_Statement :
    forall expr env ret_cont next_cont,
    step (Exec_Configuration
            (S_Return_Statement (Return_Statement expr))
             env ret_cont next_cont)
         (Eval_Configuration expr env ret_cont)

  (** <VariableGet(var), ρ, κE>eval ==> <κE, ρ(var)>pass *)
  | Eval_Variable_Get :
    forall var_id env ret_cont entry,
    env_get var_id env = Some entry ->
    step (Eval_Configuration
            (E_Variable_Get (Variable_Get var_id)) env ret_cont)
         (Value_Passing_Configuration
            ret_cont (value entry))

  (** <MethodInvocation(rcvr, name, arg), ρ, κE>eval ==>
        <rcvr, ρ, MethodInvocationEK(name, arg, ρ, κE)>eval *)
  | Eval_Method_Invocation :
    (* TODO(dmitryas): Remove [ref] after interfaceTargetReference is removed
      from constructor [Method_Invocation]. *)
    forall rcvr_expr rcvr_type name arg env ret_cont ref,
    expression_type CE (env_to_type_env env) rcvr_expr = Some rcvr_type ->
    step (Eval_Configuration
            (E_Invocation_Expression (IE_Method_Invocation
              (Method_Invocation rcvr_expr (Name name) (Arguments arg) ref)))
            env ret_cont)
         (Eval_Configuration rcvr_expr env
            (Expression_Continuation
              (Method_Invocation_Ek name arg env ret_cont)
              rcvr_type))

  (** <MethodInvocationEK(name, arg, ρ, κE), rcvrVal)pass ==>
        <arg, ρ, InvocationEK(rcvrVal, name, ρ, κE)>eval,
      rcvrVall != null *)
  | Pass_Method_Invocation_Ek_Non_Null :
    forall name arg_expr arg_type env ret_cont
        rcvr_val rcvr_type expected_rcvr_type,
    runtime_type rcvr_val = Some rcvr_type ->
    expression_type CE (env_to_type_env env) arg_expr = Some arg_type ->
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Method_Invocation_Ek name arg_expr env ret_cont)
              expected_rcvr_type)
            rcvr_val)
         (Eval_Configuration arg_expr env
            (Expression_Continuation
              (Invocation_Ek rcvr_val name env ret_cont)
              arg_type))

  (** <InvocationEK(rcvrVal, name, ρ, κE), argVal>pass ==>
        <block, ρ', κE, κS>exec,
      where ρ' = ρ0#[#this = rcvrVal#][#arg(f) = argVal#]#,
        block = body(f),
        κS = ExitSK(κE, nullVal),
        f = methods(class(rcvrVal))(name),
        ρ0 — empty environment *)
  | Pass_Invocation_Ek :
    forall rcvr_val rcvr_intf rcvr_type_opt
      proc_desc memb_data named_data func_node
      var_id var_type var_init ret_type body
      name arg_val arg_type env env'
      ret_cont next_cont null_val,
    (* TODO(dmitryas): Add the mapping: this -> rcvr_val to env'. *)
    value_of_type rcvr_val rcvr_intf rcvr_type_opt ->
    List.In proc_desc (procedures rcvr_intf) ->
    NatMap.MapsTo
      (pr_ref proc_desc)
      (M_Procedure (Procedure memb_data named_data func_node))
      ME ->
    func_node =
      Function_Node
        (Variable_Declaration var_id var_type var_init)
        ret_type
        body ->
    env' = env_extend var_id var_type arg_val empty_env ->
    next_cont = Exit_Sk ret_cont null_val ->
    value_of_type null_val (mk_interface nil nil) None ->
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Invocation_Ek rcvr_val name env ret_cont)
              arg_type)
            arg_val)
         (Exec_Configuration body env' ret_cont next_cont)

  (** <PropertyGet(rcvr, name), ρ, κE>eval ==>
        <rcvr, ρ, PropertyGetEK(name, κE)>eval *)
  | Eval_Property_Get :
    forall rcvr_expr rcvr_type name env ret_cont,
    expression_type CE (env_to_type_env env) rcvr_expr = Some rcvr_type ->
    step (Eval_Configuration
            (E_Property_Get (Property_Get rcvr_expr (Name name)))
            env ret_cont)
         (Eval_Configuration
            rcvr_expr env
            (Expression_Continuation
              (Property_Get_Ek name ret_cont)
              rcvr_type))

  (** <PropertyGetEK(name, κE), rcvrVal)pass ==> <κE, f>pass,
      where f = methods(class(rcvrVal))(name) *)
  | Pass_Property_Get_Ek :
    forall rcvr_val rcvr_intf rcvr_type_opt expected_rcvr_type
        name memb_id ret_type
        ret_val ret_intf
        ret_cont,
    value_of_type rcvr_val rcvr_intf rcvr_type_opt ->
    List.In (mk_getter_desc name memb_id ret_type) (getters rcvr_intf) ->
    value_of_type ret_val ret_intf (Some ret_type) ->
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Property_Get_Ek name ret_cont)
              expected_rcvr_type)
            rcvr_val)
         (Value_Passing_Configuration
            ret_cont ret_val)

  (** <ExitSK(κE, val), ρ>forward ==> <κE, val>pass *)
  | Forward_Exit_Sk :
    forall ret_cont val env,
    step (Forward_Configuration (Exit_Sk ret_cont val) env)
         (Value_Passing_Configuration ret_cont val)

  (** <ConstructorInvocation(cls), ρ, κE>eval ==> <κE, newVal>pass,
      where newVal = new runtime value of syntactic type cls *)
  | Eval_Constructor_Invocation :
    forall env ret_cont new_val intf type_opt class_id,
    NatMap.MapsTo class_id intf CE ->
    value_of_type new_val intf type_opt ->
    step (Eval_Configuration
            (E_Invocation_Expression (IE_Constructor_Invocation
              (Constructor_Invocation class_id)))
            env ret_cont)
         (Value_Passing_Configuration ret_cont new_val)

  (** <VariableDeclaration(var, type, NONE), ρ, κE, κS>exec ==>
        <κS, ρ'>forward,
      where ρ' = ρ#[#var = nullVal#]# *)
  | Exec_Variable_Declaration_Non_Init :
    forall var type env ret_cont next_cont null_val env',
    value_of_type null_val (mk_interface nil nil) None ->
    env' = env_extend var type null_val env ->
    step (Exec_Configuration
            (S_Variable_Declaration (Variable_Declaration var type None))
            env ret_cont next_cont)
         (Forward_Configuration next_cont env')

  (** <VariableDeclaration(var, type, expr), ρ, κE, κS>exec ==>
        <expr, ρ, VarDeclarationEK(var, ρ, κS)>eval *)
  | Exec_Variable_Declaration_Init :
    forall var var_type init_type expr env ret_cont next_cont,
    expression_type CE (env_to_type_env env) expr = Some init_type ->
    step (Exec_Configuration
            (S_Variable_Declaration
              (Variable_Declaration var var_type (Some expr)))
            env ret_cont next_cont)
         (Eval_Configuration expr env
            (Expression_Continuation
              (Var_Declaration_Ek var var_type env next_cont)
              init_type))

  (** <VarDeclarationEK(var, ρ, κS), val>pass ==> <κS, ρ'>forward,
      where ρ' = ρ#[#var = val#]# *)
  | Pass_Var_Declaration_Ek :
    forall var var_type init_type env next_cont val env',
    env' = env_extend var var_type val env ->
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Var_Declaration_Ek var var_type env next_cont)
              init_type)
            val)
         (Forward_Configuration next_cont env')

  (** <ExpressionEK(ρ, κE, κS), val>pass ==> <κS, ρ>forward *)
  | Pass_Expression_Ek :
    forall env ret_cont next_cont val val_type,
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Expression_Ek env ret_cont next_cont)
              val_type)
            val)
         (Forward_Configuration next_cont env)

  (** <MethodInvocationEK(name, arg, ρ, κE), null)pass ==>
        <HaltEK, null>pass *)
  | Pass_Method_Invocation_Ek_Null :
    forall name arg_expr arg_type env ret_cont expected_rcvr_type,
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Method_Invocation_Ek name arg_expr env ret_cont)
              expected_rcvr_type)
            (mk_runtime_value None))
         (Value_Passing_Configuration
            (Expression_Continuation
              Halt_Ek
              arg_type)
            (mk_runtime_value None))

  (** <PropertyGetEK(name, κE), null)pass ==> <HaltEK, null>pass *)
  | Pass_Property_Get_Ek_Null :
    forall name ret_cont expected_rcvr_type,
    step (Value_Passing_Configuration
            (Expression_Continuation
              (Property_Get_Ek name ret_cont)
              expected_rcvr_type)
            (mk_runtime_value None))
         (Value_Passing_Configuration
            (Expression_Continuation
              Halt_Ek
              expected_rcvr_type)
            (mk_runtime_value None)).

(* TODO(dmitryas): Add transitions to final states. *)


(** Well-formedness property over configurations is understood as the property
  of being a valid l.h.s. to the [step] relation.  The abstract machine may or
  may not end up in a well-formed configuration several steps after its
  configuration was well-formed. *)
Inductive configuration_wf : configuration -> Prop :=

  (** Well-formed variable-gets should have the variable in the environment. *)
  | Eval_Variable_Get_Configuration_Wf :
    forall var env ret_cont,
    env_in var env ->
    configuration_wf
      (Eval_Configuration
        (E_Variable_Get (Variable_Get var))
        env ret_cont)

  (** Configurations that are the beginning of a method-invocation evaluation
    are well-formed if the expression that represents the receiver is
    well-typed, because the machine proceed to evaluation of the receiver, and
    the continuation that awaits for the receiver value should be typed. *)
  | Eval_Method_Invocation_Configuration_Wf :
    forall rcvr_expr rcvr_type name arg_expr ref env ret_cont,
    expression_type CE (env_to_type_env env) rcvr_expr = Some rcvr_type ->
    configuration_wf
      (Eval_Configuration
        (E_Invocation_Expression (IE_Method_Invocation
          (Method_Invocation rcvr_expr (Name name) (Arguments arg_expr) ref)))
        env ret_cont)

  (** Configurations that are the beginning of a property-get evaluation are
    well-formed if the receiver expression is well-typed, because the machine
    always proceed to evaluation of the receiver, and the continuation that
    awaits for the receiver value should be typed. *)
  | Eval_Property_Get_Configuration_Wf :
    forall rcvr_expr rcvr_type name env ret_cont,
    expression_type CE (env_to_type_env env) rcvr_expr = Some rcvr_type ->
    configuration_wf
      (Eval_Configuration
        (E_Property_Get (Property_Get rcvr_expr (Name name)))
        env ret_cont)

  (** A constructor invocation is well-formed if the referred class exists in
    the class environment. *)
  | Eval_Constructor_Invocation_Configuration_Wf :
    forall class_id env ret_cont,
    NatMap.In class_id CE ->
    configuration_wf
      (Eval_Configuration
        (E_Invocation_Expression (IE_Constructor_Invocation
          (Constructor_Invocation class_id)))
        env ret_cont)

  (** TODO(dmitryas): Write descriptive comment here. *)
  | Exec_Variable_Declaration_Init_Wf :
  forall var var_type init_expr init_type env ret_cont next_cont,
    expression_type CE (env_to_type_env env) init_expr = Some init_type ->
    configuration_wf
      (Exec_Configuration
        (S_Variable_Declaration
          (Variable_Declaration var var_type (Some init_expr)))
        env ret_cont next_cont)

  (** TODO(dmitryas): Write descriptive comment here. *)
  | Exec_Variable_Declaration_Non_Init_Wf :
    forall var var_type env ret_cont next_cont,
    configuration_wf
      (Exec_Configuration
        (S_Variable_Declaration
          (Variable_Declaration var var_type None))
        env ret_cont next_cont)

  (** TODO(dmitryas): Write descriptive comment here. *)
  | Exec_Return_Statement_Wf :
    forall expr env ret_cont next_cont,
    configuration_wf
      (Exec_Configuration
        (S_Return_Statement (Return_Statement expr))
        env ret_cont next_cont)

  (** TODO(dmitryas): Write descriptive comment here. *)
  | Exec_Expression_Statement_Wf :
    forall expr expr_type env ret_cont next_cont,
    expression_type CE (env_to_type_env env) expr = Some expr_type ->
    configuration_wf
      (Exec_Configuration
        (S_Expression_Statement (Expression_Statement expr))
        env ret_cont next_cont)

  (** TODO(dmitryas): Write descriptive comment here. *)
  | Exec_Block_Wf :
    forall stmts env ret_cont next_cont,
    configuration_wf
      (Exec_Configuration (S_Block (Block stmts)) env ret_cont next_cont)

  (** These configurations pass the receiver to the continuation that is the
    rest of the method invocation.  These configurations are well-formed if the
    argument expression is well-typed, because the machine procedes to the
    evaluation of the argument, and the expression continuation that awaits for
    the argument value needs to be typed. *)
  | Pass_Method_Invocation_Ek_Non_Null_Configuration_Wf :
    forall name arg_expr arg_type env ret_cont
        expected_rcvr_type rcvr_type rcvr_val,
    runtime_type rcvr_val = Some rcvr_type ->
    expression_type CE (env_to_type_env env) arg_expr = Some arg_type ->
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation
          (Method_Invocation_Ek name arg_expr env ret_cont)
          expected_rcvr_type)
        rcvr_val)

  (** These configurations pass the evaluated argument to the rest of the
    method invocation.  The precondition is that the method with such name
    exists. *)
  | Pass_Invocation_Ek_Configuration_Wf :
    forall rcvr_val name ret_cont arg_val arg_type env,
    method_exists (runtime_type rcvr_val) name ->
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation
          (Invocation_Ek rcvr_val name env ret_cont)
          arg_type)
        arg_val)

  (** These configurations pass the evaluated receiver to the rest of the
    property get.  The preconditions is that the getter with such name
    exists. *)
  | Pass_Property_Get_Ek_Non_Null_Configuration_Wf :
    forall name ret_cont expected_rcvr_type rcvr_type rcvr_val,
    runtime_type rcvr_val = Some rcvr_type ->
    getter_exists (runtime_type rcvr_val) name ->
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation
          (Property_Get_Ek name ret_cont)
          expected_rcvr_type)
        rcvr_val)

  (** In the currently formalized subset of Kernel all forward configurations
    are well-formed.  The machine either proceeds to the execution of a
    a statement or proceeds to the next continuation. *)
  | Forward_Configuration_Wf :
    forall next_cont env,
    configuration_wf (Forward_Configuration next_cont env)

  (** TODO(dmitryas): Write descriptive comments. *)
  | Pass_Expression_Ek_Configuration_Wf :
    forall env ret_cont next_cont val val_type,
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation
          (Expression_Ek env ret_cont next_cont)
          val_type)
        val)

  (** TODO(dmitryas): Write descriptive comments. *)
  | Pass_Var_Declaration_Ek_Configuration_Wf :
    forall var var_type env next_cont init_type val,
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation
          (Var_Declaration_Ek var var_type env next_cont)
          init_type)
        val)

  (** Invoking a method on `null` always puts the abstract machine in a final
    state, so passing `null` to MethodInvocationEK is always well-formed. *)
  | Pass_Method_Invocation_Ek_Null_Configuration_Wf :
    forall name arg_expr env ret_cont rcvr_type rcvr_val,
    runtime_type rcvr_val = None ->
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation
          (Method_Invocation_Ek name arg_expr env ret_cont)
          rcvr_type)
        rcvr_val)

  (** Getting a property of `null` always puts the abstract machine in a final
    state, so passing `null` to propertyGetEK is always well-formed. *)
  | Pass_Property_Get_Ek_Null_Configuration_Wf :
    forall name ret_cont rcvr_type rcvr_val,
    runtime_type rcvr_val = None ->
    configuration_wf
      (Value_Passing_Configuration
        (Expression_Continuation (Property_Get_Ek name ret_cont) rcvr_type)
        rcvr_val).


Inductive configuration_final : configuration -> Prop :=

  | Configuration_Final :
    forall val ret_type,
    configuration_final
      (Value_Passing_Configuration
        (Expression_Continuation Halt_Ek ret_type)
        val).


Inductive ref_in_dart_type : nat -> dart_type -> Prop :=

  | RDT_Interface_Type :
    forall ref,
    ref_in_dart_type ref (DT_Interface_Type (Interface_Type ref))

  | RDT_Function_Type :
    forall ref param_type ret_type,
    (ref_in_dart_type ref param_type \/
     ref_in_dart_type ref ret_type) ->
    ref_in_dart_type ref (DT_Function_Type
      (Function_Type param_type ret_type)).


Inductive dart_type_valid : option dart_type -> Prop :=

  | DTV_Null :
    dart_type_valid None

  | DTV_Non_Null :
    forall class_id type,
    ref_in_dart_type class_id type ->
    NatMap.In class_id CE ->
    dart_type_valid (Some type).


Inductive runtime_value_valid (val : runtime_value) : Prop :=

  | RTV_Not_Null :
    forall intf type,
    (runtime_type val) = Some type ->
    dart_type_valid (Some type) ->
    value_of_type val intf (runtime_type val) ->
    runtime_value_valid val

  | RTV_Null :
    value_of_type val (mk_interface nil nil) None ->
    runtime_value_valid val.


(** [expression_wf] is a well-formedness condition for expression w.r.t. the
  class and member environments.  It requires that all class and member
  references in the expression are present in [CE] and [ME] respectively. *)
Inductive expression_wf : expression -> Prop :=

  | EXPWF_Variable_Get :
    forall var_get_expr,
    expression_wf (E_Variable_Get var_get_expr)

  | EXPWF_Property_Get :
    forall rcvr_expr name,
    expression_wf rcvr_expr ->
    expression_wf (E_Property_Get (Property_Get rcvr_expr name))

  | EXPWF_Method_Invocation :
    (* TODO(dmitryas): Remove [ref] when the corresponding element is removed
      from the AST. *)
    forall rcvr_expr name arg_expr ref,
    expression_wf rcvr_expr ->
    expression_wf arg_expr ->
    expression_wf (E_Invocation_Expression (IE_Method_Invocation
      (Method_Invocation rcvr_expr name (Arguments arg_expr) ref)))

  | EXPWF_Constructor_Invocation :
    forall ref,
    NatMap.In ref CE ->
    expression_wf (E_Invocation_Expression (IE_Constructor_Invocation
      (Constructor_Invocation ref))).


(** [statement_wf] is a property that is analogous to [expression_wf], but is
  defined for statements. *)
Inductive statement_wf : statement -> Prop :=

  | STWF_Expression_Statement :
    forall expr,
    expression_wf expr ->
    statement_wf (S_Expression_Statement (Expression_Statement expr))

  | STWF_Block_Empty :
    statement_wf (S_Block (Block nil))

  | STWF_Block_Non_Empty :
    forall stmt stmts,
    statement_wf stmt ->
    statement_wf (S_Block (Block stmts)) ->
    statement_wf (S_Block (Block (stmt :: stmts)))

  | STWF_Return_Statement :
    forall expr,
    expression_wf expr ->
    statement_wf (S_Return_Statement (Return_Statement expr))

  | STWF_Variable_Declaration_Non_Init :
    forall var_id type,
    (forall class_id,
      ref_in_dart_type class_id type -> NatMap.In class_id CE) ->
    statement_wf (S_Variable_Declaration
      (Variable_Declaration var_id type None))

  | STWF_Variable_Declaration_Init :
    forall var_id type init_expr,
    dart_type_valid (Some type) ->
    expression_wf init_expr ->
    statement_wf (S_Variable_Declaration
      (Variable_Declaration var_id type (Some init_expr))).


(** [environment_valid] is a property of environment validity with respect
  to the class and method environments.  For each variable in the environment
  there should be a valid interface, so that [value_of_type] predicate for the
  variable is true. *)
Inductive environment_valid : environment -> Prop :=

  | EV_Empty :
    environment_valid nil

  | EV_Non_Empty_Null :
    forall entry env,
    dart_type_valid (Some (var_type entry)) ->
    (runtime_type (value entry)) = None ->
    environment_valid env ->
    environment_valid (entry :: env)

  | EV_Non_Empty_Non_Null :
    forall entry env,
    dart_type_valid (Some (var_type entry)) ->
    (runtime_type (value entry)) = Some (var_type entry) ->
    environment_valid env ->
    environment_valid (entry :: env).


(** The given syntactic type is accepted by the given expression continuation.

  None is accepted as the second argument, because runtime type of values can
  be checkec agains the expression continuation. *)
Inductive econt_accepts :
    expression_continuation -> option dart_type -> Prop :=

  | EA_Null :
    forall econt,
    econt_accepts econt None

  | EA_Non_Null :
    forall cont expected_type type,
    type <: expected_type ->
    econt_accepts
      (Expression_Continuation cont expected_type)
      (Some type).


(** The syntactic type of the expression matches the syntactic type of the
  value expected by the expression continuation. *)
Inductive econt_accepts_expr :
    expression_continuation -> expression -> environment -> Prop :=

  | Econt_Accepts_Expr :
    forall econt expr env expr_type,
    expression_type CE (env_to_type_env env) expr = Some expr_type ->
    econt_accepts econt (Some expr_type) ->
    econt_accepts_expr econt expr env.


(** The syntactic type returned by the statement (if any) matches the syntactic
  type of the value expected by the expression continuation. *)
Inductive econt_accepts_stmt :
    expression_continuation -> statement -> environment -> Prop :=

  | Econt_Accepts_Stmt :
    forall econt stmt env ret_type te,
    statement_type CE (env_to_type_env env) stmt ret_type = Some te ->
    econt_accepts econt (Some ret_type) ->
    econt_accepts_stmt econt stmt env.


(** The syntactic type of the value matches the syntactic type of the value
  expected by the expression continuation. *)
Definition econt_accepts_val :
    expression_continuation -> runtime_value -> Prop :=
  fun econt val => econt_accepts econt (runtime_type val).


(** Each free variable referenced from the expression is present in the
  environment. *)
Inductive eval_environment_sufficient : environment -> expression -> Prop :=

  | EES_Variable_Get :
    forall var env,
    env_in var env ->
    eval_environment_sufficient env (E_Variable_Get (Variable_Get var))

  | EES_Property_Get :
    forall expr name env,
    eval_environment_sufficient env expr ->
    eval_environment_sufficient env (E_Property_Get (Property_Get expr name))

  | EES_Constructor_Invocation :
    forall class_id env,
    eval_environment_sufficient
      env
      (E_Invocation_Expression
        (IE_Constructor_Invocation
          (Constructor_Invocation class_id)))

  | EES_Method_Invocation :
    (* TODO(dmitryas): Remove ref when it's removed from the AST. *)
    forall rcvr_expr arg_expr name ref env,
    eval_environment_sufficient env rcvr_expr ->
    eval_environment_sufficient env arg_expr ->
    eval_environment_sufficient
      env
      (E_Invocation_Expression
        (IE_Method_Invocation
          (Method_Invocation rcvr_expr name (Arguments arg_expr) ref))).


(** [exec_environment_sufficient] represents the property of the environment
  w.r.t. the given statement.  The property shows if the given environment is
  sufficient to evaluate all expressions in the given statement. *)
Inductive exec_environment_sufficient : environment -> statement -> Prop :=

  | EES_Expression_Statement :
    forall env expr,
    eval_environment_sufficient env expr ->
    exec_environment_sufficient
      env
      (S_Expression_Statement (Expression_Statement expr))

  | EES_Block_Empty :
    forall env,
    exec_environment_sufficient env (S_Block (Block nil))

  | EES_Block_Non_Empty :
    forall env stmt stmts,
    exec_environment_sufficient env stmt ->
    exec_environment_sufficient env (S_Block (Block stmts)) ->
    exec_environment_sufficient env (S_Block (Block (stmt :: stmts)))

  | EES_Return_Statement :
    forall env expr,
    eval_environment_sufficient env expr ->
    exec_environment_sufficient
      env
      (S_Return_Statement (Return_Statement expr))

  | EES_Variable_Declaration_Non_Init :
    forall env var type,
    exec_environment_sufficient
      env
      (S_Variable_Declaration (Variable_Declaration var type None))

  | EES_Variable_Declaration_Init :
    forall env var type init_expr,
    eval_environment_sufficient env init_expr ->
    exec_environment_sufficient
      env
      (S_Variable_Declaration
        (Variable_Declaration var type (Some init_expr))).


(** Validity property for expression continuations [econt_valid] and statement
  continuations [scont_valid] is mutually inductive, because instances of one
  may refer to instances of the other. *)
Inductive econt_valid : expression_continuation -> Prop :=

  | CV_Expression_Ek :
    forall expr_type env ret_cont next_cont,
    environment_valid env ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    dart_type_valid (Some expr_type) ->
    econt_valid
      (Expression_Continuation
        (Expression_Ek env ret_cont next_cont)
        expr_type)

  | CV_Method_Invocation_Ek :
    forall rcvr_type name arg_exp arg_type ret_type env ret_cont,
    environment_valid env ->
    dart_type_valid (Some rcvr_type) ->
    method_accepts (Some rcvr_type) name (Some arg_type) ->
    method_returns (Some rcvr_type) name ret_type ->
    expression_wf arg_exp ->
    eval_environment_sufficient env arg_exp ->
    expression_type CE (env_to_type_env env) arg_exp = Some arg_type ->
    dart_type_valid (Some arg_type) ->
    econt_valid ret_cont ->
    dart_type_valid (Some ret_type) ->
    econt_accepts ret_cont (Some ret_type) ->
    econt_valid
      (Expression_Continuation
        (Method_Invocation_Ek name arg_exp env ret_cont)
        rcvr_type)

  | CV_Invocation_Ek :
    forall rcvr_val name env ret_cont arg_type ret_type,
    environment_valid env ->
    runtime_value_valid rcvr_val ->
    method_accepts (runtime_type rcvr_val) name (Some arg_type) ->
    method_returns (runtime_type rcvr_val) name ret_type ->
    dart_type_valid (Some arg_type) ->
    econt_valid ret_cont ->
    dart_type_valid (Some ret_type) ->
    econt_accepts ret_cont (Some ret_type) ->
    econt_valid
      (Expression_Continuation
        (Invocation_Ek rcvr_val name env ret_cont)
        arg_type)

  | CV_Property_Get_Ek :
    forall name ret_cont rcvr_type ret_type,
    dart_type_valid (Some rcvr_type) ->
    getter_returns (Some rcvr_type) name ret_type ->
    econt_valid ret_cont ->
    dart_type_valid (Some ret_type) ->
    econt_accepts ret_cont (Some ret_type) ->
    econt_valid
      (Expression_Continuation
        (Property_Get_Ek name ret_cont)
        rcvr_type)

  | CV_Var_Declaration_Ek :
    forall var var_type env next_cont init_type,
    environment_valid env ->
    dart_type_valid (Some var_type) ->
    dart_type_valid (Some init_type) ->
    init_type <: var_type ->
    scont_valid next_cont ->
    econt_valid
      (Expression_Continuation
        (Var_Declaration_Ek var var_type env next_cont)
        init_type)

with scont_valid : statement_continuation -> Prop :=

  | CV_Exit_Sk :
    forall ret_cont val,
    econt_valid ret_cont ->
    runtime_value_valid val ->
    econt_accepts_val ret_cont val ->
    scont_valid (Exit_Sk ret_cont val)

  | CV_Block_Sk_Empty :
    forall env ret_cont next_cont,
    environment_valid env ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    scont_valid (Block_Sk nil env ret_cont next_cont)

  | CV_Block_Sk_Expression_Statement :
    forall stmt expr expr_type stmts env ret_cont next_cont,
    environment_valid env ->
    stmt = S_Expression_Statement (Expression_Statement expr) ->
    statement_wf stmt ->
    expression_type CE (env_to_type_env env) expr = Some expr_type ->
    scont_valid (Block_Sk stmts env ret_cont next_cont) ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    scont_valid (Block_Sk (stmt :: stmts) env ret_cont next_cont)

  | CV_Block_Sk_Block :
    forall stmt block_stmts stmts env ret_cont next_cont,
    environment_valid env ->
    stmt = S_Block (Block block_stmts) ->
    statement_wf stmt ->
    scont_valid (Block_Sk stmts env ret_cont next_cont) ->
    scont_valid
      (Block_Sk block_stmts env ret_cont
        (Block_Sk stmts env ret_cont next_cont)) ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    scont_valid (Block_Sk (stmt :: stmts) env ret_cont next_cont)

  | CV_Block_Sk_Return_Statement :
    forall stmt expr expr_type stmts env ret_cont next_cont,
    environment_valid env ->
    stmt = S_Return_Statement (Return_Statement expr) ->
    statement_wf stmt ->
    expression_type CE (env_to_type_env env) expr = Some expr_type ->
    dart_type_valid (Some expr_type) ->
    econt_valid ret_cont ->
    econt_accepts ret_cont (Some expr_type) ->
    (* TODO(dmitryas): Do we really need the validity of the dead code? *)
    scont_valid (Block_Sk stmts env ret_cont next_cont) ->
    scont_valid next_cont ->
    scont_valid (Block_Sk (stmt :: stmts) env ret_cont next_cont)

  | CV_Block_Sk_Variable_Declaration_Init :
    forall stmt var var_type init_expr init_expr_type
        stmts env env' ret_cont next_cont,
    environment_valid env ->
    stmt = S_Variable_Declaration
      (Variable_Declaration var var_type (Some init_expr)) ->
    statement_wf stmt ->
    expression_type CE (env_to_type_env env) init_expr = Some init_expr_type ->
    init_expr_type <: var_type ->
    env' = env_extend var var_type (mk_runtime_value (Some var_type)) env ->
    scont_valid (Block_Sk stmts env' ret_cont next_cont) ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    scont_valid (Block_Sk (stmt :: stmts) env ret_cont next_cont)

  | CV_Block_Sk_Variable_Declaration_Non_Init :
    forall stmt var var_type stmts env env' ret_cont next_cont,
    environment_valid env ->
    stmt = S_Variable_Declaration
      (Variable_Declaration var var_type None) ->
    statement_wf stmt ->
    env' = env_extend var var_type (mk_runtime_value None) env ->
    scont_valid (Block_Sk stmts env' ret_cont next_cont) ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    scont_valid (Block_Sk (stmt :: stmts) env ret_cont next_cont).


Inductive configuration_valid : configuration -> Prop :=

  | Eval_Configuration_Valid :
    forall exp env cont,
    expression_wf exp ->
    environment_valid env ->
    econt_valid cont ->
    eval_environment_sufficient env exp ->
    econt_accepts_expr cont exp env ->
    configuration_valid (Eval_Configuration exp env cont)

  | Exec_Configuration_Valid :
    forall stmt env ret_cont next_cont,
    statement_wf stmt ->
    environment_valid env ->
    econt_valid ret_cont ->
    scont_valid next_cont ->
    exec_environment_sufficient env stmt ->
    econt_accepts_stmt ret_cont stmt env ->
    configuration_valid (Exec_Configuration stmt env ret_cont next_cont)

  | Value_Passing_Configuration_Valid :
    forall cont val,
    econt_valid cont ->
    runtime_value_valid val ->
    econt_accepts_val cont val ->
    configuration_valid (Value_Passing_Configuration cont val)

  | Forward_Configuration_Valid :
    forall cont env,
    scont_valid cont ->
    environment_valid env ->
    configuration_valid (Forward_Configuration cont env).


Inductive steps : configuration -> configuration -> Prop :=

  | steps_zero :
    forall conf,
    steps conf conf

  | steps_trans_right :
    forall conf1 conf2 conf3,
    steps conf1 conf2 ->
    step conf2 conf3 ->
    steps conf1 conf3.


End OperationalSemantics.