Merge pull request #64 from AeneasVerif/son/merge_back

Merge the forward/backward functions

1 files changed, 393 insertions, 751 deletions

diff --git a/tests/lean/BetreeMain/Funs.lean b/tests/lean/BetreeMain/Funs.lean
index 0d7cb984..96daa197 100644
--- a/tests/lean/BetreeMain/Funs.lean
+++ b/tests/lean/BetreeMain/Funs.lean
@@ -7,7 +7,7 @@ open Primitives
 
 namespace betree_main
 
-/- [betree_main::betree::load_internal_node]: forward function
+/- [betree_main::betree::load_internal_node]:
    Source: 'src/betree.rs', lines 36:0-36:52 -/
 def betree.load_internal_node
   (id : U64) (st : State) :
@@ -15,65 +15,53 @@ def betree.load_internal_node
   :=
   betree_utils.load_internal_node id st
 
-/- [betree_main::betree::store_internal_node]: forward function
+/- [betree_main::betree::store_internal_node]:
    Source: 'src/betree.rs', lines 41:0-41:60 -/
 def betree.store_internal_node
   (id : U64) (content : betree.List (U64 × betree.Message)) (st : State) :
   Result (State × Unit)
   :=
   do
-    let (st0, _) ← betree_utils.store_internal_node id content st
-    Result.ret (st0, ())
+  let (st1, _) ← betree_utils.store_internal_node id content st
+  Result.ret (st1, ())
 
-/- [betree_main::betree::load_leaf_node]: forward function
+/- [betree_main::betree::load_leaf_node]:
    Source: 'src/betree.rs', lines 46:0-46:44 -/
 def betree.load_leaf_node
   (id : U64) (st : State) : Result (State × (betree.List (U64 × U64))) :=
   betree_utils.load_leaf_node id st
 
-/- [betree_main::betree::store_leaf_node]: forward function
+/- [betree_main::betree::store_leaf_node]:
    Source: 'src/betree.rs', lines 51:0-51:52 -/
 def betree.store_leaf_node
   (id : U64) (content : betree.List (U64 × U64)) (st : State) :
   Result (State × Unit)
   :=
   do
-    let (st0, _) ← betree_utils.store_leaf_node id content st
-    Result.ret (st0, ())
+  let (st1, _) ← betree_utils.store_leaf_node id content st
+  Result.ret (st1, ())
 
-/- [betree_main::betree::fresh_node_id]: forward function
+/- [betree_main::betree::fresh_node_id]:
    Source: 'src/betree.rs', lines 55:0-55:48 -/
-def betree.fresh_node_id (counter : U64) : Result U64 :=
+def betree.fresh_node_id (counter : U64) : Result (U64 × U64) :=
   do
-    let _ ← counter + 1#u64
-    Result.ret counter
+  let counter1 ← counter + 1#u64
+  Result.ret (counter, counter1)
 
-/- [betree_main::betree::fresh_node_id]: backward function 0
-   Source: 'src/betree.rs', lines 55:0-55:48 -/
-def betree.fresh_node_id_back (counter : U64) : Result U64 :=
-  counter + 1#u64
-
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]: forward function
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::new]:
    Source: 'src/betree.rs', lines 206:4-206:20 -/
 def betree.NodeIdCounter.new : Result betree.NodeIdCounter :=
   Result.ret { next_node_id := 0#u64 }
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: forward function
+/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]:
    Source: 'src/betree.rs', lines 210:4-210:36 -/
-def betree.NodeIdCounter.fresh_id (self : betree.NodeIdCounter) : Result U64 :=
+def betree.NodeIdCounter.fresh_id
+  (self : betree.NodeIdCounter) : Result (U64 × betree.NodeIdCounter) :=
   do
-    let _ ← self.next_node_id + 1#u64
-    Result.ret self.next_node_id
+  let i ← self.next_node_id + 1#u64
+  Result.ret (self.next_node_id, { next_node_id := i })
 
-/- [betree_main::betree::{betree_main::betree::NodeIdCounter}::fresh_id]: backward function 0
-   Source: 'src/betree.rs', lines 210:4-210:36 -/
-def betree.NodeIdCounter.fresh_id_back
-  (self : betree.NodeIdCounter) : Result betree.NodeIdCounter :=
-  do
-    let i ← self.next_node_id + 1#u64
-    Result.ret { next_node_id := i }
-
-/- [betree_main::betree::upsert_update]: forward function
+/- [betree_main::betree::upsert_update]:
    Source: 'src/betree.rs', lines 234:0-234:70 -/
 def betree.upsert_update
   (prev : Option U64) (st : betree.UpsertFunState) : Result U64 :=
@@ -81,30 +69,30 @@ def betree.upsert_update
   | none =>
     match st with
     | betree.UpsertFunState.Add v => Result.ret v
-    | betree.UpsertFunState.Sub i => Result.ret 0#u64
-  | some prev0 =>
+    | betree.UpsertFunState.Sub _ => Result.ret 0#u64
+  | some prev1 =>
     match st with
     | betree.UpsertFunState.Add v =>
       do
-        let margin ← core_u64_max - prev0
-        if margin >= v
-        then prev0 + v
-        else Result.ret core_u64_max
+      let margin ← core_u64_max - prev1
+      if margin >= v
+      then prev1 + v
+      else Result.ret core_u64_max
     | betree.UpsertFunState.Sub v =>
-      if prev0 >= v
-      then prev0 - v
+      if prev1 >= v
+      then prev1 - v
       else Result.ret 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]: forward function
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::len]:
    Source: 'src/betree.rs', lines 276:4-276:24 -/
 divergent def betree.List.len (T : Type) (self : betree.List T) : Result U64 :=
   match self with
-  | betree.List.Cons t tl => do
-                               let i ← betree.List.len T tl
-                               1#u64 + i
+  | betree.List.Cons _ tl => do
+                             let i ← betree.List.len T tl
+                             1#u64 + i
   | betree.List.Nil => Result.ret 0#u64
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]: forward function
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::split_at]:
    Source: 'src/betree.rs', lines 284:4-284:51 -/
 divergent def betree.List.split_at
   (T : Type) (self : betree.List T) (n : U64) :
@@ -116,56 +104,45 @@ divergent def betree.List.split_at
     match self with
     | betree.List.Cons hd tl =>
       do
-        let i ← n - 1#u64
-        let p ← betree.List.split_at T tl i
-        let (ls0, ls1) := p
-        let l := ls0
-        Result.ret (betree.List.Cons hd l, ls1)
+      let i ← n - 1#u64
+      let p ← betree.List.split_at T tl i
+      let (ls0, ls1) := p
+      Result.ret (betree.List.Cons hd ls0, ls1)
     | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ())
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::push_front]:
    Source: 'src/betree.rs', lines 299:4-299:34 -/
 def betree.List.push_front
   (T : Type) (self : betree.List T) (x : T) : Result (betree.List T) :=
