libcrux_secrets/int/
classify_public.rs

1//! This module defines functions for classifying and declassifying various types.
2//! We give definitions for all conversions so that they can be tested.
3//! We define no-ops here and force inlining, to ensure that these are free.
4
5#[cfg(not(hax))]
6use crate::traits::*;
7
8#[cfg(hax)]
9use crate::traits::{ClassifyRef, DeclassifyRef, Scalar};
10
11// TODO: Remove hax exemptions once this is supported.
12//       See https://github.com/cryspen/hax/issues/1674.
13
14// Immutable references to slices can be classified
15impl<'a, T: Scalar> ClassifyRef for &'a [T] {
16    type ClassifiedRef = &'a [T];
17    #[inline(always)]
18    fn classify_ref(self) -> &'a [T] {
19        self
20    }
21}
22
23// Immutable references to slices can be declassified
24impl<'a, T: Scalar> DeclassifyRef for &'a [T] {
25    type DeclassifiedRef = &'a [T];
26    #[inline(always)]
27    fn declassify_ref(self) -> &'a [T] {
28        self
29    }
30}
31
32// Classify any mutable reference (identity)
33#[cfg(not(hax))]
34impl<'a, T> ClassifyRefMut for &'a mut T {
35    type ClassifiedRefMut = &'a mut T;
36    #[inline(always)]
37    fn classify_ref_mut(self) -> &'a mut T {
38        self
39    }
40}
41
42// Declassify any mutable reference (identity)
43#[cfg(not(hax))]
44impl<'a, T> DeclassifyRefMut for &'a mut T {
45    type DeclassifiedRefMut = &'a mut T;
46    #[inline(always)]
47    fn declassify_ref_mut(self) -> &'a mut T {
48        self
49    }
50}
libcrux_secrets/int/classify_public.rs

libcrux_secrets/int/
classify_public.rs
