test: use plain shareCommon before kernel check in vcgen benchmarks (#14304)

This PR restores the `vcgen` benchmarks that regressed with `maximum
recursion depth has been reached` at larger sizes.

The benchmark driver applied `Sym.shareCommon` to the whole proof term
before kernel checking in order to restore structural sharing.
`Sym.shareCommon` now enforces the `SymM` representation invariants and
repairs kernel projections via `Meta.transform`, which recurses under
`maxRecDepth`; on the O(n)-deep `State`/`Reader` proof terms this
overflows the limit. The driver now calls
`Lean.ShareCommon.shareCommon`, the primitive backing
`shareCommonPreDefs`, which is the step the driver was emulating.

Author: sgraf812

tests/bench/vcgen/lib/Driver.lean

@@ -41,9 +41,9 @@ def driver (goal : Name) (unfold : List Name) (n : Nat) (discharge : MetaM (TSyn
         let ([], _) ← Lean.Elab.runTactic mvarId discharge.raw {} {}
           | throwError "{dischargePp} failed to solve {mvarId}"
   let (expr, instMs) ← timeItMs (instantiateMVars mvar)
-  -- Emulate the shareCommonPreDefs step before sending the term to the kernel.
-  -- If we don't do this, kernel checking time balloons.
-  let expr ← SymM.run (shareCommon expr)
+  -- Apply the `shareCommonPreDefs` structural sharing before sending the term to the
+  -- kernel. If we don't do this, kernel checking time balloons.
+  let expr := Lean.ShareCommon.shareCommon expr
   let (_, kernelMs) ← timeItMs (checkWithKernel expr)
   let label := s!"{goal.getPrefix}({n}):"
   let pad := "".pushn ' ' (24 - min label.length 24)