Skip to content

refactor: replace the bespoke exception postcondition types with tuples - #14836

Merged
sgraf812 merged 12 commits into
masterfrom
sg/epost-to-prod
Aug 20, 2026
Merged

refactor: replace the bespoke exception postcondition types with tuples#14836
sgraf812 merged 12 commits into
masterfrom
sg/epost-to-prod

Conversation

@sgraf812

@sgraf812 sgraf812 commented Aug 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Contributor

This PR replaces the exception postcondition types EPost.Nil and EPost.Cons with products. An exception postcondition stack is now (ε₁ → Pred) × (ε₂ → Pred) × EStack⟨⟩, so the Prod API applies to it. The base monads carry bare postconditions: Except ε uses ε → Prop, and Option uses Unit → Prop. The notation EStack⟨A, B⟩ writes a stack type, and estack⟨e₁, e₂⟩ writes a stack value. Both print back as written. vcgen splits ⊥ and ⊤ exception postconditions with the same cached backward rules as the other lattice connectives.

@sgraf812 sgraf812 added the changelog-library Library label Aug 19, 2026
@github-actions github-actions Bot added the toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN label Aug 19, 2026
@mathlib-lean-pr-testing

mathlib-lean-pr-testing Bot commented Aug 19, 2026 •
edited
Loading

Copy link
Copy Markdown

Mathlib CI status (docs):

  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 16e77c407779fde9a649adf3478204d1915371a3 --onto dec70ee4980b571229f784a33d72b421ede3b1d5. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-19 08:58:12)
  • ❗ Mathlib CI can not be attempted yet, as the nightly-testing-2026-08-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-mathlib, Mathlib CI should run now. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-19 10:47:26)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 01fe11016b49e852a896f62b1590f1a763c7b145 --onto dec70ee4980b571229f784a33d72b421ede3b1d5. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-19 21:23:55)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 01fe11016b49e852a896f62b1590f1a763c7b145 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 13:39:20)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 4cf8a3b5e4b824de413a9a76eb7c33bd9e3f43c3 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 15:50:24)
  • ❗ Batteries/Mathlib CI will not be attempted unless your PR branches off the nightly-with-mathlib branch. Try git rebase 9cc41cbe25ed3b74c160f09b6dca5bc09be3ce34 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force Mathlib CI using the force-mathlib-ci label. (2026-08-20 18:18:44)

@leanprover-bot

leanprover-bot commented Aug 19, 2026 •
edited
Loading

Copy link
Copy Markdown
Collaborator

Reference manual CI status:

  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 16e77c407779fde9a649adf3478204d1915371a3 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-19 08:58:13)
  • ❗ Reference manual CI can not be attempted yet, as the nightly-testing-2026-08-19 tag does not exist there yet. We will retry when you push more commits. If you rebase your branch onto nightly-with-manual, reference manual CI should run now. You can force reference manual CI using the force-manual-ci label. (2026-08-19 10:47:28)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 01fe11016b49e852a896f62b1590f1a763c7b145 --onto 3fc29d37a70f8fd904ebab848557c12383543008. You can force reference manual CI using the force-manual-ci label. (2026-08-19 21:23:57)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 01fe11016b49e852a896f62b1590f1a763c7b145 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-20 13:39:22)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 4cf8a3b5e4b824de413a9a76eb7c33bd9e3f43c3 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-20 15:50:26)
  • ❗ Reference manual CI will not be attempted unless your PR branches off the nightly-with-manual branch. Try git rebase 9cc41cbe25ed3b74c160f09b6dca5bc09be3ce34 --onto 16e77c407779fde9a649adf3478204d1915371a3. You can force reference manual CI using the force-manual-ci label. (2026-08-20 18:18:46)

