Reference Docs
This section collects Reference Documentation for the BlueRock's proof automation.
Contents
- DSL for defining hints
- Syntax for defining hints
- Tactics for arithmetics
- Automatic Fractional Splitting
- Using breakpoints
- The `verify` notation
- Join points
- Derive instances for BI predicates
- Common UNSAFE hints for `primR`
- Inlining during verification
- The `cpp.class` command
- The `cpp.enum` command
- The `cpp.spec` command
- Derive `Bwd` hints
- Derive `Cancel` hints
- Derive Eager unfolding hints
- Derive equivalences for predicates
- Derive `Fwd` hints
- Derive `Hint Opaque` annotations
- Derive Lazy unfolding hints