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, 114 insertions, 0 deletions

diff --git a/Notraits.thy b/Notraits.thy
new file mode 100644
index 0000000..fd459f7
--- /dev/null
+++ b/Notraits.thy
@@ -0,0 +1,114 @@
+(** THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS *)
+(** [avl_verification] *)
+theory "Notraits" imports
+  "Aeneas.Primitives"
+  "HOL-Library.Datatype_Records"
+begin
+
+
+(*[avl_verification::Ordering]
+   Source: 'src/main.rs', lines 1:0-1:17*)
+datatype Ordering = Ordering_Less | Ordering_Equal | Ordering_Greater
+
+
+(*[avl_verification::AVLNode]
+   Source: 'src/main.rs', lines 10:0-10:14*)
+datatype AVLNode = mkAVLNode
+  (val: "u32") (left: "AVLNode option") (right: "AVLNode option")
+local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>AVLNode\<close>\<close>
+
+(*[avl_verification::AVLTreeSet]
+   Source: 'src/main.rs', lines 18:0-18:17*)
+datatype AVLTreeSet = mkAVLTreeSet (root: "AVLNode option")
+local_setup \<open>Datatype_Records.mk_update_defs \<^type_name>\<open>AVLTreeSet\<close>\<close>
+
+(*[avl_verification::{avl_verification::AVLTreeSet}::new]:
+   Source: 'src/main.rs', lines 23:4-23:24*)
+definition aVLTreeSet_new :: "AVLTreeSet result" where
+  "aVLTreeSet_new = Ok (\<lparr> root = None \<rparr>)"
+
+(*[avl_verification::cmp]:
+   Source: 'src/main.rs', lines 61:0-61:40*)
+fun cmp :: "u32 \<Rightarrow> u32 \<Rightarrow> Ordering result" where
+  "cmp a other =
+    (if u32_lt a other
+    then Ok Ordering_Less
+    else (if a = other then Ok Ordering_Equal else Ok Ordering_Greater))"
+
+(*[avl_verification::{avl_verification::AVLTreeSet}::find]: loop 0:
+   Source: 'src/main.rs', lines 27:4-39:5*)
+function aVLTreeSet_find_loop
+  :: "u32 \<Rightarrow> AVLNode option \<Rightarrow> (bool * AVLNode option) result" where
+  "aVLTreeSet_find_loop value1 current_tree =
+    (case current_tree of
+      None \<Rightarrow> Ok (False, None)
+    | Some current_node \<Rightarrow>
+      do {
+        o1 \<leftarrow> cmp (val current_node) value1;
+        (case o1 of
+          Ordering_Less \<Rightarrow>
+          do {
+            (b, current_tree1) \<leftarrow>
+              aVLTreeSet_find_loop value1 (right current_node);
+            Ok (b, Some
+              (current_node \<lparr> right := current_tree1 \<rparr>))
+            }
+        | Ordering_Equal \<Rightarrow> Ok (True, Some current_node)
+        | Ordering_Greater \<Rightarrow>
+          do {
+            (b, current_tree1) \<leftarrow>
+              aVLTreeSet_find_loop value1 (left current_node);
+            Ok (b, Some (current_node \<lparr> left := current_tree1 \<rparr>))
+            })
+        })"  by auto
+
+(*[avl_verification::{avl_verification::AVLTreeSet}::find]:
+   Source: 'src/main.rs', lines 27:4-27:46*)
+fun aVLTreeSet_find
+  :: "AVLTreeSet \<Rightarrow> u32 \<Rightarrow> (bool * AVLTreeSet) result" where
+  "aVLTreeSet_find self value1 =
+    do {
+      (b, as) \<leftarrow> aVLTreeSet_find_loop value1 (root self);
+      Ok (b, (\<lparr> root = as \<rparr>))
+      }"
+
+(*[avl_verification::{avl_verification::AVLTreeSet}::insert]: loop 0:
+   Source: 'src/main.rs', lines 40:4-58:5*)
+function aVLTreeSet_insert_loop
+  :: "u32 \<Rightarrow> AVLNode option \<Rightarrow> (bool * AVLNode option) result" where
+  "aVLTreeSet_insert_loop value1 current_tree =
+    (case current_tree of
+      None \<Rightarrow>
+      let a = (\<lparr> val = value1, left = None, right = None \<rparr>) in
+        Ok (True, Some a)
+    | Some current_node \<Rightarrow>
+      do {
+        o1 \<leftarrow> cmp (val current_node) value1;
+        (case o1 of
+          Ordering_Less \<Rightarrow>
+          do {
+            (b, current_tree1) \<leftarrow>
+              aVLTreeSet_insert_loop value1 (right current_node);
+            Ok (b, Some
+              (current_node \<lparr> right := current_tree1 \<rparr>))
+            }
+        | Ordering_Equal \<Rightarrow> Ok (False, Some current_node)
+        | Ordering_Greater \<Rightarrow>
+          do {
+            (b, current_tree1) \<leftarrow>
+              aVLTreeSet_insert_loop value1 (left current_node);
+            Ok (b, Some (current_node \<lparr> left := current_tree1 \<rparr>))
+            })
+        })"  by auto
+
+(*[avl_verification::{avl_verification::AVLTreeSet}::insert]:
+   Source: 'src/main.rs', lines 40:4-40:48*)
+fun aVLTreeSet_insert
+  :: "AVLTreeSet \<Rightarrow> u32 \<Rightarrow> (bool * AVLTreeSet) result" where
+  "aVLTreeSet_insert self value1 =
+    do {
+      (b, as) \<leftarrow> aVLTreeSet_insert_loop value1 (root self);
+      Ok (b, (\<lparr> root = as \<rparr>))
+      }"
+
+end
\ No newline at end of file