@sgraf812
sgraf812 force-pushed the sg/epost-to-prod branch 3 times, most recently from 1916ec4 to 8269c29 Compare August 19, 2026 16:26
@sgraf812
refactor: replace the bespoke exception postcondition types with tuples
0c5885b 
This PR replaces the `EPost.Nil`/`EPost.Cons` exception postcondition types of `Std.WP` with `Unit` and `Prod`, and gives each base monad the exception postcondition it throws: `Except ε` carries `ε → Prop`, `Option` carries `Unit → Prop`, `Id` carries `Unit`, and a transformer stacks a product layer on the postcondition of the monad below it. The `EPost⟨…⟩` and `epost⟨…⟩` notations become `EStack⟨…⟩` and `estack⟨…⟩` over the tuple types, so `EStack⟨ε → Pred⟩` is `(ε → Pred) × EStackEnd` and `estack⟨E⟩` is `(E, ())`, where `EStackEnd` is a reducible abbreviation of `Unit` that closes a stack.

`Prod` and `Unit` gain the `PartialOrder`, `CCPO` and `CompleteLattice` instances that `EPost.Cons` and `EPost.Nil` carried, transported from the `PProd` instances, together with the componentwise meet, supremum and bottom lemmas and the `PreservesSup (meet p)` instance a product lattice needs for its Heyting arrow. `pushExcept` and `pushOption`, which give a postcondition to the `Except` or `Option` value a transformer exposes when it runs, join `pushArg` in `Std.Internal.Order.PredTrans`. `vcgen` reads a component as `Prod.fst`/`Prod.snd` and closes the terminator with `Unit.unit_le`, matching it under reduction so that any name for `Unit` fires. A `CCPO` on a product is reachable both directly and through `instCCPOOfCompleteLattice`, and the two are defeq because the whole order hierarchy adds only `Prop` fields to `rel`. `vcgen` reduces a `⊥` exception postcondition through either, and `Prod.fst_bot` and `bot_apply` are stated at `CCPO` so they apply to both. A stack type prints back as `EStack⟨…⟩`, since `EStackEnd` names the terminator. A stack value prints as an ordinary tuple, since `()` carries no such name. Since a terminator is no longer appended by notation, `ExceptT ε Id` and `Except ε` are visibly distinct: their exception postconditions are `(ε → Prop) × Unit` and `ε → Prop`, isomorphic rather than equal.
@sgraf812
refactor: rewrite the ⊥ exception postcondition with Sym.simp
d4fb463 
This PR keeps `vcgen` reducing a `⊥` exception postcondition to a `pre ⊑ ⊥` verification condition, with no change in behaviour.

`replaceExceptPostFstBot?` now simplifies the entailment's right-hand side with a `Sym.simp` theorem set holding `Prod.fst_bot` and `Lean.Order.bot_apply`, and applies the resulting equation with `replaceTargetEq`. This replaces the hand-built proof term that folded the two lemmas over the excess arguments and extracted the `CCPO` instances from the `⊥` instance term. The helpers `prodCCPOComponents?` and `piCodomainCCPO?` go away with it. The `pre` method of the theorem set confines the traversal to the `Prod.fst`/`⊥` spine, so the state arguments are never visited.
@sgraf812
perf: cache the ⊥ exception postcondition rule
d45886d 
This PR speeds up `vcgen` on programs that specify the exception postcondition as `⊥`, by reducing each such verification condition with a rule built once per goal shape.

`mkExceptPostBotRule` builds the backward rule `pre ⊑ ⊥ → pre ⊑ (⊥ : eh × et).fst x₁ … xₙ`, holding `eh`, `et` and the `⊥` concrete and making the precondition and the excess arguments schematic. `Prod.fst_bot` and `Lean.Order.bot_apply` establish the equation the rule carries. `mkExceptPostBotRuleCached` keys it on the `Prod.fst eh et ⊥` prefix and the argument count, so `reduceExceptPostFst?` looks the rule up and applies it, instead of simplifying and assembling a proof term per goal.
@sgraf812
Merge remote-tracking branch 'origin/master' into sg/epost-to-prod
b1d2f49
@sgraf812

sgraf812 commented Aug 19, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Aug 19, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for b1d2f49 against 01fe110 are in. No significant results found. @sgraf812

  • 🟥 build//instructions: +1.2G (+0.01%)

