Update the F* and Coq backends and regenerate the files

AeneasVerif · Dec 5, 2024 · 4736339 · 4736339
1 parent 6ca0aa8
commit 4736339
Show file tree

Hide file tree

Showing 17 changed files with 819 additions and 71 deletions.
diff --git a/backends/coq/Primitives.v b/backends/coq/Primitives.v
@@ -578,62 +578,61 @@ Definition core_clone_CloneBool : core_clone_Clone bool := {|
   clone := fun b => Ok (core_clone_impls_CloneBool_clone b)
 |}.
 
-Record core_marker_Copy_t (Self : Type) := mkcore_marker_Copy_t {
+Record core_marker_Copy (Self : Type) := mkcore_marker_Copy {
   coreCloneInst : core_clone_Clone Self;
 }.
 
-Arguments mkcore_marker_Copy_t { _ }.
+Arguments mkcore_marker_Copy { _ }.
 Arguments coreCloneInst { _ } _.
 
-Definition core_marker_CopyU8 : core_marker_Copy_t u8 := {|
+Definition core_marker_CopyU8 : core_marker_Copy u8 := {|
   coreCloneInst := core_clone_CloneU8;
 |}.
 
-Definition core_marker_CopyU16 : core_marker_Copy_t u16 := {|
+Definition core_marker_CopyU16 : core_marker_Copy u16 := {|
   coreCloneInst := core_clone_CloneU16;
 |}.
 
-Definition core_marker_CopyU32 : core_marker_Copy_t u32 := {|
+Definition core_marker_CopyU32 : core_marker_Copy u32 := {|
   coreCloneInst := core_clone_CloneU32;
 |}.
 
-Definition core_marker_CopyU64 : core_marker_Copy_t u64 := {|
+Definition core_marker_CopyU64 : core_marker_Copy u64 := {|
   coreCloneInst := core_clone_CloneU64;
 |}.
 
-Definition core_marker_CopyU128 : core_marker_Copy_t u128 := {|
+Definition core_marker_CopyU128 : core_marker_Copy u128 := {|
   coreCloneInst := core_clone_CloneU128;
 |}.
 
-Definition core_marker_CopyUsize : core_marker_Copy_t usize := {|
+Definition core_marker_CopyUsize : core_marker_Copy usize := {|
   coreCloneInst := core_clone_CloneUsize;
 |}.
 
-Definition core_marker_CopyI8 : core_marker_Copy_t i8 := {|
+Definition core_marker_CopyI8 : core_marker_Copy i8 := {|
   coreCloneInst := core_clone_CloneI8;
 |}.
 
-Definition core_marker_CopyI16 : core_marker_Copy_t i16 := {|
+Definition core_marker_CopyI16 : core_marker_Copy i16 := {|
   coreCloneInst := core_clone_CloneI16;
 |}.
 
-Definition core_marker_CopyI32 : core_marker_Copy_t i32 := {|
+Definition core_marker_CopyI32 : core_marker_Copy i32 := {|
   coreCloneInst := core_clone_CloneI32;
 |}.
 
-Definition core_marker_CopyI64 : core_marker_Copy_t i64 := {|
+Definition core_marker_CopyI64 : core_marker_Copy i64 := {|
   coreCloneInst := core_clone_CloneI64;
 |}.
 
-Definition core_marker_CopyI128 : core_marker_Copy_t i128 := {|
+Definition core_marker_CopyI128 : core_marker_Copy i128 := {|
   coreCloneInst := core_clone_CloneI128;
 |}.
 
-Definition core_marker_CopyIsize : core_marker_Copy_t isize := {|
+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

diff --git a/backends/fstar/Primitives.fst b/backends/fstar/Primitives.fst
@@ -556,55 +556,55 @@ let core_clone_CloneI128 : core_clone_Clone i128 = {
   clone = fun x -> Ok (core_clone_impls_CloneI128_clone x)
 }
 
-noeq type core_marker_Copy_t (self : Type0) = {
+noeq type core_marker_Copy (self : Type0) = {
   cloneCloneInst : core_clone_Clone self;
 }
 
-let core_marker_CopyU8 : core_marker_Copy_t u8 = {
+let core_marker_CopyU8 : core_marker_Copy u8 = {
   cloneCloneInst = core_clone_CloneU8;
 }
 
-let core_marker_CopyU16 : core_marker_Copy_t u16 = {
+let core_marker_CopyU16 : core_marker_Copy u16 = {
   cloneCloneInst = core_clone_CloneU16;
 }
 
-let core_marker_CopyU32 : core_marker_Copy_t u32 = {
+let core_marker_CopyU32 : core_marker_Copy u32 = {
   cloneCloneInst = core_clone_CloneU32;
 }
 
-let core_marker_CopyU64 : core_marker_Copy_t u64 = {
+let core_marker_CopyU64 : core_marker_Copy u64 = {
   cloneCloneInst = core_clone_CloneU64;
 }
 
-let core_marker_CopyU128 : core_marker_Copy_t u128 = {
+let core_marker_CopyU128 : core_marker_Copy u128 = {
   cloneCloneInst = core_clone_CloneU128;
 }
 
-let core_marker_CopyUsize : core_marker_Copy_t usize = {
+let core_marker_CopyUsize : core_marker_Copy usize = {
   cloneCloneInst = core_clone_CloneUsize;
 }
 
-let core_marker_CopyI8 : core_marker_Copy_t i8 = {
+let core_marker_CopyI8 : core_marker_Copy i8 = {
   cloneCloneInst = core_clone_CloneI8;
 }
 
-let core_marker_CopyI16 : core_marker_Copy_t i16 = {
+let core_marker_CopyI16 : core_marker_Copy i16 = {
   cloneCloneInst = core_clone_CloneI16;
 }
 
-let core_marker_CopyI32 : core_marker_Copy_t i32 = {
+let core_marker_CopyI32 : core_marker_Copy i32 = {
   cloneCloneInst = core_clone_CloneI32;
 }
 
-let core_marker_CopyI64 : core_marker_Copy_t i64 = {
+let core_marker_CopyI64 : core_marker_Copy i64 = {
   cloneCloneInst = core_clone_CloneI64;
 }
 
-let core_marker_CopyI128 : core_marker_Copy_t i128 = {
+let core_marker_CopyI128 : core_marker_Copy i128 = {
   cloneCloneInst = core_clone_CloneI128;
 }
 
-let core_marker_CopyIsize : core_marker_Copy_t isize = {
+let core_marker_CopyIsize : core_marker_Copy isize = {
   cloneCloneInst = core_clone_CloneIsize;
 }
 

diff --git a/tests/coq/arrays/Primitives.v b/tests/coq/arrays/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

diff --git a/tests/coq/betree/Primitives.v b/tests/coq/betree/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

diff --git a/tests/coq/demo/Primitives.v b/tests/coq/demo/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