Theory RG_Garbage_Collector

(*
Title:         Rely-Guarantee Specification of a Concurrent Garbage Collector
Author(s):     Roger C. Su and Nisansala P. Yatapanage
Year:          2026
License:       BSD 2-Clause
Maintainer(s): Su <roger.c.su@proton.me>
               Yatapanage <Nisansala.Yatapanage@anu.edu.au>
*)

theory RG_Garbage_Collector imports Main begin

section ‹Preliminaries›

lemma holds_for_all:
  assumes "guar_b σ σ'"
      and "p s σ"
      and "∀ w. (guar_b σ σ' ∧ p w σ ⟶ q w σ σ')"
      and "p s σ ∧ q s σ σ' ⟶ rely_a σ σ'"
    shows "rely_a σ σ'"
  using assms by blast

definition reach
  :: "'a set ⇒ 'a rel ⇒ 'a set" where
  "reach S R ≡ rtrancl R `` S"

lemma reach_base:
  "w ∈ S ⟹ w ∈ reach S R"
  unfolding reach_def by blast

lemma reach_step:
  "⟦ w ∈ reach S R ; (w,w') ∈ R ⟧ ⟹ w' ∈ reach S R"
  unfolding reach_def apply clarsimp
  by (meson ImageI rtrancl.simps)

lemma reach_induct:
  assumes "w ∈ reach S R"
      and "⋀ v. v ∈ S ⟹ P v"
      and "⋀ u v. u ∈ reach S R ⟹ P u ⟹ (u,v) ∈ R ⟹ P v"
    shows "P w"
  using assms unfolding reach_def apply clarsimp
  by (metis (full_types) ImageI rtrancl_induct)

section ‹Definitions›

