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

hydro_lang/properties/
mod.rs
