Merge pull request #399 from AeneasVerif/son/borrows

Add support for symbolic values containing mutable borrows

backends/coq/Primitives.v

@@ -507,7 +507,7 @@ Axiom core_isize_max : isize. (** TODO *)
 
 (** Trait declaration: [core::clone::Clone] *)
 Record core_clone_Clone (self : Type) := {
-  clone : self -> result self
+  core_clone_Clone_clone : self -> result self
 }.
 
 Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x.
@@ -525,112 +525,112 @@ Definition core_clone_impls_CloneI64_clone (x : i64) : i64 := x.
 Definition core_clone_impls_CloneI128_clone (x : i128) : i128 := x.
 
 Definition core_clone_CloneUsize : core_clone_Clone usize := {|
-  clone := fun x => Ok (core_clone_impls_CloneUsize_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneUsize_clone x)
 |}.
 
 Definition core_clone_CloneU8 : core_clone_Clone u8 := {|
-  clone := fun x => Ok (core_clone_impls_CloneU8_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneU8_clone x)
 |}.
 
 Definition core_clone_CloneU16 : core_clone_Clone u16 := {|
-  clone := fun x => Ok (core_clone_impls_CloneU16_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneU16_clone x)
 |}.
 
 Definition core_clone_CloneU32 : core_clone_Clone u32 := {|
-  clone := fun x => Ok (core_clone_impls_CloneU32_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneU32_clone x)
 |}.
 
 Definition core_clone_CloneU64 : core_clone_Clone u64 := {|
-  clone := fun x => Ok (core_clone_impls_CloneU64_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneU64_clone x)
 |}.
 
 Definition core_clone_CloneU128 : core_clone_Clone u128 := {|
-  clone := fun x => Ok (core_clone_impls_CloneU128_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneU128_clone x)
 |}.
 
 Definition core_clone_CloneIsize : core_clone_Clone isize := {|
-  clone := fun x => Ok (core_clone_impls_CloneIsize_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneIsize_clone x)
 |}.
 
 Definition core_clone_CloneI8 : core_clone_Clone i8 := {|
-  clone := fun x => Ok (core_clone_impls_CloneI8_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneI8_clone x)
 |}.
 
 Definition core_clone_CloneI16 : core_clone_Clone i16 := {|
-  clone := fun x => Ok (core_clone_impls_CloneI16_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneI16_clone x)
 |}.
 
 Definition core_clone_CloneI32 : core_clone_Clone i32 := {|
-  clone := fun x => Ok (core_clone_impls_CloneI32_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneI32_clone x)
 |}.
 
 Definition core_clone_CloneI64 : core_clone_Clone i64 := {|
-  clone := fun x => Ok (core_clone_impls_CloneI64_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneI64_clone x)
 |}.
 
 Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
-  clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
+  core_clone_Clone_clone := fun x => Ok (core_clone_impls_CloneI128_clone x)
 |}.
 
 Definition core_clone_impls_CloneBool_clone (b : bool) : bool := b.
 
 Definition core_clone_CloneBool : core_clone_Clone bool := {|
-  clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
+  core_clone_Clone_clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
 |}.
 
 Record core_marker_Copy (Self : Type) := mkcore_marker_Copy {
-  coreCloneInst : core_clone_Clone Self;
+  cloneInst : core_clone_Clone Self;
 }.
 
 Arguments mkcore_marker_Copy { _ }.
