Theory Voblint_Compile.Source_To_Trace

theory Source_To_Trace
  imports Procedure_Ownership Simulation_Preservation "Voblint_CFG.Activation_Trace_Collect"
begin

section ‹A source run is an activation trace›

text ‹
  What the session is for.  A graph configuration is tied to a valid activation trace: the
  activation currently running ∗‹is› the trace, and the runtime frame stack is exactly
  its chain of callers.  Each \<^const>‹cstep› rule lines up with one \<^const>‹valid_activation_trace›
  constructor, so advancing the graph by an edge extends the trace by a step.

  Composed with the simulation, this turns a run of the source program into a trace, and
  so turns any store the source can reach into a member of the collecting semantics at
  that node.  Those are the statements the soundness session consumes; everything else in
  this session exists to make them true.
›

subsection ‹The representation invariant›

text ‹‹stack_repr› walks \<^const>‹caller_of› in lockstep with the runtime frame list: each
  \<^type>‹cframe› ‹(cont, dst, s)› pins the caller activation ‹caller› --- its frozen store
  ‹sink_store caller = s› --- and records the concrete \<^const>‹calls› edge that spawned the child,
  whose callee \<^term>‹FunctionEntry p› equals the child's (path-invariant) entry node.›
inductive stack_repr :: "cfg ⇒ cframe list ⇒ activation_trace ⇒ bool" for g where
  empty [intro]: "caller_of t = None ⟹ stack_repr g [] t"
