Theory Nonrelational_Transfer

theory Nonrelational_Transfer
  imports
    Nonrelational_Ops
    "Voblint_Framework.Check_Answer"
    "Voblint_Result.DG_Analysis"
begin

section ‹What each kind of CFG edge does to one abstract value per variable›

text ‹
  A non-relational domain gives every variable one abstract value. Say what an
  expression evaluates to, what the whole-value element is, what ‹Min›/‹Max› do,
  and how a guard refines its operands, and every edge operation is already
  fixed: an assignment overwrites its target with the evaluated right-hand side, a
  return writes the same into the return variable, a guard runs the backward
  branch the refinement operations determine, procedure entry resets the callee
  frame to the whole-value element and binds the formals, and skip,
  procedure-body entry and check observation leave the store alone.

  ‹sound_nonrelational_ops› is the certificate for one \<^type>‹nonrelational_ops›
  bundle: the special operations are sound, the refinement operations form a
  reductive backward domain over the bundle's evaluator, and the queries are
  sound checks over the same evaluator. From it this theory states every edge
  operation once and proves each sound --- a concrete store described by the
  input is still described by the output --- ending in the transfer contract the
  analysis framework asks a domain for. ‹mono_nonrelational_ops› adds
  monotonicity for a bundle whose evaluator, special operations and refinement
  are monotone. A domain proves its capability certificates, interprets one of
  the two locales once at its bundle, and names the results; it proves nothing
  here again.

  ‹tf_abs› is the per-edge dispatcher these operations add up to, and
  ‹tf_abs_eq_generic› identifies it with \<^const>‹generic_tf_abs› at the derived
  branch, which is what lets ‹tf_st_for_commute› inherit the executable mirror's
  commutation instead of restating it.
›

locale sound_nonrelational_ops =
  sound_minmax_ops "n_special ops" "n_aval ops"
  + backward: sound_refinement "r_intersect (n_refine ops)" "n_aval ops"
      "r_tobool (n_refine ops)" "r_inv_less (n_refine ops)" "r_inv_eq (n_refine ops)"
      "r_inv_plus (n_refine ops)" "r_inv_minus (n_refine ops)" "r_inv_times (n_refine ops)"
  + check: sound_check_query "q_less (n_query ops)" "q_eq (n_query ops)" gamma_state
      "n_aval ops"
  for ops :: "'a::numeric_domain nonrelational_ops"
begin

subsection ‹Assignment, return, and the operations that do nothing›

text ‹
  ‹assign› overwrites the target with the evaluated expression and ‹ret› does the
  same for ‹ret_var›. ‹skip›, ‹body› and ‹event› are the identity. Each
  operation gets its soundness lemma here.
›

definition assign :: "vname ⇒ exp ⇒ 'a abs_state ⇒ 'a abs_state" where
  "assign x a d = d(x := n_aval ops a d)"

definition skip :: "'a abs_state ⇒ 'a abs_state" where
  "skip d = d"

definition body :: "pname ⇒ 'a abs_state ⇒ 'a abs_state" where
  "body p d = d"

text ‹A check observes its condition but never refines the store --- narrowing a
  state against a checked condition is ‹sound_check_query›'s job --- so
  ‹event› is the identity like ‹skip› and ‹body›.›

definition event :: "analysis_event ⇒ 'a abs_state ⇒ 'a abs_state" where
  "event evt d = d"

definition ret :: "exp option ⇒ pname ⇒ 'a abs_state ⇒ 'a abs_state" where
  "ret e p d = (case e of None ⇒ d | Some a ⇒ assign ret_var a d)"

lemma assign_sound:
  assumes 𝒢: "s ∈ γ d"
  shows "s(x := ⟦a⟧⇩e s) ∈ γ (assign x a d)"
  unfolding assign_def
  using gamma_stateD[OF 𝒢] 𝒢 by blast

lemma skip_sound: "s ∈ γ d ⟹ s ∈ γ (skip d)"
  by (simp add: skip_def)

lemma body_sound: "s ∈ γ d ⟹ s ∈ γ (body p d)"
  by (simp add: body_def)

lemma event_sound: "s ∈ γ d ⟹ s ∈ γ (event evt d)"
  by (simp add: event_def)

lemma ret_sound:
  assumes 𝒢: "s ∈ γ d"
  shows "s(ret_var := (case e of None ⇒ s ret_var | Some a ⇒ ⟦a⟧⇩e s)) ∈ γ (ret e p d)"
  using assign_sound[OF 𝒢] 𝒢 by (cases e) (simp_all add: ret_def)


subsection ‹Classifier-parametric procedure entry›

text ‹
  Entry is the only operation that consults a classifier, inside
  \<^const>‹enter_frame›: assignment, guard and return never do, so everything above
  is classifier-free and only these three constants take one.