-  let tl := core.mem.replace (betree.List T) self betree.List.Nil
-  let l := tl
-  Result.ret (betree.List.Cons x l)
-
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: forward function
-   Source: 'src/betree.rs', lines 306:4-306:32 -/
-def betree.List.pop_front (T : Type) (self : betree.List T) : Result T :=
-  let ls := core.mem.replace (betree.List T) self betree.List.Nil
-  match ls with
-  | betree.List.Cons x tl => Result.ret x
-  | betree.List.Nil => Result.fail .panic
+  let (tl, _) := core.mem.replace (betree.List T) self betree.List.Nil
+  Result.ret (betree.List.Cons x tl)
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]: backward function 0
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::pop_front]:
    Source: 'src/betree.rs', lines 306:4-306:32 -/
-def betree.List.pop_front_back
-  (T : Type) (self : betree.List T) : Result (betree.List T) :=
-  let ls := core.mem.replace (betree.List T) self betree.List.Nil
+def betree.List.pop_front
+  (T : Type) (self : betree.List T) : Result (T × (betree.List T)) :=
+  let (ls, _) := core.mem.replace (betree.List T) self betree.List.Nil
   match ls with
-  | betree.List.Cons x tl => Result.ret tl
+  | betree.List.Cons x tl => Result.ret (x, tl)
   | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]: forward function
+/- [betree_main::betree::{betree_main::betree::List<T>#1}::hd]:
    Source: 'src/betree.rs', lines 318:4-318:22 -/
 def betree.List.hd (T : Type) (self : betree.List T) : Result T :=
   match self with
-  | betree.List.Cons hd l => Result.ret hd
+  | betree.List.Cons hd _ => Result.ret hd
   | betree.List.Nil => Result.fail .panic
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]: forward function
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::head_has_key]:
    Source: 'src/betree.rs', lines 327:4-327:44 -/
 def betree.ListTupleU64T.head_has_key
   (T : Type) (self : betree.List (U64 × T)) (key : U64) : Result Bool :=
   match self with
-  | betree.List.Cons hd l => let (i, _) := hd
+  | betree.List.Cons hd _ => let (i, _) := hd
                              Result.ret (i = key)
   | betree.List.Nil => Result.ret false
 
