fix(PythonToLaurel): Translate raise as exception instead of hole

[olivier-aws]

Fixes #874

Problem

raise statements in Python were translated as a deterministic Hole (<?>), which has Unknown type. The Laurel-to-Core translator rejects Unknown types with "could not infer type", causing an internal error when analyzing any function containing raise inside an except block.

Fix

Replace the Hole translation with three statements that model exception semantics:

1. maybe_except := <??> — havoc (non-deterministic Error value)
2. assume isError(maybe_except) — constrain to be a real error
3. exit <label> — exit to the catchers label (inside a try body) or exit the function (at top level)

A raiseExitLabel field is added to TranslationContext to track where raise should transfer control:

• Inside a try body → exit to the catchers/handlers label
• Inside a handler or at top level → exit the function ($body)

Each except handler is guarded by isError(maybe_except) & handler_matches_N where handler_matches_N is a non-deterministic boolean. This models that we don't know which handler matches the exception type (sound over-approximation). The handler clears the error after its body and exits the try block, so subsequent handlers are skipped on that path.

Translation example

Given this Python code:

class ErrorA(Exception):
    pass
class ErrorB(Exception):
    pass

def only_first_handler_matches() -> str:
    result: str = ""
    try:
        raise ErrorA("a")
        result = "unreachable"
    except ErrorA:
        result = "caught_a"
    except ErrorB:
        result = "caught_b"
    assert result == "caught_a"
    return result

The try/raise/except block is translated to the following Laurel IR (formatted for readability):

result := from_str("");
{
  // === Try body (catchers block) ===
  {
    maybe_except := <??>;                          // raise: havoc error
    if isError(maybe_except) then
      exit exception_handlers;                     // raise: jump to handlers
    assume isError(maybe_except);                  // raise: error is active
    if isError(maybe_except) then
      exit exception_handlers;                     // exception check
    exit exception_handlers;                       // raise always exits
    // ... unreachable code ...
    exit try_end                                   // normal completion (skipped)
  } exception_handlers;

  // === Handler 0: except ErrorA ===
  var handler_matches_0: bool := <??>;             // non-deterministic choice
  if isError(maybe_except) & handler_matches_0 then {
    result := from_str("caught_a");                // handler body
    maybe_except := NoError();                     // clear error (caught)
    exit try_end                                   // skip remaining handlers
  };

  // === Handler 1: except ErrorB ===
  var handler_matches_1: bool := <??>;             // non-deterministic choice
  if isError(maybe_except) & handler_matches_1 then {
    result := from_str("caught_b");                // handler body
    maybe_except := NoError();                     // clear error (caught)
    exit try_end                                   // skip remaining handlers
  }

  // Fall-through: no handler caught, error propagates
} try_end;

assert result == "caught_a";

The analysis explores all paths non-deterministically:

• Path where handler 0 fires → result = "caught_a" → assert passes ✅
• Path where handler 1 fires → result = "caught_b" → assert unknown ❓
• This is a sound over-approximation: we don't model exception types, so both handlers are considered possible matches.

Changes

• Strata/Languages/Python/PythonToLaurel.lean — core fix (raise translation + handler dispatch)
• StrataTest/Languages/Python/tests/test_raise_in_except.py — exact reproducer from Internal error when analyzing a Python function with raise #874
• StrataTest/Languages/Python/tests/test_raise_variants.py — edge cases (raise in try, bare re-raise, raise new in except, top-level raise)
• StrataTest/Languages/Python/tests/test_except_dispatch.py — soundness test for multiple handler dispatch
• Updated expected outputs for test_try_except, test_multiple_except, and others

Testing

All 156 pyAnalyzeLaurel tests pass. The exact reproducer from #874 now produces "Analysis success".