Complete charged native work at one live traversal entry #
Both native modulus searches, every counting call, the complete node builder and output delivery are composed here. The intermediate states are exposed as proof witnesses so the worklist proof can reuse the node builder's existing exact heavy/packed readback and allocation frame.
Main results #
visit_exec: execution of the complete native visit, charging both kernel calls, every argument instruction, the modulus copy and all output-delivery instructions.
These are original native composition proofs. The global traversal and initialized-input width and asymptotic bounds remain separate from this local calling-convention theorem.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Traversal.visit_exec {w : ℕ} (x : WordRAM.Data 128) (values : Fin 3 → ℕ → ℤ) (hm : 2 ≤ x.regs limit) (hmod : GenericRAM.Signed.Fits w ↑(x.regs limit ^ 2)) (hbudget : WordRAM.Fits (w + 2) (Modulus.budget (WordRAM.Data.comap kernel (modulusState x)))) (hnode : ∀ (M : ℕ), 1 ≤ M → M ≤ x.regs limit ^ 2 → GenericRAM.Signed.Fits w ↑(recordLayout x M).budget) (hN : 2 * x.regs limit ^ 2 ≤ x.regs groups) (hcard : x.regs primeCount = (x.regs limit).primesLE.card) (hbefore : x.regs bitmap + x.regs limit < x.regs heap) (hbitmap : ∀ q ≤ x.regs limit, x.mem (x.regs bitmap + q) = if Nat.Prime q then 1 else 0) (hvalues : ∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), GenericRAM.Signed.Fits w (values j i)) (hbdd : ∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), (values j i).natAbs ≤ x.regs magnitude) (hsrc : ∀ (j : Fin 3), x.regs (arraySource j) + x.regs (arrayLength j) ≤ x.regs heap) (hinput :
∀ (j : Fin 3), ∀ i < x.regs (arrayLength j), x.mem (x.regs (arraySource j) + i) = WordRAM.Signed.encode (values j i)) (hinj : ∀ (j : Fin 3), Set.InjOn (values j) ↑(Finset.range (x.regs (arrayLength j)))) (hone : x.regs one = 1) (htable : x.regs outputs + x.regs outputCount < x.regs heap) :
∃ (M : ℕ) (u : WordRAM.Data 128) (b : WordRAM.Data 128),
WordRAM.ExecWithin (w + 2) visit x (deliveryState b)
(Modulus.cost (WordRAM.Data.comap kernel (modulusState x)) + 66 * (recordLayout x M).total + 15 * M + 12 * x.regs groups + 277) ∧ (∀ (i : Fin 128), 64 ≤ ↑i → i ≠ selected → u.regs i = x.regs i) ∧ u.regs selected = M ∧ (∀ p < x.regs heap, u.mem p = x.mem p) ∧ NodePacking.Output (recordLayout x M) values u.mem b.mem ∧ (∀ (i : Fin 128), 64 ≤ ↑i → b.regs i = u.regs i) ∧ 1 ≤ M ∧ M ≤ x.regs limit ^ 2 ∧ M = ThreeSum.ChanHe.modulus (x.regs limit).primesLE (x.regs digits)
(Finset.image (values 0) (Finset.range (x.regs (arrayLength 0))))
(Finset.image (values 1) (Finset.range (x.regs (arrayLength 1))))
(Finset.image (values 2) (Finset.range (x.regs (arrayLength 2))))
The full native live-node visit, including all setup and output delivery. The returned intermediate states are reached by actual instructions, not supplied node or preprocessing oracles. The node's signed envelope derives the delivery address/counter fits.