Theory Source_Activation_Sound

theory Source_Activation_Sound
  imports "Voblint_Framework.Activation_Backbone" "Voblint_Compile.Source_To_Trace"
begin

section ‹End-to-end source-level activation soundness›

text ‹
  A reachable store of a compiled source program is bounded by the abstract analysis at the stable
  activation context of the trace that produced it.  The composition joins the stack-faithful source
  bridge ‹source_store_in_activation_collect› with ‹activation_collect_sound›.

  The cap-consuming theorems read the abstract map through a supplied concretization ‹γ⇩M›
  instead of fixing it to ‹'a::numeric_domain abs_state›/‹γ _›:
  the cap is the only thing they touch, so a reachability-lifted map fits as readily as a raw one.
  The backbone corollaries below read it at \<^const>‹gamma_state›, which is what
  ‹activation_collect_sound› produces.
›

theorem source_sound_from_collecting_cap:
  fixes sg :: "pp × 'c + 'g ⇒ 'M"
    and γ⇩M :: "'M ⇒ store set"
    and adm :: "'c context_policy" and c⇩0 :: 'c
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (residual, s, frs)"
    and has_ctx: "⋀t. t ∈ 𝒯⇘𝒢,compile_prog Pi ps,S⇙
                   ⟹ ∃c. activation_context_rel 𝒢 adm c⇩0 (compile_prog Pi ps) t c"
    and cap: "⋀v ctx. 𝒜⇘𝒢,adm,c⇩0,compile_prog Pi ps,S⇙ v ctx
                       ⊆ γ⇩M (sg (Inl (v, ctx)))"
  shows "∃v stk t c. Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                   ∧ activation_context_rel 𝒢 adm c⇩0 (compile_prog Pi ps) t c
                   ∧ s ∈ γ⇩M (sg (Inl (v, c)))"
proof -
  let ?g = "compile_prog Pi ps"
  from source_store_in_activation_collect
         [where adm=adm and c⇩0=c⇩0,
          OF wf s0 run has_ctx]
  obtain v stk t c where m:
    "Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)"
    and ck: "activation_context_rel 𝒢 adm c⇩0 ?g t c"
    and mem: "s ∈ 𝒜⇘𝒢,adm,c⇩0,?g,S⇙ v c"
    by blast
  have "s ∈ γ⇩M (sg (Inl (v, c)))"
    using cap[of v c] mem by blast
  then show ?thesis using m ck by blast
qed

text ‹The witness-free specialisation of the composition at top-level program points: an empty
  source frame stack lands at the fixed seed context, no \<^typ>‹activation_trace› witness exposed.›
theorem source_sound_toplevel_from_collecting_cap:
  fixes sg :: "pp × 'c + 'g ⇒ 'M"
    and γ⇩M :: "'M ⇒ store set"
    and adm :: "'c context_policy" and c⇩0 :: 'c
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (residual, s, [])"
    and cap: "⋀v ctx. 𝒜⇘𝒢,adm,c⇩0,compile_prog Pi ps,S⇙ v ctx
                       ⊆ γ⇩M (sg (Inl (v, ctx)))"
  shows "∃v. Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, []) ≈ (v, s, [])
             ∧ s ∈ γ⇩M (sg (Inl (v, c⇩0)))"
proof -
  let ?g = "compile_prog Pi ps"
  from source_toplevel_in_activation_collect
         [where adm=adm and c⇩0=c⇩0, OF wf s0 run]
  obtain v where m: "Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, []) ≈ (v, s, [])"
    and mem: "s ∈ 𝒜⇘𝒢,adm,c⇩0,?g,S⇙ v c⇩0" by blast
  have "s ∈ γ⇩M (sg (Inl (v, c⇩0)))" using cap[of v c⇩0] mem by blast
  then show ?thesis using m by blast
qed

subsection ‹Backbone corollaries: discharge the five coverage obligations to build the cap›

text ‹
  Given entry, edge, call, combine and totality obligations on the abstract map,
  ‹activation_coverage› builds the cap and the composition above yields
  source-level soundness. The node-collect variants restate it per CFG node.
›

