Defining invariant that CachedAnalysis must hold, update PrecondElim

[MikaelMayer]

Fixes #702

Problem

PrecondElim generates WF (well-formedness) checking procedures but did not update the cached call graph. This meant any downstream transform relying on the call graph would see stale data after PrecondElim.

Solution

• Document the CachedAnalyses invariant: when the call graph is present, it must reflect the current program's procedure call structure. Transforms must update it or invalidate it.
• Add CallGraph.addLeafNode for inserting nodes with no callees.
• Update PrecondElim to register generated WF procedures as leaf nodes in the call graph (they contain only assert/assume statements and make no procedure calls).

Note: the manual filtering in the Verifier's selective verification pipeline remains because CallElim does not yet maintain the call-graph invariant. Once CallElim also updates the call graph (removing call edges when it inlines contracts), FilterProcedures could replace the manual filtering entirely. This PR lays the groundwork by documenting the invariant and showing the pattern.

Testing

All existing tests pass.

[MikaelMayer]

after this patch, is FilterProcedure usable instead of the manual filtering introduced in #687?

[MikaelMayer]

Not yet — this patch only maintains the call-graph invariant for PrecondElim (registering WF procedures as leaf nodes). The manual filtering in the Verifier exists because FilterProcedures.run includes transitive callees via call-graph closure, which pulls prelude functions back in.

For FilterProcedures to replace the manual filtering, CallElim would also need to maintain the invariant by removing call edges when it inlines contracts. Once that's done, the call graph after CallElim + PrecondElim would accurately reflect that target procedures no longer call prelude functions, and FilterProcedures would work correctly.

This PR lays the groundwork for that by documenting the invariant and showing the pattern (addWFProcToCallGraph), but the CallElim update is a separate piece of work.

[MikaelMayer]

Good catch — the PR description was overclaiming. I've updated it to remove the bullet about moving FilterProcedures.run and added a note explaining that the manual filtering remains because CallElim doesn't yet maintain the call-graph invariant. This PR lays the groundwork (documenting the invariant and showing the pattern with addWFProcToCallGraph), and CallElim updating the call graph would be a follow-up.