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};
11use crate::sim_hooks::OrderingHook;
12
13/// A trait for proof mechanisms that can validate commutativity.
14///
15/// `T` and `B` name the element type and boundedness of the stream the commutative
16/// function consumes. The simulator does not trust commutativity proofs — it still
17/// explores the input ordering — so a proof may carry an [`OrderingHook`] for scripting
18/// that exploration, surfaced through [`Self::take_hook`].
19#[sealed::sealed]
20pub trait CommutativeProof<T, B: Boundedness> {
21    /// Registers the expression with the proof mechanism.
22    ///
23    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
24    fn register_proof(&self, expr: &syn::Expr);
25
26    /// Takes the simulator ordering hook attached to this proof, if any.
27    fn take_hook(&mut self) -> Option<OrderingHook<T, B>>;
28}
29
30/// A trait for proof mechanisms that can validate idempotence.
31#[sealed::sealed]
32pub trait IdempotentProof {
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 monotonicity.
40#[sealed::sealed]
41pub trait MonotoneProof {
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 order-preservation (monotonicity of a map function).
49#[sealed::sealed]
50pub trait OrderPreservingProof {
51    /// Registers the expression with the proof mechanism.
52    ///
53    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
54    fn register_proof(&self, expr: &syn::Expr);
55}
56
57/// A trait for proof mechanisms that can validate consistency of a collection.
58#[sealed::sealed]
59pub trait ConsistencyProof {}
60
61/// A hand-written human proof of the correctness property.
62///
63/// To create a manual proof, use the [`manual_proof!`] macro, which takes in a doc comment
64/// explaining why the property holds.
65///
66/// Manual proofs are not trusted by the simulator, which still explores the guarded
67/// non-determinism. `H` is the simulator hook payload (like [`crate::nondet::NonDet`]) so a
68/// commutativity proof can carry an ordering hook for scripting that exploration.
69pub struct ManualProof<H = ()> {
70    hook: H,
71}
72
73impl<H> ManualProof<H> {
74    #[doc(hidden)]
75    pub fn unhooked() -> Self
76    where
77        H: Default,
78    {
79        ManualProof { hook: H::default() }
80    }
81}
82
83impl<T, B: Boundedness> ManualProof<Option<OrderingHook<T, B>>> {
84    #[doc(hidden)]
85    pub fn hooked(hook: impl Into<Option<OrderingHook<T, B>>>) -> Self {
86        ManualProof { hook: hook.into() }
87    }
88}
89
90#[sealed::sealed]
91impl<T, B: Boundedness> CommutativeProof<T, B> for ManualProof<Option<OrderingHook<T, B>>> {
92    fn register_proof(&self, _expr: &syn::Expr) {}
93
94    fn take_hook(&mut self) -> Option<OrderingHook<T, B>> {
95        self.hook.take()
96    }
97}
98
99#[sealed::sealed]
100impl<T, B: Boundedness> CommutativeProof<T, B> for ManualProof {
101    fn register_proof(&self, _expr: &syn::Expr) {}
102
103    fn take_hook(&mut self) -> Option<OrderingHook<T, B>> {
104        None
105    }
106}
107#[sealed::sealed]
108impl IdempotentProof for ManualProof {
109    fn register_proof(&self, _expr: &syn::Expr) {}
110}
111#[sealed::sealed]
112impl MonotoneProof for ManualProof {
113    fn register_proof(&self, _expr: &syn::Expr) {}
114}
115#[sealed::sealed]
116impl OrderPreservingProof for ManualProof {
117    fn register_proof(&self, _expr: &syn::Expr) {}
118}
119#[sealed::sealed]
120impl ConsistencyProof for ManualProof {}
121
122#[doc(inline)]
123pub use crate::__manual_proof__ as manual_proof;
124
125#[macro_export]
126/// Fulfills a proof parameter by declaring a human-written justification for why
127/// the algebraic property (e.g. commutativity, idempotence) holds.
128///
129/// The argument must be a doc comment explaining why the property is satisfied.
130///
131/// # Examples
132/// ```rust
133/// # #[cfg(feature = "deploy")] {
134/// # use hydro_lang::prelude::*;
135/// # use hydro_lang::live_collections::stream::NoOrder;
136/// # use futures::StreamExt;
137/// # tokio_test::block_on(hydro_lang::test_util::stream_transform_test(|process| {
138/// # let stream = process.source_iter(q!(vec![1, 2, 3])).weaken_ordering::<NoOrder>();
139/// // stream: [1, 2, 3] (unordered)
140/// stream
141///     .fold(
142///         q!(|| 0),
143///         q!(
144///             |acc, x| *acc += x,
145///             commutative = manual_proof!(/** integer addition is commutative */)
146///         ),
147///     )
148///     .into_stream()
149/// # }, |mut stream| async move {
150/// # assert_eq!(stream.next().await.unwrap(), 6);
151/// # }));
152/// # }
153/// ```
154/// An optional trailing `hook = ...` argument attaches a **simulator ordering hook** to a
155/// commutativity proof (see `hydro_lang::sim::hooks`). The simulator does not trust manual
156/// proofs — it still explores the input ordering — so the hook lets a simulation test
157/// script that exploration:
158///
159/// ```rust,ignore
160/// commutative = manual_proof!(/** set insert is commutative */ hook = my_ordering_hook)
161/// ```
162macro_rules! __manual_proof__ {
163    ($(#[doc = $doc:expr])+hook = $hook:expr $(,)?) => {
164        $crate::properties::ManualProof::hooked($hook)
165    };
166    ($(#[doc = $doc:expr])+) => {
167        $crate::properties::ManualProof::<()>::unhooked()
168    };
169}
170
171/// Marks that the property is not proved.
172pub enum NotProved {}
173
174/// Marks that the property is proven.
175pub enum Proved {}
176
177/// Algebraic properties for an aggregation function of type (T, &mut A) -> ().
178///
179/// Commutativity:
180/// ```rust,ignore
181/// let mut state = ???;
182/// f(a, &mut state); f(b, &mut state) // produces same final state as
183/// f(b, &mut state); f(a, &mut state)
184/// ```
185///
186/// Idempotence:
187/// ```rust,ignore
188/// let mut state = ???;
189/// f(a, &mut state);
190/// let state1 = *state;
191/// f(a, &mut state);
192/// // state1 must be equal to state
193/// ```
194pub struct AggFuncAlgebra<
195    T = (),
196    B: Boundedness = crate::live_collections::boundedness::Unbounded,
197    Commutative = NotProved,
198    Idempotent = NotProved,
199    Monotone = NotProved,
200>(
201    Option<Box<dyn CommutativeProof<T, B>>>,
202    Option<Box<dyn IdempotentProof>>,
203    Option<Box<dyn MonotoneProof>>,
204    PhantomData<(Commutative, Idempotent, Monotone)>,
205);
206
207impl<T, B: Boundedness, C, I, M> AggFuncAlgebra<T, B, C, I, M> {
208    /// Marks the function as being commutative, with the given proof mechanism.
209    pub fn commutative(
210        self,
211        proof: impl CommutativeProof<T, B> + 'static,
212    ) -> AggFuncAlgebra<T, B, Proved, I, M> {
213        AggFuncAlgebra(Some(Box::new(proof)), self.1, self.2, PhantomData)
214    }
215
216    /// Marks the function as being idempotent, with the given proof mechanism.
217    pub fn idempotent(
218        self,
219        proof: impl IdempotentProof + 'static,
220    ) -> AggFuncAlgebra<T, B, C, Proved, M> {
221        AggFuncAlgebra(self.0, Some(Box::new(proof)), self.2, PhantomData)
222    }
223
224    /// Marks the function as being monotone, with the given proof mechanism.
225    pub fn monotone(
226        self,
227        proof: impl MonotoneProof + 'static,
228    ) -> AggFuncAlgebra<T, B, C, I, Proved> {
229        AggFuncAlgebra(self.0, self.1, Some(Box::new(proof)), PhantomData)
230    }
231
232    /// Registers the expression with the underlying proof mechanisms, and takes the
233    /// simulator ordering hook attached to the commutativity proof, if any.
234    pub(crate) fn register_proof(self, expr: &syn::Expr) -> Option<OrderingHook<T, B>> {
235        let mut hook = None;
236        if let Some(mut comm_proof) = self.0 {
237            comm_proof.register_proof(expr);
238            hook = comm_proof.take_hook();
239        }
240
241        if let Some(idem_proof) = self.1 {
242            idem_proof.register_proof(expr);
243        }
244
245        if let Some(monotone_proof) = self.2 {
246            monotone_proof.register_proof(expr);
247        }
248
249        hook
250    }
251}
252
253impl<T, B: Boundedness, C, I, M> Property for AggFuncAlgebra<T, B, C, I, M> {
254    type Root = AggFuncAlgebra<T, B>;
255
256    fn make_root(_target: &mut Option<Self>) -> Self::Root {
257        AggFuncAlgebra(None, None, None, PhantomData)
258    }
259}
260
261/// Algebraic properties for a singleton map function of type T -> U.
262///
263/// Order-preserving means that if the input grows monotonically, the output also grows monotonically.
264pub struct SingletonMapFuncAlgebra<
265    T = (),
266    B: Boundedness = crate::live_collections::boundedness::Unbounded,
267    OrderPreserving = NotProved,
268    Commutative = NotProved,
269    Idempotent = NotProved,
270>(
271    Option<Box<dyn OrderPreservingProof>>,
272    Option<Box<dyn CommutativeProof<T, B>>>,
273    Option<Box<dyn IdempotentProof>>,
274    PhantomData<(OrderPreserving, Commutative, Idempotent)>,
275);
276
277impl<T, B: Boundedness, O, C, I> SingletonMapFuncAlgebra<T, B, O, C, I> {
278    /// Marks the function as being order-preserving, with the given proof mechanism.
279    pub fn order_preserving(
280        self,
281        proof: impl OrderPreservingProof + 'static,
282    ) -> SingletonMapFuncAlgebra<T, B, Proved, C, I> {
283        SingletonMapFuncAlgebra(Some(Box::new(proof)), self.1, self.2, PhantomData)
284    }
285
286    /// Marks the function as being commutative, with the given proof mechanism.
287    pub fn commutative(
288        self,
289        proof: impl CommutativeProof<T, B> + 'static,
290    ) -> SingletonMapFuncAlgebra<T, B, O, Proved, I> {
291        SingletonMapFuncAlgebra(self.0, Some(Box::new(proof)), self.2, PhantomData)
292    }
293
294    /// Marks the function as being idempotent, with the given proof mechanism.
295    pub fn idempotent(
296        self,
297        proof: impl IdempotentProof + 'static,
298    ) -> SingletonMapFuncAlgebra<T, B, O, C, Proved> {
299        SingletonMapFuncAlgebra(self.0, self.1, Some(Box::new(proof)), PhantomData)
300    }
301
302    /// Registers the expression with the underlying proof mechanisms, and takes the
303    /// simulator ordering hook attached to the commutativity proof, if any.
304    pub(crate) fn register_proof(self, expr: &syn::Expr) -> Option<OrderingHook<T, B>> {
305        if let Some(proof) = self.0 {
306            proof.register_proof(expr);
307        }
308        self.1.and_then(|mut proof| {
309            proof.register_proof(expr);
310            proof.take_hook()
311        })
312    }
313}
314
315impl<T, B: Boundedness, O, C, I> Property for SingletonMapFuncAlgebra<T, B, O, C, I> {
316    type Root = SingletonMapFuncAlgebra<T, B>;
317
318    fn make_root(_target: &mut Option<Self>) -> Self::Root {
319        SingletonMapFuncAlgebra(None, None, None, PhantomData)
320    }
321}
322
323/// Algebraic properties for a stream map function of type T -> U.
324pub struct StreamMapFuncAlgebra<
325    T = (),
326    B: Boundedness = crate::live_collections::boundedness::Unbounded,
327    Commutative = NotProved,
328    Idempotent = NotProved,
329>(
330    Option<Box<dyn CommutativeProof<T, B>>>,
331    Option<Box<dyn IdempotentProof>>,
332    PhantomData<(Commutative, Idempotent)>,
333);
334
335impl<T, B: Boundedness, C, I> StreamMapFuncAlgebra<T, B, C, I> {
336    /// Marks the function as being commutative, with the given proof mechanism.
337    pub fn commutative(
338        self,
339        proof: impl CommutativeProof<T, B> + 'static,
340    ) -> StreamMapFuncAlgebra<T, B, Proved, I> {
341        StreamMapFuncAlgebra(Some(Box::new(proof)), self.1, PhantomData)
342    }
343
344    /// Marks the function as being idempotent, with the given proof mechanism.
345    pub fn idempotent(
346        self,
347        proof: impl IdempotentProof + 'static,
348    ) -> StreamMapFuncAlgebra<T, B, C, Proved> {
349        StreamMapFuncAlgebra(self.0, Some(Box::new(proof)), PhantomData)
350    }
351
352    /// Registers the expression with the underlying proof mechanisms, and takes the
353    /// simulator ordering hook attached to the commutativity proof, if any.
354    pub(crate) fn register_proof(self, expr: &syn::Expr) -> Option<OrderingHook<T, B>> {
355        let hook = self.0.and_then(|mut proof| {
356            proof.register_proof(expr);
357            proof.take_hook()
358        });
359        if let Some(proof) = self.1 {
360            proof.register_proof(expr);
361        }
362        hook
363    }
364}
365
366impl<T, B: Boundedness, C, I> Property for StreamMapFuncAlgebra<T, B, C, I> {
367    type Root = StreamMapFuncAlgebra<T, B>;
368
369    fn make_root(_target: &mut Option<Self>) -> Self::Root {
370        StreamMapFuncAlgebra(None, None, PhantomData)
371    }
372}
373
374/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
375#[diagnostic::on_unimplemented(
376    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
377    label = "required for this call",
378    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."
379)]
380#[sealed::sealed]
381pub trait ValidCommutativityFor<O: Ordering> {}
382#[sealed::sealed]
383impl ValidCommutativityFor<TotalOrder> for NotProved {}
384#[sealed::sealed]
385impl<O: Ordering> ValidCommutativityFor<O> for Proved {}
386
387/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
388#[diagnostic::on_unimplemented(
389    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
390    label = "required for this call",
391    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
392)]
393#[sealed::sealed]
394pub trait ValidIdempotenceFor<R: Retries> {}
395#[sealed::sealed]
396impl ValidIdempotenceFor<ExactlyOnce> for NotProved {}
397#[sealed::sealed]
398impl<R: Retries> ValidIdempotenceFor<R> for Proved {}
399
400/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
401#[sealed::sealed]
402#[diagnostic::on_unimplemented(
403    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
404    label = "required for this call",
405    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."
406)]
407pub trait ValidMutCommutativityFor<F: FnMut(In) -> Out, In, Out, O: Ordering, const WAS_MUT: bool> {}
408#[sealed::sealed]
409impl<In, Out, F: FnMut(In) -> Out> ValidMutCommutativityFor<F, In, Out, TotalOrder, true>
410    for NotProved
411{
412}
413#[sealed::sealed]
414impl<In, Out, F: Fn(In) -> Out, O: Ordering> ValidMutCommutativityFor<F, In, Out, O, false>
415    for NotProved
416{
417}
418#[sealed::sealed]
419impl<In, Out, F: FnMut(In) -> Out, O: Ordering> ValidMutCommutativityFor<F, In, Out, O, true>
420    for Proved
421{
422}
423#[sealed::sealed]
424impl<In, Out, F: Fn(In) -> Out, O: Ordering> ValidMutCommutativityFor<F, In, Out, O, false>
425    for Proved
426{
427}
428
429/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
430#[diagnostic::on_unimplemented(
431    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
432    label = "required for this call",
433    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
434)]
435#[sealed::sealed]
436pub trait ValidMutIdempotenceFor<F: FnMut(In) -> Out, In, Out, R: Retries, const WAS_MUT: bool> {}
437#[sealed::sealed]
438impl<In, Out, F: FnMut(In) -> Out> ValidMutIdempotenceFor<F, In, Out, ExactlyOnce, true>
439    for NotProved
440{
441}
442#[sealed::sealed]
443impl<In, Out, F: Fn(In) -> Out, R: Retries> ValidMutIdempotenceFor<F, In, Out, R, false>
444    for NotProved
445{
446}
447#[sealed::sealed]
448impl<In, Out, F: FnMut(In) -> Out, R: Retries> ValidMutIdempotenceFor<F, In, Out, R, true>
449    for Proved
450{
451}
452#[sealed::sealed]
453impl<In, Out, F: Fn(In) -> Out, R: Retries> ValidMutIdempotenceFor<F, In, Out, R, false>
454    for Proved
455{
456}
457
458/// Marker trait for commutativity of closures that borrow their input (`FnMut(&In) -> Out`).
459#[sealed::sealed]
460#[diagnostic::on_unimplemented(
461    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
462    label = "required for this call",
463    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."
464)]
465pub trait ValidMutBorrowCommutativityFor<
466    F: FnMut(&In) -> Out,
467    In: ?Sized,
468    Out,
469    O: Ordering,
470    const WAS_MUT: bool,
471>
472{
473}
474#[sealed::sealed]
475impl<In: ?Sized, Out, F: FnMut(&In) -> Out>
476    ValidMutBorrowCommutativityFor<F, In, Out, TotalOrder, true> for NotProved
477{
478}
479#[sealed::sealed]
480impl<In: ?Sized, Out, F: Fn(&In) -> Out, O: Ordering>
481    ValidMutBorrowCommutativityFor<F, In, Out, O, false> for NotProved
482{
483}
484#[sealed::sealed]
485impl<In: ?Sized, Out, F: FnMut(&In) -> Out, O: Ordering>
486    ValidMutBorrowCommutativityFor<F, In, Out, O, true> for Proved
487{
488}
489#[sealed::sealed]
490impl<In: ?Sized, Out, F: Fn(&In) -> Out, O: Ordering>
491    ValidMutBorrowCommutativityFor<F, In, Out, O, false> for Proved
492{
493}
494
495/// Marker trait for idempotence of closures that borrow their input (`FnMut(&In) -> Out`).
496#[diagnostic::on_unimplemented(
497    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
498    label = "required for this call",
499    note = "To intentionally process the stream by observing non-deterministic (randomly duplicated) retries, use `.assume_retries`. This introduces non-determinism so avoid unless necessary."
500)]
501#[sealed::sealed]
502pub trait ValidMutBorrowIdempotenceFor<
503    F: FnMut(&In) -> Out,
504    In: ?Sized,
505    Out,
506    R: Retries,
507    const WAS_MUT: bool,
508>
509{
510}
511#[sealed::sealed]
512impl<In: ?Sized, Out, F: FnMut(&In) -> Out>
513    ValidMutBorrowIdempotenceFor<F, In, Out, ExactlyOnce, true> for NotProved
514{
515}
516#[sealed::sealed]
517impl<In: ?Sized, Out, F: Fn(&In) -> Out, R: Retries>
518    ValidMutBorrowIdempotenceFor<F, In, Out, R, false> for NotProved
519{
520}
521#[sealed::sealed]
522impl<In: ?Sized, Out, F: FnMut(&In) -> Out, R: Retries>
523    ValidMutBorrowIdempotenceFor<F, In, Out, R, true> for Proved
524{
525}
526#[sealed::sealed]
527impl<In: ?Sized, Out, F: Fn(&In) -> Out, R: Retries>
528    ValidMutBorrowIdempotenceFor<F, In, Out, R, false> for Proved
529{
530}
531
532/// Marker trait identifying the boundedness of a singleton given a monotonicity property of
533/// an aggregation on a stream.
534#[sealed::sealed]
535pub trait ApplyMonotoneStream<P, B2: SingletonBound> {}
536
537#[sealed::sealed]
538impl<B: Boundedness> ApplyMonotoneStream<NotProved, B> for B {}
539
540#[sealed::sealed]
541impl<B: Boundedness> ApplyMonotoneStream<Proved, B::StreamToMonotone> for B {}
542
543/// Marker trait identifying the boundedness of a singleton given a monotonicity property of
544/// an aggregation on a keyed stream.
545#[sealed::sealed]
546pub trait ApplyMonotoneKeyedStream<P, B2: KeyedSingletonBound> {}
547
548#[sealed::sealed]
549impl<B: Boundedness> ApplyMonotoneKeyedStream<NotProved, B::KeyedStreamToNonMonotone> for B {}
550
551#[sealed::sealed]
552impl<B: Boundedness> ApplyMonotoneKeyedStream<Proved, B::KeyedStreamToMonotone> for B {}
553
554/// Marker trait identifying the boundedness of a singleton after a map operation,
555/// given an order-preserving property.
556#[sealed::sealed]
557pub trait ApplyOrderPreservingSingleton<P, B2: SingletonBound> {}
558
559#[sealed::sealed]
560impl<B: SingletonBound> ApplyOrderPreservingSingleton<NotProved, B::UnderlyingBound> for B {}
561
562#[sealed::sealed]
563impl<B: SingletonBound> ApplyOrderPreservingSingleton<Proved, B> for B {}
hydro_lang/properties/mod.rs

hydro_lang/properties/
mod.rs
