Laurel: avoid quantified modifies frames when using array theory

Strata/Cli/VerifyOptions.lean

@@ -173,7 +173,8 @@ def parseLaurelVerifyOptions (pflags : ParsedFlags)
   let translateOptions : LaurelTranslateOptions :=
     { base.translateOptions with
       keepAllFilesPrefix
-      overflowChecks := verifyOptions.overflowChecks }
+      overflowChecks := verifyOptions.overflowChecks
+      enumeratedModifiesClauses := verifyOptions.useArrayTheory }
   return { translateOptions, verifyOptions }
 
 end -- public section

Strata/Languages/Laurel/ConstrainedTypeElim.lean

@@ -248,7 +248,7 @@ public def constrainedTypeElimPass : LoweringPass where
   name := "ConstrainedTypeElim"
   documentation := "Eliminates constrained types by replacing them with their base types and generating constraint-checking functions and witness procedures. Type tests against constrained types are rewritten to call the generated constraint function."
   needsResolves := true
-  run := fun p m _ =>
+  run := fun _ p m =>
     let (p', diags) := constrainedTypeElim m p
     (p', diags, {})
 

Strata/Languages/Laurel/ContractPass.lean

@@ -453,7 +453,7 @@ public def contractPass : LoweringPass where
   documentation := "Lowers pre and postcondition to assertions and assumptions around call-sites and procedure bodies"
   comesAfter := [⟨ eliminateReturnStatementsPass.meta, "The contract pass wraps the body of procedures to get: `assume preconditions; body; assert postconditions`. Eliminating returns first means that the postcondition assertions are guaranteed to execute."⟩ ]
   needsResolves := true
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let (p', diags) := lowerContracts p
     (p', diags, {})
 

Strata/Languages/Laurel/CoreGroupingAndOrdering.lean

@@ -267,7 +267,7 @@ then collecting datatypes and constants.
 Functions are grouped into SCCs (for mutual recursion). Proofs are emitted
 as individual `procedure` decls. Both participate in the topological ordering
 so that axioms are available to functions that need them."
-  run := fun p _ _ =>
+  run := fun _ p _ =>
     (orderFunctionsAndProcedures p, [], {})
 
 end Strata.Laurel

Strata/Languages/Laurel/DesugarShortCircuit.lean

@@ -59,7 +59,7 @@ end -- public section
 public def desugarShortCircuitPass : LoweringPass where
   name := "DesugarShortCircuit"
   documentation := "Rewrites short-circuit boolean operators (`&&` and `||`) into equivalent conditional expressions. This simplifies subsequent passes and the final translation to Core, which does not have short-circuit semantics built in."
-  run := fun p _ _ =>
+  run := fun _ p _ =>
     (desugarShortCircuit p, [], {})
   comesBefore := [
       ⟨ liftImperativeExpressionsPass.meta, "The desugar short circuit pass introduces if-then-else expressions whose control-flow must be taken into account by the lifting pass."⟩]

Strata/Languages/Laurel/EliminateDeterministicHoles.lean

@@ -93,7 +93,7 @@ end -- public section
 public def eliminateDeterministicHolesPass : LoweringPass where
   name := "EliminateDeterministicHoles"
   documentation := "Replaces every deterministic hole with a call to a freshly generated uninterpreted function. After this pass the program contains only non-deterministic holes. Assumes `InferHoleTypes` has already annotated holes with types."
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let (p', stats) := eliminateDeterministicHoles p
     (p', [], stats)
 

Strata/Languages/Laurel/EliminateDoWhile.lean

@@ -76,7 +76,7 @@ def eliminateDoWhile (program : Program) : Program :=
 public def eliminateDoWhilePass : LoweringPass where
   name := "EliminateDoWhile"
   documentation := "Lowers post-test `While` loops (the `do … while` form) into the pre-test loop `{ while(true) invariant I { BODY; if (!COND) exit L } } L`, with a fresh `$`-prefixed exit label `L`. Runs early so no later pass observes a post-test loop; the invariant is checked at the loop head, matching `while`."
-  run := fun p _m _ => (eliminateDoWhile p, [], {})
+  run := fun _ p _m => (eliminateDoWhile p, [], {})
 
 end -- public section
 end Strata.Laurel

Strata/Languages/Laurel/EliminateIncrDecr.lean

@@ -103,7 +103,7 @@ def eliminateIncrDecr (program : Program) : Program :=
 public def eliminateIncrDecrPass : LoweringPass where
   name := "EliminateIncrDecr"
   documentation := "Lowers Java-style increment/decrement operators (`++x`, `x++`, `--x`, `x--`) into existing Laurel assignment and arithmetic constructs. Prefix forms yield the new value; postfix forms yield the old value. Runs early so that no later pass observes an `.IncrDecr` node."
-  run := fun p _m _ => (eliminateIncrDecr p, [], {})
+  run := fun _ p _m => (eliminateIncrDecr p, [], {})
 
 end -- public section
 end Strata.Laurel

Strata/Languages/Laurel/EliminateReturnStatements.lean

@@ -73,7 +73,7 @@ def eliminateReturnStatements (program : Program) : Program :=
 public def eliminateReturnStatementsPass : LoweringPass where
   name := "EliminateReturnStatements"
   documentation := "Lower return statements to exit statements. Wrap each procedure body with a 'return' block"
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let p' := eliminateReturnStatements p
     (p', [], {})
   -- comesBefore := [contractPass]

Strata/Languages/Laurel/EliminateValueInReturns.lean

@@ -95,6 +95,6 @@ end -- public section
 public def eliminateValueInReturnsPass : LoweringPass where
   name := "EliminateValueInReturns"
   documentation := "Rewrites `return expr` into `outParam := expr; return` for imperative procedures that have an output parameter. This decouples the return-value assignment from the final Core translation, which no longer needs to know about output parameters when translating returns."
-  run := fun p _m _ => (eliminateValueInReturnsTransform p, [], {})
+  run := fun _ p _m => (eliminateValueInReturnsTransform p, [], {})
 
 end Laurel

Strata/Languages/Laurel/HeapParameterization.lean

@@ -585,7 +585,7 @@ public def heapParameterizationPass : LoweringPass where
   name := "HeapParameterization"
   documentation := "Transforms procedures that interact with the heap by adding explicit heap parameters. The heap is modeled as `Map Composite (Map Field Box)`. Procedures that write the heap receive both an input and output heap parameter; procedures that only read the heap receive an input heap parameter. Field reads and writes are rewritten to use `readField` and `updateField` functions."
   needsResolves := false -- Only resolve again after completing HeapParam, ModifiesClauses and TypeHierarchy. These are logically one pass.
-  run := fun p m _ =>
+  run := fun _ p m =>
     (heapParameterization m p, [], {})
   comesAfter := [⟨ eliminateValueInReturnsPass.meta, "eliminate value in returns need to come before any passes that change the amount of output parameters of procedures." ⟩]
   comesBefore := [⟨ liftImperativeExpressionsPass.meta, "the heap parameterization pass introduces assignments (to the heap variables) that need to be lifted."⟩]

Strata/Languages/Laurel/InferHoleTypes.lean

@@ -195,7 +195,7 @@ end -- public section
 public def inferHoleTypesPass : LoweringPass where
   name := "InferHoleTypes"
   documentation := "Annotates every verification hole (`.Hole`) in the program with a type inferred from context. This type information is needed by subsequent passes that replace holes with uninterpreted functions or nondeterministic values."
-  run := fun p m _ =>
+  run := fun _ p m =>
     let (p', diags, stats) := inferHoleTypes m p
     (p', diags, stats)
   comesBefore := [

Strata/Languages/Laurel/LaurelCompilationPipeline.lean

@@ -148,7 +148,7 @@ private def runLaurelPasses
   let mut allStats : Statistics := {}
 
   for pass in laurelPipeline do
-    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run program model options)
+    let (program', diags, stats) ← pctx.withPhase pass.name do pure (pass.run options program model)
     program := program'
     allDiags := allDiags ++ diags
     allStats := allStats.merge stats
@@ -207,13 +207,13 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
   if passDiags.any (·.type != .Warning) then
     return (none, passDiags, program, stats)
 
-  let unorderedCore := (transparencyPass.run program model options).1
+  let unorderedCore := (transparencyPass.run options program model).1
   emit "transparencyPass" "core.st" unorderedCore
   let mut unorderedCore := unorderedCore
   let mut fnModel := model
 
   for pass in unorderedCorePipeline do
-    unorderedCore := (pass.run unorderedCore fnModel options).1
+    unorderedCore := (pass.run options unorderedCore fnModel).1
     if pass.needsResolves then
       let compositeTypes := program.types.filter (fun t => match t with | .Composite _ => true | _ => false)
       let (uc', m', errors) := resolveUnorderedCore unorderedCore (some fnModel) compositeTypes
@@ -227,10 +227,10 @@ def translateWithLaurel (options : LaurelTranslateOptions) (program : Program)
       fnModel := m'
     emit pass.name "unorderedCoreWithLaurelTypes.st" unorderedCore
 
-  let coreWithLaurelTypes := (orderingPass.run unorderedCore model options).1
+  let coreWithLaurelTypes := (orderingPass.run options unorderedCore model).1
 
   emit "CoreWithLaurelTypes" "core.st" coreWithLaurelTypes
-  let (coreProgram, coreDiagnostics, _) := laurelToCoreSchemaPass.run coreWithLaurelTypes fnModel options
+  let (coreProgram, coreDiagnostics, _) := laurelToCoreSchemaPass.run options coreWithLaurelTypes fnModel
   let mut allDiagnostics: List DiagnosticModel := passDiags ++ coreDiagnostics;
 
   emit "Core" "core.st" coreProgram

Strata/Languages/Laurel/LaurelPass.lean

@@ -16,6 +16,10 @@ public section
 structure LaurelTranslateOptions where
   inlineFunctionsWhenPossible : Bool := false
   overflowChecks : Core.OverflowChecks := {}
+  /-- Quantifier-free modifies frame for single-reference clauses. Set-valued entries
+      keep the quantified frame. If the procedure's modifies clause contains sets,
+      this option has no effect. Use with the verifier's `useArrayTheory`. -/
+  enumeratedModifiesClauses : Bool := false
   keepAllFilesPrefix : Option String := none
 
 instance : Inhabited LaurelTranslateOptions where
@@ -52,7 +56,7 @@ end
     metadata fields remain directly accessible (e.g. `p.name`). -/
 structure LaurelPass (Input: Type) (Output: Type) extends PassMeta where
   /-- The pass action. -/
-  run : Input → SemanticModel → LaurelTranslateOptions → Output × List DiagnosticModel × Statistics
+  run : LaurelTranslateOptions → Input → SemanticModel → Output × List DiagnosticModel × Statistics
 
 abbrev LoweringPass := LaurelPass Laurel.Program Laurel.Program
 

Strata/Languages/Laurel/LaurelToCoreSchemaPass.lean

@@ -806,7 +806,7 @@ public def laurelToCoreSchemaPass : LaurelPass CoreWithLaurelTypes Core.Program
   - The @[cases] parameter is inferred for recursive functions.
   - Laurel parameter definitions are translated to Core ones.
   - Laurel calling conventions are translated to Core ones."
-  run := fun p fnModel options =>
+  run := fun options p fnModel =>
     let initState : TranslateState := { model := fnModel, overflowChecks := options.overflowChecks }
     let (coreProgramOption, translateState) :=
       runTranslateM initState (translateLaurelToCore options p)

Strata/Languages/Laurel/LiftImperativeExpressions.lean

@@ -688,7 +688,7 @@ public def liftImperativeExpressionsPass : LaurelPass UnorderedCoreWithLaurelTyp
   documentation := "Lifts assignments and other imperative expressions that appear in expression contexts into preceding statements. This is necessary because Strata Core does not support assignments within expressions. The pass introduces fresh temporary variables where needed."
   comesAfter := [⟨ transparencyPass.meta, "The imperative expression lifting is only done in procedures, so it comes after the transparency pass"⟩]
   needsResolves := true
-  run := fun p m _ =>
+  run := fun _ p m =>
     (liftImperativeExpressionsInCore p m, [], {})
 
 end Laurel

Strata/Languages/Laurel/LiftInstanceProcedures.lean

@@ -129,7 +129,7 @@ public def liftInstanceProceduresPass : LoweringPass where
   name := "LiftInstanceProcedures"
   documentation := "Lifts every procedure declared inside a `composite` block to a top-level static procedure named `<CompositeName>$<methodName>` and rewrites call sites resolved to an instance procedure (including `obj#method(args)` surface syntax) to point at the lifted name. Clears `instanceProcedures` on every composite. Must run before HeapParameterization."
   needsResolves := true
-  run := fun p m _ => (liftInstanceProcedures m p, [], {})
+  run := fun _ p m => (liftInstanceProcedures m p, [], {})
   comesBefore := [⟨ eliminateValueInReturnsPass.meta, "eliminateValueInReturns only applies to static methods, hence all instance methods must have been lifted before." ⟩]
 
 end Strata.Laurel

Strata/Languages/Laurel/MergeAndLiftReturns.lean

@@ -93,7 +93,7 @@ public def mergeAndLiftReturnsPass : LoweringPass where
   documentation := "Attempts to merge and lift returns so that only a single outer return remains, enabling the procedure to be more easily converted to a functional form."
   needsResolves := true
   comesBefore := [⟨ eliminateValueInReturnsPass.meta, "Lifts returns with a value, so the value should not yet have been lowered."⟩]
-  run := fun p _m _ =>
+  run := fun _ p _m =>
     let (p', diags) := mergeAndLiftReturns p
     (p', diags, {})