Skip to content

Commit

Permalink
Merge pull request #671 from cryspen/jonas/invntt-butterfly
Browse files Browse the repository at this point in the history 
More efficient butterfly in inverse NTT layers 0-2
  • Loading branch information
@franziskuskiefer
franziskuskiefer authored Nov 15, 2024
2 parents 2608798 + e458471 commit dc479b8
Show file tree
Hide file tree
Showing 25 changed files with 2,344 additions and 2,036 deletions.
4 changes: 2 additions & 2 deletions libcrux-intrinsics/src/avx2.rs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -549,8 +549,8 @@ pub fn mm256_set_epi64x(input3: i64, input2: i64, input1: i64, input0: i64) -> V
}

#[inline(always)]
pub fn mm256_unpacklo_epi64(a: Vec256, b: Vec256) -> Vec256 {
unsafe { _mm256_unpacklo_epi64(a, b) }
pub fn mm256_unpacklo_epi64(lhs: Vec256, rhs: Vec256) -> Vec256 {
unsafe { _mm256_unpacklo_epi64(lhs, rhs) }
}

#[inline(always)]
Expand Down
727 changes: 10 additions & 717 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ntt.fst
View file

Large diffs are not rendered by default.

126 changes: 1 addition & 125 deletions libcrux-ml-dsa/proofs/fstar/extraction/Libcrux_ml_dsa.Ntt.fsti
View file
Original file line number Diff line number Diff line change
Expand Up @@ -9,73 +9,7 @@ let _ =
let open Libcrux_ml_dsa.Simd.Traits in
()

let invert_ntt_at_layer_3___STEP: usize = sz 8

let invert_ntt_at_layer_3___STEP_BY: usize = sz 1

let invert_ntt_at_layer_4___STEP: usize = sz 16

let invert_ntt_at_layer_4___STEP_BY: usize = sz 2

let invert_ntt_at_layer_5___STEP: usize = sz 32

let invert_ntt_at_layer_5___STEP_BY: usize = sz 4

let invert_ntt_at_layer_6___STEP: usize = sz 64

let invert_ntt_at_layer_6___STEP_BY: usize = sz 8

let invert_ntt_at_layer_7___STEP: usize = sz 128

let invert_ntt_at_layer_7___STEP_BY: usize = sz 16

val invert_ntt_at_layer_0___round
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
(index: usize)
(zeta_0_ zeta_1_ zeta_2_ zeta_3_: i32)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_0_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_1___round
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
(index: usize)
(zeta_0_ zeta_1_: i32)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_1_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_2___round
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
(index: usize)
(zeta: i32)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_2_
val invert_ntt_montgomery
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Expand All @@ -91,64 +25,6 @@ val ntt
Prims.l_True
(fun _ -> Prims.l_True)

val outer_3_plus
(#v_SIMDUnit: Type0)
(v_OFFSET v_STEP_BY: usize)
(v_ZETA: i32)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_3_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_4_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_5_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_6_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_at_layer_7_
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val invert_ntt_montgomery
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
(re: Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
: Prims.Pure (Libcrux_ml_dsa.Polynomial.t_PolynomialRingElement v_SIMDUnit)
Prims.l_True
(fun _ -> Prims.l_True)

val ntt_multiply_montgomery
(#v_SIMDUnit: Type0)
{| i1: Libcrux_ml_dsa.Simd.Traits.t_Operations v_SIMDUnit |}
Expand Down
Loading

0 comments on commit dc479b8

Please sign in to comment.