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.

7 files changed, 341 insertions, 24 deletions

diff --git a/.gitignore b/.gitignore
index e77655a..a2e9049 100644
--- a/.gitignore
+++ b/.gitignore
@@ -4,3 +4,5 @@
 /lake-packages/*
 .lake
 *.llbc
+/output
+*.thy~
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
diff --git a/ROOT b/ROOT
new file mode 100644
index 0000000..18d302f
--- /dev/null
+++ b/ROOT
@@ -0,0 +1,7 @@
+session "avl-verification" = "Aeneas" +
+  options [document = pdf, document_output = "output"]
+  theories
+    Notraits
+    Verification
+  document_files
+    "root.tex"
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
diff --git a/document/root.tex b/document/root.tex
new file mode 100644
index 0000000..1924cf3
--- /dev/null
+++ b/document/root.tex
@@ -0,0 +1,60 @@
+\documentclass[11pt,a4paper]{article}
+\usepackage[T1]{fontenc}
+\usepackage{isabelle,isabellesym}
+
+% further packages required for unusual symbols (see also
+% isabellesym.sty), use only when needed
+
+%\usepackage{amssymb}
+  %for \<leadsto>, \<box>, \<diamond>, \<sqsupset>, \<mho>, \<Join>,
+  %\<lhd>, \<lesssim>, \<greatersim>, \<lessapprox>, \<greaterapprox>,
+  %\<triangleq>, \<yen>, \<lozenge>
+
+%\usepackage{eurosym}
+  %for \<euro>
+
+%\usepackage[only,bigsqcap,bigparallel,fatsemi,interleave,sslash]{stmaryrd}
+  %for \<Sqinter>, \<Parallel>, \<Zsemi>, \<Parallel>, \<sslash>
+
+%\usepackage{eufrak}
+  %for \<AA> ... \<ZZ>, \<aa> ... \<zz> (also included in amssymb)
+
+%\usepackage{textcomp}
+  %for \<onequarter>, \<onehalf>, \<threequarters>, \<degree>, \<cent>,
+  %\<currency>
+
+% this should be the last package used
+\usepackage{pdfsetup}
+
+% urls in roman style, theory text in math-similar italics
+\urlstyle{rm}
+\isabellestyle{it}
+
+% for uniform font size
+%\renewcommand{\isastyle}{\isastyleminor}
+
+
+\begin{document}
+
+\title{avl-verification}
+\author{stuebinm}
+\maketitle
+
+\tableofcontents
+
+% sane default for proof documents
+\parindent 0pt\parskip 0.5ex
+
+% generated text of all theories
+\input{session}
+
+% optional bibliography
+%\bibliographystyle{abbrv}
+%\bibliography{root}
+
+\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/notes.md b/notes.md
index 942e1ca..977cbd0 100644
--- a/notes.md
+++ b/notes.md
@@ -1,3 +1,20 @@
+# Isabelle
+
+build with
+
+```
+❯ isabelle build -d path/to/aeneas/backends/IsabelleHOL/ -D .
+```
+
+or open in jedit via
+
+```
+❯ isabelle jedit -d path/to/aeneas/backends/IsabelleHOL/ Verification.thy
+```
+
+(there is no nix flake output for Isabelle. Isabelle is unpackagable and the
+one that exists in nixpkgs is but a mirage)
+
 # Formalization notes
 
 - Inhabited is not synthesized systematically for any type.
diff --git a/src/main.rs b/src/main.rs
index 1fa0f35..f42ef81 100644
--- a/src/main.rs
+++ b/src/main.rs
@@ -4,47 +4,44 @@ pub enum Ordering {
     Greater,
 }
 
-trait Ord {
-    fn cmp(&self, other: &Self) -> Ordering;
-}
 
 // TODO: la structure AVLNode est extrait comme un inductif à un cas
 // au lieu d'être extrait comme une structure
-struct AVLNode<T> {
-    value: T,
-    left: AVLTree<T>,
-    right: AVLTree<T>,
+struct AVLNode {
+    val: u32,
+    left: AVLTree,
+    right: AVLTree,
 }
 
-type AVLTree<T> = Option<Box<AVLNode<T>>>;
+type AVLTree = Option<Box<AVLNode>>;
 
-struct AVLTreeSet<T> {
-    root: AVLTree<T>,
+struct AVLTreeSet {
+    root: AVLTree,
 }
 
-impl<T: Ord> AVLTreeSet<T> {
+impl AVLTreeSet {
     pub fn new() -> Self {
         Self { root: None }
     }
 
-    pub fn find(&self, value: T) -> bool {
-        let mut current_tree = &self.root;
+    pub fn find(&mut self, value: u32) -> bool {
+        let mut current_tree = &mut self.root;
 
         while let Some(current_node) = current_tree {
-            match current_node.value.cmp(&value) {
-                Ordering::Less => current_tree = &current_node.right,
+            match cmp(&current_node.val, &value) {
+                Ordering::Less => current_tree = &mut current_node.right,
                 Ordering::Equal => return true,
-                Ordering::Greater => current_tree = &current_node.left,
+                Ordering::Greater => current_tree = &mut current_node.left,
             }
         }
 
         false
     }
-    pub fn insert(&mut self, value: T) -> bool {
+    pub fn insert(&mut self, value: u32) -> bool {
         let mut current_tree = &mut self.root;
 
         while let Some(current_node) = current_tree {
-            match current_node.value.cmp(&value) {
+            match cmp(&current_node.val, &value) {
                 Ordering::Less => current_tree = &mut current_node.right,
                 Ordering::Equal => return false,
                 Ordering::Greater => current_tree = &mut current_node.left,
@@ -52,7 +49,7 @@ impl<T: Ord> AVLTreeSet<T> {
         }
 
         *current_tree = Some(Box::new(AVLNode {
-            value,
+            val: value,
             left: None,
             right: None,
         }));
@@ -61,14 +58,12 @@ impl<T: Ord> AVLTreeSet<T> {
     }
 }
 
-impl Ord for u32 {
-    fn cmp(&self, other: &Self) -> Ordering {
-        if *self < *other {
+fn cmp(a: &u32, other: &u32) -> Ordering {
+        if *a < *other {
             Ordering::Less
-        } else if *self == *other {
+        } else if *a == *other {
             Ordering::Equal
         } else {
             Ordering::Greater
         }
     }
-}