test_foo_bar_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
5use crate::traits::*;
6
7// TODO: Remove hax exemptions once this is supported.
8//       See https://github.com/cryspen/hax/issues/1674.
9
10// Immutable references to slices can be classified
11impl<'a, T: Scalar> ClassifyRef for &'a [T] {
12    type ClassifiedRef = &'a [T];
13    #[inline(always)]
14    fn classify_ref(self) -> &'a [T] {
15        self
16    }
17}
18
19// Immutable references to slices can be declassified
20impl<'a, T: Scalar> DeclassifyRef for &'a [T] {
21    type DeclassifiedRef = &'a [T];
22    #[inline(always)]
23    fn declassify_ref(self) -> &'a [T] {
24        self
25    }
26}
27
28// Classify any mutable reference (identity)
29#[hax_lib::exclude]
30impl<'a, T> ClassifyRefMut for &'a mut T {
31    type ClassifiedRefMut = &'a mut T;
32    #[inline(always)]
33    fn classify_ref_mut(self) -> &'a mut T {
34        self
35    }
36}
37
38// Declassify any mutable reference (identity)
39#[hax_lib::exclude]
40impl<'a, T> DeclassifyRefMut for &'a mut T {
41    type DeclassifiedRefMut = &'a mut T;
42    #[inline(always)]
43    fn declassify_ref_mut(self) -> &'a mut T {
44        self
45    }
46}
test_foo_bar_secrets/int/classify_public.rs

test_foo_bar_secrets/int/
classify_public.rs
