Complete native initialization of a Chan–He node

Main results

• NodePacking.exec_initialize: exact runtime layout, encoded constants and all 4N padding writes, charged within 12N+33 native instructions.

References

This native composition proof is original.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec_initialize {w : ℕ} (x : WordRAM.Data 64) (hfit : WordRAM.Fits w (layout x).budget) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w initializeCode x y (12 * (layout x).N + 33) ∧ Parameters x y ∧ Prepared (layout x) y ∧ y.mem = paddingMemory (layout x) x.mem

All setup and padding are real instructions, starting from arbitrary old output memory.