(* * Copyright (c) 2017-present, * Programming Research Laboratory (ROPAS), Seoul National University, Korea * This software is distributed under the term of the BSD-3 clause license. *) (** * Correctness sub-proof (InsenLocal -- Valid *) Set Implicit Arguments. Require Import VocabA Global. Require SemInsenLocal ExtFin. Require Import UserProofType. Require Import vgtac. Module Make (Import PInput : PINPUT). Module InsenLocal := SemInsenLocal.Make PInput. Module EFin := ExtFin.Make PInput. Ltac dest_run_access := match goal with [H : context [run_access ?prm ?g ?n ?c ?mem] |- _] => let m := fresh "m" in let acc := fresh "acc" in let f := fresh "x" in remember (run_access prm g n c mem) as f; destruct f as [m acc] end. Section correctness. Variables (g : G.t) (Hg : G.wf g) (fis_mem: Mem.t) (amap : access_map) (orig_inputof inputof outputof : Table.t Mem.t) (Hvalid : valid g amap orig_inputof inputof outputof = true). Let s := fun idx : InsenLocal.index_t => let node := InsenLocal.node_of_index idx in let t := match InsenLocal.pos_of_index idx with | SemCommon.Inputof => inputof | SemCommon.Outputof => outputof end in table_find node t. Lemma get_valid_cfgs : valid_cfgs g amap inputof outputof = true. Proof. unfold valid in Hvalid. dest_bool. destruct Hvalid as [Hvalid1 _]. dest_bool. destruct Hvalid1 as [Hvalid1 _]. dest_bool. destruct Hvalid1 as [Hvalid1 _]. dest_bool. by destruct Hvalid1. Qed. Lemma get_valid_cfg : forall f cfg (Hfind: Some cfg = InterCfg.PidMap.find f (InterCfg.cfgs (icfg g))), valid_cfg g amap inputof outputof f cfg = true. Proof. assert (Hvalid_cfgs := get_valid_cfgs). unfold valid_cfgs in Hvalid_cfgs. i. apply InterCfg.PidMap.for_all_2 with (k:=f) (v:=cfg) in Hvalid_cfgs ; [ by auto | i; by subst | by apply InterCfg.PidMap.P.F.find_mapsto_iff ]. Qed. Lemma get_valid_cmds : forall f cfg (Hfind: Some cfg = InterCfg.PidMap.find f (InterCfg.cfgs (icfg g))), valid_cmds g amap inputof outputof f cfg. Proof. i. assert (Hcfg := get_valid_cfg _ Hfind). unfold valid_cfg in Hcfg. dest_bool. by destruct Hcfg. Qed. Lemma get_valid_cmd : forall cn cmd (Hget_cmd: Some cmd = InterCfg.get_cmd (G.icfg g) cn), valid_cmd g amap inputof outputof (InterNode.get_pid cn) (InterNode.get_node cn) cmd = true. Proof. unfold InterCfg.get_cmd. i. dest_trivial_match. assert (Hcmds := get_valid_cmds _ Heqcond). unfold valid_cmds in Hcmds. apply IntraCfg.NodeMap.for_all_2 with (k:=InterNode.get_node cn) (v:=cmd) in Hcmds ; [ by auto | i; by inversion Hk | by apply IntraCfg.NodeMap.P.F.find_mapsto_iff ]. Qed. Lemma get_valid_intra_edges : forall f cfg (Hfind: Some cfg = InterCfg.PidMap.find f (InterCfg.cfgs (icfg g))), valid_intra_edges inputof outputof f cfg. Proof. i. assert (Hcfg := get_valid_cfg _ Hfind). unfold valid_cfg in Hcfg. dest_bool. by destruct Hcfg. Qed. Lemma get_valid_intra_edge : forall f cfg (Hmapsto : InterCfg.PidMap.MapsTo f cfg (InterCfg.cfgs (G.icfg g))) n n' succs (Hsuccs : IntraCfg.NodeMap.MapsTo n succs (IntraCfg.succ cfg)) (Hn' : IntraCfg.NodeSet.In n' succs), valid_intra_edge inputof outputof f cfg n n' = true. Proof. i. apply InterCfg.PidMap.P.F.find_mapsto_iff in Hmapsto. symmetry in Hmapsto. assert (Hvalid_intra_edges := get_valid_intra_edges _ Hmapsto). unfold valid_intra_edges in Hvalid_intra_edges. apply IntraCfg.NodeMap.for_all_2 with (k:=n) (v:=succs) in Hvalid_intra_edges ; [|i; by inversion Hk|by auto]. apply IntraCfg.NodeSet.for_all_2 in Hvalid_intra_edges ; [|intros k k' Hk; by inversion Hk]. unfold IntraCfg.NodeSet.For_all in Hvalid_intra_edges. by apply Hvalid_intra_edges. Qed. Lemma get_valid_inter_edges : valid_inter_edges g amap inputof outputof = true. Proof. unfold valid in Hvalid. dest_bool. destruct Hvalid as [Hvalid1 _]. dest_bool. destruct Hvalid1 as [Hvalid1 _]. dest_bool. destruct Hvalid1 as [_ Hvalid1]. dest_bool. by destruct Hvalid1. Qed. Lemma get_valid_inter_edge : forall cn cn' succs (Hsuccs: InterCfg.NodeMap.MapsTo cn succs (InterCfg.succ (icfg g))) (Hcn' : InterCfg.NodeSet.In cn' succs), valid_inter_edge g amap inputof outputof cn cn' = true. Proof. i. assert (Hvalid_inter_edges := get_valid_inter_edges). unfold valid_inter_edges in Hvalid_inter_edges. apply InterCfg.NodeMap.for_all_2 with (k:=cn) (v:=succs) in Hvalid_inter_edges ; [|i; apply InterNode.eq_inv in Hk; by subst|by auto]. apply InterCfg.NodeSet.for_all_2 in Hvalid_inter_edges ; [|intros k k' Hk; apply InterNode.eq_inv in Hk; by subst]. unfold InterCfg.NodeSet.For_all in Hvalid_inter_edges. by apply Hvalid_inter_edges. Qed. Lemma get_valid_inter_accs : valid_inter_accs g amap = true. Proof. unfold valid in Hvalid. dest_bool. destruct Hvalid as [Hvalid1 _]. dest_bool. destruct Hvalid1 as [_ Hvalid1]. dest_bool. by destruct Hvalid1. Qed. Lemma cor_postfix_cmd : forall cn, InsenLocal.postfix_cmd g cn s. Proof. unfold InsenLocal.postfix_cmd; i. assert (Hvalid_cmd := get_valid_cmd _ Hcmd). unfold valid_cmd in Hvalid_cmd. dest_run_access; dest_if_dec; dest_if. symmetry in Heqcond; apply Mem.opt_le_prop in Heqcond. destruct cn; apply Mem.le_trans with m; [|by auto]. apply Mem.le_refl; apply Mem.eq_sym. rewrite run_only_access_same. apply Mem.eq_trans with (Acc.get_v (m, acc)); [by apply Mem.eq_refl|]. rewrite Heqx; by apply Mem.eq_refl. Qed. Lemma cor_postfix_intra_edge : forall cn, InsenLocal.postfix_intra_edge g cn s. Proof. unfold InsenLocal.postfix_intra_edge; i. inversion Hedge; subst. assert (Hvalid_intra_edge := get_valid_intra_edge Hcfg Hsuccs Hn'). unfold valid_intra_edge in Hvalid_intra_edge. dest_if ; [ elim Hcn_cond; unfold InterCfg.is_call_node ; rewrite (InterCfg.PidMap.find_1 Hcfg); s; rewrite <- Heqcond; reflexivity | dest_if; destruct cn; by apply Mem.opt_le_prop ]. Qed. Lemma cor_postfix_intra_call : forall cn, InsenLocal.postfix_intra_call g amap cn s. Proof. unfold InsenLocal.postfix_intra_call; i. destruct Hg as [_ [Hg_call_edge [_ [Hg_call_node [_ Hg_pred_succ]]]]]. assert (Hret_edge := Hg_call_edge _ _ _ Hedge Hretn). inversion Hret_edge. subst. assert (Hvalid_inter_edge := get_valid_inter_edge Hsuccs Hn'). unfold valid_inter_edge in Hvalid_inter_edge. unfold icfg in Hvalid_inter_edge. rewrite (Hg_call_node callee) in Hvalid_inter_edge. dest_if. unfold GenFunc.fail_inter_edge_no_callof in *. dest_trivial_match. assert (Hcn := InterCfg.returnof_1 _ Hg_pred_succ Hretn Heqcond0). apply InterNode.eq_inv in Hcn; subst. dest_if. dest_if. by apply Mem.opt_le_prop. Qed. Lemma cor_postfix_inter_call : forall cn, InsenLocal.postfix_inter_call g amap cn s. Proof. unfold InsenLocal.postfix_inter_call; i. inversion Hedge; subst. assert (Hvalid_inter_edge := get_valid_inter_edge Hsuccs Hn'). unfold valid_inter_edge in Hvalid_inter_edge. dest_if; [dest_if; by apply Mem.opt_le_prop|]. destruct Hg as [_ [_ [_ [_ [Hg_call_node _]]]]]. unfold G.is_exit_node in Hvalid_inter_edge. by rewrite (Hg_call_node cn callee Hedge) in Hvalid_inter_edge. Qed. Lemma cor_postfix_inter_ret : forall cn, InsenLocal.postfix_inter_ret g cn s. Proof. unfold InsenLocal.postfix_inter_ret; i; subst. inversion Hedge; subst. assert (Hvalid_inter_edge := get_valid_inter_edge Hsuccs Hn'). unfold valid_inter_edge in Hvalid_inter_edge. destruct Hg as [_ [_ [_ [Hg_call_node [_ Hg_pred_succ]]]]]. unfold icfg in Hvalid_inter_edge. rewrite (Hg_call_node p) in Hvalid_inter_edge. dest_if. unfold GenFunc.fail_inter_edge_no_callof in *. dest_trivial_match. assert (Hcn := InterCfg.returnof_1 _ Hg_pred_succ Hret Heqcond0). apply InterNode.eq_inv in Hcn; subst. dest_if. by apply Mem.opt_le_prop. Qed. Lemma cor_amap_run : InsenLocal.sound_amap_run g amap s. Proof. unfold InsenLocal.sound_amap_run; i. destruct cn as [f n]. unfold InterCfg.get_cmd in Hcmd. dest_trivial_match. unfold IntraCfg.get_cmd in Hcmd. assert (Hcmds := get_valid_cmds f Heqcond). unfold valid_cmds in Hcmds. apply IntraCfg.NodeMap.for_all_2 with (k:=n) (v:=cmd) in Hcmds ; [| i; by inversion Hk | symmetry in Hcmd ; by apply IntraCfg.NodeMap.P.F.find_mapsto_iff in Hcmd ]. unfold valid_cmd in Hcmds. unfold s. s. dest_run_access; dest_if_dec; dest_if. unfold Syn.pid_t, IntraNode.t in Heqx. rewrite <- Heqx. by apply l. Qed. Lemma cor_amap_reachable : InsenLocal.sound_amap_reachable g amap. Proof. unfold InsenLocal.sound_amap_reachable. induction 1. - apply Acc.le_refl. by apply Acc.eq_refl. - eapply Acc.le_trans; [by apply IHHr|]. assert (Haccs := get_valid_inter_accs). unfold valid_inter_accs in Haccs. inversion Hinter. apply InterCfg.NodeMap.for_all_2 with (k:=(p, n)) (v:=succs) in Haccs ; [| intros k k' [Hk1 Hk2]; destruct k, k'; simpl in Hk1; simpl in Hk2 ; inversion Hk1; inversion Hk2; reflexivity | by apply Hsuccs ]. apply InterCfg.NodeSet.for_all_2 in Haccs ; [| intros k k' [Hk1 Hk2]; destruct k, k'; simpl in Hk1; simpl in Hk2 ; inversion Hk1; inversion Hk2; reflexivity ]. assert (Hacc := Haccs (q, IntraNode.Entry) Hn'). simpl in Hacc. unfold valid_inter_acc, InterNode.is_entry_node, IntraNode.is_entry_node in Hacc. simpl in Hacc. dest_if ; [| destruct (IntraNode.eq_dec IntraNode.Entry IntraNode.Entry) ; [inversion Heqcond|elim f; by apply IntraNode.eq_refl]]. destruct (Acc.le_dec (get_access q amap) (get_access p amap)) ; [by auto|by inversion Hacc]. Qed. Lemma cor_extends' : EFin.extends' g orig_inputof (inputof, outputof). Proof. unfold valid in Hvalid. dest_bool. destruct Hvalid as [_ Hdens]. unfold valid_dens in Hdens. unfold EFin.extends'; i. apply InterCfg.PidMap.for_all_2 with (k:=f) (v:=cfg) in Hdens ; [| intros k k' Hk; subst; reflexivity | by auto ]. unfold valid_dens_cfg in Hdens. apply IntraCfg.NodeMap.for_all_2 with (k:=n) (v:=cmd) in Hdens ; [| intros k k' Hk; inversion Hk; reflexivity | by auto ]. unfold valid_dens_node in Hdens. unfold EFin.state_find, fst. unfold InterCfg.PidMap.key, IntraCfg.NodeMap.key. unfold IntraNode.t in Hdens. match goal with | [|- let '(_, _) := ?x in _] => remember x as p end. destruct p as [v acc_n]. dest_if. unfold EFin.extends_mem. intros k Hk. symmetry in Heqcond. eapply Mem.eq_wrt_1 in Heqcond; [|by apply Hk]. by auto. Qed. Lemma cor_extends : EFin.extends g orig_inputof s. Proof. eapply EFin.extends_trans; [by apply cor_extends'|]. unfold EFin.extends'', EFin.state_find, s; s; i. by apply Mem.eq_refl. Qed. Lemma correctness : exists s', InsenLocal.postfix g amap s' /\ InsenLocal.sound_amap g amap s' /\ EFin.extends g orig_inputof s'. Proof. i; exists s; split; [|split]. { repeat split. - by apply cor_postfix_cmd. - by apply cor_postfix_intra_edge. - by apply cor_postfix_intra_call. - by apply cor_postfix_inter_call. - by apply cor_postfix_inter_ret. } { split. - by apply cor_amap_run. - by apply cor_amap_reachable. } { by apply cor_extends. } Qed. End correctness. End Make.