Live arrays around the native traversal stack

The word stack occupies a reserved gap between the original arrays and the fresh heap. Pending arrays lie entirely below the gap or start above it. Actual stack writes therefore preserve their signed readback. Popping a serialized entry restores its seven registers and retains every pending array.

Main definitions

• Entry.Around: an array ends below the stack or starts above its reserved end.

Main results

• Entry.Stored.of_stack_frame: stack writes preserve live arrays.
• pop_entry: the actual seven-pop program restores the semantic entry.

These memory-layout and composition proofs are original.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Around (e : Entry) (base capacity : ℕ) : Prop

Every column lies entirely on one side of the reserved stack interval.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Around.mono_capacity {e : Entry} {base small large : ℕ} (h : e.Around base large) (hle : small ≤ large) : e.Around base small

Avoiding a larger reserved gap also avoids each smaller gap with the same base.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Stored.of_stack_frame {e : Entry} {before after : ℕ → ℕ} {base capacity : ℕ} (h : e.Stored before) (hg : e.Around base capacity) (hf : WordRAM.Modifies (WordRAM.Stack.footprint base capacity) before after) : e.Stored after

A concrete stack frame cannot alter any live column around its reserved interval.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.Entry.Around.child {e : Entry} {base capacity p : ℕ} (h : e.Around base capacity) (j : Fin 3) (zs : List ℤ) (hp : base + capacity ≤ p) : (e.child j p zs).Around base capacity

A newly allocated heavy block remains above the stack; untouched columns retain their gap.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.pop_entry {w base capacity : ℕ} (x : WordRAM.Data 128) (e : Entry) (es : List Entry) (h2 : WordRAM.Fits w 2) (hcap : WordRAM.Fits w (base + capacity)) (hr : WordRAM.Stack.Rep w base capacity (List.flatMap Entry.words (e :: es)) (WordRAM.Data.comap registers x)) : ∃ (y : WordRAM.Data 128), WordRAM.Exec w popFrame x y 99 ∧ WordRAM.Stack.Rep w base capacity (List.flatMap Entry.words es) (WordRAM.Data.comap registers y) ∧ e.Loaded y ∧ WordRAM.Modifies (WordRAM.Stack.footprint base capacity) x.mem y.mem ∧ ∀ (j : Fin 128), Outside j → ↑j < 64 ∨ 71 ≤ ↑j → y.regs j = x.regs j

Actual native popping restores the semantic entry, preserves the remaining stack and changes memory only inside the reserved stack interval.