Theory CList

(* SPDX-License-Identifier: BSD-3-Clause *)
(*
 * Copyright (C) 2002 Tobias Nipkow (TUM)
 * Copyright (C) 2013--2014 Japheth Lim (NICTA)
 * Copyright (C) 2013--2014 David Greenaway (NICTA)
 * Copyright (c) 2022 Apple Inc. All rights reserved.
 *
 * Redistribution and use in source and binary forms, with or without
 * modification, are permitted provided that the following conditions are
 * met:
 *
 * * Redistributions of source code must retain the above copyright
 * notice, this list of conditions and the following disclaimer.
 *
 * * Redistributions in binary form must reproduce the above copyright
 * notice, this list of conditions and the following disclaimer in the
 * documentation and/or other materials provided with the distribution.
 *
 * * Neither the name of the University of Cambridge or the Technische
 * Universitaet Muenchen nor the names of their contributors may be used
 * to endorse or promote products derived from this software without
 * specific prior written permission.
 *
 * THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS
 * IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED
 * TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A
 * PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
 * OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
 * SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
 * LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
 * DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
 * THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
 * (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
 * OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
 *)

theory CList imports
  "AutoCorres2_Main.AutoCorres_Main"
begin

install_C_file "list.c"

declare [[ML_print_depth=1000]]
declare [[verbose=0]]



autocorres [single_threaded] "list.c"


context list_all_impl begin

thm insert'_def
thm sorted_insert'_def
thm reverse'_def
thm revappend'_def

section "The heap"

subsection "Paths in the heap"

definition node_next where "node_next s p = next_C (heap_node_C s p)"
definition node_exists where "node_exists s (p:: node_C ptr) = (p ≠ NULL ∧ ptr_valid (heap_typing s) p)"

definition node_next_upd where
  "node_next_upd s p q = heap_node_C_update (λold. old(p := next_C_update (λ_. q) (old p))) s"

lemma "p ≠ x ⟹ heap_node_C (node_next_upd s x q) p = heap_node_C s p"
by (simp add: node_next_def node_next_upd_def fun_upd_apply)
lemma [simp]: "node_next (node_next_upd s p q) p = q"
by (simp add: node_next_def node_next_upd_def fun_upd_apply)
lemma [simp]: "p ≠ x ⟹ node_next (node_next_upd s x q) p = node_next s p"
by (simp add: node_next_def node_next_upd_def fun_upd_apply)
lemma "node_next_upd (node_next_upd s p a) p b = node_next_upd s p b"
  by (simp add: node_next_def node_next_upd_def fun_upd_apply comp_def)
lemma [simp]: "node_exists (node_next_upd s q x) p = node_exists s p"
by (simp add: node_exists_def node_next_upd_def fun_upd_apply)
lemma "p ≠ q ⟹ node_next (node_next_upd s q x) p = node_next s p"
by (simp add: node_next_def node_next_upd_def fun_upd_apply)

primrec Path :: "lifted_globals ⇒ node_C ptr ⇒ node_C ptr list ⇒ node_C ptr ⇒ bool" where
  "Path s x [] y ⟷ x = y"
| "Path s x (a#as) y ⟷ node_exists s x ∧ x = a ∧ Path s (node_next s x) as y"

lemma [iff]: "Path s NULL xs y = (xs = [] ∧ y = NULL)"
by (case_tac xs, fastforce, fastforce simp: node_exists_def)

lemma [simp]: "node_exists s a ⟹ Path s a as z =
  (as = [] ∧ a = z   ∨   (∃bs. as = a # bs ∧ Path s (node_next s a) bs z))"
by (case_tac as, fastforce, fastforce simp: node_exists_def)

lemma [simp]: "⋀x. Path s x (as@bs) z =
(∃y. Path s x as y ∧ Path s y bs z)"
by (induct as, simp+)

lemma Path_upd[simp]:
"⋀x. u ∉ set as ⟹
Path (node_next_upd s u v) x as y = Path s x as y"
apply (induct as, simp)
apply (simp add: node_exists_def node_next_def node_next_upd_def fun_upd_apply)
done

lemma Path_snoc:
"⟦ node_exists s a; Path (node_next_upd s a q) p as a ⟧ ⟹ Path (node_next_upd s a q) p (as @ [a]) q"
by simp


subsection "Non-repeating paths"

definition distPath ::
  "lifted_globals ⇒ node_C ptr ⇒ node_C ptr list ⇒ node_C ptr ⇒ bool"
  where "distPath s x as y ⟷ Path s x as y ∧ distinct as"

text‹The term @{term "distPath s x as y"} expresses the fact that a
non-repeating path @{term as} connects location @{term x} to location
@{term y} over the heap @{term s}. In the case where @{text "x = y"},
and there is a cycle from @{term x} to itself, @{term as} can
be both @{term "[]"} and the non-repeating list of nodes in the
cycle.›

lemma neq_dP: "p ≠ q ⟹ Path s p Ps q ⟹ distinct Ps ⟹
 ∃ a Qs. p = a & Ps = a#Qs & a ∉ set Qs"
by (case_tac Ps, auto)


lemma neq_dP_disp: "⟦ p ≠ q; distPath s p Ps q ⟧ ⟹
 ∃ a Qs. p = a ∧ Ps = a#Qs ∧ a ∉ set Qs"
apply (simp only:distPath_def)
by (case_tac Ps, auto)


subsection "Lists on the heap"

subsubsection "Relational abstraction"

definition List :: "lifted_globals ⇒ node_C ptr ⇒ node_C ptr list ⇒ bool"
  where "List s x as = Path s x as NULL"

lemma [simp]: "List s x [] = (x = NULL)"
by(simp add:List_def)

lemma List_case [simp]: "List s x (a#as) = (x = a ∧ node_exists s a ∧ List s (node_next s a) as)"
by(auto simp:List_def)

lemma [simp]: "List s NULL as = (as = [])"
by(case_tac as, simp_all add: node_exists_def)

lemma List_Ref[simp]: "node_exists s a ⟹ List s a as = (∃bs. as = a#bs ∧ List s (node_next s a) bs)"
by(case_tac as, simp_all add: node_exists_def, fast)

theorem notin_List_update[simp]:
 "⋀x. ⟦ node_exists s a; a ∉ set as ⟧ ⟹ List (node_next_upd s a y) x as = List s x as"
apply(induct as)
apply simp
apply(clarsimp simp add:fun_upd_apply)
done

lemma List_unique: "⋀x bs. List s x as ⟹ List s x bs ⟹ as = bs"
by(induct as, simp, clarsimp)

lemma List_unique1: "List s p as ⟹ ∃!as. List s p as"
by(blast intro:List_unique)

lemma List_app: "⋀x. List s x (as@bs) = (∃y. Path s x as y ∧ List s y bs)"
by(induct as, simp, auto)

lemma List_hd_not_in_tl[simp]: "List s (node_next s a) as ⟹ a ∉ set as"
apply(clarsimp simp add:in_set_conv_decomp)
apply(frule List_app[THEN iffD1])
apply(fastforce dest: List_unique)
done

lemma List_distinct[simp]: "⋀x. List s x as ⟹ distinct as"
apply(induct as, simp)
apply(fastforce dest:List_hd_not_in_tl)
done

lemma Path_is_List:
  "⟦node_exists s a; Path s b Ps a; a ∉ set Ps⟧ ⟹ List (node_next_upd s a NULL) b (Ps @ [a])"
apply (induct Ps arbitrary: b)
apply (auto simp: node_exists_def node_next_upd_def node_next_def fun_upd_apply)
done



subsection "Functional abstraction"

definition islist :: "lifted_globals ⇒ node_C ptr ⇒ bool"
  where "islist s p ⟷ (∃as. List s p as)"

definition list :: "lifted_globals ⇒ node_C ptr ⇒ node_C ptr list"
  where "list s p = (SOME as. List s p as)"

lemma List_conv_islist_list: "List s p as = (islist s p ∧ as = list s p)"
apply(simp add:islist_def list_def)
apply(rule iffI)
apply(rule conjI)
apply blast
apply(subst some1_equality)
  apply(erule List_unique1)
 apply assumption
apply(rule refl)
apply simp
apply(rule someI_ex)
apply fast
done

lemma [simp]: "islist s NULL"
by(simp add:islist_def)

lemma [simp]: "node_exists s a ⟹ islist s a = islist s (node_next s a)"
by(simp add:islist_def)

lemma [simp]: "⟦ node_exists s a; islist s a ⟧ ⟹ islist s (node_next s a)"
apply (clarsimp simp: islist_def)
done

lemma [simp]: "list s NULL = []"
by(simp add:list_def)

lemma list_Ref_conv[simp]:
 "⟦ node_exists s a; islist s (node_next s a) ⟧ ⟹ list s a = a # list s (node_next s a)"
apply(insert List_Ref[of s])
apply(metis List_conv_islist_list)
done

lemma [simp]: "⟦ node_exists s a; islist s (node_next s a) ⟧ ⟹ a ∉ set(list s (node_next s a))"
apply(insert List_hd_not_in_tl[of s])
apply(metis List_conv_islist_list)
done

lemma list_upd_conv[simp]:
 "islist s p ⟹ y ∉ set(list s p) ⟹ list (node_next_upd s y q) p = list s p"
  apply (clarsimp simp: islist_def node_next_upd_def)
  by (metis (mono_tags) List_def List_unique Path_upd list_def node_next_upd_def some_eq_ex)

lemma islist_upd[simp]:
 "islist s p ⟹ y ∉ set(list s p) ⟹ islist (node_next_upd s y q) p"
  apply (clarsimp simp: islist_def node_next_upd_def)
  by (metis (mono_tags) List_def List_unique Path_upd list_def node_next_upd_def some_eq_ex)


subsection "List reversal"

subsubsection "Program representation"
text ‹This is AutoCorres's representation of revappend.›
thm revappend'_def

text ‹The heap operations are a bit too low level,
        so let's lift them using our heap accessors.›
schematic_goal revappend'_abstract: "revappend' p q = ?new_definition"
  apply (subst revappend'_def)
  unfolding node_next_def[symmetric]
            node_next_upd_def[symmetric]
            modify_def
  apply (rule refl)
  done


text ‹node_exists is a prerequisite for most of our abstraction rules.
        But we cannot extract this prerequisite from the program text because it is
        implied by our Hoare preconditions (below) which are not a part of the program
        text. Here we arrange for Isabelle's tactics to infer it when needed.›


lemma node_exists_imp_valid[simp]: "node_exists s b ⟹ ptr_valid (heap_typing s) b"
  by (simp add: node_exists_def)

lemma List_node_exists [dest!]: "⟦ p ≠ NULL; List s p as ⟧ ⟹ node_exists s p"
by (case_tac as, auto simp: node_exists_def)

lemma islist_node_exists [simp]: "⟦ p ≠ NULL; islist s p ⟧ ⟹ node_exists s p"
  apply (clarsimp simp: islist_def)
  apply (rename_tac a, case_tac a, simp_all add: node_exists_def)
  done

subsubsection "Verification with relational abstraction"
text ‹Almost automatic proof using the relational abstraction.
        (The termination proof uses functional abstraction.)›

lemmas runs_to_whileLoop2 =  runs_to_whileLoop_res' [split_tuple C and B arity: 2]

lemma
"List s p Ps ⟹ List s q Qs ⟹ set Ps ∩ set Qs = {} ⟹
   revappend' p q ∙ s
 ⦃ λv s. ∃r. v = Result r ∧ List s r (rev Ps @ Qs) ⦄"
  txt ‹We verify the abstracted version of the program.›
  unfolding revappend'_abstract
  apply (runs_to_vcg)
  txt ‹Add the loop invariant and measure.›
  apply (rule runs_to_whileLoop2
    [where I = "λ(dest', list') s.
                 ∃ps qs. List s list' ps ∧ List s dest' qs ∧ set ps ∩ set qs = {} ∧
                         rev ps @ qs = rev Ps @ Qs"
       and R = " measure (λ((_, list'), s). length (list s list'))"])
  subgoal by simp (* measure wf *)
  subgoal by auto (* Precondition implies I *)
  subgoal by auto (* Invariant implies postcondition *)
  subgoal (* body *)
    apply runs_to_vcg
    subgoal (* guards *)  
      by auto 
    subgoal (* Loop invariant *) 
      by (fastforce intro: notin_List_update[THEN iffD2])
    subgoal (* Loop measure *) 
      by (fastforce simp: List_conv_islist_list)
    done
  done


subsubsection "Verification with functional abstraction"
text ‹Fully automatic proof using the functional abstraction.›
lemma
"islist s p ⟹ islist s q ⟹ Ps = list s p ⟹ Qs = list s q ⟹ set Ps ∩ set Qs = {} ⟹
   revappend' p q ∙ s
 ⦃ λv s. ∃r. v = Result r ∧ islist s r ∧ list s r = rev Ps @ Qs ⦄"
  unfolding revappend'_abstract
  apply (runs_to_vcg)

  apply (rule runs_to_whileLoop2
    [where I = "λ(q, p) s. islist s p ∧ islist s q ∧
                           set(list s p) ∩ set(list s q) = {} ∧
                           rev(list s p) @ (list s q) = rev Ps @ Qs"
       and R = "measure (λ((q, p), s). length (list s p))"])
  subgoal by simp (* measure wf *)
  subgoal by auto (* Precondition implies I *)
  subgoal by auto (* Invariant implies postcondition *)
  subgoal (* body *)
    apply runs_to_vcg
         apply auto
    done
  done

end (* context list_global_addresses *)

end