feat(control): cover the whole do fragment in every judgment, with loop rules - #188
Draft
dtumad wants to merge 1 commit into
Draft
feat(control): cover the whole do fragment in every judgment, with loop rules#188dtumad wants to merge 1 commit into
dtumad wants to merge 1 commit into
Conversation
…loop rules Give each construct core `do`-notation elaborates to a rule in each of PolyFun's judgments, so that reasoning about ordinary monadic code never has to unfold a judgment by hand: - `Control/Monad/Support/Structural.lean`: `CanReturn`, `AllOutputs`, `SomeOutput`, and `NoOutput` through `<*`, `*>`, `if`, `if h :`, `Option.elim`, `Sum.elim`, `<$>`, and `<*>`; the `Option.elim` / `Sum.elim` reachability equations are `@[simp, grind =]`, the rest `@[simp]`, since `grind` refuses `ite` heads and thunked applicative operands as patterns; - `Control/Monad/Support/Loops.lean`: invariant rules for `forIn'` / `forIn` / `foldlM` over lists and `PureForIn` containers, obtained from core's `Spec.*` specifications under the demonic and angelic `WPMonad` instances, plus `forM` by induction — support reasoning about loops without a triple; - `Control/Monad/Algebra.lean`: `wp_seqLeft`, `wp_seqRight`, `wp_ite`, `wp_dite`, `wp_option_elim`, `wp_sum_elim` join the inward-normalizing `@[simp]` set; `Control/Monad/Hom.lean` and `Hom/Loops.lean`: a monad morphism commutes with branching and with every loop combinator; `PFunctor/Free/WP.lean`: the same for `wpFold`; - `Control/Do/Spec.lean`: `@[spec] Spec.forM_list`, the list loop core does not specify, in the tactic tier of the quarantine. `Control/Monad/Support.lean` is split under the 1500-line cap: instances and lift transport move to `Support/Instances.lean`, the per-run support of `StateT` / `ReaderT` to `Support/Indexed.lean`; no declaration changes name. Canaries: `PolyFunTest/Control/SupportStructural.lean` (one-tactic gates), `PolyFunTest/Control/MonadHomLoops.lean`, and, in `PolyFunTest/Do/Support.lean`, a `let mut` accumulator over a `for` loop verified by `vcgen` with a loop invariant through core's `Spec.forIn_list`, converted back to the "always" judgment. The program-logic page gains a coverage table; the landscape memo records the follow-ups (relational loop rules, a `mapM` judgment rule, and `try/catch` through the lifted `ExceptT` instance, where `vcgen` reports no applicable spec). Validated with `./scripts/validate.sh --lint --test --axioms` (zero sorry/axiom taint). Co-Authored-By: Claude Fable 5.1 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc
dtumad
marked this pull request as draft
September 3, 2026 18:32
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
1 participant
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Summary
Stacked on #187. Gives each construct that core
do-notation elaborates to a rule in each PolyFun judgment, so reasoning about ordinary monadic code never unfolds a judgment by hand.Control/Monad/Support/Structural.lean—CanReturn/AllOutputs/SomeOutput/NoOutputthrough<*,*>,if,if h :,Option.elim,Sum.elim,<$>,<*>. Tagging follows whatgrindcan index:Option.elim/Sum.elimreachability is@[simp, grind =];iteheads and thunked applicative operands cannot be patterns, so those stay@[simp](recorded as a gotcha).Control/Monad/Support/Loops.lean— invariant rules forforIn'/forIn/foldlMover lists andPureForIncontainers, obtained from core'sSpec.*lemmas under the demonic and angelic instances of feat(control): bridge the program-logic kernel to core's lattice-generic WP stack #187, plusforMby induction.Algebra.lean,Hom.lean,Hom/Loops.lean,PFunctor/Free/WP.lean— the same constructs forMAlgOrdered.wp,MonadHom, andwpFold; morphisms commute with every loop combinator (@[simp, grind =]).Control/Do/Spec.lean—@[spec] Spec.forM_listforvcgen(tactic tier).Support.lean→ root +Support/Instances.lean+Support/Indexed.lean, no renames.Canaries
PolyFunTest/Control/SupportStructural.lean(one-tactic gates),PolyFunTest/Control/MonadHomLoops.lean, and inPolyFunTest/Do/Support.leanalet mutaccumulator over aforloop verified byvcgen … invariants · fun pref _ s => s = pref.sumthrough core'sSpec.forIn_list, converted back toAllOutputs.Left out (recorded in the landscape memo)
Relational (
MAlgRelOrdered) loop rules, amapMjudgment rule, andtry/catchthrough the liftedExceptTinstance over a PolyFun base —vcgenreportsNo spec found for program tryCatch …there althoughSpec.tryCatch_ExceptTexists at the pin; the instance path needs diagnosing.Validation
./scripts/validate.sh --lint --test --axioms— lint passes forPolyFunandToCslib; 11030 declarations, zero sorry/axiom taint.🤖 Generated with Claude Code
https://claude.ai/code/session_01Nb4g3Vxgjhnhsca7BzAsFc