From 54ade3fd69310864e123022c6965f713e1c09e73 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 20 Dec 2024 22:38:21 +0100
Subject: [PATCH 1/3] Fix an issue in SymbolicToPure.translate_assertion

---
 src/symbolic/SymbolicToPure.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/symbolic/SymbolicToPure.ml b/src/symbolic/SymbolicToPure.ml
index 3b517edc..3af4084f 100644
--- a/src/symbolic/SymbolicToPure.ml
+++ b/src/symbolic/SymbolicToPure.ml
@@ -3551,7 +3551,7 @@ and translate_assertion (ectx : C.eval_ctx) (v : V.typed_value)
   let func =
     { id = FunOrOp (Fun (Pure Assert)); generics = empty_generic_args }
   in
-  let func_ty = mk_arrow (TLiteral TBool) mk_unit_ty in
+  let func_ty = mk_arrow (TLiteral TBool) (mk_result_ty mk_unit_ty) in
   let func = { e = Qualif func; ty = func_ty } in
   let assertion = mk_apps ctx.span func args in
   mk_let monadic (mk_dummy_pattern mk_unit_ty) assertion next_e

From 584c1a6e88777fd8a5398198725d7103376c3558 Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 20 Dec 2024 22:38:40 +0100
Subject: [PATCH 2/3] Regenerate the tests

---
 tests/coq/betree/Betree_Funs.v                | 66 +++++++++----------
 tests/coq/misc/NoNestedBorrows.v              |  9 +--
 .../fstar/betree/Betree.Clauses.Template.fst  | 16 ++---
 tests/fstar/betree/Betree.Funs.fst            | 48 +++++++-------
 tests/fstar/misc/NoNestedBorrows.fst          |  6 +-
 tests/lean/Betree/Funs.lean                   | 46 ++++++-------
 tests/lean/NoNestedBorrows.lean               | 12 +---
 7 files changed, 97 insertions(+), 106 deletions(-)

diff --git a/tests/coq/betree/Betree_Funs.v b/tests/coq/betree/Betree_Funs.v
index c7c67fa4..f1b7e110 100644
--- a/tests/coq/betree/Betree_Funs.v
+++ b/tests/coq/betree/Betree_Funs.v
@@ -275,6 +275,38 @@ Definition betree_Leaf_split
     node_id_cnt2))
 .
 
+(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
+Fixpoint betree_Node_lookup_in_bindings_loop
+  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+  result (option u64)
+  :=
+  match n with
+  | O => Fail_ OutOfFuel
+  | S n1 =>
+    match bindings with
+    | Betree_List_Cons hd tl =>
+      let (i, i1) := hd in
+      if i s= key
+      then Ok (Some i1)
+      else
+        if i s> key
+        then Ok None
+        else betree_Node_lookup_in_bindings_loop n1 key tl
+    | Betree_List_Nil => Ok None
+    end
+  end
+.
+
+(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]:
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
+Definition betree_Node_lookup_in_bindings
+  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
+  result (option u64)
+  :=
+  betree_Node_lookup_in_bindings_loop n key bindings
+.
+
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: loop 0:
     Source: 'src/betree.rs', lines 796:8-810:5 *)
 Fixpoint betree_Node_lookup_first_message_for_key_loop
@@ -354,38 +386,6 @@ Definition betree_Node_apply_upserts
   betree_Node_apply_upserts_loop n msgs prev key
 .
 
