Crate provable_contracts_macros 

provable-contracts-macros — compatibility facade

Renamed to aprender-contracts-macros during the APR-MONO consolidation. The five attribute macros (contract, requires, ensures, invariant, must_contract) are re-exported unchanged, so use provable_contracts_macros::requires; keeps resolving.

This crate is deliberately NOT proc-macro = true — a proc-macro crate may export nothing but its own #[proc_macro*] functions, so it cannot forward anyone else’s. A plain library re-exporting them works, and downstream code can still invoke them through this path; compat/invoke.rs compiles an invocation of each of the five to prove it.

Bound by contracts/provable-contracts-facade-v1.yaml.

Attribute Macros

contract

Compile-time contract enforcement attribute.

ensures

Postcondition: checked via debug_assert!() after function returns. The return value is bound to ret in the predicate. Zero runtime cost in release builds.

invariant

Invariant: checked via debug_assert!() both BEFORE and AFTER. Zero runtime cost in release builds.

must_contract

Marks a public function as requiring a #[contract] annotation.

requires

Precondition: checked via debug_assert!() at function entry. Zero runtime cost in release builds.