diff options
| -rw-r--r-- | AvlVerification.lean | 20 | ||||
| -rw-r--r-- | AvlVerification/Insert.lean | 115 | ||||
| -rw-r--r-- | AvlVerification/Specifications.lean | 36 | ||||
| -rw-r--r-- | AvlVerification/Tree.lean | 3 | ||||
| -rw-r--r-- | lake-manifest.json | 2 | ||||
| -rw-r--r-- | notes.md | 5 |
6 files changed, 95 insertions, 86 deletions
diff --git a/AvlVerification.lean b/AvlVerification.lean index b90680c..f9e6830 100644 --- a/AvlVerification.lean +++ b/AvlVerification.lean @@ -32,16 +32,8 @@ structure AVLTreeSet (T : Type) where def AVLTreeSet.new (T : Type) (OrdInst : Ord T) : Result (AVLTreeSet T) := Result.ok { root := none } -/- [avl_verification::{avl_verification::AVLTreeSet<T>}::find]: - Source: 'src/main.rs', lines 30:4-30:39 -/ -def AVLTreeSet.find - (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) : - Result Bool - := - sorry - /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: loop 0: - Source: 'src/main.rs', lines 63:4-81:5 -/ + Source: 'src/main.rs', lines 43:4-61:5 -/ divergent def AVLTreeSet.insert_loop (T : Type) (OrdInst : Ord T) (value : T) (current_tree : Option (AVLNode T)) : @@ -69,17 +61,17 @@ divergent def AVLTreeSet.insert_loop Result.ok (b, some (AVLNode.mk t current_tree3 current_tree2)) /- [avl_verification::{avl_verification::AVLTreeSet<T>}::insert]: - Source: 'src/main.rs', lines 63:4-63:46 -/ + Source: 'src/main.rs', lines 43:4-43:46 -/ def AVLTreeSet.insert (T : Type) (OrdInst : Ord T) (self : AVLTreeSet T) (value : T) : Result (Bool × (AVLTreeSet T)) := do - let (b, as) ← AVLTreeSet.insert_loop T OrdInst value self.root - Result.ok (b, { root := as }) + let (b, u) ← AVLTreeSet.insert_loop T OrdInst value self.root + Result.ok (b, { root := u }) /- [avl_verification::{(avl_verification::Ord for u32)#1}::cmp]: - Source: 'src/main.rs', lines 85:4-85:43 -/ + Source: 'src/main.rs', lines 65:4-65:43 -/ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering := if self < other then Result.ok Ordering.Less @@ -89,7 +81,7 @@ def OrdU32.cmp (self : U32) (other : U32) : Result Ordering := else Result.ok Ordering.Greater /- Trait implementation: [avl_verification::{(avl_verification::Ord for u32)#1}] - Source: 'src/main.rs', lines 84:0-84:16 -/ + Source: 'src/main.rs', lines 64:0-64:16 -/ def OrdU32 : Ord U32 := { cmp := OrdU32.cmp } diff --git a/AvlVerification/Insert.lean b/AvlVerification/Insert.lean index baf3441..16e740f 100644 --- a/AvlVerification/Insert.lean +++ b/AvlVerification/Insert.lean @@ -6,55 +6,49 @@ namespace Implementation open Primitives open avl_verification -open Tree (AVLTree) -open Specifications (OrdSpec ordSpecOfTotalityAndDuality ordOfOrdSpec ltOfRustOrder gtOfRustOrder) +open Tree (AVLTree AVLTree.set) +open Specifications (OrdSpecDualityEq ordOfOrdSpec ltOfRustOrder gtOfRustOrder) -example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _ - (by - -- Totality - intro a b - unfold Ord.cmp - unfold OrdU32 - unfold OrdU32.cmp - if hlt : a < b then - use .Less - simp [hlt] - else - if heq: a = b - then - use .Equal - simp [hlt] - rw [heq] - -- TODO: simp [hlt, heq] breaks everything??? - else - use .Greater - simp [hlt, heq] - ) (by - -- Duality - intro a b Hgt - if hlt : b < a then - unfold Ord.cmp - unfold OrdU32 - unfold OrdU32.cmp - simp [hlt] - else - unfold Ord.cmp at Hgt - unfold OrdU32 at Hgt - unfold OrdU32.cmp at Hgt - have hnlt : ¬ (a < b) := sorry - have hneq : ¬ (a = b) := sorry - exfalso - apply hlt - -- I need a Preorder on U32 now. - sorry) +-- example: OrdSpec OrdU32 := ordSpecOfTotalityAndDuality _ +-- (by +-- -- Totality +-- intro a b +-- unfold Ord.cmp +-- unfold OrdU32 +-- unfold OrdU32.cmp +-- if hlt : a < b then +-- use .Less +-- simp [hlt] +-- else +-- if heq: a = b +-- then +-- use .Equal +-- simp [hlt] +-- rw [heq] +-- -- TODO: simp [hlt, heq] breaks everything??? +-- else +-- use .Greater +-- simp [hlt, heq] +-- ) (by +-- -- Duality +-- intro a b Hgt +-- if hlt : b < a then +-- unfold Ord.cmp +-- unfold OrdU32 +-- unfold OrdU32.cmp +-- simp [hlt] +-- else +-- unfold Ord.cmp at Hgt +-- unfold OrdU32 at Hgt +-- unfold OrdU32.cmp at Hgt +-- have hnlt : ¬ (a < b) := sorry +-- have hneq : ¬ (a = b) := sorry +-- exfalso +-- apply hlt +-- -- I need a Preorder on U32 now. +-- sorry) -variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpec T H) - -instance rustOrder {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): _root_.Ord U := ordOfOrdSpec O OSpec --- Why the TC fails if I don't specify the previous instance explicitly? -instance rustLt {U: Type} {O: avl_verification.Ord U} (OSpec: OrdSpec O): LT U := @ltOfOrd _ (ordOfOrdSpec O OSpec) - -instance rustLt' : LT T := rustLt Ospec +variable (T: Type) (H: avl_verification.Ord T) (Ospec: @OrdSpecDualityEq T H) @[pspec] theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) @@ -105,14 +99,11 @@ theorem AVLTreeSet.insert_loop_spec_local (p: T -> Prop) lemma AVLTreeSet.insert_loop_spec_global (a: T) (t: Option (AVLNode T)) : - haveI : LT T := (rustLt Ospec) BST.Invariant t -> ∃ added t_new, AVLTreeSet.insert_loop T H a t = Result.ok ⟨ added, t_new ⟩ - ∧ BST.Invariant t_new := by + ∧ BST.Invariant t_new ∧ AVLTree.set t_new = {a} ∪ AVLTree.set t := by intro Hbst - letI instOrd : _root_.Ord T := (rustOrder Ospec) - letI instLt : LT T := (rustLt Ospec) match t with - | none => simp [AVLTreeSet.insert_loop] + | none => simp [AVLTreeSet.insert_loop, AVLTree.set, setOf] | some (AVLNode.mk b left right) => rw [AVLTreeSet.insert_loop] simp only [] @@ -121,12 +112,13 @@ lemma AVLTreeSet.insert_loop_spec_global cases ordering all_goals simp only [] { - have ⟨ added₂, right₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst) + have ⟨ added₂, right₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a right (BST.right Hbst) progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, right₁, Hnode ⟩ exact (fun x => b < x) rewrite [Htree] at H_result; simp at H_result refine' ⟨ added₁, ⟨ some (AVLNode.mk b left right₁), _ ⟩ ⟩ simp only [true_and] + split_conjs cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right constructor exact H_forall_left @@ -135,17 +127,23 @@ lemma AVLTreeSet.insert_loop_spec_global exact H_bst_left convert H_bst exact H_result.2 + simp [AVLTree.set_some] + rewrite [H_result.2, H_set] + simp } { - simp; tauto + simp; split_conjs + . tauto + . simp [Ospec.equality _ _ Hordering] } { - have ⟨ added₂, left₂, ⟨ H_result, H_bst ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst) + have ⟨ added₂, left₂, ⟨ H_result, ⟨ H_bst, H_set ⟩ ⟩ ⟩ := AVLTreeSet.insert_loop_spec_global a left (BST.left Hbst) progress keep Htree with AVLTreeSet.insert_loop_spec_local as ⟨ added₁, left₁, Hnode ⟩ exact (fun x => x < b) rewrite [Htree] at H_result; simp at H_result refine' ⟨ added₁, ⟨ some (AVLNode.mk b left₁ right), _ ⟩ ⟩ simp only [true_and] + split_conjs cases' Hbst with _ _ _ H_forall_left H_forall_right H_bst_left H_bst_right constructor apply Hnode; exact H_forall_left @@ -154,15 +152,18 @@ lemma AVLTreeSet.insert_loop_spec_global convert H_bst exact H_result.2 exact H_bst_right + simp [AVLTree.set_some] + rewrite [H_result.2, H_set] + simp [Set.singleton_union, Set.insert_comm, Set.insert_union] } @[pspec] def AVLTreeSet.insert_spec (a: T) (t: AVLTreeSet T): - haveI : LT T := (rustLt Ospec) BST.Invariant t.root -> (∃ t' added,t.insert _ H a = Result.ok (added, t') -- it's still a binary search tree. - ∧ BST.Invariant t'.root) + ∧ BST.Invariant t'.root + ∧ AVLTree.set t'.root = {a} ∪ AVLTree.set t.root) := by rw [AVLTreeSet.insert]; intro Hbst progress keep h as ⟨ t', Hset ⟩; diff --git a/AvlVerification/Specifications.lean b/AvlVerification/Specifications.lean index 958a3e7..0694df3 100644 --- a/AvlVerification/Specifications.lean +++ b/AvlVerification/Specifications.lean @@ -42,32 +42,40 @@ namespace Specifications open Primitives open Result -variable {T: Type} (H: avl_verification.Ord T) +variable {T: Type} (H: outParam (avl_verification.Ord T)) -- TODO: reason about raw bundling vs. refined bundling. -class OrdSpec where +-- raw bundling: hypothesis with Rust extracted objects. +-- refined bundling: lifted hypothesis with Lean native objects. +class OrdSpecInfaillible where infallible: ∀ a b, ∃ (o: avl_verification.Ordering), H.cmp a b = .ok o + +class OrdSpecDuality extends OrdSpecInfaillible H where duality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less +-- TODO: OrdSpecEq := OrdSpecRel (R := Eq). +class OrdSpecEq extends OrdSpecInfaillible H where + equality: ∀ a b, H.cmp a b = .ok .Equal -> a = b + +class OrdSpecRel (R: outParam (T -> T -> Prop)) extends OrdSpecInfaillible H where + equivalence: ∀ a b, H.cmp a b = .ok .Equal -> R a b + +class OrdSpecDualityEq extends OrdSpecDuality H, OrdSpecEq H + instance: Coe (avl_verification.Ordering) (_root_.Ordering) where coe a := a.toLeanOrdering -def ordSpecOfTotalityAndDuality - (H: avl_verification.Ord T) - (Hresult: ∀ a b, ∃ o, H.cmp a b = Primitives.Result.ok o) - (Hduality: ∀ a b, H.cmp a b = .ok .Greater -> H.cmp b a = .ok .Less) - : OrdSpec H where - infallible := Hresult - duality := Hduality - -def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpec H): Ord T where +def ordOfOrdSpec (H: avl_verification.Ord T) (spec: OrdSpecInfaillible H): Ord T where compare x y := (H.cmp x y).get? (by cases' (spec.infallible x y) with o Hcmp rewrite [isok, Hcmp] simp only ) -theorem ltOfRustOrder {Spec: OrdSpec H}: +instance [spec: OrdSpecInfaillible H]: Ord T := ordOfOrdSpec H spec +instance [OrdSpecInfaillible H]: LT T := ltOfOrd + +theorem ltOfRustOrder {Spec: OrdSpecInfaillible H}: haveI O := ordOfOrdSpec H Spec haveI := @ltOfOrd _ O ∀ a b, H.cmp a b = .ok .Less -> a < b := by @@ -81,8 +89,8 @@ theorem ltOfRustOrder {Spec: OrdSpec H}: simp_rw [Hcmp, get?, avl_verification.Ordering.toLeanOrdering] rfl -theorem gtOfRustOrder {Spec: OrdSpec H}: - haveI O := ordOfOrdSpec H Spec +theorem gtOfRustOrder {Spec: OrdSpecDuality H}: + haveI O := ordOfOrdSpec H Spec.toOrdSpecInfaillible haveI := @ltOfOrd _ O ∀ a b, H.cmp a b = .ok .Greater -> b < a := by intros a b diff --git a/AvlVerification/Tree.lean b/AvlVerification/Tree.lean index fdd4b78..8a043a1 100644 --- a/AvlVerification/Tree.lean +++ b/AvlVerification/Tree.lean @@ -75,4 +75,7 @@ def AVLTree.mem_some {x: T} {left right: AVLTree T}: AVLTree.mem (some (AVLNode. def AVLTree.set (t: AVLTree T): Set T := _root_.setOf (AVLTree.mem t) +@[simp] +def AVLTree.set_some {x: T} {left right: AVLTree T}: AVLTree.set (some (AVLNode.mk x left right)) = {x} ∪ AVLTree.set left ∪ AVLTree.set right := sorry + end Tree diff --git a/lake-manifest.json b/lake-manifest.json index 3e20e73..3c33932 100644 --- a/lake-manifest.json +++ b/lake-manifest.json @@ -67,7 +67,7 @@ {"url": "https://github.com/AeneasVerif/aeneas", "type": "git", "subDir": "backends/lean", - "rev": "03a175b423c9ccff2160300c4d349978f9b1aeb9", + "rev": "23da71768c03d955c916635bfc5c9d5806a80187", "name": "base", "manifestFile": "lake-manifest.json", "inputRev": "main", @@ -123,3 +123,8 @@ Source: 'src/main.rs', lines 132:4-158:5 [Error] There should be no bottoms in the value Source: 'src/main.rs', lines 175:52-181:9 ``` + +## Réunion + +- Prédicat avec `setOf`: OK. +- `ForallNode` négatif pour exclure l'appartenance d'un élément à l'arbre |