Charged initialization from the actual depth header

Main results

• Encoding.exec_setup: load the header and compute both powers, buffer addresses and loop parameters within 5L+18 native instructions, preserving every memory cell.

def Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.addressBound (L : ℕ) : ℕ

An explicit bound for the encoder's unsigned addresses, index products and counters.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.SetupPost (L : ℕ) (x y : WordRAM.Data 32) : Prop

Registers and memory after header initialization. This is only a postcondition; it contains no execution, resource or intermediate-fit assumption.

• mem : y.mem = x.mem

  Memory is unchanged.

• depth : y.regs Encoding.depth = L

  Depth loaded from memory address one.

• inputSize : y.regs Encoding.inputSize = 7 ^ L

  Computed input size.

• capacity : y.regs Encoding.capacity = 10 ^ L

  Computed buffer capacity.

• output : y.regs Encoding.output = outputBase L

  First output address.

• scratch : y.regs Encoding.scratch = scratchBase L

  First scratch address.

• src : y.regs Encoding.src = 2

  Original input base.

• dst : y.regs Encoding.dst = outputBase L

  First destination buffer.

• stride : y.regs Encoding.stride = 7 ^ L

  First source suffix length.

• prefixes : y.regs Encoding.prefixes = 1

  The empty transformed prefix.

• stage : y.regs Encoding.stage = 0

  No coordinates transformed yet.

• one : y.regs Encoding.one = 1

  Counter increment.

• seven : y.regs Encoding.seven = 7

  Input radix.

• ten : y.regs Encoding.ten = 10

  Output radix.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.exec_setup {w : ℕ} (L : ℕ) (x : WordRAM.Data 32) (hheader : x.mem 1 = L) (haddr : WordRAM.Fits w (addressBound L)) : ∃ (y : WordRAM.Data 32), WordRAM.ExecWithin w setup x y (5 * L + 18) ∧ SetupPost L x y

Header loads, both power computations, address arithmetic and counter initialization are included. The only fit premise is the explicit bound on ordinary natural numbers.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.Encoding.input_fits {w L : ℕ} (hw : 0 < w) (a : Fin (7 ^ L) → ℤ) (A : ℤ) (hA : 0 ≤ A) (ha : ∀ (i : Fin (7 ^ L)), |a i| ≤ A) (hmag : ↑(7 ^ L) * A < 2 ^ (w - 1)) (haddr : WordRAM.Fits (w + 2) (addressBound L)) : WordRAM.InputFits (w + 2) (input L a)

The actual flat input fits the target machine. Each signed input value uses the existing canonical encoding; the depth and the ordinary unsigned length header are bounded separately.