Theory FindP
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⇘1⇩L⇙ = id"
unfolding id_lens_def by simp
section‹ Example: findP\label{sec:ex_findP} ›
text‹
We demonstrate assume/guarantee reasoning by showing the safety of ‹findP›, a classic exercise in
concurrency verification. It has been treated by at least:
▪ \<^citet>‹‹Example~5.1› in "KarpMiller:1969"›
▪ \<^citet>‹‹\S3› in "Rosen:1976"›
▪ \<^citet>‹‹\S4 Example~2› in "OwickiGries:1976"›
▪ \<^citet>‹‹\S2.4› in "Jones:1983"›
▪ \<^citet>‹‹\S3.1› in "XuCauCollette:1994"›
▪ \<^citet>‹‹p161› in "Brookes:1996"› (no proof)
▪ \<^citet>‹‹Examples~3.57~and~8.26› in "deRoeverEtAl:2001"› (atomic guarded commands)
▪ \<^citet>‹‹\S6.2› in "Dingel:2002"› (refinement)
▪ \<^citet>‹‹\S10› in "PrensaNieto:2003"› (mechanized, arbitrary number of threads)
▪ \<^citet>‹‹\S7.4, \S8.6› in "AptDeBoerOlderog:2009"›
▪ \<^citet>‹‹\S4› in "HayesJones:2017"› (refinement)
We take the task to be of finding the first element of a given
array ‹A› that satisfies a given predicate
‹pred›, if it exists, or yielding ‹length A›
if it does not. This search is performed with two threads: one
searching the even indices and the other the odd. There is the
possibility of a thread terminating early if it notices that the other
thread has found a better candidate than it could.
We generalise previous treatments by allowing the predicate to be
specified modularly and to be a function of the state. It is required
to be pure, i.e., it cannot change the observable/shared state, though
it could have its own local state.
Our search loops are defined recursively; one could just as easily use
\<^const>‹prog.while›. We use a list and not an array for
simplicity -- at this level of abstraction there is no difference --
and a mix of variables, where the monadic ones are purely local and
the state-based are shared between the threads. The lens allows the
array to be a value or reside in the (observable/shared) state.
›
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"
assumes iag_pred: "⋀a. prog.p2s (pred a) ≤ ⦃predPre ❙∧ ⟨a⟩ ❙∈ SET get⇘array⇙⦄, A⇧= ∩ Id⇘get⇘array⇙⇙ ∩ ceilr predPre ∩ Id⇘predP 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⇘foundO⇙
; prog.whenM (i < fO)
(do { v ← prog.read (λs. get⇘array'⇙ s ! i)
; b ← prog.localize (pred v)
; if b then prog.write (λs. put⇘foundE⇙ 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⇘foundE⇙
; prog.whenM (i < fE)
(do { v ← prog.read (λs. get⇘array'⇙ s ! i)
; b ← prog.localize (pred v)
; if b then prog.write (λs. put⇘foundO⇙ s i) else findP_loop_odds (i + 2)
})
}"
definition findP :: "('s, nat) prog" where
"findP = prog.local (
do { N ← prog.read (SIZE get⇘array'⇙)
; prog.write (λs. put⇘foundE⇙ s N)
; prog.write (λs. put⇘foundO⇙ s N)
; (findP_loop_evens 0 ∥ findP_loop_odds 1)
; fE ← prog.read (get⇘foundE⇙)
; fO ← prog.read (get⇘foundO⇙)
; prog.return (min fE fO)
})"
paragraph‹ Relies and guarantees ›
abbreviation (input) A' :: "'s rel" where "A' ≡ A⇧= ∩ ceilr predPre ∩ (⋂a. Id⇘predP a⇙)"
definition AE :: "'s state rel" where
"AE = UNIV ×⇩R A' ∩ Id⇘get⇘array'⇙⇙ ∩ Id⇘get⇘foundE⇙⇙ ∩ ❙≤⇘get⇘foundO⇙⇙"
definition GE :: "'s state rel" where
"GE = Id⇘snd⇙ ∩ Id⇘get⇘foundO⇙⇙ ∩ ❙≤⇘get⇘foundE⇙⇙"
definition AO :: "'s state rel" where
"AO = UNIV ×⇩R A' ∩ Id⇘get⇘array'⇙⇙ ∩ Id⇘get⇘foundO⇙⇙ ∩ ❙≤⇘get⇘foundE⇙⇙"
definition GO :: "'s state rel" where
"GO = Id⇘snd⇙ ∩ Id⇘get⇘foundE⇙⇙ ∩ ❙≤⇘get⇘foundO⇙⇙"
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⟩ ❙∧ (λs. predPre (snd s)) ❙∧ get⇘foundE⇙ ❙= SIZE get⇘array'⇙ ❙∧ get⇘foundO⇙ ❙≤ SIZE get⇘array'⇙⦄, AE ⊢ GE,
⦃λ_. (get⇘foundE⇙ ❙< SIZE get⇘array'⇙ ❙⟶ localize1 predP ❙$❙$ get⇘array'⇙ ❙! get⇘foundE⇙)
❙∧ (❙∀j. ⟨i ≤ j ∧ even j⟩ ❙∧ ⟨j⟩ ❙< pred_min get⇘foundE⇙ get⇘foundO⇙ ❙⟶ ❙¬ localize1 predP ❙$❙$ get⇘array'⇙ ❙! ⟨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)+
apply (rename_tac v va vb)
apply (rule_tac P="⟨va⟩ ❙= get⇘array'⇙ ❙! ⟨i⟩ ❙∧ ⟨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)
apply (rename_tac v va)
apply (rule_tac Q="λvb. (λs. predPre (snd s)) ❙∧ get⇘foundE⇙ ❙= SIZE get⇘array'⇙ ❙∧ get⇘foundO⇙ ❙≤ SIZE get⇘array'⇙ ❙∧ ⟨v⟩ ❙≤ SIZE get⇘array'⇙ ❙∧ ⟨va⟩ ❙= get⇘array'⇙ ❙! ⟨i⟩ ❙∧ ⟨vb⟩ ❙= localize1 predP va"
in ag.post_imp)
apply (clarsimp simp: GE_def exI[where x="⟨i⟩ ❙≤ get⇘foundE⇙"]; 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)+
apply force
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⟩ ❙≤ get⇘foundE⇙"]; clarsimp; metis)
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⟩ ❙∧ (λs. predPre (snd s)) ❙∧ get⇘foundO⇙ ❙= SIZE get⇘array'⇙ ❙∧ get⇘foundE⇙ ❙≤ SIZE get⇘array'⇙⦄, AO ⊢ GO,
⦃λ_. (get⇘foundO⇙ ❙< SIZE get⇘array'⇙ ❙⟶ localize1 predP ❙$❙$ get⇘array'⇙ ❙! get⇘foundO⇙)
❙∧ (❙∀j. ⟨i ≤ j ∧ odd j⟩ ❙∧ ⟨j⟩ ❙< pred_min get⇘foundE⇙ get⇘foundO⇙ ❙⟶ ❙¬ localize1 predP ❙$❙$ get⇘array'⇙ ❙! ⟨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)+
apply (rename_tac v va vb)
apply (rule_tac P="⟨va⟩ ❙= get⇘array'⇙ ❙! ⟨i⟩ ❙∧ ⟨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)
apply (rename_tac v va)
apply (rule_tac Q="λvb. (λs. predPre (snd s)) ❙∧ get⇘foundO⇙ ❙= SIZE get⇘array'⇙ ❙∧ get⇘foundE⇙ ❙≤ SIZE get⇘array'⇙ ❙∧ ⟨v⟩ ❙≤ SIZE get⇘array'⇙ ❙∧ ⟨va⟩ ❙= get⇘array'⇙ ❙! ⟨i⟩ ❙∧ ⟨vb⟩ ❙= localize1 predP va"
in ag.post_imp)
apply (clarsimp simp: GO_def exI[where x="⟨i⟩ ❙≤ get⇘foundO⇙"]; 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)+
apply force
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⟩ ❙≤ get⇘foundO⇙"]; clarsimp; metis)
apply (fastforce simp: AO_def stable_def monotone_def)+
done
qed simp_all
theorem ag_findP:
shows "prog.p2s findP
≤ ⦃predPre⦄, A' ∩ Id⇘get⇘array⇙⇙
⊢ Id, ⦃λv s. v = (LEAST i. i < SIZE get⇘array⇙ s ⟶ predP (get⇘array⇙ 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⇘foundE⇙ ❙≤ SIZE get⇘array'⇙ ❙∧ get⇘foundO⇙ ❙≤ SIZE get⇘array'⇙"])
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])
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])
apply (force simp: stable_def monotone_def AE_def AO_def GE_def GO_def)
apply (rule iag.intro)+
apply fastforce
apply (simp;
intro conjI Int_greatest INT_greatest ceilr.largest;
fastforce simp: AE_def AO_def stable_def monotone_def)
done
end
text‹
We 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⇘gcd.x⇙ s a)
; prog.write (λs. put⇘gcd.y⇙ s b)
; prog.while (λ_.
do { xv ← prog.read get⇘gcd.x⇙
; yv ← prog.read get⇘gcd.y⇙
; if xv = yv
then prog.return (Inr ())
else (do { (if xv < yv
then prog.write (λs. put⇘gcd.y⇙ s (yv - xv))
else prog.write (λs. put⇘gcd.x⇙ s (xv - yv)))
; prog.return (Inl ()) })
}) ()
; prog.read get⇘gcd.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⇘gcd.x⇙ s) (get⇘gcd.y⇙ s) = gcd a b"])+
apply (auto simp: gcd_diff1_nat)[1]
apply (metis gcd.commute gcd_diff1_nat less_or_eq_imp_le)
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⇘fst⇩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⇘snd⇩L⇙ s) ⟶ coprime (get⇘fst⇩L⇙ s) (get⇘snd⇩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⇘fst⇩L⇙ s) b" and predPre="⟨True⟩"])
apply (rule iag.init)
apply (rule iag.intro)+
apply (rule_tac Q="⟨⟨v⟩ ❙= get⇘fst⇩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:
shows "prog.p2s findP_coprime
≤ ⦃⟨a⟩ ❙= get⇘fst⇩L⇙⦄, Id
⊢ Id, ⦃λrv s. rv = (LEAST i. i < length (get⇘snd⇩L⇙ s) ⟶ coprime a (get⇘snd⇩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