Merge pull request #382 from AeneasVerif/son/features

Add some definitions to the standard library

backends/coq/Primitives.v

@@ -510,12 +510,6 @@ Record core_clone_Clone (self : Type) := {
   clone : self -> result self
 }.
 
-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)
-|}.
-
 Definition core_clone_impls_CloneUsize_clone (x : usize) : usize := x.
 Definition core_clone_impls_CloneU8_clone (x : u8) : u8 := x.
 Definition core_clone_impls_CloneU16_clone (x : u16) : u16 := x.
@@ -578,6 +572,67 @@ Definition core_clone_CloneI128 : core_clone_Clone i128 := {|
   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)
+|}.
+
+Record core_marker_Copy (Self : Type) := mkcore_marker_Copy {
+  coreCloneInst : core_clone_Clone Self;
+}.
+
+Arguments mkcore_marker_Copy { _ }.
+Arguments coreCloneInst { _ } _.
+
+Definition core_marker_CopyU8 : core_marker_Copy u8 := {|
+  coreCloneInst := core_clone_CloneU8;
+|}.
+
+Definition core_marker_CopyU16 : core_marker_Copy u16 := {|
+  coreCloneInst := core_clone_CloneU16;
+|}.
+
+Definition core_marker_CopyU32 : core_marker_Copy u32 := {|
+  coreCloneInst := core_clone_CloneU32;
+|}.
+
+Definition core_marker_CopyU64 : core_marker_Copy u64 := {|
+  coreCloneInst := core_clone_CloneU64;
+|}.
+
+Definition core_marker_CopyU128 : core_marker_Copy u128 := {|
+  coreCloneInst := core_clone_CloneU128;
+|}.
+
+Definition core_marker_CopyUsize : core_marker_Copy usize := {|
+  coreCloneInst := core_clone_CloneUsize;
+|}.
+
+Definition core_marker_CopyI8 : core_marker_Copy i8 := {|
+  coreCloneInst := core_clone_CloneI8;
+|}.
+
+Definition core_marker_CopyI16 : core_marker_Copy i16 := {|
+  coreCloneInst := core_clone_CloneI16;
+|}.
+
+Definition core_marker_CopyI32 : core_marker_Copy i32 := {|
+  coreCloneInst := core_clone_CloneI32;
+|}.
+
+Definition core_marker_CopyI64 : core_marker_Copy i64 := {|
+  coreCloneInst := core_clone_CloneI64;
+|}.
+
+Definition core_marker_CopyI128 : core_marker_Copy i128 := {|
+  coreCloneInst := core_clone_CloneI128;
+|}.
+
+Definition core_marker_CopyIsize : core_marker_Copy isize := {|
+  coreCloneInst := core_clone_CloneIsize;
+|}.
+
 (** [core::option::{core::option::Option<T>}::unwrap] *)
 Definition core_option_Option_unwrap {T : Type} (x : option T) : result T :=
   match x with

backends/fstar/Primitives.fst

@@ -556,6 +556,58 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
+noeq type core_marker_Copy (self : Type0) = {
+  cloneCloneInst : core_clone_Clone self;
+}
+
+let core_marker_CopyU8 : core_marker_Copy u8 = {
+  cloneCloneInst = core_clone_CloneU8;
+}
+
+let core_marker_CopyU16 : core_marker_Copy u16 = {
+  cloneCloneInst = core_clone_CloneU16;
+}
+
+let core_marker_CopyU32 : core_marker_Copy u32 = {
+  cloneCloneInst = core_clone_CloneU32;
+}
+
+let core_marker_CopyU64 : core_marker_Copy u64 = {
+  cloneCloneInst = core_clone_CloneU64;
+}
+
+let core_marker_CopyU128 : core_marker_Copy u128 = {
+  cloneCloneInst = core_clone_CloneU128;
+}
+
+let core_marker_CopyUsize : core_marker_Copy usize = {
+  cloneCloneInst = core_clone_CloneUsize;
+}
+
+let core_marker_CopyI8 : core_marker_Copy i8 = {
+  cloneCloneInst = core_clone_CloneI8;
+}
+
+let core_marker_CopyI16 : core_marker_Copy i16 = {
+  cloneCloneInst = core_clone_CloneI16;
+}
+
+let core_marker_CopyI32 : core_marker_Copy i32 = {
+  cloneCloneInst = core_clone_CloneI32;
+}
+
+let core_marker_CopyI64 : core_marker_Copy i64 = {
+  cloneCloneInst = core_clone_CloneI64;
+}
+
+let core_marker_CopyI128 : core_marker_Copy i128 = {
+  cloneCloneInst = core_clone_CloneI128;
+}
+
+let core_marker_CopyIsize : core_marker_Copy isize = {
+  cloneCloneInst = core_clone_CloneIsize;
+}
+
 (** [core::option::{core::option::Option<T>}::unwrap] *)
 let core_option_Option_unwrap (#t : Type0) (x : option t) : result t =
   match x with

backends/lean/Base/Primitives/ArraySlice.lean

@@ -577,4 +577,12 @@ def core.slice.index.SliceIndexUsizeSliceTInst (T : Type) :
   index_mut := core.slice.index.Usize.index_mut
 }
 
