Fix self.field.method() calls bypassing dispatch resolution (#1085)

Fixes #1082

`self.field.method()` calls inside class methods were bypassing dispatch
resolution. The type inference for `self` fell through to `Package`, so
chained calls like `self.store.put_item(...)` were flattened into
underscore-separated package calls instead of resolving through the
field's type and dispatching to the correct spec.

The fix registers `self` with the current class name in `variableTypes`
during method body translation, so `inferExprType` can resolve `self` →
class → field type → correct method dispatch.

Tested with a new end-to-end test that verifies `self.store.put_item()`
correctly dispatches through the Storage spec and detects a precondition
violation. Existing tests pass.

Author: MikaelMayer

Strata/Languages/Python/PythonToLaurel.lean

@@ -2213,6 +2213,9 @@ def translateFunction (ctx : TranslationContext) (sourceRange: SourceRange) (fun
     let inputTypes := funcDecl.args.map fun arg =>
       (arg.name, highTypeToPyLauType arg.laurelType.val)
     let ctx := {ctx with variableTypes:= ("nullcall_ret", PyLauType.Any)::inputTypes}
+    let ctx := match ctx.currentClassName with
+      | some cn => {ctx with variableTypes := ("self", cn) :: ctx.variableTypes}
+      | none => ctx
     let (bodyTrans, newCtx) ← match body with
     | some body =>
         let (bodyBlock, newCtx) ←  translateFunctionBody ctx funcDecl.kwargsName inputs body

StrataTestExtra/Languages/Python/AnalyzeLaurelTest.lean

@@ -383,4 +383,29 @@ recursively translates subclasses, so the type
       let msgs := result.errors.toList.map (·.message)
       throw <| IO.userError s!"Resolution errors after FilterPrelude:\n{"\n".intercalate msgs}"
 
+/-! ## Self-field dispatch test
+
+Verifies that `self.field.method()` inside a class method resolves through
+dispatch rather than being flattened to an underscore-separated package call.
+Without the fix, `self.store.put_item(...)` would produce a Hole instead of
+invoking the Storage spec, so precondition violations would go undetected. -/
+
+#eval withPython fun pythonCmd => do
+  IO.FS.withTempDir fun tmpDir => do
+    setupFixture pythonCmd tmpDir
+    let result ← runAnalyzeAndVerify pythonCmd tmpDir
+      "test_self_field_dispatch_precondition.py" (useRoots := true)
+    match result with
+    | .error msg => throw <| IO.userError s!"Pipeline failed: {msg}"
+    | .ok vcResults =>
+      let mut foundAlwaysFalse := false
+      for r in vcResults do
+        if r.obligation.label.startsWith "servicelib_Storage_" then
+          let line := r.formatOutcome
+          if (line.splitOn "✖️").length != 1 then
+            foundAlwaysFalse := true
+      if !foundAlwaysFalse then
+        throw <| IO.userError
+          "Expected ✖️ always false for empty bucket violation via self.field dispatch"
+
 end Strata.Python.AnalyzeLaurelTest

StrataTestExtra/Languages/Python/Specs/dispatch_test/test_self_field_dispatch_precondition.py

@@ -0,0 +1,13 @@
+import servicelib
+
+class MyService:
+    def __init__(self):
+        self.store: Storage = servicelib.connect("storage")
+
+    def save_empty_bucket(self) -> bool:
+        self.store.put_item(Bucket="", Key="k", Data="v")
+        return True
+
+def trigger() -> bool:
+    svc: MyService = MyService()
+    return svc.save_empty_bucket()