Charged runtime layout and tag setup for one Chan–He node

Main definitions

• NodePacking.Prepared: exact computed layout, encoded tags and fixed constants.

Main results

• NodePacking.exec_layout: all address calculations are native instructions.

References

These native setup proofs are original.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Parameters (x y : WordRAM.Data 64) : Prop

The immutable caller arguments survive every phase of the node program.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Frame (x y : WordRAM.Data 64) : Prop

Runtime arguments, computed bases, encoded tags and constants retained by every round. Register 61 is the sole setup scratch register in this range.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Prepared (L : Layout) (y : WordRAM.Data 64) : Prop

The computed runtime layout and encoded tag constants.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Prepared.of_frame {L : Layout} {x y : WordRAM.Data 64} (hx : Prepared L x) (hr : Frame x y) : Prepared L y

A caller frame transports the prepared address/tag interface.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.Parameters.of_frame {x y z : WordRAM.Data 64} (hy : Parameters x y) (hr : Frame y z) : Parameters x z

A caller frame transports the immutable input/size interface.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.PaddingReady (L : Layout) (y : WordRAM.Data 64) : Prop

Exact native arguments for writing the four-column padding pattern.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec_layout {w : ℕ} (x : WordRAM.Data 64) (hfit : WordRAM.Fits w (layout x).budget) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w layoutCode x y 12 ∧ Parameters x y ∧ y.mem = x.mem ∧ y.regs packed = (layout x).packed ∧ y.regs scratch = (layout x).scratch ∧ y.regs histogram = (layout x).hist ∧ y.regs one = 1 ∧ y.regs four = 4 ∧ y.regs temporary = 3

Compute the disjoint addresses from the supplied runtime lengths and fresh base.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec_constants {w : ℕ} (L : Layout) (x : WordRAM.Data 64) (hfit : WordRAM.Fits w L.budget) (hU : x.regs magnitude = L.U) (hN : x.regs groups = L.N) (hk : x.regs scratch = L.scratch) (hh : x.regs histogram = L.hist) (hp : x.regs packed = L.packed) (h1 : x.regs one = 1) (h4 : x.regs four = 4) (h3 : x.regs temporary = 3) : ∃ (y : WordRAM.Data 64), WordRAM.ExecWithin w constantsCode x y 16 ∧ Parameters x y ∧ y.mem = x.mem ∧ Prepared L y ∧ PaddingReady L y

Compute encoded tags and signed padding through native arithmetic in sixteen instructions. The single envelope supplies every intermediate fit, including the third-column subtraction.