+def core.slice.Slice.copy_from_slice {T : Type} (_ : core.marker.Copy T)
+  (s : Slice T) (src: Slice T) : Result (Slice T) :=
+  if s.len = src.len then ok src
+  else fail panic
+
+/- [core::array::TryFromSliceError] -/
+def core.array.TryFromSliceError := ()
+
 end Primitives

backends/lean/Base/Primitives/Core.lean

@@ -53,6 +53,10 @@ def clone.CloneBool : clone.Clone Bool := {
   clone := fun b => ok (clone.impls.CloneBool.clone b)
 }
 
+/- [core::marker::Copy] -/
+structure marker.Copy (Self : Type) where
+  cloneInst : core.clone.Clone Self
+
 /- [core::mem::replace]
 
    This acts like a swap effectively in a functional pure world.
@@ -81,3 +85,69 @@ end core
 @[simp] def core.clone.Clone.clone_from
   {Self : Type} (cloneInst : core.clone.Clone Self) (_self : Self) (source : Self) : Result Self :=
   cloneInst.clone source
+
+/- [core::convert::Into] -/
+structure core.convert.Into (Self : Type) (T : Type) where
+  into : Self → Result T
+
+/- [core::convert::{core::convert::Into<U> for T}::into] -/
+@[reducible, simp]
+def core.convert.IntoFrom.into {T : Type} {U : Type}
+  (fromInst : core.convert.From U T) (x : T) : Result U :=
+  fromInst.from_ x
+
+/- Trait implementation: [core::convert::{core::convert::Into<U> for T}] -/
+@[reducible]
+def core.convert.IntoFrom {T : Type} {U : Type} (fromInst : core.convert.From U T)
+  : core.convert.Into T U := {
+  into := core.convert.IntoFrom.into fromInst
+}
+
+/- [core::convert::{core::convert::From<T> for T}::from] -/
+@[simp] def core.convert.FromSame.from_ {T : Type} (x : T) : T := x
+
+/- [core::convert::{core::convert::From<T> for T}] -/
+@[reducible]
+def core.convert.FromSame (T : Type) : core.convert.From T T := {
+  from_ := fun x => ok (core.convert.FromSame.from_ x)
+}
+
+/- [core::result::Result] -/
+inductive core.result.Result (T : Type) (E : Type) :=
+| Ok : T → core.result.Result T E
+| Err : E → core.result.Result T E
+
+/- [core::fmt::Error] -/
+@[reducible] def core.fmt.Error := Unit
+
+structure core.convert.TryFrom (Self T : Type) where
+  Error : Type
+  try_from : T → Result (core.result.Result Self Error)
+
+structure core.convert.TryInto (Self T : Type) where
+  Error : Type
+  try_into : Self → Result (core.result.Result T Error)
+
+@[reducible, simp]
+def core.convert.TryIntoFrom.try_into {T U : Type} (fromInst : core.convert.TryFrom U T)
+  (x : T) : Result (core.result.Result U fromInst.Error) :=
+  fromInst.try_from x
+
+@[reducible]
+def core.convert.TryIntoFrom {T U : Type} (fromInst : core.convert.TryFrom U T) :
+  core.convert.TryInto T U := {
+  Error := fromInst.Error
+  try_into := core.convert.TryIntoFrom.try_into fromInst
+}
+
+/- TODO: -/
+axiom Formatter : Type
+
+structure core.fmt.Debug (T : Type) where
+  fmt : T → Formatter → Result (Formatter × Formatter → Formatter)
+
+def core.result.Result.unwrap {T E : Type}
+  (_ : core.fmt.Debug T) (e : core.result.Result T E) : Primitives.Result T :=
+  match e with
+  | .Ok x => ok x
+  | .Err _ => fail .panic

backends/lean/Base/Primitives/CoreConvertNum.lean

@@ -296,6 +296,8 @@ def FromI128I128 : core.convert.From I128 I128 := {
   from_ := fun x => ok (num.FromI128I128.from x)
 }
 
+end core.convert
+
 -- to_le_bytes
 def core.num.U8.to_le_bytes (x : U8) : Array U8 1#usize := sorry
 def core.num.U16.to_le_bytes (x : U16) : Array U8 2#usize := sorry
@@ -310,6 +312,18 @@ def core.num.U32.to_be_bytes (x : U32) : Array U8 4#usize := sorry
 def core.num.U64.to_be_bytes (x : U64) : Array U8 8#usize := sorry
 def core.num.U128.to_be_bytes (x : U128) : Array U8 128#usize := sorry
 
