(*<*)
theory FindP
imports
  "Optics.Lenses"
  Assume_Guarantee
begin

declare lens_comp_def[simp] fst_lens_def[simp] snd_lens_def[simp]

lemma get_1[simp]:
  shows "get_L = id"
unfolding id_lens_def by simp

(*>*)
section‹ Example: findP\label{sec:ex_findP} ›

text‹

  demonstrate assume/guarantee reasoning by showing the safety of ‹findP›, a classic exercise in
  verification. It has been treated by at least:

 ▪ 🚫‹‹Example~5.1› in "KarpMiller:1969"›
 ▪ 🚫‹‹\S3› in "Rosen:1976"›
 ▪ 🚫‹‹\S4 Example~2› in "OwickiGries:1976"›
 ▪ 🚫‹‹\S2.4› in "Jones:1983"›
 ▪ 🚫‹‹\S3.1› in "XuCauCollette:1994"›
 ▪ 🚫‹‹p161› in "Brookes:1996"› (no proof)
 ▪ 🚫‹‹Examples~3.57~and~8.26› in "deRoeverEtAl:2001"› (atomic guarded commands)
 ▪ 🚫‹‹\S6.2› in "Dingel:2002"› (refinement)
 ▪ 🚫‹‹\S10› in "PrensaNieto:2003"› (mechanized, arbitrary number of threads)
 ▪ 🚫‹‹\S7.4, \S8.6› in "AptDeBoerOlderog:2009"›
 ▪ 🚫‹‹\S4› in "HayesJones:2017"› (refinement)

  take the task to be of finding the first element of a given
  ‹A› that satisfies a given predicate
 ‹pred›, if it exists, or yielding ‹length A›
  it does not. This search is performed with two threads: one
  the even indices and the other the odd. There is the
  of a thread terminating early if it notices that the other
  has found a better candidate than it could.

  generalise previous treatments by allowing the predicate to be
  modularly and to be a function of the state. It is required
  be pure, i.e., it cannot change the observable/shared state, though
  could have its own local state.

  search loops are defined recursively; one could just as easily use
 const‹prog.while›. We use a list and not an array for
  -- at this level of abstraction there is no difference --
  a mix of variables, where the monadic ones are purely local and
  state-based are shared between the threads. The lens allows the
  to be a value or reside in the (observable/shared) state.

 ›
(* The program and proofs should carry over to TSO directly: the assume is already strong enough. *)

type_synonym 's state = "(nat × nat) × 's"

abbreviation foundE :: "nat ==> 's state" where "foundE ≡ fst_L ;_L fst_L"
abbreviation foundO :: "nat ==> 's state" where "foundO ≡ snd_L ;_L fst_L"

context
  fixes pred :: "'a → ('s, bool) prog"
  fixes predPre :: "'s pred"
  fixes predP :: "'a → 's pred"
  fixes A :: "'s rel"
  fixes array :: "'a list ==> 's"
  ―‹ A guarantee of ‹Id› indicates that ‹pred a› is observationally pure. ›
  assumes iag_pred: "∧a. prog.p2s (pred a) ≤ {predPre \<and> ⟨a⟩ \<in> SET get}, A⁼ ∩ Id ∩ ceilr predPre ∩ Id _a ⊨ Id, {λrv. ⟨rv⟩ = predP a}"
begin

abbreviation array' :: "'a list ==> 's state" where "array' ≡ array ;_L snd_L"

