A shared polynomial envelope for native traversal calls

The dynamic heap and all input blocks lie below H; each list has at most n elements. The candidate bound, label parameter, magnitude and common group count have fixed bounds m,Λ,U,N. A fourth-degree polynomial covers both existing kernel envelopes, including their native setup. This bound is later instantiated at the worklist's global heap frontier.

Main definitions

• envelope: a common polynomial bound for the actual native modulus and node calls.

Main results

• modulus_budget_le_envelope: the concrete selector budget is covered.
• node_budget_le_envelope: every selected modulus at most m² is covered.

The envelope and elementary inequalities are original resource estimates.

def Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.envelope (H n m Λ U N : ℕ) : ℕ

One fixed polynomial in the heap, list, candidate, label, magnitude and output-size bounds.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.envelope_ge_sum (H n m Λ U N : ℕ) : H + n + m ^ 2 + Λ + m + U + N + 100 ≤ envelope H n m Λ U N

The common envelope covers each size parameter and every smaller native word.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.modulus_budget_le_envelope (x : WordRAM.Data 128) (H n m Λ U N : ℕ) (hheap : x.regs heap ≤ H) (hsrc : ∀ (j : Fin 3), x.regs (arraySource j) + x.regs (arrayLength j) ≤ H) (hlen : ∀ (j : Fin 3), x.regs (arrayLength j) ≤ n) (hm : x.regs limit ≤ m) (hΛ : x.regs digits ≤ Λ) (hcard : x.regs primeCount ≤ m) (hbitmap : x.regs bitmap ≤ H) : Modulus.budget (WordRAM.Data.comap kernel (modulusState x)) ≤ envelope H n m Λ U N

The exact selector envelope, including all copied source pointers and histogram addresses, is bounded by one polynomial in the runtime size bounds.

theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.node_budget_le_envelope (x : WordRAM.Data 128) (H n m Λ U N M : ℕ) (hheap : x.regs heap ≤ H) (hlen : ∀ (j : Fin 3), x.regs (arrayLength j) ≤ n) (hM : M ≤ m ^ 2) (hU : x.regs magnitude ≤ U) (hN : x.regs groups ≤ N) : (recordLayout x M).budget ≤ envelope H n m Λ U N

The node layout, including every allocated output/scratch cell and tag value, is covered uniformly for every selected product at most m².