-Arguments coreCloneInst { _ } _.
+Arguments cloneInst { _ } _.
 
 Definition core_marker_CopyU8 : core_marker_Copy u8 := {|
-  coreCloneInst := core_clone_CloneU8;
+  cloneInst := core_clone_CloneU8;
 |}.
 
 Definition core_marker_CopyU16 : core_marker_Copy u16 := {|
-  coreCloneInst := core_clone_CloneU16;
+  cloneInst := core_clone_CloneU16;
 |}.
 
 Definition core_marker_CopyU32 : core_marker_Copy u32 := {|
-  coreCloneInst := core_clone_CloneU32;
+  cloneInst := core_clone_CloneU32;
 |}.
 
 Definition core_marker_CopyU64 : core_marker_Copy u64 := {|
-  coreCloneInst := core_clone_CloneU64;
+  cloneInst := core_clone_CloneU64;
 |}.
 
 Definition core_marker_CopyU128 : core_marker_Copy u128 := {|
-  coreCloneInst := core_clone_CloneU128;
+  cloneInst := core_clone_CloneU128;
 |}.
 
 Definition core_marker_CopyUsize : core_marker_Copy usize := {|
-  coreCloneInst := core_clone_CloneUsize;
+  cloneInst := core_clone_CloneUsize;
 |}.
 
 Definition core_marker_CopyI8 : core_marker_Copy i8 := {|
-  coreCloneInst := core_clone_CloneI8;
+  cloneInst := core_clone_CloneI8;
 |}.
 
 Definition core_marker_CopyI16 : core_marker_Copy i16 := {|
-  coreCloneInst := core_clone_CloneI16;
+  cloneInst := core_clone_CloneI16;
 |}.
 
 Definition core_marker_CopyI32 : core_marker_Copy i32 := {|
-  coreCloneInst := core_clone_CloneI32;
+  cloneInst := core_clone_CloneI32;
 |}.
 
 Definition core_marker_CopyI64 : core_marker_Copy i64 := {|
-  coreCloneInst := core_clone_CloneI64;
+  cloneInst := core_clone_CloneI64;
 |}.
 
 Definition core_marker_CopyI128 : core_marker_Copy i128 := {|
-  coreCloneInst := core_clone_CloneI128;
+  cloneInst := core_clone_CloneI128;
 |}.
 
 Definition core_marker_CopyIsize : core_marker_Copy isize := {|
-  coreCloneInst := core_clone_CloneIsize;
+  cloneInst := core_clone_CloneIsize;
 |}.
 
 (** [core::option::{core::option::Option<T>}::unwrap] *)

backends/fstar/Primitives.fst

@@ -557,55 +557,55 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
 }
 
 noeq type core_marker_Copy (self : Type0) = {
-  cloneCloneInst : core_clone_Clone self;
+  cloneInst : core_clone_Clone self;
 }
 
 let core_marker_CopyU8 : core_marker_Copy u8 = {
-  cloneCloneInst = core_clone_CloneU8;
+  cloneInst = core_clone_CloneU8;
 }
 
 let core_marker_CopyU16 : core_marker_Copy u16 = {
-  cloneCloneInst = core_clone_CloneU16;
+  cloneInst = core_clone_CloneU16;
 }
 
 let core_marker_CopyU32 : core_marker_Copy u32 = {
-  cloneCloneInst = core_clone_CloneU32;
+  cloneInst = core_clone_CloneU32;
 }
 
 let core_marker_CopyU64 : core_marker_Copy u64 = {
-  cloneCloneInst = core_clone_CloneU64;
+  cloneInst = core_clone_CloneU64;
 }
 
 let core_marker_CopyU128 : core_marker_Copy u128 = {
-  cloneCloneInst = core_clone_CloneU128;
+  cloneInst = core_clone_CloneU128;
 }
 
 let core_marker_CopyUsize : core_marker_Copy usize = {
-  cloneCloneInst = core_clone_CloneUsize;
+  cloneInst = core_clone_CloneUsize;
 }
 
 let core_marker_CopyI8 : core_marker_Copy i8 = {
-  cloneCloneInst = core_clone_CloneI8;
+  cloneInst = core_clone_CloneI8;
 }
 
 let core_marker_CopyI16 : core_marker_Copy i16 = {
-  cloneCloneInst = core_clone_CloneI16;
+  cloneInst = core_clone_CloneI16;
 }
 
 let core_marker_CopyI32 : core_marker_Copy i32 = {
-  cloneCloneInst = core_clone_CloneI32;
+  cloneInst = core_clone_CloneI32;
 }
 
 let core_marker_CopyI64 : core_marker_Copy i64 = {
-  cloneCloneInst = core_clone_CloneI64;
+  cloneInst = core_clone_CloneI64;
 }
 
 let core_marker_CopyI128 : core_marker_Copy i128 = {
-  cloneCloneInst = core_clone_CloneI128;
+  cloneInst = core_clone_CloneI128;
 }
 
 let core_marker_CopyIsize : core_marker_Copy isize = {
-  cloneCloneInst = core_clone_CloneIsize;
+  cloneInst = core_clone_CloneIsize;
 }
 
 (** [core::option::{core::option::Option<T>}::unwrap] *)

backends/lean/Base/List/List.lean

