Boole frontend

[kondylidou]

Issue #, if available:

Description of changes:

Summary

This PR presents the Boole frontend end-to-end: grammar support, Boole-to-Core lowering, meta-verification integration, regression tests, and feature-request examples.

Boole is the IR for CSLib (Pillar 2). Boole is built on Strata Core and serves as a staging ground for Strata Core feature requests from the CSLib community. Not all of these may make it into Core, but we will strive to have Boole and Core share as many components as possible. This will allow both CSLib and Strata to make progress without blocking on each other (due to differences in philosophies, priorities, etc.) and to keep up with each other.

Main changes

• Added and refined the Boole frontend pipeline across parsing, lowering, and verification
• Integrated Boole programs with #strata, Core VC generation, and SMT-based checking
• Added Boole regression tests and moved Boole examples into StrataTest/Languages/Boole
• Added StrataTest/Languages/Boole/FeatureRequests/ with Boole-facing seeds for unsupported or partially supported features
• Added docs/BooleFeatureRequests.md to summarize the current Boole feature backlog and point to the example files

Structure

The PR touches the Boole frontend in four layers:

• grammar and surface syntax
• Boole-to-Core translation
• meta-verifier integration
• Boole tests and feature-request examples

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[joscoh]

Also, can you please add a more informative description to the PR that describes the changes, structure, tests, etc?

[kondylidou]

Elab.lean is not the ideal end state, but it is the best place for the compatibility of the Boole quantifier syntax. The dotted Unicode form is a legacy surface-syntax issue that needs to be normalized before the DDM parser commits to the canonical quantifier shape. Doing that in Elab.lean keeps HashCommands.lean generic and avoids Boole-specific preprocessing in #strata. Longer term, the cleaner solution would be native parser support for dotted Unicode quantifiers so no pre-parse rewrite is needed. @joscoh do you have a better suggestion?

[kondylidou]

@joscoh I decided to remove CoreBridge until a general better approach is found

[shigoel]

Also, can you please add a more informative description to the PR that describes the changes, structure, tests, etc?

Thanks for raising this, @joscoh. @kondylidou: I have one more suggestion. What do you think about the following addition?

Boole is the IR for CSLib (Pillar 2). Boole is being built atop Strata Core and serves as a staging ground for feature requests to Strata Core from the CSLib community. Not all of these may make into Core, but we will strive for Boole and Core to share as many components as possible. This will allow both CSLib and Strata to make progress without blocking on each other (due to differences in philosophies, priorities, etc.) and to keep up with each other.

[kondylidou]

@shigoel @joscoh I believe I have worked through all your comments, thanks a lot for the help. I also updated the pr description and cleaned up the code. Please let me know if anything is missing.