fix: invariants of the ST.Ref implementation

[hargoniX]

This PR fixes the remaining issues with ST.Ref. We now enforce that ST.Ref acts truly like a spinlock by introducing two changes:

1. ST.Ref.set is now just discard <| ST.Ref.swap and fulfills no special purpose for closing the critical section opened by ST.Ref.take anymore
2. We introduce an unsafe function called ST.Ref.put which may only be called after a critical section has been opened using the unsafe ST.Ref.take. We then implement modify and friends using these operations.

In addition, enforcing that ST.Ref is a proper spinlock allows us to remove a few branches around previous races with ST.Ref.set.

The PR is accompanied by a formalization on the stref-veil repo: TODO

[hargoniX]

!bench

[leanprover-radar]

Benchmark results for 270f2c7 against 5847d9b are in. No significant results found. @hargoniX

• ✅ build//instructions: -11.4G (-0.10%)

New metrics (19✅, 43🟥, 1)

• ✅ elab/bv_decide_incremental//cycles: -15.9M (-0.03%)
• 🟥 elab/bv_decide_incremental//instructions: +146.0M (+0.13%)
• ✅ elab/bv_decide_incremental//many_medium_hyps_many_goals_inc: -5ms (-0.30%)
• 🟥 elab/bv_decide_incremental//many_medium_hyps_many_goals_noninc: +21ms (+0.83%)
• 🟥 elab/bv_decide_incremental//many_medium_hyps_many_goals_speedup: +17.5mx (+1.14%)
• 🟥 elab/bv_decide_incremental//many_medium_hyps_one_goal_inc: +9ms (+1.50%)
• 🟥 elab/bv_decide_incremental//many_medium_hyps_one_goal_noninc: +1ms (+0.16%)
• ✅ elab/bv_decide_incremental//many_medium_hyps_one_goal_speedup: -13.5mx (-1.31%)
• 🟥 elab/bv_decide_incremental//many_small_hyps_many_goals_inc: +3ms (+0.24%)
• 🟥 elab/bv_decide_incremental//many_small_hyps_many_goals_noninc: +8ms (+0.56%)
• 🟥 elab/bv_decide_incremental//many_small_hyps_many_goals_speedup: +3.7mx (+0.32%)
• 🟥 elab/bv_decide_incremental//many_small_hyps_one_goal_inc: +2ms (+0.99%)
• 🟥 elab/bv_decide_incremental//many_small_hyps_one_goal_noninc: +1ms (+0.50%)
• ✅ elab/bv_decide_incremental//many_small_hyps_one_goal_speedup: -4.8mx (-0.49%)
• ✅ elab/bv_decide_incremental//maxrss: -414kiB (-0.02%)
• 🟥 elab/bv_decide_incremental//one_big_hyp_many_goals_inc: +4ms (+0.28%)
• 🟥 elab/bv_decide_incremental//one_big_hyp_many_goals_noninc: +22ms (+1.11%)
• 🟥 elab/bv_decide_incremental//one_big_hyp_many_goals_speedup: +11.6mx (+0.82%)
• elab/bv_decide_incremental//one_big_hyp_one_goal_inc: +0s (+0.00%)
• 🟥 elab/bv_decide_incremental//one_big_hyp_one_goal_noninc: +13ms (+2.40%)
• and 43 more

Small changes (3✅, 1🟥)

• 🟥 build/module/Init.System.ST//instructions: +31.8M (+2.09%)
• ✅ compiled/deriv//maxrss: -367kiB (-0.07%)
• ✅ compiled/select//instructions: -21.2M (-0.77%)
• ✅ elab/big_do//instructions: -20.3M (-0.11%)

[mathlib-lean-pr-testing]

Mathlib CI status (docs):

• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 5847d9b42750a5a1552088d483fd05b97743cb13 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-13 13:07:00)

[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 5847d9b42750a5a1552088d483fd05b97743cb13 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-13 13:07:02)