sir: a bump allocator over the memory watermark - #20
Closed
Eduardogbg wants to merge 4 commits into
Closed
Conversation
MemoryState.watermark is the high end of everything provisioned, and bumpAlloc hands out the next region above it. It satisfies IsValidNewAlloc whenever the watermark plus the request fits the address space: the region starts where every existing one has ended, so disjointness is immediate. That inequality is the first half of IsValidNewAlloc, since the end of a bump allocation is the watermark plus the size. At a watermark of 2^256 the offset wraps to zero and the bound forces a zero-size request.
…ator progress_reachable_nonIcall assumes a valid fresh allocation exists for mallocUninit. Supplying the bump allocator turns that assumption into an arithmetic side condition: the watermark plus the requested size fits the address space.
The toNat/ofNat round-trip was proved twice, once in the memory algebra and once in the byte-window layer, and both copies sat above the arithmetic they are about. It moves to Evm.UInt256 next to toNat_limbs, keeping the shorter of the two proofs; call sites across the bytecode layer, the IR lowering experiment, and the SIR bump allocator now name it there. That also lets Sir/Proofs/Bump.lean drop its import of the Hoare layer, which it only ever wanted for this one fact.
The control-point disjunction and the two allocation obligations were written out at every use: twice in Theorems.lean, once in Readiness.lean, once in Bump.lean, and the allocator work adds more. They become Program.NonIcallControl, Program.AllocationAvailable and Program.BumpFits in Spec/Step.lean, next to the step relation whose preconditions they are. They unfold definitionally, so no proof changes.
Eduardogbg
force-pushed
the
sir/bump-allocator
branch
from
August 5, 2026 13:29
984f54d to
b1cbc69
Compare
Collaborator
Author
|
superseded by #26 |
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.
Adds a bump allocator and uses it to discharge the allocation hypothesis of the progress theorem.
MemoryState.watermarkis the fold ofAllocation.endExclusiveoverprovisioned, zero when nothing is provisioned.MemoryState.bumpAllocation m sizehands out the region starting there.isValidNewAlloc_bumpAllocationproves it satisfiesIsValidNewAllocwhenwatermark + size ≤ Evm.UInt256.size. That inequality is the first half ofIsValidNewAlloc: for a bump allocation the end of the region is the watermark plus the size. Disjointness comes fromendExclusive_le_watermark, since the new region starts where every live one has ended. When the watermark sits at2^256the offset wraps to zero and the bound forces a zero-size request.progress_reachable_nonIcallassumes a valid fresh allocation exists whenever the next statement ismallocUninit.progress_reachable_nonIcall_bumpsupplies the bump allocator and leaves the caller the arithmetic condition instead. Both stay: a fragmented memory can have a valid hole where the bump allocator has none.toNat/ofNatround trip was proved twice, in the memory algebra and in the byte-window layer. It now lives once asEvm.UInt256.toNat_ofNatbesidetoNat_limbs; the bytecode layer, the IR lowering experiment and the allocator all use that one.Program.NonIcallControl,Program.AllocationAvailableandProgram.BumpFitsinSpec/Step.lean, beside the step relation whose preconditions they are. They unfold definitionally, so no proof changed.