Future development: add an angelic Std.WP bridge after Lean 4.35

[quangvdao]

Status: future development, blocked on the public Lean 4.35 Std.WP release

This issue is a handoff specification for future work. Do not implement or merge the bridge against PolyFun's current Lean 4.33.1 toolchain, and do not depend on Std.Internal.Do. Resume when all of the following are true:

• Lean 4.35 has a stable release containing the public Std.WP API.
• Compatible mathlib and cslib release tags are available.
• PolyFun can migrate its existing demonic WP bridge to the public API without changing its semantics.

No cslib source change is proposed or required.

Anchored at PolyFun main commit 3937f7ff0830cca33d6b35a24aef55bcbe3b6bc9 after #175.

Goal

Expose PolyFun's existing angelic support semantics as a public Lean weakest-precondition construction suitable for vcgen:

angelicWP x post := MonadAttach.SomeOutput post x
                 := ∃ a, MonadAttach.CanReturn x a ∧ post a

This means some possible execution/output satisfies post. It is appropriate for reachability, search, synthesis, witness-producing nondeterminism, or a scheduler whose choices may be resolved favorably. It is not an all-executions safety claim.

Why this is deferred

PolyFun currently uses Lean 4.33.1 and quarantines its sole public Std.Tactic.Do import in PolyFun/Control/Do/Basic.lean. At that version, Std.Do.PredTrans requires conjunctivity:

wp x (P ∧ Q) ↔ wp x P ∧ wp x Q

Angelic support is not conjunctive. Let x : SetM Nat have support {0, 1}, with P := (· = 0) and Q := (· = 1). Both SomeOutput P x and SomeOutput Q x hold, but SomeOutput (fun a ⇒ P a ∧ Q a) x does not. This is a mathematical obstruction, not a missing proof.

Lean master has resolved the abstraction problem:

• Std.WP.WP requires monotonicity only.
• WPConjunctive is optional.
• WPMonad uses lax pure/bind laws, which PolyFun's exact SomeOutput equations satisfy.
• The promotion from Std.Internal.Do to public Std.WP landed in Lean PR #14783.

As checked on 2026-08-28, Lean 4.33.1 is stable, Lean 4.34.0-rc2 still has the new framework under Std.Internal.Do, and master is 4.35-pre. The public API therefore arrives no earlier than Lean 4.35. The reference-manual migration is also still in progress.

Existing groundwork

#175 added the semantic layer required by this bridge. Relevant definitions and theorems are in:

• PolyFun/Control/Monad/Support.lean
  • MonadAttach.SomeOutput
  • someOutput_mono
  • someOutput_pure
  • someOutput_bind
  • mAlgOrderedPropAngelic
  • wp_angelic_iff_someOutput
• PolyFun/Control/Monad/Algebra/Relational/Support.lean
  • exact-support angelic relational algebra
  • strict-bind and anchored witnesses
• PolyFun/Control/Do/Basic.lean
  • the quarantined current Std.Do bridge
  • a prose explanation of the 4.35 transition and the conjunctivity obstruction

The eventual Std.WP adapter should therefore be thin. Do not duplicate the support or monad-law theory.

Required semantic boundaries

The angelic construction must deliberately not provide either of these:

1. WPConjunctive. The {0,1} example above refutes it.
2. Std.WP.LawfulWPMonadAttach. That class has demonic/universal soundness: from CanReturn x a and a WP proof it concludes the postcondition for that particular reachable a. SomeOutput post x supplies only one favorable witness, not every reachable output.

Consequently, rules requiring conjunctivity—currently including Triple.and, Triple.mp, and Triple.observe—must not be advertised for angelic WP. Basic vcgen support needs to be tested explicitly rather than assumed.

Also document these interpretation limits:

• Empty support makes angelic WP false; demonic WP is vacuously true there.
• Existential support is not a probability bound and must not be presented as a cryptographic security claim.
• Under scheduler nondeterminism, angelic WP means that some favorable schedule exists. It says nothing about a fixed, fair, random, or adversarial scheduler without an additional bridge.

Recommended implementation stack

PR A: migrate the existing bridge to public Std.WP

Keep this PR semantically neutral:

