summaryrefslogtreecommitdiff
path: root/tests/lean
diff options
context:
space:
mode:
authorSon HO2023-08-09 09:58:04 +0200
committerGitHub2023-08-09 09:58:04 +0200
commit3d377976afe382a32f6ce718b473db5f016b1e47 (patch)
tree3f5b7147d1c4edc2b5c9ac002e1a203cfb396427 /tests/lean
parent1cbc7ce007cf3433a6df9bdeb12c4e27511fad9c (diff)
parent967d08107de73f7f151dc8b4fb1f1cc61f109051 (diff)
Merge pull request #33 from AeneasVerif/son_refactor
Update the code following Charon's refactor
Diffstat (limited to 'tests/lean')
-rw-r--r--tests/lean/BetreeMain/Funs.lean412
-rw-r--r--tests/lean/BetreeMain/Types.lean8
-rw-r--r--tests/lean/NoNestedBorrows.lean10
3 files changed, 215 insertions, 215 deletions
diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index a6c6f496..933aac88 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -209,20 +209,6 @@ def betree.Leaf.split_back
let _ ← betree.store_leaf_node id1 content1 st0
betree.NodeIdCounter.fresh_id_back node_id_cnt0
-/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
-divergent def betree.Node.lookup_in_bindings
- (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
- match bindings with
- | betree.List.Cons hd tl =>
- let (i, i0) := hd
- if i = key
- then Result.ret (Option.some i0)
- else
- if i > key
- then Result.ret Option.none
- else betree.Node.lookup_in_bindings key tl
- | betree.List.Nil => Result.ret Option.none
-
/- [betree_main::betree::Node::{5}::lookup_first_message_for_key]: forward function -/
divergent def betree.Node.lookup_first_message_for_key
(key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -312,8 +298,46 @@ divergent def betree.Node.apply_upserts_back
betree.List.push_front (U64 × betree.Message) msgs (key,
betree.Message.Insert v)
+/- [betree_main::betree::Node::{5}::lookup_in_bindings]: forward function -/
+divergent def betree.Node.lookup_in_bindings
+ (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+ match bindings with
+ | betree.List.Cons hd tl =>
+ let (i, i0) := hd
+ if i = key
+ then Result.ret (Option.some i0)
+ else
+ if i > key
+ then Result.ret Option.none
+ else betree.Node.lookup_in_bindings key tl
+ | betree.List.Nil => Result.ret Option.none
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
+mutual divergent def betree.Internal.lookup_in_children
+ (self : betree.Internal) (key : U64) (st : State) :
+ Result (State × (Option U64))
+ :=
+ let ⟨ _, i, n, n0 ⟩ := self
+ if key < i
+ then betree.Node.lookup n key st
+ else betree.Node.lookup n0 key st
+
+/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
+divergent def betree.Internal.lookup_in_children_back
+ (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
+ let ⟨ i, i0, n, n0 ⟩ := self
+ if key < i0
+ then
+ do
+ let n1 ← betree.Node.lookup_back n key st
+ Result.ret (betree.Internal.mk i i0 n1 n0)
+ else
+ do
+ let n1 ← betree.Node.lookup_back n0 key st
+ Result.ret (betree.Internal.mk i i0 n n1)
+
/- [betree_main::betree::Node::{5}::lookup]: forward function -/
-mutual divergent def betree.Node.lookup
+divergent def betree.Node.lookup
(self : betree.Node) (key : U64) (st : State) :
Result (State × (Option U64))
:=
@@ -455,126 +479,8 @@ divergent def betree.Node.lookup_back
let _ ← betree.Node.lookup_in_bindings key bindings
Result.ret (betree.Node.Leaf node)
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: forward function -/
-divergent def betree.Internal.lookup_in_children
- (self : betree.Internal) (key : U64) (st : State) :
- Result (State × (Option U64))
- :=
- let ⟨ _, i, n, n0 ⟩ := self
- if key < i
- then betree.Node.lookup n key st
- else betree.Node.lookup n0 key st
-
-/- [betree_main::betree::Internal::{4}::lookup_in_children]: backward function 0 -/
-divergent def betree.Internal.lookup_in_children_back
- (self : betree.Internal) (key : U64) (st : State) : Result betree.Internal :=
- let ⟨ i, i0, n, n0 ⟩ := self
- if key < i0
- then
- do
- let n1 ← betree.Node.lookup_back n key st
- Result.ret (betree.Internal.mk i i0 n1 n0)
- else
- do
- let n1 ← betree.Node.lookup_back n0 key st
- Result.ret (betree.Internal.mk i i0 n n1)
-
end
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
-divergent def betree.Node.lookup_mut_in_bindings
- (key : U64) (bindings : betree.List (U64 × U64)) :
- Result (betree.List (U64 × U64))
- :=
- match bindings with
- | betree.List.Cons hd tl =>
- let (i, i0) := hd
- if i >= key
- then Result.ret (betree.List.Cons (i, i0) tl)
- else betree.Node.lookup_mut_in_bindings key tl
- | betree.List.Nil => Result.ret betree.List.Nil
-
-/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
-divergent def betree.Node.lookup_mut_in_bindings_back
- (key : U64) (bindings : betree.List (U64 × U64))
- (ret0 : betree.List (U64 × U64)) :
- Result (betree.List (U64 × U64))
- :=
- match bindings with
- | betree.List.Cons hd tl =>
- let (i, i0) := hd
- if i >= key
- then Result.ret ret0
- else
- do
- let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
- Result.ret (betree.List.Cons (i, i0) tl0)
- | betree.List.Nil => Result.ret ret0
-
-/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
-def betree.Node.apply_to_leaf
- (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
- :
- Result (betree.List (U64 × U64))
- :=
- do
- let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
- let b ← betree.List.head_has_key U64 bindings0 key
- if b
- then
- do
- let hd ← betree.List.pop_front (U64 × U64) bindings0
- match new_msg with
- | betree.Message.Insert v =>
- do
- let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
- let bindings2 ←
- betree.List.push_front (U64 × U64) bindings1 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings2
- | betree.Message.Delete =>
- do
- let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
- betree.Node.lookup_mut_in_bindings_back key bindings bindings1
- | betree.Message.Upsert s =>
- do
- let (_, i) := hd
- let v ← betree.upsert_update (Option.some i) s
- let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
- let bindings2 ←
- betree.List.push_front (U64 × U64) bindings1 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings2
- else
- match new_msg with
- | betree.Message.Insert v =>
- do
- let bindings1 ←
- betree.List.push_front (U64 × U64) bindings0 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings1
- | betree.Message.Delete =>
- betree.Node.lookup_mut_in_bindings_back key bindings bindings0
- | betree.Message.Upsert s =>
- do
- let v ← betree.upsert_update Option.none s
- let bindings1 ←
- betree.List.push_front (U64 × U64) bindings0 (key, v)
- betree.Node.lookup_mut_in_bindings_back key bindings bindings1
-
-/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
- (there is a single backward function, and the forward function returns ()) -/
-divergent def betree.Node.apply_messages_to_leaf
- (bindings : betree.List (U64 × U64))
- (new_msgs : betree.List (U64 × betree.Message)) :
- Result (betree.List (U64 × U64))
- :=
- match new_msgs with
- | betree.List.Cons new_msg new_msgs_tl =>
- do
- let (i, m) := new_msg
- let bindings0 ← betree.Node.apply_to_leaf bindings i m
- betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
- | betree.List.Nil => Result.ret bindings
-
/- [betree_main::betree::Node::{5}::filter_messages_for_key]: merged forward/backward function
(there is a single backward function, and the forward function returns ()) -/
divergent def betree.Node.filter_messages_for_key
@@ -706,8 +612,174 @@ divergent def betree.Node.apply_messages_to_internal
betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
| betree.List.Nil => Result.ret msgs
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: forward function -/
+divergent def betree.Node.lookup_mut_in_bindings
+ (key : U64) (bindings : betree.List (U64 × U64)) :
+ Result (betree.List (U64 × U64))
+ :=
+ match bindings with
+ | betree.List.Cons hd tl =>
+ let (i, i0) := hd
+ if i >= key
+ then Result.ret (betree.List.Cons (i, i0) tl)
+ else betree.Node.lookup_mut_in_bindings key tl
+ | betree.List.Nil => Result.ret betree.List.Nil
+
+/- [betree_main::betree::Node::{5}::lookup_mut_in_bindings]: backward function 0 -/
+divergent def betree.Node.lookup_mut_in_bindings_back
+ (key : U64) (bindings : betree.List (U64 × U64))
+ (ret0 : betree.List (U64 × U64)) :
+ Result (betree.List (U64 × U64))
+ :=
+ match bindings with
+ | betree.List.Cons hd tl =>
+ let (i, i0) := hd
+ if i >= key
+ then Result.ret ret0
+ else
+ do
+ let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret0
+ Result.ret (betree.List.Cons (i, i0) tl0)
+ | betree.List.Nil => Result.ret ret0
+
+/- [betree_main::betree::Node::{5}::apply_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) -/
+def betree.Node.apply_to_leaf
+ (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
+ :
+ Result (betree.List (U64 × U64))
+ :=
+ do
+ let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
+ let b ← betree.List.head_has_key U64 bindings0 key
+ if b
+ then
+ do
+ let hd ← betree.List.pop_front (U64 × U64) bindings0
+ match new_msg with
+ | betree.Message.Insert v =>
+ do
+ let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+ let bindings2 ←
+ betree.List.push_front (U64 × U64) bindings1 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings2
+ | betree.Message.Delete =>
+ do
+ let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+ | betree.Message.Upsert s =>
+ do
+ let (_, i) := hd
+ let v ← betree.upsert_update (Option.some i) s
+ let bindings1 ← betree.List.pop_front_back (U64 × U64) bindings0
+ let bindings2 ←
+ betree.List.push_front (U64 × U64) bindings1 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings2
+ else
+ match new_msg with
+ | betree.Message.Insert v =>
+ do
+ let bindings1 ←
+ betree.List.push_front (U64 × U64) bindings0 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+ | betree.Message.Delete =>
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings0
+ | betree.Message.Upsert s =>
+ do
+ let v ← betree.upsert_update Option.none s
+ let bindings1 ←
+ betree.List.push_front (U64 × U64) bindings0 (key, v)
+ betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+
+/- [betree_main::betree::Node::{5}::apply_messages_to_leaf]: merged forward/backward function
+ (there is a single backward function, and the forward function returns ()) -/
+divergent def betree.Node.apply_messages_to_leaf
+ (bindings : betree.List (U64 × U64))
+ (new_msgs : betree.List (U64 × betree.Message)) :
+ Result (betree.List (U64 × U64))
+ :=
+ match new_msgs with
+ | betree.List.Cons new_msg new_msgs_tl =>
+ do
+ let (i, m) := new_msg
+ let bindings0 ← betree.Node.apply_to_leaf bindings i m
+ betree.Node.apply_messages_to_leaf bindings0 new_msgs_tl
+ | betree.List.Nil => Result.ret bindings
+
+/- [betree_main::betree::Internal::{4}::flush]: forward function -/
+mutual divergent def betree.Internal.flush
+ (self : betree.Internal) (params : betree.Params)
+ (node_id_cnt : betree.NodeIdCounter)
+ (content : betree.List (U64 × betree.Message)) (st : State) :
+ Result (State × (betree.List (U64 × betree.Message)))
+ :=
+ do
+ let ⟨ _, i, n, n0 ⟩ := self
+ let p ← betree.List.partition_at_pivot betree.Message content i
+ let (msgs_left, msgs_right) := p
+ let len_left ← betree.List.len (U64 × betree.Message) msgs_left
+ if len_left >= params.min_flush_size
+ then
+ do
+ let (st0, _) ←
+ betree.Node.apply_messages n params node_id_cnt msgs_left st
+ let (_, node_id_cnt0) ←
+ betree.Node.apply_messages_back n params node_id_cnt msgs_left st
+ let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+ if len_right >= params.min_flush_size
+ then
+ do
+ let (st1, _) ←
+ betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0
+ let _ ←
+ betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
+ st0
+ Result.ret (st1, betree.List.Nil)
+ else Result.ret (st0, msgs_right)
+ else
+ do
+ let (st0, _) ←
+ betree.Node.apply_messages n0 params node_id_cnt msgs_right st
+ let _ ←
+ betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
+ Result.ret (st0, msgs_left)
+
+/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
+divergent def betree.Internal.flush_back
+ (self : betree.Internal) (params : betree.Params)
+ (node_id_cnt : betree.NodeIdCounter)
+ (content : betree.List (U64 × betree.Message)) (st : State) :
+ Result (betree.Internal × betree.NodeIdCounter)
+ :=
+ do
+ let ⟨ i, i0, n, n0 ⟩ := self
+ let p ← betree.List.partition_at_pivot betree.Message content i0
+ let (msgs_left, msgs_right) := p
+ let len_left ← betree.List.len (U64 × betree.Message) msgs_left
+ if len_left >= params.min_flush_size
+ then
+ do
+ let (st0, _) ←
+ betree.Node.apply_messages n params node_id_cnt msgs_left st
+ let (n1, node_id_cnt0) ←
+ betree.Node.apply_messages_back n params node_id_cnt msgs_left st
+ let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+ if len_right >= params.min_flush_size
+ then
+ do
+ let (n2, node_id_cnt1) ←
+ betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
+ st0
+ Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1)
+ else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0)
+ else
+ do
+ let (n1, node_id_cnt0) ←
+ betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
+ Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
+
/- [betree_main::betree::Node::{5}::apply_messages]: forward function -/
-mutual divergent def betree.Node.apply_messages
+divergent def betree.Node.apply_messages
(self : betree.Node) (params : betree.Params)
(node_id_cnt : betree.NodeIdCounter)
(msgs : betree.List (U64 × betree.Message)) (st : State) :
@@ -806,78 +878,6 @@ divergent def betree.Node.apply_messages_back
let _ ← betree.store_leaf_node node.id content0 st0
Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt)
-/- [betree_main::betree::Internal::{4}::flush]: forward function -/
-divergent def betree.Internal.flush
- (self : betree.Internal) (params : betree.Params)
- (node_id_cnt : betree.NodeIdCounter)
- (content : betree.List (U64 × betree.Message)) (st : State) :
- Result (State × (betree.List (U64 × betree.Message)))
- :=
- do
- let ⟨ _, i, n, n0 ⟩ := self
- let p ← betree.List.partition_at_pivot betree.Message content i
- let (msgs_left, msgs_right) := p
- let len_left ← betree.List.len (U64 × betree.Message) msgs_left
- if len_left >= params.min_flush_size
- then
- do
- let (st0, _) ←
- betree.Node.apply_messages n params node_id_cnt msgs_left st
- let (_, node_id_cnt0) ←
- betree.Node.apply_messages_back n params node_id_cnt msgs_left st
- let len_right ← betree.List.len (U64 × betree.Message) msgs_right
- if len_right >= params.min_flush_size
- then
- do
- let (st1, _) ←
- betree.Node.apply_messages n0 params node_id_cnt0 msgs_right st0
- let _ ←
- betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
- st0
- Result.ret (st1, betree.List.Nil)
- else Result.ret (st0, msgs_right)
- else
- do
- let (st0, _) ←
- betree.Node.apply_messages n0 params node_id_cnt msgs_right st
- let _ ←
- betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
- Result.ret (st0, msgs_left)
-
-/- [betree_main::betree::Internal::{4}::flush]: backward function 0 -/
-divergent def betree.Internal.flush_back
- (self : betree.Internal) (params : betree.Params)
- (node_id_cnt : betree.NodeIdCounter)
- (content : betree.List (U64 × betree.Message)) (st : State) :
- Result (betree.Internal × betree.NodeIdCounter)
- :=
- do
- let ⟨ i, i0, n, n0 ⟩ := self
- let p ← betree.List.partition_at_pivot betree.Message content i0
- let (msgs_left, msgs_right) := p
- let len_left ← betree.List.len (U64 × betree.Message) msgs_left
- if len_left >= params.min_flush_size
- then
- do
- let (st0, _) ←
- betree.Node.apply_messages n params node_id_cnt msgs_left st
- let (n1, node_id_cnt0) ←
- betree.Node.apply_messages_back n params node_id_cnt msgs_left st
- let len_right ← betree.List.len (U64 × betree.Message) msgs_right
- if len_right >= params.min_flush_size
- then
- do
- let (n2, node_id_cnt1) ←
- betree.Node.apply_messages_back n0 params node_id_cnt0 msgs_right
- st0
- Result.ret (betree.Internal.mk i i0 n1 n2, node_id_cnt1)
- else Result.ret (betree.Internal.mk i i0 n1 n0, node_id_cnt0)
- else
- do
- let (n1, node_id_cnt0) ←
- betree.Node.apply_messages_back n0 params node_id_cnt msgs_right st
- Result.ret (betree.Internal.mk i i0 n n1, node_id_cnt0)
-
end
/- [betree_main::betree::Node::{5}::apply]: forward function -/
diff --git a/tests/lean/BetreeMain/Types.lean b/tests/lean/BetreeMain/Types.lean
index c02c148a..2f5de6a0 100644
--- a/tests/lean/BetreeMain/Types.lean
+++ b/tests/lean/BetreeMain/Types.lean
@@ -28,15 +28,15 @@ structure betree.Leaf where
mutual
+/- [betree_main::betree::Internal] -/
+inductive betree.Internal :=
+| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
+
/- [betree_main::betree::Node] -/
inductive betree.Node :=
| Internal : betree.Internal → betree.Node
| Leaf : betree.Leaf → betree.Node
-/- [betree_main::betree::Internal] -/
-inductive betree.Internal :=
-| mk : U64 → U64 → betree.Node → betree.Node → betree.Internal
-
end
/- [betree_main::betree::Params] -/
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index 1a180c60..884e62c4 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -251,16 +251,16 @@ def test_char : Result Char :=
mutual
-/- [no_nested_borrows::NodeElem] -/
-inductive NodeElem (T : Type) :=
-| Cons : Tree T → NodeElem T → NodeElem T
-| Nil : NodeElem T
-
/- [no_nested_borrows::Tree] -/
inductive Tree (T : Type) :=
| Leaf : T → Tree T
| Node : T → NodeElem T → Tree T → Tree T
+/- [no_nested_borrows::NodeElem] -/
+inductive NodeElem (T : Type) :=
+| Cons : Tree T → NodeElem T → NodeElem T
+| Nil : NodeElem T
+
end
/- [no_nested_borrows::list_length]: forward function -/