theorem source_activation_sound:
  fixes sg :: "pp × 'c + 'g ⇒ 'a::numeric_domain abs_state"
    and adm :: "'c context_policy" and c⇩0 :: 'c
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (residual, s, frs)"
    and ENTRY_G: "⋀x. x ∈ S ⟹ x ∈ γ (sg (Inl (cfg_entry (compile_prog Pi ps), c⇩0)))"
    and EDGE: "⋀u a v c x x'. (u, a, v) ∈ intra (compile_prog Pi ps)
        ⟹ x ∈ γ (sg (Inl (u, c))) ⟹ x' ∈ edge_step a x
        ⟹ x' ∈ γ (sg (Inl (v, c)))"
    and CALL: "⋀u dst pars args p cont c c' x.
        (u, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)
        ⟹ x ∈ γ (sg (Inl (u, c)))
        ⟹ c' ∈ adm u c (call_info_of (CallEdge dst pars args) p) x
              (call_enter 𝒢 (CallEdge dst pars args) x)
        ⟹ call_enter 𝒢 (CallEdge dst pars args) x ∈ γ (sg (Inl (FunctionEntry p, c')))"
    and COMB: "⋀cl dst pars args p cont c1 c' p' x t es.
        (cl, CallEdge dst pars args, FunctionEntry p, cont) ∈ calls (compile_prog Pi ps)
        ⟹ x ∈ γ (sg (Inl (cl, c1)))
        ⟹ admits_call_context 𝒢 (compile_prog Pi ps) adm cl c1 p' x es c'
        ⟹ t ∈ γ (sg (Inl (FunctionResult p, c')))
        ⟹ combine_collect 𝒢 dst x t ∈ γ (sg (Inl (cont, c1)))"
    and TOTAL: "call_context_total_on (λv c. γ (sg (Inl (v, c)))) adm 𝒢 (compile_prog Pi ps)"
  shows "∃v stk t c. Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                   ∧ activation_context_rel 𝒢 adm c⇩0 (compile_prog Pi ps) t c
                   ∧ s ∈ γ (sg (Inl (v, c)))"
proof -
  interpret G: activation_coverage "compile_prog Pi ps" S "λv c. γ (sg (Inl (v, c)))" adm c⇩0 𝒢
    by (standard; blast intro: ENTRY_G EDGE CALL COMB TOTAL)
  have cap: "⋀v ctx. 𝒜⇘𝒢,adm,c⇩0,compile_prog Pi ps,S⇙ v ctx
                     ⊆ γ (sg (Inl (v, ctx)))"
    by (rule activation_collect_sound[OF G.activation_coverage_axioms])
  have has_ctx: "⋀t. t ∈ 𝒯⇘𝒢,compile_prog Pi ps,S⇙
                   ⟹ ∃c. activation_context_rel 𝒢 adm c⇩0 (compile_prog Pi ps) t c"
    using G.valid_activation_trace_has_context by blast
  show ?thesis
    by (rule source_sound_from_collecting_cap[where γ⇩M=gamma_state,
          OF wf s0 run has_ctx cap])
qed

subsection ‹Monovariant source bridge into the trace collecting›

text ‹
  The context-forgetting specialisation projects the activation collector at trivial routing
  directly to \<^const>‹node_collect› via ‹activation_collect_le_node_collect›.
›

theorem source_reaches_node_collect:
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (residual, s, frs)"
  shows "∃v stk. Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                 ∧ s ∈ 𝒞⇘𝒢,compile_prog Pi ps,S⇙ v"
proof -
  let ?g = "compile_prog Pi ps"
  from source_store_in_activation_collect_of_fun
         [where f = "λ_ _ _. ()" and c⇩0 = "()",
          OF wf s0 run]
  obtain v stk t c where m:
    "Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)"
    and "activation_context_of (λ_ _ _. ()) () t = c"
    and mem: "s ∈ 𝒜⇘𝒢,context_policy_of_fun (λ_ _ _. ()),(),?g,S⇙ v c"
    by blast
  have "s ∈ 𝒞⇘𝒢,?g,S⇙ v"
    using mem by (rule subsetD[OF activation_collect_le_node_collect])
  then show ?thesis using m by blast
qed

text ‹The monovariant counterpart of ‹source_sound_from_collecting_cap›: the cap is stated on
  \<^const>‹node_collect› alone, so there is no context index for a caller to instantiate.  This is
  the shape a whole-program analysis result supplies, whose per-node bound has already forgotten
  the context.›

theorem source_sound_from_node_collect_cap:
  fixes G :: "pp ⇒ store set"
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (residual, s, frs)"
    and cap: "⋀v. 𝒞⇘𝒢,compile_prog Pi ps,S⇙ v ⊆ G v"
  shows "∃v stk. Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)
                 ∧ s ∈ G v"
proof -
  from source_reaches_node_collect[OF wf s0 run]
  obtain v stk where m: "Pi, compile_prog Pi ps, prog_main_name ⊢ (residual, s, frs) ≈ (v, s, stk)"
    and mem: "s ∈ 𝒞⇘𝒢,compile_prog Pi ps,S⇙ v" by blast
  have "s ∈ G v" using cap[of v] mem by blast
  then show ?thesis using m by blast
qed

subsection ‹Completed runs reach a procedure result›

text ‹
  A source run that has completed at the top level (residual \<^const>‹SKIP›, empty frame stack)
  is collected at the \<^const>‹FunctionResult› of the activation it completed.  Two structural
  facts do the work, both from the CFG layer: the located node reaches its fragment exit along
  store-preserving intra flow (‹compile_control_at_SKIP_exit_path›), and \<^const>‹compiled_at›
  supplies the fall-through \<^term>‹EA_Ret None p› edge from that exit into
  \<^term>‹FunctionResult p›.

  The witness is kept: the completing activation is the ∗‹root› one (empty frame stack, so
  \<^const>‹caller_of› is \<^const>‹None›), which is what pins its procedure --- see
  ‹source_completes_node_collect_exit›.  Projecting into \<^const>‹node_collect› first would lose
  that: the collection at a \<^const>‹FunctionResult› deliberately merges every activation of
  that procedure.
›

theorem source_completes_valid_activation_trace_result:
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (SKIP (), s, [])"
  shows "∃t p. t ∈ 𝒯⇘𝒢,compile_prog Pi ps,S⇙
               ∧ caller_of t = None
               ∧ fst (hd (path_of t)) = cfg_entry (compile_prog Pi ps)
               ∧ sink_node t = FunctionResult p
               ∧ sink_store t = s"
proof -
  let ?g = "compile_prog Pi ps"
  from source_run_has_activation_trace[OF wf s0 run]
  obtain v stk t where sim: "Pi, ?g, prog_main_name ⊢ (SKIP (), 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 hd_t: "fst (hd (path_of t)) = cfg_entry ?g"
    by (rule valid_activation_trace_caller_None_entry[OF tv cof])
  ― ‹the located node of a completed activation is its procedure's result›
  from sim obtain p body_p k n where
    ca: "control_at Pi p body_p k n (SKIP ()) v" and cat: "compiled_at Pi ?g p body_p k n"
    by blast
  from cat obtain n' en E K where
    cc: "compile Pi p body_p k n = (n', en, E, K)" and Esub: "E ⊆ intra ?g"
    and ret: "(k, EA_Ret None p, FunctionResult p) ∈ intra ?g"
    by blast
  ― ‹the whole extension is intra flow, so it stays inside this same (root) activation›
  have path_to_ret: "intra_path ?g (sink_node t, sink_store t) (FunctionResult p, s)"
  proof -
    have a: "intra_path ?g (sink_node t, sink_store t) (k, s)"
      using compile_control_at_SKIP_exit_path[OF ca cc Esub] sn ss by simp
    have b: "intra_path ?g (k, s) (FunctionResult p, s)"
      by (rule intra_path_single[OF ret]) simp
    from a b show ?thesis by (rule star_trans)

  qed
  from valid_activation_trace_intra_path_extend[OF path_to_ret tv]
  obtain t' where t'v: "t' ∈ 𝒯⇘𝒢,?g,S⇙" and t'n: "sink_node t' = FunctionResult p"
    and t's: "sink_store t' = s" and t'c: "caller_of t' = caller_of t"
    and t'h: "fst (hd (path_of t')) = fst (hd (path_of t))" by blast
  show ?thesis
  proof (intro exI conjI)
    show "t' ∈ 𝒯⇘𝒢,?g,S⇙" by (rule t'v)
    show "caller_of t' = None" using t'c cof by simp
    show "fst (hd (path_of t')) = cfg_entry ?g" using t'h hd_t by simp
    show "sink_node t' = FunctionResult p" by (rule t'n)
    show "sink_store t' = s" by (rule t's)
  qed
qed

text ‹Whole-program completion.  The completing activation is the root one, so it entered at
  \<^term>‹FunctionEntry prog_main_name›; activation procedure locality
  (‹valid_activation_trace_entry_result_eq›) then forces its result node to be
  \<^term>‹FunctionResult prog_main_name› ‹= cfg_exit›.  No assumption about the
  ∗‹number› of declared procedures is needed: a program may call as many as it likes.›

corollary source_completes_node_collect_exit:
  assumes wf: "wf_compile_input 𝒢 Pi ps"
    and s0: "s0 ∈ S"
    and run: "𝒢, Pi ⊢ (main_body Pi, s0, []) →⇩p⇧* (SKIP (), s, [])"
  shows "s ∈ 𝒞⇘𝒢,compile_prog Pi ps,S⇙
              (cfg_exit (compile_prog Pi ps))"
proof -
  let ?g = "compile_prog Pi ps"
  from source_completes_valid_activation_trace_result[OF wf s0 run]
  obtain t p where tv: "t ∈ 𝒯⇘𝒢,?g,S⇙" and hd_t: "fst (hd (path_of t)) = cfg_entry ?g"
    and sn: "sink_node t = FunctionResult p" and ss: "sink_store t = s" by blast
  have "fst (hd (path_of t)) = FunctionEntry prog_main_name"
    using hd_t by (simp add: compile_prog_def Let_def split: prod.splits)
  from valid_activation_trace_entry_result_eq[OF wf tv this sn] have "prog_main_name = p" .
  with sn ss tv show ?thesis
    using node_collect_I by fastforce
qed

end