test: add vcgen benchmark over the verina corpus

Add `tests/bench/vcgenVerina.lean`: the Verina verification corpus (27 programs plus two intrinsic re-proofs), each discharged with `vcgen … with finish` in the `Std.Internal.Do` Hoare logic, every fixture in its own namespace with `@[local grind]` lemmas.

Everything `vcgen` cannot discharge on its own, the supporting lemmas and a few manual verification-condition steps, is `sorry`'d following the `dag_hassorry_issue.lean` precedent, so the measured elaboration cost is the `vcgen` decomposition and `grind` search itself.

Verified compiling on nightly-2026-07-07; not yet re-verified against current master, as `vcgen`/`finish` still changes frequently and the proofs may need minor re-tuning.

Author: sgraf812