-/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]: forward function
+/- [betree_main::betree::{betree_main::betree::List<(u64, T)>#2}::partition_at_pivot]:
    Source: 'src/betree.rs', lines 339:4-339:73 -/
 divergent def betree.ListTupleU64T.partition_at_pivot
   (T : Type) (self : betree.List (U64 × T)) (pivot : U64) :
@@ -178,334 +155,186 @@ divergent def betree.ListTupleU64T.partition_at_pivot
     then Result.ret (betree.List.Nil, betree.List.Cons (i, t) tl)
     else
       do
-        let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
-        let (ls0, ls1) := p
-        let l := ls0
-        Result.ret (betree.List.Cons (i, t) l, ls1)
+      let p ← betree.ListTupleU64T.partition_at_pivot T tl pivot
+      let (ls0, ls1) := p
+      Result.ret (betree.List.Cons (i, t) ls0, ls1)
   | betree.List.Nil => Result.ret (betree.List.Nil, betree.List.Nil)
 
-/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: forward function
+/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]:
    Source: 'src/betree.rs', lines 359:4-364:17 -/
 def betree.Leaf.split
   (self : betree.Leaf) (content : betree.List (U64 × U64))
   (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
-  Result (State × betree.Internal)
+  Result (State × (betree.Internal × betree.NodeIdCounter))
   :=
   do
-    let p ← betree.List.split_at (U64 × U64) content params.split_size
-    let (content0, content1) := p
-    let p0 ← betree.List.hd (U64 × U64) content1
-    let (pivot, _) := p0
-    let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt
-    let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt
-    let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0
-    let (st0, _) ← betree.store_leaf_node id0 content0 st
-    let (st1, _) ← betree.store_leaf_node id1 content1 st0
-    let n := betree.Node.Leaf { id := id0, size := params.split_size }
-    let n0 := betree.Node.Leaf { id := id1, size := params.split_size }
-    Result.ret (st1, betree.Internal.mk self.id pivot n n0)
-
-/- [betree_main::betree::{betree_main::betree::Leaf#3}::split]: backward function 2
-   Source: 'src/betree.rs', lines 359:4-364:17 -/
-def betree.Leaf.split_back
-  (self : betree.Leaf) (content : betree.List (U64 × U64))
-  (params : betree.Params) (node_id_cnt : betree.NodeIdCounter) (st : State) :
-  Result betree.NodeIdCounter
-  :=
-  do
-    let p ← betree.List.split_at (U64 × U64) content params.split_size
-    let (content0, content1) := p
-    let _ ← betree.List.hd (U64 × U64) content1
-    let id0 ← betree.NodeIdCounter.fresh_id node_id_cnt
-    let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt
-    let id1 ← betree.NodeIdCounter.fresh_id node_id_cnt0
-    let (st0, _) ← betree.store_leaf_node id0 content0 st
-    let _ ← betree.store_leaf_node id1 content1 st0
-    betree.NodeIdCounter.fresh_id_back node_id_cnt0
-
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: forward function
+  let p ← betree.List.split_at (U64 × U64) content params.split_size
+  let (content0, content1) := p
+  let p1 ← betree.List.hd (U64 × U64) content1
+  let (pivot, _) := p1
+  let (id0, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt
+  let (id1, nic1) ← betree.NodeIdCounter.fresh_id nic
+  let (st1, _) ← betree.store_leaf_node id0 content0 st
+  let (st2, _) ← betree.store_leaf_node id1 content1 st1
+  let n := betree.Node.Leaf { id := id0, size := params.split_size }
+  let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
+  Result.ret (st2, (betree.Internal.mk self.id pivot n n1, nic1))
+
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]:
    Source: 'src/betree.rs', lines 789:4-792:34 -/
 divergent def betree.Node.lookup_first_message_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
-  Result (betree.List (U64 × betree.Message))
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
   :=
   match msgs with
   | betree.List.Cons x next_msgs =>
     let (i, m) := x
     if i >= key
-    then Result.ret (betree.List.Cons (i, m) next_msgs)
-    else betree.Node.lookup_first_message_for_key key next_msgs
-  | betree.List.Nil => Result.ret betree.List.Nil
-
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_for_key]: backward function 0
-   Source: 'src/betree.rs', lines 789:4-792:34 -/
-divergent def betree.Node.lookup_first_message_for_key_back
-  (key : U64) (msgs : betree.List (U64 × betree.Message))
-  (ret : betree.List (U64 × betree.Message)) :
-  Result (betree.List (U64 × betree.Message))
-  :=
-  match msgs with
-  | betree.List.Cons x next_msgs =>
-    let (i, m) := x
-    if i >= key
-    then Result.ret ret
+    then Result.ret (betree.List.Cons (i, m) next_msgs, Result.ret)
     else
       do
-        let next_msgs0 ←
-          betree.Node.lookup_first_message_for_key_back key next_msgs ret
-        Result.ret (betree.List.Cons (i, m) next_msgs0)
-  | betree.List.Nil => Result.ret ret
+      let (l, lookup_first_message_for_key_back) ←
+        betree.Node.lookup_first_message_for_key key next_msgs
+      let back_'a :=
+        fun ret =>
+          do
+          let next_msgs1 ← lookup_first_message_for_key_back ret
+          Result.ret (betree.List.Cons (i, m) next_msgs1)
+      Result.ret (l, back_'a)
+  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]: forward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_in_bindings]:
    Source: 'src/betree.rs', lines 636:4-636:80 -/
 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
+    let (i, i1) := hd
     if i = key
-    then Result.ret (some i0)
+    then Result.ret (some i1)
     else
       if i > key
       then Result.ret none
       else betree.Node.lookup_in_bindings key tl
   | betree.List.Nil => Result.ret none
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: forward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]:
    Source: 'src/betree.rs', lines 819:4-819:90 -/
 divergent def betree.Node.apply_upserts
   (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
   (st : State) :
-  Result (State × U64)
+  Result (State × (U64 × (betree.List (U64 × betree.Message))))
   :=
   do
-    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
-    if b
-    then
-      do
-        let msg ← betree.List.pop_front (U64 × betree.Message) msgs
-        let (_, m) := msg
-        match m with
-        | betree.Message.Insert i => Result.fail .panic
-        | betree.Message.Delete => Result.fail .panic
-        | betree.Message.Upsert s =>
-          do
-            let v ← betree.upsert_update prev s
-            let msgs0 ←
-              betree.List.pop_front_back (U64 × betree.Message) msgs
-            betree.Node.apply_upserts msgs0 (some v) key st
-    else
-      do
-        let (st0, v) ← core.option.Option.unwrap U64 prev st
-        let _ ←
-          betree.List.push_front (U64 × betree.Message) msgs (key,
-            betree.Message.Insert v)
-        Result.ret (st0, v)
-
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_upserts]: backward function 0
-   Source: 'src/betree.rs', lines 819:4-819:90 -/
-divergent def betree.Node.apply_upserts_back
-  (msgs : betree.List (U64 × betree.Message)) (prev : Option U64) (key : U64)
-  (st : State) :
-  Result (betree.List (U64 × betree.Message))
-  :=
-  do
-    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
-    if b
-    then
-      do
-        let msg ← betree.List.pop_front (U64 × betree.Message) msgs
-        let (_, m) := msg
-        match m with
-        | betree.Message.Insert i => Result.fail .panic
-        | betree.Message.Delete => Result.fail .panic
-        | betree.Message.Upsert s =>
-          do
-            let v ← betree.upsert_update prev s
-            let msgs0 ←
-              betree.List.pop_front_back (U64 × betree.Message) msgs
-            betree.Node.apply_upserts_back msgs0 (some v) key st
-    else
+  let b ← betree.ListTupleU64T.head_has_key betree.Message msgs key
+  if b
+  then
+    do
+    let (msg, l) ← betree.List.pop_front (U64 × betree.Message) msgs
+    let (_, m) := msg
+    match m with
+    | betree.Message.Insert _ => Result.fail .panic
+    | betree.Message.Delete => Result.fail .panic
+    | betree.Message.Upsert s =>
       do
-        let (_, v) ← core.option.Option.unwrap U64 prev st
-        betree.List.push_front (U64 × betree.Message) msgs (key,
-          betree.Message.Insert v)
+      let v ← betree.upsert_update prev s
+      betree.Node.apply_upserts l (some v) key st
+  else
+    do
+    let (st1, v) ← core.option.Option.unwrap U64 prev st
+    let l ←
+      betree.List.push_front (U64 × betree.Message) msgs (key,
+        betree.Message.Insert v)
+    Result.ret (st1, (v, l))
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]: forward function
+/- [betree_main::betree::{betree_main::betree::Internal#4}::lookup_in_children]:
    Source: 'src/betree.rs', lines 395:4-395:63 -/
 mutual divergent def betree.Internal.lookup_in_children
   (self : betree.Internal) (key : U64) (st : State) :
-  Result (State × (Option U64))
+  Result (State × ((Option U64) × betree.Internal))
   :=
-  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::{betree_main::betree::Internal#4}::lookup_in_children]: backward function 0
-   Source: 'src/betree.rs', lines 395:4-395:63 -/
-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
+  let ⟨ i, i1, n, n1 ⟩ := self
+  if key < i1
   then
     do
-      let n1 ← betree.Node.lookup_back n key st
-      Result.ret (betree.Internal.mk i i0 n1 n0)
+    let (st1, (o, n2)) ← betree.Node.lookup n key st
+    Result.ret (st1, (o, betree.Internal.mk i i1 n2 n1))
   else
     do
-      let n1 ← betree.Node.lookup_back n0 key st
-      Result.ret (betree.Internal.mk i i0 n n1)
+    let (st1, (o, n2)) ← betree.Node.lookup n1 key st
+    Result.ret (st1, (o, betree.Internal.mk i i1 n n2))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: forward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]:
    Source: 'src/betree.rs', lines 709:4-709:58 -/
 divergent def betree.Node.lookup
   (self : betree.Node) (key : U64) (st : State) :
-  Result (State × (Option U64))
+  Result (State × ((Option U64) × betree.Node))
   :=
   match self with
   | betree.Node.Internal node =>
     do
-      let ⟨ i, i0, n, n0 ⟩ := node
-      let (st0, msgs) ← betree.load_internal_node i st
-      let pending ← betree.Node.lookup_first_message_for_key key msgs
-      match pending with
-      | betree.List.Cons p l =>
-        let (k, msg) := p
-        if k != key
-        then
-          do
-            let (st1, o) ←
-              betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0)
-                key st0
-            let _ ←
-              betree.Node.lookup_first_message_for_key_back key msgs
-                (betree.List.Cons (k, msg) l)
-            Result.ret (st1, o)
-        else
-          match msg with
-          | betree.Message.Insert v =>
-            do
-              let _ ←
-                betree.Node.lookup_first_message_for_key_back key msgs
-                  (betree.List.Cons (k, betree.Message.Insert v) l)
-              Result.ret (st0, some v)
-          | betree.Message.Delete =>
-            do
-              let _ ←
-                betree.Node.lookup_first_message_for_key_back key msgs
-                  (betree.List.Cons (k, betree.Message.Delete) l)
-              Result.ret (st0, none)
-          | betree.Message.Upsert ufs =>
-            do
-              let (st1, v) ←
-                betree.Internal.lookup_in_children (betree.Internal.mk i i0 n
-                  n0) key st0
-              let (st2, v0) ←
-                betree.Node.apply_upserts (betree.List.Cons (k,
-                  betree.Message.Upsert ufs) l) v key st1
-              let node0 ←
-                betree.Internal.lookup_in_children_back (betree.Internal.mk i
-                  i0 n n0) key st0
-              let ⟨ i1, _, _, _ ⟩ := node0
-              let pending0 ←
-                betree.Node.apply_upserts_back (betree.List.Cons (k,
-                  betree.Message.Upsert ufs) l) v key st1
-              let msgs0 ←
-                betree.Node.lookup_first_message_for_key_back key msgs pending0
-              let (st3, _) ← betree.store_internal_node i1 msgs0 st2
-              Result.ret (st3, some v0)
-      | betree.List.Nil =>
+    let ⟨ i, i1, n, n1 ⟩ := node
+    let (st1, msgs) ← betree.load_internal_node i st
+    let (pending, lookup_first_message_for_key_back) ←
+      betree.Node.lookup_first_message_for_key key msgs
+    match pending with
+    | betree.List.Cons p l =>
+      let (k, msg) := p
+      if k != key
+      then
         do
-          let (st1, o) ←
-            betree.Internal.lookup_in_children (betree.Internal.mk i i0 n n0)
-              key st0
+        let (st2, (o, i2)) ←
+          betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
+            st1
+        let _ ←
+          lookup_first_message_for_key_back (betree.List.Cons (k, msg) l)
+        Result.ret (st2, (o, betree.Node.Internal i2))
+      else
+        match msg with
+        | betree.Message.Insert v =>
+          do
           let _ ←
-            betree.Node.lookup_first_message_for_key_back key msgs
-              betree.List.Nil
-          Result.ret (st1, o)
-  | betree.Node.Leaf node =>
-    do
-      let (st0, bindings) ← betree.load_leaf_node node.id st
-      let o ← betree.Node.lookup_in_bindings key bindings
-      Result.ret (st0, o)
-
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup]: backward function 0
-   Source: 'src/betree.rs', lines 709:4-709:58 -/
-divergent def betree.Node.lookup_back
-  (self : betree.Node) (key : U64) (st : State) : Result betree.Node :=
-  match self with
-  | betree.Node.Internal node =>
-    do
-      let ⟨ i, i0, n, n0 ⟩ := node
-      let (st0, msgs) ← betree.load_internal_node i st
-      let pending ← betree.Node.lookup_first_message_for_key key msgs
-      match pending with
-      | betree.List.Cons p l =>
-        let (k, msg) := p
-        if k != key
-        then
+            lookup_first_message_for_key_back (betree.List.Cons (k,
+              betree.Message.Insert v) l)
+          Result.ret (st1, (some v, betree.Node.Internal (betree.Internal.mk i
+            i1 n n1)))
+        | betree.Message.Delete =>
           do