text ‹The \emph{nodes} in memory are represented as an arbitrary type @{typ 'a}.›

text ‹Part of the system state is the local variables of the Collector, 
which cannot be accessed by the Mutator.›

record 'a localC =
    safe :: "'a set"
  consid :: "'a set"

text ‹The state of the system is defined as the following record-type.›

record 'a state =
   roots :: "'a set"
      hp :: "'a rel" ― ‹the heap is modelled as a directed graph (i.e.\ a relation)›
    free :: "'a set"
  marked :: "'a set"
     tbm :: "'a option"
  localCvar :: "'a localC"

text ‹Then we formulate the notion of ``a node being reachable in a state''.›

definition reachable
  :: "'a state ⇒ 'a ⇒ bool" where
  "reachable σ x ≡ x ∈ reach (roots σ) (hp σ)"

lemma reachable_exists:
  "reachable σ y ⟹ y ∈ roots σ ∨ (∃ x. reachable σ x ∧ (x,y) ∈ hp σ)"
  unfolding reachable_def reach_def apply clarsimp
  by (metis ImageI rtrancl.cases)

text ‹We now define the various clauses that make up of our specification.›

text ‹In the definitions below, if @{term xy} is a pair in the heap, then
@{term "fst xy"} is the node in the domain (@{text "(a,j) ∈ dom hp"} in the paper),
and @{term "snd xy"} is any child of the node (@{text "hp(a,j)"} in the paper).›

text ‹All the marked nodes in the given set have marked children.›

definition all_ok
  :: "'a set ⇒ 'a state ⇒ bool" where
  "all_ok s σ ≡  ∀ xy ∈ hp σ.
    fst xy ∈ marked σ ∧
    fst xy ∈ s 
    ⟶ (snd xy ∈ marked σ)"

text ‹For all marked nodes in the given set that have unmarked children,
there is another path to that child.›

definition can_be_marked
  :: "'a set ⇒ 'a state ⇒ bool" where
  "can_be_marked s σ ≡ ∀ xy ∈ hp σ.
    fst xy ∈ marked σ ∩ s ∧
    snd xy ∉ marked σ ∧
    reachable σ (snd xy) 
    ⟶ (∃ zw ∈ hp σ.
      (fst zw ∈  reach (roots σ) (hp σ) ∨ fst zw ∈ reach (marked σ ∩ -s) (hp σ)) ∧
      (fst zw ∉ s ∨ fst zw ∉ marked σ) ∧
       fst xy ≠ fst zw ∧
       snd xy = snd zw)"

text ‹The @{term tbm} field is the only child node that
(1) is unmarked and
(2) has a marked parent.›

definition tbm_put
  :: "'a set ⇒ 'a state ⇒ bool" where
  "tbm_put s σ ≡ ∀ xy ∈ hp σ.
    tbm σ ≠ Some (snd xy) ∧
    fst xy ∈ s ∧
    fst xy ∈ marked σ
    ⟶ (snd xy ∈ marked σ)"

text ‹The rely condition of the collector.›

definition rely_collector
  :: "'a state ⇒ 'a state ⇒ bool" where
 "rely_collector σ σ' ≡ marked σ ⊆ marked σ' ∧ localCvar σ = localCvar σ' ∧
   (all_ok (safe (localCvar σ)) σ ⟶
      can_be_marked (safe (localCvar σ)) σ' ∨ marked σ ⊂ marked σ')"

text ‹The guarantee condition of the Propagate phase of the Collector.›

definition guar_collector
  :: "'a state ⇒ 'a state  ⇒ bool" where
  "guar_collector σ σ' ≡ marked σ ⊆ marked σ' ∧
    consid (localCvar σ) ⊆ consid (localCvar σ') ∧
    safe (localCvar σ') ⊆ safe (localCvar σ) ∧
    ((safe (localCvar σ') = consid (localCvar σ')) ∨
     ((safe (localCvar σ') ⊂ consid (localCvar σ))) ∧ (marked σ ⊂ marked σ))"

text ‹The post condition of the Propagate phase of the Collector.›

definition post_propagate
  :: "'a state ⇒ 'a state  ⇒ bool" where
  "post_propagate σ σ' ≡ ∀ (x,y) ∈ hp σ.
     x ∈ marked σ' ∩ consid (localCvar σ') ⟶ 
    (y ∈ marked σ' ∨ (marked σ ⊂ marked σ'))"

text ‹The post condition of the remove action of the Mutator.›

definition post_change_remove
  :: "'a state ⇒ 'a state ⇒ bool" where
  "post_change_remove σ σ' ≡ ∃ xy.
    xy ∉ hp σ' ∧ hp σ = hp σ' ∪ {xy} ∧ reachable σ (fst xy) ∧
    tbm σ' = None"

text ‹The post condition of the redirect action of the Mutator.›

definition post_change_redirect
  :: "'a state ⇒ 'a state ⇒ bool" where
  "post_change_redirect σ σ' ≡ ∃ x y z.
    hp σ - hp σ' = {(x,y)} ∧ hp σ' - hp σ = {(x,z)} ∧ reachable σ x ∧
    tbm σ' = Some z ∧ reachable σ z" 

text ‹The common post condition of the remove and redirect actions of the Mutator.
It describes the behaviour when the edge @{term "(x,y)"} is removed or redirected
to @{term "(x,a)"}.›

definition post_change
  :: "'a state ⇒ 'a state ⇒ bool" where
  "post_change σ σ' ≡ roots σ ≠ {} ∧
   (post_change_remove σ σ' ∨ post_change_redirect σ σ') ∧ 
   (marked σ =  marked σ') ∧
   (roots σ = roots σ') ∧
   (tbm σ =  tbm σ') ∧
   (localCvar σ = localCvar σ')"

text ‹The post condition of the action of the Mutator that sets @{term tbm}.›

definition post_mark_tbm
  :: "'a state ⇒ 'a state ⇒ bool" where
  "post_mark_tbm σ σ' ≡
     ((tbm σ = None ∧ marked σ' = marked σ) ∨
      (∃x. tbm σ = Some x ∧ marked σ' = marked σ ∪ {x})) ∧
     tbm σ' = None ∧ hp σ = hp σ' ∧ roots σ = roots σ' ∧
     (localCvar σ = localCvar σ')"

text ‹An invariant that the roots always remain marked.›

definition inv_roots
  :: "'a state ⇒ bool" where
  "inv_roots σ ≡ roots σ ⊆ marked σ"

lemma inv_roots_change:
  "⟦ post_change σ σ' ; inv_roots σ ⟧ ⟹ inv_roots σ'"
  unfolding post_change_def inv_roots_def by blast

lemma inv_roots_mark:
  "⟦ post_mark_tbm σ σ' ; inv_roots σ ⟧ ⟹ inv_roots σ'"
  unfolding post_mark_tbm_def inv_roots_def by blast

text ‹A Mutator step preserves the invariant.›

lemma inv_roots_step:
  "⟦ post_change σ σ' ∨ post_mark_tbm σ σ' ; inv_roots σ ⟧ ⟹ inv_roots σ'"
  using inv_roots_change inv_roots_mark by blast

section ‹Lemmas›

text ‹This lemma establishes one of the premises when instantiating
@{theory_text holds_for_all} to the concurrent garbage collector.›

lemma p_q_gives_rely:
  assumes "all_ok (safe (localCvar σ)) σ"
      and "marked σ ⊆ marked σ' ∧ localCvar σ = localCvar σ' ∧
              (can_be_marked (safe (localCvar σ)) σ' ∨ marked σ ⊂ marked σ')"
    shows "rely_collector σ σ'"
  using assms unfolding rely_collector_def by blast

lemma all_ok_conseqs:
  assumes "all_ok s σ"
    shows "can_be_marked s σ"
      and "tbm_put s σ"
  using assms unfolding all_ok_def can_be_marked_def tbm_put_def by auto

subsection ‹Stability Lemmas›

text ‹A Mutator remove step preserves @{term all_ok}.›

lemma stable_all_ok_remove:
  assumes "post_change σ σ' ∧ post_change_remove σ σ'"
      and "all_ok s σ"
    shows "all_ok s σ'"
  using assms unfolding post_change_remove_def post_change_def all_ok_def
  apply clarsimp
  by (metis (no_types, opaque_lifting) fst_conv snd_conv)

lemma reachable_post_pre:
  assumes assm_step: "post_change σ σ'"
      and assm_ok: "all_ok s σ"
    shows "∀ x. reachable σ' x ⟶ reachable σ x"
proof -
  from assm_step have "post_change_remove σ σ' ∨ post_change_redirect σ σ'"
    unfolding post_change_def by simp
  then show ?thesis
  proof (rule disjE, goal_cases case_remove case_redirect)
    case case_remove
    then show ?case
      unfolding post_change_remove_def reachable_def apply clarsimp
      by (smt (verit, ccfv_SIG) DiffE Diff_insert_absorb assm_step post_change_def
          reach_base reach_induct reach_step reachable_def)
  next
    case case_redirect
    then show ?case
      unfolding post_change_redirect_def reachable_def apply clarsimp
      by (smt (verit, ccfv_SIG) Diff_iff Diff_insert assm_step case_redirect
          insert_Diff_single insert_absorb insert_iff post_change_def reach_base reach_induct
          reach_step reachable_def singletonD singletonI snd_conv)
  qed
qed

text ‹The @{text all_ok} property and a redirect step by the Mutator together
establishes @{term can_be_marked}.›

lemma stable_can_be_marked_redirect:
  assumes assm_step: "post_change σ σ' ∧ post_change_redirect σ σ'"
      and assm_ok: "all_ok s σ"
      and assm_roots_marked: "roots σ ⊆ marked σ"
    shows "can_be_marked s σ'"
proof -
  from assm_step have ln_marked_eq: "marked σ' = marked σ"
    unfolding post_change_def by simp
  then have "roots σ' ⊆ marked σ'"
    using assm_step assm_roots_marked unfolding post_change_def by simp

  from assm_step obtain x y z where assm_xyz:
    "hp σ  - hp σ' = {(x,y)} ∧
     hp σ' - hp σ  = {(x,z)} ∧
     reachable σ x ∧
     tbm σ' = Some z ∧
     reachable σ z"
    unfolding post_change_redirect_def by force

  show ?thesis
  proof -
    { fix a b assume assm_ab: ― ‹The assumption-part of @{text can_be_marked}›
        "(a,b) ∈ hp σ' ∧ (a ∈ marked σ' ∩ s) ∧ b ∉ marked σ' ∧ reachable σ' b"

      then have ln_ab: "(a ∈ marked σ ∩ s) ∧ b ∉ marked σ ∧ reachable σ b"
        using assm_ab ln_marked_eq reachable_post_pre assm_step assm_ok by blast
  
      ― ‹The assumptions on @{term "(a,b)"} imply that this edge is exactly
         @{term "(x,z)"} from earlier.›
      then have ln_ab_xy: "(a,b) = (x,z)"
        using assm_ab assm_ok assm_xyz unfolding all_ok_def by fastforce
  
      ― ‹The node @{term z} must have another parent @{term c}›
      have "z ∈ roots σ ∨ (∃ c. reachable σ c ∧ (c,z) ∈ hp σ)"
        using assm_xyz reachable_exists by fast
      moreover have "z ∉ roots σ"
        using assm_roots_marked assm_ab ln_ab_xy ln_marked_eq by blast
      ultimately obtain c where ln_c:
        "reachable σ c ∧ (c,z) ∈ hp σ"
        by blast
      then have ln_c1: "c ≠ x ∧ (c,z) ∈ hp σ'"
        using assm_xyz by blast

      ― ‹We now establish the conclusion-part of @{term "can_be_marked s σ'"},
          using @{term "(c,z)"} as the witness to the existential quantifier.›
      
      ― ‹Clause 2 of 3, done first because it is needed later›
      have ln_c2: "c ∉ s ∨ c ∉ marked σ'"
        by (metis all_ok_def assm_ab assm_ok ln_ab_xy ln_c ln_marked_eq
            fst_conv snd_conv)
        
      ― ‹Clause 1 of 3›
      moreover
      have "c ∈ reach (roots σ') (hp σ') ∨ c ∈ reach (marked σ' ∩ - s) (hp σ')"
       (is "?Clause1 c")
      proof -
        define Q where "Q = (λw. ?Clause1 w ∨ (w ∈ marked σ' ∧ w ∈ s))"
        have ln_marked_Q: "⋀ w. w ∈ marked σ ⟹ Q w"
          by (metis reach_base assm_step post_change_def IntI Q_def Compl_iff)
        have "⋀ w. reachable σ w ⟹ Q w"
        proof -
          fix w assume assm_reachable: "reachable σ w"
          show "Q w"
          proof (rule reach_induct[where P=Q and S="roots σ" and R="hp σ"],
                 goal_cases)
            case 1
            then show ?case by (meson assm_reachable reachable_def)
          next
            case 2
            then show ?case using assm_roots_marked ln_marked_Q by blast
          next
            case (3 u v)
            assume assm_ln_1: "u ∈ reach (roots σ) (hp σ)"
               and assm_ln_2: "Q u"
               and assm_ln_3: "(u,v) ∈ hp σ"
            have v_r: "reachable σ v"
              unfolding reachable_def by (rule reach_step[OF assm_ln_1 assm_ln_3])
            show ?case
            proof (cases "(u,v) = (x,y)")
              case True
              then have "v ∈ marked σ"
                by (metis assm_ab assm_ln_3 assm_ok all_ok_def ln_ab_xy ln_marked_eq
                          Int_iff fst_conv snd_conv)
              then show ?thesis using ln_marked_Q by simp
            next
              case False
              then have "(u,v) ∈ hp σ'"
                using assm_xyz assm_ln_3 by auto
              moreover have "Q u"
                using assm_ln_2 unfolding Q_def by auto
              ultimately show ?thesis unfolding Q_def
                apply (elim disjE)
                  apply (metis reach_step)
                 apply (metis reach_step)
                by (metis assm_ok all_ok_def assm_ln_3 ln_marked_Q ln_marked_eq
                          Q_def fst_conv snd_conv)
            qed
          qed
        qed ― ‹for @{theory_text "⋀ w. reachable σ w ⟹ Q w"}›
        then show ?thesis
          using ln_c ln_c2 unfolding Q_def by blast
      qed ― ‹for Clause 2 of 3›

      ― ‹Clause 3 of 3›
      moreover have "a ≠ c ∧ b = z"
        using ln_ab_xy ln_c1 by blast

      ultimately have "(∃ zw ∈ hp σ'.
              (fst zw ∈ reach (roots σ') (hp σ') ∨
               fst zw ∈ reach (marked σ' ∩ - s) (hp σ')) ∧
              (fst zw ∉ s ∨ fst zw ∉ marked σ') ∧ a ≠ fst zw ∧ b = snd zw)"
        using ln_c1 by force
    }
    then show ?thesis unfolding can_be_marked_def by simp
  qed
qed

lemma stable_can_be_marked_remove:
  assumes "post_change σ σ' ∧ post_change_remove σ σ'"
      and "all_ok s σ"
    shows "can_be_marked s σ'"
  unfolding can_be_marked_def apply clarsimp
  by (metis all_ok_def assms fst_eqD snd_eqD stable_all_ok_remove)

subsection ‹Lemma 1›

text ‹This subsection establishes Lemma 1 from the paper, which concerns the
properties that follow from a Mutator change.›

lemma lemma_1_can_be_marked:
  assumes assm_step: "post_change σ σ'"
      and assm_all_ok: "all_ok s σ"
      and assm_roots_marked: "roots σ ⊆ marked σ"
    shows "can_be_marked s σ'"
proof -
  from assm_step have "post_change_remove σ σ' ∨ post_change_redirect σ σ'"
    using post_change_def by fast
  then show ?thesis
  proof (standard, goal_cases remove redirect)
    case remove
    then show ?case
      using stable_can_be_marked_remove 
      by (metis stable_can_be_marked_remove remove assm_step assm_all_ok)
  next
    case redirect
    then show ?case 
      using assms stable_can_be_marked_redirect post_change_def by blast
  qed
qed

lemma lemma_1_tbm_put:
  assumes assm_step:   "post_change σ σ'"
      and assm_all_ok: "all_ok s σ"
    shows "tbm_put s σ'"
proof -
  have "⋀ xy. xy ∈ hp σ' ⟹ tbm σ' ≠ Some (snd xy) ⟹ xy ∈ hp σ"
  proof -
    fix xy
    assume assm_local_hp: "xy ∈ hp σ'"
       and assm_local_tbm: "tbm σ' ≠ Some (snd xy)"
    have "post_change_remove σ σ' ∨ post_change_redirect σ σ'"
      using assm_step unfolding post_change_def by blast
    then show "xy ∈ hp σ"
      apply standard
      using assm_local_hp post_change_remove_def apply blast
      by (metis assm_local_hp assm_local_tbm post_change_redirect_def
                DiffI singletonD snd_conv)
  qed
  then show ?thesis
    using assm_all_ok assm_step
    unfolding all_ok_def post_change_def tbm_put_def
    by fastforce
qed

lemma lemma_1:
  assumes "post_change σ σ'"
      and "all_ok s σ"
      and "roots σ ⊆ marked σ"
    shows "can_be_marked s σ' ∧ tbm_put s σ'"
  using assms lemma_1_can_be_marked lemma_1_tbm_put by blast

subsection ‹Lemma 2›

text ‹This subsection establishes Lemma 2 from the paper: after a Mutator step
that marks @{term tbm} and @{term tbm_put}, either @{term all_ok} holds or the
number of marked nodes increases.›

lemma lemma_2:
  assumes "tbm_put s σ"
      and "post_mark_tbm σ σ'"
    shows "all_ok s σ' ∨ (marked σ ⊂ marked σ')"
  using assms unfolding tbm_put_def post_mark_tbm_def apply clarsimp
  by (metis all_ok_def antisym_conv1 insert_iff option.distinct(1) option.inject
      subset_insertI)

section ‹Theorems›

subsection ‹Holds for All›

text ‹This establishes the @{text forall_guar_p_w} premise when instantiating
the @{text holds_for_all} lemma to the concurrent garbage collector.
Here, @{term p} is @{term "all_ok w σ"} and @{term q} is
@{text "can_be_marked w σ' ∨ marked σ ⊂ marked σ'"}.›

lemma works_for_all_w:
  assumes "post_change σ σ' ∨ post_mark_tbm σ σ'"
      and "inv_roots σ"
      and "all_ok w σ"
    shows "can_be_marked w σ' ∨ marked σ ⊂ marked σ'"
  by (metis assms all_ok_conseqs inv_roots_def lemma_1 lemma_2)

text ‹This lemma continues the @{text works_for_all_w} reasoning, 
but with @{text q} extended to include the case where the Collector's
local variables are unchanged and the marking only increases.›

theorem works_for_all_w2:
  assumes "post_change σ σ' ∨ post_mark_tbm σ σ'"
      and "inv_roots σ"
      and "all_ok w σ"
    shows "marked σ ⊆ marked σ' ∧ localCvar σ = localCvar σ' ∧
           (can_be_marked w σ' ∨ marked σ ⊂ marked σ')"
proof (intro conjI, goal_cases)
  case 1 show ?case
    using assms(1) unfolding post_change_def post_mark_tbm_def by blast
next
  case 2 show ?case
    using assms(1) unfolding post_change_def post_mark_tbm_def by blast
next
  case 3 show ?case
    using assms works_for_all_w by blast
qed

text ‹This theorem shows that the rely of the Collector holds,
based on the @{theory_text holds_for_all} reasoning.›

theorem using_holds_for_all2:
  assumes "post_change σ σ' ∨ post_mark_tbm σ σ'"
      and "all_ok s σ"
      and "∀ w. ((post_change σ σ' ∨ post_mark_tbm σ σ') ∧ all_ok w σ)
            ⟶ (marked σ ⊆ marked σ' ∧ localCvar σ = localCvar σ' ∧
                 (can_be_marked w σ' ∨ marked σ ⊂ marked σ'))"
      and "all_ok s σ ∧ marked σ ⊆ marked σ' ∧ localCvar σ = localCvar σ' ∧
           (can_be_marked s σ' ∨ marked σ ⊂ marked σ')
           ⟶ rely_collector σ σ'"
    shows "rely_collector σ σ'"
  using assms holds_for_all by force

subsection ‹Propagate›

lemma chain_mono:
  "⟦ ⋀ m. f m ⊆ f (Suc m) ; a ≤ b ⟧ ⟹ f a ⊆ f b"
  using lift_Suc_mono_le by blast

lemma chain_anti:
  "⟦ ⋀ m. f (Suc m) ⊆ f m ; a ≤ b ⟧ ⟹ f b ⊆ f a"
  using lift_Suc_antimono_le by blast

text ‹This theorem shows that @{term post_propagate} holds over a sequence of steps, 
where each step either satisfies @{term rely_collector} or @{term guar_collector}, 
and the @{term safe} and @{term consid} sets are initially empty.›

theorem propagate_seq:
    fixes st :: "nat ⇒ 'a state"
  assumes step: "⋀ m. rely_collector (st m) (st (Suc m))
                    ∨ guar_collector (st m) (st (Suc m))"
      and init_empty: "safe (localCvar (st 0)) = {} ∧
                     consid (localCvar (st 0)) = {}"
    shows "post_propagate (st 0) (st n)"
proof -
  have init_eq: "safe (localCvar (st 0)) = consid (localCvar (st 0))"
    using init_empty by simp
  have ok0: "all_ok (safe (localCvar (st 0))) (st 0)"
    using init_empty all_ok_def by blast
  have mark_step: "⋀m. marked (st m) ⊆ marked (st (Suc m))"
    by (metis rely_collector_def guar_collector_def local.step)
  have safe_step: "⋀m. safe (localCvar (st (Suc m))) ⊆ safe (localCvar (st m))"
    by (metis rely_collector_def guar_collector_def local.step dual_order.refl)

  have "⋀x y. (x,y) ∈ hp (st 0) ⟹ x ∈ marked (st n) ⟹
                   x ∈ consid (localCvar (st n)) ⟹
                   y ∈ marked (st n) ∨ marked (st 0) ⊂ marked (st n)"
  proof -
    fix x y assume "(x,y) ∈ hp (st 0)"
               and "x ∈ marked (st n)"
               and local_assm3: "x ∈ consid (localCvar (st n))"
    show "y ∈ marked (st n) ∨ marked (st 0) ⊂ marked (st n)"
    proof -
      { assume "¬ (marked (st 0) ⊂ marked (st n))"
        moreover have "marked (st 0) ⊆ marked (st n)"
          by (rule chain_mono[of "λm. marked (st m)", OF mark_step, of 0 n]) simp
        ultimately have eqn: "marked (st 0) = marked (st n)"
          by simp

        ― ‹marked is constant on 0..n›
        have eqm: "⋀m. m ≤ n ⟹ marked (st m) = marked (st 0)"
        proof -
          fix m assume assm: "m ≤ n"
          then have "marked (st m) ⊆ marked (st n)"
            by (rule chain_mono[of "λm. marked (st m)", OF mark_step, of m n])
          moreover have "marked (st 0) ⊆ marked (st m)"
            apply (rule chain_mono[of "λm. marked (st m)", OF mark_step, of 0 m])
            by simp
          ultimately show "marked (st m) = marked (st 0)"
            using eqn by blast
        qed

        ― ‹@{text "safe = consid"} holds at every state up to n, by induction from 0›
        have all_eq: "⋀m. m ≤ n ⟹
                       safe (localCvar (st m)) = consid (localCvar (st m))"
        proof -
          fix m show "m ≤ n ⟹
                      safe (localCvar (st m)) = consid (localCvar (st m))"
            apply (induction m)
             apply (rule init_eq)
            apply clarsimp
            by (metis rely_collector_def local.step guar_collector_def psubsetE)
        qed

        have "safe (localCvar (st n)) = consid (localCvar (st n))"
          by (rule all_eq[OF order_refl])
        moreover
        have s_down: "safe (localCvar (st n)) ⊆ safe (localCvar (st 0))"
          by (rule chain_anti[of "λm. safe (localCvar (st m))",
              OF safe_step, of 0 n]) simp
        ultimately have "x ∈ safe (localCvar (st 0))"
          using local_assm3 by auto
        then have "y ∈ marked (st n)"
          using init_empty by blast
      }
      then show ?thesis by blast
    qed
  qed

  then show ?thesis unfolding post_propagate_def by force
qed

subsection ‹Every Reachable Node Is Marked›

text ‹This final theorem establishes the overall post condition of the Collector,
that ``if a node is reachable initially, then it has been marked by the Collector.›

theorem reachable_subset_marked:
  assumes assm_post: "post_propagate σ σ'"
      and assm_marked: "marked σ' = marked σ"
      and assm_roots: "roots σ ⊆ marked σ"
      and assm_consid: "consid (localCvar σ') = Field (hp σ)"
          ― ‹@{term consid} contains all the nodes in the heap.›
    shows "∀ w. reachable σ w ⟶ w ∈ marked σ"
proof (intro allI impI)
  fix w assume "reachable σ w"
  hence hw: "w ∈ reach (roots σ) (hp σ)" unfolding reachable_def .
  show "w ∈ marked σ"
  proof (rule reach_induct[where P="λu. u ∈ marked σ", OF hw])
    fix u assume "u ∈ roots σ"
    thus "u ∈ marked σ" using assm_roots by blast
  next
    fix u v
    assume "u ∈ marked σ" and "(u,v) ∈ hp σ"
    moreover from this have "u ∈ marked σ' ∧ u ∈ consid (localCvar σ')"
      using assm_marked Field_iff assm_consid by force
    ultimately show "v ∈ marked σ"
      by (metis assm_marked assm_post post_propagate_def Int_iff psubsetE split_conv)
  qed
qed

end