Theory WickersonDoddsParkinson

(*<*)
theory WickersonDoddsParkinson
imports
  "Assume_Guarantee"
begin

(*>*)
section‹ Wickerson, Dodds and Parkinson: explicit stabilisation\label{sec:explicit_stabilisation} ›

text‹

Notes on \<^citet>‹"WickersonDoddsParkinson:2010"› (all references here are to the technical report):
 ▪ motivation: techniques for eliding redundant stability conditions
  ▪ the standard rules check the interstitial assertion in ‹c ; d› twice
 ▪ they claim in \S7 to supersede the ``mid stability'' of \<^citet>‹‹\S4.1› in "Vafeiadis:2008"› (wssa, sswa)
 ▪ Appendix D:
  ▪ not a complete set of rules
  ▪ \textsc{AtomR-S} does not self-compose: consider ‹c ; d› -- the interstitial assertion is either a floor or ceiling
   ▪ every step therefore requires a use of weakening/monotonicity

The basis of their approach is to make assertions a function of a
relation (a ∗‹rely›). By considering a set of
relations, a single rely-guarantee specification can satisfy several
call sites. Separately they tweak the RGSep rules of \<^citet>‹"Vafeiadis:2008"›.

The definitions are formally motivated as follows (\S3):

\begin{quote}

Our operators can also be defined using Dijkstra's predicate
transformer semantics: ‹⌊p⌋R› is the
weakest precondition of ‹R⇧^*› given postcondition
‹p›, while ‹⌈p⌉R› is the
strongest postcondition of ‹R⇧^*› given
pre-condition ‹p›.

\end{quote}

The following adapts their definitions and proofs to our setting.

›

setup ‹Sign.mandatory_path "wdp"›

definition floor :: "'a rel ⇒ 'a pred ⇒ 'a pred" where ―‹ An interior operator, or a closure in the dual lattice ›
  "floor r P s ⟷ (∀s'. (s, s') ∈ r⇧^* ⟶ P s')"

definition ceiling :: "'a rel ⇒ 'a pred ⇒ 'a pred" where ―‹ A closure operator ›
  "ceiling r P s ⟷ (∃s'. (s', s) ∈ r⇧^* ∧ P s')"

setup ‹Sign.mandatory_path "floor"›

lemma empty_rel[simp]:
  shows "wdp.floor {} P = P"
by (simp add: wdp.floor_def fun_eq_iff)

lemma reflcl:
  shows "wdp.floor (r⇧⁼) = wdp.floor r"
by (simp add: wdp.floor_def fun_eq_iff)

lemma const:
  shows "wdp.floor r ⟨c⟩ = ⟨c⟩"
by (auto simp: wdp.floor_def fun_eq_iff)

lemma contractive:
  shows "wdp.floor r P ≤ P"
by (simp add: wdp.floor_def le_fun_def le_bool_def)

lemma idempotent:
  shows "wdp.floor r (wdp.floor r P) = wdp.floor r P"
by (auto simp: fun_eq_iff wdp.floor_def dest: rtrancl_trans)

lemma mono:
  assumes "r' ⊆ r"
  assumes "P ≤ P'"
  shows "wdp.floor r P ≤ wdp.floor r' P'"
using assms by (auto 6 0 simp add: wdp.floor_def le_bool_def le_fun_def dest: rtrancl_mono)

lemma strengthen[strg]:
  assumes "st_ord (¬F) r r'"
  assumes "st_ord F P P'"
  shows "st_ord F (wdp.floor r P) (wdp.floor r' P')"
using assms by (cases F; simp add: wdp.floor.mono)

lemma weakest:
  assumes "Q ≤ P"
  assumes "stable r Q"
  shows "Q ≤ wdp.floor r P"
using assms by (simp add: wdp.floor_def stable_def monotone_def le_fun_def le_bool_def) (metis rtrancl_induct)

lemma Chernoff:
  assumes "P ≤ Q"
  shows "(wdp.floor r P ❙∧ Q) ≤ wdp.floor r Q"
