Theory Challenge2A

section ‹Challenge 2.A›
theory Challenge2A
imports "lib/VTcomp"

text ‹Problem definition:

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.
  "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 "ij" "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

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 i0)  k<i0"  
  apply (induction i0 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!jv) 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);

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 "i0 < length xs"
  assumes "i<i0"
  assumes "left_spec i0  Some i"
  shows "if xs!i < xs!i0 then left_spec i0 = Some i
         else left_spec i0  left_spec i"
  using assms           
  apply (simp; intro impI conjI; clarsimp)
    apply (auto simp: left_alt split: if_splits)
    apply (simp add: le_antisym le_the_leftI)
    apply (auto simp: has_left_def)
    apply (auto simp: left_alt split: if_splits)
      apply (drule the_leftI)
      using nat_less_le by (auto simp: has_left_def)
      using le_the_leftI the_leftI by fastforce

text ‹Using this lemma, we can show that the stack popping procedure preserves the form of the stack.›
lemma pop_aux: " k<i0; i0<length xs; left_spec i0  Some k   pop (k # der_stack k) (xs!i0) = der_stack i0"
  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)
    by (metis der_stack.simps left_alt less_Suc_eq list.distinct(1) nth_list_update)
    by (metis der_stack.simps left_alt less_Suc_eq list.sel(1) nth_list_update)

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  
    (λ_. set stk  {0..<length xs}) 
    (λ[]  RETURN False | k#stk  doN { ASSERT (k<length xs); RETURN (v  xs!k) })
    (λstk. mop_list_tl 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
    apply (subst monadic_WHILEIT_unfold)
    by auto
    apply (subst monadic_WHILEIT_unfold)
    unfolding mop_list_tl_def op_list_tl_def by auto
end ― ‹Context fixing the input xs›.›

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  Idnres_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_assnk 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) 
   Idlist_rel  Idoption_rellist_relnres_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 (* Convert from option to 1-based indexes *)
  fun cnv NONE = 0
    | cnv (SOME i) = @{code integer_of_nat} i + 1

  (* The verified algorithm, boxing the input list into an array, 
    and unboxing the output to a list, and converting it from option to 1-based *)
  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 ]