Deriving every native visit fit from the worklist envelope

The fixed arena envelope covers the current heap, every live source block and every candidate product. This discharges the actual selector and node calls uniformly, without asking the loop invariant to carry per-call execution advice or a separate width for each selected modulus.

Main results

• emit_admitted: exact native emission from a loaded admissible entry and the common envelope.

These resource and composition proofs are original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.emit_admitted {a : Arena} {w : ℕ} (x : WordRAM.Data 128) (e : Entry) (ha : a.Separated) (hw : a.Ready w) (hc : a.Controls x) (hl : e.Loaded x) (hv : e.Valid a.n a.U) (hs : e.Stored x.mem) (hbitmap : a.Bitmap x.mem) (hfloor : a.floor ≤ x.regs heap) (hheap : x.regs heap ≤ a.ceiling) (hsrc : ∀ (j : Fin 3), e.source j + (e.data j).length ≤ x.regs heap) (htable : x.regs outputs + x.regs outputCount < x.regs heap) : ∃ (y : WordRAM.Data 128), WordRAM.ExecWithin (w + 2) visit x y (visitTime a.n a.m a.N) ∧ Nonempty (Emission a.m.primesLE a.Λ e x y)

The worklist's one signed envelope derives every local native kernel fit.