feat(free): run vcgen over free programs on the canonical WP stack

[dtumad]

Summary

Stacked on #188. Puts the free monad on core's lattice-generic weakest-precondition stack (Std.Internal.Do, the stack vcgen consumes) and retires the legacy Std.Do bridge, so do programs over FreeM P with uninterpreted operations are verified by vcgen end to end.

• PFunctor/Free/WP/Upstream.lean — OpSpec.toWPMonad (the syntactic fold wpFold as a core WPMonad, by rfl), FreeM.wpMonadOfHandler (transport of any core WPMonad on the target along liftMHom, with wp = wp (x.liftM s) by rfl), and wpFold_le_wp_liftM: an op-spec sound for a handler bounds the handler's wp of the interpretation, against any core WPMonad on the target.
• PFunctor/Free/Do.lean rewritten — scoped DemonicWP (wp x Q = AllOutputs Q x, with LawfulWPMonadAttach and WPConjunctive instances) and AngelicWP (wp x Q = SomeOutput Q x) interpretations, and the @[spec] rules Spec.lift (every response), Spec.liftBind, Spec.lift_angelic (some response), Spec.lift_ofHandler (the handler's wp).
• PFunctor/Free/Support.lean — allOutputs_lift / someOutput_lift (@[simp]).
• Deleted — Control/Do/Basic.lean (the Std.Do / mvcgen bridge); PolyFun.lean regenerated. No mvcgen use remains.

Canaries

PolyFunTest/Do/FreeM.lean (bind chains through Spec.lift, soundness back to CanReturn / AllOutputs, the angelic reading), PolyFunTest/Do/Transport.lean (a handler-relative interpretation installed locally), and the new PolyFunTest/Do/Loops.lean: let mut over for with vcgen … invariants, if let, StateT Nat (FreeM coinP) with a state invariant through core's lifted instance, and tail-position operations.

Found on the way (recorded as gotcha 11e and a landscape follow-up)

vcgen applies @[spec] lemmas through core's Sym matcher, which compares the program and its value type structurally (only instances go through isDefEq). Spec.lift is stated at the dependent value type P.B a, so it applies under bind (where the type comes from the operation) but not to an operation in tail position once the elaborated triple carries the normalized type (Bool on an abbrev interface); registering FreeM.lift a = FreeM.liftBind a pure as an equation spec does not help because Spec.pure then meets the same mismatch. The canary shows the fallback (vcgen -errorOnMissingSpec, then rw [DemonicWP.wp_apply_eq, FreeM.allOutputs_lift (P := …)]) and the generic-interface form where vcgen closes tail position directly. Worth raising upstream.

Validation

./scripts/validate.sh --lint --test --axioms — lint passes for PolyFun and ToCslib; 11031 declarations, zero sorry/axiom taint.

🤖 Generated with Claude Code

https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc