Merge pull request #404 from AeneasVerif/son/update1

Update Charon and fix an issue in `SymbolicToPure.translate_assertion`

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

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

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))

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 *)

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 =

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)))

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 *)

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))

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 -/