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

hydro_lang/properties/
mod.rs
