insertion is overkill for inclusion proofs

[porcuquine]

In thinking through inclusion-proof arities for other reasons, I realized that we don't actually need the insertion gadget. What we did there is clever, especially the hand-optimized constraint for the 8-ary version which sees heavy use. However, fundamentally, 'insertion' proves more than necessary.

Specifically, we are showing that there exist seven (using the 8-ary case as an example) sibling hashes, from which the preimage can be constructed by inserting a known hash at the chosen index. While this is accurate, we only need to show that we know 8 hashes constituting the preimage, and that the one at the chosen index is the one we know. The former is implicit in the latter, even though the latter tells us nothing about the relationship between the preimage and the siblings. That is fine, since that relationship is irrelevant for inclusion proofs, so doesn't need to be proved.

This means that for inclusion proofs of any arity, we could just use simple binary selection — the cost of which scales linearly with the arity (it is n - 1 constraints).

Since 8-ary insertion costs 22 constraints, that means we could save 15 (22 - 7) constraints per inclusion hash, or about 150 per inclusion proof for a 32GiB sector. This is not a huge savings, but I make this note so we don't needlessly perpetuate this pattern in any future proofs which could be rewritten to be simpler and slightly cheaper.

Note that in the general case (without hand-optimization), the cost of insertion goes up with the square of the arity, but the cost of binary selection goes up linearly with the arity. This might suggest that we could use a higher arity for better constraint efficiency in proofs — now that the cost of increasing it is less.

However, this is not true. Given the concrete costs of Poseidon hashing in Neptune, 8-ary inclusion proofs are still optimal. For example, consider a path length of 12 (for inclusion of a tree with 2^12 leaves). For arity N, this requires (12 / log2(N)) * (arity_constraints(N) + N - 1).

N = 2: (12 / 1) * (311 + 1) = 3744
N = 4: (12 / 2) * (377 + 3) = 2280
N = 8: (12 / 3) * (505 + 7) = 2048
N = 16: (12 / 4) * (761 + 15) = 2328

The increased cost of hashes greater than 8 grows faster than the savings from an incremental decrease in number of hashes required — even though the number of constraints per preimage element continues to decrease.

So oct (8-ary) hashes remain optimal. I won't dredge up the previous numbers here, but without Neptune's sparse matrix optimizations, quad (4-ary) hashes were slightly better. So any future proofs using a hash with different costs should perform this analysis again to determine the optimal arity.

I think the reason we took this approach is that it was an incremental change from the historical procedure used for binary inclusion proofs: prove procedural transformation of a partial specification of the preimage into the actual preimage. This framing of the problem is likely due to previous use of conditionally_reverse for that purpose. As noted in the insertion gadget's documentation, insert is a 'generalization of conditionally_reverse'.

However, all we really need is select. Note that select is a generalization of pick.

Also note that pick requires only half the constraints of conditionally_reverse (1 vs 2). In point of fact, the same reframing I describe here could be applied to the binary case also. Since it is only a difference of one constraint, the change would be a very minor optimization in the case of binary hashes. However, it does frame the problem as one to be solved procedurally/constructively, rather than non-deterministically. Then the sins of the father are visited upon the son.

You can read this issue as an extended mea culpa — with some retrospective analysis as partial atonement. Although it seems obvious now, I had not fully processed the idea that inclusion proofs can be thought of as 'traversals' of non-deterministic hash-based data structures. Rather, at the time of writing the Filecoin Proofs, we still thought in terms of 'constructing a root' bottom-up, then checking it for correctness.

Noticing the simplicity which comes from reversing this formulation was one of the triggers that led to implementing Lurk. When considered this way, a Merkle inclusion proof is just 'proof of correct calculation of the nth member of the tree "named" by the root hash' — a slight but significant difference in orientation.

Given how obvious this is in retrospect, it took me a moment to understand why we ever thought otherwise. Consideration of the history of our practice helped me understand the genesis of the mistake. I summarized it here in the interest of unpacking the implications for how we write circuits.

[porcuquine]

but without Neptune's sparse matrix optimizations, quad (4-ary) hashes were slightly better

Note for posterity: the sparse matrix optimizations don't actually affect circuit size. The above was actually a performance consideration related (I believe) to circuit-synthesis time. (The optimizations do affect non-circuit hashing performance significantly, but I don't think this was the issue. If memory serves, 8-ary hashes were theoretically best but presented synthesis problems until the optimizations were in place.)