Initializing the four columns of a Chan–He node

Main definitions

• Padding.program: a fixed loop writing a four-word pattern to every group.

Main results

• Padding.exec: exact memory and a charged 12N+5 instruction bound.

References

This native program and its execution proof are original.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.dst : Fin 10

Packed output base.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.len : Fin 10

Number of four-cell groups.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.pad0 : Fin 10

Padding word for column zero.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.pad1 : Fin 10

Padding word for column one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.pad2 : Fin 10

Padding word for column two.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.pad3 : Fin 10

Padding word for column three.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.idx : Fin 10

Group cursor.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.addr : Fin 10

Temporary address.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.one : Fin 10

Constant one.

@[reducible, inline]

abbrev Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.four : Fin 10

Constant four.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.pattern (p₀ p₁ p₂ p₃ u : ℕ) : ℕ

A concrete four-word pattern, addressed by its residue modulo four.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.memory (mem : ℕ → ℕ) (dst p₀ p₁ p₂ p₃ k : ℕ) : ℕ → ℕ

Initial memory with the first k groups overwritten, including all padding.

@[simp]

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.memory_zero (mem : ℕ → ℕ) (dst p₀ p₁ p₂ p₃ : ℕ) : memory mem dst p₀ p₁ p₂ p₃ 0 = mem

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.memory_succ (mem : ℕ → ℕ) (dst p₀ p₁ p₂ p₃ k : ℕ) : memory mem dst p₀ p₁ p₂ p₃ (k + 1) = Function.update (Function.update (Function.update (Function.update (memory mem dst p₀ p₁ p₂ p₃ k) (dst + 4 * k) p₀) (dst + 4 * k + 1) p₁) (dst + 4 * k + 2) p₂) (dst + 4 * k + 3) p₃

Four distinct stores make one complete group.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.body : WordRAM.Code WordRAM.Basis.standard 10

Every address, store and increment of a four-word group is charged.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.program : WordRAM.Code WordRAM.Basis.standard 10

Runtime pattern values and length, with fixed code and registers.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Padding.exec {w : ℕ} (x : WordRAM.Data 10) (h4 : WordRAM.Fits w 4) (hfit : WordRAM.Fits w (x.regs dst + 4 * x.regs len)) : ∃ (y : WordRAM.Data 10), WordRAM.ExecWithin w program x y (12 * x.regs len + 5) ∧ y.mem = memory x.mem (x.regs dst) (x.regs pad0) (x.regs pad1) (x.regs pad2) (x.regs pad3) (x.regs len) ∧ ∀ (i : Fin 10), ↑i < 6 → y.regs i = x.regs i

Initialize exactly 4N cells from arbitrary old memory.