Merge pull request #538 from hacspec/misc-additions-proofs-lib

feat(proofs-lib/fstar): intro Core.Mem, Core.Fmt, impl__usize__leadin…
hacspec · Mar 4, 2024 · b5b9982 · b5b9982
2 parents 2e099e3 + 7e0739b
commit b5b9982
Show file tree

Hide file tree

Showing 3 changed files with 9 additions and 1 deletion.
diff --git a/proof-libs/fstar/core/Core.Fmt.fsti b/proof-libs/fstar/core/Core.Fmt.fsti
@@ -0,0 +1,3 @@
+module Core.Fmt
+
+val t_Arguments: Type0
diff --git a/proof-libs/fstar/core/Core.Mem.fsti b/proof-libs/fstar/core/Core.Mem.fsti
@@ -0,0 +1,5 @@
+module Core.Mem
+open Rust_primitives
+
+// FIXME(unsafe!): remove default type (see #545)
+val size_of (#[FStar.Tactics.exact (`eqtype_as_type unit)]t:Type): unit -> usize
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
@@ -42,5 +42,5 @@ val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v ex
 val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError
 
 val impl__usize__ilog2: i32 -> u32 
-
+val impl__usize__leading_zeros: usize -> u32