Theory Exec_Backward

theory Exec_Backward
    imports "Voblint_Exec.Default_St_Reachability" "Voblint_Domain.Backward_Domain_Mono"
begin

unbundle default_st_syntax

section ‹Generic executable mirror of backward filtering›

text ‹
  Every interpretation of @{locale sound_refinement} gets an executable
  @{typ "'a default_st"} mirror of its @{text afilter} / @{text bfilter}
  for free, parameterized by an explicit location classifier ‹𝒢›:
  ‹afilter_st› / ‹bfilter_st› and their commutation with the abstract
  filters through @{const default_st_to_fun}, proved once here so no
    domain needs to repeat the induction by hand. Each concrete domain names its
  specialization through its existing ‹sound_refinement› interpretation; Sign,
  Interval, Congruence, and Int all reuse the same correspondence.
›

subsection ‹Standalone executable recursion, outside the semantic locale›

text ‹
  ‹afilter_st_lift›/‹bfilter_st_lift› below are proved *inside*
  \<^locale>‹sound_refinement›, so once exported their ‹.simps› each carry that
  locale's own soundness assumptions as a hypothesis -- a fact code generation
  cannot discharge, so a recursive ‹fun› defined that way has no usable code
  equation, no matter how it is later aliased. ‹refine_ops› packages
  the same raw operations directly, and ‹afilter_st_lift_with›/
  ‹bfilter_st_lift_with› recurse over an explicit ‹'a::executable_domain›
  value instead of interpreting the soundness locale, so their equations carry
  no such premise. The \<^locale>‹sound_refinement› context below builds an
  ‹ops› value from its own fixed operations and proves the two recursions
  agree; ‹branch_st› calls the standalone form directly.
›

record 'a refine_ops =
  r_tobool    :: "'a ⇒ bool option"
  r_inv_less  :: "bool ⇒ 'a ⇒ 'a ⇒ 'a × 'a"
  r_inv_eq    :: "bool ⇒ 'a ⇒ 'a ⇒ 'a × 'a"
  r_inv_plus  :: "'a ⇒ 'a ⇒ 'a ⇒ 'a × 'a"
  r_inv_minus :: "'a ⇒ 'a ⇒ 'a ⇒ 'a × 'a"
  r_inv_times :: "'a ⇒ 'a ⇒ 'a ⇒ 'a × 'a"
  r_intersect :: "'a ⇒ 'a ⇒ 'a"

lemma refine_ops_eta [simp]:
  "⦇r_tobool = r_tobool R, r_inv_less = r_inv_less R, r_inv_eq = r_inv_eq R,
    r_inv_plus = r_inv_plus R, r_inv_minus = r_inv_minus R,
    r_inv_times = r_inv_times R, r_intersect = r_intersect R⦈ = R"
  by (cases R) simp

definition feasible_with ::
  "(exp ⇒ 'a abs_state ⇒ 'a) ⇒ 'a::executable_domain refine_ops ⇒ exp ⇒ bool ⇒ 'a abs_state ⇒ bool"
where
  "feasible_with ev ops e pol sigma =
     (¬ is_empty (ev e sigma) ∧ r_tobool ops (ev e sigma) ≠ Some (¬ pol))"

fun afilter_st_lift_with ::
  "(exp ⇒ 'a abs_state ⇒ 'a) ⇒ 'a::executable_domain refine_ops
   ⇒ (vname ⇒ bool) ⇒ exp ⇒ 'a ⇒ 'a default_st lifted ⇒ 'a default_st lifted"
where
    "afilter_st_lift_with ev ops 𝒢 (V x) a x_lift = do {
       s <- x_lift;
       default_st_set_lift (Lifted s) (location_of 𝒢 x)
         (r_intersect ops a (ρ⇘𝒢⇙ s x))
     }"
  | "afilter_st_lift_with ev ops 𝒢 (Plus e1 e2) a x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_plus ops a
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "afilter_st_lift_with ev ops 𝒢 (Minus e1 e2) a x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_minus ops a
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "afilter_st_lift_with ev ops 𝒢 (Times e1 e2) a x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_times ops a
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "afilter_st_lift_with ev ops 𝒢 _ a x_lift = x_lift"

