core_models/abstractions/
funarr.rs

1/// A fixed-size array wrapper with functional semantics and F* integration.
2///
3/// `FunArray<N, T>` represents an array of `T` values of length `N`, where `N` is a compile-time constant.
4/// Internally, it uses a fixed-length array of `Option<T>` with a maximum capacity of 512 elements.
5/// Unused elements beyond `N` are filled with `None`.
6///
7/// This type is integrated with F* through various `#[hax_lib::fstar::replace]` attributes to support
8/// formal verification workflows.
9
10#[hax_lib::fstar::replace(
11    r#"
12open FStar.FunctionalExtensionality
13noeq type t_FunArray (n: u64) (t: Type0) = | FunArray : (i:u64 {v i < v n} ^-> t) -> t_FunArray n t
14
15let ${FunArray::<0, ()>::get} (v_N: u64) (#v_T: Type0) (self: t_FunArray v_N v_T) (i: u64 {v i < v v_N}) : v_T = 
16    self._0 i
17
18let ${FunArray::<0, ()>::from_fn::<fn(u64)->()>}
19    (v_N: u64)
20    (#v_T: Type0)
21    (f: (i: u64 {v i < v v_N}) -> v_T)
22    : t_FunArray v_N v_T = FunArray (on (i: u64 {v i < v v_N}) f)
23
24let ${FunArray::<0, ()>::as_vec} n #t (self: t_FunArray n t) = FStar.Seq.init (v n) (fun i -> self._0 (mk_u64 i))
25
26let rec ${FunArray::<0, ()>::fold::<()>} n #t #a (arr: t_FunArray n t) (init: a) (f: a -> t -> a): Tot a (decreases (v n)) = 
27    match n with
28    | MkInt 0 -> init
29    | MkInt n ->
30        let acc: a = f init (arr._0 (mk_u64 0)) in
31        let n = MkInt (n - 1) in
32        ${FunArray::<0, ()>::fold::<()>}  n #t #a
33                      (${FunArray::<0, ()>::from_fn::<fn(u64)->()>} n (fun i -> arr._0 (i +. mk_u64 1)))
34                      acc f
35"#
36)]
37#[derive(Copy, Clone, Eq, PartialEq)]
38pub struct FunArray<const N: u64, T>([Option<T>; 512]);
39
40#[hax_lib::exclude]
41impl<const N: u64, T> FunArray<N, T> {
42    /// Gets a reference to the element at index `i`.
43    pub fn get(&self, i: u64) -> &T {
44        self.0[i as usize].as_ref().unwrap()
45    }
46    /// Constructor for FunArray. `FunArray<N,T>::from_fn` constructs a funarray out of a function that takes usizes smaller than `N` and produces an element of type T.
47    pub fn from_fn<F: Fn(u64) -> T>(f: F) -> Self {
48        // let vec = (0..N).map(f).collect();
49        let arr = core::array::from_fn(|i| {
50            if (i as u64) < N {
51                Some(f(i as u64))
52            } else {
53                None
54            }
55        });
56        Self(arr)
57    }
58
59    /// Converts the `FunArray` into a `Vec<T>`.
60    pub fn as_vec(&self) -> Vec<T>
61    where
62        T: Clone,
63    {
64        self.0[0..(N as usize)]
65            .iter()
66            .cloned()
67            .map(|x| x.unwrap())
68            .collect()
69    }
70
71    /// Folds over the array, accumulating a result.
72    ///
73    /// # Arguments
74    /// * `init` - The initial value of the accumulator.
75    /// * `f` - A function combining the accumulator and each element.
76    pub fn fold<A>(&self, mut init: A, f: fn(A, T) -> A) -> A
77    where
78        T: Clone,
79    {
80        for i in 0..N {
81            init = f(init, self[i].clone());
82        }
83        init
84    }
85}
86
87macro_rules! impl_pointwise {
88    ($n:literal, $($i:literal)*) => {
89        impl<T: Copy> FunArray<$n, T> {
90            pub fn pointwise(self) -> Self {
91                Self::from_fn(|i| match i {
92                    $($i => self[$i],)*
93                    _ => unreachable!(),
94                })
95            }
96        }
97    };
98}
99
100impl_pointwise!(4, 0 1 2 3);
101impl_pointwise!(8, 0 1 2 3 4 5 6 7);
102impl_pointwise!(16, 0 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15);
103
104#[hax_lib::exclude]
105impl<const N: u64, T: Clone> TryFrom<Vec<T>> for FunArray<N, T> {
106    type Error = ();
107    fn try_from(v: Vec<T>) -> Result<Self, ()> {
108        if (v.len() as u64) < N {
109            Err(())
110        } else {
111            Ok(Self::from_fn(|i| v[i as usize].clone()))
112        }
113    }
114}
115
116#[hax_lib::exclude]
117impl<const N: u64, T: core::fmt::Debug + Clone> core::fmt::Debug for FunArray<N, T> {
118    fn fmt(&self, f: &mut core::fmt::Formatter<'_>) -> core::fmt::Result {
119        write!(f, "{:?}", self.as_vec())
120    }
121}
122
123#[hax_lib::attributes]
124impl<const N: u64, T> core::ops::Index<u64> for FunArray<N, T> {
125    type Output = T;
126    #[requires(index < N)]
127    fn index(&self, index: u64) -> &Self::Output {
128        self.get(index)
129    }
130}
core_models/abstractions/funarr.rs

core_models/abstractions/
funarr.rs
