refactor: derive vcgen's exception postcondition rules from a type class

[sgraf812]

This PR lets vcgen weaken the exception postcondition of a spec for any exception postcondition type that converts into an assertion stack, not only for the Prod/Unit stacks themselves.

AssertionHom E T hom converts an assertion E into a stack T whose factors are the assertions of the individual exception layers, reflects an entailment between the images back to an entailment between the arguments, and identifies the image of ⊥. The spec rule construction decomposes epostSpec ⊑ epost over bare Prod/Unit stacks directly; for an exception postcondition type with an AssertionHom instance it converts both sides once, decomposes the entailment between the images factor by factor, and reflects it back with AssertionHom.le_of_hom_le. A factor of the converted spec value is a projection of a literal, which the construction reduces so each verification condition states the assertion the user wrote. The instance lookup runs during rule construction, which is cached per spec theorem, WPMonad instance and excess-argument count, so no goal pays for it.

The test's Thrown structure, converting to EStack⟨String → Prop⟩, is the motivating instance: a concrete factor yields a pointwise verification condition, and a schematic factor is assigned the goal's factor instead of yielding one.

[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 0bdfa796ef6e1c94fa3c57a4fe0e5f728abb176e --onto dec70ee4980b571229f784a33d72b421ede3b1d5. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-18 15:48:03)
• ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase c129c5fda2e6da773e3fc23afbec64d6dd7efa4b --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-21 10:05:50)

[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 0bdfa796ef6e1c94fa3c57a4fe0e5f728abb176e --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-18 15:48:05)
• ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase c129c5fda2e6da773e3fc23afbec64d6dd7efa4b --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-21 10:05:51)

[sgraf812]

!bench

[leanprover-radar]

Benchmark results for 5e7ac81 against 0bdfa79 are in. No significant results found. @sgraf812

• ✅ build//instructions: -108.0M (-0.00%)

Small changes (3🟥)

• 🟥 build/module/Lean.Elab.Tactic.VCGen.RuleConstruction//instructions: +454.7M (+7.13%) (reduced significance based on *//lines)
• 🟥 build/module/Std.WP.Assertion//instructions: +98.7M (+10.00%) (reduced significance based on *//lines)
• 🟥 build/module/Std.WP.ExceptPost//instructions: +97.3M (+3.80%) (reduced significance based on *//lines)