›

definition enter_frame_for :: "(vname ⇒ bool) ⇒ 'a abs_state ⇒ 'a abs_state" where
  "enter_frame_for 𝒢 = enter_frame 𝒢 top"

definition enter_for ::
    "(vname ⇒ bool) ⇒ vname list ⇒ exp list ⇒ 'a abs_state ⇒ 'a abs_state" where
  "enter_for 𝒢 = enter_binding 𝒢 top (n_aval ops)"

definition enter_ci_for ::
    "(vname ⇒ bool) ⇒ call_info ⇒ 'a abs_state ⇒ 'a abs_state" where
  "enter_ci_for 𝒢 ci = enter_for 𝒢 (ci_formals ci) (ci_args ci)"

lemma enter_for_sound:
  assumes 𝒢: "s ∈ γ d"
  shows "bind_formals xs (map (λe. ⟦e⟧⇩e s) es) (enter_state cls s)
           ∈ γ (enter_for cls xs es d)"
  unfolding enter_for_def enter_binding_concrete[symmetric]
proof (rule enter_binding_sound[OF 𝒢 gamma_top])
  fix e
  show "⟦e⟧⇩e s ∈ γ (n_aval ops e d)"
    using gamma_stateD[OF 𝒢] by blast
qed

lemma enter_ci_for_sound:
  assumes 𝒢: "s ∈ γ d"
  shows "bind_formals (ci_formals ci) (map (λe. ⟦e⟧⇩e s) (ci_args ci)) (enter_state cls s)
           ∈ γ (enter_ci_for cls ci d)"
  using enter_for_sound[OF 𝒢, of ‹ci_formals ci› ‹ci_args ci›]
  by (simp add: enter_ci_for_def)


subsection ‹The transfer contract, and the per-edge dispatcher›

text ‹The eight operations discharge the framework's contract in one
  ‹unfold_locales›: the call boundary the contract fixes is the structural one,
  so only the per-edge operations and the callee entry are the domain's own.›

lemma is_sound_nonrelational_transfer:
  "sound_nonrelational_transfer 𝒢 skip assign special_transfer backward.branch body ret (enter_ci_for 𝒢) event"
  by unfold_locales
     (simp_all add: assign_sound special_transfer_sound backward.branch_sound skip_sound body_sound
        ret_sound enter_ci_for_sound event_sound)

text ‹The per-edge dispatcher. The executable mirror a domain runs dispatches on
  the action, so the equations relating the two through the represented function are stated at this shape
  rather than one lemma per operation.›

definition tf_abs :: "edge_action ⇒ 'a abs_state ⇒ 'a abs_state" where
  "tf_abs = local_spec_step skip assign special_transfer backward.branch body ret event"

lemma tf_abs_simps [simp]:
  "tf_abs EA_Nop = skip"
  "tf_abs (EA_Assign x e) = assign x e"
  "tf_abs (EA_Special sc y) = special_transfer sc y"
  "tf_abs (EA_Assume b) = backward.branch b True"
  "tf_abs (EA_AssumeNot b) = backward.branch b False"
  "tf_abs (EA_Body p) = body p"
  "tf_abs (EA_Ret eo p) = ret eo p"
  "tf_abs (EA_Check l c) = event (Check_Event l c)"
  by (simp_all add: tf_abs_def)

text ‹The bundle an executable mirror unfolds against. \<^const>‹tf_abs› itself is
  not in it: ‹tf_abs_simps› is already ‹[simp]›, so a proof reaches the operation
  the action selects without naming the dispatcher.›

lemmas op_defs =
  assign_def skip_def body_def event_def ret_def
  enter_frame_for_def enter_for_def enter_ci_for_def

subsection ‹Agreement with the executable mirror›

text ‹
  Each operation above is the one the bundle determines --- ‹Nondet_Int›'s
  \<^const>‹top›, and every other case is definitional ---
  so this domain's dispatcher is \<^const>‹generic_tf_abs› at its own bundle and
  branch. That identification is the whole content: the executable mirror's
  commutation is already proved once against \<^const>‹generic_tf_abs›.
›

lemma tf_abs_eq_generic: "tf_abs = generic_tf_abs ops backward.branch"
proof (rule ext, rule ext)
  fix a :: edge_action and d :: "'a abs_state"
  show "tf_abs a d = generic_tf_abs ops backward.branch a d"
    by (cases a)
       (simp_all add: op_defs split: special_call.splits option.splits)
qed

text ‹
  The derived guard filter is the backward domain's executable branch, so it
  commutes with the abstract guard on every live store, and the whole
  executable step with it.
›

