libcrux-ml-dsa 0.0.4

Libcrux ML-DSA implementation
Documentation 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70

use hax_lib::*;

pub mod simd {
    use super::*;
    pub mod portable {
        use super::*;
        pub mod sample {
            use super::*;
            pub fn rejection_sample_less_than_field_modulus_pre(
                randomness: &[u8],
                out: &[i32],
            ) -> Prop {
                (randomness.len() / 3 <= 4_294_967_295 && randomness.len() / 3 <= out.len()).into()
            }

            #[fstar::replace_body(
                r#"let s = Spec.MLDSA.Math.rejection_sample_field_modulus $randomness in
                v $r <= Seq.length out /\ v $r == Seq.length s /\
                Seq.slice out 0 (v $r) == s"#
            )]
            pub fn rejection_sample_less_than_field_modulus_post(
                randomness: &[u8],
                out: &[i32],
                r: usize,
            ) -> Prop {
                true.into()
            }

            pub fn rejection_sample_less_than_eta_equals_2_pre(
                randomness: &[u8],
                out: &[i32],
            ) -> Prop {
                (randomness.len() * 2 <= 4_294_967_295 && randomness.len() * 2 <= out.len()).into()
            }

            #[fstar::replace_body(
                r#"let s = Spec.MLDSA.Math.rejection_sample_eta_2 $randomness in
                v $r <= Seq.length out /\ v $r == Seq.length s /\
                Seq.slice out 0 (v $r) == s"#
            )]
            pub fn rejection_sample_less_than_eta_equals_2_post(
                randomness: &[u8],
                out: &[i32],
                r: usize,
            ) -> Prop {
                true.into()
            }

            pub fn rejection_sample_less_than_eta_equals_4_pre(
                randomness: &[u8],
                out: &[i32],
            ) -> Prop {
                (randomness.len() * 2 <= 4_294_967_295 && randomness.len() * 2 <= out.len()).into()
            }

            #[fstar::replace_body(
                r#"let s = Spec.MLDSA.Math.rejection_sample_eta_4 $randomness in
                v $r <= Seq.length out /\ v $r == Seq.length s /\
                Seq.slice out 0 (v $r) == s"#
            )]
            pub fn rejection_sample_less_than_eta_equals_4_post(
                randomness: &[u8],
                out: &[i32],
                r: usize,
            ) -> Prop {
                true.into()
            }
        }
    }
}