Improve exception logic for missing Python models

[keyboardDrummer]

Changes

• Improve handling of missing models by also assigning a hole to maybe_except
• Improve Laurel's type inference for holes

Testing

• Update expect file for test_missing_models

By submitting this pull request, I confirm that you can use, modify, copy, and redistribute this contribution, under the terms of your choice.

[keyboardDrummer]

@keyboardDrummer-bot can you resolve the conflicts and fix the build?

[keyboardDrummer-bot]

I've merged main into this branch to resolve the conflicts. The only conflict was in StrataTest/Languages/Python/expected_laurel/test_missing_models.expected — I took main's version since the output format changed significantly on main (new diagnostic format from #741 and #722).

Regarding the build failure: the PreludeVerifyTest was failing because the #guard_msgs assert IDs shifted (e.g. assert(40418) → assert(40420)). After merging main, the IDs are now different (main has 41770, 41837, 41945), and the PR's changes to InferHoleTypes.lean may shift them further. I can't determine the correct IDs without running the Lean build, so I'll wait for CI to report the actual values and then update the test.

Two things that will likely need updating once CI runs:

1. PreludeVerifyTest.lean — the assert(...) IDs in the #guard_msgs block will need to match the new output
2. test_missing_models.expected — this file currently has main's expected output, but the PR's behavioral changes (havoc maybe_except for unmodeled calls) may produce different results in the new format

I'll update both once CI reports the actual output.

[MikaelMayer]

Yes this is a good soundness fix.

[atomb]

I'm not sure I understand the translation of exceptions from Python well enough to be sure whether this is correct, but I noticed one place where the code and comment seem inconsistent.

[keyboardDrummer-bot]

The conflicts have already been resolved (from my earlier merge), and the build is now green — all 15 CI checks are passing ✅

There's one outstanding review comment from @atomb on InferHoleTypes.lean line 126 asking whether the pattern [tgt] should be tgt :: _ instead, since the comment says "first target's type" (implying it should work for multi-target assignments too, not just single-target ones). @keyboardDrummer — would you like me to make that change?

[keyboardDrummer-bot]

I've pushed the fix in draft PR #788 (targeting this branch):

1. Updated the comment to: -- Use the single target's type as the expected type for the value
2. Removed the redundant match targetType.val since defaultHoleType is already .Unknown, so the fallback was a no-op.
3. Inlined inferredType — now just passes targetType directly to inferExpr.

[atomb]

@keyboardDrummer-bot, can you fix the merge conflicts?

[keyboardDrummer-bot]

I've resolved the merge conflicts and pushed the fix. Here's what I did:

• Strata/Languages/Python/PythonToLaurel.lean: Combined changes from both branches — kept the exceptionCheck additions from main and the .Hole => holeExceptHavoc case from this branch.
• StrataTest/Languages/Python/PreludeVerifyTest.lean: Updated the assertion IDs (41900, 41967, 42075) to match the merged code.

The build and PreludeVerifyTest pass successfully. The only failing test (StrataTest.DDM.Integration.Java.TestGen) is a pre-existing issue due to a missing test data jar file, unrelated to this PR.

[keyboardDrummer-bot]

I've resolved the merge conflict by merging main into this branch. The conflict was in StrataTest/Languages/Python/PreludeVerifyTest.lean — the assertion IDs had shifted on both sides (42488/42555/42663 on this branch vs 43154/43221/43329 on main). I took main's IDs since they reflect the latest codebase.

Note: since this PR's code changes in PythonToLaurel.lean affect assertion numbering, the IDs in the expect file may need to be updated if CI fails. Please check the CI results.

[keyboardDrummer-bot]

The "Build and test Lean (stable)" CI failure was caused by stale assertion IDs in PreludeVerifyTest.lean. After the merge with main, the internal assertion numbering shifted by 2, so the #guard_msgs expected output no longer matched.

Fixed by updating the three assertion IDs: 43154→43156, 43221→43223, 43329→43331.

(The other failing check, DDM.Integration.Java.TestGen, is unrelated — it requires a ion-java jar that CI downloads separately.)

[keyboardDrummer-bot]

Responding to @tautschnig's two review comments. Both are good observations — the code duplication is straightforward to fix with a helper, and the path explosion in the test output is a consequence of the havoc-at-each-call-site approach. Deferring to @keyboardDrummer on whether to proceed with both changes.

[keyboardDrummer]

@keyboardDrummer-bot please resolve merge conflicts

[keyboardDrummer-bot]

Merge conflicts resolved and pushed.

The conflict was in Strata/Languages/Python/PythonToLaurel.lean — PR #769 (merged to main) moved the md field from Procedure into the Identifier name field. The two compositeToString procedure constructions in this PR still had md := md at the Procedure level, which I removed since that field no longer exists. The name field already carries md := .empty from the main branch changes.

Build passes locally (492/492 jobs).

[github-actions]

👋 Hi, @keyboardDrummer,
I detected conflicts against the base branch 🙊
You'll want to sync 🔄 your branch with upstream!

---

This message is automatically generated by prince-chrismc/label-merge-conflicts-action so don't hesitate to report issues/improvements there.

[tautschnig]

@keyboardDrummer-bot please resolve merge conflicts.

[keyboardDrummer-bot]

Merge conflicts resolved. There was one conflict in StrataTest/Languages/Python/PreludeVerifyTest.lean — the assert obligation IDs (43156, 43223, 43331 on the branch vs 43079, 43146, 43254 on main) were both stale after the merge. I rebuilt the test to get the correct post-merge IDs (43081, 43148, 43256) and updated the expect file accordingly. Build passes locally.

[keyboardDrummer-bot]

The branch is already up to date with main — no merge conflicts to resolve (the automated conflict bot message may have been stale).

I addressed @tautschnig's review comments:

1. PythonToLaurel.lean line 1400 — Added a comment explaining why exceptionCheck is dropped for the .Hole arm (pushed in 540fae2).
2. PreludeVerifyTest.lean line 197 — The fragile byte-offset assertion IDs are a pre-existing issue, not introduced by this PR. Deferred to @keyboardDrummer on whether to track separately.

Build passes (101/101 jobs).

[keyboardDrummer-bot]

The branch is already up to date with main — no merge conflicts to resolve. The merge base (5096a68) matches main's tip, and all 17 CI checks are passing ✅

The open review thread on PythonToLaurel.lean line 1060 (extracting a shared helper for the exceptHavoc pattern) is pending a decision from @keyboardDrummer — he indicated he'd prefer not to add a helper for such a small amount of code, and @tautschnig noted the risk is mainly about future evolution. @keyboardDrummer, would you like to resolve that thread or should I extract the helper?

[MikaelMayer]

Havoc-ing maybeExcept is a rightful soundness fix.