theory a3
imports 
  AutoCorres.AutoCorres "HOL-Number_Theory.Number_Theory"
begin

(* To run this file you need the AutoCorres tool used
   in the lecture.

  1. Download AutoCorres from 
       \url{http://www.cse.unsw.edu.au/~cs4161/autocorres-1.7.tar}

  2. Unpack the .tar.gz file, which will create the directory autocorres-1.7
       tar -xzf autocorres-1.7.tar.gz

  3. Build the AutoCorres heap
     L4V_ARCH=X64 isabelle build -v -b -d autocorres-1.7 AutoCorres

  4. Load this file using the AutoCorres heap
     L4V_ARCH=X64 isabelle jedit -d autocorres-1.7 -l AutoCorres a3.thy

*)

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

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=is_prime_2, ts_force nondet=is_prime_2] "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>    \<comment>\<open> valid predicate \<close>
              (node_C ptr \<Rightarrow> node_C) \<Rightarrow>  \<comment>\<open> the heap \<close>
              (node_C \<Rightarrow> node_C ptr) \<Rightarrow>  \<comment>\<open> the function that maps to next element, 
                                            i.e. the field of the node \<close>
               node_C ptr \<Rightarrow>             \<comment>\<open> the starting pointer \<close>
               node_C ptr list \<Rightarrow>        \<comment>\<open> the list of traversed pointers \<close>
               node_C ptr \<Rightarrow>             \<comment>\<open> the end pointer \<close>
               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 "Primality modulo 2"

context dlist begin

thm is_prime_2'_def

(* Q2 a): Loop invariant for "is_prime_2". *)
definition
  is_prime_inv :: "nat \<Rightarrow> nat \<Rightarrow> bool"
where
  "is_prime_inv i n \<equiv>	undefined" (*TODO*)


(* Q2 b): Measure function for "is_prime_2". Must be strictly decreasing
 * for each loop iteration. *)
definition
  is_prime_measure :: "nat \<Rightarrow> nat \<Rightarrow> nat"
where
  "is_prime_measure i n \<equiv> undefined" (*TODO*)


(* Q2 c1): A prime is either 2 or an odd number *)
lemma prime_2_or_odd: "prime n \<Longrightarrow> n = 2 \<or> n mod 2 = Suc 0"
  sorry (* TODO *)


(* Q2 c2): The loop invariant holds coming into the loop. *)
lemma is_prime_precond_implies_inv: 
  "True"
  sorry (*TODO*)


(* Q2 c3): The loop invariant holds for each loop iteration. *)
lemma is_prime_body_obeys_inv:
  "True"
  sorry (*TODO*)


(* Q2 c4): The loop measure decrements each loop iteration. *)
lemma is_prime_body_obeys_measure:
  "\<lbrakk> is_prime_inv i n; n mod i \<noteq> 0 \<rbrakk>
      \<Longrightarrow> is_prime_measure i n > is_prime_measure (i + 2) n"
  sorry (*TODO*)


(* Q2 c5): The loop invariant implies there is no overflow. *)
lemma is_prime_body_implies_no_overflow:
  "\<lbrakk> is_prime_inv i n; n mod i \<noteq> 0\<rbrakk> \<Longrightarrow> i + 2 \<le> UINT_MAX"
  sorry


(* Q2 c6): The loop invariant implies the post-condition. *)
lemma is_prime_inv_implies_postcondition:
  "True"
  sorry (*TODO*)


(*
 * Q2 d): Show that "is_prime' n" is correct.
 *
 * AutoCorres has applied "word abstraction" to this function,
 * meaning that you are able to reason using "nats" instead of
 * "word32" data types, at the price of having to reason that
 * your values don't overflow UINT_MAX.
 *)
lemma is_prime_correct:
  "\<lbrace>\<lambda>s. n \<le> UINT_MAX \<rbrace> is_prime_2' n \<lbrace>\<lambda>r s. r = (if prime n then 1 else 0) \<rbrace>!"
  (* Unfold the program body. *)
  apply (unfold is_prime_2'_def)
  (* Annotate the loop with an invariant and measure. *)
  apply (subst whileLoop_add_inv [where
     I="\<lambda>i s. is_prime_inv i n" and
     M="\<lambda>(i, s). is_prime_measure i n" ])

  (*
   * Run "wp" to generate verification conditions.
   *
   * The resulting subgoals are:
   *    1. The loop body obeys the invariant, causes the measure to decrease, and
            does not lead to overflow;
   *    2. The invariant implies the post-condition of the function; and
   *    3. The pre-condition of the function implies the invariant.
   *
   *)
  apply wp
  sorry (*TODO*)

end



end