feat: redesign mvcgen' for a new meta theory

[volodeyka]

This PR rewrites the experimental mvcgen' tactic on top of a new meta theory from #12965.

Except new meta theory, the main technical difference from the current mvcgen' is that it, when solving pre ⊑ wp x post epost eagerly introduces all the state components. In other words, if for a monad m we are working with, the shape of the corresponding assertion language Pred is σ₁ → σ₂ → ⋯ → σₙ → l, then we will immediately introduce s₁ : σ₁, s₂ : σ₂, … , sₙ : σₙ yielding pre s₁ s₂ ⋯ sₙ ⊑ wp x post epost s₁ s₂ ⋯ sₙ. Most of the time, since we work with Pred type of σ₁ → σ₂ → ⋯ → σₙ → Prop shape, pre s₁ s₂ ⋯ sₙ would be of type Prop and we can introduce it into a local context. This prevents us from information loss and potentially enables more grind internalization (since more facts are introduced to a local context).

We also change how we specify the invariants for all kinds of loops, iterators, folds, maps and so on…
Before, if you had a loop throwing an exception inside, say,

def throwing_loop : ExceptT Nat (StateT Nat Id) Nat := do
  let mut x := 0
  let s ← get
  for i in [1:s] do { x := x + i; if x > 4 then throw 42 }
  set 1
  return x

when you call mvgen' you should have specified the invariant together with a condition on exception:

theorem throwing_loop_spec :
  ⦃fun s => ⌜s = 4⌝⦄
  throwing_loop
  ⦃post⟨fun _ _ => ⌜False⌝,
        fun e s => ⌜e = 42 ∧ s = 4⌝⟩⦄ := by
  mvcgen' [throwing_loop]
  case inv1 => exact post⟨fun (xs, r) s => ⌜r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⌝, -- actual invarinat
                         fun e s => ⌜e = 42 ∧ s = 4⌝⟩  -- condition on exception

Now The condition on exception would be just assumed to be the one specified in the Triple globally:

theorem throwing_loop_spec :
  ⦃fun s => s = 4⦄
  throwing_loop
  ⦃fun _ _ => False;
  fun e s => e = 42 ∧ s = 4⦄ := by
  mvcgen' [throwing_loop]
  case inv1 => exact ⟨fun (xs, r) s => r ≤ 4 ∧ s = 4 ∧ r + xs.suffix.sum > 4⟩ -- only the invariant

This should make the invariant specification more straightforward.

Internally, the Internal/VCGen rule-construction layer is split into a RuleConstruct/ submodule by rule kind (Logic, Match, Simp, Spec), a new EPost module is added for exception-postcondition handling, and shared Types/Utils modules are introduced; the previous flat Context, Entails, Reduce, RuleConstruction, and Util modules are removed. The assumption discharger is threaded from the frontend config through the driver into the solver.

On the library side it reorganizes the Std.Internal.Do order/assertion metatheory into an Order/ namespace (Basic, Frame, Lemmas), renaming Std/Internal/Do/Frame.lean to Std/Internal/Do/Order/Frame.lean, and updates the Std.Internal.Do.Triple/WP specs that build on it.

This is the second of two steps that land vova/new-mvcgen onto master. The first step (#13954) updated the @[spec] builtin attribute and regenerated stage0, so this PR reuses master's stage0 and contains no generated C changes.

[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 6b63f7d1b6974968df366dd8746f6f8ce9b7f956 --onto 8391b966bc6078e6357d0916745f4ff226de1f61. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-09 06:23:43)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 659e8bb858995b0a1ada239c5b3819c8f8f2772f --onto a806b5c9771998bcd75a5920da160b6d14a39346. You can force Mathlib CI using the force-mathlib-ci label. (2026-06-09 15:09:51)

[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 6b63f7d1b6974968df366dd8746f6f8ce9b7f956 --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-09 06:23:45)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 659e8bb858995b0a1ada239c5b3819c8f8f2772f --onto 803553a556fd82fa1060efb0c43eda542130cb16. You can force reference manual CI using the force-manual-ci label. (2026-06-09 15:09:53)