Support a module mode that verifies the contained proofs are in EPR and if so, enables the mbqi quant. instantiation strategy

[GenericMonkey]

Changes

Attributes

• Add a module-level attribute #[verifier::epr_check] to run the EPR checker on all proofs in a particular module.
  • This module also enables options to turn on MBQI for the quantifiers in this module.
• Add verifier::inline_only attribute to suppress generation of the function body in the Verification Condition
• Add #![no_triggers] trigger annotation to produce an empty pattern. Together with pi.enabled this will effectively eliminate trigger based instantiation for the given quantifier (i.e. MBQI only)

EPR Core Logic

• Added new file alternation_check.rs that runs a 3 pass check for quantifier alternation.
  • First pass to check if all features used in module are supported in EPR
  • Second pass to collect all recursively mentioned spec functions
  • Third pass to construct the edges in the quantifier alternation graph
• Augment pruning logic in prune.rs to also return a boolean saying all reached types are opaque datatypes.
• Add a new EPR-friendly prelude that is produced when the module is decorated with epr_check

Testing

• Added epr.rs to test harness to test interesting cases of the quantifier alternation graph generation
• Add delmap_epr.rs to examples/ to further test feature and show an example of code organization around the EPR feature

[tjhance]

What's the difference between inline and inline_only? Is the original inline conditional on something?

[GenericMonkey]

What's the difference between inline and inline_only? Is the original inline conditional on something?

I think the original inline will not suppress the creation of the function definition in the VC. Since we care about reducing the QA graph by eliminating the function defn (defn(x) <==> body), we added this option.