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

core_models/abstractions/
funarr.rs
