theory a3
imports 
  AutoCorres
begin


(*---------------------------------------------------------*)
(*---------------------------------------------------------*)
section \<open> Induction (25 marks) \<close>

fun
  mystery_f :: "nat \<Rightarrow> string \<Rightarrow> string"
where
    "mystery_f 0 _ = []"
  | "mystery_f (Suc 0) a = a"
  | "mystery_f k a =
      (if k mod 2 = 0 then mystery_f (k div 2) (a @ a)
      else mystery_f (k div 2) (a @ a) @ a)"

(* (a) Explain in one sentence or two what this function is doing.
       Justify your answer with a few representative examples. *)

(*TODO*)

(* (b) Prove the following properties: *)

lemma "(mystery_f n []) = TODO" (*you may reformulate the lemma slightly*)
  (*TODO*)
  sorry

lemma length_mystery_f :
  "length (mystery_f n s) = TODO"
  (*TODO*)
  sorry

lemma "mystery_f (n+m) s = TODO"
  (*TODO*)
  sorry

(*---*)

definition
  mystery_g :: "string \<Rightarrow> nat \<Rightarrow> string \<Rightarrow> string option"
where
  "mystery_g c k s =
  (if size c \<noteq> 1 \<or> size s > k
   then None
   else Some (mystery_f (k - size s) c @ s))"

(* (c) Explain in one sentence or two what this function is doing.
       Justify your answer with a few representative examples.
       Try for instance @{term "mystery_g ''0'' 8 ''101''"}.*)

(*TODO*)

(* (d) Prove the following lemma: *)

lemma mystery_g_length:
  "mystery_g c k s = Some xs \<Longrightarrow> length xs = k"
  (*TODO*)
  sorry


(* (e) Prove the following lemma: *)

lemma mystery_g_suffix:
  "mystery_g [c] k s = Some xs \<Longrightarrow> \<exists>zs. xs = zs @ s \<and> (k=length s \<or> set zs = {c})"
  (*TODO*)
  sorry
  


(*---------------------------------------------------------*)
(*---------------------------------------------------------*)

section \<open> C verification: doubly-linked list (40 marks) \<close>

(* Installing the C file and converting it using the AutoCorress tool *)

install_C_file "dlist.c"

autocorres [unsigned_word_abs=f, ts_force nondet=f] "dlist.c"

term "is_valid_node_C p"


(* Definition of *path*: (path vld hp nxt p l q) says that you start 
   from pointer p, and "follow" the function nxt, adding each encountered 
   pointer to the list l, until you reach the pointer q, and that 
   all encountered pointers are valid nodes according to the predicate vld, 
   are not NULL, and not q:

      l=[ p ,  p1 , p2 , q    ]
          \<down>    \<down>    \<down>    \<down>
          []\<longrightarrow>[]\<longrightarrow>[]\<longrightarrow>[]
            nxt  nxt  nxt 
*)
  
primrec
  path :: "(node_C ptr \<Rightarrow> bool) \<Rightarrow>    (* valid predicate *)
              (node_C ptr \<Rightarrow> node_C) \<Rightarrow>  (* the heap *)
              (node_C \<Rightarrow> node_C ptr) \<Rightarrow>  (* the function that maps to next element, 
                                            i.e. the field of the node *)
               node_C ptr \<Rightarrow>             (* the starting pointer *)
               node_C ptr list \<Rightarrow>        (* the list of traversed pointers *)
               node_C ptr \<Rightarrow>             (* the end pointer *)
               bool"
where
  "path vld hp nxt p [] q = (p = q)"
| "path vld hp nxt p (x#xs) q = (p \<noteq> q \<and> vld p \<and> p \<noteq> NULL \<and> p=x \<and> 
                                path vld hp nxt (nxt (hp p)) xs q)"


(* Definition of *is_dlist*: (is_dlist vld hp p q xs) is True if we 
   have a valid doubly-linked list starting from p and ending in q:
        xs=[ p , p1, p2, q ]
             \<down>   \<down>   \<down>   \<down>
       NULL\<leftarrow>[]\<rightleftharpoons>[]\<rightleftharpoons>[]\<rightleftharpoons>[]\<rightarrow> NULL
*)   


