perf: improve join point finding

[hargoniX]

This PR improves join point finding in the compiler through two means:

1. We now handle situations where a function f can only become a join point when a function g
   becomes a join point as well correctly.
2. We introduce a second join point finding pass after specialisation and before the following
   simplification pass, as the specialiser might have introduced new join point opportunities for
   the simplifier to exploit.

Notably in the code from #10995 we now correctly detect the missing join point which required both
of these changes to be made.

Closes: #10995

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 3f1522d against 19533ab are in! @hargoniX

[leanprover-community-bot]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 19533ab1d4312903f98ff0429a5962db24ce402b --onto 3a42ee0c3060e2a8365927d205ead5990366053d. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-28 18:52:37)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase a51822ead20707e1114066b4908c3220fb8fe39e --onto 106b0fa661d96fd1fa6ff96e2ee5f55f23f307f2. You can force Mathlib CI using the force-mathlib-ci label. (2025-10-29 16:24:08)

[leanprover-bot]

Reference manual CI status:

• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 19533ab1d4312903f98ff0429a5962db24ce402b --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-28 18:52:38)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase a51822ead20707e1114066b4908c3220fb8fe39e --onto d3dda9f6d4428a906c096067ecb75e432afc4615. You can force reference manual CI using the force-manual-ci label. (2025-10-29 16:24:10)

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 4442762 against a51822e are in! @hargoniX

Minor changes (1)

• stdlib//instructions changed by -0.1% (✅).

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 02bcc41 against a51822e are in! @hargoniX

Minor changes (3)

• big_beq//instructions changed by +0.5% (🟥).
• iterators (elab)//instructions changed by +1.1% (🟥).
• stdlib//instructions changed by +0.2% (🟥).

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for 79e0306 against a51822e are in! @hargoniX

Minor changes (3)

• big_beq//instructions changed by +0.5% (🟥).
• iterators (elab)//instructions changed by +1.1% (🟥).
• stdlib//instructions changed by +0.2% (🟥).

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for db7cda4 against a51822e are in! @hargoniX

Minor changes (1)

• stdlib//instructions changed by -0.2% (✅).

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 5a0b63a against a51822e are in! @hargoniX

Minor changes (3)

• big_beq//instructions changed by +0.5% (🟥).
• iterators (elab)//instructions changed by +1.1% (🟥).
• stdlib//instructions changed by +0.2% (🟥).

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for b8bd409 against a51822e are in! @hargoniX

Runs (1)

• other exited with code -1 (🟥)

Minor changes (1)

• stdlib//instructions changed by -0.2% (✅).

[leanprover-bot]

Here are the benchmark results for commit 5a0b63a.
There were significant changes against commit a51822e:

  Benchmark          Metric          Change
  ==================================================
+ channel.lean       unbounded_seq    -2.7%
- iterators (elab)   instructions      1.1% (29.1 σ)

[hargoniX]

!radar

[leanprover-radar]

Benchmark results for c31beeb against a51822e are in! @hargoniX

Minor changes (1)

• stdlib//instructions changed by -0.2% (✅).