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
13/// A trait for proof mechanisms that can validate idempotence.
14#[sealed::sealed]
15pub trait IdempotentProof {}
16
17/// A hand-written human proof of the correctness property.
18pub struct ManualProof();
19#[sealed::sealed]
20impl CommutativeProof for ManualProof {}
21#[sealed::sealed]
22impl IdempotentProof for ManualProof {}
23
24/// Marks that the property is not proved.
25pub enum NotProved {}
26
27/// Marks that the property is proven.
28pub enum Proved {}
29
30/// Algebraic properties for an aggregation function of type (T, &mut A) -> ().
31///
32/// Commutativity:
33/// ```rust,ignore
34/// let mut state = ???;
35/// f(a, &mut state); f(b, &mut state) // produces same final state as
36/// f(b, &mut state); f(a, &mut state)
37/// ```
38///
39/// Idempotence:
40/// ```rust,ignore
41/// let mut state = ???;
42/// f(a, &mut state);
43/// let state1 = *state;
44/// f(a, &mut state);
45/// // state1 must be equal to state
46/// ```
47pub struct AggFuncAlgebra<Commutative = NotProved, Idempotent = NotProved>(
48    PhantomData<(Commutative, Idempotent)>,
49);
50impl<C, I> AggFuncAlgebra<C, I> {
51    /// Marks the function as being commutative, with the given proof mechanism.
52    pub fn commutative(self, _proof: impl CommutativeProof) -> AggFuncAlgebra<Proved, I> {
53        AggFuncAlgebra(PhantomData)
54    }
55
56    /// Marks the function as being idempotent, with the given proof mechanism.
57    pub fn idempotent(self, _proof: impl IdempotentProof) -> AggFuncAlgebra<C, Proved> {
58        AggFuncAlgebra(PhantomData)
59    }
60}
61
62impl<C, I> Property for AggFuncAlgebra<C, I> {
63    type Root = AggFuncAlgebra;
64
65    fn make_root(_target: &mut Option<Self>) -> Self::Root {
66        AggFuncAlgebra(PhantomData)
67    }
68}
69
70/// Marker trait identifying that the commutativity property is valid for the given stream ordering.
71#[diagnostic::on_unimplemented(
72    message = "Because the input stream has ordering `{O}`, the closure must demonstrate commutativity with a `commutative = ...` annotation.",
73    label = "required for this call"
74)]
75#[sealed::sealed]
76pub trait ValidCommutativityFor<O: Ordering> {}
77#[sealed::sealed]
78impl ValidCommutativityFor<TotalOrder> for NotProved {}
79#[sealed::sealed]
80impl<O: Ordering> ValidCommutativityFor<O> for Proved {}
81
82/// Marker trait identifying that the idempotence property is valid for the given stream ordering.
83#[diagnostic::on_unimplemented(
84    message = "Because the input stream has retries `{R}`, the closure must demonstrate idempotence with an `idempotent = ...` annotation.",
85    label = "required for this call"
86)]
87#[sealed::sealed]
88pub trait ValidIdempotenceFor<R: Retries> {}
89#[sealed::sealed]
90impl ValidIdempotenceFor<ExactlyOnce> for NotProved {}
91#[sealed::sealed]
92impl<R: Retries> ValidIdempotenceFor<R> for Proved {}
hydro_lang/properties/mod.rs

hydro_lang/properties/
mod.rs
