Theory Challenge2A
section ‹Challenge 2.A›
theory Challenge2A
imports "lib/VTcomp"
begin
text ‹Problem definition:
🌐‹https://ethz.ch/content/dam/ethz/special-interest/infk/chair-program-method/pm/documents/Verify%20This/Challenges%202019/cartesian_trees.pdf››
text ‹Polished and worked-over version.›
subsection ‹Specification›
text ‹We first fix the input, a list of integers›
context fixes xs :: "int list" begin
text ‹We then specify the desired output:
For each index ‹j›, return the greatest index ‹i<j› such that ‹xs!i < xs!j›, or ‹None› if
no such index exists.
Note that our indexes start at zero, and we use an option datatype to model that
no left-smaller value may exists.
›
definition
"left_spec j = (if (∃i<j. xs ! i < xs ! j) then Some (GREATEST i. i < j ∧ xs ! i < xs ! j) else None)"
text ‹The output of the algorithm should be an array ‹lf›, containing the indexes of the
left-smaller values:
›
definition "all_left_spec lf ≡ length lf = length xs ∧ (∀i<length xs. lf!i = left_spec i)"
subsection ‹Auxiliary Theory›
text ‹We derive some theory specific to this algorithm›
subsubsection ‹Has-Left and The-Left›
text ‹We split the specification of nearest left value into a predicate and a total function›
definition "has_left j = (∃i<j. xs ! i < xs ! j)"
definition "the_left j = (GREATEST i. i < j ∧ xs ! i < xs ! j)"
lemma left_alt: "left_spec j = (if has_left j then Some (the_left j) else None)"
by (auto simp: left_spec_def has_left_def the_left_def)
lemma the_leftI: "has_left j ⟹ the_left j < j ∧ xs!the_left j < xs!j"
apply (clarsimp simp: has_left_def the_left_def)
by (metis (no_types, lifting) GreatestI_nat less_le_not_le nat_le_linear pinf(5))
lemma the_left_decr[simp]: "has_left i ⟹ the_left i < i"
by (simp add: the_leftI)
lemma le_the_leftI:
assumes "i≤j" "xs!i < xs!j"
shows "i ≤ the_left j"
using assms unfolding the_left_def
by (metis (no_types, lifting)
Greatest_le_nat le_less_linear less_imp_not_less less_irrefl
order.not_eq_order_implies_strict)
lemma the_left_leI:
assumes "∀k. j<k ∧ k<i ⟶ ¬xs!k<xs!i"
assumes "has_left i"
shows "the_left i ≤ j"
using assms
unfolding the_left_def has_left_def
apply auto
by (metis (full_types) the_leftI assms(2) not_le the_left_def)
subsubsection ‹Derived Stack›
text ‹We note that the stack in the algorithm doesn't contain any
extra information. It can be derived from the left neighbours that have been
computed so far:
The first element of the stack is the current index - 1, and each next element is
the nearest left smaller value of the previous element:
›
fun der_stack where
"der_stack i = (if has_left i then the_left i # der_stack (the_left i) else [])"
declare der_stack.simps[simp del]
text ‹
Although the refinement framework would allow us to phrase the
algorithm without a stack first, and then introduce the stack in a subsequent
refinement step (or omit it altogether), for simplicity of presentation, we decided
to model the algorithm with a stack in first place. However, the invariant will account for
the stack being derived.
›
lemma set_der_stack_lt: "k ∈ set (der_stack i⇩0) ⟹ k<i⇩0"
apply (induction i⇩0 rule: der_stack.induct)
apply (subst (asm) der_stack.simps)
apply auto
using less_trans the_leftI by blast
subsection ‹Abstract Implementation›
text ‹We first implement the algorithm on lists.
The assertions that we annotated into the algorithm ensure
that all list index accesses are in bounds.
›
definition "pop stk v ≡ dropWhile (λj. xs!j≥v) stk"
lemma pop_Nil[simp]: "pop [] v = []" by (auto simp: pop_def)
lemma pop_cons: "pop (j#js) v = (if xs!j ≥ v then pop js v else j#js)"
by (simp add: pop_def)
definition "all_left ≡ doN {
(_,lf) ← nfoldli [0..<length xs] (λ_. True) (λi (stk,lf). doN {
ASSERT (set stk ⊆ {0..<length xs} );
let stk = pop stk (xs!i);
ASSERT (stk = der_stack i);
ASSERT (i<length lf);
if (stk = []) then doN {
let lf = lf[i:=None];
RETURN (i#stk,lf)
} else doN {
let lf = lf[i:= Some (hd stk)];
RETURN (i#stk,lf)
}
}) ([],replicate (length xs) None);
RETURN lf
}"
subsection ‹Correctness Proof›
subsubsection ‹Popping From the Stack›
text ‹We show that the abstract algorithm implements its specification.
The main idea here is the popping of the stack.
Top obtain a left smaller value, it is enough to follow the left-values of
the left-neighbour, until we have found the value or there are no more left-values.
The following theorem formalizes this idea:
›
theorem find_left_rl:
assumes "i⇩0 < length xs"
assumes "i<i⇩0"
assumes "left_spec i⇩0 ≤ Some i"
shows "if xs!i < xs!i⇩0 then left_spec i⇩0 = Some i
else left_spec i⇩0 ≤ left_spec i"
using assms
apply (simp; intro impI conjI; clarsimp)
subgoal
apply (auto simp: left_alt split: if_splits)
apply (simp add: le_antisym le_the_leftI)
apply (auto simp: has_left_def)
done
subgoal
apply (auto simp: left_alt split: if_splits)
subgoal
apply (drule the_leftI)
using nat_less_le by (auto simp: has_left_def)
subgoal
using le_the_leftI the_leftI by fastforce
done
done
text ‹Using this lemma, we can show that the stack popping procedure preserves the form of the stack.›
lemma pop_aux: "⟦ k<i⇩0; i⇩0<length xs; left_spec i⇩0 ≤ Some k ⟧ ⟹ pop (k # der_stack k) (xs!i⇩0) = der_stack i⇩0"
apply (induction k rule: nat_less_induct)
apply (clarsimp)
by (smt der_stack.simps left_alt pop_def the_leftI dropWhile.simps(1) find_left_rl leD less_option_None_Some option.inject pop_cons)
subsubsection ‹Main Algorithm›
text ‹Ad-Hoc lemmas›
lemma swap_adhoc[simp]:
"None = left i ⟷ left i = None"
"Some j = left i ⟷ left i = Some j" by auto
lemma left_spec_None_iff[simp]: "left_spec i = None ⟷ ¬has_left i" by (auto simp: left_alt)
lemma [simp]: "left_spec 0 = None" by (auto simp: left_spec_def)
lemma [simp]: "has_left 0 = False"
by (simp add: has_left_def)
lemma [simp]: "der_stack 0 = []"
by (subst der_stack.simps) auto
lemma algo_correct: "all_left ≤ SPEC all_left_spec"
unfolding all_left_def all_left_spec_def
apply (refine_vcg nfoldli_upt_rule[where I="
λk (stk,lf).
(length lf = length xs)
∧ (∀i<k. lf!i = left_spec i)
∧ (case k of Suc kk ⇒ stk = kk#der_stack kk | _ ⇒ stk=[])
"])
apply (vc_solve split: nat.splits)
subgoal using set_der_stack_lt by fastforce
subgoal for lf k
by (metis left_alt less_Suc_eq_le less_eq_option_None less_eq_option_Some nat_in_between_eq(2) pop_aux the_leftI)
subgoal
by (metis der_stack.simps left_alt less_Suc_eq list.distinct(1) nth_list_update)
subgoal
by (metis der_stack.simps left_alt less_Suc_eq list.sel(1) nth_list_update)
done
subsection ‹Implementation With Arrays›
text ‹We refine the algorithm to use actual arrays for the input and output.
The stack remains a list, as pushing and popping from a (functional) list is efficient.
›
subsubsection ‹Implementation of Pop›
text ‹In a first step, we refine the pop function to an explicit loop.›
definition "pop2 stk v ≡
monadic_WHILEIT
(λ_. set stk ⊆ {0..<length xs})
(λ[] ⇒ RETURN False | k#stk ⇒ doN { ASSERT (k<length xs); RETURN (v ≤ xs!k) })
(λstk. mop_list_tl stk)
stk"
lemma pop2_refine_aux: "set stk ⊆ {0..<length xs} ⟹ pop2 stk v ≤ RETURN (pop stk v)"
apply (induction stk)
unfolding pop_def pop2_def
subgoal
apply (subst monadic_WHILEIT_unfold)
by auto
subgoal
apply (subst monadic_WHILEIT_unfold)
unfolding mop_list_tl_def op_list_tl_def by auto
done
end
text ‹The refinement lemma written in higher-order form.›
lemma pop2_refine: "(uncurry2 pop2, uncurry2 (RETURN ooo pop)) ∈ [λ((xs,stk),v). set stk ⊆ {0..<length xs}]⇩f (Id ×⇩r Id) ×⇩r Id → ⟨Id⟩nres_rel"
using pop2_refine_aux
by (auto intro!: frefI nres_relI)
text ‹Next, we use the Sepref tool to synthesize an implementation on arrays.›
sepref_definition pop2_impl is "uncurry2 pop2" :: "(array_assn id_assn)⇧k *⇩a (list_assn id_assn)⇧k *⇩a id_assn⇧k →⇩a list_assn id_assn"
unfolding pop2_def
by sepref
lemmas [sepref_fr_rules] = pop2_impl.refine[FCOMP pop2_refine]
subsubsection ‹Implementation of Main Algorithm›
sepref_definition all_left_impl is all_left :: "(array_assn id_assn)⇧k →⇩a array_assn (option_assn id_assn)"
unfolding all_left_def
apply (rewrite at "nfoldli _ _ _ (⌑,_)" HOL_list.fold_custom_empty)
apply (rewrite in "nfoldli _ _ _ (_,⌑)" array_fold_custom_replicate)
by sepref
subsubsection ‹Correctness Theorem for Concrete Algorithm›
text ‹We compose the correctness theorem and the refinement theorem, to get a correctness
theorem for the final implementation.›
text ‹Abstract correctness theorem in higher-order form.›
lemma algo_correct': "(all_left, SPEC o all_left_spec)
∈ ⟨Id⟩list_rel → ⟨⟨⟨Id⟩option_rel⟩list_rel⟩nres_rel"
using algo_correct by (auto simp: nres_relI)
text ‹Main correctness theorem in higher-order form.›
theorem algo_impl_correct:
"(all_left_impl, SPEC o all_left_spec)
∈ (array_assn int_assn, array_assn int_assn) →⇩a array_assn (option_assn nat_assn)"
using all_left_impl.refine[FCOMP algo_correct', simplified] .
text ‹Main correctness theorem as Hoare-Triple›
theorem algo_impl_correct': "
<array_assn int_assn xs xsi>
all_left_impl xsi
<λlfi. ∃⇩Alf. array_assn int_assn xs xsi
* array_assn (option_assn id_assn) lf lfi
* ↑(all_left_spec xs lf)>⇩t"
apply (rule cons_rule[OF _ _ algo_impl_correct[to_hnr, THEN hn_refineD, unfolded autoref_tag_defs]])
apply (simp add: hn_ctxt_def, rule ent_refl)
by (auto simp: hn_ctxt_def)
subsection ‹Code Generation›
export_code all_left_impl checking SML Scala Haskell? OCaml?
text ‹The example from the problem description, in ML using the verified algorithm›
ML_val ‹
fun cnv NONE = 0
| cnv (SOME i) = @{code integer_of_nat} i + 1
fun all_left xs =
@{code all_left_impl} (Array.fromList (map @{code int_of_integer} xs)) ()
|> Array.foldr (op ::) []
|> map cnv
val test = all_left [ 4, 7, 8, 1, 2, 3, 9, 5, 6 ]
›
end