Separate type-checking, partial evaluation and ANF into Core-to-Core phases

[MikaelMayer]

Summary

Resolves #749. Separates the verification pipeline into distinct Core-to-Core phases: type checking, symbolic evaluation, and ANF encoding. Proof obligation extraction is a separate step on the final Core tree.

Problem

On main, the partial evaluator, type checker, and ANF deduplication are interleaved in a single evaluation pass. The ANF (common subexpression elimination) lives inside the SMT encoder as define-fun emission. This makes each concern harder to reason about, test, and extend independently.

Solution

The pipeline is now:

transforms → typeCheck → toCoreProofObligationProgram → ANFEncoder → ObligationExtraction → SMT Encoder

• Type checking and symbolic evaluation are proper PipelinePhase entries in the pipeline loop, with phase-specific error messages and source location propagation.
• Symbolic evaluation (toCoreProofObligationProgram) produces an obligations program: a Core program where each procedure body is a tree of assume/assert/if * blocks representing proof obligations, with function declarations and axioms inlined. Path conditions are emitted in logical order: spec-level preconditions first, then branch conditions (achieved by reversing the path condition stack before flattening). The obligation procedure uses the first procedure name as a representative label; downstream phases (ObligationExtraction) walk the body and ignore the header name.
• ANF encoding is a Core-to-Core transformation that extracts common subexpressions into var declarations using hash-based duplicate detection. Expression hashing uses shared per-constructor hash combiners (hashConst, hashBVar, hashFVar, hashOp, hashApp, hashIte, hashEqExpr, hashAbs, hashQuantExpr, hashOptTy) defined once in LExpr.lean and reused by hashExpr, replaceExprs, and collectSubexprHashes. Both replaceExprs and collectSubexprHashes compute hashes bottom-up, reusing child hashes from recursive calls to avoid redundant traversals. LConst derives Hashable so constants are hashed structurally rather than via toString. The phase returns false when no deduplication targets are found, enabling fixed-point convergence.
• Obligation extraction is a simple linear pass that extracts proof obligations with reconstructed path conditions. It accepts only the minimal Core subset produced by the PE and ANF phases: assume, assert, cover, var declarations, and nondet if *. Any other statement type produces an error. Path conditions can contain variable definitions (including ANF-generated ones).
• SMT encoder emits define-fun for ANF variable definitions (path condition entries starting with $__anf.), treating them as macro expansions rather than equality constraints. ANF variables are filtered from UF declarations, get-value ids, and model variable lists.

The pipeline error type is DiagnosticModel (not String), so source locations propagate through all phases.

API changes

• buildEvalEnv and buildSMTEnv combined into buildEnv with registerCustomFunctions : Bool parameter
• symbolicEval renamed to toCoreProofObligationProgram
• typeCheckAndEval restored to its original signature returning (List Env) × Statistics; the new typeCheckAndBuildObligationProgram returns Program × Statistics
• toSMTTermString renamed to toSMTCommandsWithAssert
• Statement.collectExprs simplified to return expressions directly (no collect parameter)
• ProofObligation.toSMTTerms now returns ANF definitions separately as ANFDefinition structs
• encodeCore accepts an anfDefinitions parameter for define-fun emission
• Statement.mapExprs refactored to delegate structural recursion to Stmt.mapExpr/Block.mapExpr (generic over command types) and command-level mapping to Command.mapExpr, reducing duplication
• SMT encoder builds lists in reverse and reverses at the end for O(n) list construction

Utilities

• Stmt.mapExpr, Block.mapExpr — generic expression mapping at the imperative layer, reusable across languages.
• Command.mapExpr — Core-specific command expression mapping.
• mapExprs, collectExprs on Statement — exhaustive (no catch-all patterns), non-partial, with a proved identity theorem (mapExprs_id).
• isLeaf, hasBVar, hashExpr moved to LExpr.lean.
• Per-constructor hash combiners extracted as standalone functions in LExpr.lean, shared across hashExpr and ANF encoder traversals.
• List.findDuplicates — generic duplicate detection utility in Strata/Util/List.lean.

[joscoh]

One question (about procName), the other comments are not blocking but would be nice.