Crate aristo 

Aristo SDK — annotation macros and verification.

This is the meta-crate. Downstream users add aristo to their Cargo.toml and receive the proc-macros (#[aristo::intent], #[aristo::assume], aristo::intent_stmt!(), aristo::assume_stmt!()) via re-export. Shared types from aristo-core are re-exported as that crate’s public API stabilizes.

Why a meta-crate: per K2 / K3 the canonical implementation is the Rust aristo-cli binary; the proc-macro work happens in aristo-macros; the types live in aristo-core. Downstream users should not need to learn that split — they depend on aristo and get everything they need.

Modules

instrument

aristo::instrument — Phase 2 surface for making private state observable to verification harnesses. Three proc-macros (Inspect, expose_pub, yield_point) re-exported from aristo-macros, plus a thread-local runtime hook (set_hook + __yield_point) defined inline because a proc-macro = true crate can’t export non-macro items and aristo-core already depends on this crate.

Macros

assume_stmt

aristo::assume_stmt!("...", parent = ..., id = ...);

intent_stmt

aristo::intent_stmt!("...", verify = ..., parent = ..., id = ...);

Attribute Macros

assume

#[aristo::assume("...", parent = ..., id = ...)]

intent

#[aristo::intent("...", verify = ..., parent = ..., id = ...)]