Native dispatch after popping a Chan–He entry #
The zero-fuel and empty-array cases execute their actual branch paths. Live calls execute the complete visit followed by all three native child pushes. No guard is evaluated by a host program, and skipped entries retain the same charged pop as live entries.
Main results #
body_skip: actual pop and dispatch for every skipped entry.body_live: the four actual negative branches connect a pop to the complete live suffix.
These control-flow composition proofs are original.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.body_skip {w : ℕ} {x y : WordRAM.Data 128} {e : Entry} (hp : WordRAM.Exec w popFrame x y 99) (hl : e.Loaded y) (hz : y.regs zero = 0) (hskip : e.fuel = 0 ∨ (e.data 0).length = 0 ∨ (e.data 1).length = 0 ∨ (e.data 2).length = 0) :
WordRAM.ExecWithin w body x y 107
Every skipped entry executes the actual seven pops and the appropriate guard path. The resulting data is exactly the pop result; the self-copy does not change it.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.body_live {w T : ℕ} {x a b y : WordRAM.Data 128} {e : Entry} (hp : WordRAM.Exec w popFrame x a 99) (hl : e.Loaded a) (hz : a.regs zero = 0) (hf : e.fuel ≠ 0) (hn : ∀ (j : Fin 3), (e.data j).length ≠ 0) (hv : WordRAM.ExecWithin w visit a b T) (hc : WordRAM.Exec w pushChildren b y 207) :
WordRAM.ExecWithin w body x y (T + 314)
A live entry takes all four native negative branches before executing the supplied actual visit and three-push executions. The bound charges the seven pops and eight branch/jump steps.