lemma afilter_st_lift_with_Bot [simp]: "afilter_st_lift_with ev ops 𝒢 e a Bot = Bot"
  by (induction e) simp_all

fun bfilter_st_lift_with ::
  "(exp ⇒ 'a abs_state ⇒ 'a) ⇒ 'a::executable_domain refine_ops
   ⇒ (vname ⇒ bool) ⇒ exp ⇒ bool ⇒ 'a default_st lifted ⇒ 'a default_st lifted"
where
    "bfilter_st_lift_with ev ops 𝒢 (Less e1 e2) res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_less ops res
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (GreaterEq e1 e2) res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_less ops (¬ res)
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (Greater e1 e2) res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_less ops res
             (ev e2 (ρ⇘𝒢⇙ s))
             (ev e1 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e2 a1 (afilter_st_lift_with ev ops 𝒢 e1 a2 (Lifted s))
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (LessEq e1 e2) res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_less ops (¬ res)
             (ev e2 (ρ⇘𝒢⇙ s))
             (ev e1 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e2 a1 (afilter_st_lift_with ev ops 𝒢 e1 a2 (Lifted s))
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (Not b) res x_lift =
       bfilter_st_lift_with ev ops 𝒢 b (¬ res) x_lift"
  | "bfilter_st_lift_with ev ops 𝒢 (And b1 b2) True x_lift =
       bfilter_st_lift_with ev ops 𝒢 b1 True (bfilter_st_lift_with ev ops 𝒢 b2 True x_lift)"
  | "bfilter_st_lift_with ev ops 𝒢 (And b1 b2) False x_lift = do {
       s <- x_lift;
       (if feasible_with ev ops b1 False (ρ⇘𝒢⇙ s)
        then bfilter_st_lift_with ev ops 𝒢 b1 False (Lifted s) else Bot)
       ⊔ (if feasible_with ev ops b2 False (ρ⇘𝒢⇙ s)
          then bfilter_st_lift_with ev ops 𝒢 b2 False (Lifted s) else Bot)
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (Or b1 b2) True x_lift = do {
       s <- x_lift;
       (if feasible_with ev ops b1 True (ρ⇘𝒢⇙ s)
        then bfilter_st_lift_with ev ops 𝒢 b1 True (Lifted s) else Bot)
       ⊔ (if feasible_with ev ops b2 True (ρ⇘𝒢⇙ s)
          then bfilter_st_lift_with ev ops 𝒢 b2 True (Lifted s) else Bot)
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (Or b1 b2) False x_lift =
       bfilter_st_lift_with ev ops 𝒢 b1 False (bfilter_st_lift_with ev ops 𝒢 b2 False x_lift)"
  | "bfilter_st_lift_with ev ops 𝒢 (Eq e1 e2) res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_eq ops res
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "bfilter_st_lift_with ev ops 𝒢 (NotEq e1 e2) res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_eq ops (¬ res)
             (ev e1 (ρ⇘𝒢⇙ s))
             (ev e2 (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e1 a1 (afilter_st_lift_with ev ops 𝒢 e2 a2 (Lifted s))
     }"
  | "bfilter_st_lift_with ev ops 𝒢 e res x_lift = do {
       s <- x_lift;
       let (a1, a2) = r_inv_eq ops (¬ res)
             (ev e (ρ⇘𝒢⇙ s))
             (ev (N 0) (ρ⇘𝒢⇙ s));
       afilter_st_lift_with ev ops 𝒢 e a1 (Lifted s)
     }"

lemma bfilter_st_lift_with_Bot [simp]: "bfilter_st_lift_with ev ops 𝒢 b res Bot = Bot"
proof (induction b arbitrary: res)
  case (And b1 b2) then show ?case by (cases res) simp_all
next
  case (Or b1 b2) then show ?case by (cases res) simp_all
qed simp_all

text ‹
    ‹map_lift_sup›'s left-hand side is ‹map_lift ?f (?x ⊔ ?y)›, so using it with a
  schematic ‹?f› makes the simplifier search higher-order matches and, in the join
  cases below, exceed its unification bound. Specializing ‹f› to ‹default_st_to_fun 𝒢› once
  leaves a first-order rewrite that needs no search --- and the specialization is
  proved by the case split directly rather than through ‹map_lift_sup›, since
  resolving against that rule is itself where the search happens.
›

lemma map_lift_default_st_to_fun_sup [simp]:
  "ρ⇘𝒢⇙ (x ⊔ y :: _ default_st lifted) =
     ρ⇘𝒢⇙ x ⊔ ρ⇘𝒢⇙ y"
  by (cases x; cases y) simp_all

text ‹
  The executable branch, determined by the evaluator and the refinement
  operations alone. A non-relational analysis derives its guard filter from its
  operations through this, so no domain supplies a filter of its own;
  ‹branch_st_with_ops› below identifies it with the locale's ‹branch_st›.
›

definition branch_st_with ::
  "(exp ⇒ 'a abs_state ⇒ 'a) ⇒ 'a::executable_domain refine_ops
   ⇒ (vname ⇒ bool) ⇒ exp ⇒ bool ⇒ 'a default_st ⇒ 'a default_st"
where
  "branch_st_with ev ops 𝒢 e pol s =
     (if feasible_with ev ops e pol (ρ⇘𝒢⇙ s)
      then collapse_lift (bfilter_st_lift_with ev ops 𝒢 e pol (Lifted s))
      else bot)"

context sound_refinement
begin

fun afilter_st ::
  "(vname => bool) => exp => 'a => 'a default_st => 'a default_st"
where
    "afilter_st 𝒢 (V x) a s =
       s⟨location_of 𝒢 x := intersect a (ρ⇘𝒢⇙ s x)⟩"
  | "afilter_st 𝒢 (Plus e1 e2) a s =
       (let (a1, a2) = inv_plus a
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "afilter_st 𝒢 (Minus e1 e2) a s =
       (let (a1, a2) = inv_minus a
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "afilter_st 𝒢 (Times e1 e2) a s =
       (let (a1, a2) = inv_times a
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "afilter_st 𝒢 _ a s = s"

fun bfilter_st ::
  "(vname => bool) => exp => bool => 'a default_st => 'a default_st"
where
    "bfilter_st 𝒢 (Less e1 e2) res s =
       (let (a1, a2) = inv_less res
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "bfilter_st 𝒢 (GreaterEq e1 e2) res s =
       (let (a1, a2) = inv_less (¬ res)
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "bfilter_st 𝒢 (Greater e1 e2) res s =
       (let (a1, a2) = inv_less res
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e2 a1 (afilter_st 𝒢 e1 a2 s))"
  | "bfilter_st 𝒢 (LessEq e1 e2) res s =
       (let (a1, a2) = inv_less (¬ res)
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e2 a1 (afilter_st 𝒢 e1 a2 s))"
  | "bfilter_st 𝒢 (Not b) res s = bfilter_st 𝒢 b (¬ res) s"
  | "bfilter_st 𝒢 (And b1 b2) True s =
       bfilter_st 𝒢 b1 True (bfilter_st 𝒢 b2 True s)"
  | "bfilter_st 𝒢 (And b1 b2) False s =
       (if feasible b1 False (ρ⇘𝒢⇙ s)
        then bfilter_st 𝒢 b1 False s else bot)
       ⊔ (if feasible b2 False (ρ⇘𝒢⇙ s)
            then bfilter_st 𝒢 b2 False s else bot)"
  | "bfilter_st 𝒢 (Or b1 b2) True s =
       (if feasible b1 True (ρ⇘𝒢⇙ s)
        then bfilter_st 𝒢 b1 True s else bot)
       ⊔ (if feasible b2 True (ρ⇘𝒢⇙ s)
            then bfilter_st 𝒢 b2 True s else bot)"
  | "bfilter_st 𝒢 (Or b1 b2) False s =
       bfilter_st 𝒢 b1 False (bfilter_st 𝒢 b2 False s)"
  | "bfilter_st 𝒢 (Eq e1 e2) res s =
       (let (a1, a2) = inv_eq res
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "bfilter_st 𝒢 (NotEq e1 e2) res s =
       (let (a1, a2) = inv_eq (¬ res)
              (⟦e1⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦e2⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e1 a1 (afilter_st 𝒢 e2 a2 s))"
  | "bfilter_st 𝒢 e res s =
       (let (a1, a2) = inv_eq (¬ res)
              (⟦e⟧⇧♯ (ρ⇘𝒢⇙ s))
              (⟦N 0⟧⇧♯ (ρ⇘𝒢⇙ s))
        in afilter_st 𝒢 e a1 s)"

text ‹
  ‹afilter_st_lift›/‹bfilter_st_lift› mirror ‹afilter_st›/‹bfilter_st›'s own recursion
  exactly, but thread a ‹default_st lifted› value through it: a ‹Bot› input never
  reaches a further narrowing step, and a leaf whose freshly narrowed element is
  ‹is_empty› collapses to ‹Bot› via @{const default_st_set_lift}.  The compound
  cases either sequence two single-variable narrows (never re-checking a location
  the other branch already settled) or join two gated branches via ‹⊔›.  Joining
  two live branches can never produce a witness-bottom result, since ‹is_empty› is
  downward closed (@{thm is_empty_antimono}) and each branch's own value is a lower bound
  of the join; a branch whose gate ruled its polarity out contributes ‹bot›
  instead, so the join is witness-bottom exactly when both arms are -- either
  because a gate ruled the polarity out, or because the arm's own recursion
  narrowed to ‹Bot›.  A permitting gate is therefore not on its own enough to
  keep the join live.  No
  per-domain code is needed: this is generic in the @{locale sound_refinement}
  operations, exactly like ‹afilter_st›/‹bfilter_st› themselves.
›

text ‹
  ‹ops› packages this locale's own fixed operations into a ‹refine_ops›
  value, so the lifted filters below are the standalone recursion instantiated here
  rather than a second copy of it. It is an ‹abbreviation›, not a ‹definition›: it
  must inline to the record literal at every use site, including inside
  ‹branch_st›'s own executable definition below, rather than naming a separate
  locale-internal constant whose own code equation would carry
  \<^locale>‹sound_refinement›'s assumptions as a premise -- the same problem
  ‹afilter_st_lift_with›/‹bfilter_st_lift_with› exist to avoid, one level up.
›

abbreviation ops :: "'a refine_ops" where
  "ops ≡ ⦇r_tobool = tobool, r_inv_less = inv_less,
           r_inv_eq = inv_eq, r_inv_plus = inv_plus, r_inv_minus = inv_minus,
           r_inv_times = inv_times, r_intersect = intersect⦈"

lemma feasible_with_ops [simp]: "feasible_with aval_abs ops = feasible"
  by (intro ext) (simp add: feasible_with_def feasible_def)

definition afilter_st_lift ::
  "(vname => bool) => exp => 'a => 'a default_st lifted => 'a default_st lifted"
where
  "afilter_st_lift 𝒢 e a x_lift = afilter_st_lift_with aval_abs ops 𝒢 e a x_lift"

lemmas afilter_st_lift_simps [simp] =
  afilter_st_lift_with.simps [of aval_abs ops, folded afilter_st_lift_def]

lemma afilter_st_lift_Bot [simp]: "afilter_st_lift 𝒢 e a Bot = Bot"
  by (simp add: afilter_st_lift_def)

lemma afilter_st_commute:
  "ρ⇘𝒢⇙ (afilter_st 𝒢 e a s) =
     afilter e a (ρ⇘𝒢⇙ s)"
proof (induction e arbitrary: a s)
  case (N n)
  then show ?case by simp
next
  case (V x)
  then show ?case by simp
next
  case (Plus e1 e2)
  show ?case by (simp add: Plus.IH split: prod.splits)
next
  case (Minus e1 e2)
  show ?case by (simp add: Minus.IH split: prod.splits)
next
  case (Times e1 e2)
  show ?case by (simp add: Times.IH split: prod.splits)
next
  case (Less e1 e2) then show ?case by simp
next
  case (Div e1 e2) then show ?case by simp
next
  case (Mod e1 e2) then show ?case by simp
next
  case (LessEq e1 e2) then show ?case by simp
next
  case (Greater e1 e2) then show ?case by simp
next
  case (GreaterEq e1 e2) then show ?case by simp
next
  case (Eq e1 e2) then show ?case by simp
next
  case (NotEq e1 e2) then show ?case by simp
next
  case (Not e) then show ?case by simp
next
  case (And e1 e2) then show ?case by simp
next
  case (Or e1 e2) then show ?case by simp
qed

text ‹
  ‹bfilter_st_lift› mirrors ‹bfilter_lifted›'s recursion one constructor at a
  time, exactly as ‹bfilter_st› mirrors plain ‹bfilter›: the sequential cases
  (‹Not›/‹And True›/‹Or False›/‹Less›/‹Eq›) chain two narrowing steps, and the
  compound-join cases (‹And False›/‹Or True›) gate each arm to structural
  ‹Bot› via @{const feasible} and join at the lifted level, ahead of the
  join rather than after it. This is what ‹bfilter›'s own join (kept plain and
  pointwise so ‹bfilter_sign›/‹bfilter_ivl› stay code-generatable) cannot
  afford: a witness-bottom arm collapses to ‹Bot› here regardless of what the
  other arm's unrefined locations look like, so ‹Bot ⊔ x = x› discards it
  exactly, with no whole-expression probe needed afterward.
›

definition bfilter_st_lift ::
  "(vname => bool) => exp => bool => 'a default_st lifted => 'a default_st lifted"
where
  "bfilter_st_lift 𝒢 b res x_lift = bfilter_st_lift_with aval_abs ops 𝒢 b res x_lift"

lemmas bfilter_st_lift_simps [simp] =
  bfilter_st_lift_with.simps [of aval_abs ops, folded bfilter_st_lift_def afilter_st_lift_def]

lemma bfilter_st_lift_Bot [simp]: "bfilter_st_lift 𝒢 b res Bot = Bot"
  by (simp add: bfilter_st_lift_def)

end

context sound_refinement
begin

lemma afilter_lift_step:
  fixes s :: "'a default_st"
  assumes IH1: "!!s'. live_default_st 𝒢 s' ==>
                ρ⇘𝒢⇙ (afilter_st_lift 𝒢 e1 a1 (Lifted s')) =
                normalize_lift is_empty_state (afilter e1 a1 (ρ⇘𝒢⇙ s'))"
    and IH2: "ρ⇘𝒢⇙ (afilter_st_lift 𝒢 e2 a2 (Lifted s)) =
                normalize_lift is_empty_state (afilter e2 a2 (ρ⇘𝒢⇙ s))"
  shows "map_lift ρ⇘𝒢⇙
           (afilter_st_lift 𝒢 e1 a1 (afilter_st_lift 𝒢 e2 a2 (Lifted s))) =
         normalize_lift is_empty_state
           (afilter e1 a1 (afilter e2 a2 (ρ⇘𝒢⇙ s)))"
proof (cases "is_empty_state (afilter e2 a2 (ρ⇘𝒢⇙ s))")
  case True
  then have bot2: "afilter_st_lift 𝒢 e2 a2 (Lifted s) = Bot"
    using IH2 by (cases "afilter_st_lift 𝒢 e2 a2 (Lifted s)") simp_all
  have "is_empty_state (afilter e1 a1 (afilter e2 a2 (ρ⇘𝒢⇙ s)))"
    using is_empty_state_antimono[OF afilter_reductive True] .
  with bot2 show ?thesis by simp
next
  case False
  then obtain t where t: "afilter_st_lift 𝒢 e2 a2 (Lifted s) = Lifted t"
    using IH2 by (cases "afilter_st_lift 𝒢 e2 a2 (Lifted s)") simp_all
  have ft: "ρ⇘𝒢⇙ t = afilter e2 a2 (ρ⇘𝒢⇙ s)"
    using IH2 t False by simp
  have live_t: "live_default_st 𝒢 t"
    unfolding live_default_st_def ft using False by simp
  show ?thesis
    unfolding t using IH1[OF live_t] ft by simp
qed

text ‹
  ‹bfilter_lift_bind_step› composes two sequential lifted narrowing steps
  (‹And True›, ‹Or False›): if the inner step already went ‹Bot›, the outer
  step is never reached and the composite is ‹Bot› too; otherwise it recurses
  on the inner step's live witness. This is @{const bind_lift}'s own
  associativity, specialized to the executable/lifted correspondence.
›

lemma bfilter_lift_bind_step:
  fixes s :: "'a default_st"
  assumes IH1: "!!s'. live_default_st 𝒢 s' ==>
                ρ⇘𝒢⇙ (bfilter_st_lift 𝒢 b1 res (Lifted s')) =
                bfilter_lifted b1 res (ρ⇘𝒢⇙ s')"
    and IH2: "ρ⇘𝒢⇙ (bfilter_st_lift 𝒢 b2 res (Lifted s)) =
                bfilter_lifted b2 res (ρ⇘𝒢⇙ s)"
  shows "map_lift ρ⇘𝒢⇙
           (bfilter_st_lift 𝒢 b1 res (bfilter_st_lift 𝒢 b2 res (Lifted s))) =
         bind (bfilter_lifted b2 res (ρ⇘𝒢⇙ s)) (bfilter_lifted b1 res)"
proof (cases "bfilter_st_lift 𝒢 b2 res (Lifted s)")
  case Bot
  then show ?thesis using IH2 by simp
next
  case (Lifted t)
    have eq: "Lifted (ρ⇘𝒢⇙ t)
              = bfilter_lifted b2 res (ρ⇘𝒢⇙ s)"
      using IH2 Lifted by simp
  have live_t: "live_default_st 𝒢 t"
  proof -
    have "normalized_lift is_empty_state (Lifted (ρ⇘𝒢⇙ t))"
      using bfilter_lifted_normalized[of b2 res "ρ⇘𝒢⇙ s"] eq by simp
    then show ?thesis by (simp add: live_default_st_def)
  qed
    show ?thesis
      unfolding Lifted using IH1[OF live_t] eq[symmetric] by simp
qed

text ‹
  ‹bfilter_lift_gate_step› is the executable/lifted correspondence for a
  single gated disjunct, feeding @{const feasible} the same represented state
  ‹bfilter_lifted›'s own gate reads: a feasible disjunct recurses, an
  infeasible one contributes ‹Bot› on both sides.
›

lemma bfilter_lift_gate_step:
  fixes s :: "'a default_st"
  assumes IH: "ρ⇘𝒢⇙ (bfilter_st_lift 𝒢 b pol (Lifted s)) =
                 bfilter_lifted b pol (ρ⇘𝒢⇙ s)"
  shows "map_lift ρ⇘𝒢⇙
           (if feasible b pol (ρ⇘𝒢⇙ s)
            then bfilter_st_lift 𝒢 b pol (Lifted s) else Bot)
         = (if feasible b pol (ρ⇘𝒢⇙ s)
            then bfilter_lifted b pol (ρ⇘𝒢⇙ s) else Bot)"
  by (cases "feasible b pol (ρ⇘𝒢⇙ s)") (simp_all add: IH)


lemma afilter_st_lift_correct:
  fixes s :: "'a default_st"
  assumes "live_default_st 𝒢 s"
  shows "ρ⇘𝒢⇙ (afilter_st_lift 𝒢 e a (Lifted s)) =
         normalize_lift is_empty_state (afilter e a (ρ⇘𝒢⇙ s))"
using assms proof (induction e arbitrary: a s)
  case (N n)
  then show ?case by (simp add: live_default_st_def)
next
    case (V x)
  show ?case
    unfolding afilter_st_lift_simps bind_lift_left_identity afilter.simps
      refine_ops.select_convs
    by (rule default_st_set_lift_correct[OF V.prems])
next
  case (Plus e1 e2)
  show ?case
    unfolding afilter_st_lift_simps afilter_Plus_unfold
              bind_lift_left_identity Let_def case_prod_beta
    using afilter_lift_step[OF Plus.IH(1) Plus.IH(2)[OF Plus.prems]]
    by simp
next
  case (Minus e1 e2)
  show ?case
    unfolding afilter_st_lift_simps afilter_Minus_unfold
              bind_lift_left_identity Let_def case_prod_beta
    using afilter_lift_step[OF Minus.IH(1) Minus.IH(2)[OF Minus.prems]]
    by simp
next
  case (Times e1 e2)
  show ?case
    unfolding afilter_st_lift_simps afilter_Times_unfold
              bind_lift_left_identity Let_def case_prod_beta
    using afilter_lift_step[OF Times.IH(1) Times.IH(2)[OF Times.prems]]
    by simp
next
  case (Less e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (Div e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (Mod e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (LessEq e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (Greater e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (GreaterEq e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (Eq e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (NotEq e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (Not e) then show ?case by (simp add: live_default_st_def)
next
  case (And e1 e2) then show ?case by (simp add: live_default_st_def)
next
  case (Or e1 e2) then show ?case by (simp add: live_default_st_def)
qed

lemma bfilter_st_lift_correct:
  fixes s :: "'a default_st"
  assumes "live_default_st 𝒢 s"
    shows "ρ⇘𝒢⇙ (bfilter_st_lift 𝒢 b res (Lifted s)) =
         bfilter_lifted b res (ρ⇘𝒢⇙ s)"
using assms proof (induction b arbitrary: res s)
  case (N n)
  show ?case
    using N.prems
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_st_lift_correct[OF N.prems] live_default_st_def)
next
  case (V x)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        default_st_set_lift_correct[OF V.prems] fun_upd_def)
next
  case (Plus e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF Plus.prems]])
next
  case (Minus e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF Minus.prems]])
next
  case (Times e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF Times.prems]])
next
  case (Div e1 e2)
  then show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity live_default_st_def)
next
  case (Mod e1 e2)
  then show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity live_default_st_def)
next
  case (Not b)
  then show ?case by (simp add: Not.IH)
next
    case (And b1 b2)
  show ?case
  proof (cases res)
    case True
    then show ?thesis
      using bfilter_lift_bind_step[OF And.IH(1) And.IH(2)[OF And.prems]]
      by simp
  next
    case False
    have g1: "map_lift ρ⇘𝒢⇙
                (if feasible b1 False (ρ⇘𝒢⇙ s)
                 then bfilter_st_lift 𝒢 b1 False (Lifted s) else Bot)
              = (if feasible b1 False (ρ⇘𝒢⇙ s)
                 then bfilter_lifted b1 False (ρ⇘𝒢⇙ s) else Bot)"
      by (rule bfilter_lift_gate_step[OF And.IH(1)[OF And.prems]])
    have g2: "map_lift ρ⇘𝒢⇙
                (if feasible b2 False (ρ⇘𝒢⇙ s)
                 then bfilter_st_lift 𝒢 b2 False (Lifted s) else Bot)
              = (if feasible b2 False (ρ⇘𝒢⇙ s)
                 then bfilter_lifted b2 False (ρ⇘𝒢⇙ s) else Bot)"
      by (rule bfilter_lift_gate_step[OF And.IH(2)[OF And.prems]])
    show ?thesis
      using False
      by (simp add: g1 g2)
  qed
next
  case (Or b1 b2)
  show ?case
  proof (cases res)
    case True
    have g1: "map_lift ρ⇘𝒢⇙
                (if feasible b1 True (ρ⇘𝒢⇙ s)
                 then bfilter_st_lift 𝒢 b1 True (Lifted s) else Bot)
              = (if feasible b1 True (ρ⇘𝒢⇙ s)
                 then bfilter_lifted b1 True (ρ⇘𝒢⇙ s) else Bot)"
      by (rule bfilter_lift_gate_step[OF Or.IH(1)[OF Or.prems]])
    have g2: "map_lift ρ⇘𝒢⇙
                (if feasible b2 True (ρ⇘𝒢⇙ s)
                 then bfilter_st_lift 𝒢 b2 True (Lifted s) else Bot)
              = (if feasible b2 True (ρ⇘𝒢⇙ s)
                 then bfilter_lifted b2 True (ρ⇘𝒢⇙ s) else Bot)"
      by (rule bfilter_lift_gate_step[OF Or.IH(2)[OF Or.prems]])
    show ?thesis
      using True
      by (simp add: g1 g2)
  next
    case False
    then show ?thesis
      using bfilter_lift_bind_step[OF Or.IH(1) Or.IH(2)[OF Or.prems]]
      by simp
  qed
next
    case (Less e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF Less.prems]])
next
  case (LessEq e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF LessEq.prems]])
next
  case (Greater e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF Greater.prems]])
next
  case (GreaterEq e1 e2)
  show ?case
    by (simp add: Let_def case_prod_beta bind_lift_left_identity
        afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF GreaterEq.prems]])
next
  case (Eq e1 e2)
    show ?case
      by (simp add: Let_def case_prod_beta bind_lift_left_identity
          afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF Eq.prems]])
next
  case (NotEq e1 e2)
    show ?case
      by (simp add: Let_def case_prod_beta bind_lift_left_identity
          afilter_lift_step[OF afilter_st_lift_correct afilter_st_lift_correct[OF NotEq.prems]])
qed

text ‹
  ‹branch_st› is ‹branch›'s executable ‹default_st› mirror. It carries no
  runtime liveness test: ‹live_default_st›/‹is_empty_state› have no code
  equation by design (they existentially quantify over ‹vname›), so an
  executable definition must never mention them. ‹branch_st_commute›
  therefore only holds on live inputs -- a live-input contract, not a gap.
  Production never calls ‹tf_st› on a dead payload: ‹transfer_lift› already
  normalizes every intermediate result through ‹normalize_lift›, so a dead
  result becomes structural ‹Bot› before it can be handed to the next step's
  ‹tf_st›. On a dead input ‹bfilter_st_lift›'s leaf updates
  (\<^const>‹default_st_set_lift›) may fail to rediscover a pre-existing,
  untouched witness-bottom location the way ‹bfilter_lifted_witness_bottom›
  guarantees at the specification level, so ‹branch_st›'s raw result need not
  match ‹branch›'s there; the lifted commutation theorem the solver actually
  uses (‹step_lift_commute›) closes this gap from the normalization
  invariant instead of a runtime check.
›

definition branch_st ::
  "(vname => bool) => exp => bool => 'a default_st => 'a default_st"
where
  "branch_st 𝒢 e pol s =
     (if feasible_with aval_abs ops e pol (ρ⇘𝒢⇙ s)
      then collapse_lift (bfilter_st_lift_with aval_abs ops 𝒢 e pol (Lifted s))
      else bot)"

lemma branch_st_with_ops: "branch_st_with aval_abs ops = branch_st"
  by (simp add: fun_eq_iff branch_st_with_def branch_st_def)

lemma branch_st_commute:
  assumes "live_default_st 𝒢 s"
  shows
    "ρ⇘𝒢⇙ (branch_st 𝒢 e pol s) =
       branch e pol (ρ⇘𝒢⇙ s)"
  proof (cases "feasible e pol (ρ⇘𝒢⇙ s)")
  case True
  have eq: "ρ⇘𝒢⇙ (bfilter_st_lift 𝒢 e pol (Lifted s)) =
              bfilter_lifted e pol (ρ⇘𝒢⇙ s)"
    by (rule bfilter_st_lift_correct[OF assms])
  have "ρ⇘𝒢⇙ (collapse_lift (bfilter_st_lift 𝒢 e pol (Lifted s)))
          = collapse_lift (map_lift ρ⇘𝒢⇙
                             (bfilter_st_lift 𝒢 e pol (Lifted s)))"
    by (rule collapse_lift_map_lift[where f = "default_st_to_fun 𝒢",
          OF default_st_to_fun_bot, symmetric])
  also have "... = collapse_lift (bfilter_lifted e pol (ρ⇘𝒢⇙ s))"
    using eq by simp
    finally show ?thesis
      using True
      by (simp add: branch_st_def branch_def branch_lifted_def
          bfilter_st_lift_def [symmetric])
next
  case False
  then show ?thesis
    by (simp add: branch_st_def branch_def branch_lifted_def)
qed

end

unbundle no default_st_syntax

end