Proof search for stateful operation contracts #
stateful uses local contracts and the Stateful Aesop rule set. The initial rules cover pure
results and individual calls. Use Spec.CostHoare.bind with an intermediate contract and budgets
to expose sequencing obligations, and Spec.CostHoare.link to select an implementation.
Neither rule is applied blindly: its intermediate assertions or implementation are proof inputs.
This tactic proves the stated semantic or operation-cost contract. It does not reinterpret that
contract as total machine time; polytime certificates for controllers remain separate.
Main definitions #
stateful: search for a stateful contract using local facts and registered rules.
Prove a stateful semantic or operation-cost contract from compositional rules.