-(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 650:8-660:5 *)
-Fixpoint betree_Node_lookup_in_bindings_loop
-  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
-  result (option u64)
-  :=
-  match n with
-  | O => Fail_ OutOfFuel
-  | S n1 =>
-    match bindings with
-    | Betree_List_Cons hd tl =>
-      let (i, i1) := hd in
-      if i s= key
-      then Ok (Some i1)
-      else
-        if i s> key
-        then Ok None
-        else betree_Node_lookup_in_bindings_loop n1 key tl
-    | Betree_List_Nil => Ok None
-    end
-  end
-.
-
-(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]:
-    Source: 'src/betree.rs', lines 649:4-660:5 *)
-Definition betree_Node_lookup_in_bindings
-  (n : nat) (key : u64) (bindings : betree_List_t (u64 * u64)) :
-  result (option u64)
-  :=
-  betree_Node_lookup_in_bindings_loop n key bindings
-.
-
 (** [betree::betree::{betree::betree::Internal}#4::lookup_in_children]:
     Source: 'src/betree.rs', lines 414:4-420:5 *)
 Fixpoint betree_Internal_lookup_in_children
@@ -466,7 +466,7 @@ with betree_Node_lookup
 .
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 684:8-691:9 *)
+    Source: 'src/betree.rs', lines 684:8-692:5 *)
 Fixpoint betree_Node_filter_messages_for_key_loop
   (n : nat) (key : u64) (msgs : betree_List_t (u64 * betree_Message_t)) :
   result (betree_List_t (u64 * betree_Message_t))
diff --git a/tests/coq/misc/NoNestedBorrows.v b/tests/coq/misc/NoNestedBorrows.v
index c36d2791..f7afa577 100644
--- a/tests/coq/misc/NoNestedBorrows.v
+++ b/tests/coq/misc/NoNestedBorrows.v
@@ -157,20 +157,17 @@ Definition copy_int (x : i32) : result i32 :=
 (** [no_nested_borrows::test_unreachable]:
     Source: 'tests/src/no_nested_borrows.rs', lines 145:0-149:1 *)
 Definition test_unreachable (b : bool) : result unit :=
-  if b then Fail_ Failure else Ok tt
-.
+  massert b.
 
 (** [no_nested_borrows::test_panic]:
     Source: 'tests/src/no_nested_borrows.rs', lines 152:0-156:1 *)
 Definition test_panic (b : bool) : result unit :=
-  if b then Fail_ Failure else Ok tt
-.
+  massert b.
 
 (** [no_nested_borrows::test_panic_msg]:
     Source: 'tests/src/no_nested_borrows.rs', lines 160:0-164:1 *)
 Definition test_panic_msg (b : bool) : result unit :=
-  if b then Fail_ Failure else Ok tt
-.
+  massert b.
 
 (** [no_nested_borrows::test_copy_int]:
     Source: 'tests/src/no_nested_borrows.rs', lines 167:0-172:1 *)
diff --git a/tests/fstar/betree/Betree.Clauses.Template.fst b/tests/fstar/betree/Betree.Clauses.Template.fst
index 648cd72b..cc52428b 100644
--- a/tests/fstar/betree/Betree.Clauses.Template.fst
+++ b/tests/fstar/betree/Betree.Clauses.Template.fst
@@ -35,6 +35,13 @@ let betree_ListPairU64T_partition_at_pivot_loop_decreases (#t : Type0)
   (end1 : betree_List_t (u64 & t)) (self : betree_List_t (u64 & t)) : nat =
   admit ()
 
+(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: decreases clause
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
+unfold
+let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
+  (bindings : betree_List_t (u64 & u64)) : nat =
+  admit ()
+
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: decreases clause
     Source: 'src/betree.rs', lines 796:8-810:5 *)
 unfold
@@ -50,13 +57,6 @@ let betree_Node_apply_upserts_loop_decreases
   (key : u64) : nat =
   admit ()
 
-(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: decreases clause
-    Source: 'src/betree.rs', lines 650:8-660:5 *)
-unfold
-let betree_Node_lookup_in_bindings_loop_decreases (key : u64)
-  (bindings : betree_List_t (u64 & u64)) : nat =
-  admit ()
-
 (** [betree::betree::{betree::betree::Internal}#4::lookup_in_children]: decreases clause
     Source: 'src/betree.rs', lines 414:4-420:5 *)
 unfold
@@ -72,7 +72,7 @@ let betree_Node_lookup_decreases (self : betree_Node_t) (key : u64)
   admit ()
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: decreases clause
-    Source: 'src/betree.rs', lines 684:8-691:9 *)
+    Source: 'src/betree.rs', lines 684:8-692:5 *)
 unfold
 let betree_Node_filter_messages_for_key_loop_decreases (key : u64)
   (msgs : betree_List_t (u64 & betree_Message_t)) : nat =
