[PVerifier] Improve proof speed by not generating unused procedures

[TheKK]

I found that there are unused procedures stand inside .ucl files generated by PVerifier backend and we get visible speed up (about 10% for Advanced/4_Paxos) in time after removing them.

This speed up should be positively correlated to the number of handlers of the entire system, thus give us better experience in the iteration of proofing.

I'll add some number later and also want to make sure that I didn't miss anything about call dependencies for entry/event_handler in .ucl files.

Please let me know if there's anything I could do better :)

[TheKK]

Here's the result of running all examples in repo and seems that we got about 10%~25% speed up.

Benchmark 1: ~modified-p compile -pp 1_ChainReplicationVerification/ChainReplicationVerification.pproj
  Time (abs ≡):        27.259 s               [User: 173.720 s, System: 7.950 s]
Benchmark 2: p compile -pp 1_ChainReplicationVerification/ChainReplicationVerification.pproj
  Time (abs ≡):        30.247 s               [User: 175.938 s, System: 8.245 s]
Summary
  ~modified-p compile -pp 1_ChainReplicationVerification/ChainReplicationVerification.pproj ran
    1.11 times faster than p compile -pp 1_ChainReplicationVerification/ChainReplicationVerification.pproj

Benchmark 1: ~modified-p compile -pp 2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj
  Time (abs ≡):        44.393 s               [User: 283.704 s, System: 13.295 s]
Benchmark 2: p compile -pp 2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj
  Time (abs ≡):        49.930 s               [User: 312.367 s, System: 13.609 s]
Summary
  ~modified-p compile -pp 2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj ran
    1.12 times faster than p compile -pp 2_TwoPhaseCommitVerification/KeyValue/TwoPhaseCommitVerification.pproj

Benchmark 1: ~modified-p compile -pp 2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj
  Time (abs ≡):        23.992 s               [User: 144.704 s, System: 6.826 s]
Benchmark 2: p compile -pp 2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj
  Time (abs ≡):        28.363 s               [User: 164.549 s, System: 7.879 s]
Summary
  ~modified-p compile -pp 2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj ran
    1.18 times faster than p compile -pp 2_TwoPhaseCommitVerification/Rounds/TwoPhaseCommitVerification.pproj

Benchmark 1: ~modified-p compile -pp 2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj
  Time (abs ≡):        108.964 s               [User: 659.741 s, System: 32.760 s]
Benchmark 2: p compile -pp 2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj
  Time (abs ≡):        132.758 s               [User: 847.269 s, System: 38.617 s]
Summary
  ~modified-p compile -pp 2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj ran
    1.22 times faster than p compile -pp 2_TwoPhaseCommitVerification/Single/TwoPhaseCommitVerification.pproj

Benchmark 1: ~modified-p compile -pp 3_RingLeaderVerification/RingLeaderVerification.pproj
  Time (abs ≡):        26.214 s               [User: 156.995 s, System: 8.448 s]
Benchmark 2: p compile -pp 3_RingLeaderVerification/RingLeaderVerification.pproj
  Time (abs ≡):        32.203 s               [User: 163.893 s, System: 8.467 s]
Summary
  ~modified-p compile -pp 3_RingLeaderVerification/RingLeaderVerification.pproj ran
    1.23 times faster than p compile -pp 3_RingLeaderVerification/RingLeaderVerification.pproj

Benchmark 1: ~modified-p compile -pp 4_Paxos/PVerifiedPaxos.pproj
  Time (abs ≡):        490.009 s               [User: 3307.878 s, System: 151.284 s]
Benchmark 2: p compile -pp 4_Paxos/PVerifiedPaxos.pproj
  Time (abs ≡):        605.831 s               [User: 4063.889 s, System: 180.511 s]
Summary
  ~modified-p compile -pp 4_Paxos/PVerifiedPaxos.pproj ran
    1.24 times faster than p compile -pp 4_Paxos/PVerifiedPaxos.pproj

Benchmark 1: ~modified-p compile -pp 5_Consensus/Consensus.pproj
  Time (abs ≡):        19.682 s               [User: 116.744 s, System: 6.099 s]
Benchmark 2: p compile -pp 5_Consensus/Consensus.pproj
  Time (abs ≡):        25.228 s               [User: 134.031 s, System: 6.692 s]
