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::stream::{ExactlyOnce, Ordering, Retries, TotalOrder};
8
9/// A trait for proof mechanisms that can validate commutativity.
10#[sealed::sealed]
11pub trait CommutativeProof {
12    /// Registers the expression with the proof mechanism.
13    ///
14    /// This should not perform any blocking analysis; it is only intended to record the expression for later processing.
15    fn register_proof(&self, expr: &syn::Expr);
16}
17
18/// A trait for proof mechanisms that can validate idempotence.
19#[sealed::sealed]
20pub trait IdempotentProof {
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
27/// A hand-written human proof of the correctness property.
28pub struct ManualProof();
29#[sealed::sealed]
30impl CommutativeProof for ManualProof {
31    fn register_proof(&self, _expr: &syn::Expr) {}
32}
33#[sealed::sealed]
34impl IdempotentProof for ManualProof {
35    fn register_proof(&self, _expr: &syn::Expr) {}
36}
37
38/// Marks that the property is not proved.
39pub enum NotProved {}
40
41/// Marks that the property is proven.
42pub enum Proved {}
43
44/// Algebraic properties for an aggregation function of type (T, &mut A) -> ().
45///
46/// Commutativity:
47/// ```rust,ignore
48/// let mut state = ???;
49/// f(a, &mut state); f(b, &mut state) // produces same final state as
50/// f(b, &mut state); f(a, &mut state)
51/// ```
52///
53/// Idempotence:
54/// ```rust,ignore
55/// let mut state = ???;
56/// f(a, &mut state);
57/// let state1 = *state;
58/// f(a, &mut state);
59/// // state1 must be equal to state
60/// ```
61pub struct AggFuncAlgebra<Commutative = NotProved, Idempotent = NotProved>(
62    Option<Box<dyn CommutativeProof>>,
63    Option<Box<dyn IdempotentProof>>,
64    PhantomData<(Commutative, Idempotent)>,
65);
66
67impl<C, I> AggFuncAlgebra<C, I> {
68    /// Marks the function as being commutative, with the given proof mechanism.
69    pub fn commutative(self, proof: impl CommutativeProof + 'static) -> AggFuncAlgebra<Proved, I> {
70        AggFuncAlgebra(Some(Box::new(proof)), self.1, PhantomData)
71    }
72
73    /// Marks the function as being idempotent, with the given proof mechanism.
74    pub fn idempotent(self, proof: impl IdempotentProof + 'static) -> AggFuncAlgebra<C, Proved> {
75        AggFuncAlgebra(self.0, Some(Box::new(proof)), PhantomData)
76    }
77
78    /// Registers the expression with the underlying proof mechanisms.
79    pub(crate) fn register_proof(self, expr: &syn::Expr) {
80        if let Some(comm_proof) = self.0 {
81            comm_proof.register_proof(expr);
82        }
83
84        if let Some(idem_proof) = self.1 {
85            idem_proof.register_proof(expr);
86        }
87    }
88}
89
90impl<C, I> Property for AggFuncAlgebra<C, I> {
91    type Root = AggFuncAlgebra;
92
93    fn make_root(_target: &mut Option<Self>) -> Self::Root {
94        AggFuncAlgebra(None, None, PhantomData)
95    }
96}
97
98/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
99#[diagnostic::on_unimplemented(
100    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
101    label = "required for this call",
102    note = "To intentionally process the stream with a non-deterministic (shuffled) order of elements, use `.assume_ordering`. This bypasses the safety guarantees so avoid unless necessary."
103)]
104#[sealed::sealed]
105pub trait ValidCommutativityFor<O: Ordering> {}
106#[sealed::sealed]
107impl ValidCommutativityFor<TotalOrder> for NotProved {}
108#[sealed::sealed]
109impl<O: Ordering> ValidCommutativityFor<O> for Proved {}
110
111/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
112#[diagnostic::on_unimplemented(
113    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
114    label = "required for this call",
115    note = "To intentionally process the stream with non-deterministic (randomly duplicated) retries, use `.assume_retries`. This bypasses the safety guarantees so avoid unless necessary."
116)]
117#[sealed::sealed]
118pub trait ValidIdempotenceFor<R: Retries> {}
119#[sealed::sealed]
120impl ValidIdempotenceFor<ExactlyOnce> for NotProved {}
121#[sealed::sealed]
122impl<R: Retries> ValidIdempotenceFor<R> for Proved {}
hydro_lang/properties/mod.rs

hydro_lang/properties/
mod.rs
