Theory Solver_Trace

theory Solver_Trace
  imports Globals_Rule
begin

section ‹A solver trace inside the exported code›

text ‹The vendored interface hides the solver's state fields (‹TD_side_Interface›).
  The traced equations below restate the solver's own terms, so this theory names
  those fields again, as input abbreviations of the hidden constants.›

abbreviation (input) point where "point ≡ TD_side_upd_rule.state.point"
abbreviation (input) point_update where "point_update ≡ TD_side_upd_rule.state.point_update"
abbreviation (input) σ where "σ ≡ TD_side.state.σ"
abbreviation (input) σ_update where "σ_update ≡ TD_side.state.σ_update"

text ‹
  The executable solver can report its steps. ‹trace_event› is the identity on
  the logic's side: it takes a channel name and a suspended event and returns
  ‹()›, so every equation below is proved equal to the untraced one by
  unfolding it. Code export maps the constant to a target-language hook
  (‹Trace_Run›); the hook forces the suspension only when tracing is on, so an
  untraced run never builds an event. The Eval target keeps the equation, so
  proofs by evaluation run the same code without any hook.

  The traced solver is a copy of the vendored solver's executable functions
  under new constants, each defined as the function it copies and given the
  traced equation as its code equation. The vendored functions keep their own
  code equations, so a caller that names them runs no hook; only a caller that
  names the traced constants reports events.
›

definition trace_event :: "String.literal ⇒ (unit ⇒ 'e) ⇒ unit" where
  "trace_event channel e = ()"

text ‹
  One event per solver step that Goblint's tracing of its top-down solvers
  reports (@{url "https://github.com/goblint/analyzer/blob/master/src/solver/td_simplified.ml"},
  @{url "https://github.com/goblint/analyzer/blob/master/src/solver/td3.ml"}), plus two with
  no counterpart there:
  ‹Ev_Rhs›, the value a right-hand side returns, and the start and end of one
  solve, and ‹Ev_Wpoint_Clear›, an iteration of an already stable unknown
  dropping it from the widening points. A local unknown is ‹'x›, a global one
  ‹'g›, a value ‹'d›. Booleans are
  the solver's own sets read at the step: ‹called›, ‹stabl›, and ‹point›, the
  widening points, and whether an old value is ‹⊥›.
›