Summary
  ~modified-p compile -pp 5_Consensus/Consensus.pproj ran
    1.28 times faster than p compile -pp 5_Consensus/Consensus.pproj

Benchmark 1: ~modified-p compile -pp 6_DistributedLock/DistributedLock.pproj
  Time (abs ≡):         7.310 s               [User: 41.898 s, System: 2.308 s]
Benchmark 2: p compile -pp 6_DistributedLock/DistributedLock.pproj
  Time (abs ≡):         9.184 s               [User: 43.424 s, System: 2.333 s]
Summary
  ~modified-p compile -pp 6_DistributedLock/DistributedLock.pproj ran
    1.26 times faster than p compile -pp 6_DistributedLock/DistributedLock.pproj

Benchmark 1: ~modified-p compile -pp 7_ShardedKV/ShardedKV.pproj
  Time (abs ≡):         7.225 s               [User: 40.830 s, System: 2.087 s]
Benchmark 2: p compile -pp 7_ShardedKV/ShardedKV.pproj
  Time (abs ≡):         9.134 s               [User: 43.148 s, System: 2.209 s]
Summary
  ~modified-p compile -pp 7_ShardedKV/ShardedKV.pproj ran
    1.26 times faster than p compile -pp 7_ShardedKV/ShardedKV.pproj

Benchmark 1: ~modified-p compile -pp 8_LockServer/LockServer.pproj
  Time (abs ≡):        25.263 s               [User: 158.151 s, System: 8.087 s]
Benchmark 2: p compile -pp 8_LockServer/LockServer.pproj
  Time (abs ≡):        29.718 s               [User: 168.993 s, System: 7.582 s]
Summary
  ~modified-p compile -pp 8_LockServer/LockServer.pproj ran
    1.18 times faster than p compile -pp 8_LockServer/LockServer.pproj

[FedericoAureliano]

Very cool and makes sense! Is there an issue when a function appears as a dependency twice? I am not sure this is possible, but I think it would lead to multiple generations of the same function, since you are using a list to keep track of the dependencies.

[ankushdesai]

Nice find — the speedups are very real and consistent. Two things to consider before this is ready:

1. Federico's dedup question. In the current diff this is actually not triggerable: GenerateEntryHandler only ever appends s.Entry (the one else branch), and GenerateEventHandler returns at most one element from its switch. So per GenerateMain call the list has 0 or 1 items. That said, switching List<Function> → HashSet<Function> is cheap insurance and makes the dedup intent explicit — especially relevant for point 2.

2. Transitive callees — possible correctness gap. GenerateMachineProcedures previously emitted every entry in m.Methods, which includes both anonymous handler bodies and named machine-scoped funs. The new code only emits the handler's direct callee (s.Entry or EventDoAction.Target). But that callee's body can itself contain FunCallStmts, which the codegen lowers unconditionally at Uclid5CodeGenerator.cs:1801-1804 as call <other_fun>(...). If the entry function calls a named helper, the helper's procedure is no longer emitted and Uclid will hit an unresolved call.

Sketch:
```p
machine M {
fun helper() { /* ... */ }
state Init { entry { helper(); } }
}
```
Before this PR, `helper` was always emitted (it's in `m.Methods`). After, only `s.Entry` is — so `call helper(...)` inside the entry body is dangling.

Why the benchmarks still all pass: I checked `Tutorial/Advanced/*Verification` and none of them declare machine-scoped named `fun`s — the only `fun` declarations are top-level globals (`RandomInt`, `RandomParticipant`) which flow through `GenerateGlobalProcedures`, a separate code path. So this benchmark set never exercises machine-method → machine-method calls; the perf wins are sound but the test surface doesn't catch the issue.

Suggested fix: compute the transitive call closure from the handler's direct callee — walk each function's body collecting `FunCallStmt` targets whose `Function.Owner == machine`, until fixpoint. A `HashSet` naturally handles both this and Federico's dedup point. Adding a small regression test with a machine helper that calls another helper would lock the invariant in.

Minor nit while you're in there: `functionDependeicies` typo in `GenerateMain` (spelled correctly as `functionDependencies` inside `GenerateEntryHandler`).