Complete bounded native Chan–He worklist loop

Each body execution is discharged by the actual pop, modulus, histogram, packing and push programs. The explicit proof-state loop rule then counts every pending entry, including skipped calls. Termination returns the exact finite preorder, whose native pointer table and packed arrays have full readback. The arena bounds cover all live memory throughout the loop.

Main results

• transition: actual native body execution and invariant preservation for every pending entry.
• loop_exec: the complete actual native loop terminates with exact finite node output.

These native composition and resource proofs are original. Initialized-input preprocessing composition is a separate obligation.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.transition {a : Arena} {w : ℕ} {target : List ThreeSum.ChanHe.Node} (ha : a.Separated) (hw : a.Ready w) (h2 : WordRAM.Fits (w + 2) 2) (hcap : WordRAM.Fits (w + 2) (a.stack + a.capacity)) (s : Cursor) (x : WordRAM.Data 128) (h : Cursor.Invariant a w target s x) (hc : (WordRAM.Cond.lt zero (registers WordRAM.Stack.len)).Holds x) : ∃ (s' : Cursor) (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) body x y (visitTime a.n a.m a.N + 314) ∧ Cursor.Invariant a w target s' y ∧ s'.work < s.work

Every actual live loop header admits a native body execution with the same finite program.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.loop_exec {a : Arena} {w : ℕ} {target : List ThreeSum.ChanHe.Node} (ha : a.Separated) (hw : a.Ready w) (h2 : WordRAM.Fits (w + 2) 2) (hcap : WordRAM.Fits (w + 2) (a.stack + a.capacity)) (s : Cursor) (x : WordRAM.Data 128) (h : Cursor.Invariant a w target s x) : ∃ (ns : List (ℕ × ThreeSum.ChanHe.Node)) (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) loop x y (s.work * (visitTime a.n a.m a.N + 316) + 2) ∧ Cursor.Invariant a w target { pending := [], emitted := ns } y ∧ List.map Prod.snd ns = target

Execute the complete actual native loop. Every call and fit is discharged by transition; the final emitted list equals the entire target, with exact pointer and packed-array readback.