datatype ('x, 'g, 'd) solver_event =
    Ev_Start 'x
  | Ev_Stop
  | Ev_Query 'x 'x bool bool
  | Ev_Query_Wpoint 'x bool
  | Ev_Iterate_From_Query 'x
  | Ev_Add_Infl "'x + 'g" 'x
  | Ev_Answer 'x 'x 'd
  | Ev_Query_Global 'x 'g
  | Ev_Answer_Global 'x 'g 'd
  | Ev_Iterate 'x bool bool bool
  | Ev_Eq 'x
  | Ev_Rhs 'x 'd
  | Ev_Still_Unstable 'x
  | Ev_Widen 'x bool
  | Ev_Sol 'x bool 'd 'd 'd
  | Ev_Wpoint_Remove 'x bool
  | Ev_Wpoint_Clear 'x bool
  | Ev_Update 'x bool bool 'd 'd
  | Ev_Iterate_Changed 'x
  | Ev_Side 'x 'g 'd
  | Ev_Update_Global 'x 'g bool 'd 'd
  | Ev_Destabilize "'x + 'g"
  | Ev_Stable_Remove 'x

text ‹
  Destabilization. ‹destab_opt x› clears the unknowns that read ‹x› from the
  stable set and continues through each one not currently being solved.
›

lemma destab_iter_opt_traced:
  fixes i :: "('x + 'g, 'x list) fmap"
  shows
    "destab_iter_opt [] i s c = (i, s)"
    "destab_iter_opt (y # ys) i s c =
      (let _ = trace_event STR ''solver''
                 (λ_. (Ev_Stable_Remove y :: ('x, 'g, unit) solver_event)) in
       let (i, s) = (if y ∈ c then (i, s - {y}) else destab_opt (Inl y) i (s - {y}) c) in
       destab_iter_opt ys i s c)"
  by (simp_all only: destab_iter_opt.simps trace_event_def Let_def)

lemma destab_opt_traced:
  fixes x :: "'x + 'g"
  shows
    "destab_opt x i s c =
      (let _ = trace_event STR ''solver''
                 (λ_. (Ev_Destabilize x :: ('x, 'g, unit) solver_event)) in
       destab_iter_opt (fmlookup_default i [] x) (fmdrop x i) s c)"
  by (simp only: destab_opt.simps trace_event_def Let_def)

definition traced_destab_iter_opt ::
    "'x list ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x + 'g, 'x list) fmap × 'x set"
  where [code del]: "traced_destab_iter_opt ys i s c = destab_iter_opt ys i s c"

definition traced_destab_opt ::
    "'x + 'g ⇒ ('x + 'g, 'x list) fmap ⇒ 'x set ⇒ 'x set ⇒ ('x + 'g, 'x list) fmap × 'x set"
  where [code del]: "traced_destab_opt x i s c = destab_opt x i s c"

lemmas traced_destab_code [code] =
  destab_iter_opt_traced[folded traced_destab_iter_opt_def traced_destab_opt_def]
  destab_opt_traced[folded traced_destab_iter_opt_def traced_destab_opt_def]

text ‹
  The solver. The equation below is the vendored ‹solve_rec_c› equation with
  events added at the steps Goblint traces: ‹Q› is a query, ‹I› an iteration,
  ‹R› one evaluation of the right-hand side, ‹E› one instruction of it.
›

unbundle lattice_syntax

lemma solve_rec_c_traced:
  fixes T :: "('x, 'g, 'd::{bounded_semilattice_sup_bot,warrowing}) eqsT"
  shows "TD_side_rule_Interp_solve_rec_c r T s = (case s of
    TD_side_upd_rule.func_state.Q (y, x, state, ug_state) ⇒
      (let _ = trace_event STR ''solver'' (λ_. (Ev_Query y x (x ∈ stabl state) (x ∈ called state)
                 :: ('x, 'g, 'd) solver_event)) in
       Option.bind (
        if x ∈ called state then
          (let _ = trace_event STR ''solver''
                     (λ_. (Ev_Query_Wpoint x (x ∈ point state) :: ('x, 'g, 'd) solver_event)) in
           Some ((σ state) (Inl x), state⦇ point := insert x (point state) ⦈, ug_state))
        else
          (let _ = trace_event STR ''solver''
                     (λ_. (Ev_Iterate_From_Query x :: ('x, 'g, 'd) solver_event)) in
           TD_side_rule_Interp_solve_rec_c r T
             (TD_side_upd_rule.func_state.I (x, state⦇ called := insert x (called state) ⦈, ug_state))))
        (λ(xd, state, ug_state).
          let _ = trace_event STR ''solver'' (λ_. (Ev_Add_Infl (Inl x) y :: ('x, 'g, 'd) solver_event)) in
          let _ = trace_event STR ''solver'' (λ_. (Ev_Answer y x xd :: ('x, 'g, 'd) solver_event)) in
          Some (xd, state⦇infl := fminsert (infl state) (Inl x) y⦈, ug_state)))
  | TD_side_upd_rule.func_state.I (x, state, ug_state) ⇒
      (let _ = trace_event STR ''solver''
                 (λ_. (Ev_Iterate x (x ∈ called state) (x ∈ stabl state) (x ∈ point state)
                   :: ('x, 'g, 'd) solver_event)) in
       if x ∉ stabl state then Option.bind (
        TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.R (x, state, ug_state)))
        (λ(d_new, state1, ug_state1).
          let _ = trace_event STR ''solver''
                    (λ_. (Ev_Widen x (x ∈ point state) :: ('x, 'g, 'd) solver_event)) in
          let d_new' = (if x ∈ point state then (σ state1) (Inl x) ∇Δ d_new else d_new) in
          let _ = trace_event STR ''solver''
                    (λ_. (Ev_Sol x (x ∈ point state) ((σ state1) (Inl x)) d_new d_new'
                      :: ('x, 'g, 'd) solver_event)) in
          if (σ state1) (Inl x) = d_new' then
            (let _ = trace_event STR ''solver''
                       (λ_. (Ev_Wpoint_Remove x (x ∈ point state1) :: ('x, 'g, 'd) solver_event)) in
             Some (d_new', state1⦇ called := called state1 - {x}, point := (point state1) - {x}⦈,
               ug_state1))
          else
            (let _ = trace_event STR ''solver''
                       (λ_. (Ev_Update x (x ∈ point state1) ((σ state1) (Inl x) = ⊥)
                               ((σ state1) (Inl x)) d_new' :: ('x, 'g, 'd) solver_event)) in
             let (infl1, stabl1) = destab_opt (Inl x) (infl state1) (stabl state1) (called state1) in
             let _ = trace_event STR ''solver''
                       (λ_. (Ev_Iterate_Changed x :: ('x, 'g, 'd) solver_event)) in
             TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.I (x, state1⦇ infl := infl1, stabl := stabl1,
               σ := (σ state1)(Inl x := d_new') ⦈, ug_state1))))
      else
        (let _ = trace_event STR ''solver''
                   (λ_. (Ev_Wpoint_Clear x (x ∈ point state) :: ('x, 'g, 'd) solver_event)) in
         Some ((σ state) (Inl x), state⦇ called := called state - {x}, point := (point state) - {x}⦈,
          ug_state)))
  | TD_side_upd_rule.func_state.R (x, state, ug_state) ⇒
      (let _ = trace_event STR ''solver'' (λ_. (Ev_Eq x :: ('x, 'g, 'd) solver_event)) in
       Option.bind (
        TD_side_rule_Interp_solve_rec_c r T
          (TD_side_upd_rule.func_state.E (x, T x, (λ_. ⊥), state ⦇stabl := insert x (stabl state)⦈, ug_state)))
        (λ(xd, state, ug_state). if x ∈ stabl state then Some (xd, state, ug_state)
          else (let _ = trace_event STR ''solver''
                          (λ_. (Ev_Still_Unstable x :: ('x, 'g, 'd) solver_event)) in
                TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.R (x, state, ug_state)))))
  | TD_side_upd_rule.func_state.E (x, t, sides, state, ug_state) ⇒ (case t of
        Answer d ⇒
          (let _ = trace_event STR ''solver'' (λ_. (Ev_Rhs x d :: ('x, 'g, 'd) solver_event)) in
           Some (d, state, ug_state))
      | QueryL y g ⇒ Option.bind (TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.Q (x, y, state, ug_state)))
            (λ(yd, state, ug_state).
              TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.E (x, g yd, sides, state, ug_state)))
      | QueryG y g ⇒
          (let _ = trace_event STR ''solver'' (λ_. (Ev_Query_Global x y :: ('x, 'g, 'd) solver_event)) in
           let _ = trace_event STR ''solver'' (λ_. (Ev_Add_Infl (Inr y) x :: ('x, 'g, 'd) solver_event)) in
           let _ = trace_event STR ''solver''
                     (λ_. (Ev_Answer_Global x y ((σ state) (Inr y)) :: ('x, 'g, 'd) solver_event)) in
           TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.E (x, g ((σ state) (Inr y)), sides,
             state⦇ infl := fminsert (infl state) (Inr y) x⦈, ug_state)))
      | Side y d t ⇒
          (let _ = trace_event STR ''solver'' (λ_. (Ev_Side x y d :: ('x, 'g, 'd) solver_event)) in
           let d = sides y ⊔ d in
           let sides = sides(y := d) in
           let (upd, ug_state) = update_global_of r (σ state (Inr y)) x y d ug_state in
           case upd of None ⇒ TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.E (x, t, sides, state, ug_state))
           | Some d ⇒
             let _ = trace_event STR ''solver''
                       (λ_. (Ev_Update_Global x y ((σ state) (Inr y) = ⊥) ((σ state) (Inr y)) d
                         :: ('x, 'g, 'd) solver_event)) in
             let (infl', stabl') = destab_opt (Inr y) (infl state) (stabl state) (called state) in
             TD_side_rule_Interp_solve_rec_c r T (TD_side_upd_rule.func_state.E (x, t, sides, state⦇ infl := infl', stabl := stabl',
               σ := (σ state)(Inr y := d)⦈, ug_state)))))"
  by (rule trans[OF TD_side_rule_Interp.solve_rec_c.simps])
     (simp only: trace_event_def Let_def)

definition traced_solve_rec_c
  where [code del]: "traced_solve_rec_c r T s = TD_side_rule_Interp_solve_rec_c r T s"

lemmas traced_solve_rec_c_code [code] =
  solve_rec_c_traced[folded traced_solve_rec_c_def traced_destab_opt_def]

definition traced_solve_c ::
    "globals_rule ⇒ ('x, 'g, 'd::{bounded_semilattice_sup_bot,warrowing}) eqsT ⇒ 'x
       ⇒ ('x set × ('x + 'g ⇒ 'd)) option"
  where [code del]: "traced_solve_c r T x = TD_side_rule_Interp_solve_c r T x"

lemmas traced_solve_c_code [code] =
  TD_side_rule_Interp.solve_c_def[folded traced_solve_c_def traced_solve_rec_c_def]

text ‹
  One solve, from its root unknown to its result, between a start and a stop event.
  It is ‹solve_c› in the logic; a traced caller names it in place of ‹solve_c›.
›

definition solve_c_traced ::
    "globals_rule ⇒ ('x, 'g, 'd::{bounded_semilattice_sup_bot,warrowing}) eqsT ⇒ 'x
       ⇒ ('x set × ('x + 'g ⇒ 'd)) option" where
  "solve_c_traced r T x =
    (let _ = trace_event STR ''solver'' (λ_. (Ev_Start x :: ('x, 'g, 'd) solver_event)) in
     let res = TD_side_rule_Interp_solve_c r T x in
     let _ = trace_event STR ''solver'' (λ_. (Ev_Stop :: ('x, 'g, 'd) solver_event)) in
     res)"

lemma solve_c_traced_eq: "solve_c_traced r T x = TD_side_rule_Interp_solve_c r T x"
  by (simp add: solve_c_traced_def trace_event_def)

lemma solve_c_traced_code [code]:
  fixes T :: "('x, 'g, 'd::{bounded_semilattice_sup_bot,warrowing}) eqsT"
  shows "solve_c_traced r T x =
    (let _ = trace_event STR ''solver'' (λ_. (Ev_Start x :: ('x, 'g, 'd) solver_event)) in
     let res = traced_solve_c r T x in
     let _ = trace_event STR ''solver'' (λ_. (Ev_Stop :: ('x, 'g, 'd) solver_event)) in
     res)"
  by (simp only: solve_c_traced_def traced_solve_c_def)

end