feat: Translate PySpec preconditions to Laurel assertions for bug finding

Strata/Languages/Python/PySpecPipeline.lean

@@ -31,6 +31,8 @@ public structure PySpecLaurelResult where
   laurelProgram : Laurel.Program
   overloads : OverloadTable
   functionSignatures : List Python.PythonFunctionDecl := []
+  /-- Maps unprefixed class names to prefixed names for type resolution. -/
+  typeAliases : Std.HashMap String String := {}
 
 /-! ### Private Helpers -/
 
@@ -110,6 +112,7 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
   let mut combinedTypes : Array (Laurel.TypeDefinition × String) := #[]
   let mut allOverloads := overloads
   let mut funcSigs : List Python.PythonFunctionDecl := []
+  let mut allTypeAliases : Std.HashMap String String := {}
   for ionPath in pyspecPaths do
     let ionFile : System.FilePath := ionPath
     let some mod := ionFile.fileStem
@@ -121,14 +124,15 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
       match ← Python.Specs.readDDM ionFile |>.toBaseIO with
       | .ok t => pure t
       | .error msg => throw s!"Could not read {ionFile}: {msg}"
-    let { program, errors, overloads } :=
+    let { program, errors, overloads, typeAliases } :=
       Python.Specs.ToLaurel.signaturesToLaurel ionPath sigs modulePrefix
     if errors.size > 0 then
       let _ ← IO.eprintln
         s!"{errors.size} PySpec translation warning(s) for {ionPath}:" |>.toBaseIO
       for err in errors do
         let _ ← IO.eprintln s!"  {err.file}: {err.message}" |>.toBaseIO
     allOverloads := mergeOverloads allOverloads overloads
+    allTypeAliases := typeAliases.fold (init := allTypeAliases) fun m k v => m.insert k v
     match extractFunctionSignatures sigs modulePrefix with
     | .ok fs => funcSigs := funcSigs ++ fs
     | .error msg => throw msg
@@ -163,7 +167,7 @@ public def buildPySpecLaurel (pyspecPaths : Array String)
     constants := []
   }
   return { laurelProgram := combinedLaurel, overloads := allOverloads
-           functionSignatures := funcSigs }
+           functionSignatures := funcSigs, typeAliases := allTypeAliases }
 
 /-- Read dispatch Ion files and merge their overload tables. -/
 public def readDispatchOverloads
@@ -237,7 +241,8 @@ public def buildPreludeInfo (result : PySpecLaurelResult) : Python.PreludeInfo :
     (Python.PreludeInfo.ofLaurelProgram result.laurelProgram)
   { merged with
     functionSignatures :=
-      result.functionSignatures ++ merged.functionSignatures }
+      result.functionSignatures ++ merged.functionSignatures
+    typeAliases := result.typeAliases }
 
 /-- Combine PySpec and user Laurel programs into a single program,
     prepending External stubs so the Laurel `resolve` pass can see

Strata/Languages/Python/PythonToLaurel.lean

@@ -91,6 +91,8 @@ structure TranslationContext where
   filePath : String := ""
   /-- Known composite type names (user-defined classes + PySpec types) -/
   compositeTypeNames : Std.HashSet String := {}
+  /-- Maps unprefixed class names to prefixed names (from pyspec). -/
+  typeAliases : Std.HashMap String String := {}
   /-- Track current class during method translation -/
   currentClassName : Option String := none
   loopBreakLabel : Option String := none
@@ -99,6 +101,11 @@ deriving Inhabited
 
 /-! ## Error Handling -/
 
+/-- Resolve a type name through aliases. Returns the prefixed name if an alias
+    exists, otherwise the original name. -/
+def resolveTypeName (ctx : TranslationContext) (name : String) : String :=
+  ctx.typeAliases.getD name name
+
 /-- Translation errors with context -/
 inductive TranslationError where
   | unsupportedConstruct (msg : String) (pyAst : String)
