typechecker loop: disable OZ_Math directional summary when Math.Rounding is unresolvable

[jar-ben]

Problem

The scene-based OZ Math summary (OZ_Math-<Contract>.spec) emits an active directional
mulDiv summary that references the Math.Rounding enum type:

function Math.mulDiv(uint256 x, uint256 y, uint256 denominator, Math.Rounding rounding) internal
    returns (uint256) => mulDivDirectionalSummary(x, y, denominator, rounding);
...
function mulDivDirectionalSummary(...) returns uint256 {
    if (rounding == Math.Rounding.Ceil) { ... } else { ... }
}

Rounding is declared in the OZ Math library. In scenes where that library is inlined /
duplicated across compilation units, Math.Rounding is not a usable CVL enum type and no
contract re-declares it, so the typechecker rejects the reference:

Error in spec file (OZ_Math-ERC20.spec:12:21): could not type expression "Math.Rounding.Ceil",
message: In enum constant Math.Rounding.Ceil, Math.Rounding is not a valid enum type

Crucially this error carries no Did you mean suggestion (there is no valid alternative
qualifier), so the loop's existing ambiguous-Rounding requalification path has nothing to act
on. The generated spec fails to typecheck, breaking setup for the affected project.

Fix

Teach the typechecker loop to recognize and recover from this case
(certora_autosetup/typechecker_loop.py):

• Parse — a new pattern flags the no-suggestion X.Rounding is not a valid enum type error
  as ROUNDING_UNRESOLVABLE (kept distinct from the requalifiable ROUNDING_AMBIGUOUS case,
  which always carries suggestions).
• Recover — a new callback comments out each CVL function the error falls inside (reusing
  the existing AST-range block expansion, so a partially-commented function never remains) plus
  the methods{} entries that dispatch to those functions.

The recovery runs only when the typechecker offers no requalification, so scenes where
Math.Rounding — or a contract-qualified C.Rounding — does resolve are unchanged and keep the
directional summary.

Testing

• tests/test_typechecker_rounding_fix.py — added coverage: parsing the unresolvable error,
  guarding it against mis-classification as the ambiguous case (both directions), and the
  disable-directional callback. Full file: 12 passed.
• tests/test_oz_math_rounding_unit.py — 19 passed (module untouched).
• Reproduced the failure end-to-end on a real project's fetched scene and confirmed
  certoraRun --compilation_steps_only passes after the fix (certora-cli-beta 8.18.0).

🤖 Generated with Claude Code

[shellygr]

it probably happens in other functions but it's odd not to use the AST here too