APSP in $O(n^{2.996001})$: definitions, part 2 of 2

/-
Copyright (c) 2026 Anthropic, PBC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
SPDX-License-Identifier: Apache-2.0
-/
-- Generated by skeleton subtraction from the ThreeSumApsp library at commit 7c34437be804.

import Definitions.Def_APSP2996001_Defs1

set_option autoImplicit false
set_option relaxedAutoImplicit false

section
-- Source module: ThreeSumApsp.Filter.HostFinal
/-!
# The filtering host: the last phase

For every group `g` that is not done, the blocks of its active candidates are scanned
(`groupBody`); the flag of `g` is 1 if it is done or a scan finds a zero triangle.  The time depends
on the number of active candidates (`final_spec`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits} {P : Program} {d : ℕ}

/-! ## Counting loops whose rounds take different times -/

/-! ## The scan of a block -/

/-- The scan of the block `j` for the pair of the group `g`. -/
def blockHit (n s : ℕ) (AB BC AC : List ℤ) (j g : ℕ) : Bool :=
  scanHit n AB BC AC (g / n) (g % n) (j * s) (min s (n - j * s))

/-! ## One group -/

/-- One block of the group.  Locals: 0 n, 1 ab, 2 bc, 3 ac, 4 out, 5 done, 6 act, 7 s, 8 m, 9 N,
10 a, 11 b, 12 g, 13 hit, 14 j, 15 c0, 16 len. -/
def groupRound (pScan : ℕ) : Stmt :=
  .ite (Light.v 13 =' Light.k 0)
    (.ite (M (Light.v 6 +' Light.v 14 *' Light.v 9 +' Light.v 12) =' Light.k 0) .skip
      (.set 15 (Light.v 14 *' Light.v 7) ;;
       .set 16 (Light.v 7) ;;
       .ite (Light.v 0 -' Light.v 15 <' Light.v 7) (.set 16 (Light.v 0 -' Light.v 15)) .skip ;;
       .call pScan [Light.v 1, Light.v 2, Light.v 3, Light.v 0, Light.v 10, Light.v 11, Light.v 15, Light.v 16] 13))
    .skip

/-- group(n, ab, bc, ac, out, done, act, s, m, N, a, b, g): the flag of the group `g = a n + b`. -/
def groupBody (pScan : ℕ) : Stmt :=
  .set 13 (M (Light.v 5 +' Light.v 12)) ;;
  Stmt.for 14 (Light.v 8) (groupRound pScan) ;;
  .store (Light.v 4 +' Light.v 12) (Light.v 13) ;;
  .set 0 (Light.k 0)

/-- The flag of the group `g` after the first `j` blocks. -/
def hitB (n s : ℕ) (AB BC AC : List ℤ) (act D : ℕ → Bool) (g j : ℕ) : Bool :=
  D g || (List.range j).any fun j' => act (j' * (n * n) + g) && blockHit n s AB BC AC j' g

/-- The number of active candidates of a group that is not done. -/
def cntG (N m : ℕ) (act D : ℕ → Bool) (g : ℕ) : ℕ :=
  ∑ j ∈ Finset.range m, if (act (j * N + g) && !D g) then 1 else 0

/-- The time of group. -/
def tGroup (m s c : ℕ) : ℕ := 60 * m + 20 + c * tScan s

/-! ## All groups -/

/-- final(n, ab, bc, ac, out, done, act, s, m, N): the flags of all groups.
Locals: 0 n, 1 ab, 2 bc, 3 ac, 4 out, 5 done, 6 act, 7 s, 8 m, 9 N, 10 a, 11 b, 12 g, 13 r. -/
def finalBody (pGroup : ℕ) : Stmt :=
  Stmt.for 12 (Light.v 9) (
    .call pGroup [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9, Light.v 10, Light.v 11, Light.v 12] 13 ;;
    .set 11 (Light.v 11 +' Light.k 1) ;;
    .ite (Light.v 11 =' Light.v 0) (.set 11 (Light.k 0) ;; .set 10 (Light.v 10 +' Light.k 1)) .skip) ;;
  .set 0 (Light.k 0)

/-- The time of final, with `c` the number of active candidates of the groups that are not done. -/
def tFinal (N m s c : ℕ) : ℕ := N * (60 * m + 60) + c * tScan s + 10

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostStep
/-!
# The filtering host: the layout, and one step of a round

* The layout of the memory of the host above the free pointer `fr`: the primes below `2R`, the pool,
  the marks `act` of the `L = m n²` candidates, the flags `done` of the `n²` groups, the masses `ua`
  of the groups, the counts `cnt` of the oracle, the table `gt` of the masses at the moduli `M q`,
  and the free pointer `top` of the oracle.
* `Env`: what the host knows about the limits and the instance; `FMem`: the memory between the
  steps.
* `stepBody`: one step of a round (`step_spec`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits}

/-! ## The layout -/

/-- The number of candidates, `m n²`. -/
def LL (n : ℕ) : ℕ := mOf n * (n * n)

/-- The pool. -/
def aPL (n fr : ℕ) : ℕ := fr + 2 * RR n
/-- The marks of the candidates. -/
def aACT (n fr : ℕ) : ℕ := fr + 4 * RR n
/-- The flags of the groups. -/
def aDONE (n fr : ℕ) : ℕ := aACT n fr + Light.Filter.LL n
/-- The masses of the groups at the current modulus. -/
def aUA (n fr : ℕ) : ℕ := aDONE n fr + n * n
/-- The counts written by the oracle. -/
def aCNT (n fr : ℕ) : ℕ := aUA n fr + n * n
/-- The table of the masses at the moduli `M q`. -/
def aGT (n fr : ℕ) : ℕ := aCNT n fr + Light.Filter.LL n
/-- The free pointer of the oracle (and the table of the sieve). -/
def aTOP (n fr : ℕ) : ℕ := aGT n fr + 2 * RR n * (n * n)

/-- The largest time of the oracle at the moduli up to `Pmax`. -/
def supTo (To : List ℕ → ℕ) (n U : ℕ) : ℕ :=
  (Finset.range (PmaxOf n + 1)).sup fun p => To [n, U, sOf n, p]

/-- A bound on the numbers that the host forms. -/
def filterWord (n U : ℕ) : ℕ :=
  10 ^ 9 * ((n + 1) ^ 3 * (U + 1) * (RR n + 1) * (PmaxOf n + 1)) ^ 2

/-- What the host knows: the instance (in the first memory `μ0`), the limits, and the need of the
oracle at all moduli up to `Pmax`.  The host runs at depth `d`. -/
structure Env (lim : Limits) (d : ℕ) (x : AEInst) (fr : ℕ) (μ0 : ℕ → ℤ) (needo : List ℕ → Light.Need) :
    Prop where
  pre : x.Pre μ0 fr
  hw : (lim.space : ℤ) ≤ lim.word
  space : aTOP x.n fr + 2 * RR x.n ≤ lim.space
  word : (filterWord x.n x.U : ℤ) ≤ lim.word
  oracle : ∀ p ≤ PmaxOf x.n, (needo [x.n, x.U, sOf x.n, p]).Ok lim (aTOP x.n fr) (d + 4)
  depth : d + 5 ≤ lim.depth

/-- The memory between two steps: nothing below `fr` has changed, and the pool, the marks `act` and
the flags `D` are in place. -/
structure FMem (x : AEInst) (fr : ℕ) (μ0 μ : ℕ → ℤ) (act D : ℕ → Bool) : Prop where
  kept : Light.Kept μ0 μ fr
  pool : Light.Filter.Arr μ (aPL x.n fr) (QOf x.n) fun t => (poolAt x.n t : ℤ)
  act : Light.Filter.Arr μ (aACT x.n fr) (Light.Filter.LL x.n) fun i => bitB (act i)
  done : Light.Filter.Arr μ (aDONE x.n fr) (x.n * x.n) fun g => bitB (D g)

/-- The masses of the groups that are not done, at the modulus `M`. -/
def UOk (x : AEInst) (fr : ℕ) (μ : ℕ → ℤ) (act D : ℕ → Bool) (M : ℕ) : Prop :=
  ∀ g < x.n * x.n, D g = false →
    μ (aUA x.n fr + g) = (mass x.n (sOf x.n) x.AB x.BC x.AC act M g : ℤ)

/-- The instance of the oracle at the modulus `p`. -/
def oInst (x : AEInst) (fr p : ℕ) : OracleInst :=
  { toTriInst := x.toTriInst, s := sOf x.n, p := p, cnt := aCNT x.n fr }

/-! ## Bounds on the numbers -/

/-- The product behind `filterWord`. -/
def KW (n U : ℕ) : ℕ := (n + 1) ^ 3 * (U + 1) * (RR n + 1) * (PmaxOf n + 1)

/-! ## Keeping the memory -/

section keep

variable {x : AEInst} {fr : ℕ} {μ0 μ μ' : ℕ → ℤ} {act D : ℕ → Bool} {M : ℕ}

/-- The table of the masses at the moduli `M q`, for the first `t` primes of the pool. -/
def GOk (x : AEInst) (fr : ℕ) (μ : ℕ → ℤ) (act : ℕ → Bool) (M t : ℕ) : Prop :=
  ∀ t' < t, ∀ g < x.n * x.n, μ (aGT x.n fr + (t' * (x.n * x.n) + g)) =
    (mass x.n (sOf x.n) x.AB x.BC x.AC act (M * poolAt x.n t') g : ℤ)

end keep

/-! ## One step -/

/-- step(n, U, ab, bc, ac, s, pl, act, done, ua, cnt, gt, top, N, m, Q, h, M): the oracle at every
`M q`, the certificate, the choice of `q*`; it returns `M q*`.  Locals: 18 t, 19 scratch, 20 the
row `t*`. -/
def stepBody (pO pAggr pCert pArg pCopy : ℕ) : Stmt :=
  Stmt.for 18 (Light.v 15) (
    .call pO [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 17 *' M (Light.v 6 +' Light.v 18), Light.v 10, Light.v 12] 19 ;;
    .call pAggr [Light.v 10, Light.v 7, Light.v 11 +' Light.v 18 *' Light.v 13, Light.v 13, Light.v 14] 19) ;;
  .call pCert [Light.v 9, Light.v 11, Light.v 8, Light.v 13, Light.v 15, Light.v 16] 19 ;;
  .call pArg [Light.v 11, Light.v 8, Light.v 13, Light.v 15] 20 ;;
  .call pCopy [Light.v 11 +' Light.v 20 *' Light.v 13, Light.v 9, Light.v 13] 19 ;;
  .set 0 (Light.v 17 *' M (Light.v 6 +' Light.v 20))

/-- The arguments of step. -/
def stepArgs (x : AEInst) (fr M : ℕ) : List ℤ :=
  [x.n, x.U, x.ab, x.bc, x.ac, sOf x.n, aPL x.n fr, aACT x.n fr, aDONE x.n fr, aUA x.n fr,
    aCNT x.n fr, aGT x.n fr, aTOP x.n fr, ((x.n * x.n : ℕ) : ℤ), mOf x.n, QOf x.n, hOf x.n x.U, M]

/-- The time of step. -/
def tStep (To : List ℕ → ℕ) (n U : ℕ) : ℕ :=
  QOf n * (supTo To n U + tAggr (n * n) (mOf n) + 40) + tCert (n * n) (QOf n) +
    tArgmin (n * n) (QOf n) + copyTime (n * n) + 60

/-- The procedures that step calls. -/
structure StepProcs (P : Program) (pAggr pCert pArg pCopy : ℕ) : Prop where
  aggr : P[pAggr]? = some aggrBody
  cert : P[pCert]? = some certBody
  arg : P[pArg]? = some argminBody
  copy : P[pCopy]? = some copyBody

instance (n s U : ℕ) (AB BC AC : List ℤ) (act : ℕ → Bool) (M g : ℕ) :
    Decidable (certOf n s U AB BC AC act M g) := by
  unfold certOf; infer_instance

section step

variable {P₀ R : Program} {pO pAggr pCert pArg pCopy : ℕ} {To : List ℕ → ℕ}
  {needo : List ℕ → Need} {d0 : ℕ} {x : AEInst} {fr : ℕ} {μ0 : ℕ → ℤ}

/-- The flags after the certificate of a step at the modulus `Mc`. -/
def stepD (x : AEInst) (act D : ℕ → Bool) (Mc : ℕ) : ℕ → Bool := fun g =>
  D g || decide (∀ t < QOf x.n, hOf x.n x.U * mass x.n (sOf x.n) x.AB x.BC x.AC act Mc g <
    QOf x.n * mass x.n (sOf x.n) x.AB x.BC x.AC act (Mc * poolAt x.n t) g)

/-- The remaining mass at the modulus `M`, outside the groups that are done. -/
def remMass (x : AEInst) (act D : ℕ → Bool) (M : ℕ) : ℕ :=
  ∑ g ∈ Finset.range (x.n * x.n), if D g then 0 else mass x.n (sOf x.n) x.AB x.BC x.AC act M g

end step

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostRound
/-!
# The filtering host: one round

A round: the masses at the modulus `1`, then `r` steps, each of which certifies some groups and
multiplies the modulus by a prime of the pool, and at the end the marks of the candidates whose
count at the final modulus is `0` are cleared (`round_spec`).

The invariants: a group that is done has a witness (`Inv1`), and every candidate of a group that is
not done whose block has a witness is marked (`Inv2`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits}

/-- A group that is done has a witness. -/
def Inv1 (x : AEInst) (D : ℕ → Bool) : Prop :=
  ∀ g < x.n * x.n, D g = true → ∃ c < x.n, triSum x.n x.AB x.BC x.AC g c = 0

/-- A candidate of a group that is not done, whose block has a witness, is marked. -/
def Inv2 (x : AEInst) (act D : ℕ → Bool) : Prop :=
  ∀ i < Light.Filter.LL x.n, D (i % (x.n * x.n)) = false → 0 < cntOf x.n (sOf x.n) 0 x.AB x.BC x.AC i →
    act i = true

/-- round(n, U, ab, bc, ac, s, pl, act, done, ua, cnt, gt, top, N, m, Q, h, r).  Locals: 18 the
modulus `M`, 19 the step, 20 scratch. -/
def roundBody (pO pAggr pStep pFA : ℕ) : Stmt :=
  .call pO [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.k 1, Light.v 10, Light.v 12] 20 ;;
  .call pAggr [Light.v 10, Light.v 7, Light.v 9, Light.v 13, Light.v 14] 20 ;;
  .set 18 (Light.k 1) ;;
  Stmt.for 19 (Light.v 17) (.call pStep [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9, Light.v 10, Light.v 11,
    Light.v 12, Light.v 13, Light.v 14, Light.v 15, Light.v 16, Light.v 18] 18) ;;
  .call pO [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 18, Light.v 10, Light.v 12] 20 ;;
  .call pFA [Light.v 7, Light.v 10, Light.v 14 *' Light.v 13] 20

/-- The time of round. -/
def tRound (To : List ℕ → ℕ) (n U : ℕ) : ℕ :=
  2 * supTo To n U + tAggr (n * n) (mOf n) + rOf n * (tStep To n U + 58) + tFilterAct (Light.Filter.LL n) + 200

/-- The locals of round. -/
def rFrame (x : AEInst) (fr Mc st : ℕ) (z : ℤ) : List ℤ :=
  stepArgs x fr (rOf x.n) ++ [(Mc : ℤ), (st : ℤ), z]

/-- The procedures that round calls. -/
structure RoundProcs (P : Program) (pO pAggr pStep pFA pCert pArg pCopy : ℕ) : Prop where
  step : P[pStep]? = some (stepBody pO pAggr pCert pArg pCopy)
  sp : StepProcs P pAggr pCert pArg pCopy
  fa : P[pFA]? = some filterActBody

section round

variable {P₀ R : Program} {pO pAggr pStep pFA pCert pArg pCopy : ℕ} {To : List ℕ → ℕ}
  {needo : List ℕ → Need} {d0 : ℕ} {x : AEInst} {fr : ℕ} {μ0 : ℕ → ℤ}

/-- The invariant of the loop over the steps. -/
def StepInv (x : AEInst) (fr : ℕ) (μ0 : ℕ → ℤ) (act D : ℕ → Bool) (st : ℕ) (σ : State) : Prop :=
  ∃ (Mc : ℕ) (z : ℤ) (D' : ℕ → Bool) (μ' : ℕ → ℤ), σ = ⟨Light.frame (rFrame x fr Mc st z), μ'⟩ ∧
    FMem x fr μ0 μ' act D' ∧ UOk x fr μ' act D' Mc ∧ 1 ≤ Mc ∧ Mc ≤ (2 * RR x.n) ^ st ∧
    Inv1 x D' ∧ (∀ g, D g = true → D' g = true) ∧
    QOf x.n ^ st * tot x.n (sOf x.n) x.AB x.BC x.AC (eff (x.n * x.n) act D') Mc ≤
      (2 * hOf x.n x.U) ^ st * tot x.n (sOf x.n) x.AB x.BC x.AC (eff (x.n * x.n) act D) 1

end round

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostCore
/-!
# The filtering host: the rounds and the final scans

`core` runs the rounds and then scans the blocks of the candidates that are still marked, in the
groups that are not done (`core_spec`).  The flags it writes are the flags of all-edges Exact
Triangle, whatever the guard; with the guard, no candidate is marked after the rounds, so that the
final scans cost nothing.
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits}

/-! ## The flags -/

/-! ## The program -/

/-- core(n, U, ab, bc, ac, s, pl, act, done, ua, cnt, gt, top, N, m, Q, h, r, rounds, out).  Locals:
20 the round, 21 scratch. -/
def coreBody (pRound pFinal : ℕ) : Stmt :=
  Stmt.for 20 (Light.v 18) (.call pRound [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 5, Light.v 6, Light.v 7, Light.v 8, Light.v 9, Light.v 10, Light.v 11,
    Light.v 12, Light.v 13, Light.v 14, Light.v 15, Light.v 16, Light.v 17] 21) ;;
  .call pFinal [Light.v 0, Light.v 2, Light.v 3, Light.v 4, Light.v 19, Light.v 8, Light.v 7, Light.v 5, Light.v 14, Light.v 13] 21 ;;
  .set 0 (Light.k 0)

/-- The arguments of core. -/
def coreArgs (x : AEInst) (fr : ℕ) : List ℤ :=
  stepArgs x fr (rOf x.n) ++ [(roundsOf x.n : ℤ), (x.out : ℤ)]

/-- The number of candidates that the final scans may meet: none with the guard, all without. -/
def cFin (n U : ℕ) : ℕ := if Guard n U then 0 else Light.Filter.LL n

/-- The time of core. -/
def tCore (To : List ℕ → ℕ) (n U : ℕ) : ℕ :=
  roundsOf n * (Light.Filter.tRound To n U + 30) + tFinal (n * n) (mOf n) (sOf n) (cFin n U) + 30

/-- The procedures of the final scans. -/
structure FinalProcs (P : Program) (pFinal pGroup pScan : ℕ) : Prop where
  final : P[pFinal]? = some (finalBody pGroup)
  group : P[pGroup]? = some (groupBody pScan)
  scan : P[pScan]? = some scanBody

section core

variable {P₀ R : Program} {pO pAggr pStep pFA pCert pArg pCopy : ℕ} {To : List ℕ → ℕ}
  {needo : List ℕ → Need} {d0 : ℕ} {x : AEInst} {fr : ℕ} {μ0 : ℕ → ℤ}

/-- The invariant of the rounds. -/
def CoreInv (x : AEInst) (fr : ℕ) (μ0 : ℕ → ℤ) (ρ : ℕ) (μ : ℕ → ℤ) : Prop :=
  ∃ act D : ℕ → Bool, FMem x fr μ0 μ act D ∧ Inv1 x D ∧ Inv2 x act D ∧
    (Guard x.n x.U → 2 ^ (dOf x.n * ρ) * cardA x.n (sOf x.n) (eff (x.n * x.n) act D) ≤ Light.Filter.LL x.n)

end core

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostTop
/-!
# The filtering host: the parameters

The first part of the host computes the parameters of the filtering from `n` and `U` and lays out
the memory above the free pointer (`params_spec`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits}

/-! ## The computation of the parameters -/

/-- The parameters, from `n` (local 0), `U` (local 1) and the free pointer (local 6): 7 `k`, 8 `ℓ`,
9 `R`, 10 `b`, 11 `d`, 12 the number of rounds, 13 `s`, 14 `m`, 15 `c_K`, 16 `r`, 17 `B`, 18 `h`,
19 `N = n²`, and the places 20 `pl`, 21 `act`, 22 `done`, 23 `ua`, 24 `cnt`, 25 `gt`, 26 `top`. -/
def paramsStmt (pLog pSqrt pPow pDiv : ℕ) : Stmt :=
  .call pLog [Light.v 0] 7 ;; .set 7 (Light.v 7 +' Light.k 1) ;;
  .call pSqrt [Light.v 7] 8 ;; .set 8 (Light.v 8 +' Light.k 1) ;;
  .call pPow [Light.v 8] 9 ;;
  .call pSqrt [Light.v 8] 10 ;; .set 10 (Light.v 8 *' (Light.v 10 +' Light.k 1)) ;;
  .call pDiv [Light.v 10, Light.k 2] 11 ;;
  .call pDiv [Light.k 3 *' Light.v 7, Light.v 11] 12 ;; .set 12 (Light.v 12 +' Light.k 1) ;;
  .call pDiv [Light.k 284225 *' Light.v 7, Light.k 10000000] 13 ;; .call pPow [Light.v 13] 13 ;;
  .call pDiv [Light.v 0 +' Light.v 13 -' Light.k 1, Light.v 13] 14 ;;
  .call pLog [Light.v 13] 15 ;; .set 15 (Light.v 15 +' Light.k 1) ;;
  .call pDiv [Light.v 15 +' Light.v 10, Light.v 8] 16 ;; .set 16 (Light.v 16 +' Light.k 1) ;;
  .call pLog [Light.k 3 *' Light.v 1] 17 ;; .set 17 (Light.v 17 +' Light.k 1) ;;
  .call pDiv [Light.v 17 -' Light.k 1, Light.v 8] 18 ;;
  .set 19 (Light.v 0 *' Light.v 0) ;;
  .set 20 (Light.v 6 +' Light.k 2 *' Light.v 9) ;;
  .set 21 (Light.v 6 +' Light.k 4 *' Light.v 9) ;;
  .set 22 (Light.v 21 +' Light.v 14 *' Light.v 19) ;;
  .set 23 (Light.v 22 +' Light.v 19) ;;
  .set 24 (Light.v 23 +' Light.v 19) ;;
  .set 25 (Light.v 24 +' Light.v 14 *' Light.v 19) ;;
  .set 26 (Light.v 25 +' Light.k 2 *' Light.v 9 *' Light.v 19)

/-- The locals after the parameters. -/
def topFrame (x : AEInst) (fr : ℕ) : List ℤ :=
  [x.n, x.U, x.ab, x.bc, x.ac, x.out, fr, kOf x.n, ellOf x.n, RR x.n, bOf x.n, dOf x.n,
    roundsOf x.n, sOf x.n, mOf x.n, cKOf x.n, rOf x.n, BOf x.U, hOf x.n x.U, ((x.n * x.n : ℕ) : ℤ),
    aPL x.n fr, aACT x.n fr, aDONE x.n fr, aUA x.n fr, aCNT x.n fr, aGT x.n fr, aTOP x.n fr]

/-- The time of the parameters. -/
def tParams (n U : ℕ) : ℕ :=
  log2Time n + sqrtTime (kOf n) + tPow2 (ellOf n) + sqrtTime (ellOf n) + tDiv (bOf n) 2 +
    tDiv (3 * kOf n) (dOf n) + tDiv (284225 * kOf n) (10 ^ 7) + tPow2 (284225 * kOf n / 10 ^ 7) +
    tDiv (n + sOf n - 1) (sOf n) + log2Time (sOf n) + tDiv (cKOf n + bOf n) (ellOf n) +
    log2Time (3 * U) + tDiv (BOf U - 1) (ellOf n) + 400

/-- The procedures for the parameters. -/
structure ParamProcs (P : Program) (pLog pSqrt pPow pDiv : ℕ) : Prop where
  log : P[pLog]? = some log2Body
  sqrt : P[pSqrt]? = some sqrtBody
  pow : P[pPow]? = some pow2Body
  div : P[pDiv]? = some divBody

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostAssemble
/-!
# The filtering host: the top procedure

After the parameters, the host sieves the primes below `2R`, keeps those of the pool, marks all
candidates and no group, and runs `core` (`top_spec`).
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

variable {lim : Limits}

/-- The pool, the marks and the flags, and the core.  Locals 27 `Q`, 28 scratch. -/
def restStmt (pSieve pPF pFill pCore : ℕ) : Stmt :=
  .call pSieve [Light.k 2 *' Light.v 9 -' Light.k 1, Light.v 6, Light.v 26] 27 ;;
  .call pPF [Light.v 6, Light.v 27, Light.v 9, Light.v 20] 27 ;;
  .call pFill [Light.v 21, Light.v 14 *' Light.v 19, Light.k 1] 28 ;;
  .call pFill [Light.v 22, Light.v 19, Light.k 0] 28 ;;
  .call pCore [Light.v 0, Light.v 1, Light.v 2, Light.v 3, Light.v 4, Light.v 13, Light.v 20, Light.v 21, Light.v 22, Light.v 23, Light.v 24, Light.v 25, Light.v 26, Light.v 19,
    Light.v 14, Light.v 27, Light.v 18, Light.v 16, Light.v 12, Light.v 5] 28 ;;
  .set 0 (Light.k 0)

/-- The host. -/
def topBody (pLog pSqrt pPow pDiv pSieve pPF pFill pCore : ℕ) : Stmt :=
  paramsStmt pLog pSqrt pPow pDiv ;; restStmt pSieve pPF pFill pCore

/-- The time of the host. -/
def tTop (To : List ℕ → ℕ) (n U : ℕ) : ℕ :=
  tParams n U + sieveTime (2 * RR n - 1) + tPoolFilter (2 * RR n) + fillTime (Light.Filter.LL n) +
    fillTime (n * n) + tCore To n U + 200

/-- The procedures of the host besides core. -/
structure TopProcs (P : Program) (pSieve pPF pFill : ℕ) : Prop where
  sieve : P[pSieve]? = some sieveBody
  pf : P[pPF]? = some poolFilterBody
  fill : P[pFill]? = some fillBody

section top

variable {P₀ R : Program} {pO pAggr pStep pFA pCert pArg pCopy : ℕ} {To : List ℕ → ℕ}
  {needo : List ℕ → Need} {d : ℕ} {x : AEInst} {fr : ℕ} {μ0 : ℕ → ℤ}

end top

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostMain
/-!
# The filtering host solves all-edges Exact Triangle

`filter_host`: from a solver of the counting oracle, the host builds a solver of all-edges Exact
Triangle, within `filterTime To` steps and with the need `filterNeed needo`; its need is
polynomially bounded if that of the oracle is.
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

/-! ## The program -/

/-- The procedures of the host, appended to a program of length `o` whose procedure `po` is the
counting oracle.  The host is procedure `o + 18`. -/
def hostProcs (o po : ℕ) : Program :=
  [aggrBody, certBody, argminBody, copyBody, filterActBody,
    stepBody po o (o + 1) (o + 2) (o + 3),
    roundBody po o (o + 5) (o + 4),
    scanBody, groupBody (o + 7), finalBody (o + 8), coreBody (o + 6) (o + 9),
    log2Body, sqrtBody, pow2Body, divBody, sieveBody, poolFilterBody, fillBody,
    Light.Filter.topBody (o + 11) (o + 12) (o + 13) (o + 14) (o + 15) (o + 16) (o + 17) (o + 10)]

/-! ## The time and the need -/

/-- **The time of the host**: the parameters, the sieve, the pool, the marks, and the core, which
runs `roundsOf n` rounds of `rOf n` steps; a step calls the oracle `QOf n` times (once per prime of
the pool) and a round twice more, each call within `supTo To n U`. -/
def filterTime (To : List ℕ → ℕ) (n U : ℕ) : ℕ := tTop To n U

/-- The largest word of the oracle at the moduli up to `Pmax`. -/
def supW (needo : List ℕ → Light.Need) (n U : ℕ) : ℕ :=
  (Finset.range (PmaxOf n + 1)).sup fun p => (needo [n, U, sOf n, p]).word

/-- The most cells of the oracle at the moduli up to `Pmax`. -/
def supC (needo : List ℕ → Light.Need) (n U : ℕ) : ℕ :=
  (Finset.range (PmaxOf n + 1)).sup fun p => (needo [n, U, sOf n, p]).cells

/-- The largest depth of the oracle at the moduli up to `Pmax`. -/
def supD (needo : List ℕ → Light.Need) (n U : ℕ) : ℕ :=
  (Finset.range (PmaxOf n + 1)).sup fun p => (needo [n, U, sOf n, p]).depth

/-- **The need of the host.** -/
def filterNeed (needo : List ℕ → Light.Need) (n U : ℕ) : Light.Need where
  word := filterWord n U + supW needo n U
  cells := aTOP n 0 + 2 * RR n + supC needo n U
  depth := supD needo n U + 5

variable {lim : Limits}

/-! ## The host solves all-edges Exact Triangle -/

/-! ## The need is polynomially bounded -/

/-- A bound on the need of the oracle at the moduli up to `Pmax`. -/
def oBound (s0 k0 n U : ℕ) : ℕ :=
  2 ^ s0 * ((n + 1) * ((U + 1) * ((2 * n + 2) * ((2 ^ 8 * (2 * n + 1) ^ 11 + 1) * 1)))) ^ k0

end Light.Filter
end
end

section
-- Source module: ThreeSumApsp.Filter.HostTime
/-!
# The time of the filtering host

`filterTime_le`: the host calls the oracle `roundsOf n * (rOf n * QOf n + 2)` times, each within
`supTo To n U`; besides, it spends `1000 (n + 1)² (Q + 1) (m + Q + 1)` steps per step of a round and
once for the final pass, `cFin n U * tScan (sOf n)` steps for the final scans (`0` under the guard,
`m n² (24 s + 35)` without it), and `tPrelude n U` steps for the parameters, the sieve, the pool and
the marks.
-/

@[expose] public section

open ThreeSumApsp

namespace Light.Filter

open ThreeSumApsp.Spec Light.Sec3

/-- The time of the parameters, the sieve, the pool and the marks. -/
def tPrelude (n U : ℕ) : ℕ :=
  tParams n U + sieveTime (2 * RR n - 1) + tPoolFilter (2 * RR n) + fillTime (Light.Filter.LL n) +
    fillTime (n * n) + 300

/-- The work of one step of a round, apart from the calls of the oracle (a bound). -/
def stepWork (n : ℕ) : ℕ := 1000 * ((n + 1) ^ 2 * (QOf n + 1) * (mOf n + QOf n + 1))

end Light.Filter
end
end