using assms by (simp add: wdp.floor_def le_fun_def le_bool_def)

lemma floor1:
  assumes "r ⊆ r'"
  shows "wdp.floor r' (wdp.floor r P) = wdp.floor r' P"
unfolding wdp.floor_def by (meson assms rtrancl_cl.cl_mono rtrancl_eq_or_trancl rtrancl_trans)

lemma floor2:
  assumes "r ⊆ r'"
  shows "wdp.floor r (wdp.floor r' P) = wdp.floor r' P"
by (metis assms antisym wdp.floor.contractive wdp.floor.idempotent wdp.floor.mono)

setup ‹Sign.parent_path›

interpretation ceiling: closure_complete_lattice_distributive_class "wdp.ceiling r" for r
by standard (auto 5 0 simp: wdp.ceiling_def le_fun_def le_bool_def dest: rtrancl_trans)

setup ‹Sign.mandatory_path "ceiling"›

lemma empty_rel[simp]:
  shows "wdp.ceiling {} P = P"
by (simp add: wdp.ceiling_def fun_eq_iff)

lemma reflcl:
  shows "wdp.ceiling (r⇧⁼) = wdp.ceiling r"
by (simp add: wdp.ceiling_def fun_eq_iff)

lemma const:
  shows "wdp.ceiling r ⟨c⟩ = ⟨c⟩"
by (auto simp: wdp.ceiling_def fun_eq_iff)

lemma mono:
  assumes "r ⊆ r'"
  assumes "P ≤ P'"
  shows "wdp.ceiling r P ≤ wdp.ceiling r' P'"
using assms by (auto 7 0 simp: wdp.ceiling_def le_bool_def le_fun_def dest: rtrancl_mono)

lemma strengthen[strg]:
  assumes "st_ord F r r'"
  assumes "st_ord F P P'"
  shows "st_ord F (wdp.ceiling r P) (wdp.ceiling r' P')"
using assms by (cases F; simp add: wdp.ceiling.mono)

lemma strongest:
  assumes "P ≤ Q"
  assumes "stable r Q"
  shows "wdp.ceiling r P ≤ Q"
using assms by (simp add: wdp.ceiling_def stable_def monotone_def le_fun_def le_bool_def) (metis rtrancl_induct)

lemma ceiling1:
  assumes "r ⊆ r'"
  shows "wdp.ceiling r' (wdp.ceiling r P) = wdp.ceiling r' P"
unfolding wdp.ceiling_def by (meson assms rtrancl_cl.cl_mono rtrancl_eq_or_trancl rtrancl_trans)

lemma ceiling2:
  assumes "r ⊆ r'"
  shows "wdp.ceiling r (wdp.ceiling r' P) = wdp.ceiling r' P"
by (metis assms antisym wdp.ceiling.ceiling1 wdp.ceiling.expansive wdp.ceiling.idempotent(1))

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "stable"›

lemma floor:
  shows "stable r (wdp.floor r P)"
unfolding wdp.floor_def stable_def monotone_def by (simp add: converse_rtrancl_into_rtrancl le_boolI)

lemma ceiling:
  shows "stable r (wdp.ceiling r P)"
by (fastforce simp: wdp.ceiling_def stable_def monotone_def le_bool_def
              dest: rtrancl_into_rtrancl)

lemma floor_conv:
  assumes "stable r P"
  shows "P = wdp.floor r P"
using assms unfolding wdp.floor_def stable_def monotone_def le_bool_def fun_eq_iff
by (metis rtrancl_refl rtrancl_induct)

lemma ceiling_conv:
  assumes "stable r P"
  shows "P = wdp.ceiling r P"
using assms unfolding wdp.ceiling_def stable_def monotone_def le_bool_def fun_eq_iff
by (metis rtrancl_refl rtrancl_induct)

setup ‹Sign.parent_path›

