From 2281630be328d064f0aab62f815e876f1630bc5d Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Mon, 29 Apr 2024 14:59:26 +0200 Subject: [PATCH 1/3] add F* core arch type --- proof-libs/fstar/core/Core.Core_arch.X86.fsti | 3 +++ proof-libs/fstar/core/Core.Core_arch.fsti | 3 +++ proof-libs/fstar/core/Core.fst | 1 + 3 files changed, 7 insertions(+) create mode 100644 proof-libs/fstar/core/Core.Core_arch.X86.fsti create mode 100644 proof-libs/fstar/core/Core.Core_arch.fsti diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.fsti new file mode 100644 index 000000000..4d115808c --- /dev/null +++ b/proof-libs/fstar/core/Core.Core_arch.X86.fsti @@ -0,0 +1,3 @@ +module Core.Core_arch.X86 + +val t____m256i:Type diff --git a/proof-libs/fstar/core/Core.Core_arch.fsti b/proof-libs/fstar/core/Core.Core_arch.fsti new file mode 100644 index 000000000..f5f98326b --- /dev/null +++ b/proof-libs/fstar/core/Core.Core_arch.fsti @@ -0,0 +1,3 @@ +module Core.Core_arch + +include Core.Core_arch.X86 diff --git a/proof-libs/fstar/core/Core.fst b/proof-libs/fstar/core/Core.fst index e7b1d30a3..51fb6bd39 100644 --- a/proof-libs/fstar/core/Core.fst +++ b/proof-libs/fstar/core/Core.fst @@ -4,3 +4,4 @@ include Rust_primitives include Core.Num include Core.Iter include Core.Ops +include Core.Core_arch From f4f28c05b18a9065f18403b00b50e11e20e7aa8b Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Mon, 29 Apr 2024 15:10:40 +0200 Subject: [PATCH 2/3] Update proof-libs/fstar/core/Core.Core_arch.fsti Co-authored-by: Lucas Franceschino --- proof-libs/fstar/core/Core.Core_arch.fsti | 1 - 1 file changed, 1 deletion(-) diff --git a/proof-libs/fstar/core/Core.Core_arch.fsti b/proof-libs/fstar/core/Core.Core_arch.fsti index f5f98326b..a3921ebe3 100644 --- a/proof-libs/fstar/core/Core.Core_arch.fsti +++ b/proof-libs/fstar/core/Core.Core_arch.fsti @@ -1,3 +1,2 @@ module Core.Core_arch -include Core.Core_arch.X86 From cf0f319d4f61b178b49a30da19266aff5e337db2 Mon Sep 17 00:00:00 2001 From: Franziskus Kiefer Date: Mon, 29 Apr 2024 15:10:48 +0200 Subject: [PATCH 3/3] Update proof-libs/fstar/core/Core.fst Co-authored-by: Lucas Franceschino --- proof-libs/fstar/core/Core.fst | 1 - 1 file changed, 1 deletion(-) diff --git a/proof-libs/fstar/core/Core.fst b/proof-libs/fstar/core/Core.fst index 51fb6bd39..e7b1d30a3 100644 --- a/proof-libs/fstar/core/Core.fst +++ b/proof-libs/fstar/core/Core.fst @@ -4,4 +4,3 @@ include Rust_primitives include Core.Num include Core.Iter include Core.Ops -include Core.Core_arch