Changes in Boole after integrating `#strata_gen`

Stream: CSLib: Code Reasoning

[Lydia Kondylidou]

We replaced the old handwritten DDMTransform.Translate pipeline with the generated BooleDDM.* produced by #strata_gen.

Previously the pipeline was:

Strata.Program         (representation)
  → translateProgram   (handwritten parser/translation)
    → Boole.Program    (Boogie-style AST, handwritten)
      → toCoreProgram  (handwritten translation)
        → Core.Program (representation)
          → Core.verify

Here, Boole.Program was essentially a copy of the Boogie AST, and translateProgram was a handwritten parser that converted Lean syntax into that AST (largely duplicating Strata/Core parsing logic).

Now it is:

Strata.Program               (representation)
  → BooleDDM.Program.ofAst   (generated parser/translation)
    → BooleDDM.Program       (AST generated by #strata_gen)
      → toCoreProgram        (handwritten, WIP)
        → Core.Program       (representation)
          → Core.verify

Both translateProgram (before) and BooleDDM.Program.ofAst (now) act as parsers: they take Lean syntax and construct a Boole AST (Strata → Boole). The difference is that this step is now generated automatically. The only remaining handwritten step is toCoreProgram (BooleDDM → Core).

With this refactoring, we reuse the shared Strata generation/translation infrastructure instead of maintaining our own frontend translation logic, which reduces duplication and keeps Boole aligned with the common Strata architecture.