Complete charged native rounds of a Chan–He node

Main definitions

• NodePacking.CallArgs: exact runtime delivery to the existing complete counting/placement code.

References

These native setup and composition proofs are original.

structure Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.CallArgs (L : Layout) (s : Fin 3 → ℕ) (j : Fin 3) (x : WordRAM.Data 64) : Prop

Exact runtime parameters delivered to one complete counting/placement call.

• len : x.regs CountPlace.len = L.n j

  Actual input length.

• src : x.regs CountPlace.src = s j

  Actual signed input base.

• scratch : x.regs CountPlace.scratch = L.scratch

  Computed residue workspace.

• hist : x.regs CountPlace.hist = L.hist

  Computed histogram workspace.

• heavy : x.regs CountPlace.heavy = L.heavy j

  Computed compact heavy data base.

• packed : x.regs CountPlace.packed = L.packed

  Computed packed array base.

• modulus : x.regs CountPlace.modulus = L.M

  Actual positive modulus.

• tag : x.regs CountPlace.tag = 2 * L.tag j

  Exact encoded positive tag.

• column : x.regs CountPlace.column = ↑j + 1

  Packed column.

• distance : x.regs CountPlace.distance = if j = 2 then 4 * L.M else 0

  Duplicate-store offset.

• negative : x.regs CountPlace.negative = if j = 2 then 1 else 0

  Sign multiplier flag.

• descriptor : x.regs CountPlace.descriptor = L.descriptor j

  Computed descriptor/count cell.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.prepare_preserves (j : Fin 3) (i : Fin 64) (hi : 46 ≤ ↑i) (hne : i ≠ temporary) : WordRAM.Code.Preserves i (prepare j)

Runtime argument delivery keeps all persistent caller registers.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.round_preserves (j : Fin 3) (i : Fin 64) (hi : 46 ≤ ↑i) (hne : i ≠ temporary) : WordRAM.Code.Preserves i (round j)

Every complete native round retains the caller arguments and prepared layout/constants.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec_prepare {w : ℕ} (x y : WordRAM.Data 64) (j : Fin 3) (hparams : Parameters x y) (hready : Prepared (layout x) y) (hfit : WordRAM.Fits w (layout x).budget) (hN : 2 * (layout x).M ≤ (layout x).N) : ∃ (q : WordRAM.Data 64), WordRAM.ExecWithin w (prepare j) y q 20 ∧ CallArgs (layout x) (fun (j : Fin 3) => x.regs (source j)) j q ∧ q.mem = y.mem

All count/place arguments are computed from actual retained caller values in at most twenty instructions. In particular no output pointer or encoded tag is supplied for free.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.NodePacking.exec_round {w : ℕ} (x y : WordRAM.Data 64) (values : Fin 3 → ℕ → ℤ) (j : Fin 3) (hparams : Parameters x y) (hready : Prepared (layout x) y) (hfit : WordRAM.Fits (w + 2) (layout x).budget) (hM : 0 < (layout x).M) (hN : 2 * (layout x).M ≤ (layout x).N) (hmod : GenericRAM.Signed.Fits w ↑(layout x).M) (hsrc : x.regs (source j) + (layout x).n j ≤ (layout x).base) (hbdd : ∀ i < (layout x).n j, (values j i).natAbs ≤ (layout x).U) (hsigned : ∀ i < (layout x).n j, GenericRAM.Signed.Fits w (values j i)) (hinput : ∀ i < (layout x).n j, y.mem (x.regs (source j) + i) = WordRAM.Signed.encode (values j i)) (hinj : Set.InjOn (values j) ↑(Finset.range ((layout x).n j))) : ∃ (z : WordRAM.Data 64), WordRAM.ExecWithin (w + 2) (round j) y z (66 * (layout x).n j + 5 * (layout x).M + 65) ∧ z.mem = roundMemory (layout x) values j y.mem ∧ Frame y z ∧ Parameters x z ∧ Prepared (layout x) z

A complete native round, with all actual counting calls discharged and all pointer, tag, duplicate-store and count-descriptor work charged.