lemma floor_alt_def: ―‹ \<^citet>‹‹\S3› in "WickersonDoddsParkinson:2010"› ›
  shows "wdp.floor r P = ⨆{Q. Q ≤ P ∧ stable r Q}"
by (rule antisym)
   (auto simp: Sup_upper wdp.floor.contractive wdp.stable.floor
        intro: wdp.floor.weakest[unfolded le_bool_def le_fun_def, rule_format])

lemma ceiling_alt_def: ―‹ \<^citet>‹‹\S3› in "WickersonDoddsParkinson:2010"› ›
  shows "wdp.ceiling r P = ⨅{Q. P ≤ Q ∧ stable r Q}"
by (rule antisym)
   (auto simp: Inf_lower wdp.ceiling.expansive wdp.stable.ceiling
         dest: wdp.ceiling.strongest[unfolded le_bool_def le_fun_def, rule_format, rotated])

lemma duality_floor_ceiling:
  shows "wdp.ceiling r (❙¬P) = (❙¬wdp.floor (r¯) P)"
by (simp add: wdp.ceiling_def wdp.floor_def fun_eq_iff rtrancl_converse)

lemma ceiling_floor:
  assumes "r ⊆ r'"
  shows "wdp.ceiling r (wdp.floor r' P) = wdp.floor r' P"
by (metis assms wdp.ceiling.ceiling2 wdp.stable.ceiling_conv wdp.stable.floor)

lemma floor_ceiling:
  assumes "r ⊆ r'"
  shows "wdp.floor r (wdp.ceiling r' P) = wdp.ceiling r' P"
by (metis assms wdp.floor.floor2 wdp.stable.ceiling wdp.stable.floor_conv)

lemma floor_ceilr:
  shows "wdp.floor (ceilr P) P = P"
by (metis ceilr.stable wdp.stable.floor_conv)

lemma ceiling_ceilr:
  shows "wdp.ceiling (ceilr P) P = P"
by (metis ceilr.stable wdp.stable.ceiling_conv)

setup ‹Sign.parent_path›


subsection‹ Assume/Guarantee rules\label{sec:explicit_stabilisation-ag} ›

paragraph‹ \S3.2 traditional assume/guarantee rules ›

setup ‹Sign.mandatory_path "wdp"›

lemma action: ―‹ arbitrary ‹A› ›
  fixes F :: "('v × 's × 's) set"
  assumes Q: "⋀v s s'. ⟦P s; (v, s, s') ∈ F⟧ ⟹ Q v s'"
  assumes G: "⋀v s s'. ⟦P s; s ≠ s'; (v, s, s') ∈ F⟧ ⟹ (s, s') ∈ G"
  shows "prog.p2s (prog.action F) ≤ ⦃wdp.floor A P⦄, A ⊢ G, ⦃λv. wdp.ceiling A (Q v)⦄"
by (rule ag.prog.action)
   (auto simp: wdp.stable.floor wdp.stable.ceiling
        intro: G
         dest: Q[rotated]
         elim: wdp.floor.contractive[unfolded le_fun_def le_bool_def, rule_format]
               wdp.ceiling.expansive[unfolded le_fun_def le_bool_def, rule_format])

lemmas mono = ag.mono
lemmas bind = ag.prog.bind

text‹ etc. -- the other rules are stock ›

setup ‹Sign.parent_path›


paragraph‹ \S4, Appendix C parametric specifications ›

definition pag :: "('s rel ⇒ 's pred) ⇒ 's rel set ⇒ 's rel ⇒ ('s rel ⇒ 'v ⇒ 's pred) ⇒ (sequential, 's, 'v) spec" ("⦃_⦄, _/ ⊢⇩_P _, ⦃_⦄" [0,0,0,0] 100) where
  "⦃P⦄, As ⊢⇩_P G, ⦃Q⦄ = (⨅A∈As. ⦃P A⦄, A ⊢ G, ⦃Q A⦄)"

setup ‹Sign.mandatory_path "pag"›

lemma empty:
  shows "⦃P⦄, {} ⊢⇩_P G, ⦃Q⦄ = ⊤"