partial_function (lfp) findP_loop_evens :: "nat → ('s state, unit) prog" where
  "findP_loop_evens i =
    do { fO ← prog.read get
       ; prog.whenM (i < fO)
          (do { v ← prog.read (λs. get_' s ! i)
              ; b ← prog.localize (pred v)
              ; if b then prog.write (λs. put s i) else findP_loop_evens (i + 2)
              })
       }"

partial_function (lfp) findP_loop_odds :: "nat → ('s state, unit) prog" where
  "findP_loop_odds i =
    do { fE ← prog.read get
       ; prog.whenM (i < fE)
          (do { v ← prog.read (λs. get_' s ! i)
              ; b ← prog.localize (pred v)
              ; if b then prog.write (λs. put s i) else findP_loop_odds (i + 2)
              })
       }"

definition findP :: "('s, nat) prog" where
  "findP = prog.local (
    do { N ← prog.read (SIZE get_')
       ; prog.write (λs. put s N)
       ; prog.write (λs. put s N)
       ; (findP_loop_evens 0 ∥ findP_loop_odds 1)
       ; fE ← prog.read (get)
       ; fO ← prog.read (get)
       ; prog.return (min fE fO)
       })"


paragraph‹ Relies and guarantees ›

abbreviation (input) A' :: "'s rel" where "A' ≡ A⁼ ∩ ceilr predPre ∩ (∩a. Id _a)"

definition AE :: "'s state rel" where
  "AE = UNIV ×_R A' ∩ Id_' ∩ Id ∩ \<le>"

definition GE :: "'s state rel" where
  "GE = Id ∩ Id ∩ \<le>"

definition AO :: "'s state rel" where
  "AO = UNIV ×_R A' ∩ Id_' ∩ Id ∩ \<le>"

definition GO :: "'s state rel" where
  "GO = Id ∩ Id ∩ \<le>"

lemma AG_refl_trans:
  shows
    "refl AE"
    "refl AO"
    "trans A ==> trans AE"
    "trans A ==> trans AO"
    "refl GE"
    "refl GO"
    "trans GE"
    "trans GO"
unfolding AE_def AO_def GE_def GO_def
by (auto simp: refl_inter_conv refl_relprod_conv
       intro!: trans_Int refl_UnionI refl_INTER trans_INTER)

lemma AG_containment:
  shows "GO ⊆ AE"
    and "GE ⊆ AO"
by (auto simp: AE_def AO_def GO_def GE_def refl_onD[OF ceilr.refl])

lemma G_containment:
  shows "GE ∪ GO ⊆ UNIV ×_R Id"
by (fastforce simp: GE_def GO_def)

paragraph‹ Safety proofs ›

lemma ag_findP_loop_evens:
  shows "prog.p2s (findP_loop_evens i)
       ≤ {⟨even i⟩ \<and> (λs. predPre (snd s)) \<and> get = SIZE get_' \<and> get \<le> SIZE get_'}, AE ⊨ GE,
                   {λ_. (get < SIZE get_' \<longrightarrow> localize1 predP $$ get_' ! get)
                      \<and> (\<forall>j. ⟨i ≤ j ∧ even j⟩ \<and> ⟨j⟩ < pred_min get get \<longrightarrow> \<not> localize1 predP $$ get_' ! ⟨j⟩)}"
proof(intro ag.gen_asm,
      induct arbitrary: i rule: findP_loop_evens.fixp_induct[case_names bot adm step])
  case (step R i) show ?case
apply (rule iag.init)
  apply (rule iag.intro)+
      ―‹ else branch, recursive call ›
      apply (rename_tac v va vb)
      apply (rule_tac P="⟨va⟩ = get_' ! ⟨i⟩ \<and> ⟨vb⟩ = localize1 predP va"
                   in iag.stable_augment[OF step.hyps])
        apply (simp add: ‹even i›; fail)
       apply clarsimp
       apply (metis ‹even i› even_Suc less_Suc_eq not_less)
      apply (force simp: GE_def AE_def stable_def monotone_def) (* stability for \<open>iag.stable_augment\<close> *)
     ―‹ ‹prog.localize (pred ...)› ›
     apply (rename_tac v va)
     apply (rule_tac Q="λvb. (λs. predPre (snd s)) \<and> get = SIZE get_' \<and> get \<le> SIZE get_' \<and> ⟨v⟩ \<le> SIZE get_' \<and> ⟨va⟩ = get_' ! ⟨i⟩ \<and> ⟨vb⟩ = localize1 predP va"
                  in ag.post_imp)
      apply (clarsimp simp: GE_def exI[where x="⟨i⟩ \<le> get"]; fail)
     apply (rule iag.pre_g[where G'=GE, OF iag.stable_augment_post[OF iag.augment_a[where A'=AE, OF ag.prog.localize_lift[OF iag_pred, simplified]]]])
      apply (fastforce simp: AE_def stable_def monotone_def)
     apply (metis AG_refl_trans(5) refl_alt_def)
    apply (rule iag.intro)+
 ―‹ precondition ›
 apply force
―‹ assume ›
apply (intro conjI Int_greatest INT_greatest ceilr.largest)
apply ((fastforce simp: stable_def monotone_def AE_def)+)[6]
apply (clarsimp simp: stable_def monotone_def AE_def GE_def; rule exI[where x="⟨i⟩ \<le> get"]; clarsimp; metis) (* FIXME ouch *)
apply (fastforce simp: stable_def monotone_def AE_def)+
done
qed simp_all

lemma ag_findP_loop_odds:
  shows "prog.p2s (findP_loop_odds i)
       ≤ {⟨odd i⟩ \<and> (λs. predPre (snd s)) \<and> get = SIZE get_' \<and> get \<le> SIZE get_'}, AO ⊨ GO,
                   {λ_. (get < SIZE get_' \<longrightarrow> localize1 predP $$ get_' ! get)
                      \<and> (\<forall>j. ⟨i ≤ j ∧ odd j⟩ \<and> ⟨j⟩ < pred_min get get \<longrightarrow> \<not> localize1 predP $$ get_' ! ⟨j⟩)}"
proof(intro ag.gen_asm,
      induct arbitrary: i rule: findP_loop_odds.fixp_induct[case_names bot adm step])
  case (step R i) show ?case
apply (rule iag.init)
  apply (rule iag.intro)+
      ―‹ else branch, recursive call ›
      apply (rename_tac v va vb)
      apply (rule_tac P="⟨va⟩ = get_' ! ⟨i⟩ \<and> ⟨vb⟩ = localize1 predP va"
                   in iag.stable_augment[OF step.hyps])
        apply (simp add: ‹odd i›; fail)
       apply clarsimp
       apply (metis ‹odd i› even_Suc less_Suc_eq not_less)
      apply (force simp: GO_def AO_def stable_def monotone_def) (* stability for \<open>ag.stable_augment\<close> *)
     ―‹ ‹prog.localize (pred ...)› ›
     apply (rename_tac v va)
     apply (rule_tac Q="λvb. (λs. predPre (snd s)) \<and> get = SIZE get_' \<and> get \<le> SIZE get_' \<and> ⟨v⟩ \<le> SIZE get_' \<and> ⟨va⟩ = get_' ! ⟨i⟩ \<and> ⟨vb⟩ = localize1 predP va"
                  in ag.post_imp)
      apply (clarsimp simp: GO_def exI[where x="⟨i⟩ \<le> get"]; fail)
     apply (rule iag.pre_g[where G'=GO, OF iag.stable_augment_post[OF iag.augment_a[where A'=AO, OF ag.prog.localize_lift[OF iag_pred, simplified]]]])
      apply (fastforce simp: AO_def stable_def monotone_def)
     apply (metis AG_refl_trans(6) refl_alt_def)
    apply (rule iag.intro)+
 ―‹ precondition ›
 apply force
―‹ assume ›
apply (intro conjI Int_greatest INT_greatest ceilr.largest)
apply ((fastforce simp: AO_def stable_def monotone_def)+)[6]
apply (clarsimp simp: AO_def GO_def stable_def monotone_def; rule exI[where x="⟨i⟩ \<le> get"]; clarsimp; metis) (* FIXME ouch *)
apply (fastforce simp: AO_def stable_def monotone_def)+
done
qed simp_all

theorem ag_findP:
  shows "prog.p2s findP
           ≤ {predPre}, A' ∩ Id
                ⊨ Id, {λv s. v = (LEAST i. i < SIZE get s ⟶ predP (get s ! i) s)}"
unfolding findP_def
apply (rule ag.prog.local)
apply (rule iag.init)
  apply (rule iag.intro)+
     apply (rule iag.augment_post_imp[where Q="λv. get \<le> SIZE get_' \<and> get \<le> SIZE get_'"])
     apply (rule iag.pre_g[OF _ G_containment])
     apply (rule iag.stable_augment_frame)
      apply (rule iag.parallel[OF ag_findP_loop_evens ag_findP_loop_odds _ AG_containment order.refl])
      ―‹ postcondition from ‹iag.parallel› ›
      apply clarsimp
      apply (rule Least_equality, linarith)
      subgoal for x y s z by (clarsimp simp: min_le_iff_disj not_less not_le dest!: spec[where x=z])
     ―‹ stability for ‹iag.stable_augment_frame› ›
     apply (force simp: stable_def monotone_def AE_def AO_def GE_def GO_def)
    apply (rule iag.intro)+
 ―‹ precondition ›
 apply fastforce
―‹ assume ›
 apply (simp;
        intro conjI Int_greatest INT_greatest ceilr.largest;
        fastforce simp: AE_def AO_def stable_def monotone_def)
done

end

text‹

  conclude by showing how we can instantiate the above with a ‹coprime› predicate.

 ›

setup ‹Sign.mandatory_path "gcd"›

type_synonym 's state = "(nat × nat) × 's"

abbreviation x :: "nat ==> 's gcd.state" where "x ≡ fst_L ;_L fst_L"
abbreviation y :: "nat ==> 's gcd.state" where "y ≡ snd_L ;_L fst_L"

definition seq :: "nat → nat → ('s, nat) prog" where
  "seq a b =
     prog.local (
       do { prog.write (λs. put_.x s a)
          ; prog.write (λs. put_.y s b)
          ; prog.while (λ_.
              do { xv ← prog.read get_.x
                 ; yv ← prog.read get_.y
                 ; if xv = yv
                   then prog.return (Inr ())
                   else (do { (if xv < yv
                               then prog.write (λs. put_.y s (yv - xv))
                               else prog.write (λs. put_.x s (xv - yv)))
                            ; prog.return (Inl ()) })
                 }) ()
          ; prog.read get_.x
          })"

setup ‹Sign.parent_path›

setup ‹Sign.mandatory_path "ag.gcd"›

lemma seq:
  shows "prog.p2s (gcd.seq a b) ≤ {⟨True⟩}, UNIV ⊨ Id, {λv. ⟨v = gcd a b⟩}"
unfolding gcd.seq_def
apply (rule ag.prog.local)
apply (rule iag.init)
  apply (rule iag.intro iag.while[where I="λ_ s. gcd (get_.x s) (get_.y s) = gcd a b"])+
 ―‹ precond ›
 apply (auto simp: gcd_diff1_nat)[1]
 apply (metis gcd.commute gcd_diff1_nat less_or_eq_imp_le)
―‹ assume ›
apply (intro stable.intro stable.local_only INFI infI)
apply auto
done

setup ‹Sign.parent_path›

definition findP_coprime :: "(nat × nat list, nat) prog" where
  "findP_coprime = findP (λa. prog.read get_L ⤜ gcd.seq a ⤜ (λc. prog.return (c = 1))) snd_L"

lemma ag_findP_coprime':
  shows "prog.p2s findP_coprime
           ≤ {⟨True⟩}, Id
                ⊨ Id, {λrv s. rv = (LEAST i. i < length (get_L s) ⟶ coprime (get_L s) (get_L s ! i))}"
unfolding findP_coprime_def
apply (rule iag.init)
  apply (rule ag_findP[where A=Id and array="snd_L" and predP="λb s. coprime (get_L s) b" and predPre="⟨True⟩"])
  apply (rule iag.init)
    apply (rule iag.intro)+
     apply (rule_tac Q="⟨⟨v⟩ = get_L⟩" in iag.augment_post_imp)
     apply (rule iag.stable_augment_frame)
      apply (rule iag.pre[OF ag.gcd.seq, where A'=Id and P'="⟨True⟩", simplified, OF order.refl])
      apply (clarsimp simp: ac_simps coprime_iff_gcd_eq_1 simp flip: One_nat_def; fail)
     apply (force simp: stable_def monotone_def)
    apply (rule iag.intro)+
 apply (simp; intro conjI INT_greatest ceilr.largest; fastforce simp: stable_def monotone_def)+
done

lemma ag_findP_coprime: ―‹ Shuffle the parameter to the precondition, exploiting purity. ›
  shows "prog.p2s findP_coprime
           ≤ {⟨a⟩ = get_L}, Id
                ⊨ Id, {λrv s. rv = (LEAST i. i < length (get_L s) ⟶ coprime a (get_L s ! i))}"
apply (rule ag.pre_pre)
 apply (rule ag.stable_augment_post[OF ag_findP_coprime'])
 apply (fastforce simp: stable_def)+
done
(*<*)

end
(*>*)