diff --git a/tests/fstar/betree/Betree.Funs.fst b/tests/fstar/betree/Betree.Funs.fst
index d7556f98..18122a3f 100644
--- a/tests/fstar/betree/Betree.Funs.fst
+++ b/tests/fstar/betree/Betree.Funs.fst
@@ -224,6 +224,29 @@ let betree_Leaf_split
   let n1 = Betree_Node_Leaf { id = id1; size = params.split_size } in
   Ok (st2, ({ id = self.id; pivot; left = n; right = n1 }, node_id_cnt2))
 
+(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
+    Source: 'src/betree.rs', lines 650:8-660:5 *)
+let rec betree_Node_lookup_in_bindings_loop
+  (key : u64) (bindings : betree_List_t (u64 & u64)) :
+  Tot (result (option u64))
+  (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings))
+  =
+  begin match bindings with
+  | Betree_List_Cons hd tl ->
+    let (i, i1) = hd in
+    if i = key
+    then Ok (Some i1)
+    else
+      if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl
+  | Betree_List_Nil -> Ok None
+  end
+
+(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]:
+    Source: 'src/betree.rs', lines 649:4-660:5 *)
+let betree_Node_lookup_in_bindings
+  (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) =
+  betree_Node_lookup_in_bindings_loop key bindings
+
 (** [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: loop 0:
     Source: 'src/betree.rs', lines 796:8-810:5 *)
 let rec betree_Node_lookup_first_message_for_key_loop
@@ -292,29 +315,6 @@ let betree_Node_apply_upserts
   =
   betree_Node_apply_upserts_loop msgs prev key
 
-(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-    Source: 'src/betree.rs', lines 650:8-660:5 *)
-let rec betree_Node_lookup_in_bindings_loop
-  (key : u64) (bindings : betree_List_t (u64 & u64)) :
-  Tot (result (option u64))
-  (decreases (betree_Node_lookup_in_bindings_loop_decreases key bindings))
-  =
-  begin match bindings with
-  | Betree_List_Cons hd tl ->
-    let (i, i1) = hd in
-    if i = key
-    then Ok (Some i1)
-    else
-      if i > key then Ok None else betree_Node_lookup_in_bindings_loop key tl
-  | Betree_List_Nil -> Ok None
-  end
-
-(** [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]:
-    Source: 'src/betree.rs', lines 649:4-660:5 *)
-let betree_Node_lookup_in_bindings
-  (key : u64) (bindings : betree_List_t (u64 & u64)) : result (option u64) =
-  betree_Node_lookup_in_bindings_loop key bindings
-
 (** [betree::betree::{betree::betree::Internal}#4::lookup_in_children]:
     Source: 'src/betree.rs', lines 414:4-420:5 *)
 let rec betree_Internal_lookup_in_children
@@ -374,7 +374,7 @@ and betree_Node_lookup
   end
 
 (** [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-    Source: 'src/betree.rs', lines 684:8-691:9 *)
+    Source: 'src/betree.rs', lines 684:8-692:5 *)
 let rec betree_Node_filter_messages_for_key_loop
   (key : u64) (msgs : betree_List_t (u64 & betree_Message_t)) :
   Tot (result (betree_List_t (u64 & betree_Message_t)))
diff --git a/tests/fstar/misc/NoNestedBorrows.fst b/tests/fstar/misc/NoNestedBorrows.fst
index 45ea814a..8912d770 100644
--- a/tests/fstar/misc/NoNestedBorrows.fst
+++ b/tests/fstar/misc/NoNestedBorrows.fst
@@ -132,17 +132,17 @@ let copy_int (x : i32) : result i32 =
 (** [no_nested_borrows::test_unreachable]:
     Source: 'tests/src/no_nested_borrows.rs', lines 145:0-149:1 *)
 let test_unreachable (b : bool) : result unit =
-  if b then Fail Failure else Ok ()
+  massert b
 
 (** [no_nested_borrows::test_panic]:
     Source: 'tests/src/no_nested_borrows.rs', lines 152:0-156:1 *)
 let test_panic (b : bool) : result unit =
-  if b then Fail Failure else Ok ()
+  massert b
 
 (** [no_nested_borrows::test_panic_msg]:
     Source: 'tests/src/no_nested_borrows.rs', lines 160:0-164:1 *)
 let test_panic_msg (b : bool) : result unit =
-  if b then Fail Failure else Ok ()
+  massert b
 
 (** [no_nested_borrows::test_copy_int]:
     Source: 'tests/src/no_nested_borrows.rs', lines 167:0-172:1 *)
diff --git a/tests/lean/Betree/Funs.lean b/tests/lean/Betree/Funs.lean
index 97bfbab9..089bb01b 100644
--- a/tests/lean/Betree/Funs.lean
+++ b/tests/lean/Betree/Funs.lean
@@ -225,6 +225,28 @@ def betree.Leaf.split
   let n1 := betree.Node.Leaf { id := id1, size := params.split_size }
   Result.ok (st2, (betree.Internal.mk self.id pivot n n1, node_id_cnt2))
 
+/- [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
+   Source: 'src/betree.rs', lines 650:8-660:5 -/
+divergent def betree.Node.lookup_in_bindings_loop
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  match bindings with
+  | betree.List.Cons hd tl =>
+    let (i, i1) := hd
+    if i = key
+    then Result.ok (some i1)
+    else
+      if i > key
+      then Result.ok none
+      else betree.Node.lookup_in_bindings_loop key tl
+  | betree.List.Nil => Result.ok none
+
+/- [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]:
+   Source: 'src/betree.rs', lines 649:4-660:5 -/
+@[reducible]
+def betree.Node.lookup_in_bindings
+  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
+  betree.Node.lookup_in_bindings_loop key bindings
+
 /- [betree::betree::{betree::betree::Node}#5::lookup_first_message_for_key]: loop 0:
    Source: 'src/betree.rs', lines 796:8-810:5 -/
 divergent def betree.Node.lookup_first_message_for_key_loop
@@ -294,28 +316,6 @@ def betree.Node.apply_upserts
   :=
   betree.Node.apply_upserts_loop msgs prev key
 
-/- [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]: loop 0:
-   Source: 'src/betree.rs', lines 650:8-660:5 -/
-divergent def betree.Node.lookup_in_bindings_loop
-  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
-  match bindings with
-  | betree.List.Cons hd tl =>
-    let (i, i1) := hd
-    if i = key
-    then Result.ok (some i1)
-    else
-      if i > key
-      then Result.ok none
-      else betree.Node.lookup_in_bindings_loop key tl
-  | betree.List.Nil => Result.ok none
-
-/- [betree::betree::{betree::betree::Node}#5::lookup_in_bindings]:
-   Source: 'src/betree.rs', lines 649:4-660:5 -/
-@[reducible]
-def betree.Node.lookup_in_bindings
-  (key : U64) (bindings : betree.List (U64 × U64)) : Result (Option U64) :=
-  betree.Node.lookup_in_bindings_loop key bindings
-
 /- [betree::betree::{betree::betree::Internal}#4::lookup_in_children]:
    Source: 'src/betree.rs', lines 414:4-420:5 -/
 mutual divergent def betree.Internal.lookup_in_children
@@ -378,7 +378,7 @@ divergent def betree.Node.lookup
 end
 
 /- [betree::betree::{betree::betree::Node}#5::filter_messages_for_key]: loop 0:
-   Source: 'src/betree.rs', lines 684:8-691:9 -/
+   Source: 'src/betree.rs', lines 684:8-692:5 -/
 divergent def betree.Node.filter_messages_for_key_loop
   (key : U64) (msgs : betree.List (U64 × betree.Message)) :
   Result (betree.List (U64 × betree.Message))
diff --git a/tests/lean/NoNestedBorrows.lean b/tests/lean/NoNestedBorrows.lean
index c7c202c4..2319c3ad 100644
--- a/tests/lean/NoNestedBorrows.lean
+++ b/tests/lean/NoNestedBorrows.lean
@@ -148,23 +148,17 @@ def copy_int (x : I32) : Result I32 :=
 /- [no_nested_borrows::test_unreachable]:
    Source: 'tests/src/no_nested_borrows.rs', lines 145:0-149:1 -/
 def test_unreachable (b : Bool) : Result Unit :=
-  if b
-  then Result.fail .panic
-  else Result.ok ()
+  massert b
 
 /- [no_nested_borrows::test_panic]:
    Source: 'tests/src/no_nested_borrows.rs', lines 152:0-156:1 -/
 def test_panic (b : Bool) : Result Unit :=
-  if b
-  then Result.fail .panic
-  else Result.ok ()
+  massert b
 
 /- [no_nested_borrows::test_panic_msg]:
    Source: 'tests/src/no_nested_borrows.rs', lines 160:0-164:1 -/
 def test_panic_msg (b : Bool) : Result Unit :=
-  if b
-  then Result.fail .panic
-  else Result.ok ()
+  massert b
 
 /- [no_nested_borrows::test_copy_int]:
    Source: 'tests/src/no_nested_borrows.rs', lines 167:0-172:1 -/

From 9145ff59f43dc4e224d5d233c18801da21f3122b Mon Sep 17 00:00:00 2001
From: Son Ho <hosonmarc@gmail.com>
Date: Fri, 20 Dec 2024 22:38:47 +0100
Subject: [PATCH 3/3] Update the Charon pin

---
 charon-pin |  2 +-
 flake.lock | 12 ++++++------
 2 files changed, 7 insertions(+), 7 deletions(-)

diff --git a/charon-pin b/charon-pin
index 2d18ef63..df24719b 100644
--- a/charon-pin
+++ b/charon-pin
@@ -1,2 +1,2 @@
 # This is the commit from https://github.com/AeneasVerif/charon that should be used with this version of aeneas.
-4925c99ccab9613d6af784dd52d69fccaf3f5f5d
+945ab5bedea86c1ee7e890f6a896c660744c10b5
diff --git a/flake.lock b/flake.lock
index 04e84738..b07efcab 100644
--- a/flake.lock
+++ b/flake.lock
@@ -9,11 +9,11 @@
         "rust-overlay": "rust-overlay"
       },
       "locked": {
-        "lastModified": 1734535109,
-        "narHash": "sha256-j1kKIeXg0Rl3TTujt60alOflycGyJUPpeDCw37AP15k=",
+        "lastModified": 1734724004,
+        "narHash": "sha256-1dQ35aUZ2P6xIV4k8ueOcY+q7Et6puFccMhJ/0NJWXM=",
         "owner": "aeneasverif",
         "repo": "charon",
-        "rev": "4925c99ccab9613d6af784dd52d69fccaf3f5f5d",
+        "rev": "945ab5bedea86c1ee7e890f6a896c660744c10b5",
         "type": "github"
       },
       "original": {
@@ -177,11 +177,11 @@
         ]
       },
       "locked": {
-        "lastModified": 1734489114,
-        "narHash": "sha256-dKBBZr2pw7KDI/7GeiN5qPccqqtvnK2jqAMcMo4rVvU=",
+        "lastModified": 1734661750,
+        "narHash": "sha256-BI58NBdimxu1lnpOrG9XxBz7Cwqy+qIf99zunWofX5w=",
         "owner": "oxalica",
         "repo": "rust-overlay",
-        "rev": "b2e385f8e5c1d7c0d9ce738d650955c2e94555ae",
+        "rev": "7d3d910d5fd575e6e8c5600d83d54e5c47273bfe",
         "type": "github"
       },
       "original": {