Laurel: rename buildPointwiseFrame to buildQuantifiedFrame

Author: julesmt

Strata/Languages/Laurel/ModifiesClauses.lean

@@ -74,13 +74,13 @@ def conjoinAll (exprs : List StmtExprMd) : StmtExprMd :=
   | first :: rest => rest.foldl (fun acc e => mkMd <| .PrimitiveOp .And [acc, e]) first
 
 /--
-Pointwise frame: every allocated object the `modifies` clause does not name keeps
+Quantified (pointwise) frame: every allocated object the `modifies` clause does not name keeps
 all of its field values across the call.
 
   forall $obj: Composite, $fld: Field =>
     notModified($obj) && $obj < old($heap).nextReference ==> readField(old($heap), $obj, $fld) == readField($heap, $obj, $fld)
 -/
-def buildPointwiseFrame (proc : Procedure) (entries : List ModifiesEntry)
+def buildQuantifiedFrame (proc : Procedure) (entries : List ModifiesEntry)
     (heapIn heapOut : StmtExprMd) : StmtExprMd :=
   let objName : Identifier := "$modifies_obj"
   let fldName : Identifier := "$modifies_fld"
@@ -155,15 +155,15 @@ def transformModifiesClauses (model: SemanticModel)
         if useEnumeratedFrame && onlyIndividualRefs entries then
           -- Callers assume the quantifier-free frame; the body re-checks the
           -- pointwise frame at every exit.
-          let pointwise := buildPointwiseFrame proc entries heapIn heapOut
+          let pointwise := buildQuantifiedFrame proc entries heapIn heapOut
           let framePost : Condition :=
             { condition := buildEnumeratedFrame proc entries heapIn heapOut,
               summary := "modifies clause", free := true }
           let impl' := impl.map (insertFrameChecks proc pointwise)
           .ok { proc with body := .Opaque (postconds ++ [framePost]) impl' [] }
         else
           let framePost : Condition :=
-            { condition := buildPointwiseFrame proc entries heapIn heapOut,
+            { condition := buildQuantifiedFrame proc entries heapIn heapOut,
               summary := "modifies clause" }
           .ok { proc with body := .Opaque (postconds ++ [framePost]) impl [] }
       else

StrataTest/Languages/Laurel/ModifiesFrameQuantifierFreeTest.lean

@@ -7,7 +7,7 @@
 /-
 Structural check, independent of the solver: the enumerated modifies frame
 (`buildEnumeratedFrame`) must contain no quantifier, so there is nothing for the
-solver to instantiate. The `∀`-based frame it replaces (`buildPointwiseFrame`)
+solver to instantiate. The `∀`-based frame it replaces (`buildQuantifiedFrame`)
 does contain one; asserting both pins the property and shows the check
 discriminates between the two encodings.
 -/
@@ -29,6 +29,6 @@ private def hasQuantifier (e : StmtExprMd) : Bool :=
   (s.splitOn "forall").length > 1 || (s.splitOn "exists").length > 1
 
 #guard !hasQuantifier (buildEnumeratedFrame default singleRefModifies heapIn heapOut)
-#guard  hasQuantifier (buildPointwiseFrame   default singleRefModifies heapIn heapOut)
+#guard  hasQuantifier (buildQuantifiedFrame   default singleRefModifies heapIn heapOut)
 
 end StrataTest.Laurel.ModifiesFrameQuantifierFree