-            let _ ←
-              betree.Node.lookup_first_message_for_key_back key msgs
-                (betree.List.Cons (k, msg) l)
-            let node0 ←
-              betree.Internal.lookup_in_children_back (betree.Internal.mk i i0
-                n n0) key st0
-            Result.ret (betree.Node.Internal node0)
-        else
-          match msg with
-          | betree.Message.Insert v =>
-            do
-              let _ ←
-                betree.Node.lookup_first_message_for_key_back key msgs
-                  (betree.List.Cons (k, betree.Message.Insert v) l)
-              Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0))
-          | betree.Message.Delete =>
-            do
-              let _ ←
-                betree.Node.lookup_first_message_for_key_back key msgs
-                  (betree.List.Cons (k, betree.Message.Delete) l)
-              Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0))
-          | betree.Message.Upsert ufs =>
-            do
-              let (st1, v) ←
-                betree.Internal.lookup_in_children (betree.Internal.mk i i0 n
-                  n0) key st0
-              let (st2, _) ←
-                betree.Node.apply_upserts (betree.List.Cons (k,
-                  betree.Message.Upsert ufs) l) v key st1
-              let node0 ←
-                betree.Internal.lookup_in_children_back (betree.Internal.mk i
-                  i0 n n0) key st0
-              let ⟨ i1, i2, n1, n2 ⟩ := node0
-              let pending0 ←
-                betree.Node.apply_upserts_back (betree.List.Cons (k,
-                  betree.Message.Upsert ufs) l) v key st1
-              let msgs0 ←
-                betree.Node.lookup_first_message_for_key_back key msgs pending0
-              let _ ← betree.store_internal_node i1 msgs0 st2
-              Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1
-                n2))
-      | betree.List.Nil =>
-        do
           let _ ←
-            betree.Node.lookup_first_message_for_key_back key msgs
-              betree.List.Nil
-          let node0 ←
-            betree.Internal.lookup_in_children_back (betree.Internal.mk i i0 n
-              n0) key st0
-          Result.ret (betree.Node.Internal node0)
+            lookup_first_message_for_key_back (betree.List.Cons (k,
+              betree.Message.Delete) l)
+          Result.ret (st1, (none, betree.Node.Internal (betree.Internal.mk i i1
+            n n1)))
+        | betree.Message.Upsert ufs =>
+          do
+          let (st2, (v, i2)) ←
+            betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1)
+              key st1
+          let (st3, (v1, l1)) ←
+            betree.Node.apply_upserts (betree.List.Cons (k,
+              betree.Message.Upsert ufs) l) v key st2
+          let ⟨ i3, i4, n2, n3 ⟩ := i2
+          let msgs1 ← lookup_first_message_for_key_back l1
+          let (st4, _) ← betree.store_internal_node i3 msgs1 st3
+          Result.ret (st4, (some v1, betree.Node.Internal (betree.Internal.mk
+            i3 i4 n2 n3)))
+    | betree.List.Nil =>
+      do
+      let (st2, (o, i2)) ←
+        betree.Internal.lookup_in_children (betree.Internal.mk i i1 n n1) key
+          st1
+      let _ ← lookup_first_message_for_key_back betree.List.Nil
+      Result.ret (st2, (o, betree.Node.Internal i2))
   | betree.Node.Leaf node =>
     do
