Module prelude 

A “prelude” for users of the hydro_lang crate.

This prelude is similar to the standard library’s prelude in that you’ll almost always want to import its entire contents, but unlike the standard library’s prelude you’ll have to do so manually:

use hydro_lang::prelude::*;

The prelude may grow over time as additional items see ubiquitous use.

Re-exports

pub use crate::compile::builder::FlowBuilder;

pub use crate::live_collections::boundedness::Bounded;

pub use crate::live_collections::boundedness::Unbounded;

pub use crate::live_collections::keyed_singleton::KeyedSingleton;

pub use crate::live_collections::keyed_singleton::MonotonicKeys;

pub use crate::live_collections::keyed_stream::KeyedStream;

pub use crate::live_collections::optional::InitNone;

pub use crate::live_collections::optional::Optional;

pub use crate::live_collections::singleton::Singleton;

pub use crate::live_collections::sliced::sliced;

pub use crate::live_collections::stream::Stream;

pub use crate::location::Cluster;

pub use crate::location::External;

pub use crate::location::Location as _;

pub use crate::location::Process;

pub use crate::location::Tick;

pub use crate::networking::TCP;

pub use crate::networking::UDP;

pub use crate::nondet::NonDet;

pub use crate::properties::ConsistencyProof;

pub use crate::properties::ManualProof;

pub use crate::properties::VerusCommutativeProof;

Macros

manual_proof

Fulfills a proof parameter by declaring a human-written justification for why the algebraic property (e.g. commutativity, idempotence) holds.

nondet

Fulfills a non-determinism guard parameter by declaring a reason why the non-determinism is tolerated or providing other non-determinism guards that forward the inner non-determinism.

q

Creates a quoted expression for Hydro.

verus_proof_commutative_effect

Fulfills a commutative = ... proof parameter for a unit-returning, effectful closure (shape |item| -> (), e.g. for for_each or inspect) that mutates a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity of the captured-state update.

verus_proof_commutative_filter

Fulfills a commutative = ... proof parameter for a filter predicate (shape |item| -> bool where item is received by reference) that may mutate a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity.

verus_proof_commutative_fold

Fulfills a commutative = ... proof parameter for an aggregation closure (fold / reduce, shape |acc, item| with acc: &mut A) with a Verus-checked proof of commutativity.

verus_proof_commutative_map

Fulfills a commutative = ... proof parameter for a map-like closure (shape |item| -> out, e.g. for map) that may mutate a captured singleton reference (from Singleton::by_mut), with a Verus-checked proof of commutativity.