Computing the shared native prime bitmap #
The forest copies its computed candidate bound and fresh frontend endpoint into the existing native trial-division program. Its actual bitmap and count are retained for every recursion root.
Main results #
primes_exec: execute argument delivery and the complete table builder, preserving the frontend.
This native composition proof is original and reuses the existing primality computation.
theorem Cslib.Algorithms.WordRAM.ThreeSum.ChanHe.Preprocessing.primes_exec {κ n w : ℕ} (x : WordRAM.Data 128) (hs : Saved κ n x) (hfit : WordRAM.Fits w ((Frontend.layout κ n).endpoint + ThreeSum.ChanHe.mPar n (2 * (n + 2) ^ κ) + 4)) :
have m := ThreeSum.ChanHe.mPar n (2 * (n + 2) ^ κ);
have base := (Frontend.layout κ n).endpoint;
∃ (y : WordRAM.Data 128),
WordRAM.ExecWithin w (preparePrimes.seq (WordRAM.Code.rename primeRegisters PrimeTable.program)) x y
(2 + ((m + 1) * (7 * m + 15) + 8)) ∧ Saved κ n y ∧ y.mem = PrimeTable.memory x.mem base (m + 1) ∧ y.regs (primeRegisters PrimeTable.count) = m.primesLE.card ∧ (∀ q ≤ m, y.mem (base + q) = if Nat.Prime q then 1 else 0) ∧ ∀ p < base, y.mem p = x.mem p
Compute the actual shared bitmap from the already computed frontend and numeric parameters.