Entry and return assertions for the native node induction

Main definitions

• PrunedQuery.NodeReady: the actual stored frame and timestamped query representation.
• PrunedQuery.NodeResult: register, value and spatial conclusions after returning.

Main results

• PrunedQuery.exec_ready_zero: the terminal induction case for arbitrary supplied arrays.

Neither assertion contains execution, time or fit fields. Width and magnitude assumptions are ordinary numerical input bounds, and execution is proved in the existing native semantics.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady (L f a0 b0 n d p E : ℕ) (S : Finset (MatrixMultiplication.Schonhage.OutStr n)) (x : WordRAM.Data registers) : Prop

Entry to one node, as established by the native root scan or a native child push.

• regs : KernelRegs L f a0 b0 x

  The computed workspace pointers and constant registers.

• depth_add : d + n = L

  The two tuple lengths agree with the original depth.

• prefix_lt : p < 10 ^ d

  The leaf prefix is within its already processed digit space.

• level_eq : x.regs level = d

  The actual cursor points to this frame.

• mode_eq : x.regs mode = 0

  This node has not begun its entry phase.

• active_eq : x.regs active = 1

  The traversal is still active.

• epoch_eq : x.regs epoch = E

  Current actual timestamp generation.

• frame : { base := f + 4 * d, length := 4 }.Realizes x.mem ![S.card, p, 10 ^ d, 0]

  Four stored words: count, prefix, stride and first term.

• requests : ScanMemory x.mem (f + 4 * (L + 1) + d * 10 ^ L) (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L) E (10 ^ L) (Finset.image (fun (q : MatrixMultiplication.Schonhage.OutStr n) => ↑(queryIndex q)) S)

  The actual list and directory represent exactly the requested numerical codes.

structure Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeResult (L f a0 b0 n d E : ℕ) (S : Finset (MatrixMultiplication.Schonhage.OutStr n)) (a b : MatrixMultiplication.Schonhage.Leaf n → ℤ) (x y : WordRAM.Data registers) : Prop

The spatial and mathematical result of one node. This is a postcondition on the actual data, with no execution or time claim embedded in it.

• regs : KernelRegs L f a0 b0 y

  Constant parameters remain unchanged.

• level_eq : y.regs level = if d = 0 then 0 else d - 1

  Return to the parent, keeping zero at the root.

• mode_eq : 0 < d → y.regs mode = 2

  A parent resumes accumulation after a non-root node.

• active_eq : y.regs active = if d = 0 then 0 else 1

  Only returning from the root stops traversal.

• epoch_le : E ≤ y.regs epoch

  Timestamp generations do not go backwards.

• epoch_upper : y.regs epoch ≤ E + epochAllowance n

  All fresh generations are covered by the remaining-depth allowance.

• timestamps (q : ℕ) : q < 10 ^ L → y.mem (f + 4 * (L + 1) + 2 * (L + 1) * 10 ^ L + q) ≤ y.regs epoch

  The directory is ready for the next fresh-generation scan.

• values (q : MatrixMultiplication.Schonhage.OutStr n) : q ∈ S → y.mem (f + 4 * (L + 1) + (L + 1) * 10 ^ L + d * 10 ^ L + ↑(queryIndex q)) = WordRAM.Signed.encode (MatrixMultiplication.Schonhage.Pruned.result n a b S q)

  Every requested cell holds the existing pruned result, in its original code position.

• frame : WordRAM.Modifies (nodeWrites L f d) x.mem y.mem

  Caller memory, including ancestor rows, is preserved outside the concrete node frame.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.card_le {L f a0 b0 n d p E : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) : S.card ≤ 10 ^ L

A ready frame's stored count cannot exceed its actual list row capacity.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.image_read {L f a0 b0 n d p E : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) : Finset.image (fun (i : ℕ) => x.mem (f + 4 * (L + 1) + d * 10 ^ L + i)) (Finset.range S.card) = Finset.image (fun (q : MatrixMultiplication.Schonhage.OutStr n) => ↑(queryIndex q)) S

The occupied words of the actual row encode exactly the requested output strings.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.exists_of_read {L f a0 b0 n d p E i : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) (hi : i < S.card) : ∃ q ∈ S, ↑(queryIndex q) = x.mem (f + 4 * (L + 1) + d * 10 ^ L + i)

Every occupied source-list word comes from one of the requested mathematical outputs.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.read_lt {L f a0 b0 n d p E i : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) (hi : i < S.card) : x.mem (f + 4 * (L + 1) + d * 10 ^ L + i) < 10 ^ n

Actual query words fit the remaining query space, not only the original workspace row.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.exists_read {L f a0 b0 n d p E : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) {q : MatrixMultiplication.Schonhage.OutStr n} (hq : q ∈ S) : ∃ i < S.card, x.mem (f + 4 * (L + 1) + d * 10 ^ L + i) = ↑(queryIndex q)

Every requested output occurs at a concrete occupied position of the native list.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.injOn_read {L f a0 b0 n d p E : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) : Set.InjOn (fun (i : ℕ) => x.mem (f + 4 * (L + 1) + d * 10 ^ L + i)) {i : ℕ | i < S.card}

Distinct occupied positions cannot name the same parent query.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.NodeReady.source_before {L f a0 b0 n d p E base : ℕ} {S : Finset (MatrixMultiplication.Schonhage.OutStr n)} {x : WordRAM.Data registers} (h : NodeReady L f a0 b0 n d p E S x) (hbase : base + 10 ^ L ≤ f) (v : MatrixMultiplication.Schonhage.Leaf n) : base + p + 10 ^ d * ↑(Encoding.leafIndex v) < f

Each strided input address remains inside the original input block below the workspace.

theorem Cslib.Algorithms.WordRAM.MatrixMultiplication.Schonhage.PrunedQuery.exec_ready_zero {w L f a0 b0 d p E A B : ℕ} (S : Finset (MatrixMultiplication.Schonhage.OutStr 0)) (a b : MatrixMultiplication.Schonhage.Leaf 0 → ℤ) (x : WordRAM.Data registers) (hx : NodeReady L f a0 b0 0 d p E S x) (hleft : ∀ (v : MatrixMultiplication.Schonhage.Leaf 0), x.mem (a0 + p + 10 ^ d * ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (a v)) (hright : ∀ (v : MatrixMultiplication.Schonhage.Leaf 0), x.mem (b0 + p + 10 ^ d * ↑(Encoding.leafIndex v)) = WordRAM.Signed.encode (b v)) (ha : ∀ (v : MatrixMultiplication.Schonhage.Leaf 0), |a v| ≤ ↑A) (hb : ∀ (v : MatrixMultiplication.Schonhage.Leaf 0), |b v| ≤ ↑B) (hw : 0 < w) (hmag : magnitudeBound L A B < 2 ^ (w - 1)) (hfit : WordRAM.Fits (w + 2) (nodeBudget L f a0 b0 E 0)) : ∃ (y : WordRAM.Data registers), NodeResult L f a0 b0 0 d E S a b x y ∧ ∀ (z : WordRAM.Data registers) (U : ℕ), WordRAM.ExecWithin (w + 2) controller y z U → WordRAM.ExecWithin (w + 2) controller x z (traceWeight S + U)

The terminal node proof obtains its signed fits from the common original magnitude envelope. The same returned memory satisfies the result and the charged native continuation.