Merge pull request #769 from hacspec/ml-kem-lax-check

Extensions to the proof-libs for libcrux-ml-kem
hacspec · Jul 15, 2024 · 7eb5391 · 7eb5391
2 parents 717d606 + adcbf6a
commit 7eb5391
Show file tree

Hide file tree

Showing 5 changed files with 12 additions and 1 deletion.
diff --git a/proof-libs/fstar/core/Core.Array.fst b/proof-libs/fstar/core/Core.Array.fst
@@ -3,8 +3,10 @@ open Rust_primitives
 
 type t_TryFromSliceError = | TryFromSliceError
 
-let impl_23__map #a #b n (arr: t_Array a n) (f: a -> b): t_Array b n 
+let impl_23__map #a n #b (arr: t_Array a n) (f: a -> b): t_Array b n 
   = map_array arr f
 
 let impl_23__as_slice #a len (arr: t_Array a len): t_Slice a = arr
 
+let from_fn #a len (f: usize -> a): t_Array a len = admit()
+
diff --git a/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti b/proof-libs/fstar/core/Core.Core_arch.Arm_shared.Neon.fsti
@@ -1,6 +1,7 @@
 module Core.Core_arch.Arm_shared.Neon
 
 val t_int16x4_t:Type0
+val t_int16x8_t:Type0
 val t_int32x2_t:Type0
 val t_int32x4_t:Type0
 val t_int64x2_t:Type0

diff --git a/proof-libs/fstar/core/Core.Core_arch.X86.fsti b/proof-libs/fstar/core/Core.Core_arch.X86.fsti
@@ -1,3 +1,5 @@
 module Core.Core_arch.X86
 
+val t____m128i:Type0
+
 val t____m256i:Type0
diff --git a/proof-libs/fstar/core/Core.Hint.fsti b/proof-libs/fstar/core/Core.Hint.fsti
@@ -0,0 +1,3 @@
+module Core.Hint
+
+val black_box: #a:Type0 -> x:a -> y:a{y == x}
diff --git a/proof-libs/fstar/core/Core.Num.fsti b/proof-libs/fstar/core/Core.Num.fsti
@@ -38,8 +38,11 @@ val impl__u16__pow (base: u16) (exponent: u32): result : u16 {v base == 2 /\ v e
 val impl__u32__pow (base: u32) (exponent: u32): result : u32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.U32 (pow2 (v exponent))}
 val impl__u64__pow: u64 -> u32 -> u64
 val impl__u128__pow: u128 -> u32 -> u128
+val impl__i16__pow (base: i16) (exponent: u32): result: i16 {v base == 2 /\ v exponent < 15 ==> result == mk_int #Lib.IntTypes.S16 (pow2 (v exponent))}
 val impl__i32__pow (base: i32) (exponent: u32): result: i32 {v base == 2 /\ v exponent <= 16 ==> result == mk_int #Lib.IntTypes.S32 (pow2 (v exponent))}
 
+val impl__u8__count_ones: u8 -> u32
+
 val impl__u8__from_str_radix: string -> u32 -> Core.Result.t_Result u8 Core.Num.Error.t_ParseIntError
 
 val impl__usize__ilog2: i32 -> u32
Original file line number	Diff line number	Diff line change
		@@ -0,0 +1,3 @@
		module Core.Hint

		val black_box: #a:Type0 -> x:a -> y:a{y == x}