Small changes (7✅, 5🟥)

  • 🟥 build/module/Init.Internal.Order.Basic//instructions: +289.4M (+5.52%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Elab.Tactic.VCGen.Entails//instructions: +315.9M (+7.04%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Elab.Tactic.VCGen.RuleCache//instructions: +527.3M (+19.79%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Internal.Order.PredTrans//instructions: +166.9M (+11.68%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Internal.Order.PreservesSup//instructions: +438.1M (+33.71%) (reduced significance based on *//lines)
  • ✅ build/module/Std.WP.Monad.Instances//instructions: -132.4M (-5.09%) (reduced significance based on *//lines)
  • ✅ vcgen/GetThrowSet/200/kernel//wall-clock: -4ms (-8.21%)
  • ✅ vcgen/GetThrowSet/500/kernel//wall-clock: -19ms (-8.77%)
  • ✅ vcgen/GetThrowSet/500/vcgen//wall-clock: -5ms (-6.77%)
  • ✅ vcgen/GetThrowSet/800/kernel//wall-clock: -45ms (-8.84%)
  • ✅ vcgen/GetThrowSet/800/vcgen//wall-clock: -11ms (-8.44%)
  • ✅ vcgen/GetThrowSetGrind/100/vcgen//wall-clock: -6ms (-6.30%)

@sgraf812
refactor: split ⊥/⊤ exception postcondition projections as lattic…
4362e5d 
…e ops

This PR makes `vcgen` reduce a projected `⊥` or `⊤` exception postcondition through the generic lattice-split pipeline, and closes the `⊤` case outright.

`LatticeOp.fst` and `LatticeOp.snd` register `Prod.fst`/`Prod.snd` as built-in lattice operators with the rewrites `Prod.fst_bot`/`Prod.fst_top`/`Prod.snd_bot`/`Prod.snd_top` and the pointwise `bot_apply`/`top_apply`; the last three product lemmas are new. `numConst := 3` holds the tuple operand concrete, since which rewrite fires depends on it. The `⊥` residual becomes the sole subgoal, the `⊤` residual closes with the `le_top` terminal. A new `LatticeOp.applies?` filter lets an operator decline a shape before rule construction; the projections decline every operand not headed by `⊥`/`⊤` (for example a schematic stack projection `E.fst s`), and `splitLatticeOp?` then falls through to the remaining dispatch. The bespoke `mkExceptPostBotRule`, its cache field and its cached wrapper are gone.
@sgraf812
doc: rewrite the EStack module comments
2414232
@sgraf812
sgraf812 marked this pull request as ready for review August 20, 2026 14:05
@sgraf812
sgraf812 requested review from TwoFX and kim-em as code owners August 20, 2026 14:05
@sgraf812

sgraf812 commented Aug 20, 2026

Copy link
Copy Markdown
Contributor Author

!bench

@leanprover-radar

leanprover-radar commented Aug 20, 2026 •
edited
Loading

Copy link
Copy Markdown

Benchmark results for 0cbce06 against 01fe110 are in. No significant results found. @sgraf812

  • ✅ build//instructions: -2.4G (-0.02%)

