Expand description
Pure, allocation-free decisions shared by the UI’s asynchronous requests.
proofs/ proves the Charon/Aeneas translation of these exact modules.
Nominal pipeline tags, serialization, payload identity and effects live in
the application adapter; neither providers nor terminal IO enter this crate.
Modules§
- generation
- Monotonic request issuance. Exhaustion refuses instead of reusing an epoch.
- request
- A request accepts partial replies until exactly one terminal reply lands.