Completing the native forest reservations #
The actual power loop computes the per-root tree reservation. Three further instructions multiply by the root count and place the initial heap above the complete pointer table.
Main results #
finish_exec: execute reservation and layout completion with exact native heap/table metadata.
The native composition and memory-frame proofs are original.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.finish_exec {κ n w : ℕ} (x : WordRAM.Data 128) (hs : Saved κ n x) (hc : (arena κ n x.mem).Controls x) (hcount : x.regs Traversal.outputCount = 0) (hp : x.regs power = 1) (hr : x.regs remaining = ThreeSum.ChanHe.fuel n + 1) (hscalar : x.regs scalar = 3) (hpow : WordRAM.Fits w (3 ^ (ThreeSum.ChanHe.fuel n + 1))) (hfloor : WordRAM.Fits w (arena κ n x.mem).floor) :
∃ (y : WordRAM.Data 128),
WordRAM.ExecWithin w (reserve.seq finishLayout) x y (4 * (ThreeSum.ChanHe.fuel n + 1) + 5) ∧ Saved κ n y ∧ (arena κ n x.mem).Controls y ∧ y.regs Traversal.outputCount = 0 ∧ y.regs Traversal.heap = (arena κ n x.mem).floor ∧ y.regs outputCapacity = (arena κ n x.mem).outputCapacity ∧ y.regs heapFloor = (arena κ n x.mem).floor ∧ y.mem = x.mem
Compute all root reservations and the actual first fresh heap address by native code.