wip itree semantics control flow - #75
Draft
alexkeizer wants to merge 84 commits into
Draft
Conversation
alexkeizer
commented
Jul 10, 2026
alexkeizer
commented
Collaborator
- refactor: replace Effect with a typeclass
- feat: Reduce notation class
- refactor: drop dependently typed CFG in favour of plain BlockIds
- feat: block arguments
- feat: implement ITree.interpM
- rename Is{Node,Leaf} and move to separate file
- Itree: strong bisim
- ITree.Bisim: simplify definition, golf proof, add scoped notation
- interp_congr proof 🎉
- refactor: migrate local ITree modules to use ITreeExtras
- feat: hasEffect_iter proof
- refactor: move iter' and hasEffect_iter' proof into ITreeExtras module
- claude: include instruction to use nix
- feat: hasEffect_bind_of helper lemmas
- feat: bind_raise{UB, Error} simp-lemmas
- refactor: Effect-set aliasses
- feat: hasEffect_bind
- refactor: make effect lifting more explicit
- chore: Subeffect.map normalization
- chore: MultiContext.denote simp lemmas
- chore: Subeffect.map_fst_eq_self
- feat: mayReturn_bind
- feat: hasEffect_trigger
- feat: hasEffect/mayReturn_forM
- chore: hasEffect / mayReturn_lift lemma statements
- chore: generalize mayReturn_forM
- chore: Subeffect.map_{inl,inr} lemmas
- chore: hasEffect_pushVar lemma statement
- chore: hasEffect_seqRight corollary of hasEffect_bind
- refactor: more Subeffect.map normalization simp-lemmas
- feat: finish interpHoles_program proof
- post-rebase fixups
- post-rebase fixup: Stub
- multi-context fix
- CFG: drop annotations
This PR refactors the Effect structure into a(n empty) typeclass, where the old Effect.I and Effect.O fields are now represented as *parameters* the typeclass (with Effect.O in particular being an outParam). By doing so, we avoid the headaches that come from, e.g, `Sum` being def-eq to `SumE.I`, yet, certain definitions and rewrites expecting one or the other. By moving to the typeclass, there's no longer any need for a seperate `SumE` definition. The effect is just defined by the actual type, Sum, and the "`O`" output is found via the typeclass instance `Effect (Sum _ _) ...`. While refactoring, we also take the opportunity to use greek letters for (effect) type variables, over latin capital `E`, to bring the library closer to idiomatic Lean style.
Some sorries left, which look like they should be easy to prove with the right simp-lemmas on ITree.lift
This PR pull `LocalStack` out into its own file, and refactors its definition to be a quotient of a hashmap over `HashMap.Equiv`. We do this, so that we get that two local stacks that assign the same values (or lack thereof) to each variable are considered strictly equal. WIthout this property, refinement is not a proper partial order.
…dd lemmas about mapEff abbreviation
alexkeizer
force-pushed
the
wip-itree-semantics-control-flow
branch
from
July 17, 2026 10:47
d822e82 to
a993c07
Compare
This PR collects various definitions about holes that were spread throughout the project, and moves them to a newly dedicated Hole.lean file
alexkeizer
force-pushed
the
wip-itree-semantics-control-flow
branch
from
July 24, 2026 16:28
851d075 to
554627b
Compare
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.