| (* 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.SetoidList. |
| |
| Require Import Common. |
| Require Import Syntax. |
| Require Import ObjectModel. |
| Require Import OperationalSemantics. |
| |
| Import Common.NatMapFacts. |
| |
| |
| Lemma maps_in_mapsto : |
| forall A (m : NatMap.t A) key, |
| NatMap.In key m -> |
| exists el, NatMap.MapsTo key el m. |
| Proof. |
| intros. |
| pose proof (NatMapFacts.find_mapsto_iff m key). |
| pose proof (NatMapFacts.in_find_iff m key). |
| unfold iff in H1. destruct H1 as [H1a H1b]. |
| pose proof (H1a H). |
| destruct (NatMap.find key m) eqn:?. |
| exists a. pose proof (H0 a). unfold iff in H2. destruct H2 as [H2a H2b]. |
| apply H2b. congruence. |
| contradiction. |
| Qed. |
| |
| |
| Section OperationalSemanticsSpec. |
| |
| |
| Variable CE : class_env. |
| |
| Variable FE : func_env. |
| |
| |
| (** Placeholder for the well-formedness properties of the program. *) |
| |
| (** Predicate for [class_env] [CE] being well-formed w.r.t. [func_env] [FE]. *) |
| 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. |
| |
| |
| Lemma runtime_value_interface_wf : |
| forall val intf type proc_desc, |
| value_of_type CE FE val intf type -> |
| List.In proc_desc (procedures intf) -> |
| NatMap.In (pr_ref proc_desc) FE. |
| Proof. |
| intros. destruct H. |
| |
| (* Case 1. Value of Interface Type. *) |
| apply program_wf with (class_id := class_id) (intf := intf). |
| apply NatMapFacts.find_mapsto_iff. auto. |
| auto. |
| |
| (* Case 2. Value of Function Type. *) |
| rewrite H1 in H0. |
| pose proof (List.in_inv H0). |
| destruct H6. |
| rewrite <- H6. auto. |
| pose proof (List.in_nil H6). contradiction. |
| |
| (* Case 3. Null Value. *) |
| rewrite H in H0. pose proof (List.in_nil H0). contradiction. |
| Qed. |
| |
| |
| Theorem step_configuration_wf : |
| forall conf1, configuration_wf CE FE conf1 -> |
| exists conf2, step CE FE conf1 conf2. |
| Proof. |
| intros. |
| |
| (* Construct the second configuration from the preconditions of |
| well-formedness of the first configuration. *) |
| destruct H. |
| |
| (* Case 1. Eval Variable Get. *) |
| unfold env_in in H. |
| destruct ( |
| List.find |
| (fun entry : environment_entry => Nat.eqb var_id (variable_id entry)) |
| env |
| ) eqn:?; try contradiction. |
| exists (Value_Passing_Configuration cont (value e)). |
| constructor. |
| unfold env_get. auto. |
| |
| (* Case 2. Eval Method Invocation. *) |
| exists (Eval_Configuration rcvr env |
| (Method_Invocation_Ek name arg env cont)). |
| constructor. |
| |
| (* Case 3. Eval Property Get. *) |
| exists (Eval_Configuration rcvr env (Property_Get_Ek name cont)). |
| constructor. |
| |
| (* Case 4. Eval Constructor Invocation. *) |
| pose proof (maps_in_mapsto interface CE class_id H). |
| destruct H0 as (intf & H1). |
| set (type := DT_Interface_Type (Interface_Type class_id)). |
| set (new_val := mk_runtime_value (Some type)). |
| exists (Value_Passing_Configuration cont new_val). |
| constructor 14 with (intf := intf) (type := Some type); try auto. |
| constructor 1 with (class_id := class_id); try (simpl; auto). |
| apply NatMapFacts.find_mapsto_iff. auto. |
| |
| (* Case 5. Exec. *) |
| destruct stmt. |
| |
| (* Case 5.1. Exec Expression Statement. *) |
| destruct e. |
| exists (Eval_Configuration e env (Expression_Ek env ret_cont next_cont)). |
| constructor. |
| |
| (* Case 5.2. Exec Block. *) |
| destruct b. destruct l. |
| |
| (* Case 5.2.1. Exec Empty Block. *) |
| exists (Forward_Configuration next_cont env). |
| constructor. |
| |
| (* Case 5.2.2. Exec Non-Empty Block. *) |
| exists (Exec_Configuration s env ret_cont |
| (Block_Sk l env ret_cont next_cont)). |
| constructor. |
| |
| (* Case 5.3. Exec Return Statement. *) |
| destruct r. |
| exists (Eval_Configuration e env ret_cont). |
| constructor. |
| |
| (* Case 5.4. Exec Variable Declaration. *) |
| destruct v. destruct o. |
| |
| (* Case 5.4.1. Exec Variable Declaration with Initializer. *) |
| exists (Eval_Configuration e env (Var_Declaration_Ek n env next_cont)). |
| constructor. |
| |
| (* Case 5.4.2. Exec Variable Declaration without Initializer. *) |
| set (null_val := mk_runtime_value None). |
| set (env' := env_extend n null_val env). |
| exists (Forward_Configuration next_cont env'). |
| constructor 15 with (null_val := null_val). |
| constructor 3. simpl. congruence. |
| simpl. congruence. |
| trivial. |
| |
| (* Case 6. Pass Value to MethodInvocationEK. *) |
| exists (Eval_Configuration arg env (Invocation_Ek val name env cont)). |
| constructor. |
| |
| (* Case 7. Pass Value to InvocationEK. *) |
| pose proof (runtime_value_interface_wf rcvr_val intf type proc_desc H). |
| pose proof (H2 H0). |
| apply maps_in_mapsto in H3. destruct H3 as (el & H4). |
| destruct el eqn:?. destruct v eqn:?. |
| set (env' := env_extend n arg_val empty_env). |
| set (null_val := mk_runtime_value None). |
| set (next_cont := Exit_Sk ret_cont null_val). |
| exists (Exec_Configuration s env' ret_cont next_cont). |
| constructor 10 with (intf := intf) (type := type) (proc_desc := proc_desc) |
| (func_node := el) (var_id := n) (var_type := d0) (var_init := o) |
| (ret_type := d) (null_val := null_val). |
| auto. |
| auto. |
| rewrite Heqf; auto. |
| rewrite Heqf; auto. |
| trivial. |
| trivial. |
| constructor. simpl. congruence. |
| simpl. congruence. |
| |
| (* Case 8. Pass Value to PropertyGetEK. *) |
| set (func_type := pr_type proc_desc). |
| set (func_proc_desc := |
| mk_procedure_desc "call" (pr_ref proc_desc) func_type). |
| set (func_val := mk_runtime_value (Some (DT_Function_Type func_type))). |
| exists (Value_Passing_Configuration cont func_val). |
| constructor 12 with (rcvr_intf := intf) (rcvr_type := type) |
| (rcvr_proc_desc := proc_desc) (func_proc_desc := func_proc_desc); try auto. |
| destruct func_type eqn:?. |
| constructor 2 with |
| (par_type := d) |
| (ret_type := d0) |
| (proc := func_proc_desc); (try (simpl; congruence)). |
| simpl. apply runtime_value_interface_wf with |
| (val := rcvr_val) (intf := intf) (type := type); auto. |
| |
| (* Case 9. Forward. *) |
| destruct cont. |
| |
| (* Case 9.1. Forward to Exit. *) |
| exists (Value_Passing_Configuration e r). |
| constructor. |
| |
| (* Case 9.2. Forward to the Next Statement in Block. *) |
| destruct l. |
| |
| (* Case 9.2.1. Block is Empty. *) |
| exists (Forward_Configuration cont e). |
| constructor. |
| |
| (* Case 9.2.2. Block is Non-Empty. *) |
| exists (Exec_Configuration s env e0 (Block_Sk l e e0 cont)). |
| constructor. |
| Qed. |
| |
| |
| End OperationalSemanticsSpec. |