some isabelle/hol verificationHEADmain

doesn't do much, just proves that the find function won't cause an
error.

also removes all uses of rust traits, since these are currently broken
on the aeneas side.

1 files changed, 122 insertions, 0 deletions

diff --git a/Verification.thy b/Verification.thy
new file mode 100644
index 0000000..bdb1743
--- /dev/null
+++ b/Verification.thy
@@ -0,0 +1,122 @@
+theory Verification imports
+ Notraits
+begin
+
+
+fun height_of_node :: "AVLNode option \<Rightarrow> nat" where
+  "height_of_node None = 0"
+| "height_of_node (Some (mkAVLNode _ l r)) =
+     max (height_of_node l) (height_of_node r) + 1"
+
+  
+
+fun is_ok :: "'a result \<Rightarrow> bool" where
+  "is_ok (Ok _) = True"
+| "is_ok _ = False"
+
+
+lemma[simp]: "is_ok (cmp a b)"
+  by simp
+
+
+(* nicer induction rule for type AVLNode option *)
+lemma AVLNode_option_induct: 
+  assumes "\<And>v l r. (\<And>x. x \<in> set_option l \<Longrightarrow> P (Some x))
+  \<Longrightarrow> (\<And>x. x \<in> set_option r \<Longrightarrow> P (Some x))
+  \<Longrightarrow> P (Some (mkAVLNode v l r))"
+  and "P None"
+  shows "P AVLNodeOption"
+proof (cases AVLNodeOption)
+  case None
+  then show ?thesis using assms by simp
+next
+  case (Some a)
+  then show ?thesis 
+    apply (induction a arbitrary: AVLNodeOption)
+    using Some assms(1) by blast
+qed
+
+
+lemma right_is_smaller: "height_of_node r < height_of_node (Some (mkAVLNode v l r))"
+  by (cases l) auto
+  
+lemma left_is_smaller: "height_of_node l < height_of_node (Some (mkAVLNode v l r))"
+  by (cases r) auto
+  
+
+(* the loop in find always terminates (important for using \<open>obtain\<close> further down *)
+termination aVLTreeSet_find_loop
+proof (relation "measure (\<lambda>(v, t). height_of_node t)")
+  show "wf (measure (\<lambda>(v, t). height_of_node t))" by simp
+next
+  fix value1 current_tree and x2 :: "AVLNode"
+  assume "current_tree = Some x2"
+  then show "((value1, right x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)"
+  using right_is_smaller in_measure 
+  by (metis AVLNode.collapse case_prod_conv)
+next
+  fix value1 current_tree and x2 :: "AVLNode"
+  assume "current_tree = Some x2"
+  then show "((value1, left x2), value1, current_tree) \<in> measure (\<lambda>(v, t). height_of_node t)"
+  using left_is_smaller in_measure 
+  by (metis AVLNode.collapse case_prod_conv)
+qed
+
+
+value "cmp (u32 1) (u32 1)"
+
+value "left (mkAVLNode (u32 0) None (Some (mkAVLNode (u32 0) None None)))"
+
+lemma find_loop_ok: "is_ok (aVLTreeSet_find_loop v n)"
+proof (induction n arbitrary: v rule: AVLNode_option_induct)
+  case (1 u l r)
+  obtain ordering where order: "Ok ordering = cmp u v"
+    by force
+  then show ?case 
+  proof (cases ordering)
+    case Ordering_Less
+    hence "is_ok (aVLTreeSet_find_loop v r)" 
+      using 1 by (simp add: option.split_sel_asm)
+    then obtain b r' where a: "Ok (b, r') = aVLTreeSet_find_loop v r"
+       by (auto elim: is_ok.elims)
+    hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) =
+               Ok (b, Some (mkAVLNode u l r'))"
+      using Ordering_Less order apply simp
+      by (smt (verit) AVLNode.expand AVLNode.record_simps(12) AVLNode.record_simps(13) AVLNode.record_simps(14) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4))
+    then show ?thesis by simp
+  next
+    case Ordering_Equal
+    hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) = Ok (True, Some (mkAVLNode u l r))"
+      using 1 order by simp
+    then show ?thesis by simp
+  next
+    case Ordering_Greater
+    hence "is_ok (aVLTreeSet_find_loop v l)" 
+      using 1 by (simp add: option.split_sel_asm)
+    then obtain b l' where a: "Ok (b, l') = aVLTreeSet_find_loop v l"
+       by (auto elim: is_ok.elims)
+    hence "aVLTreeSet_find_loop v (Some (mkAVLNode u l r)) =
+               Ok (b, Some (mkAVLNode u l' r))"
+      using Ordering_Greater order apply simp
+      by (smt (verit, ccfv_threshold) AVLNode.expand AVLNode.record_simps(6) AVLNode.record_simps(7) AVLNode.record_simps(8) AVLNode.sel(1) AVLNode.sel(2) AVLNode.sel(3) case_prod_conv result.simps(4))
+    then show ?thesis by simp
+  qed
+next
+  case 2
+  then show ?case by simp
+qed
+
+(* find never produces an error *)
+lemma find_ok: "\<exists>res. aVLTreeSet_find t v = Ok res"
+proof -
+  obtain b as where "Ok (b, as) = aVLTreeSet_find_loop v (root t)"
+    using find_loop_ok by (metis is_ok.elims(2) old.prod.exhaust)
+  then have "aVLTreeSet_find t v = Ok (b, \<lparr> root = as \<rparr>)" 
+    apply simp unfolding bind_def
+    by (metis old.prod.case result.simps(4))
+  thus ?thesis 
+    by simp
+qed
+
+
+end
\ No newline at end of file