Skip to content

Commit

Permalink
Merge pull request #781 from cryspen/update-fstar-new-naming
Browse files Browse the repository at this point in the history 
Update F* output with latest hax (after merging new naming).
  • Loading branch information
@maximebuyse
maximebuyse authored Jan 30, 2025
2 parents 0ca79fc + 39f2dbf commit 59fcb15
Show file tree
Hide file tree
Showing 104 changed files with 1,931 additions and 1,926 deletions.
309 changes: 153 additions & 156 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fst
View file

Large diffs are not rendered by default.

154 changes: 77 additions & 77 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Arm64_extract.fsti
View file
Original file line number Diff line number Diff line change
@@ -1,160 +1,160 @@
module Libcrux_intrinsics.Arm64_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

val v__vdupq_n_s16 (i: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vdupq_n_s16 (i: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vdupq_n_u64 (i: u64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vdupq_n_u64 (i: u64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vst1q_s16 (out: t_Slice i16) (v: u8)
val e_vst1q_s16 (out: t_Slice i16) (v: u8)
: Prims.Pure (t_Slice i16) Prims.l_True (fun _ -> Prims.l_True)

val v__vld1q_s16 (array: t_Slice i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vld1q_s16 (array: t_Slice i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vld1q_bytes_u64 (array: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vld1q_bytes_u64 (array: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vld1q_u64 (array: t_Slice u64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vld1q_u64 (array: t_Slice u64) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vst1q_u64 (out: t_Slice u64) (v: u8)
val e_vst1q_u64 (out: t_Slice u64) (v: u8)
: Prims.Pure (t_Slice u64) Prims.l_True (fun _ -> Prims.l_True)

val v__vst1q_bytes_u64 (out: t_Slice u8) (v: u8)
val e_vst1q_bytes_u64 (out: t_Slice u8) (v: u8)
: Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

val v__vaddq_s16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vaddq_s16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vsubq_s16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vsubq_s16 (lhs rhs: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmulq_n_s16 (v: u8) (c: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmulq_n_s16 (v: u8) (c: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmulq_n_u16 (v: u8) (c: u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmulq_n_u16 (v: u8) (c: u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshrq_n_s16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshrq_n_s16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshrq_n_u16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshrq_n_u16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshrq_n_u64 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshrq_n_u64 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshlq_n_u64 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshlq_n_u64 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshlq_n_s16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshlq_n_s16 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshlq_n_u32 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshlq_n_u32 (v_SHIFT_BY: i32) (v: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vqdmulhq_n_s16 (k: u8) (b: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vqdmulhq_n_s16 (k: u8) (b: i16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vqdmulhq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vqdmulhq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vcgeq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vcgeq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vandq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vandq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vbicq_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vbicq_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s16_u16 (m0: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s16_u16 (m0: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_u16_s16 (m0: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_u16_s16 (m0: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmulq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmulq_s16 (v c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__veorq_s16 (mask shifted: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_veorq_s16 (mask shifted: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__veorq_u64 (mask shifted: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_veorq_u64 (mask shifted: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vdupq_n_u32 (value: u32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vdupq_n_u32 (value: u32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vaddq_u32 (compressed half: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vaddq_u32 (compressed half: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s32_u32 (compressed: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s32_u32 (compressed: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vqdmulhq_n_s32 (a: u8) (b: i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vqdmulhq_n_s32 (a: u8) (b: i32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_u32_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_u32_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshrq_n_u32 (v_N: i32) (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshrq_n_u32 (v_N: i32) (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vandq_u32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vandq_u32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_u32_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_u32_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s16_u32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s16_u32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn1q_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn1q_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn2q_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn2q_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmulq_n_u32 (a: u8) (b: u32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmulq_n_u32 (a: u8) (b: u32) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn1q_s32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn1q_s32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s16_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s16_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s32_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s32_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn2q_s32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn2q_s32 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn1q_s64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn1q_s64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn1q_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn1q_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s16_s64 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s16_s64 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s64_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s64_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn2q_s64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn2q_s64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vtrn2q_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vtrn2q_u64 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmull_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmull_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vget_low_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vget_low_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmull_high_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmull_high_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmlal_s16 (a b c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmlal_s16 (a b c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vmlal_high_s16 (a b c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vmlal_high_s16 (a b c: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vld1q_u8 (ptr: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vld1q_u8 (ptr: t_Slice u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_u8_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_u8_s16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vqtbl1q_u8 (t idx: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vqtbl1q_u8 (t idx: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s16_u8 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s16_u8 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshlq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshlq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vshlq_u16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vshlq_u16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vaddv_u16 (a: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True)
val e_vaddv_u16 (a: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True)

val v__vget_low_u16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vget_low_u16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vget_high_u16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vget_high_u16 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vaddvq_s16 (a: u8) : Prims.Pure i16 Prims.l_True (fun _ -> Prims.l_True)
val e_vaddvq_s16 (a: u8) : Prims.Pure i16 Prims.l_True (fun _ -> Prims.l_True)

val v__vsliq_n_s32 (v_N: i32) (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vsliq_n_s32 (v_N: i32) (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_s64_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_s64_s32 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vsliq_n_s64 (v_N: i32) (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vsliq_n_s64 (v_N: i32) (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_u8_s64 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_u8_s64 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vst1q_u8 (out: t_Slice u8) (v: u8)
val e_vst1q_u8 (out: t_Slice u8) (v: u8)
: Prims.Pure (t_Slice u8) Prims.l_True (fun _ -> Prims.l_True)

val v__vdupq_n_u16 (value: u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vdupq_n_u16 (value: u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vandq_u16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vandq_u16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vreinterpretq_u16_u8 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vreinterpretq_u16_u8 (a: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vld1q_u16 (ptr: t_Slice u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vld1q_u16 (ptr: t_Slice u16) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vcleq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)
val e_vcleq_s16 (a b: u8) : Prims.Pure u8 Prims.l_True (fun _ -> Prims.l_True)

val v__vaddvq_u16 (a: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True)
val e_vaddvq_u16 (a: u8) : Prims.Pure u16 Prims.l_True (fun _ -> Prims.l_True)
12 changes: 6 additions & 6 deletions libcrux-intrinsics/proofs/fstar/extraction/Libcrux_intrinsics.Avx2_extract.fst
View file
Original file line number Diff line number Diff line change
@@ -1,13 +1,8 @@
module Libcrux_intrinsics.Avx2_extract
#set-options "--fuel 0 --ifuel 1 --z3rlimit 80"
#set-options "--fuel 0 --ifuel 1 --z3rlimit 15"
open Core
open FStar.Mul

assume
val mm256_movemask_ps': a: u8 -> Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)

let mm256_movemask_ps = mm256_movemask_ps'

[@@ FStar.Tactics.Typeclasses.tcinstance]
assume
val impl': Core.Clone.t_Clone t_Vec256
Expand Down Expand Up @@ -231,6 +226,11 @@ val mm256_castsi256_ps': a: t_Vec256 -> Prims.Pure u8 Prims.l_True (fun _ -> Pri

let mm256_castsi256_ps = mm256_castsi256_ps'

assume
val mm256_movemask_ps': a: u8 -> Prims.Pure i32 Prims.l_True (fun _ -> Prims.l_True)

let mm256_movemask_ps = mm256_movemask_ps'

assume
val mm_mulhi_epi16': lhs: t_Vec128 -> rhs: t_Vec128
-> Prims.Pure t_Vec128
Expand Down
Loading

0 comments on commit 59fcb15

Please sign in to comment.