definition
  "is_dlist vld hp p xs q \<equiv> 
  path vld hp next_C p xs NULL \<and> path vld hp prev_C q (rev xs) NULL"

(* (a) Start proof of insert_after_inserts *)

(* TODO: start the proof in question (d) below, just to give you 
   a feeling of what the goal looks like and why we need
   all the helper lemmas *)


(* (b) Prove path_upd *)

lemma path_upd:
  "x \<notin> set xs \<Longrightarrow> path vld (hp (x := y)) n p xs q = path vld hp n p xs q"
  (*TODO*)
  sorry

(* (c) Prove path_in, path_unique, path_appendD, path_hd_not_in_tl,
       path_append_last *)

lemma path_in:
  "\<lbrakk>path vld hp n p xs q; xs \<noteq> []\<rbrakk> \<Longrightarrow> p \<in> set xs"
  (*TODO*)
  sorry

lemma path_unique:
  "\<lbrakk> path vld hp n p xs q; path vld hp n p ys q \<rbrakk> \<Longrightarrow> xs = ys"
  (*TODO*)
  sorry

lemma path_appendD:
  "path vld hp n p (xs@ys) q \<Longrightarrow> 
   \<exists>r. path vld hp n p xs r \<and>  path vld hp n r ys q"
  (*TODO*)
  sorry

lemma path_hd_not_in_tl:
  "path vld hp n (n (hp p)) xs q \<Longrightarrow> p \<notin> set xs"
  (*TODO*)
  sorry

lemma path_append_last:
  "path vld hp n p (xs@ys) q = 
  (path vld hp n p xs (if ys = [] then q else hd ys) \<and> 
   path vld hp n (if ys = [] then q else hd ys) ys q \<and> set xs \<inter> set ys = {} \<and> q \<notin> set xs)"
  (*TODO*)
  sorry



(* (d) Finish proof of correctness insert_after_inserts *)

definition insert_pre
where
  "insert_pre p xs q nd s= 
    (xs\<noteq>[] \<and> is_dlist (is_valid_node_C s) (heap_node_C s) p xs q \<and>  
    nd \<noteq> NULL \<and> is_valid_node_C s nd \<and>  nd \<notin> set xs )"

definition insert_post
where
  "insert_post p xs nd s= 
    is_dlist (is_valid_node_C s) (heap_node_C s) p (xs @ [nd]) nd "

context dlist
begin

lemma insert_after_inserts:
  "\<lbrace>\<lambda> s. insert_pre p xs q nd s\<rbrace>
     insert_after' nd q
   \<lbrace>\<lambda>_ s. insert_post p xs nd  s\<rbrace>"
  (* TODO *)
  sorry

end 

(*---------------------------------------------------------*)
(*---------------------------------------------------------*)

section \<open> C verification: invariant (35 marks) \<close>

(* (a) What is the invariant for the loop? Trace a few example computations in your 
  favourite programming language to discover the relationship between the variables. *)

(*TODO*)

(* (b) What is a variant for the loop that guarantees that the loop terminates? *)

(*TODO*)

(* (c) State the property as a (total correctness) Hoare triple  and prove it.*)

context dlist begin

lemma f_correct:
  "\<lbrace>\<lambda>_. a \<le> SQ_MAX \<rbrace>
     f' a
   \<lbrace>\<lambda>r _. (0 < a \<longrightarrow> (r - 1) * (r - 1) < a \<and> a \<le> r*r) \<and>
          (a = 0 \<longrightarrow> r = 0) \<rbrace>!"
  apply (unfold f'_def)
  apply (subst whileLoop_add_inv [where
    I = "\<lambda>(k, m, n) _. TODO" and   (* the invariant*) 
    M = "\<lambda>((k, m, n), _). TODO"]) (*the variant *)
  (*TODO: finish proof*)
  sorry

end


end