Defining invariant that CachedAnalysis must hold, update PrecondElim

Strata/Languages/Core/CallGraph.lean

@@ -64,6 +64,10 @@ def CallGraph.decrementEdge (cg : CallGraph) (caller : String) (callee : String)
     callers := new_callers
   }
 
+/-- Add a node with no callees to the call graph. -/
+def CallGraph.addLeafNode (cg : CallGraph) (name : String) : CallGraph :=
+  { cg with callees := cg.callees.insert name {} }
+
 /-- BFS worker for transitive closure. `getNeighbors` provides the edges.
 `allNodes` is a fixed universe of node names (all keys in the graph);
 termination is proved via the lexicographic measure

Strata/Transform/CoreTransform.lean

@@ -85,7 +85,13 @@ def isGlobalVar (p : Program) (ident : Expression.Ident) : Bool :=
 
 
 /-- Cached results of program analyses that are helpful for program
-    transformation. -/
+    transformation.
+
+    Invariant: When `callGraph` is `some cg`, `cg` must reflect the current
+    program's procedure call structure. Every procedure in the program must
+    have an entry in `cg.callees`, and every call edge must be accounted for.
+    Transforms that add, remove, or modify procedures must update the call
+    graph accordingly (or set it to `.none` to invalidate it). -/
 structure CachedAnalyses where
   callGraph: Option CallGraph := .none
 

Strata/Transform/PrecondElim.lean

@@ -277,6 +277,14 @@ end
 
 /-! ## Main transformation -/
 
+/-- Add a WF procedure as a leaf node in the cached call graph.
+WF procedures contain only assert/assume statements and make no procedure calls. -/
+private def addWFProcToCallGraph (name : String) : CoreTransformM Unit :=
+  modify fun σ => match σ.cachedAnalyses.callGraph with
+  | .some cg => { σ with cachedAnalyses := { σ.cachedAnalyses with
+      callGraph := .some (cg.addLeafNode name) } }
+  | .none => σ
+
 /--
 Transform an entire program:
 1. For each procedure, transform its body and if needed generate a WF procedure
@@ -305,7 +313,9 @@ where
         let procDecl := Decl.proc proc' md
         let (changed', rest') ← transformDecls rest
         match mkContractWFProc F proc md with
-        | some wfDecl => return (true, wfDecl :: procDecl :: rest')
+        | some wfDecl => do
+          addWFProcToCallGraph (wfProcName (CoreIdent.toPretty proc.header.name))
+          return (true, wfDecl :: procDecl :: rest')
         | none => return (changed || changed', procDecl :: rest')
       | .func func md => do
         let F ← getFactory
@@ -316,7 +326,9 @@ where
         let hasPreconds := !func.preconditions.isEmpty
         let (changed, rest') ← transformDecls rest
         match mkFuncWFProc F' func md with
-        | some wfDecl => return (true, wfDecl :: funcDecl :: rest')
+        | some wfDecl => do
+          addWFProcToCallGraph (wfProcName (CoreIdent.toPretty func.name))
+          return (true, wfDecl :: funcDecl :: rest')
         | none => return (changed || hasPreconds, funcDecl :: rest')
       | .recFuncBlock funcs md => do
         let F ← getFactory