Update EIP-8288: state the aggregation circuit's required properties

EIPS/eip-8288.md

@@ -214,6 +214,12 @@ The recursive STARK is verified using a fixed protocol-level `AGGREGATED_VK`.
 
 To enable unlimited-depth recursion, we need to pass the `AGGREGATED_VK` in as an input to the proof itself.
 
+The aggregation circuit MUST satisfy all of the following, for any number of dependencies proven:
+
+1. The serialized size of a recursive STARK MUST be bounded by a constant.
+2. The cost of verifying a recursive STARK MUST be bounded by a constant.
+3. The cost of absorbing a recursive STARK as a nested proof MUST be bounded by a constant.
+
 #### Block Validity Rules
 
 A block is valid if and only if:
@@ -373,6 +379,8 @@ verification_gas(dep_verify_frame) = sum(
 )
 ```
 
+`LEANSPHINCS_VERIFICATION_GAS` and `LEANSTARK_VERIFICATION_GAS` price establishing a dependency for the first time. They do not price a recursive aggregation round.
+
 The actual STARK verification is performed off-chain by the builder, so the gas cost represents the _expected_ cost of verifying the recursive STARK, not the actual cost. It is much cheaper than the onchain costs for similar operations because the cost is only paid by the builder and the mempool, not by all validating nodes.
 
 Each transaction also pays for its share of the `recursive_stark` header field:
@@ -429,6 +437,8 @@ There may be two valid reasons to adjust the current fixed-cost approach and swi
 - **Mixed k-time and unlimited-time usage of leanSPHINCS**: k-time signatures are significantly smaller than unlimited-time signatures, and SPHINCS could expose a parametrization that supports both. In this case, the former would need to have appropriately lower gas costs.
 - **Different STARK sizes based on client-side proving time tradeoffs** Smaller proofs take longer to generate. We want larger proofs (cheaper to generate) to be possible, while still encouraging smaller proofs that put less load on the mempool nodes. This can be achieved by making gas cost proportional to proof size (or a related metric, like query count, and even polynomial degree).
 
+The per-dependency charge prices the first hop, where a client establishes its own dependencies before any aggregation has happened. It does not price a recursive round: by the third circuit requirement, the cost of absorbing a nested proof is bounded however many dependencies it covers, so the marginal cost of one more dependency to a node already aggregating is not proportional to the charge. Like the corresponding values in [EIP-8141](./eip-8141.md), these are provisional benchmark targets, expected to be recalibrated against the aggregation implementation as it stabilizes.
+
 ### Why dependency frames may not sit in an atomic batch
 
 Requiring `flags == 0` keeps a dependency verification frame from being a flagged batch member, but leaves it a valid terminator. [EIP-8141](./eip-8141.md) defines an atomic batch as a maximal run `[i, j]` where frames `i` through `j-1` carry `ATOMIC_BATCH_FLAG` and frame `j` does not, and its successor rule excludes only `VERIFY` frames.
@@ -439,6 +449,14 @@ The terminator is the frame at which the batch commits. When a batch fails its r
 
 [EIP-8141](./eip-8141.md) requires a frame receipt per frame, builds the transaction's logs by concatenating them in frame order, and exposes per-frame results through `FRAMEPARAM` `0x05`, `0x0A` and `0x0B`, which read by frame index. Omitting the entry for a frame that does not execute would renumber every later frame's results, on exactly the transactions [Transaction Execution Visibility](#transaction-execution-visibility) invites contracts to walk. EIP-8141's own rationale prices its per-frame cost as covering the receipt sub-entry that each frame adds.
 
+### Why the circuit requirements?
+
+Three properties of the aggregation circuit are load-bearing for the rest of this specification.
+
+Bounded proof size is what allows the proof to ride in the block header without its size scaling with the block's contents. Bounded verification cost is what keeps the cost of validating a block from growing with the number of dependencies that block declares. Bounded absorption cost is what allows a mempool node to broadcast one wrapper per `AGGREGATION_INTERVAL` covering all currently active transactions: a node absorbs its own previous aggregate rather than re-proving its pool, so its per-round cost does not grow with the size of that pool.
+
+A proof covering fewer claims may be cheaper on any of these dimensions. Each requirement asks only for a bound. A circuit without all three does not support the constant-per-peer bandwidth claimed in [Censorship Resistance](#censorship-resistance) or the fixed per-interval overhead claimed above.
+
 ## Backwards Compatibility
 
 This EIP introduces new transaction types and frame modes. It does not modify the behavior of existing transactions. Transactions without signature or STARK verification frames are unaffected.