[kernel] Add the first draft of Kernel operational semantics in Coq
The semantics is defined for a small subset of Kernel.
Change-Id: I39b72c5671e9ca0dee86a5a6068fe745ad1728f1
Reviewed-on: https://dart-review.googlesource.com/5860
Reviewed-by: Samir Jindel <sjindel@google.com>
diff --git a/pkg/kernel/coq/OperationalSemantics.v b/pkg/kernel/coq/OperationalSemantics.v
new file mode 100644
index 0000000..8060525
--- /dev/null
+++ b/pkg/kernel/coq/OperationalSemantics.v
@@ -0,0 +1,409 @@
+(* 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.
+
+
+(** Placeholder for a mapping from function node ids to function nodes. At
+ some point the mapping should be defined in the syntax module along with its
+ well-formedness definitions. *)
+Definition func_env : Type := NatMap.t function_node.
+
+
+Section OperationalSemantics.
+
+
+(** This instance of [class_env] is referred in many properties in the section
+ for the operational semantics. One may think about [CE] as a "global" class
+ environment for the program. *)
+Variable CE : class_env.
+
+
+(** The "global" environment of function nodes for the program. *)
+Variable FE : func_env.
+
+(** Placeholder for one of the well-formedness properties of the program. At
+ some point a property like this one (or another property that will allow this
+ property to be established) should be defined in the syntax module. *)
+Hypothesis program_wf:
+ forall class_id intf proc_desc,
+ NatMap.MapsTo class_id intf CE ->
+ List.In proc_desc (procedures intf) ->
+ NatMap.In (pr_ref proc_desc) FE.
+
+
+(** [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 {
+
+ (** In the currently formalized subset of Kernel any runtime type can be
+ represented by a syntactic description that is not necessarily defined
+ in the program. In all cases we assume how such type could be potentially
+ given using the syntax of the current Kernel subset.
+
+ Null is currently modelled using None as the value of [syntactic_type].
+ It may change in future once [dart_type] includes a constructor for Null
+ or Bottom. *)
+ syntactic_type : option dart_type;
+}.
+
+
+(** [value_of_type] defines the meaning of statement "the runtime value has the
+ given interface and the given syntactic type". *)
+Inductive value_of_type :
+ runtime_value -> interface -> option dart_type -> Prop :=
+
+ (** If the syntactic 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 : runtime_value) (intf : interface) (type : dart_type)
+ (class_id : nat),
+ type = DT_Interface_Type (Interface_Type class_id) ->
+ NatMap.find class_id CE = Some intf ->
+ (syntactic_type val) = Some type ->
+ value_of_type val intf (Some type)
+
+ (** If the syntactic 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 : runtime_value) (intf : interface) (type : dart_type)
+ (par_type ret_type : dart_type)
+ (proc : procedure_desc) (proc_rest : list procedure_desc),
+ type = DT_Function_Type (Function_Type par_type ret_type) ->
+ List.length (procedures intf) = 1%nat ->
+ (procedures intf) = List.cons proc proc_rest ->
+ ((pr_name proc) = "call")%string ->
+ (pr_type proc) = Function_Type par_type ret_type ->
+ NatMap.In (pr_ref proc) FE ->
+ (syntactic_type val) = Some type ->
+ value_of_type val intf (Some type)
+
+ | RFS_Null_Type :
+ forall (val : runtime_value) (intf : interface),
+ (procedures intf) = nil ->
+ (syntactic_type val) = None ->
+ value_of_type val intf None.
+
+
+(** The environment that is used by the abstract machine to map the currently
+ visible set of variables to their runtime values is represented as a list of
+ pairs. *)
+Record environment_entry := mk_environment_entry {
+ variable_id : nat;
+ value : runtime_value;
+}.
+
+Definition environment := list environment_entry.
+
+Definition env_get : nat -> environment -> option environment_entry :=
+ fun var_id env =>
+ List.find (fun entry => Nat.eqb var_id (variable_id entry)) env.
+
+Definition env_extend : nat -> runtime_value -> environment -> environment :=
+ fun var_id val env => (mk_environment_entry var_id val) :: env.
+
+Definition empty_env : environment := nil.
+
+(* TODO(dmitryas): Add some hypotheses about well-formedness of an environment
+ w.r.t. to other components. *)
+
+
+(** TODO(dmitryas): Write descriptive comments. *)
+Inductive expression_continuation : Set :=
+
+ (** The constructor receives the following parameters:
+
+ - an [environment]
+ - an [expression_continuation]
+ - a [statement_continuation] *)
+ | Expression_Ek :
+ environment
+ -> expression_continuation
+ -> statement_continuation
+ -> expression_continuation
+
+ (** The constructor receives the following parameters:
+
+ - a [string]
+ - an [expression]
+ - an [environment]
+ - an [expression_continuation] *)
+ | Method_Invocation_Ek :
+ string
+ -> expression
+ -> environment
+ -> expression_continuation
+ -> expression_continuation
+
+ (** The constructor receives the following parameters:
+
+ - a [runtime_value]
+ - a [string]
+ - an [environment]
+ - an [expression_continuation] *)
+ | Invocation_Ek :
+ runtime_value
+ -> string
+ -> environment
+ -> expression_continuation
+ -> expression_continuation
+
+ (** The constructor receives the following parameters:
+
+ - a [string]
+ - an [expression_continuation] *)
+ | Property_Get_Ek :
+ string
+ -> expression_continuation
+ -> expression_continuation
+
+(** TODO(dmitryas): Write descriptive comments. *)
+with statement_continuation : Set :=
+
+ (** The constructor receives the following parameters:
+
+ - an [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]
+ - an [expression_continuation]
+ - a [statement_continuation] *)
+ | Block_Sk :
+ list statement
+ -> environment
+ -> expression_continuation
+ -> statement_continuation
+ -> statement_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;
+ - an [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;
+ - an [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:
+
+ - an [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,
+ step (Exec_Configuration
+ (S_Expression_Statement (Expression_Statement expr))
+ env ret_cont next_cont)
+ (Eval_Configuration expr env (Expression_Ek env ret_cont next_cont))
+
+ (** <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 cont entry,
+ env_get var_id env = Some entry ->
+ step (Eval_Configuration (E_Variable_Get (Variable_Get var_id)) env cont)
+ (Value_Passing_Configuration 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 name arg env cont ref,
+ step (Eval_Configuration
+ (E_Invocation_Expression (IE_Method_Invocation
+ (Method_Invocation rcvr (Name name) (Arguments arg) ref)))
+ env cont)
+ (Eval_Configuration rcvr env
+ (Method_Invocation_Ek name arg env cont))
+
+ (** <MethodInvocationEK(name, arg, ρ, κE), rcvrVal)pass ==>
+ <arg, ρ, InvocationEK(rcvrVal, name, ρ, κE)>eval *)
+ | Pass_Method_Invocation_Ek :
+ forall name arg env cont val,
+ step (Value_Passing_Configuration
+ (Method_Invocation_Ek name arg env cont) val)
+ (Eval_Configuration arg env (Invocation_Ek val name env cont))
+
+ (** <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 name env ret_cont arg_val body env' next_cont
+ intf type proc_desc proc var_id var_type var_init ret_type null_val,
+ (* TODO(dmitryas): Add the mapping: this -> rcvr_val to env'. *)
+ value_of_type rcvr_val intf type ->
+ List.In proc_desc (procedures intf) ->
+ NatMap.MapsTo (pr_ref proc_desc) proc FE ->
+ proc = Function_Node (Variable_Declaration var_id var_type var_init)
+ ret_type body ->
+ env' = env_extend var_id arg_val empty_env ->
+ next_cont = Exit_Sk ret_cont null_val ->
+ value_of_type null_val (mk_interface nil) None ->
+ step (Value_Passing_Configuration
+ (Invocation_Ek rcvr_val name env ret_cont) 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 name env cont,
+ step (Eval_Configuration (E_Property_Get (Property_Get rcvr (Name name)))
+ env cont)
+ (Eval_Configuration rcvr env (Property_Get_Ek name cont))
+
+ (** <PropertyGetEK(name, κE), rcvrVal)pass ==> <κE, f>pass,
+ where f = methods(class(rcvrVal))(name) *)
+ | Pass_Property_Get_Ek :
+ forall name cont rcvr_val rcvr_intf rcvr_type func_val proc_desc,
+ value_of_type rcvr_val rcvr_intf rcvr_type ->
+ List.In proc_desc (procedures rcvr_intf) ->
+ (pr_name proc_desc) = name ->
+ value_of_type
+ func_val
+ (mk_interface (proc_desc :: nil))
+ (Some (DT_Function_Type (pr_type proc_desc))) ->
+ step (Value_Passing_Configuration (Property_Get_Ek name cont) rcvr_val)
+ (Value_Passing_Configuration cont func_val)
+
+ (** <ExitSK(κE, val), ρ>forward ==> <κE, val>pass *)
+ | Forward_Exit_Sk :
+ forall cont val env,
+ step (Forward_Configuration (Exit_Sk cont val) env)
+ (Value_Passing_Configuration cont val)
+
+ (** <ConstructorInvocation(cls), ρ, κE>eval ==> <κE, newVal>pass,
+ where newVal = new runtime value of syntactic type cls *)
+ | Eval_Constructor_Invocation :
+ forall env cont new_val intf type proc_desc,
+ value_of_type new_val intf type ->
+ List.In proc_desc (procedures intf) ->
+ step (Eval_Configuration
+ (E_Invocation_Expression (IE_Constructor_Invocation
+ (Constructor_Invocation (pr_ref proc_desc))))
+ env cont)
+ (Value_Passing_Configuration cont new_val).
+
+
+End OperationalSemantics.