Size-aware base-case weights + RecAwareGradedScore#53
Open
segevem wants to merge 5 commits into
Open
Conversation
added 5 commits
July 10, 2026 18:40
Non-recursive constructors now receive the actual `size'` in the size>0 branch (and literal 0 in the size=0 branch) instead of always getting 0. This lets weight modifiers scale base-case probability as a function of recursion depth. Refactors compileWeightedProducer into compileSubProducer + wrapWithWeight so the sub-producer body is compiled once and wrapped with different weight terms for each size branch. Adds `inverseScaleBase` modifier to BoundedBuffer that smoothly reduces base-case dominance as size grows: `max 1 (baseWeight / (size + 1))`. Without this, EveryBBTrace.All_Empty (badness=0 → weight 16) produced 668/1000 empty traces; with it, only ~95/1000 are empty. Adds generator quality regression tests for SafeBBTrace and EveryBBTrace.
…mode calls Instead of relying on inProgress memo state (which depends on derivation order), detect mutual recursion structurally: a NonRec dep that targets the same inductive as the current key but with different output indices or deriveSort is a cross-mode call that will become mutual recursion at codegen time. This is reliably visible during scoring regardless of derivation order.
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
RecAwareGradedScore: a scorer that distinguishes direct recursion (Source.Rec) from same-inductive cross-mode calls (Source.NonRec targeting the same inductive with different output indices or derive sort), preferring direct recursion as the simpler patternsize'to non-recursive constructor weight functions/modifiers in the size>0 branch (literal 0 in size=0), enabling modifiers that scale base-case probability with depthcompileWeightedProducerintocompileSubProducer+wrapWithWeight— compiles the sub-producer body once and wraps it with different weight terms per size branchinverseScaleBaseweight modifier to BoundedBuffer:max 1 (baseWeight / (size + 1))Context
Switching BoundedBuffer to
RecAwareGradedScoreexposed a latent issue withbalancedCtorWeight:EveryBBTrace.All_Emptyhas a trivially perfect schedule (density=Total, badness=0.0) which gets quality=4 → base weight 16. The recursiveAll_Op(badness=0.91) gets quality=1 → weight=size. At size=10: P(base)=62%, producing 668/1000 empty traces.The fix passes runtime size to weight modifiers so they can reduce base-case weight as depth increases. With
inverseScaleBase, empty traces drop to ~95/1000 and both SafeBBTrace and EveryBBTrace produce comparable trace lengths.Test plan
lake buildpasses#guard_msgsquality tests pass (>2000 ops, <20% empty, >100 successful gets per 1000 samples)backwardOnlySizeOpsstill pass