by (simp add: pag_def)

lemma singleton:
  shows "⦃P⦄, {A} ⊢⇩_P G, ⦃Q⦄ = ⦃P A⦄, A ⊢ G, ⦃Q A⦄"
by (simp add: pag_def)

lemma mono: ―‹ strengthening of the ▩‹WEAKEN› rule in Figure~4, needed for the example  ›
  assumes "⋀A. A ∈ As' ⟹ P' A ≤ P A"
  assumes "As' ≤ As"
  assumes "G ≤ G'"
  assumes "⋀A. A ∈ As' ⟹ Q A ≤ Q' A"
  shows "⦃P⦄, As ⊢⇩_P G, ⦃Q⦄ ≤ ⦃P'⦄, As' ⊢⇩_P G', ⦃Q'⦄"
by (simp add: assms pag_def INF_superset_mono[OF ‹As' ≤ As› ag.mono] le_funD)

lemma action: ―‹ allow assertions to depend on assume ‹A›, needed for the example ›
  fixes F :: "('v × 's × 's) set"
  assumes Q: "⋀A v s s'. ⟦A ∈ As; P A s; (v, s, s') ∈ F⟧ ⟹ Q A v s'"
  assumes G: "⋀A v s s'. ⟦A ∈ As; P A s; s ≠ s'; (v, s, s') ∈ F⟧ ⟹ (s, s') ∈ G"
  shows "prog.p2s (prog.action F) ≤ ⦃λA. wdp.floor A (P A)⦄, As ⊢⇩_P G, ⦃λA v. wdp.ceiling A (Q A v)⦄"
by (simp add: assms pag_def wdp.action INFI)

lemmas sup = ag.prog.sup

lemma bind:
  assumes "⋀v. prog.p2s (g v) ≤ ⦃λA. Q' A v⦄, As ⊢⇩_P G, ⦃Q⦄"
  assumes "prog.p2s f ≤ ⦃P⦄, As ⊢⇩_P G, ⦃Q'⦄"
  shows "prog.p2s (f ⤜ g) ≤ ⦃P⦄, As ⊢⇩_P G, ⦃Q⦄"
unfolding pag_def
by (fastforce intro: INFI ag.prog.bind[rotated]
                     order.trans[OF assms(2) pag.mono[OF _ _ _ order.refl]]
                     order.trans[OF assms(1) pag.mono[where As'="{A}" for A], simplified pag.singleton]
          simp flip: pag.singleton)+

lemma parallel:
  assumes "prog.p2s c⇩₁ ≤ ⦃P⇩₁⦄, (∪) G⇩₂ ` A ⊢⇩_P G⇩₁, ⦃Q⇩₁⦄"
  assumes "prog.p2s c⇩₂ ≤ ⦃P⇩₂⦄, (∪) G⇩₁ ` A ⊢⇩_P G⇩₂, ⦃Q⇩₂⦄"
  shows "prog.p2s (prog.parallel c⇩₁ c⇩₂)
      ≤ ⦃λR. P⇩₁ (R ∪ G⇩₂) ❙∧ P⇩₂ (R ∪ G⇩₁)⦄, A ⊢⇩_P G⇩₁ ∪ G⇩₂, ⦃λR v. Q⇩₁ (R ∪ G⇩₂) v ❙∧ Q⇩₂ (R ∪ G⇩₁) v⦄"
unfolding pag_def
by (force intro: INFI ag.prog.parallel order.trans[OF assms(1) pag.mono]
                 order.trans[OF assms(2) pag.mono]
      simp flip: pag.singleton)

text‹ etc. -- the other rules follow similarly ›

setup ‹Sign.parent_path›


subsection‹ Examples\label{sec:explicit_stabilisation_eg} ›

text‹

There is not always a single (traditional) most general assume/guarantee specification (\S2.1).

›

type_synonym state = int ―‹ just ‹x› ›
abbreviation (input) "incr ≡ prog.write ((+) 1)" ―‹ atomic increment ›
abbreviation (input) increases :: "int rel" where "increases ≡ {(x, x'). x ≤ x'}"

lemma ag_incr1: ―‹ the precondition is stable as the rely is very strong ›
  shows "prog.p2s incr ≤ ⦃(=) c⦄, {} ⊢ increases, ⦃⟨(=) (c + 1)⟩⦄"
by (rule ag.prog.action; simp add: stable.empty)

lemma ag_incr2: ―‹ note the weaker precondition due to the larger assume ›
  shows "prog.p2s incr ≤ ⦃(≤) c⦄, increases ⊢ increases, ⦃⟨(≤) (c + 1)⟩⦄"
by (rule ag.prog.action; auto simp: stable_def monotone_def le_bool_def)

lemma ag_incr1_par_incr1:
  shows "prog.p2s (incr ∥ incr) ≤ ⦃λx. c ≤ x⦄, increases ⊢ increases, ⦃λ_ x. c + 1 ≤ x⦄"
apply (rule ag.pre_pre)
 apply (rule ag.pre_post)
  apply (rule ag.prog.parallel[where P⇩₁="λx. c ≤ x" and P⇩₂="λx. c ≤ x"
                                 and Q⇩₁="λ_ x. c + 1 ≤ x" and Q⇩₂="λ_ x. c + 1 ≤ x"
                                 and G⇩₁="increases" and G⇩₂="increases", simplified])
    apply (rule ag.prog.action; simp add: stable_def monotone_def le_boolI; fail)
   apply (rule ag.prog.action; simp add: stable_def monotone_def le_boolI; fail)
  apply simp_all
done

text‹

Using explicit stabilisation we can squash the two specifications for \<^const>‹incr› into a single one (\S4).

›

lemma ―‹ postcondition cannot be simplified for arbitrary ‹A› ›
  shows "prog.p2s incr ≤ ⦃wdp.ceiling A ((=) c)⦄, A ⊢ increases, ⦃⟨wdp.ceiling A (λs. wdp.ceiling A ((=) c) (s - 1))⟩⦄"
by (rule ag.pre_pre[OF wdp.action]) (simp add: wdp.floor_ceiling)+

―‹ The set of assumes that commute with the increment ›
abbreviation (input) comm_xpp :: "int rel set" where
  "comm_xpp ≡ {A. ∀p s. wdp.ceiling A p (s - 1) = wdp.ceiling A (λs. p (s - 1)) s}"

lemma pag_incr: ―‹ postcondition can be simplified wrt ‹comm_xpp› ›
  shows "prog.p2s incr ≤ ⦃λA. wdp.ceiling A ((=) c)⦄, comm_xpp ⊢⇩_P increases, ⦃λA. ⟨wdp.ceiling A ((=) (c + 1))⟩⦄"
apply (rule order.trans[OF _ pag.mono[OF _  order.refl order.refl]])
  apply (rule pag.action[where P="λA. wdp.ceiling A ((=) c)"
                           and Q="λA v s. wdp.ceiling A ((=) c) (s - 1)"])
   apply (simp_all add: wdp.floor_ceiling eq_diff_eq)
done

―‹ the two earlier specifications can be recovered ›
lemma
  shows "prog.p2s incr ≤ ⦃(=) c⦄, {} ⊢ increases, ⦃⟨(=) (c + 1)⟩⦄"
apply (rule order.trans[OF pag_incr])
apply (subst pag.singleton[symmetric])
apply (rule pag.mono; force)
done

lemma
  shows "prog.p2s incr ≤ ⦃(≤) c⦄, increases ⊢ increases, ⦃⟨(≤) (c + 1)⟩⦄"
apply (rule order.trans[OF pag_incr[where c=c]])
apply (subst pag.singleton[symmetric])
apply (rule pag.mono; force simp: wdp.ceiling_def order_rtrancl dest: zless_imp_add1_zle)
done

(*<*)

end
(*>*)