-      let (_, bindings) ← betree.load_leaf_node node.id st
-      let _ ← betree.Node.lookup_in_bindings key bindings
-      Result.ret (betree.Node.Leaf node)
+    let (st1, bindings) ← betree.load_leaf_node node.id st
+    let o ← betree.Node.lookup_in_bindings key bindings
+    Result.ret (st1, (o, betree.Node.Leaf node))
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ())
+/- [betree_main::betree::{betree_main::betree::Node#5}::filter_messages_for_key]:
    Source: 'src/betree.rs', lines 674:4-674:77 -/
 divergent def betree.Node.filter_messages_for_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
@@ -517,33 +346,19 @@ divergent def betree.Node.filter_messages_for_key
     if k = key
     then
       do
-        let msgs0 ←
-          betree.List.pop_front_back (U64 × betree.Message) (betree.List.Cons
-            (k, m) l)
-        betree.Node.filter_messages_for_key key msgs0
+      let (_, l1) ←
+        betree.List.pop_front (U64 × betree.Message) (betree.List.Cons (k, m)
+          l)
+      betree.Node.filter_messages_for_key key l1
     else Result.ret (betree.List.Cons (k, m) l)
   | betree.List.Nil => Result.ret betree.List.Nil
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: forward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]:
    Source: 'src/betree.rs', lines 689:4-692:34 -/
 divergent def betree.Node.lookup_first_message_after_key
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
-  Result (betree.List (U64 × betree.Message))
-  :=
-  match msgs with
-  | betree.List.Cons p next_msgs =>
-    let (k, m) := p
-    if k = key
-    then betree.Node.lookup_first_message_after_key key next_msgs
-    else Result.ret (betree.List.Cons (k, m) next_msgs)
-  | betree.List.Nil => Result.ret betree.List.Nil
-
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_first_message_after_key]: backward function 0
-   Source: 'src/betree.rs', lines 689:4-692:34 -/
-divergent def betree.Node.lookup_first_message_after_key_back
-  (key : U64) (msgs : betree.List (U64 × betree.Message))
-  (ret : betree.List (U64 × betree.Message)) :
-  Result (betree.List (U64 × betree.Message))
+  Result ((betree.List (U64 × betree.Message)) × (betree.List (U64 ×
+    betree.Message) → Result (betree.List (U64 × betree.Message))))
   :=
   match msgs with
   | betree.List.Cons p next_msgs =>
@@ -551,14 +366,18 @@ divergent def betree.Node.lookup_first_message_after_key_back
     if k = key
     then
       do
-        let next_msgs0 ←
-          betree.Node.lookup_first_message_after_key_back key next_msgs ret
-        Result.ret (betree.List.Cons (k, m) next_msgs0)
-    else Result.ret ret
-  | betree.List.Nil => Result.ret ret
+      let (l, lookup_first_message_after_key_back) ←
+        betree.Node.lookup_first_message_after_key key next_msgs
+      let back_'a :=
+        fun ret =>
+          do
+          let next_msgs1 ← lookup_first_message_after_key_back ret
+          Result.ret (betree.List.Cons (k, m) next_msgs1)
+      Result.ret (l, back_'a)
+    else Result.ret (betree.List.Cons (k, m) next_msgs, Result.ret)
+  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ())
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_internal]:
    Source: 'src/betree.rs', lines 521:4-521:89 -/
 def betree.Node.apply_to_internal
   (msgs : betree.List (U64 × betree.Message)) (key : U64)
@@ -566,66 +385,63 @@ def betree.Node.apply_to_internal
   Result (betree.List (U64 × betree.Message))
   :=
   do
-    let msgs0 ← betree.Node.lookup_first_message_for_key key msgs
-    let b ← betree.ListTupleU64T.head_has_key betree.Message msgs0 key
-    if b
-    then
-      match new_msg with
-      | betree.Message.Insert i =>
+  let (msgs1, lookup_first_message_for_key_back) ←
+    betree.Node.lookup_first_message_for_key key msgs
+  let b ← betree.ListTupleU64T.head_has_key betree.Message msgs1 key
+  if b
+  then
+    match new_msg with
+    | betree.Message.Insert i =>
+      do
+      let l ← betree.Node.filter_messages_for_key key msgs1
+      let l1 ←
+        betree.List.push_front (U64 × betree.Message) l (key,
+          betree.Message.Insert i)
+      lookup_first_message_for_key_back l1
+    | betree.Message.Delete =>
+      do
+      let l ← betree.Node.filter_messages_for_key key msgs1
+      let l1 ←
+        betree.List.push_front (U64 × betree.Message) l (key,
+          betree.Message.Delete)
+      lookup_first_message_for_key_back l1
+    | betree.Message.Upsert s =>
+      do
+      let p ← betree.List.hd (U64 × betree.Message) msgs1
+      let (_, m) := p
+      match m with
+      | betree.Message.Insert prev =>
         do
-          let msgs1 ← betree.Node.filter_messages_for_key key msgs0
-          let msgs2 ←
-            betree.List.push_front (U64 × betree.Message) msgs1 (key,
-              betree.Message.Insert i)
-          betree.Node.lookup_first_message_for_key_back key msgs msgs2
+        let v ← betree.upsert_update (some prev) s
+        let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1
+        let l1 ←
+          betree.List.push_front (U64 × betree.Message) l (key,
+            betree.Message.Insert v)
+        lookup_first_message_for_key_back l1
       | betree.Message.Delete =>
         do
-          let msgs1 ← betree.Node.filter_messages_for_key key msgs0
-          let msgs2 ←
-            betree.List.push_front (U64 × betree.Message) msgs1 (key,
-              betree.Message.Delete)
-          betree.Node.lookup_first_message_for_key_back key msgs msgs2
-      | betree.Message.Upsert s =>
+        let (_, l) ← betree.List.pop_front (U64 × betree.Message) msgs1
+        let v ← betree.upsert_update none s
+        let l1 ←
+          betree.List.push_front (U64 × betree.Message) l (key,
+            betree.Message.Insert v)
+        lookup_first_message_for_key_back l1
+      | betree.Message.Upsert _ =>
         do
-          let p ← betree.List.hd (U64 × betree.Message) msgs0
-          let (_, m) := p
-          match m with
-          | betree.Message.Insert prev =>
-            do
-              let v ← betree.upsert_update (some prev) s
-              let msgs1 ←
-                betree.List.pop_front_back (U64 × betree.Message) msgs0
-              let msgs2 ←
-                betree.List.push_front (U64 × betree.Message) msgs1 (key,
-                  betree.Message.Insert v)
-              betree.Node.lookup_first_message_for_key_back key msgs msgs2
-          | betree.Message.Delete =>
-            do
-              let v ← betree.upsert_update none s
-              let msgs1 ←
-                betree.List.pop_front_back (U64 × betree.Message) msgs0
-              let msgs2 ←
-                betree.List.push_front (U64 × betree.Message) msgs1 (key,
-                  betree.Message.Insert v)
-              betree.Node.lookup_first_message_for_key_back key msgs msgs2
-          | betree.Message.Upsert ufs =>
-            do
-              let msgs1 ←
-                betree.Node.lookup_first_message_after_key key msgs0
-              let msgs2 ←
-                betree.List.push_front (U64 × betree.Message) msgs1 (key,
-                  betree.Message.Upsert s)
-              let msgs3 ←
-                betree.Node.lookup_first_message_after_key_back key msgs0 msgs2
-              betree.Node.lookup_first_message_for_key_back key msgs msgs3
-    else
-      do
-        let msgs1 ←
-          betree.List.push_front (U64 × betree.Message) msgs0 (key, new_msg)
-        betree.Node.lookup_first_message_for_key_back key msgs msgs1
+        let (msgs2, lookup_first_message_after_key_back) ←
+          betree.Node.lookup_first_message_after_key key msgs1
+        let l ←
+          betree.List.push_front (U64 × betree.Message) msgs2 (key,
+            betree.Message.Upsert s)
+        let msgs3 ← lookup_first_message_after_key_back l
+        lookup_first_message_for_key_back msgs3
+  else
+    do
+    let l ←
+      betree.List.push_front (U64 × betree.Message) msgs1 (key, new_msg)
+    lookup_first_message_for_key_back l
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ())
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_internal]:
    Source: 'src/betree.rs', lines 502:4-505:5 -/
 divergent def betree.Node.apply_messages_to_internal
   (msgs : betree.List (U64 × betree.Message))
