diff options
| -rw-r--r-- | .gitignore | 3 | ||||
| -rw-r--r-- | AvlVerification.lean | 87 | ||||
| -rw-r--r-- | Main.lean | 91 | ||||
| -rw-r--r-- | lakefile.lean | 19 | ||||
| -rw-r--r-- | lean-toolchain | 1 | ||||
| -rw-r--r-- | src/main.rs | 16 |
6 files changed, 208 insertions, 9 deletions
@@ -1 +1,4 @@ /target +/build +/lakefile.olean +/lake-packages/* diff --git a/AvlVerification.lean b/AvlVerification.lean new file mode 100644 index 0000000..e0516b4 --- /dev/null +++ b/AvlVerification.lean @@ -0,0 +1,87 @@ +-- THIS FILE WAS AUTOMATICALLY GENERATED BY AENEAS +-- [avl_verification] +import Base +open Primitives + +namespace avl_verification + +/- [avl_verification::Ordering] + Source: 'src/main.rs', lines 1:0-1:17 -/ +inductive Ordering := +| Less : Ordering +| Equal : Ordering +| Greater : Ordering + +/- Trait declaration: [avl_verification::Ord] + Source: 'src/main.rs', lines 7:0-7:9 -/ +structure Ord (Self : Type) where + cmp : Self → Self → Result Ordering + +/- [avl_verification::AVLNode] + Source: 'src/main.rs', lines 11:0-11:17 -/ +inductive AVLNode (T : Type) := +| mk : T → Option (AVLNode T) → Option (AVLNode T) → AVLNode T + +/- [avl_verification::AVLTreeSet] + Source: 'src/main.rs', lines 19:0-19:20 -/ +structure AVLTreeSet (T : Type) where + root : Option (AVLNode T) + +/- [avl_verification::{avl_verification::AVLTreeSet<T>}::new]: + Source: 'src/main.rs', lines 24:4-24:24 -/ +def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) := + Result.ret { root := none } + +/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0: + Source: 'src/main.rs', lines 28:4-46:5 -/ +divergent def AVLTreeSet.insert_loop + (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T)) + : + Result (Bool × (Option (AVLNode T))) + := + match current_tree with + | none => let a := AVLNode.mk value none none + Result.ret (true, some a) + | some current_node => + do + let ⟨ t, current_tree1, current_tree2 ⟩ := current_node + let o ← OrdInst.cmp t value + match o with + | Ordering.Less => + do + let (b, back) ← AVLTreeSet.insert_loop T OrdInst value current_tree2 + Result.ret (b, some (AVLNode.mk t current_tree1 back)) + | Ordering.Equal => + Result.ret (false, some (AVLNode.mk t current_tree1 current_tree2)) + | Ordering.Greater => + do + let (b, back) ← AVLTreeSet.insert_loop T OrdInst value current_tree1 + Result.ret (b, some (AVLNode.mk t back current_tree2)) + +/- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: + Source: 'src/main.rs', lines 28:4-28:46 -/ +def AVLTreeSet.insert + (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) : + Result (Bool × (AVLTreeSet T)) + := + do + let (b, back) ← AVLTreeSet.insert_loop T OrdInst value self.root + Result.ret (b, { root := back }) + +/- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]: + Source: 'src/main.rs', lines 50:4-50:43 -/ +def OrdU32.cmp (self : U32) (other : U32) : Result Ordering := + if self < other + then Result.ret Ordering.Less + else + if self = other + then Result.ret Ordering.Equal + else Result.ret Ordering.Greater + +/- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}] + Source: 'src/main.rs', lines 49:0-49:16 -/ +def OrdU32 : Ord U32 := { + cmp := OrdU32.cmp +} + +end avl_verification diff --git a/Main.lean b/Main.lean new file mode 100644 index 0000000..dea47e5 --- /dev/null +++ b/Main.lean @@ -0,0 +1,91 @@ +import «AvlVerification» +open Primitives + +namespace Avl + +-- synthesize inhabited? +-- synthesize type aliases +-- AVLTree T := Option<Box<AVLNode>> ~ AVLTree T := Option<AVLNode> + +open avl_verification +variable {T: Type} + +def AVL.nil: AVLTreeSet T := { root := none } + + +-- TODO: AVLTree T ou AVLNode T? +noncomputable def AVL.height' (tree: AVLNode T): Nat := AVLNode.rec tree + (mk := fun _ _ _ ihl ihr => 1 + ihl + ihr) + (none := 0) + (some := fun _ ih => 1 + ih) + +-- Otherwise, Lean cannot prove termination by itself. +@[reducible] +def AVLTree (U: Type) := Option (AVLNode U) + +mutual +def AVL.height'' (tree: AVLNode T): Nat := match tree with +| AVLNode.mk y left right => 1 + AVL.height left + AVL.height right + +def AVL.height (tree: AVLTree T): Nat := match tree with +| none => 0 +| some node => 1 + AVL.height'' node +end + + +def AVLTree.mem (tree: AVLTree T) (x: T): Prop := + match tree with + | none => false + | some (AVLNode.mk y left right) => x = y ∨ AVLTree.mem left x ∨ AVLTree.mem right y + +def AVLTree.setOf: AVLTree T -> Set T := AVLTree.mem + +#check AVL.nil +#check U32.ofInt 0 +#check 0#u32 +-- TODO: créer une instance OfNat pour les Uxyz. +-- TODO: générer {} adéquatement... ? + +#check (AVL.nil.insert _ _ 0#u32) + + +#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root)) +#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root)) +#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun (added, tree) => Result.ret (added, AVLTree.setOf tree.root)) +#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root)) +#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun (added, tree) => Result.ret (added, AVLTree.setOf tree.root)) +#check Primitives.bind (AVL.nil.insert _ _ 0#u32) (fun x => Result.ret (x.1, AVLTree.setOf x.2.root)) + +def AVLTreeSet.setOfInsert {H: avl_verification.Ord T} (a: T) (t: AVLTreeSet T) := Primitives.bind (t.insert _ H a) (fun (_, tree) => Result.ret (AVLTree.setOf tree.root)) + +-- TODO: derive from Ord an Lean Order instance. +-- TODO: oh no, H.cmp returns a Result! + +@[pspec] +def AVLTreeSet.insert_loop_spec {H: avl_verification.Ord T} + (a: T) (t: Option (AVLNode T)) + (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o): + ∃ t', AVLTreeSet.insert_loop T H a t = Result.ret t' := by + match t with + | none => simp [AVLTreeSet.insert_loop] + | some (AVLNode.mk b left right) => + rw [AVLTreeSet.insert_loop] + simp only [] + progress as ⟨ ordering ⟩ + cases ordering + all_goals { + simp only [] + try progress + simp + } + +@[pspec] +def AVLTreeSet.insert_spec + {H: avl_verification.Ord T} + (Hcmp_spec: ∀ a b, ∃ o, H.cmp a b = Result.ret o) + (a: T) (t: AVLTreeSet T): + ∃ t', t.insert _ H x = Result.ret t' ∧ AVLTree.setOf t'.2.root = insert a (AVLTree.setOf t.root) := by + rw [AVLTreeSet.insert] + progress; simp + +end Avl diff --git a/lakefile.lean b/lakefile.lean new file mode 100644 index 0000000..f92b653 --- /dev/null +++ b/lakefile.lean @@ -0,0 +1,19 @@ +import Lake +open Lake DSL + +require base from git + "https://github.com/AeneasVerif/aeneas"@"main"/"backends/lean" + +package «AvlVerification» where + -- add package configuration options here + +lean_lib «AvlVerification» where + -- add library configuration options here + +@[default_target] +lean_exe «avlverification» where + root := `Main + -- Enables the use of the Lean interpreter by the executable (e.g., + -- `runFrontend`) at the expense of increased binary size on Linux. + -- Remove this line if you do not need such functionality. + supportInterpreter := true diff --git a/lean-toolchain b/lean-toolchain new file mode 100644 index 0000000..cfcdd32 --- /dev/null +++ b/lean-toolchain @@ -0,0 +1 @@ +leanprover/lean4:v4.6.0-rc1 diff --git a/src/main.rs b/src/main.rs index d5bb8f9..884b367 100644 --- a/src/main.rs +++ b/src/main.rs @@ -1,10 +1,14 @@ -use std::cmp::Ordering; +pub enum Ordering { + Less, + Equal, + Greater, +} trait Ord { fn cmp(&self, other: &Self) -> Ordering; } -struct AVLNode<T: Ord> { +struct AVLNode<T> { value: T, left: AVLTree<T>, right: AVLTree<T>, @@ -12,7 +16,7 @@ struct AVLNode<T: Ord> { type AVLTree<T> = Option<Box<AVLNode<T>>>; -struct AVLTreeSet<T: Ord> { +struct AVLTreeSet<T> { root: AVLTree<T>, } @@ -53,9 +57,3 @@ impl Ord for u32 { } } } - -fn main() { - let mut tree = AVLTreeSet::new(); - tree.insert(3); - tree.insert(2); -} |