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

hydro_lang/properties/
mod.rs
