Conversation
added 2 commits
September 24, 2026 00:48
origin allowed one structural read below a column, so a self-call on a field of a field was rejected. A value is now traced to a place, the column plus the path of reads below it, and facts are about places. Each read needs its own place guarded; a fact about a place also holds above it. A tagged vector putting a place's fields back at their own indexes rebuilds that place, so it is no larger than it.
An Int return is proved an integer and a Nat return is then proved not negative, so a call of the fn is an integer term and a Nat atom for the arithmetic. An induction hypothesis that is an unconditional linear comparison is now also a fact, which the nonnegative step needs. Contract goals run callees first, and one that failed is retried only once a fn its code reaches gets a new contract. Before, a contract that could not be proved was searched again on every pass; on the fetch example that was 45s per target, now 15s. Contracts are cached in their own file keyed on writ, the code, its signatures and data, so law and proof namespace edits keep them.
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.
Closes writ-fuu and writ-vlb.
Descent: a self-call on a field of a field was rejected, because origin allowed only one structural read below a column. Values are now traced to a place (the column plus the path of reads below it), and branch facts are about places. Each read needs its own place guarded. A fact about a deeper place also guards the places above it. A tagged vector that puts a matched field's own fields back at their indexes counts as that field, so
(ev [:Cons h2 t2])descends. A rest below an element read still needs finiteness, so it is rejected.Contracts: an Int return is proved
(integer? call). A Nat return then also gets(<= 0 call), which int-term? and the linear arithmetic read. To prove the nonnegative step, an unconditional linear induction hypothesis is now assumed as a fact as well as used as a rewrite. The checker builds its contexts the same way, so it replays these proofs.Speed: a contract that could not be proved was searched again on every pass. On fetch that was next-action, 15s three times per target. Goals now run callees first, and a failure is retried only once something its code reaches gets a new contract. Contracts are also cached in their own file, keyed on writ, the code, its signatures and data, so editing a law or the proof namespace keeps them.
writ tests: 373 pass. Examples: 28 pass, cold run 23.4 min (was about 26).