Disallow transparent statement bodies

Strata/Languages/Laurel/Grammar/AbstractToConcreteTreeTranslator.lean

@@ -190,8 +190,11 @@ private def ensuresClauseToArg (c : Condition) : Arg :=
   laurelOp "ensuresClause" #[stmtExprToArg c.condition, errOpt]
 
 private def modifiesClauseToArg (modifies : List StmtExprMd) : Arg :=
-  let refs := modifies.map stmtExprToArg |>.toArray
-  laurelOp "modifiesClause" #[commaSep refs]
+  if modifies.any (fun e => match e.val with | .All => true | _ => false) then
+    laurelOp "modifiesWildcard" #[]
+  else
+    let refs := modifies.map stmtExprToArg |>.toArray
+    laurelOp "modifiesClause" #[commaSep refs]
 
 private def procedureToOp (proc : Procedure) : Strata.Operation :=
   let opName := if proc.isFunctional then "function" else "procedure"
@@ -215,19 +218,19 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
   let requiresArgs := proc.preconditions.map requiresClauseToArg |>.toArray
   let invokeOnArg := optionArg (proc.invokeOn.map fun e =>
     laurelOp "invokeOnClause" #[stmtExprToArg e])
-  let (ensuresArgs, modifiesArgs, bodyArg) := match proc.body with
+  let (opaqueSpecArg, bodyArg) := match proc.body with
     | .Transparent body =>
-      (#[], #[], optionArg (some (laurelOp "body" #[stmtExprToArg body])))
+      (optionArg none, optionArg (some (laurelOp "body" #[stmtExprToArg body])))
     | .Opaque postconds impl modifies =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
       let mods := if modifies.isEmpty then #[] else #[modifiesClauseToArg modifies]
       let body := optionArg (impl.map fun e => laurelOp "body" #[stmtExprToArg e])
-      (ens, mods, body)
+      (optionArg (some (laurelOp "opaqueSpec" #[seqArg ens, seqArg mods])), body)
     | .Abstract postconds =>
       let ens := postconds.map ensuresClauseToArg |>.toArray
-      (ens, #[], optionArg none)
+      (optionArg (some (laurelOp "opaqueSpec" #[seqArg ens, seqArg #[]])), optionArg none)
     | .External =>
-      (#[], #[], optionArg (some (laurelOp "externalBody")))
+      (optionArg none, optionArg (some (laurelOp "externalBody")))
   { ann := sr
     name := { dialect := "Laurel", name := opName }
     args := #[
@@ -237,8 +240,7 @@ private def procedureToOp (proc : Procedure) : Strata.Operation :=
       returnParamsArg,
       seqArg requiresArgs,
       invokeOnArg,
-      seqArg ensuresArgs,
-      seqArg modifiesArgs,
+      opaqueSpecArg,
       bodyArg
     ] }
 

Strata/Languages/Laurel/Grammar/ConcreteToAbstractTreeTranslator.lean

@@ -378,6 +378,8 @@ def translateModifiesClauses (arg : Arg) : TransM (List StmtExprMd) := do
         | q`Laurel.modifiesClause, #[refsArg] =>
           let refs ← translateModifiesExprs refsArg
           allModifies := allModifies ++ refs
+        | q`Laurel.modifiesWildcard, #[] =>
+          allModifies := allModifies ++ [{ val := .All, source := none }]
         | _, _ => TransM.error s!"Expected modifiesClause operation, got {repr clauseOp.name}"
       | _ => TransM.error s!"Expected modifiesClause operation in modifies sequence"
     pure allModifies
@@ -433,9 +435,9 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
 
   match op.name, op.args with
   | q`Laurel.procedure, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg]
+      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg]
   | q`Laurel.function, #[nameArg, paramArg, returnTypeArg, returnParamsArg,
-      requiresArg, invokeOnArg, ensuresArg, modifiesArg, bodyArg] =>
+      requiresArg, invokeOnArg, opaqueSpecArg, bodyArg] =>
     let name ← translateIdent nameArg
     let parameters ← translateParameters paramArg
     -- Either returnTypeArg or returnParamsArg may have a value, not both
@@ -465,10 +467,16 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
         | _, _ => TransM.error s!"Expected invokeOnClause operation, got {repr invokeOnOp.name}"
       | .option _ none => pure none
       | _ => pure none
-    -- Parse postconditions (ensures clauses - zero or more)
-    let postconditions ← translateEnsuresClauses ensuresArg
-    -- Parse modifies clauses (zero or more)
-    let modifies ← translateModifiesClauses modifiesArg
+    -- Parse optional opaqueSpec (contains ensures and modifies)
+    let (isOpaque, postconditions, modifies) ← match opaqueSpecArg with
+      | .option _ (some (.op opaqueSpecOp)) => match opaqueSpecOp.name, opaqueSpecOp.args with
+        | q`Laurel.opaqueSpec, #[ensuresArg, modifiesArg] =>
+          let postconditions ← translateEnsuresClauses ensuresArg
+          let modifies ← translateModifiesClauses modifiesArg
+          pure (true, postconditions, modifies)
+        | _, _ => TransM.error s!"Expected opaqueSpec operation, got {repr opaqueSpecOp.name}"
+      | .option _ none => pure (false, [], [])
+      | _ => pure (false, [], [])
     -- Parse optional body
     let isExternal ← match bodyArg with
       | .option _ (some (.op bodyOp)) => match bodyOp.name, bodyOp.args with
@@ -485,10 +493,10 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     -- Determine procedure body kind
     let procBody :=
       if isExternal then Body.External
-      else match postconditions, body with
-      | _ :: _, bodyOpt => Body.Opaque postconditions bodyOpt modifies
-      | [], some b => Body.Transparent b
-      | [], none => Body.Opaque [] none modifies
+      else if isOpaque then Body.Opaque postconditions body modifies
+      else match body with
+      | some b => Body.Transparent b
+      | none => Body.Opaque [] none modifies
     return {
       name := name
       inputs := parameters
@@ -501,7 +509,7 @@ def parseProcedure (arg : Arg) : TransM Procedure := do
     }
   | q`Laurel.procedure, args
   | q`Laurel.function, args =>
-    TransM.error s!"parseProcedure expects 9 arguments, got {args.size}"
+    TransM.error s!"parseProcedure expects 8 arguments, got {args.size}"
   | _, _ =>
     TransM.error s!"parseProcedure expects procedure or function, got {repr op.name}"
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.lean

@@ -9,7 +9,7 @@ module
 -- Laurel dialect definition, loaded from LaurelGrammar.st
 -- NOTE: Changes to LaurelGrammar.st are not automatically tracked by the build system.
 -- Update this file (e.g. this comment) to trigger a recompile after modifying LaurelGrammar.st.
--- Last grammar change: parameterized bvType with arbitrary width
+-- Last grammar change: added modifiesWildcard op for wildcard modifies clauses.
 public import Strata.DDM.Integration.Lean
 public meta import Strata.DDM.Integration.Lean
 

Strata/Languages/Laurel/Grammar/LaurelGrammar.st

@@ -157,10 +157,15 @@ op ensuresClause(cond: StmtExpr, errorMessage: Option ErrorSummary): EnsuresClau
 
 category ModifiesClause;
 op modifiesClause(refs: CommaSepBy StmtExpr): ModifiesClause => "\n  modifies " refs;
+op modifiesWildcard: ModifiesClause => "\n  modifies *";
 
 category ReturnParameters;
 op returnParameters(parameters: CommaSepBy Parameter): ReturnParameters => "\n  returns " "(" parameters ")";
 
+category OpaqueSpec;
+op opaqueSpec(ensures: Seq EnsuresClause, modifies: Seq ModifiesClause): OpaqueSpec =>
+  "\n  opaque" ensures modifies;
+
 category Body;
 op body(body: StmtExpr): Body => "\n" body:0;
 op externalBody: Body => "external";
@@ -171,20 +176,18 @@ op procedure (name : Ident, parameters: CommaSepBy Parameter,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
   invokeOn: Option InvokeOnClause,
-  ensures: Seq EnsuresClause,
-  modifies: Seq ModifiesClause,
+  opaqueSpec: Option OpaqueSpec,
   body : Option Body) : Procedure =>
-  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
+  "procedure " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
 
 op function (name : Ident, parameters: CommaSepBy Parameter,
   returnType: Option ReturnType,
   returnParameters: Option ReturnParameters,
   requires: Seq RequiresClause,
   invokeOn: Option InvokeOnClause,
-  ensures: Seq EnsuresClause,
-  modifies: Seq ModifiesClause,
+  opaqueSpec: Option OpaqueSpec,
   body : Option Body) : Procedure =>
-  "function " name "(" parameters ")" returnType returnParameters requires invokeOn ensures modifies body ";";
+  "function " name "(" parameters ")" returnType returnParameters requires invokeOn opaqueSpec body ";";
 
 op composite (name: Ident, extending: Option Extends, fields: Seq Field, procedures: Seq Procedure): Composite => "composite " name extending " {" fields procedures " }";
 

Strata/Languages/Laurel/HeapParameterization.lean

@@ -99,9 +99,12 @@ def analyzeProc (proc : Procedure) : AnalysisResult :=
   let bodyResult := match proc.body with
     | .Transparent b => (collectExprMd b).run {} |>.2
     | .Opaque postconds impl modif =>
-        -- A non-empty modifies clause implies the procedure reads and writes the heap;
-        -- no need to inspect the body further in that case.
-        if !modif.isEmpty then
+        -- A non-empty modifies clause (excluding wildcard `*`) implies the procedure
+        -- reads and writes the heap; no need to inspect the body further in that case.
+        -- Wildcard modifies does not imply heap access — it only suppresses the frame condition.
+        let isWildcard (e : StmtExprMd) : Bool := match e.1 with | .All => true | _ => false
+        let concreteModifies := modif.filter (fun e => !isWildcard e)
+        if !concreteModifies.isEmpty then
           { readsHeapDirectly := true, writesHeapDirectly := true, callees := [] }
         else
           let r1 := postconds.foldl (fun (acc : AnalysisResult) (pc : Condition) =>

Strata/Languages/Laurel/ModifiesClauses.lean

@@ -136,20 +136,31 @@ indicating it mutates the heap.
 def hasHeapOut (proc : Procedure) : Bool :=
   proc.outputs.any (fun p => p.name.text == "$heap")
 
+/--
+Check whether a modifies list contains a wildcard (`All`), meaning anything can be modified.
+-/
+def hasWildcardModifies (modifiesExprs : List StmtExprMd) : Bool :=
+  modifiesExprs.any (fun e => match e.val with | .All => true | _ => false)
+
 /--
 Transform a single procedure: if it has modifies clauses, generate the frame
 condition and conjoin it with the postcondition, then clear the modifies list.
 
 If the procedure has a `$heap` but no modifies clause, adds a postcondition
 that all allocated objects are preserved between heaps:
   `forall $obj: Composite, $fld: Field => $obj < $heap_in.nextReference ==> readField($heap_in, $obj, $fld) == readField($heap, $obj, $fld)`
+
+If the modifies clause uses a wildcard (`*`), the frame condition is skipped
+entirely — the procedure may modify anything.
 -/
 def transformModifiesClauses (model: SemanticModel)
     (proc : Procedure) : Except (Array DiagnosticModel) Procedure :=
   match proc.body with
   | .External => .ok proc
   | .Opaque postconds impl modifiesExprs =>
-      if hasHeapOut proc then
+      if hasWildcardModifies modifiesExprs then
+        .ok { proc with body := .Opaque postconds impl [] }
+      else if hasHeapOut proc then
         let heapInName : Identifier := "$heap_in"
         let heapName : Identifier := "$heap"
         let frameCondition := buildModifiesEnsures proc model modifiesExprs heapInName heapName
@@ -172,10 +183,13 @@ def filterBodyNonCompositeModifies (model : SemanticModel) (body : Body)
   match body with
   | .Opaque posts impl mods =>
     let (kept, diags) := mods.foldl (fun (acc, ds) e =>
-      let ty := (computeExprType model e).val
-      if isHeapRelevantType ty then (acc ++ [e], ds)
-      else
-        (acc, ds ++ [(fileRangeToCoreMd e.source e.md).toDiagnostic s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
+      match e.val with
+      | .All => (acc ++ [e], ds)
+      | _ =>
+        let ty := (computeExprType model e).val
+        if isHeapRelevantType ty then (acc ++ [e], ds)
+        else
+          (acc, ds ++ [(fileRangeToCoreMd e.source e.md).toDiagnostic s!"modifies clause entry has non-composite type '{formatHighTypeVal ty}' and will be ignored"])
     ) ([], [])
     (.Opaque posts impl kept, diags)
   | other => (other, [])

Strata/Languages/Laurel/Resolution.lean

@@ -450,6 +450,10 @@ def resolveProcedure (proc : Procedure) : ResolveM Procedure := do
     let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr)
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    if !proc.isFunctional && body'.isTransparent then
+      let diag := proc.name.md.toDiagnostic
+        s!"transparent statement bodies are not supported. Add 'opaque' to make the procedure opaque"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     return { name := procName', inputs := inputs', outputs := outputs',
              isFunctional := proc.isFunctional,
@@ -475,6 +479,10 @@ def resolveInstanceProcedure (typeName : Identifier) (proc : Procedure) : Resolv
     let pres' ← proc.preconditions.mapM (·.mapM resolveStmtExpr)
     let dec' ← proc.decreases.mapM resolveStmtExpr
     let body' ← resolveBody proc.body
+    if !proc.isFunctional && body'.isTransparent then
+      let diag := proc.name.md.toDiagnostic
+        s!"transparent statement bodies are not supported. Add 'opaque' to make the procedure opaque"
+      modify fun s => { s with errors := s.errors.push diag }
     let invokeOn' ← proc.invokeOn.mapM resolveStmtExpr
     modify fun s => { s with instanceTypeName := savedInstType }
     return { name := procName', inputs := inputs', outputs := outputs',

Strata/Languages/Python/PythonRuntimeLaurelPart.lean

@@ -329,6 +329,7 @@ function List_len (l : ListAny) : int
 
 procedure List_len_pos(l : ListAny)
   invokeOn List_len(l)
+  opaque
   ensures List_len(l) >= 0;
 
 function List_contains (l : ListAny, x: Any) : bool
@@ -367,6 +368,7 @@ function List_take (l : ListAny, i: int) : ListAny
 
 procedure List_take_len(l : ListAny, i: int)
   invokeOn List_len(List_take(l,i))
+  opaque
   ensures i >= 0 && i <= List_len(l) ==> List_len(List_take(l,i)) == i;
 
 function List_drop (l : ListAny, i: int) : ListAny
@@ -379,6 +381,7 @@ function List_drop (l : ListAny, i: int) : ListAny
 
 procedure List_drop_len(l : ListAny, i: int)
   invokeOn List_len(List_drop(l,i))
+  opaque
   ensures i >= 0 && i <= List_len(l) ==> List_len(List_drop(l,i)) == List_len(l) - i;
 
 function int_max (i1: int, i2: int) : int
@@ -543,6 +546,7 @@ function Any_len_to_Any (v: Any) : Any {
 
 procedure Any_len_pos(v: Any)
   invokeOn Any_len(v)
+  opaque
   ensures Any_len(v) >= 0;
 
 function Any_iter_index(iter: Any, index: int) : Any;
@@ -1011,10 +1015,12 @@ function datetime_strptime(dtstring: Any, format: Any) : Any;
 
 procedure datetime_tostring_cancel(dt: Any)
   invokeOn datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d"))
+  opaque
   ensures datetime_strptime(to_string_any(dt), from_str ("%Y-%m-%d")) == dt;
 
 procedure datetime_date(d: Any) returns (ret: Any, error: Error)
   requires Any..isfrom_datetime(d) summary "(Origin_datetime_date_Requires)d_type"
+  opaque
   ensures Any..isfrom_datetime(ret) && Any..as_datetime!(ret) <= Any..as_datetime!(d) summary "ret_type"
 {
   var timedt: int;
@@ -1031,6 +1037,7 @@ procedure datetime_date(d: Any) returns (ret: Any, error: Error)
 };
 
 procedure datetime_now(tz: Any) returns (ret: Any)
+  opaque
   ensures Any..isfrom_datetime(ret) summary "ret_type"
 {
   var d: int;
@@ -1042,6 +1049,7 @@ procedure timedelta_func(days: Any, hours: Any) returns (delta : Any, maybe_exce
   requires Any..isfrom_None(hours) || Any..isfrom_int(hours) summary "(Origin_timedelta_Requires)hours_type"
   requires Any..isfrom_int(days) ==> Any..as_int!(days)>=0 summary "(Origin_timedelta_Requires)days_pos"
   requires Any..isfrom_int(hours) ==> Any..as_int!(hours)>=0 summary "(Origin_timedelta_Requires)hours_pos"
+  opaque
   ensures Any..isfrom_int(delta) && Any..as_int!(delta)>=0 summary "ret_pos"
 {
   var days_i : int := 0;
@@ -1063,6 +1071,7 @@ procedure test_helper_procedure(req_name : Any, opt_name : Any) returns (ret: An
   requires req_name == from_str("foo") summary "(Origin_test_helper_procedure_Requires)req_name_is_foo"
   requires (Any..isfrom_None(opt_name)) || (Any..isfrom_str(opt_name)) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_str"
   requires (opt_name == from_None()) || (opt_name == from_str("bar")) summary "(Origin_test_helper_procedure_Requires)req_opt_name_none_or_bar"
+  opaque
   ensures (Error..isNoError(maybe_except)) summary "ensures_maybe_except_none"
 {
   assert req_name == from_str("foo") summary "assert_name_is_foo";