Use mapStmtExprChildrenM to simplify transformExpr

[keyboardDrummer-bot]

Addresses #40.

Summary

Adds mapStmtExprChildrenM to MapStmtExpr.lean — a utility that maps a function over the immediate children of a StmtExprMd node (one level, no recursion), with an optional reverseChildren flag for right-to-left traversal.

Uses it in LiftImperativeExpressions.lean to replace the explicit PrimitiveOp arm in transformExpr with a generic catch-all:

| _ => mapStmtExprChildrenM transformExpr (reverseChildren := true) expr

This means the pass no longer needs to enumerate language features it doesn't relate to. If a new StmtExpr constructor is added, it will be traversed automatically without updating transformExpr.

Changes

MapStmtExpr.lean:

• Add mapStmtExprChildrenM: one-level child mapping with optional right-to-left order
• Add mapStmtExprPrePostM: full traversal with pre/post hooks (useful for other passes)

LiftImperativeExpressions.lean:

• Remove explicit PrimitiveOp arm from transformExpr
• Replace catch-all | _ => return expr with mapStmtExprChildrenM transformExpr (reverseChildren := true) expr
• Add explicit | .Assert _ | .Assume _ => return expr since these are statement-like constructs lifted out of blocks and should not have substitutions applied
• Remove mutual block (no longer needed since transformStmt doesn't need mutual recursion with transformExpr)
• Mark transformExpr as partial since mapStmtExprChildrenM is opaque to the termination checker

Trade-off

The use of partial is a trade-off: we lose the termination proof for transformExpr in exchange for not needing to enumerate every constructor. The termination checker cannot see through mapStmtExprChildrenM to verify that transformExpr is only called on structurally smaller values. The original code avoided this by listing every constructor with .attach proofs.

Testing

All 591 test jobs pass.
"

[keyboardDrummer-bot]

I investigated the "Run internal benchmarks of Strata" CI failure. The benchmark job triggers an AWS CodeBuild build that runs internal tests.

Finding: This failure is not caused by the code changes in this PR. The same benchmark job is also failing on other unrelated PRs:

• PR Improve block formatting and diagnostic reporting #38 (formatting changes only) — benchmark failed
• PR Add EliminateReturnStatements and ContractPass #34 (contract pass) — benchmark failed

The benchmark infrastructure appears to have a pre-existing issue (likely AWS credentials, CodeBuild configuration, or the benchmark environment itself). The failure happens quickly (~100 seconds), suggesting it fails during setup or early build rather than during actual test execution.

Local verification:

• lake build ✅ (577 jobs, all successful)
• lake test ✅ (all tests pass; the one failure is an unrelated missing jar file for Java integration tests)
• All #guard_msgs tests pass, confirming the lift pass produces correct output