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
87/// # #[cfg(feature = "deploy")] {
88/// # use hydro_lang::prelude::*;
89/// # use hydro_lang::live_collections::stream::NoOrder;
90/// # use futures::StreamExt;
91/// # tokio_test::block_on(hydro_lang::test_util::stream_transform_test(|process| {
92/// # let stream = process.source_iter(q!(vec![1, 2, 3])).weaken_ordering::<NoOrder>();
93/// // stream: [1, 2, 3] (unordered)
94/// stream
95///     .fold(
96///         q!(|| 0),
97///         q!(
98///             |acc, x| *acc += x,
99///             commutative = manual_proof!(/** integer addition is commutative */)
100///         ),
101///     )
102///     .into_stream()
103/// # }, |mut stream| async move {
104/// # assert_eq!(stream.next().await.unwrap(), 6);
105/// # }));
106/// # }
107/// ```
108macro_rules! __manual_proof__ {
109    ($(#[doc = $doc:expr])+) => {
110        $crate::properties::ManualProof()
111    };
112}
113
114/// Marks that the property is not proved.
115pub enum NotProved {}
116
117/// Marks that the property is proven.
118pub enum Proved {}
119
120/// Algebraic properties for an aggregation function of type (T, &mut A) -> ().
121///
122/// Commutativity:
123/// ```rust,ignore
124/// let mut state = ???;
125/// f(a, &mut state); f(b, &mut state) // produces same final state as
126/// f(b, &mut state); f(a, &mut state)
127/// ```
128///
129/// Idempotence:
130/// ```rust,ignore
131/// let mut state = ???;
132/// f(a, &mut state);
133/// let state1 = *state;
134/// f(a, &mut state);
135/// // state1 must be equal to state
136/// ```
137pub struct AggFuncAlgebra<Commutative = NotProved, Idempotent = NotProved, Monotone = NotProved>(
138    Option<Box<dyn CommutativeProof>>,
139    Option<Box<dyn IdempotentProof>>,
140    Option<Box<dyn MonotoneProof>>,
141    PhantomData<(Commutative, Idempotent, Monotone)>,
142);
143
144impl<C, I, M> AggFuncAlgebra<C, I, M> {
145    /// Marks the function as being commutative, with the given proof mechanism.
146    pub fn commutative(
147        self,
148        proof: impl CommutativeProof + 'static,
149    ) -> AggFuncAlgebra<Proved, I, M> {
150        AggFuncAlgebra(Some(Box::new(proof)), self.1, self.2, PhantomData)
151    }
152
153    /// Marks the function as being idempotent, with the given proof mechanism.
154    pub fn idempotent(self, proof: impl IdempotentProof + 'static) -> AggFuncAlgebra<C, Proved, M> {
155        AggFuncAlgebra(self.0, Some(Box::new(proof)), self.2, PhantomData)
156    }
157
158    /// Marks the function as being monotone, with the given proof mechanism.
159    pub fn monotone(self, proof: impl MonotoneProof + 'static) -> AggFuncAlgebra<C, I, Proved> {
160        AggFuncAlgebra(self.0, self.1, Some(Box::new(proof)), PhantomData)
161    }
162
163    /// Registers the expression with the underlying proof mechanisms.
164    pub(crate) fn register_proof(self, expr: &syn::Expr) {
165        if let Some(comm_proof) = self.0 {
166            comm_proof.register_proof(expr);
167        }
168
169        if let Some(idem_proof) = self.1 {
170            idem_proof.register_proof(expr);
171        }
172
173        if let Some(monotone_proof) = self.2 {
174            monotone_proof.register_proof(expr);
175        }
176    }
177}
178
179impl<C, I, M> Property for AggFuncAlgebra<C, I, M> {
180    type Root = AggFuncAlgebra;
181
182    fn make_root(_target: &mut Option<Self>) -> Self::Root {
183        AggFuncAlgebra(None, None, None, PhantomData)
184    }
185}
186
187/// Algebraic properties for a singleton map function of type T -> U.
188///
189/// Order-preserving means that if the input grows monotonically, the output also grows monotonically.
190pub struct SingletonMapFuncAlgebra<
191    OrderPreserving = NotProved,
192    Commutative = NotProved,
193    Idempotent = NotProved,
194>(
195    Option<Box<dyn OrderPreservingProof>>,
196    Option<Box<dyn CommutativeProof>>,
197    Option<Box<dyn IdempotentProof>>,
198    PhantomData<(OrderPreserving, Commutative, Idempotent)>,
199);
200
201impl<O, C, I> SingletonMapFuncAlgebra<O, C, I> {
202    /// Marks the function as being order-preserving, with the given proof mechanism.
203    pub fn order_preserving(
204        self,
205        proof: impl OrderPreservingProof + 'static,
206    ) -> SingletonMapFuncAlgebra<Proved, C, I> {
207        SingletonMapFuncAlgebra(Some(Box::new(proof)), self.1, self.2, PhantomData)
208    }
209
210    /// Marks the function as being commutative, with the given proof mechanism.
211    pub fn commutative(
212        self,
213        proof: impl CommutativeProof + 'static,
214    ) -> SingletonMapFuncAlgebra<O, Proved, I> {
215        SingletonMapFuncAlgebra(self.0, Some(Box::new(proof)), self.2, PhantomData)
216    }
217
218    /// Marks the function as being idempotent, with the given proof mechanism.
219    pub fn idempotent(
220        self,
221        proof: impl IdempotentProof + 'static,
222    ) -> SingletonMapFuncAlgebra<O, C, Proved> {
223        SingletonMapFuncAlgebra(self.0, self.1, Some(Box::new(proof)), PhantomData)
224    }
225
226    /// Registers the expression with the underlying proof mechanisms.
227    pub(crate) fn register_proof(self, expr: &syn::Expr) {
228        if let Some(proof) = self.0 {
229            proof.register_proof(expr);
230        }
231    }
232}
233
234impl<O, C, I> Property for SingletonMapFuncAlgebra<O, C, I> {
235    type Root = SingletonMapFuncAlgebra;
236
237    fn make_root(_target: &mut Option<Self>) -> Self::Root {
238        SingletonMapFuncAlgebra(None, None, None, PhantomData)
239    }
240}
241
242/// Algebraic properties for a stream map function of type T -> U.
243pub struct StreamMapFuncAlgebra<Commutative = NotProved, Idempotent = NotProved>(
244    Option<Box<dyn CommutativeProof>>,
245    Option<Box<dyn IdempotentProof>>,
246    PhantomData<(Commutative, Idempotent)>,
247);
248
249impl<C, I> StreamMapFuncAlgebra<C, I> {
250    /// Marks the function as being commutative, with the given proof mechanism.
251    pub fn commutative(
252        self,
253        proof: impl CommutativeProof + 'static,
254    ) -> StreamMapFuncAlgebra<Proved, I> {
255        StreamMapFuncAlgebra(Some(Box::new(proof)), self.1, PhantomData)
256    }
257
258    /// Marks the function as being idempotent, with the given proof mechanism.
259    pub fn idempotent(
260        self,
261        proof: impl IdempotentProof + 'static,
262    ) -> StreamMapFuncAlgebra<C, Proved> {
263        StreamMapFuncAlgebra(self.0, Some(Box::new(proof)), PhantomData)
264    }
265
266    /// Registers the expression with the underlying proof mechanisms.
267    pub(crate) fn register_proof(self, expr: &syn::Expr) {
268        if let Some(proof) = self.0 {
269            proof.register_proof(expr);
270        }
271        if let Some(proof) = self.1 {
272            proof.register_proof(expr);
273        }
274    }
275}
276
277impl<C, I> Property for StreamMapFuncAlgebra<C, I> {
278    type Root = StreamMapFuncAlgebra;
279
280    fn make_root(_target: &mut Option<Self>) -> Self::Root {
281        StreamMapFuncAlgebra(None, None, PhantomData)
282    }
283}
284
285/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
286#[diagnostic::on_unimplemented(
287    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
288    label = "required for this call",
289    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."
290)]
291#[sealed::sealed]
292pub trait ValidCommutativityFor<O: Ordering> {}
293#[sealed::sealed]
294impl ValidCommutativityFor<TotalOrder> for NotProved {}
295#[sealed::sealed]
296impl<O: Ordering> ValidCommutativityFor<O> for Proved {}
297
298/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
299#[diagnostic::on_unimplemented(
300    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
301    label = "required for this call",
302    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
303)]
304#[sealed::sealed]
305pub trait ValidIdempotenceFor<R: Retries> {}
306#[sealed::sealed]
307impl ValidIdempotenceFor<ExactlyOnce> for NotProved {}
308#[sealed::sealed]
309impl<R: Retries> ValidIdempotenceFor<R> for Proved {}
310
311/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
312#[sealed::sealed]
313#[diagnostic::on_unimplemented(
314    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
315    label = "required for this call",
316    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."
317)]
318pub trait ValidMutCommutativityFor<F: FnMut(In) -> Out, In, Out, O: Ordering, const WAS_MUT: bool> {}
319#[sealed::sealed]
320impl<In, Out, F: FnMut(In) -> Out> ValidMutCommutativityFor<F, In, Out, TotalOrder, true>
321    for NotProved
322{
323}
324#[sealed::sealed]
325impl<In, Out, F: Fn(In) -> Out, O: Ordering> ValidMutCommutativityFor<F, In, Out, O, false>
326    for NotProved
327{
328}
329#[sealed::sealed]
330impl<In, Out, F: FnMut(In) -> Out, O: Ordering> ValidMutCommutativityFor<F, In, Out, O, true>
331    for Proved
332{
333}
334#[sealed::sealed]
335impl<In, Out, F: Fn(In) -> Out, O: Ordering> ValidMutCommutativityFor<F, In, Out, O, false>
336    for Proved
337{
338}
339
340/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
341#[diagnostic::on_unimplemented(
342    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
343    label = "required for this call",
344    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
345)]
346#[sealed::sealed]
347pub trait ValidMutIdempotenceFor<F: FnMut(In) -> Out, In, Out, R: Retries, const WAS_MUT: bool> {}
348#[sealed::sealed]
349impl<In, Out, F: FnMut(In) -> Out> ValidMutIdempotenceFor<F, In, Out, ExactlyOnce, true>
350    for NotProved
351{
352}
353#[sealed::sealed]
354impl<In, Out, F: Fn(In) -> Out, R: Retries> ValidMutIdempotenceFor<F, In, Out, R, false>
355    for NotProved
356{
357}
358#[sealed::sealed]
359impl<In, Out, F: FnMut(In) -> Out, R: Retries> ValidMutIdempotenceFor<F, In, Out, R, true>
360    for Proved
361{
362}
363#[sealed::sealed]
364impl<In, Out, F: Fn(In) -> Out, R: Retries> ValidMutIdempotenceFor<F, In, Out, R, false>
365    for Proved
366{
367}
368
369/// Marker trait for commutativity of closures that borrow their input (`FnMut(&In) -> Out`).
370#[sealed::sealed]
371#[diagnostic::on_unimplemented(
372    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
373    label = "required for this call",
374    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."
375)]
376pub trait ValidMutBorrowCommutativityFor<
377    F: FnMut(&In) -> Out,
378    In: ?Sized,
379    Out,
380    O: Ordering,
381    const WAS_MUT: bool,
382>
383{
384}
385#[sealed::sealed]
386impl<In: ?Sized, Out, F: FnMut(&In) -> Out>
387    ValidMutBorrowCommutativityFor<F, In, Out, TotalOrder, true> for NotProved
388{
389}
390#[sealed::sealed]
391impl<In: ?Sized, Out, F: Fn(&In) -> Out, O: Ordering>
392    ValidMutBorrowCommutativityFor<F, In, Out, O, false> for NotProved
393{
394}
395#[sealed::sealed]
396impl<In: ?Sized, Out, F: FnMut(&In) -> Out, O: Ordering>
397    ValidMutBorrowCommutativityFor<F, In, Out, O, true> for Proved
398{
399}
400#[sealed::sealed]
401impl<In: ?Sized, Out, F: Fn(&In) -> Out, O: Ordering>
402    ValidMutBorrowCommutativityFor<F, In, Out, O, false> for Proved
403{
404}
405
406/// Marker trait for idempotence of closures that borrow their input (`FnMut(&In) -> Out`).
407#[diagnostic::on_unimplemented(
408    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
409    label = "required for this call",
410    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
411)]
412#[sealed::sealed]
413pub trait ValidMutBorrowIdempotenceFor<
414    F: FnMut(&In) -> Out,
415    In: ?Sized,
416    Out,
417    R: Retries,
418    const WAS_MUT: bool,
419>
420{
421}
422#[sealed::sealed]
423impl<In: ?Sized, Out, F: FnMut(&In) -> Out>
424    ValidMutBorrowIdempotenceFor<F, In, Out, ExactlyOnce, true> for NotProved
425{
426}
427#[sealed::sealed]
428impl<In: ?Sized, Out, F: Fn(&In) -> Out, R: Retries>
429    ValidMutBorrowIdempotenceFor<F, In, Out, R, false> for NotProved
430{
431}
432#[sealed::sealed]
433impl<In: ?Sized, Out, F: FnMut(&In) -> Out, R: Retries>
434    ValidMutBorrowIdempotenceFor<F, In, Out, R, true> for Proved
435{
436}
437#[sealed::sealed]
438impl<In: ?Sized, Out, F: Fn(&In) -> Out, R: Retries>
439    ValidMutBorrowIdempotenceFor<F, In, Out, R, false> for Proved
440{
441}
442
443/// Marker trait identifying the boundedness of a singleton given a monotonicity property of
444/// an aggregation on a stream.
445#[sealed::sealed]
446pub trait ApplyMonotoneStream<P, B2: SingletonBound> {}
447
448#[sealed::sealed]
449impl<B: Boundedness> ApplyMonotoneStream<NotProved, B> for B {}
450
451#[sealed::sealed]
452impl<B: Boundedness> ApplyMonotoneStream<Proved, B::StreamToMonotone> for B {}
453
454/// Marker trait identifying the boundedness of a singleton given a monotonicity property of
455/// an aggregation on a keyed stream.
456#[sealed::sealed]
457pub trait ApplyMonotoneKeyedStream<P, B2: KeyedSingletonBound> {}
458
459#[sealed::sealed]
460impl<B: Boundedness> ApplyMonotoneKeyedStream<NotProved, B::KeyedStreamToNonMonotone> for B {}
461
462#[sealed::sealed]
463impl<B: Boundedness> ApplyMonotoneKeyedStream<Proved, B::KeyedStreamToMonotone> for B {}
464
465/// Marker trait identifying the boundedness of a singleton after a map operation,
466/// given an order-preserving property.
467#[sealed::sealed]
468pub trait ApplyOrderPreservingSingleton<P, B2: SingletonBound> {}
469
470#[sealed::sealed]
471impl<B: SingletonBound> ApplyOrderPreservingSingleton<NotProved, B::UnderlyingBound> for B {}
472
473#[sealed::sealed]
474impl<B: SingletonBound> ApplyOrderPreservingSingleton<Proved, B> for B {}
hydro_lang/properties/mod.rs

hydro_lang/properties/
mod.rs
