feat!: infer ownership transfer for attaching helpers - #33
Merged
Merged
Conversation
Adds the accepted design for inferring reusable memory contracts over stateful, recursive C workflows, and the validation record covering its 103 implementation candidates. The record is kept deliberately complete, including the candidates that failed, the three false proofs found and corrected, and the first re-measurement of the corpus completion and cost gates. That measurement is a release blocker for the implementation and is documented as such: checked contract mode regressed far past the mandatory 1.10x cost gate, driven by a 6.6x growth in checked input-case requests, and one corpus project now exceeds its 600-second deadline. The design stays Accepted rather than Implemented, as its own acceptance section requires while those gates are unmet.
Implements the accepted recursive-workflow design: semantic discovery of buffer and cursor roles, relational inputs and outputs projected through helpers, recursive contract groups checked as a unit, synchronous callback requirements as caller obligations, and the byte-level reasoning the parser workflows need. The headline new capability is the attaching-helper transfer. A complete attach now publishes the disjoint union of both owned inputs and the payload it allocated itself, forwards that guarantee through a direct return, and installs it on an immediate test of the call's result. This verifies the unchanged upstream object and array attach lifecycles. Also corrects four general defects found while validating it: a recognized minimum losing its relation to its operands, a directly returned fresh result settling no allocation, a complete release helper not settling a represented allocation head, and an automatic-storage write retiring a forest built entirely from this invocation's allocations. The third of these had silently broken a mandatory upstream client for roughly twenty candidates. Portable records move to summary format 26, sidecar format 27 and checked encoding 12, with no compatibility readers. Existing objects must be rebuilt and existing analysis caches discarded. Not ready to merge: checked contract mode fails the mandatory cost gate. See docs/validation-rfc0029.md for the measurements and the diagnosis.
owenthcarey
force-pushed
the
feat/ownership-transfer-attaching-helpers
branch
from
September 17, 2026 22:19
d8e2c49 to
9be55b9
Compare
Profiles the checked-mode regression against a checker rebuilt from bbf14c3. On one linenoise unit, user CPU goes from 3.47 s to 74.35 s. That 21x is 2.9x more function analyses times 7.3x cost per analysis, and the per-analysis factor dominates. Also records the invalidation churn found along the way (465 distinct contexts analyzed 1,429 times, because one @callback-globals change retires every dependent specialization) and a reverted scheduling experiment that moved analyses between passes without reducing time. The conclusion is that the mandatory 1.10x gate cannot be reached by optimization; meeting it as written would require cutting scope. The three available courses are recorded for the owner to choose, since this RFC forbids silently reducing a resource bound.
Every integer range query that lacks a direct bound called equalsOf, which linearly scanned all tracked relations and returned a freshly allocated vector. Profiling the corpus put that query, integerRangeAt and the allocator at the top of the profile. Replaces it with a visitor that allocates nothing and skips the keys that cannot name the queried place, since keys are canonical ordered pairs. One linenoise unit falls from 74.35s to 60.76s of user CPU. This is an internal index refinement, visiting exactly the same edges. Behaviour is unchanged: 811 Analysis, 561 Core and 86 Frontend unit tests, 205 lit tests, the 44/44 and 32/32 fixed evaluation, and twenty-six frozen populations all report their existing outcomes. Also corrects the validation record. It previously claimed checked mode failed a mandatory 1.10x cost gate; that bound applies to ordinary Release runs, which are unaffected. Checked projects carry a 600-second deadline instead, which four of five meet. lua exceeds it, and that is now the single demonstrated cost violation.
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.
Implements the accepted design for inferring reusable memory contracts over stateful, recursive C workflows, and records its validation. Intended to be squash-merged as one commit.
RFC 0029 stays Accepted, not Implemented, as with RFCs 0007–0013 and 0018. The open items below are recorded in
docs/validation-rfc0029.md(candidate 105) and are not waived.Open acceptance items
lua exceeds its 600-second checked deadline. Checked whole-program mode, user CPU, against the RFC 0028 baseline:
lua had 1.2% headroom before this milestone. The deadline is unchanged and still gates the flip to Implemented. The weekly corpus job runs ordinary analysis only, so it is not affected.
The ordinary 1.10x time/RSS gate is unmeasured. Three runs on this machine spread from 149 to 197 seconds, too noisy to resolve 10%. It needs an isolated machine.
Four upstream cJSON workflows (parse-delete, malformed-delete, nested-serialize, nested-print) still end
checking-incomplete.The unregistered
mixed-helper-framesprobe has never passed: its two positive cases endchecking-incompleteon every candidate since it was frozen, while its three negatives are correctly rejected. That makes it a precision gap, not a soundness one.The recommended next milestone is checked per-analysis cost, tracked by
checked_case_requestsand user CPU on every candidate.What is verified
attached-payload-transferpopulation through both source and ordinary objects.Breaking
Summary format 26, sidecar format 27, checked encoding 12, with no compatibility readers. Existing objects must be rebuilt and existing analysis caches discarded.
Suggested review order
docs/rfcs/0029-compositional-recursive-workflows.mdfor the proof rules.docs/validation-rfc0029.md, particularly the last two sections.lib/Corefor the portable records, thenlib/Analysis.test/evaluation/rfc0029/.