Migrate Lido locked case to executable Verity contract

[Th0rgal]

Summary

• migrate the Lido vaulthub_locked case from a pure helper-only shape to an executable Verity contract entrypoint via VaultHubLocked.syncLocked
• restate the F-01 spec over contract post-state and bridge the executable run back to the arithmetic model in the reference proofs
• document the case structure and clarify that generated task files are public proof templates, not part of the green reference build

Verification

• lake build Benchmark.Cases.Lido.VaulthubLocked.Compile
• ./scripts/run_case.sh lido/vaulthub_locked
• lake build Benchmark.Generated.Lido.VaulthubLocked.Tasks.ReserveRatioBounds now fails only at the intentional ?_ placeholder in the public template

---

Note

Medium Risk
Refactors the vaulthub_locked benchmark from a pure model to an executable contract run with new storage effects (slot 6) and updates specs/proofs accordingly, so mistakes could invalidate the intended solvency property despite being proof-checked.

Overview
Migrates the Lido vaulthub_locked benchmark to an executable Verity entrypoint VaultHubLocked.syncLocked that computes the _locked amount from storage slots 0..5, stores the result in a new lockedAmount slot 6, and returns it.

Restates the F-01 solvency spec over the post-state of running syncLocked (reading s'.storage 6), adds helpers (vaultState, lockedRunResult, lockedPostState) to model execution, and updates reference proofs to bridge the executable run back to the existing pure locked arithmetic lemma.

Minor generated task templates are adjusted to open Verity, and the case README is updated to document the new executable-contract shape and clarify generated task files are public templates (not part of the green build).

^{Written by Cursor Bugbot for commit 7eb60a2. This will update automatically on new commits. Configure here.}