@@ -658,7 +665,8 @@ partial def refineFunctionCallExpr (ctx : TranslationContext) (func: Python.expr
         if callerTy == PyLauType.Any then
           return ("AnyTyInstance" ++ "@" ++ callname, some v, true)
         else
-          return (callerTy ++ "_" ++ callname, some v, false)
+          let resolvedTy := resolveTypeName ctx callerTy
+          return (resolvedTy ++ "_" ++ callname, some v, false)
     | _ => throw (.internalError s!"{repr func} is not a function")
 
 --Kwargs can be a single Dict variable: func_call (**var) or a normal Kwargs (key1 = val1, key2 =val2 ...)
@@ -792,8 +800,15 @@ partial def translateCall (ctx : TranslationContext)
   | .Attribute _ val _attr _ =>
       let _target_trans ← translateExpr ctx val
       if opt_firstarg.isSome then
-        return mkStmtExprMd (.Hole)
-        --return mkStmtExprMd (StmtExpr.InstanceCall target_trans attr.val (trans_args ++ trans_kwords_exprs))
+        -- Only emit StaticCall when the caller type was resolved through a
+        -- pyspec type alias, indicating the procedure has precondition assertions.
+        let callerTy := match f with
+          | .Attribute _ v _ _ => (inferExprType ctx v).toOption.getD ""
+          | _ => ""
+        if ctx.typeAliases.contains callerTy && funcName ∈ ctx.preludeProcedures then
+          return mkStmtExprMd (StmtExpr.StaticCall funcName (trans_args ++ trans_kwords_exprs))
+        else
+          return mkStmtExprMd (.Hole)
       else
         return mkStmtExprMd (StmtExpr.StaticCall funcName (trans_args ++ trans_kwords_exprs))
   | _ =>  throw (.unsupportedConstruct "Invalid call construct" (toString (repr f)))
@@ -884,7 +899,8 @@ partial def translateAssign  (ctx : TranslationContext)
         newctx := match rhs_trans.val with
         | .StaticCall fnname _ =>
             if fnname.text ∈ ctx.compositeTypeNames then
-              {newctx with variableTypes:= newctx.variableTypes ++ [(n.val, fnname.text)]}
+              let resolved := resolveTypeName ctx fnname.text
+              {newctx with variableTypes:= newctx.variableTypes ++ [(n.val, resolved)]}
             else newctx
         | .New className =>
             {newctx with variableTypes:= newctx.variableTypes ++ [(n.val, className.text)]}
@@ -1546,6 +1562,8 @@ structure PreludeInfo where
   functions : List String := []
   /-- Procedure names (non-function callables) -/
   procedureNames : List String := []
+  /-- Maps unprefixed class names to prefixed names (from pyspec). -/
+  typeAliases : Std.HashMap String String := {}
 
 /-- Extract `PreludeInfo` from a `Core.Program`. -/
 def PreludeInfo.ofCoreProgram (prelude : Core.Program) : PreludeInfo where
@@ -1627,6 +1645,7 @@ def PreludeInfo.merge (a b : PreludeInfo) : PreludeInfo where
   functionSignatures := a.functionSignatures ++ b.functionSignatures
   functions := a.functions ++ b.functions
   procedureNames := a.procedureNames ++ b.procedureNames
+  typeAliases := b.typeAliases.fold (init := a.typeAliases) fun m k v => m.insert k v
 
 /-- Translate Python module to Laurel Program using pre-extracted prelude info. -/
 def pythonToLaurel' (info : PreludeInfo)
@@ -1681,16 +1700,26 @@ def pythonToLaurel' (info : PreludeInfo)
     let mut ctx : TranslationContext := match prev_ctx with
     | some prev_ctx => prev_ctx
     | _ =>
+    -- Add unprefixed method names as procedure aliases
+    -- e.g. MessageService_send → same signature as prefix_MessageService_send
+    let preludeProcedures := info.typeAliases.fold (init := info.procedures)
+      fun procs unprefixed prefixed =>
+        procs.fold (init := procs) fun procs' name sig =>
+          if name.startsWith (prefixed ++ "_") then
+            let unprefixedName := unprefixed ++ name.drop prefixed.length
+            procs'.insert unprefixedName sig
+          else procs'
     {
       currentClassName := none,
-      preludeProcedures := info.procedures,
+      preludeProcedures := preludeProcedures,
       functionSignatures := info.functionSignatures
       preludeFunctions := info.functions
       preludeTypes := info.types,
       userFunctions := userFunctions,
       compositeTypeNames := compositeTypeNames,
       classFieldHighType := classFieldHighType,
       overloadTable := overloadTable,
+      typeAliases := info.typeAliases,
       filePath := filePath
     }
 

Strata/Languages/Python/Specs/ToLaurel.lean

@@ -61,6 +61,8 @@ structure ToLaurelState where
   procedures : Array Procedure := #[]
   types : Array TypeDefinition := #[]
   overloads : OverloadTable := {}
+  /-- Maps unprefixed class names to prefixed names for type resolution. -/
+  typeAliases : Std.HashMap String String := {}
 
 /-- Monad for PySpec to Laurel translation. -/
 @[expose] abbrev ToLaurelM := ReaderT ToLaurelContext (StateM ToLaurelState)
@@ -259,6 +261,114 @@ def specTypeToLaurelType (ty : SpecType) : ToLaurelM HighTypeMd := do
     | .stringLiteral _ => return mkTy .TString
     | .typedDict _ _ _ => return mkCore "DictStrAny"
 
+/-! ## SpecExpr to Laurel Translation -/
+
+/-- Wrap a StmtExpr with default metadata. -/
+private def mkStmt (e : StmtExpr) : StmtExprMd :=
+  { val := e, md := .empty }
+
+/-- Translate a SpecExpr to a Laurel StmtExpr.
+    All values are assumed to be Core(Any)-typed, matching the Python pipeline.
+    Returns `none` for unsupported expressions (placeholders).
+    Uses Core prelude function names (Str.Length, DictStrAny_contains, etc.)
+    which are resolved after the Core prelude is prepended. -/
+partial def specExprToLaurel (e : SpecExpr) : Option StmtExprMd :=
+  match e with
+  | .placeholder => none
+  | .var name => some (mkStmt (.Identifier (mkId name)))
+  | .intLit v => some (mkStmt (.StaticCall (mkId "from_int") [mkStmt (.LiteralInt v)]))
+  | .floatLit _ => none -- TODO: decimal literals
+  | .getIndex subject field =>
+    match subject with
+    -- kwargs["fieldName"] → direct reference to the expanded parameter
+    | .var "kwargs" => some (mkStmt (.Identifier (mkId field)))
+    | _ => subject |> specExprToLaurel |>.map fun s =>
+             mkStmt (.FieldSelect s (mkId field))
+  | .isInstanceOf _ _ => none -- TODO: isinstance checks
+  | .len subject =>
+    -- len(x) where x is Any: Str.Length(Any..as_string!(x)) wrapped back as from_int
+    subject |> specExprToLaurel |>.map fun s =>
+      let unwrapped := mkStmt (.StaticCall (mkId "Any..as_string!") [s])
+      mkStmt (.StaticCall (mkId "from_int") [mkStmt (.StaticCall (mkId "Str.Length") [unwrapped])])
+  | .intGe subject bound => do
+    -- Compare as ints: Any..as_int!(subject) >= Any..as_int!(bound)
+    let s ← specExprToLaurel subject
+    let b ← specExprToLaurel bound
+    let sInt := mkStmt (.StaticCall (mkId "Any..as_int!") [s])
+    let bInt := mkStmt (.StaticCall (mkId "Any..as_int!") [b])
+    some (mkStmt (.PrimitiveOp .Geq [sInt, bInt]))
+  | .intLe subject bound => do
+    let s ← specExprToLaurel subject
+    let b ← specExprToLaurel bound
+    let sInt := mkStmt (.StaticCall (mkId "Any..as_int!") [s])
+    let bInt := mkStmt (.StaticCall (mkId "Any..as_int!") [b])
+    some (mkStmt (.PrimitiveOp .Leq [sInt, bInt]))
+  | .floatGe subject bound => do
+    let s ← specExprToLaurel subject
+    let b ← specExprToLaurel bound
+    some (mkStmt (.PrimitiveOp .Geq [s, b]))
+  | .floatLe subject bound => do
+    let s ← specExprToLaurel subject
+    let b ← specExprToLaurel bound
+    some (mkStmt (.PrimitiveOp .Leq [s, b]))
+  | .not inner =>
+    inner |> specExprToLaurel |>.map fun i =>
+      mkStmt (.PrimitiveOp .Not [i])
+  | .implies cond body => do
+    let c ← specExprToLaurel cond
+    let b ← specExprToLaurel body
+    some (mkStmt (.PrimitiveOp .Implies [c, b]))
+  | .enumMember subject values =>
+    -- Check if Any..as_string!(subject) is one of the string values
+    subject |> specExprToLaurel |>.map fun s =>
+      let sStr := mkStmt (.StaticCall (mkId "Any..as_string!") [s])
+      let eqs := values.toList.map fun v =>
+        mkStmt (.PrimitiveOp .Eq [sStr, mkStmt (.LiteralString v)])
+      eqs.foldl (init := mkStmt (.LiteralBool false)) fun acc eq =>
+        mkStmt (.PrimitiveOp .Or [acc, eq])
+  | .containsKey container key =>
+    -- DictStrAny_contains(Any..as_Dict!(container), key)
+    container |> specExprToLaurel |>.map fun c =>
+      let unwrapped := mkStmt (.StaticCall (mkId "Any..as_Dict!") [c])
+      mkStmt (.StaticCall (mkId "DictStrAny_contains") [unwrapped, mkStmt (.LiteralString key)])
+  | .regexMatch subject pattern =>
+    -- Assumes future Laurel functions:
+    --   string_to_regex(pattern: string) -> Regex
+    --   regex_matches(regex: Regex, subject: string) -> bool
+    subject |> specExprToLaurel |>.map fun s =>
+      let sStr := mkStmt (.StaticCall (mkId "Any..as_string!") [s])
+      let regex := mkStmt (.StaticCall (mkId "string_to_regex") [mkStmt (.LiteralString pattern)])
+      mkStmt (.StaticCall (mkId "regex_matches") [regex, sStr])
+  | .forallList _ _ _ => none -- TODO: quantifiers
+  | .forallDict _ _ _ _ => none -- TODO: quantifiers
+
+/-- Format an Assertion's message parts into a string for diagnostics. -/
+private def formatAssertionMessage (msg : Array MessagePart) : String :=
+  let parts := msg.map fun
+    | .str s => s
+    | .expr _ => "<expr>"
+  String.join parts.toList
+
+/-- Build a procedure body that asserts preconditions and havocs outputs. -/
+def buildSpecBody (preconditions : Array Assertion) (outputs : List Parameter)
+    : ToLaurelM Body := do
+  let mut stmts : List StmtExprMd := []
+  for assertion in preconditions do
+    match specExprToLaurel assertion.formula with
+    | some condExpr =>
+      stmts := stmts ++ [mkStmt (.Assert condExpr)]
+    | none =>
+      -- Emit assert true for untranslatable preconditions so they're visible but don't block
+      let msg := formatAssertionMessage assertion.message
+      reportError default s!"Untranslatable precondition (emitting assert true): {msg}"
+      stmts := stmts ++ [mkStmt (.Assert (mkStmt (.LiteralBool true)))]
+  -- Havoc each output by assigning a nondeterministic hole
+  for output in outputs do
+    let hole := mkStmt (.Hole (deterministic := false) (type := some output.type))
+    stmts := stmts ++ [mkStmt (.Assign [mkStmt (.Identifier output.name)] hole)]
+  let body := mkStmt (.Block stmts none)
+  return .Transparent body
+
 /-! ## Declaration Translation -/
 
 /-- Convert an Arg to a Laurel Parameter. -/
@@ -300,8 +410,19 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
     match retType.val with
     | .TVoid => []
     | _ => [{ name := "result", type := retType }]
-  if func.preconditions.size > 0 || func.postconditions.size > 0 then
-    reportError func.loc "Preconditions/postconditions not yet supported"
+  if func.postconditions.size > 0 then
+    reportError func.loc "Postconditions not yet supported"
+  -- When preconditions exist, use TCore "Any" for all parameters and outputs
+  -- to match the Python→Laurel pipeline's Any-wrapping convention.
+  let (inputs, outputs, body) ←
+    if func.preconditions.size > 0 then do
+      let anyTy : HighTypeMd := mkCore "Any"
+      let anyInputs := inputs.map fun p => { p with type := anyTy }
+      let anyOutputs := outputs.map fun p => { p with type := anyTy }
+      let body ← buildSpecBody func.preconditions anyOutputs
+      pure (anyInputs, anyOutputs, body)
+    else
+      pure (inputs, outputs, Body.Opaque [] none [])
   return {
     name := procName
     inputs := inputs.toList
@@ -310,13 +431,16 @@ def funcDeclToLaurel (procName : String) (func : FunctionDecl)
     determinism := .nondeterministic
     decreases := none
     isFunctional := false
-    body := .Opaque [] none []
+    body := body
     md := .empty
   }
 
 /-- Convert a class definition to Laurel types and procedures. -/
 def classDefToLaurel (cls : ClassDef) : ToLaurelM Unit := do
   let prefixedName ← prefixName cls.name
+  -- Register alias from unprefixed to prefixed name for type resolution
+  if prefixedName != cls.name then
+    modify fun s => { s with typeAliases := s.typeAliases.insert cls.name prefixedName }
   let laurelFields ← cls.fields.toList.mapM fun f => do
     let ty ← specTypeToLaurelType f.type
     pure { name := f.name, isMutable := true, type := ty : Laurel.Field }
@@ -414,6 +538,8 @@ structure TranslationResult where
   program : Laurel.Program
   errors : Array SpecError
   overloads : OverloadTable
+  /-- Maps unprefixed class names to prefixed names for type resolution. -/
+  typeAliases : Std.HashMap String String := {}
 
 /-- Run the translation and return a Laurel Program, dispatch table,
     and any errors. -/
@@ -430,7 +556,8 @@ def signaturesToLaurel (filepath : System.FilePath) (sigs : Array Signature)
   }
   { program := pgm
     errors := state.errors
-    overloads := state.overloads }
+    overloads := state.overloads
+    typeAliases := state.typeAliases }
 
 /-- Extract only the overload dispatch table from PySpec signatures.
     Processes `@overload` function declarations, ignoring classDef,