Laurel: field access on Any-typed values

Strata/Languages/Laurel/HeapParameterization.lean

@@ -291,7 +291,18 @@ where
 
         let valTy := (model.get fieldName).getType
         let selectTarget' ← recurseOne selectTarget
-        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectTarget', mkMd (.StaticCall qualifiedName [])], source ⟩
+        -- Unbox an `Any`-typed target to a `Composite` using the field's
+        -- owning-class tag; other targets pass through unchanged.
+        let targetTy := (computeExprType model selectTarget).val
+        let selectComposite : StmtExprMd :=
+          match targetTy with
+          | .UserDefined n =>
+            if n.text == "Any" then
+              let owner := (qualifiedName.splitOn ".").head!
+              mkMd (.StaticCall "anyToComposite" [selectTarget', mkMd (.StaticCall (owner ++ "_TypeTag") [])])
+            else selectTarget'
+          | _ => selectTarget'
+        let readExpr := ⟨ .StaticCall "readField" [mkMd (.Var (.Local heapVar)), selectComposite, mkMd (.StaticCall qualifiedName [])], source ⟩
         -- Unwrap Box: apply the appropriate destructor
         recordBoxConstructor model valTy.val
         return [mkMd <| .StaticCall (boxDestructorName model valTy.val) [readExpr]]

Strata/Languages/Laurel/HeapParameterizationConstants.lean

@@ -75,6 +75,28 @@ def heapConstants : Program :=
   | .ok program => program
   | .error e => dbg_trace s!"BUG: Laurel heap prelude parse error: {e}"; default
 
+/- Convert between an `Any` holding a heap reference and a `Composite`.
+   Injected by `typeHierarchyTransform` only when the program defines `Any`. -/
+private def pyspecHeapBridgeDDM :=
+#strata
+program Laurel;
+
+function anyToComposite(a: Any, tag: TypeTag): Composite {
+  MkComposite(Any..as_ref!(a), tag)
+};
+
+function compositeToAny(c: Composite): Any {
+  from_Reference(Composite..ref!(c))
+};
+
+#end
+
+/-- Parsed Any<->Composite bridge program (see `pyspecHeapBridgeDDM`). -/
+def pyspecHeapBridge : Program :=
+  match Laurel.TransM.run none (Laurel.parseProgram pyspecHeapBridgeDDM) with
+  | .ok program => program
+  | .error e => dbg_trace s!"BUG: Laurel pyspec heap bridge parse error: {e}"; default
+
 end -- public section
 
 end Strata.Laurel

Strata/Languages/Laurel/Resolution.lean

@@ -301,6 +301,12 @@ def resolveFieldRef (target : StmtExprMd) (fieldName : Identifier)
   if let some instTypeName := (← get).instanceTypeName then
     if let some resolved ← resolveFieldInTypeScope instTypeName fieldName then
       return resolved
+  -- For `Any`-typed targets only, resolve the field by name across all type
+  -- scopes. Gating on `Any` keeps a concrete target from binding a foreign field.
+  if typeName? == some "Any" then
+    for (_, fieldScope) in (← get).typeScopes.toList do
+      if let some (defId, _) := fieldScope.get? fieldName.text then
+        return { fieldName with uniqueId := some defId }
   resolveRef fieldName source
 
 /-- Save and restore scope around a block (for lexical scoping). -/

Strata/Languages/Laurel/TypeHierarchy.lean

@@ -173,9 +173,24 @@ def typeHierarchyTransform (model: SemanticModel) (program : Program) : Program
           else c }
       else td
     | _ => td
+  -- Inject the bridge only when the program defines `Any`; it needs the 2-arg
+  -- `MkComposite` and `TypeTag` produced by this pass.
+  let definesAny : Bool := program.types.any fun td =>
+    match td with
+    | .Datatype d => d.name.text == "Any"
+    | _ => false
+  let bridgeProcs : List Procedure :=
+    if definesAny then pyspecHeapBridge.staticProcedures else []
+  -- Fill each `__box_<C>` marker with a `compositeToAny(c)` body.
+  let procsBodied := procs'.map fun p =>
+    if p.name.text.startsWith "__box_" then
+      match p.inputs with
+      | [inp] => { p with body := .Transparent (mkMd (.StaticCall "compositeToAny" [mkMd (.Var (.Local inp.name))])) }
+      | _ => p
+    else p
   let transformed : Program :=
     { program with
-      staticProcedures := procs',
+      staticProcedures := procsBodied ++ bridgeProcs,
       types := [typeTagDatatype] ++ remainingTypes,
       constants := program.constants ++ typeHierarchyConstants }
   -- Now that `New`/`IsType` have been lowered (they needed the original

StrataPython/StrataPython/PythonLaurelCorePrelude.lean

@@ -82,6 +82,7 @@ datatype Any () {
   from_DictStrAny (as_Dict: DictStrAny),
   from_ListAny (as_ListAny : ListAny),
   from_ClassInstance (classname : string, instance_attributes: DictStrAny),
+  from_Reference (as_ref : int),
   from_Slice(start: int, stop: OptionInt),
   exception (get_error: Error)
 }

StrataPython/StrataPython/PythonRuntimeLaurelPart.lean

@@ -81,6 +81,7 @@ datatype Any {
   from_DictStrAny (as_Dict: DictStrAny),
   from_ListAny (as_ListAny : ListAny),
   from_ClassInstance (classname : string, instance_attributes: DictStrAny),
+  from_Reference (as_ref : int),
   from_Slice(start: int, stop: OptionInt),
   exception (get_error: Error)
 }

StrataTest/Languages/Laurel/AnyBridgeFieldResolutionTest.lean

@@ -0,0 +1,115 @@
+/-
+  Copyright Strata Contributors
+
+  SPDX-License-Identifier: Apache-2.0 OR MIT
+-/
+
+/-
+Regression tests for `Any`-typed field resolution: the cross-scope fallback in
+`resolveFieldRef` fires only for `Any` targets, so a concrete target can't bind
+an unrelated composite's field.
+-/
+
+import StrataTest.Util.TestLaurel
+
+open StrataTest.Util
+open Strata
+
+/-! ## `meow` (on `Cat`) is not a field of `Dog`, so `d#meow` is rejected -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+composite Dog { var bark: int }
+composite Cat { var meow: int }
+procedure test() opaque {
+  var d: Dog := new Dog;
+  var x: int := d#meow
+//                ^^^^ error: Resolution failed: 'meow' is not defined
+};
+#end
+
+/-! ## Correct field access on the same composites still resolves -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+composite Dog { var bark: int }
+composite Cat { var meow: int }
+procedure test() opaque {
+  var d: Dog := new Dog;
+  var x: int := d#bark
+};
+#end
+
+/-! ## An `Any`-typed target resolves a field cross-scope (gate TRUE branch) -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+datatype Any { from_Reference(as_ref: int) }
+composite Dog { var bark: int }
+procedure test() opaque {
+  var a: Any := from_Reference(0);
+  var x: int := a#bark
+};
+#end
+
+/-! ## An `Any`-typed target accessing a field defined on no composite still errors -/
+
+#eval testLaurelResolution <|
+#strata
+program Laurel;
+datatype Any { from_Reference(as_ref: int) }
+composite Dog { var bark: int }
+procedure test() opaque {
+  var a: Any := from_Reference(0);
+  var x: int := a#nope
+//                ^^^^ error: Resolution failed: 'nope' is not defined
+};
+#end
+
+/-! ## A field write/read round-trip verifies -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Dog { var bark: int }
+procedure test() opaque {
+  var d: Dog := new Dog;
+  d#bark := 7;
+  assert d#bark == 7;
+  d#bark := d#bark + 1;
+  assert d#bark == 8
+};
+#end
+
+/-! ## Two instances have independent fields (no aliasing collapse) -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Dog { var bark: int }
+procedure test() opaque {
+  var d1: Dog := new Dog;
+  var d2: Dog := new Dog;
+  d1#bark := 1;
+  d2#bark := 2;
+  assert d1#bark == 1;
+  assert d2#bark == 2
+};
+#end
+
+/-! ## A false field assertion is caught by the verifier -/
+
+#eval testLaurel <|
+#strata
+program Laurel;
+composite Dog { var bark: int }
+procedure test() opaque {
+  var d: Dog := new Dog;
+  d#bark := 1;
+  assert d#bark == 2
+//^^^^^^^^^^^^^^^^^^ error: assertion could not be proved
+};
+#end