Verification Frontend
====================

BooleanProgram
--------------

**Location**: ``lib/Verification/Frontend/BooleanProgram/``

**Status**: Internal/Experimental — not exposed via any production tool.

A parser+lowerer for a Boolean/predicate program specification language
(Bebop/SATABS-style). Reads a textual format where programs consist of
predicates with procedures, control-flow statements, and BooleanExpr terms.
Lowers parsed programs to the NPA dataflow framework via
``PredicateProgramLowering``.

**Components**:
- ``BooleanProgramParser`` — recursive-descent parser (hand-written)
- ``BooleanProgram`` — AST data structures (Procedure, Statement, BooleanExpr, etc.)
- ``PredicateProgramLowering`` — lowers to NPA ``PredicateRelation``-based CFG

Only linked by unit tests (``boolean_program_frontend_test``).