@@ -635,45 +451,36 @@ divergent def betree.Node.apply_messages_to_internal
   match new_msgs with
   | betree.List.Cons new_msg new_msgs_tl =>
     do
-      let (i, m) := new_msg
-      let msgs0 ← betree.Node.apply_to_internal msgs i m
-      betree.Node.apply_messages_to_internal msgs0 new_msgs_tl
+    let (i, m) := new_msg
+    let l ← betree.Node.apply_to_internal msgs i m
+    betree.Node.apply_messages_to_internal l new_msgs_tl
   | betree.List.Nil => Result.ret msgs
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: forward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::lookup_mut_in_bindings]:
    Source: 'src/betree.rs', lines 653:4-656:32 -/
 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::{betree_main::betree::Node#5}::lookup_mut_in_bindings]: backward function 0
-   Source: 'src/betree.rs', lines 653:4-656:32 -/
-divergent def betree.Node.lookup_mut_in_bindings_back
-  (key : U64) (bindings : betree.List (U64 × U64))
-  (ret : betree.List (U64 × U64)) :
-  Result (betree.List (U64 × U64))
+  Result ((betree.List (U64 × U64)) × (betree.List (U64 × U64) → Result
+    (betree.List (U64 × U64))))
   :=
   match bindings with
   | betree.List.Cons hd tl =>
-    let (i, i0) := hd
+    let (i, i1) := hd
     if i >= key
-    then Result.ret ret
+    then Result.ret (betree.List.Cons (i, i1) tl, Result.ret)
     else
       do
-        let tl0 ← betree.Node.lookup_mut_in_bindings_back key tl ret
-        Result.ret (betree.List.Cons (i, i0) tl0)
-  | betree.List.Nil => Result.ret ret
+      let (l, lookup_mut_in_bindings_back) ←
+        betree.Node.lookup_mut_in_bindings key tl
+      let back_'a :=
+        fun ret =>
+          do
+          let tl1 ← lookup_mut_in_bindings_back ret
+          Result.ret (betree.List.Cons (i, i1) tl1)
+      Result.ret (l, back_'a)
+  | betree.List.Nil => Result.ret (betree.List.Nil, Result.ret)
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ())
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_to_leaf]:
    Source: 'src/betree.rs', lines 460:4-460:87 -/
 def betree.Node.apply_to_leaf
   (bindings : betree.List (U64 × U64)) (key : U64) (new_msg : betree.Message)
@@ -681,49 +488,39 @@ def betree.Node.apply_to_leaf
   Result (betree.List (U64 × U64))
   :=
   do
-    let bindings0 ← betree.Node.lookup_mut_in_bindings key bindings
-    let b ← betree.ListTupleU64T.head_has_key U64 bindings0 key
-    if b
-    then
+  let (bindings1, lookup_mut_in_bindings_back) ←
+    betree.Node.lookup_mut_in_bindings key bindings
+  let b ← betree.ListTupleU64T.head_has_key U64 bindings1 key
+  if b
+  then
+    do
+    let (hd, l) ← betree.List.pop_front (U64 × U64) bindings1
+    match new_msg with
+    | betree.Message.Insert v =>
       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 (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 none s
-          let bindings1 ←
-            betree.List.push_front (U64 × U64) bindings0 (key, v)
-          betree.Node.lookup_mut_in_bindings_back key bindings bindings1
+      let l1 ← betree.List.push_front (U64 × U64) l (key, v)
+      lookup_mut_in_bindings_back l1
+    | betree.Message.Delete => lookup_mut_in_bindings_back l
+    | betree.Message.Upsert s =>
+      do
+      let (_, i) := hd
+      let v ← betree.upsert_update (some i) s
+      let l1 ← betree.List.push_front (U64 × U64) l (key, v)
+      lookup_mut_in_bindings_back l1
+  else
+    match new_msg with
+    | betree.Message.Insert v =>
+      do
+      let l ← betree.List.push_front (U64 × U64) bindings1 (key, v)
+      lookup_mut_in_bindings_back l
+    | betree.Message.Delete => lookup_mut_in_bindings_back bindings1
+    | betree.Message.Upsert s =>
+      do
+      let v ← betree.upsert_update none s
+      let l ← betree.List.push_front (U64 × U64) bindings1 (key, v)
+      lookup_mut_in_bindings_back l
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]: merged forward/backward function
-   (there is a single backward function, and the forward function returns ())
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages_to_leaf]:
    Source: 'src/betree.rs', lines 444:4-447:5 -/
 divergent def betree.Node.apply_messages_to_leaf
   (bindings : betree.List (U64 × U64))
@@ -733,337 +530,182 @@ divergent def betree.Node.apply_messages_to_leaf
   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
+    let (i, m) := new_msg
+    let l ← betree.Node.apply_to_leaf bindings i m
+    betree.Node.apply_messages_to_leaf l new_msgs_tl
   | betree.List.Nil => Result.ret bindings
 
-/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]: forward function
+/- [betree_main::betree::{betree_main::betree::Internal#4}::flush]:
    Source: 'src/betree.rs', lines 410:4-415:26 -/
 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)))
+  Result (State × ((betree.List (U64 × betree.Message)) × (betree.Internal
+    × betree.NodeIdCounter)))
   :=
   do