| frame [intro]: "caller_of t = Some caller ⟹ sink_store caller = s
          ⟹ fst (hd (path_of t)) = FunctionEntry p
          ⟹ (sink_node caller, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls g
          ⟹ stack_repr g stk caller
          ⟹ stack_repr g ((cont, dst, s) # stk) t"


text ‹Inversion by the shape of the runtime stack.  A frame's clause recurses on the shorter
  stack, so it stays plain ‹[elim]›; an empty stack has only one clause and is ‹[elim!]›.›
inductive_cases stack_repr_NilE [elim!]: "stack_repr g [] t"
inductive_cases stack_repr_ConsE [elim]: "stack_repr g (cf # stk) t"

text ‹‹activation_trace_repr› pins a valid activation trace to a located configuration: the trace's sink is the current
  node/store, and its caller chain is the runtime stack.›
definition activation_trace_repr ::
  "(vname ⇒ bool) ⇒ cfg ⇒ store set ⇒ cconf ⇒ activation_trace ⇒ bool" where
  "activation_trace_repr 𝒢 g S cf t = (case cf of (v, s, stk) ⇒
     t ∈ 𝒯⇘𝒢,g,S⇙ ∧ sink_node t = v ∧ sink_store t = s ∧ stack_repr g stk t)"

definition located_activation_trace :: "(vname ⇒ bool) ⇒ cfg ⇒ store set ⇒ cconf ⇒ bool" where
  "located_activation_trace 𝒢 g S cf = (∃t. activation_trace_repr 𝒢 g S cf t)"

text ‹‹stack_repr› reads only the top \<^const>‹caller_of› and the path-invariant entry node,
  so it transfers across activations sharing both (an \<^const>‹extend› appends --- entry
  unchanged --- and a \<^const>‹Resume› prepends the same activation's path --- entry
  unchanged).›
lemma stack_repr_cong:
  "stack_repr g stk t1 ⟹ caller_of t2 = caller_of t1
   ⟹ fst (hd (path_of t2)) = fst (hd (path_of t1)) ⟹ stack_repr g stk t2"
  by (cases rule: stack_repr.cases) auto

subsection ‹The return step›

text ‹The load-bearing case.  A \<^const>‹cstep› return pops the top frame; ‹stack_repr›
  identifies the caller ‹c› (\<^const>‹caller_of› recovers it) and its spawning \<^const>‹calls›
  edge, whose callee \<^term>‹FunctionEntry q› matches the returning \<^term>‹FunctionResult q› by
  ‹valid_activation_trace_entry_result_eq› --- so the trace composes by ‹valid_activation_trace.ret›, and the combined
  store equals the \<^const>‹cstep› store.›
lemma activation_trace_repr_Return:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and rep: "activation_trace_repr 𝒢 (compile_prog Π ps) S
                  (FunctionResult q, tst, (cont, dst, caller) # stk) t0"
  shows "activation_trace_repr 𝒢 (compile_prog Π ps) S
           (cont, combine_collect 𝒢 dst caller tst, stk)
           (Resume (the (caller_of t0)) t0
              (path_of (the (caller_of t0)) @ [(cont, combine_collect 𝒢 dst caller tst)]))"
proof -
  let ?g = "compile_prog Π ps"
  from rep have t0v: "t0 ∈ 𝒯⇘𝒢,?g,S⇙" and sn0: "sink_node t0 = FunctionResult q"
    and ss0: "sink_store t0 = tst"
    and stk0: "stack_repr ?g ((cont, dst, caller) # stk) t0"
    by (auto simp: activation_trace_repr_def)
  from stk0 obtain c p pars args where cof: "caller_of t0 = Some c"
    and ssc: "sink_store c = caller" and entryp: "fst (hd (path_of t0)) = FunctionEntry p"
    and edge: "(sink_node c, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls ?g"
    and stkc: "stack_repr ?g stk c"
    by (cases rule: stack_repr.cases) auto
  have cvalid: "c ∈ 𝒯⇘𝒢,?g,S⇙" using valid_activation_trace_caller_valid[OF t0v cof] .
  have pq: "p = q" using valid_activation_trace_entry_result_eq[OF wf t0v entryp sn0] .
  have cthe: "the (caller_of t0) = c" using cof by simp
  let ?r = "combine_collect 𝒢 dst caller tst"
  let ?t' = "Resume c t0 (path_of c @ [(cont, ?r)])"
  have edge_q: "(sink_node c, CallEdge dst pars args, FunctionEntry q, cont) ∈ calls ?g"
    using edge pq by simp
  have valid': "?t' ∈ 𝒯⇘𝒢,?g,S⇙"
    using valid_activation_trace.ret[OF t0v cof sn0 edge_q] ssc ss0 by simp
  have sn': "sink_node ?t' = cont" by (simp add: sink_node_def)
  have ss': "sink_store ?t' = ?r" by (simp add: sink_store_def)
  have entry': "fst (hd (path_of ?t')) = fst (hd (path_of c))"
    using valid_activation_trace_path_nonempty[OF cvalid] by simp
  have stk': "stack_repr ?g stk ?t'"
    using stack_repr_cong[OF stkc, of ?t'] entry' by simp
  show ?thesis
    unfolding cthe using valid' sn' ss' stk' by (simp add: activation_trace_repr_def)
qed

subsection ‹The invariant is preserved by located CFG steps›

text ‹Each \<^const>‹cstep› rule maps to one \<^const>‹valid_activation_trace› constructor: intra ‹↦›
  \<^const>‹extend›, call ‹↦› \<^const>‹Call›, return ‹↦› \<^const>‹Resume› (‹activation_trace_repr_Return›).›
lemma cstep_preserves_activation_trace_repr:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and step: "𝒢, compile_prog Π ps ⊢ cf →⇩c cf'"
    and rep: "activation_trace_repr 𝒢 (compile_prog Π ps) S cf t"
  shows "∃t'. activation_trace_repr 𝒢 (compile_prog Π ps) S cf' t'"
  using step rep
proof (cases rule: cstep.cases)
  case (Intra u a v s' s stk')
  let ?g = "compile_prog Π ps"
  from rep have tv: "t ∈ 𝒯⇘𝒢,?g,S⇙" and sn: "sink_node t = u"
    and ss: "sink_store t = s"
    and str: "stack_repr ?g stk' t"
    using Intra by (auto simp: activation_trace_repr_def)
  have e1: "(sink_node t, a, v) ∈ intra ?g" using Intra sn by simp
  have e2: "s' ∈ edge_step a (sink_store t)" using Intra ss by simp
  have "extend t (v, s') ∈ 𝒯⇘𝒢,?g,S⇙" using valid_activation_trace.intra[OF tv e1 e2] .
  moreover have "stack_repr ?g stk' (extend t (v, s'))"
    using stack_repr_cong[OF str] valid_activation_trace_path_nonempty[OF tv] by simp
  ultimately have "activation_trace_repr 𝒢 ?g S (v, s', stk') (extend t (v, s'))"
    by (simp add: activation_trace_repr_def)
  then show ?thesis using Intra by auto
next
  case (Call u dst pars actuals q cont s stk')
  let ?g = "compile_prog Π ps"
  from rep have tv: "t ∈ 𝒯⇘𝒢,?g,S⇙" and sn: "sink_node t = u"
    and ss: "sink_store t = s"
    and str: "stack_repr ?g stk' t"
    using Call by (auto simp: activation_trace_repr_def)
  have edge: "(sink_node t, CallEdge dst pars actuals, FunctionEntry q, cont) ∈ calls ?g"
    using Call sn by simp
  let ?child = "Call t [(FunctionEntry q, call_enter 𝒢 (CallEdge dst pars actuals) s)]"
  have child_valid: "?child ∈ 𝒯⇘𝒢,?g,S⇙"
    using valid_activation_trace.call[OF tv edge] ss by simp
  have "stack_repr ?g ((cont, dst, s) # stk') ?child"
  proof (rule stack_repr.frame)
    show "caller_of ?child = Some t" by simp
    show "sink_store t = s" using ss .
    show "fst (hd (path_of ?child)) = FunctionEntry q" by simp
    show "(sink_node t, CallEdge dst pars actuals, FunctionEntry q, cont) ∈ calls ?g"
      using edge .
    show "stack_repr ?g stk' t" using str .
  qed
  with child_valid have "activation_trace_repr 𝒢 ?g S
      (FunctionEntry q, call_enter 𝒢 (CallEdge dst pars actuals) s,
       (cont, dst, s) # stk') ?child"
    by (simp add: activation_trace_repr_def sink_node_def sink_store_def)
  then show ?thesis using Call by auto
next
  case (Return q tst cont dst caller stk')
  from rep Return(1)
  have rep': "activation_trace_repr 𝒢 (compile_prog Π ps) S
                (FunctionResult q, tst, (cont, dst, caller) # stk') t" by simp
  from activation_trace_repr_Return[OF wf rep'] show ?thesis using Return(2) by auto
qed

lemma located_activation_trace_entry:
  assumes "s ∈ S"
  shows "located_activation_trace 𝒢 g S (cfg_entry g, s, [])"
proof -
  have "activation_trace_repr 𝒢 g S (cfg_entry g, s, []) (Root [(cfg_entry g, s)])"
    using assms
    by (auto simp: activation_trace_repr_def sink_node_def sink_store_def
      valid_activation_trace.root)
  then show ?thesis by (auto simp: located_activation_trace_def)
qed

lemma cstep_preserves_located_activation_trace:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and "located_activation_trace 𝒢 (compile_prog Π ps) S cf"
    and "𝒢, compile_prog Π ps ⊢ cf →⇩c cf'"
  shows "located_activation_trace 𝒢 (compile_prog Π ps) S cf'"
proof -
  from assms(2) obtain t where "activation_trace_repr 𝒢 (compile_prog Π ps) S cf t"
    by (auto simp: located_activation_trace_def)
  then obtain t' where "activation_trace_repr 𝒢 (compile_prog Π ps) S cf' t'"
    using cstep_preserves_activation_trace_repr[OF wf assms(3)] by blast
  then show ?thesis by (auto simp: located_activation_trace_def)
qed

lemma csteps_preserve_located_activation_trace:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and "located_activation_trace 𝒢 (compile_prog Π ps) S cf"
    and "𝒢, compile_prog Π ps ⊢ cf →⇩c⇧* cf'"
  shows "located_activation_trace 𝒢 (compile_prog Π ps) S cf'"
  using assms(3) assms(2)
proof (induction rule: star.induct)
  case (refl a)
  then show ?case .
next
  case (step a b c)
  have "located_activation_trace 𝒢 (compile_prog Π ps) S b"
    by (rule cstep_preserves_located_activation_trace[OF wf step.prems step.hyps(1)])
  then show ?case by (rule step.IH)
qed

subsection ‹The initial main activation›

text ‹The program entry \<^term>‹FunctionEntry prog_main_name› is an ordinary ‹csim.Base›
  activation: the distinguished main procedure is declared in ‹Π› (‹wf_compile_input›), so its
  body fragment is certified by ‹procs_embedded_compile_prog›.  One \<^term>‹EA_Body› edge crosses
  from \<^term>‹FunctionEntry prog_main_name› to the body entry ‹en›, where the ‹Base› activation
  simulates the source ‹main_body Π›.›
lemma compile_prog_main_base:
  assumes wf: "wf_compile_input 𝒢 Π ps"
  obtains en where
    "(FunctionEntry prog_main_name, EA_Body prog_main_name, en) ∈ intra (compile_prog Π ps)"
    "Π, compile_prog Π ps, prog_main_name ⊢ (main_body Π, s, []) ≈ (en, s, [])"
proof -
  let ?g = "compile_prog Π ps"
  have pc: "procs_embedded Π ?g" by (rule procs_embedded_compile_prog[OF wf])
  have main_decl: "Π prog_main_name = Some (⦇formals = [], body = (main_body Π)⦈)"
    by (rule wf_compile_inputD(2)[OF wf])
  obtain k m en where
    cacc: "compiled_at Π ?g prog_main_name (body (⦇formals = [], body = (main_body Π)⦈)) k m"
      and ctrl: "control_at Π prog_main_name (body (⦇formals = [], body = (main_body Π)⦈)) k m
                   (body (⦇formals = [], body = (main_body Π)⦈)) en"
      and entry: "(FunctionEntry prog_main_name, EA_Body prog_main_name, en) ∈ intra ?g"
    by (rule procs_embedded_activation[OF pc main_decl])
  have bodyeq: "body (⦇formals = [], body = (main_body Π)⦈) = (main_body Π)" by simp
  have base: "Π, ?g, prog_main_name ⊢ (main_body Π, s, []) ≈ (en, s, [])"
    by (rule csim.Base[OF ctrl[unfolded bodyeq] cacc[unfolded bodyeq]])
  from entry base show ?thesis ..
qed

subsection ‹Top-level structural facts of the invariant›

text ‹A trace has no caller exactly when its activation is at the top level (empty runtime stack).›
lemma stack_repr_Nil_iff:
  "stack_repr g stk t ⟹ (stk = []) = (caller_of t = None)"
  by (cases rule: stack_repr.cases) auto

text ‹A callerless activation carries exactly the initial context, whatever the policy ---
  the ‹Root› case never consults ‹adm›, and the ‹Resume› case only forwards to the same
  callerless ancestor. No validity is needed: the two clauses involved name no edge.›
lemma activation_context_rel_caller_of_None:
  "caller_of t = None
   ⟹ activation_context_rel 𝒢 adm c⇩0 g t c ⟷ c = c⇩0"
  by (induction t) auto

subsection ‹The source bridge›

text ‹Composing the initial ‹csim.Base› with ‹csim_star› (the source-to-\<^const>‹cstep›
  simulation) and the located invariant: every source run produces a matching valid
  activation trace at the simulated node.›
theorem source_run_has_activation_trace:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (residual, s, frs)"
  shows "∃v stk t. Π, compile_prog Π ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                   ∧ activation_trace_repr 𝒢 (compile_prog Π ps) S (v, s, stk) t"
proof -
  let ?g = "compile_prog Π ps"
  have pc: "procs_embedded Π ?g" by (rule procs_embedded_compile_prog[OF wf])
  have swf: "return_safe (main_body Π)" by (rule wf_compile_input_return_safe[OF wf])
  obtain en where entry: "(FunctionEntry prog_main_name, EA_Body prog_main_name, en) ∈ intra ?g"
    and base: "Π, ?g, prog_main_name ⊢ (main_body Π, s0, []) ≈ (en, s0, [])"
    by (rule compile_prog_main_base[OF wf])
  have loc0:
    "located_activation_trace 𝒢 (compile_prog Π ps) S (FunctionEntry prog_main_name, s0, [])"
    using located_activation_trace_entry[where g = "compile_prog Π ps", OF s0] by simp
  have step0: "𝒢, ?g ⊢ (FunctionEntry prog_main_name, s0, []) →⇩c (en, s0, [])"
    by (rule cstep_body[OF entry])
  have loc_en: "located_activation_trace 𝒢 ?g S (en, s0, [])"
    by (rule cstep_preserves_located_activation_trace[OF wf loc0 step0])
  from csim_star[OF base pc swf run] obtain cf'
    where run_c: "𝒢, ?g ⊢ (en, s0, []) →⇩c⇧* cf'"
      and sim': "Π, ?g, prog_main_name ⊢ (residual, s, frs) ≈ cf'"
    by blast
  obtain v s' stk where cf': "cf' = (v, s', stk)" by (cases cf')
  have store: "s' = s" using csim_store_eq[OF sim'[unfolded cf']] by simp
  have loc_v: "located_activation_trace 𝒢 ?g S (v, s, stk)"
    using csteps_preserve_located_activation_trace[OF wf loc_en run_c] cf' store by simp
  from loc_v obtain t where "activation_trace_repr 𝒢 ?g S (v, s, stk) t"
    by (auto simp: located_activation_trace_def)
  then show ?thesis using sim' cf' store by blast
qed

text ‹The plain projected source bridge: a reachable source store lies in the activation-trace
  collecting \<^const>‹activation_collect› at the simulated node, in a context the witness
  trace carries. A relational policy may leave a trace without any context, so the bridge
  asks for one: ‹has_ctx› is what ‹activation_coverage›'s ‹TOTAL› buys downstream, and what a
  functional policy has outright (‹source_store_in_activation_collect_of_fun›).›
theorem source_store_in_activation_collect:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (residual, s, frs)"
    and has_ctx: "⋀t. t ∈ 𝒯⇘𝒢,compile_prog Π ps,S⇙
                   ⟹ ∃c. activation_context_rel 𝒢 adm c⇩0 (compile_prog Π ps) t c"
  shows "∃v stk t c. Π, compile_prog Π ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                   ∧ activation_trace_repr 𝒢 (compile_prog Π ps) S (v, s, stk) t
                   ∧ activation_context_rel 𝒢 adm c⇩0 (compile_prog Π ps) t c
                   ∧ s ∈ 𝒜⇘𝒢,adm,c⇩0,compile_prog Π ps,S⇙ v c"
proof -
  let ?g = "compile_prog Π ps"
  from source_run_has_activation_trace[OF wf s0 run] obtain v stk t
    where sim: "Π, ?g, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)"
      and rep: "activation_trace_repr 𝒢 ?g S (v, s, stk) t" by blast
  from rep have tv: "t ∈ 𝒯⇘𝒢,?g,S⇙" and sn: "sink_node t = v"
    and ss: "sink_store t = s"
    by (auto simp: activation_trace_repr_def)
  from has_ctx[OF tv] obtain c where tc: "activation_context_rel 𝒢 adm c⇩0 ?g t c" by blast
  have "s ∈ 𝒜⇘𝒢,adm,c⇩0,?g,S⇙ v c"
    using activation_collect_I[OF tv sn tc] ss by simp
  then show ?thesis using sim rep tc by blast
qed

text ‹A functional policy carries \<^const>‹activation_context_of›'s context on every valid activation trace, so it needs no
  context witness.›
corollary source_store_in_activation_collect_of_fun:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (residual, s, frs)"
  shows "∃v stk t c. Π, compile_prog Π ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                   ∧ activation_trace_repr 𝒢 (compile_prog Π ps) S (v, s, stk) t
                   ∧ activation_context_of f c⇩0 t = c
                   ∧ s ∈ 𝒜⇘𝒢,context_policy_of_fun f,c⇩0,compile_prog Π ps,S⇙ v c"
proof -
  let ?g = "compile_prog Π ps"
  from source_run_has_activation_trace[OF wf s0 run] obtain v stk t
    where sim: "Π, ?g, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)"
      and rep: "activation_trace_repr 𝒢 ?g S (v, s, stk) t" by blast
  from rep have tv: "t ∈ 𝒯⇘𝒢,?g,S⇙" and sn: "sink_node t = v"
    and ss: "sink_store t = s"
    by (auto simp: activation_trace_repr_def)
  have tc:
    "activation_context_rel 𝒢 (context_policy_of_fun f) c⇩0 ?g t (activation_context_of f c⇩0 t)"
    by (simp add: activation_context_rel_of_fun_iff[OF tv])
  have "s ∈ 𝒜⇘𝒢,context_policy_of_fun f,c⇩0,?g,S⇙ v
              (activation_context_of f c⇩0 t)"
    using activation_collect_I[OF tv sn tc] ss by simp
  then show ?thesis using sim rep by blast
qed

text ‹The witness-free top-level result: a store reached with an empty source frame stack lies in
  the activation collecting at the fixed seed context --- no \<^typ>‹activation_trace› witness and no context
  existential. This is the shape a user reads for main-level program points.›
theorem source_toplevel_in_activation_collect:
  assumes wf: "wf_compile_input 𝒢 Π ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Π ⊢ (main_body Π, s0, []) →⇩p⇧* (residual, s, [])"
  shows "∃v. Π, compile_prog Π ps, prog_main_name ⊢ (residual, s, []) ≈ (v, s, [])
             ∧ s ∈ 𝒜⇘𝒢,adm,c⇩0,compile_prog Π ps,S⇙ v c⇩0"
proof -
  let ?g = "compile_prog Π ps"
  from source_run_has_activation_trace[OF wf s0 run] obtain v stk t
    where sim: "Π, ?g, prog_main_name ⊢ (residual, s, []) ≈ (v, s, stk)"
      and rep: "activation_trace_repr 𝒢 ?g S (v, s, stk) t" by blast
  have stk0: "stk = []" using sim by blast
  from rep stk0 have tv: "t ∈ 𝒯⇘𝒢,?g,S⇙" and sn: "sink_node t = v"
    and ss: "sink_store t = s" and sr: "stack_repr ?g [] t"
    by (auto simp: activation_trace_repr_def)
  have cof: "caller_of t = None" using stack_repr_Nil_iff[OF sr] by simp
  have covered: "activation_context_rel 𝒢 adm c⇩0 ?g t c⇩0"
    by (simp add: activation_context_rel_caller_of_None[OF cof])
  have "s ∈ 𝒜⇘𝒢,adm,c⇩0,?g,S⇙ v c⇩0"
    using activation_collect_I[OF tv sn covered] ss by simp
  then show ?thesis using sim stk0 by blast
qed

section ‹The bridge is inhabited›

text ‹‹source_run_has_activation_trace› and the collecting corollaries all assume a well-formed compiler
  input, so the session ends by exhibiting one and running the bridge on it.  The zero-step
  run of the empty ‹main› is enough: it yields an actual node of an actual compiled graph and
  an actual \<^const>‹valid_activation_trace› witness, so none of the above is vacuously true.›

theorem source_run_has_activation_trace_witness:
  "∃v stk t. witness_pi, witness_cfg, prog_main_name ⊢ (SKIP (), s0, []) ≈ (v, s0, stk)
           ∧ activation_trace_repr (λ_. False) witness_cfg {s0} (v, s0, stk) t"
  using source_run_has_activation_trace[OF witness_wf singletonI star.refl] by simp

end