theorem tf_st_for_commute:
  assumes "live_default_st 𝒢 s"
  shows
    "ρ⇘𝒢⇙ (generic_tf_st_for ops 𝒢 a s) =
     tf_abs a (ρ⇘𝒢⇙ s)"
  unfolding tf_abs_eq_generic
  by (rule generic_tf_st_for_commute)
     (simp add: backward.branch_st_with_ops [simplified] backward.branch_st_commute[OF assms])

lemma enter_st_for_commute:
  "ρ⇘𝒢⇙ (generic_enter_st_for ops 𝒢 ci s) =
   enter_ci_for 𝒢 ci (ρ⇘𝒢⇙ s)"
  by (simp add: generic_enter_st_for_def op_defs enter_binding_def enter_frame_def)

subsection ‹Registering the bundle with the pipeline›

text ‹
  The bundle already settles everything \<^locale>‹dg_analysis_exec› asks of the domain:
  the derived transfer is sound, the executable step and entry represent it, and the
  derived classifier is sound in both directions. What remains belongs to the context
  policy (the routing agreement and the seed key), the solver (a
  \<^locale>‹certified_solver›) and the initial state, and stays a premise.
›

theorem dg_analysis_execI:
  assumes route_agree:
      "⋀𝒢 u ctx d ca. route 𝒢 u ctx d ca
         = route_abs 𝒢 u ctx (ρ⇘𝒢⇙ d) ca"
    and seed_ne_buffer_key: "⋀v ctx. seed v ctx ≠ buffer_key"
    and solver: "certified_solver solve solve_dom solve_c"
    and init_sound: "⋀𝒢. cinit_stores 𝒢 ⊆ default_st_gamma 𝒢 init_st"
    and own_key: "⋀n. global_of n = buffer_key"
  shows "dg_analysis_exec (generic_tf_st_for ops) (generic_enter_st_for ops) init_st buffer_key
           global_of seed
           route solve solve_dom bot check.classify_check
           skip assign special_transfer backward.branch body ret enter_ci_for event route_abs solve_c"
proof (rule dg_analysis_exec.intro[OF solver dg_analysis_exec_axioms.intro], goal_cases)
  case (1 𝒢) show ?case by (rule is_sound_nonrelational_transfer)
next
  case (2 𝒢 a s) then show ?case
    unfolding tf_abs_def[symmetric] by (rule tf_st_for_commute)
next
  case (3 𝒢 ci s) show ?case
    by (rule enter_st_for_commute)
qed (fact route_agree seed_ne_buffer_key init_sound own_key
       check.classify_check_proved check.classify_check_refuted refl)+

subsection ‹The specification and its soundness, before any context›

text ‹
  What the bundle supplies to the framework on its own: a whole-state D/G
  specification over the executable step and entry, and its soundness against the
  concretization of the read-back local value, ‹λd g. γ (ρ⇘𝒢⇙ d)›. Neither
  mentions a context, a routing function, a seed key or a solver, so every domain
  reads them off its bundle instead of restating them.
›

definition spec_exec ::
  "(vname ⇒ bool) ⇒ ('a default_st ⇒ bool)
   ⇒ ('x, 'k, unit, 'a default_st lifted, 'a default_st lifted) dg_spec" where
  "spec_exec 𝒢 empty_pred =
     exec_dg_spec 𝒢 empty_pred (generic_tf_st_for ops 𝒢) (generic_enter_st_for ops 𝒢)"

lemma dg_spec_wf_spec_exec [intro, simp]: "dg_spec_wf (spec_exec 𝒢 empty_pred)"
  by (simp add: spec_exec_def)

context
  includes default_st_syntax
  fixes 𝒢 :: "vname ⇒ bool" and empty_pred :: "'a default_st ⇒ bool"
  assumes exact: "⋀s. empty_pred s = is_empty_state (ρ⇘𝒢⇙ s)"
begin

interpretation dom: dg_domain_exec
  𝒢 empty_pred "generic_tf_st_for ops 𝒢" "generic_enter_st_for ops 𝒢"
  skip assign special_transfer backward.branch body ret "enter_ci_for 𝒢" event
  by unfold_locales
     (rule tf_st_for_commute[unfolded tf_abs_def], assumption,
      rule enter_st_for_commute, rule exact)

lemma gamma_exec_readback: "dom.gamma_exec = (λd g. γ (ρ⇘𝒢⇙ d))"
  by (intro ext) (simp add: dom.gamma_exec_def gamma_lift_default_st_gamma_to_fun)

theorem sound_exec:
  "analysis_contract (spec_exec 𝒢 empty_pred) (λd g. γ (ρ⇘𝒢⇙ d)) 𝒢"
proof -
  have "analysis_contract dom.spec_st (λd e. dom.gamma_exec d (e ())) 𝒢"
    by (rule dom.analysis_contract_st[OF is_sound_nonrelational_transfer])
  then show ?thesis by (simp add: gamma_exec_readback spec_exec_def)