-    let ⟨ _, i, n, n0 ⟩ := self
-    let p ← betree.ListTupleU64T.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
+  let ⟨ i, i1, n, n1 ⟩ := self
+  let p ← betree.ListTupleU64T.partition_at_pivot betree.Message content i1
+  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 (st1, p1) ←
+      betree.Node.apply_messages n params node_id_cnt msgs_left st
+    let (n2, node_id_cnt1) := p1
+    let len_right ← betree.List.len (U64 × betree.Message) msgs_right
+    if len_right >= 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)
+      let (st2, p2) ←
+        betree.Node.apply_messages n1 params node_id_cnt1 msgs_right st1
+      let (n3, node_id_cnt2) := p2
+      Result.ret (st2, (betree.List.Nil, (betree.Internal.mk i i1 n2 n3,
+        node_id_cnt2)))
     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::{betree_main::betree::Internal#4}::flush]: backward function 0
-   Source: 'src/betree.rs', lines 410:4-415:26 -/
-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.ListTupleU64T.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::{betree_main::betree::Node#5}::apply_messages]: forward function
-   Source: 'src/betree.rs', lines 588:4-593:5 -/
-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) :
-  Result (State × Unit)
-  :=
-  match self with
-  | betree.Node.Internal node =>
-    do
-      let ⟨ i, i0, n, n0 ⟩ := node
-      let (st0, content) ← betree.load_internal_node i st
-      let content0 ← betree.Node.apply_messages_to_internal content msgs
-      let num_msgs ← betree.List.len (U64 × betree.Message) content0
-      if num_msgs >= params.min_flush_size
-      then
-        do
-          let (st1, content1) ←
-            betree.Internal.flush (betree.Internal.mk i i0 n n0) params
-              node_id_cnt content0 st0
-          let (node0, _) ←
-            betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params
-              node_id_cnt content0 st0
-          let ⟨ i1, _, _, _ ⟩ := node0
-          let (st2, _) ← betree.store_internal_node i1 content1 st1
-          Result.ret (st2, ())
-      else
-        do
-          let (st1, _) ← betree.store_internal_node i content0 st0
-          Result.ret (st1, ())
-  | betree.Node.Leaf node =>
+      Result.ret (st1, (msgs_right, (betree.Internal.mk i i1 n2 n1,
+        node_id_cnt1)))
+  else
     do
-      let (st0, content) ← betree.load_leaf_node node.id st
-      let content0 ← betree.Node.apply_messages_to_leaf content msgs
-      let len ← betree.List.len (U64 × U64) content0
-      let i ← 2#u64 * params.split_size
-      if len >= i
-      then
-        do
-          let (st1, _) ←
-            betree.Leaf.split node content0 params node_id_cnt st0
-          let (st2, _) ← betree.store_leaf_node node.id betree.List.Nil st1
-          Result.ret (st2, ())
-      else
-        do
-          let (st1, _) ← betree.store_leaf_node node.id content0 st0
-          Result.ret (st1, ())
+    let (st1, p1) ←
+      betree.Node.apply_messages n1 params node_id_cnt msgs_right st
+    let (n2, node_id_cnt1) := p1
+    Result.ret (st1, (msgs_left, (betree.Internal.mk i i1 n n2, node_id_cnt1)))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]: backward function 0
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply_messages]:
    Source: 'src/betree.rs', lines 588:4-593:5 -/
-divergent def betree.Node.apply_messages_back
+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) :
-  Result (betree.Node × betree.NodeIdCounter)
+  Result (State × (betree.Node × betree.NodeIdCounter))
   :=
   match self with
   | betree.Node.Internal node =>
     do
-      let ⟨ i, i0, n, n0 ⟩ := node
-      let (st0, content) ← betree.load_internal_node i st
-      let content0 ← betree.Node.apply_messages_to_internal content msgs
-      let num_msgs ← betree.List.len (U64 × betree.Message) content0
-      if num_msgs >= params.min_flush_size
-      then
-        do
-          let (st1, content1) ←
-            betree.Internal.flush (betree.Internal.mk i i0 n n0) params
-              node_id_cnt content0 st0
-          let (node0, node_id_cnt0) ←
-            betree.Internal.flush_back (betree.Internal.mk i i0 n n0) params
-              node_id_cnt content0 st0
-          let ⟨ i1, i2, n1, n2 ⟩ := node0
-          let _ ← betree.store_internal_node i1 content1 st1
-          Result.ret (betree.Node.Internal (betree.Internal.mk i1 i2 n1 n2),
-            node_id_cnt0)
-      else
-        do
-          let _ ← betree.store_internal_node i content0 st0
-          Result.ret (betree.Node.Internal (betree.Internal.mk i i0 n n0),
-            node_id_cnt)
+    let ⟨ i, i1, n, n1 ⟩ := node
+    let (st1, content) ← betree.load_internal_node i st
+    let l ← betree.Node.apply_messages_to_internal content msgs
+    let num_msgs ← betree.List.len (U64 × betree.Message) l
+    if num_msgs >= params.min_flush_size
+    then
+      do
+      let (st2, (content1, p)) ←
+        betree.Internal.flush (betree.Internal.mk i i1 n n1) params node_id_cnt
+          l st1
+      let (node1, node_id_cnt1) := p
+      let ⟨ i2, i3, n2, n3 ⟩ := node1
+      let (st3, _) ← betree.store_internal_node i2 content1 st2
+      Result.ret (st3, (betree.Node.Internal (betree.Internal.mk i2 i3 n2 n3),
+        node_id_cnt1))
+    else
+      do
+      let (st2, _) ← betree.store_internal_node i l st1
+      Result.ret (st2, (betree.Node.Internal (betree.Internal.mk i i1 n n1),
+        node_id_cnt))
   | betree.Node.Leaf node =>
     do