@@ -390,4 +390,13 @@ theorem lookup_not_none_imp_length_pos [BEq α] (l : List (α × β)) (key : α)
 
 end
 
+@[simp]
+theorem list_update_index_eq α [Inhabited α] (x : List α) (i : ℕ) :
+  x.update i (x.index i) = x := by
+  revert i
+  induction x
+  . simp
+  . intro i
+    dcases hi: 0 < i <;> simp_all
+
 end List

backends/lean/Base/Primitives/ArraySlice.lean

@@ -402,6 +402,16 @@ theorem Slice.update_subslice_spec {α : Type u} [Inhabited α] (a : Slice α) (
     have := h2 i (by int_tac) (by int_tac)
     simp [*]
 
+@[simp]
+theorem Array.update_index_eq α n [Inhabited α] (x : Array α n) (i : Usize) :
+  x.update i (x.val.index i.toNat) = x := by
+  simp [Array, Subtype.eq_iff]
+
+@[simp]
+theorem Slice.update_index_eq α [Inhabited α] (x : Slice α) (i : Usize) :
+  x.update i (x.val.index i.toNat) = x := by
+  simp [Slice, Subtype.eq_iff]
+
 /- Trait declaration: [core::slice::index::private_slice_index::Sealed] -/
 structure core.slice.index.private_slice_index.Sealed (Self : Type) where
 

backends/lean/Base/Primitives/Vec.lean

@@ -254,4 +254,9 @@ theorem alloc.vec.Vec.resize_spec {T} (cloneInst : core.clone.Clone T)
   . simp
   . simp [*]
 
+@[simp]
+theorem alloc.vec.Vec.update_index_eq α [Inhabited α] (x : alloc.vec.Vec α) (i : Usize) :
+  x.update i (x.val.index i.toNat) = x := by
+  simp [Vec, Subtype.eq_iff]
+
 end Primitives

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.
-c114a3aabc989b5ea3d72c3eccbde9869834460e
+2909a3c23b1abbc780aad5dca76a0f101fedc6ea

src/Errors.ml

@@ -36,10 +36,10 @@ let push_error (span : Meta.span option) (msg : string) =
   error_list := (span, msg) :: !error_list
 
 (** Register an error, and throw an exception if [throw] is true *)
-let save_error (file : string) (line : int) ?(throw : bool = false)
-    (span : Meta.span option) (msg : string) =
+let save_error (file : string) (line : int) (span : Meta.span option)
+    (msg : string) =
   push_error span msg;
-  if !Config.fail_hard && throw then (
+  if !Config.fail_hard then (
     let msg = format_error_message_with_file_line file line span msg in
     log#serror (msg ^ "\n");
     raise (Failure msg))

src/Translate.ml

@@ -164,6 +164,8 @@ let translate_function_to_pure_aux (trans_ctx : trans_ctx)
       loops = Pure.LoopId.Map.empty;
       mk_return = None;
       mk_panic = None;
+      mut_borrow_to_consumed = BorrowId.Map.empty;
+      var_id_to_default = Pure.VarId.Map.empty;
     }
   in
 

src/extract/Extract.ml

@@ -124,12 +124,19 @@ let extract_adt_g_value (span : Meta.span)
         else ("(", ")")
       in
       F.pp_print_string fmt lb;
+      (* F* doesn't parse lambdas and tuples the same way as other backends: the
+         the consequence is that we need to use more parentheses... *)
+      let inside =
+        match backend () with
+        | FStar -> true
+        | _ -> false
+      in
       let ctx =
         Collections.List.fold_left_link
           (fun () ->
             F.pp_print_string fmt ",";
             F.pp_print_space fmt ())
-          (fun ctx v -> extract_value ctx false v)
+          (fun ctx v -> extract_value ctx inside v)
           ctx field_values
       in
       F.pp_print_string fmt rb;
@@ -773,7 +780,11 @@ and extract_Lambda (span : Meta.span) (ctx : extraction_ctx) (fmt : F.formatter)
   (* Print the lambda - note that there should always be at least one variable *)
   sanity_check __FILE__ __LINE__ (xl <> []) span;
   F.pp_print_string fmt "fun";
-  let with_type = backend () = Coq in
+  let with_type =
+    match backend () with
+    | Coq -> true
+    | _ -> false
+  in
   let ctx =
     List.fold_left
       (fun ctx x ->