hydro_lang/properties/
mod.rs

1//! Types for reasoning about algebraic properties for Rust closures.
2
3use std::marker::PhantomData;
4
5use stageleft::properties::Property;
6
7use crate::live_collections::boundedness::Boundedness;
8use crate::live_collections::keyed_singleton::KeyedSingletonBound;
9use crate::live_collections::singleton::SingletonBound;
10use crate::live_collections::stream::{ExactlyOnce, Ordering, Retries, TotalOrder};
11
12/// A trait for proof mechanisms that can validate commutativity.
13#[sealed::sealed]
14pub trait CommutativeProof {
15    /// Registers the expression with the proof mechanism.
16    ///
17    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
18    fn register_proof(&self, expr: &syn::Expr);
19}
20
21/// A trait for proof mechanisms that can validate idempotence.
22#[sealed::sealed]
23pub trait IdempotentProof {
24    /// Registers the expression with the proof mechanism.
25    ///
26    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
27    fn register_proof(&self, expr: &syn::Expr);
28}
29
30/// A trait for proof mechanisms that can validate monotonicity.
31#[sealed::sealed]
32pub trait MonotoneProof {
33    /// Registers the expression with the proof mechanism.
34    ///
35    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
36    fn register_proof(&self, expr: &syn::Expr);
37}
38
39/// A trait for proof mechanisms that can validate order-preservation (monotonicity of a map function).
40#[sealed::sealed]
41pub trait OrderPreservingProof {
42    /// Registers the expression with the proof mechanism.
43    ///
44    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
45    fn register_proof(&self, expr: &syn::Expr);
46}
47
48/// A trait for proof mechanisms that can validate consistency of a collection.
49#[sealed::sealed]
50pub trait ConsistencyProof {}
51
52/// A hand-written human proof of the correctness property.
53///
54/// To create a manual proof, use the [`manual_proof!`] macro, which takes in a doc comment
55/// explaining why the property holds.
56pub struct ManualProof();
57#[sealed::sealed]
58impl CommutativeProof for ManualProof {
59    fn register_proof(&self, _expr: &syn::Expr) {}
60}
61#[sealed::sealed]
62impl IdempotentProof for ManualProof {
63    fn register_proof(&self, _expr: &syn::Expr) {}
64}
65#[sealed::sealed]
66impl MonotoneProof for ManualProof {
67    fn register_proof(&self, _expr: &syn::Expr) {}
68}
69#[sealed::sealed]
70impl OrderPreservingProof for ManualProof {
71    fn register_proof(&self, _expr: &syn::Expr) {}
72}
73#[sealed::sealed]
74impl ConsistencyProof for ManualProof {}
75
76#[doc(inline)]
77pub use crate::__manual_proof__ as manual_proof;
78
79#[macro_export]
80/// Fulfills a proof parameter by declaring a human-written justification for why
81/// the algebraic property (e.g. commutativity, idempotence) holds.
82///
83/// The argument must be a doc comment explaining why the property is satisfied.
84///
85/// # Examples
86/// ```rust,ignore
87/// use hydro_lang::prelude::*;
88///
89/// stream.fold(
90///     q!(|| 0),
91///     q!(
92///         |acc, x| *acc += x,
93///         commutative = manual_proof!(/** integer addition is commutative */)
94///     )
95/// )
96/// ```
97macro_rules! __manual_proof__ {
98    ($(#[doc = $doc:expr])+) => {
99        $crate::properties::ManualProof()
100    };
101}
102
103/// Marks that the property is not proved.
104pub enum NotProved {}
105
106/// Marks that the property is proven.
107pub enum Proved {}
108
109/// Query whether a proof marker is `Proved`.
110pub trait IsProved {
111    /// Whether the property has been proven.
112    const IS_PROVED: bool;
113}
114impl IsProved for NotProved {
115    const IS_PROVED: bool = false;
116}
117impl IsProved for Proved {
118    const IS_PROVED: bool = true;
119}
120
121/// Algebraic properties for an aggregation function of type (T, &mut A) -> ().
122///
123/// Commutativity:
124/// ```rust,ignore
125/// let mut state = ???;
126/// f(a, &mut state); f(b, &mut state) // produces same final state as
127/// f(b, &mut state); f(a, &mut state)
128/// ```
129///
130/// Idempotence:
131/// ```rust,ignore
132/// let mut state = ???;
133/// f(a, &mut state);
134/// let state1 = *state;
135/// f(a, &mut state);
136/// // state1 must be equal to state
137/// ```
138pub struct AggFuncAlgebra<Commutative = NotProved, Idempotent = NotProved, Monotone = NotProved>(
139    Option<Box<dyn CommutativeProof>>,
140    Option<Box<dyn IdempotentProof>>,
141    Option<Box<dyn MonotoneProof>>,
142    PhantomData<(Commutative, Idempotent, Monotone)>,
143);
144
145impl<C, I, M> AggFuncAlgebra<C, I, M> {
146    /// Marks the function as being commutative, with the given proof mechanism.
147    pub fn commutative(
148        self,
149        proof: impl CommutativeProof + 'static,
150    ) -> AggFuncAlgebra<Proved, I, M> {
151        AggFuncAlgebra(Some(Box::new(proof)), self.1, self.2, PhantomData)
152    }
153
154    /// Marks the function as being idempotent, with the given proof mechanism.
155    pub fn idempotent(self, proof: impl IdempotentProof + 'static) -> AggFuncAlgebra<C, Proved, M> {
156        AggFuncAlgebra(self.0, Some(Box::new(proof)), self.2, PhantomData)
157    }
158
159    /// Marks the function as being monotone, with the given proof mechanism.
160    pub fn monotone(self, proof: impl MonotoneProof + 'static) -> AggFuncAlgebra<C, I, Proved> {
161        AggFuncAlgebra(self.0, self.1, Some(Box::new(proof)), PhantomData)
162    }
163
164    /// Registers the expression with the underlying proof mechanisms.
165    pub(crate) fn register_proof(self, expr: &syn::Expr) {
166        if let Some(comm_proof) = self.0 {
167            comm_proof.register_proof(expr);
168        }
169
170        if let Some(idem_proof) = self.1 {
171            idem_proof.register_proof(expr);
172        }
173
174        if let Some(monotone_proof) = self.2 {
175            monotone_proof.register_proof(expr);
176        }
177    }
178}
179
180impl<C, I, M> Property for AggFuncAlgebra<C, I, M> {
181    type Root = AggFuncAlgebra;
182
183    fn make_root(_target: &mut Option<Self>) -> Self::Root {
184        AggFuncAlgebra(None, None, None, PhantomData)
185    }
186}
187
188/// Algebraic properties for a map function of type T -> U.
189///
190/// Order-preserving means that if the input grows monotonically, the output also grows monotonically.
191pub struct MapFuncAlgebra<OrderPreserving = NotProved>(
192    Option<Box<dyn OrderPreservingProof>>,
193    PhantomData<OrderPreserving>,
194);
195
196impl<O> MapFuncAlgebra<O> {
197    /// Marks the function as being order-preserving, with the given proof mechanism.
198    pub fn order_preserving(
199        self,
200        proof: impl OrderPreservingProof + 'static,
201    ) -> MapFuncAlgebra<Proved> {
202        MapFuncAlgebra(Some(Box::new(proof)), PhantomData)
203    }
204
205    /// Registers the expression with the underlying proof mechanisms.
206    pub(crate) fn register_proof(self, expr: &syn::Expr) {
207        if let Some(proof) = self.0 {
208            proof.register_proof(expr);
209        }
210    }
211}
212
213impl<O> Property for MapFuncAlgebra<O> {
214    type Root = MapFuncAlgebra;
215
216    fn make_root(_target: &mut Option<Self>) -> Self::Root {
217        MapFuncAlgebra(None, PhantomData)
218    }
219}
220
221/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
222#[diagnostic::on_unimplemented(
223    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
224    label = "required for this call",
225    note = "To intentionally process the stream by observing a non-deterministic (shuffled) order of elements, use `.assume_ordering`. This introduces non-determinism so avoid unless necessary."
226)]
227#[sealed::sealed]
228pub trait ValidCommutativityFor<O: Ordering> {}
229#[sealed::sealed]
230impl ValidCommutativityFor<TotalOrder> for NotProved {}
231#[sealed::sealed]
232impl<O: Ordering> ValidCommutativityFor<O> for Proved {}
233
234/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
235#[diagnostic::on_unimplemented(
236    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
237    label = "required for this call",
238    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
239)]
240#[sealed::sealed]
241pub trait ValidIdempotenceFor<R: Retries> {}
242#[sealed::sealed]
243impl ValidIdempotenceFor<ExactlyOnce> for NotProved {}
244#[sealed::sealed]
245impl<R: Retries> ValidIdempotenceFor<R> for Proved {}
246
247/// Marker trait identifying the boundedness of a singleton given a monotonicity property of
248/// an aggregation on a stream.
249#[sealed::sealed]
250pub trait ApplyMonotoneStream<P, B2: SingletonBound> {}
251
252#[sealed::sealed]
253impl<B: Boundedness> ApplyMonotoneStream<NotProved, B> for B {}
254
255#[sealed::sealed]
256impl<B: Boundedness> ApplyMonotoneStream<Proved, B::StreamToMonotone> for B {}
257
258/// Marker trait identifying the boundedness of a singleton given a monotonicity property of
259/// an aggregation on a keyed stream.
260#[sealed::sealed]
261pub trait ApplyMonotoneKeyedStream<P, B2: KeyedSingletonBound> {}
262
263#[sealed::sealed]
264impl<B: Boundedness> ApplyMonotoneKeyedStream<NotProved, B> for B {}
265
266#[sealed::sealed]
267impl<B: Boundedness> ApplyMonotoneKeyedStream<Proved, B::KeyedStreamToMonotone> for B {}
268
269/// Marker trait identifying the boundedness of a singleton after a map operation,
270/// given an order-preserving property.
271#[sealed::sealed]
272pub trait ApplyOrderPreservingSingleton<P, B2: SingletonBound> {}
273
274#[sealed::sealed]
275impl<B: SingletonBound> ApplyOrderPreservingSingleton<NotProved, B::UnderlyingBound> for B {}
276
277#[sealed::sealed]
278impl<B: SingletonBound> ApplyOrderPreservingSingleton<Proved, B> for B {}
hydro_lang/properties/mod.rs

hydro_lang/properties/
mod.rs
