Initial extraction

Signed-off-by: Raito Bezarius <masterancpp@gmail.com>

6 files changed, 208 insertions, 9 deletions

diff --git a/.gitignore b/.gitignore
index ea8c4bf..3842f24 100644
--- a/.gitignore
+++ b/.gitignore
@@ -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);
-}