-end core.convert
+-- from_le_bytes
+def core.num.U8.from_le_bytes (a : Array U8 1#usize) : U8 := sorry
+def core.num.U16.from_le_bytes (a : Array U8 2#usize) : U16 := sorry
+def core.num.U32.from_le_bytes (a : Array U8 4#usize) : U32 := sorry
+def core.num.U64.from_le_bytes (a : Array U8 8#usize) : U64 := sorry
+def core.num.U128.from_le_bytes (a : Array U8 128#usize) : U128 := sorry
+
+-- from_be_bytes
+def core.num.U8.from_be_bytes (a : Array U8 1#usize) : I8 := sorry
+def core.num.U16.from_be_bytes (a : Array U8 2#usize) : I16 := sorry
+def core.num.U32.from_be_bytes (a : Array U8 4#usize) : I32 := sorry
+def core.num.U64.from_be_bytes (a : Array U8 8#usize) : I64 := sorry
+def core.num.U128.from_be_bytes (a : Array U8 128#usize) : I128 := sorry
 
 end Primitives

backends/lean/Base/Primitives/Scalar.lean

@@ -958,6 +958,66 @@ def core.clone.CloneI128 : core.clone.Clone I128 := {
   clone := fun x => ok (core.clone.impls.CloneI128.clone x)
 }
 
+@[reducible]
+def core.marker.CopyU8 : core.marker.Copy U8 := {
+  cloneInst := core.clone.CloneU8
+}
+
+@[reducible]
+def core.marker.CopyU16 : core.marker.Copy U16 := {
+  cloneInst := core.clone.CloneU16
+}
+
+@[reducible]
+def core.marker.CopyU32 : core.marker.Copy U32 := {
+  cloneInst := core.clone.CloneU32
+}
+
+@[reducible]
+def core.marker.CopyU64 : core.marker.Copy U64 := {
+  cloneInst := core.clone.CloneU64
+}
+
+@[reducible]
+def core.marker.CopyU128 : core.marker.Copy U128 := {
+  cloneInst := core.clone.CloneU128
+}
+
+@[reducible]
+def core.marker.CopyUsize : core.marker.Copy Usize := {
+  cloneInst := core.clone.CloneUsize
+}
+
+@[reducible]
+def core.marker.CopyI8 : core.marker.Copy I8 := {
+  cloneInst := core.clone.CloneI8
+}
+
+@[reducible]
+def core.marker.CopyI16 : core.marker.Copy I16 := {
+  cloneInst := core.clone.CloneI16
+}
+
+@[reducible]
+def core.marker.CopyI32 : core.marker.Copy I32 := {
+  cloneInst := core.clone.CloneI32
+}
+
+@[reducible]
+def core.marker.CopyI64 : core.marker.Copy I64 := {
+  cloneInst := core.clone.CloneI64
+}
+
+@[reducible]
+def core.marker.CopyI128 : core.marker.Copy I128 := {
+  cloneInst := core.clone.CloneI128
+}
+
+@[reducible]
+def core.marker.CopyIsize : core.marker.Copy Isize := {
+  cloneInst := core.clone.CloneIsize
+}
+
 -- This is easier defined this way than with the modulo operation (because of the
 -- unsigned cases).
 def int_overflowing_add (ty : ScalarTy) (x y : Int) : Int × Bool :=

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.
-e6033230aab5cbff5e3840473844e913b59062af
+7744bf94275e2ba3e7a2e4163c1fa062225d7a75

src/Config.ml

@@ -45,6 +45,9 @@ let if_backend (f : unit -> 'a) (default : 'a) : 'a =
   | None -> default
   | Some _ -> f ()
 
+(** Print all the external definitions which are not listed in the builtin functions *)
+let print_unknown_externals = ref false
+
 (** {1 Interpreter} *)
 
 (** Activate the sanity checks, and in particular the invariant checks

src/Errors.ml

@@ -57,6 +57,16 @@ let craise_opt_span (file : string) (line : int) (span : Meta.span option)
 let craise (file : string) (line : int) (span : Meta.span) (msg : string) =
   craise_opt_span file line (Some span) msg
 
+(** Lazy assert *)
+let classert_opt_span (file : string) (line : int) (b : bool)
+    (span : Meta.span option) (msg : string Lazy.t) =
+  if not b then craise_opt_span file line span (Lazy.force msg)
+
+(** Lazy assert *)
+let classert (file : string) (line : int) (b : bool) (span : Meta.span)
+    (msg : string Lazy.t) =
+  classert_opt_span file line b (Some span) msg
+
 let cassert_opt_span (file : string) (line : int) (b : bool)
     (span : Meta.span option) (msg : string) =
   if not b then craise_opt_span file line span msg