qed

text ‹Entry is stated apart from \<^locale>‹analysis_contract›, so a routed instance cites
  it separately; the alternative list is the singleton this entry answers.›

theorem entry_cover_exec:
  assumes "s ∈ γ (ρ⇘𝒢⇙ d)"
  shows "entry_pairs_cover (λd'. γ (ρ⇘𝒢⇙ d')) s
           (call_enter 𝒢 (CallEdge (ci_dst ci) (ci_formals ci) (ci_args ci)) s)
           [(d, transfer_lift empty_pred (generic_enter_st_for ops 𝒢 ci) d)]"
proof -
  have "s ∈ gamma_lift (default_st_gamma 𝒢) d"
    using assms by (simp add: gamma_lift_default_st_gamma_to_fun)
  from dom.entry_pairs_cover_st [OF is_sound_nonrelational_transfer this]
  show ?thesis by (simp add: gamma_lift_default_st_gamma_to_fun)
qed

end

end

section ‹Monotone bundles›

text ‹
  Monotonicity is a separate certificate: the transfer contract asks only for
  soundness, and a bundle whose evaluator or refinement has no monotonicity
  proof (Int's fixpoint refinement) is still a sound one. A monotone bundle additionally has
  monotone special operations and a monotone backward domain, and then every
  derived operation is monotone.
›

locale mono_nonrelational_ops = sound_nonrelational_ops ops
  + mono_minmax_ops "n_special ops" "n_aval ops"
  + backward: mono_refinement "r_intersect (n_refine ops)" "n_aval ops"
      "r_tobool (n_refine ops)" "r_inv_less (n_refine ops)" "r_inv_eq (n_refine ops)"
      "r_inv_plus (n_refine ops)" "r_inv_minus (n_refine ops)" "r_inv_times (n_refine ops)"
  for ops :: "'a::numeric_domain nonrelational_ops"
begin

lemma assign_mono: "d1 ≤ d2 ⟹ assign x a d1 ≤ assign x a d2"
  unfolding assign_def by (simp add: aval_abs_mono le_funD le_funI)

lemma ret_mono: "d1 ≤ d2 ⟹ ret e p d1 ≤ ret e p d2"
  by (cases e) (simp_all add: ret_def assign_mono)

lemma enter_for_mono:
  assumes "d1 ≤ d2"
  shows "enter_for 𝒢 xs es d1 ≤ enter_for 𝒢 xs es d2"
  unfolding enter_for_def
  by (rule enter_binding_mono[OF assms]) (rule aval_abs_mono[OF assms])

end

subsection ‹Certifying a bundle from its capability certificates›

text ‹
  ‹sound_nonrelational_opsI› and ‹mono_nonrelational_opsI› assemble the bundle
  certificates from the special-call, refinement and check-query certificates, so
  a domain never unfolds the combined locales itself.
›

lemma sound_nonrelational_opsI:
  assumes "sound_minmax_ops (n_special ops) (n_aval ops)"
    and "sound_refinement (r_intersect (n_refine ops)) (n_aval ops)
           (r_tobool (n_refine ops)) (r_inv_less (n_refine ops)) (r_inv_eq (n_refine ops))
           (r_inv_plus (n_refine ops)) (r_inv_minus (n_refine ops)) (r_inv_times (n_refine ops))"
    and "sound_check_query (q_less (n_query ops)) (q_eq (n_query ops)) gamma_state (n_aval ops)"
  shows "sound_nonrelational_ops ops"
  by (intro sound_nonrelational_ops.intro assms)

lemma mono_nonrelational_opsI:
  assumes special: "mono_minmax_ops (n_special ops) (n_aval ops)"
    and backward: "mono_refinement (r_intersect (n_refine ops)) (n_aval ops)
           (r_tobool (n_refine ops)) (r_inv_less (n_refine ops)) (r_inv_eq (n_refine ops))
           (r_inv_plus (n_refine ops)) (r_inv_minus (n_refine ops)) (r_inv_times (n_refine ops))"
    and "sound_check_query (q_less (n_query ops)) (q_eq (n_query ops)) gamma_state (n_aval ops)"
  shows "mono_nonrelational_ops ops"
proof -
  interpret mono_minmax_ops "n_special ops" "n_aval ops" by (rule special)
  interpret mono_refinement "r_intersect (n_refine ops)" "n_aval ops"
      "r_tobool (n_refine ops)" "r_inv_less (n_refine ops)" "r_inv_eq (n_refine ops)"
      "r_inv_plus (n_refine ops)" "r_inv_minus (n_refine ops)" "r_inv_times (n_refine ops)"
    by (rule backward)
  show ?thesis
    by (intro mono_nonrelational_ops.intro sound_nonrelational_opsI assms)
       unfold_locales
qed

end