Small changes (11✅, 5🟥)

  • 🟥 build/module/Init.Internal.Order.Basic//instructions: +289.6M (+5.53%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Elab.Tactic.VCGen.Driver//instructions: -39.6M (-0.97%)
  • ✅ build/module/Lean.Elab.Tactic.VCGen.Entails//instructions: -189.9M (-4.23%) (reduced significance based on *//lines)
  • ✅ build/module/Lean.Elab.Tactic.VCGen.Frontend//instructions: -83.7M (-0.71%)
  • 🟥 build/module/Lean.Elab.Tactic.VCGen.LatticeOp//instructions: +104.7M (+3.93%) (reduced significance based on *//lines)
  • 🟥 build/module/Lean.Elab.Tactic.VCGen.Reduce//instructions: +50.8M (+4.18%)
  • ✅ build/module/Lean.Elab.Tactic.VCGen//instructions: -46.8M (-4.45%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Internal.Order.PredTrans//instructions: +166.0M (+11.62%) (reduced significance based on *//lines)
  • 🟥 build/module/Std.Internal.Order.PreservesSup//instructions: +503.5M (+38.74%) (reduced significance based on *//lines)
  • ✅ build/module/Std.WP.Monad.Instances//instructions: -135.0M (-5.19%) (reduced significance based on *//lines)
  • ✅ vcgen/GetThrowSet/200/kernel//wall-clock: -4ms (-8.07%)
  • ✅ vcgen/GetThrowSet/500/kernel//wall-clock: -16ms (-7.42%)
  • ✅ vcgen/GetThrowSet/500/vcgen//wall-clock: -5ms (-5.67%)
  • ✅ vcgen/GetThrowSet/800/kernel//wall-clock: -33ms (-6.53%)
  • ✅ vcgen/GetThrowSet/800/vcgen//wall-clock: -10ms (-7.38%)
  • ✅ vcgen/GetThrowSetGrind/100/vcgen//wall-clock: -6ms (-6.14%)

@sgraf812
sgraf812 enabled auto-merge August 20, 2026 14:36
@sgraf812
Merge remote-tracking branch 'origin/master' into sg/epost-to-prod
72cc4d8 
# Conflicts:
#	src/Lean/Elab/Tactic/VCGen/FrameProc.lean
@sgraf812
sgraf812 added this pull request to the merge queue Aug 20, 2026
@github-merge-queue
github-merge-queue Bot removed this pull request from the merge queue due to failed status checks Aug 20, 2026
@sgraf812
sgraf812 added this pull request to the merge queue Aug 20, 2026
Merged via the queue into master with commit ae12a79 Aug 20, 2026
19 checks passed
@sgraf812
sgraf812 deleted the sg/epost-to-prod branch August 21, 2026 07:26
sgraf812 added a commit to leanprover/reference-manual that referenced this pull request Aug 21, 2026
@sgraf812
chore: target nightly-2026-08-21 and port to exception stacks
1fe451a 
The tuple refactor (leanprover/lean4#14836) replaces the bespoke
exception postcondition types. In the vcgen documents, EPost.Nil
becomes EStack⟨⟩, EPost.Nil.mk becomes (), and the Result monad
carries a bare Error → Prop exception postcondition, so epost e
replaces epost.head e and the head-projection step leaves the
monotonicity proof. The push helpers for transformers are
PredTrans.pushExceptT and PredTrans.pushOptionT.

The EStack⟨…⟩ and estack⟨…⟩ notations get a syntax block in the
exception postcondition section.

The recorded Lake transcripts gain the new lint option --checks and
the package configuration field checks.

Verified with ./generate-html.sh on nightly-2026-08-21.
@sgraf812 sgraf812 mentioned this pull request Aug 21, 2026
Draft
sgraf812 added a commit to leanprover/reference-manual that referenced this pull request Aug 21, 2026
@sgraf812
doc: port the vcgen documents to exception stacks
1f725b7 
The tuple refactor (leanprover/lean4#14836) replaces the bespoke
exception postcondition types. EPost.Nil becomes EStack⟨⟩,
EPost.Nil.mk becomes (), and the Result monad carries a bare
Error → Prop exception postcondition, so epost e replaces
epost.head e and the head-projection step leaves the monotonicity
proof. The push helpers for transformers are PredTrans.pushExceptT
and PredTrans.pushOptionT. The EStack⟨…⟩ and estack⟨…⟩ notations get
a syntax block in the exception postcondition section.

Verified with ./generate-html.sh on nightly-2026-08-21.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Reviewers

@TwoFX TwoFX Awaiting requested review from TwoFX TwoFX is a code owner
@kim-em kim-em Awaiting requested review from kim-em kim-em is a code owner

Assignees

No one assigned

Labels

changelog-library Library toolchain-available A toolchain is available for this PR, at leanprover/lean4-pr-releases:pr-release-NNNN

Projects

None yet

Milestone

No milestone

Development

Successfully merging this pull request may close these issues.

3 participants

@sgraf812 @leanprover-bot @leanprover-radar