-      let (st0, content) ← betree.load_leaf_node node.id st
-      let content0 ← betree.Node.apply_messages_to_leaf content msgs
-      let len ← betree.List.len (U64 × U64) content0
-      let i ← 2#u64 * params.split_size
-      if len >= i
-      then
-        do
-          let (st1, new_node) ←
-            betree.Leaf.split node content0 params node_id_cnt st0
-          let _ ← betree.store_leaf_node node.id betree.List.Nil st1
-          let node_id_cnt0 ←
-            betree.Leaf.split_back node content0 params node_id_cnt st0
-          Result.ret (betree.Node.Internal new_node, node_id_cnt0)
-      else
-        do
-          let _ ← betree.store_leaf_node node.id content0 st0
-          Result.ret (betree.Node.Leaf { node with size := len }, node_id_cnt)
+    let (st1, content) ← betree.load_leaf_node node.id st
+    let l ← betree.Node.apply_messages_to_leaf content msgs
+    let len ← betree.List.len (U64 × U64) l
+    let i ← 2#u64 * params.split_size
+    if len >= i
+    then
+      do
+      let (st2, (new_node, nic)) ←
+        betree.Leaf.split node l params node_id_cnt st1
+      let (st3, _) ← betree.store_leaf_node node.id betree.List.Nil st2
+      Result.ret (st3, (betree.Node.Internal new_node, nic))
+    else
+      do
+      let (st2, _) ← betree.store_leaf_node node.id l st1
+      Result.ret (st2, (betree.Node.Leaf { node with size := len },
+        node_id_cnt))
 
 end
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: forward function
+/- [betree_main::betree::{betree_main::betree::Node#5}::apply]:
    Source: 'src/betree.rs', lines 576:4-582:5 -/
 def betree.Node.apply
   (self : betree.Node) (params : betree.Params)
   (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
   (st : State) :
-  Result (State × Unit)
+  Result (State × (betree.Node × betree.NodeIdCounter))
   :=
   do
-    let l := betree.List.Nil
-    let (st0, _) ←
-      betree.Node.apply_messages self params node_id_cnt (betree.List.Cons
-        (key, new_msg) l) st
-    let _ ←
-      betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons
-        (key, new_msg) l) st
-    Result.ret (st0, ())
+  let (st1, p) ←
+    betree.Node.apply_messages self params node_id_cnt (betree.List.Cons (key,
+      new_msg) betree.List.Nil) st
+  let (self1, node_id_cnt1) := p
+  Result.ret (st1, (self1, node_id_cnt1))
 
-/- [betree_main::betree::{betree_main::betree::Node#5}::apply]: backward function 0
-   Source: 'src/betree.rs', lines 576:4-582:5 -/
-def betree.Node.apply_back
-  (self : betree.Node) (params : betree.Params)
-  (node_id_cnt : betree.NodeIdCounter) (key : U64) (new_msg : betree.Message)
-  (st : State) :
-  Result (betree.Node × betree.NodeIdCounter)
-  :=
-  let l := betree.List.Nil
-  betree.Node.apply_messages_back self params node_id_cnt (betree.List.Cons
-    (key, new_msg) l) st
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]: forward function
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::new]:
    Source: 'src/betree.rs', lines 849:4-849:60 -/
 def betree.BeTree.new
   (min_flush_size : U64) (split_size : U64) (st : State) :
   Result (State × betree.BeTree)
   :=
   do
-    let node_id_cnt ← betree.NodeIdCounter.new
-    let id ← betree.NodeIdCounter.fresh_id node_id_cnt
-    let (st0, _) ← betree.store_leaf_node id betree.List.Nil st
-    let node_id_cnt0 ← betree.NodeIdCounter.fresh_id_back node_id_cnt
-    Result.ret (st0,
-      {
-        params :=
-          { min_flush_size := min_flush_size, split_size := split_size },
-        node_id_cnt := node_id_cnt0,
-        root := (betree.Node.Leaf { id := id, size := 0#u64 })
-      })
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: forward function
+  let node_id_cnt ← betree.NodeIdCounter.new
+  let (id, nic) ← betree.NodeIdCounter.fresh_id node_id_cnt
+  let (st1, _) ← betree.store_leaf_node id betree.List.Nil st
+  Result.ret (st1,
+    {
+      params := { min_flush_size := min_flush_size, split_size := split_size },
+      node_id_cnt := nic,
+      root := (betree.Node.Leaf { id := id, size := 0#u64 })
+    })
+
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]:
    Source: 'src/betree.rs', lines 868:4-868:47 -/
 def betree.BeTree.apply
   (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      betree.Node.apply self.root self.params self.node_id_cnt key msg st
-    let _ ←
-      betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::apply]: backward function 0
-   Source: 'src/betree.rs', lines 868:4-868:47 -/
-def betree.BeTree.apply_back
-  (self : betree.BeTree) (key : U64) (msg : betree.Message) (st : State) :
-  Result betree.BeTree
+  Result (State × betree.BeTree)
   :=
   do
-    let (n, nic) ←
-      betree.Node.apply_back self.root self.params self.node_id_cnt key msg st
-    Result.ret { self with node_id_cnt := nic, root := n }
+  let (st1, p) ←
+    betree.Node.apply self.root self.params self.node_id_cnt key msg st
+  let (n, nic) := p
+  Result.ret (st1, { self with node_id_cnt := nic, root := n })
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: forward function
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]:
    Source: 'src/betree.rs', lines 874:4-874:52 -/
 def betree.BeTree.insert
   (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
-  Result (State × Unit)
-  :=
-  do
-    let (st0, _) ←
-      betree.BeTree.apply self key (betree.Message.Insert value) st
-    let _ ←
-      betree.BeTree.apply_back self key (betree.Message.Insert value) st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::insert]: backward function 0
-   Source: 'src/betree.rs', lines 874:4-874:52 -/
-def betree.BeTree.insert_back
-  (self : betree.BeTree) (key : U64) (value : U64) (st : State) :
-  Result betree.BeTree
+  Result (State × betree.BeTree)
   :=
-  betree.BeTree.apply_back self key (betree.Message.Insert value) st
+  betree.BeTree.apply self key (betree.Message.Insert value) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: forward function
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]:
    Source: 'src/betree.rs', lines 880:4-880:38 -/
 def betree.BeTree.delete
-  (self : betree.BeTree) (key : U64) (st : State) : Result (State × Unit) :=
-  do
-    let (st0, _) ← betree.BeTree.apply self key betree.Message.Delete st
-    let _ ← betree.BeTree.apply_back self key betree.Message.Delete st
-    Result.ret (st0, ())
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::delete]: backward function 0
-   Source: 'src/betree.rs', lines 880:4-880:38 -/
-def betree.BeTree.delete_back
-  (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
-  betree.BeTree.apply_back self key betree.Message.Delete st
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: forward function
-   Source: 'src/betree.rs', lines 886:4-886:59 -/
-def betree.BeTree.upsert
-  (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
-  :
-  Result (State × Unit)
+  (self : betree.BeTree) (key : U64) (st : State) :
+  Result (State × betree.BeTree)
   :=
-  do
-    let (st0, _) ←
-      betree.BeTree.apply self key (betree.Message.Upsert upd) st
-    let _ ← betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
-    Result.ret (st0, ())
+  betree.BeTree.apply self key betree.Message.Delete st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]: backward function 0
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::upsert]:
    Source: 'src/betree.rs', lines 886:4-886:59 -/
-def betree.BeTree.upsert_back
+def betree.BeTree.upsert
   (self : betree.BeTree) (key : U64) (upd : betree.UpsertFunState) (st : State)
   :
-  Result betree.BeTree
+  Result (State × betree.BeTree)
   :=
-  betree.BeTree.apply_back self key (betree.Message.Upsert upd) st
+  betree.BeTree.apply self key (betree.Message.Upsert upd) st
 
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: forward function
+/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]:
    Source: 'src/betree.rs', lines 895:4-895:62 -/
 def betree.BeTree.lookup
   (self : betree.BeTree) (key : U64) (st : State) :
-  Result (State × (Option U64))
+  Result (State × ((Option U64) × betree.BeTree))
   :=
-  betree.Node.lookup self.root key st
-
-/- [betree_main::betree::{betree_main::betree::BeTree#6}::lookup]: backward function 0
-   Source: 'src/betree.rs', lines 895:4-895:62 -/
-def betree.BeTree.lookup_back
-  (self : betree.BeTree) (key : U64) (st : State) : Result betree.BeTree :=
   do
-    let n ← betree.Node.lookup_back self.root key st
-    Result.ret { self with root := n }
+  let (st1, (o, n)) ← betree.Node.lookup self.root key st
+  Result.ret (st1, (o, { self with root := n }))
 
-/- [betree_main::main]: forward function
+/- [betree_main::main]:
    Source: 'src/betree_main.rs', lines 5:0-5:9 -/
 def main : Result Unit :=
   Result.ret ()