• Bump Lean, mathlib, and cslib pins to compatible stable releases. Do not modify cslib itself.
• Replace the quarantined Std.Tactic.Do / Std.Do dependency with public Std.WP and vcgen.
• Port the existing demonic construction and soundness/elimination theorems.
• Prefer truth-in-advertising names such as toDemonicWP and toDemonicWPMonad; deprecate old ambiguous names if downstream compatibility warrants it.
• Port MonadHom.transportWP and transportWPMonad if the public API still supports the same abstraction cleanly.
• Preserve the current rule that these are named constructions, not global instances.
• Update quarantine documentation and committed demonic vcgen tests.
• Make no angelic-semantic change in this PR.

PR B: add the angelic adapter

The API below is schematic and must be reconciled with the released 4.35 names:

namespace MonadAttach

@[instance_reducible]
def toAngelicWP (m : Type u → Type v) [MonadAttach m] (α : Type u) :
    Std.WP.WP (m α) α Prop Std.WP.EStack⟨⟩ where
  wpTrans x := ⟨fun post _ ⇒ SomeOutput post x⟩
  wp_trans_monotone := by
    -- use `someOutput_mono`

@[instance_reducible]
def toAngelicWPMonad (m : Type u → Type v)
    [Monad m] [LawfulMonad m] [MonadAttach m] [ExactMonadAttach m] :
    Std.WP.WPMonad m Prop Std.WP.EStack⟨⟩ where
  toLawfulMonad := inferInstance
  toWP := toAngelicWP m
  pure_le_wp_pure := by
    -- use `someOutput_pure`
  bind_le_wp_bind := by
    -- use `someOutput_bind`

theorem angelic_wp_iff_someOutput ... :
    Std.WP.wp x post ↔ SomeOutput post x := ...

end MonadAttach

Design constraints:

• Construct the adapter directly from SomeOutput so m : Type u → Type v remains universe-polymorphic. The current MAlgOrdered Prop carrier uses a narrower Type → Type v domain and should not become an accidental restriction.
• Provide a named construction and/or tightly scoped registration. Do not add a competing global WP instance.
• Keep the characterization theorem transparent and easy for downstream proofs to rewrite with.
• Add PFunctor.FreeM.AngelicWP only if a real vcgen consumer or worked example needs it; do not add a wrapper solely for symmetry with the demonic bridge.

Acceptance tests

The tests should be small and semantic, not a broad duplication of the support suite.

Positive tests

• wp x post ↔ SomeOutput post x.
• Pure: angelicWP (pure a) post ↔ post a.
• Bind with a branch-dependent witness, exercising both stages of the existential choice.
• Empty support yields False.
• A nontrivial SetM or FreeM vcgen example proves existential reachability without requiring conjunctivity.
• The existing demonic vcgen examples still work after the migration.

Negative/canary tests

Use a computation with support {0,1} to pin both failures:

• Non-conjunctivity: angelicWP x P ∧ angelicWP x Q does not imply angelicWP x (P ∧ Q) for P := (· = 0) and Q := (· = 1).
• Non-universal soundness: angelicWP x (· = 0) and CanReturn x 1 coexist, so the WP proof cannot establish the postcondition for every reachable output.

These canaries should prove the counterexamples as ordinary theorems; they need not try to prove meta-level absence of a typeclass instance.

Resume checklist for a future agent

1. Confirm lean-toolchain, mathlib, and cslib all have compatible stable 4.35-or-later tags.
2. Inspect the released forms of:
   • Std.WP.WP
   • Std.WP.WPMonad
   • Std.WP.WPConjunctive
   • Std.WP.LawfulWPMonadAttach
   • vcgen
3. Re-check whether Triple.and, Triple.mp, Triple.observe, direct spec application, and framing still require conjunctivity.
4. Use separate worktrees/branches for the toolchain migration and angelic adapter PRs.
5. Land or stabilize PR A before stacking PR B.
6. Run at least lake build, lake test, and lake lint; also run the repository's axiom sweep and CI-equivalent checks.
7. Validate one downstream VCVio existential/reachability consumer before adding FreeM-specific convenience API.
8. In the PR description, state plainly that this is may/existential semantics, not all-runs safety or probabilistic security.

Non-goals

• No compatibility layer over Std.Internal.Do.
• No cslib source changes.
• No global selection between demonic and angelic WP semantics.
• No claim that angelic support implies positive or non-negligible probability.
• No scheduler fairness or adversarial-scheduler theorem without separately specified scheduler semantics.