diff options
| -rw-r--r-- | .gitignore | 2 | ||||
| -rw-r--r-- | Notraits.thy | 114 | ||||
| -rw-r--r-- | ROOT | 7 | ||||
| -rw-r--r-- | Verification.thy | 122 | ||||
| -rw-r--r-- | document/root.tex | 60 | ||||
| -rw-r--r-- | notes.md | 17 | ||||
| -rw-r--r-- | src/main.rs | 43 |
7 files changed, 341 insertions, 24 deletions
@@ -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 @@ -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: @@ -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 = ¤t_node.right, + match cmp(¤t_node.val, &value) { + Ordering::Less => current_tree = &mut current_node.right, Ordering::Equal => return true, - Ordering::Greater => current_tree = ¤t_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(¤t_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 } } -} |