Should a proof survive a guest change? One METHOD_ID, and what we would do the day we are forced off it

[defenwycke]

Hazync proves Bitcoin's history inside a zkVM. Every proof is checked against a METHOD_ID — a
hash committing to the exact guest code that produced it — and the verifier accepts exactly one. So
when the guest changes, the id changes, and every proof made under the old id stops verifying.

That has happened 17 times so far. Today it means a guest change retires the whole back catalogue at
once: a new consensus rule and a two-line speed optimisation cost exactly the same.

We are not changing anything right now, and we are not asking anyone to review a patch. We would
rather argue the plan out in advance than improvise it the day something forces our hand.

The full position is in
docs/METHOD_ID_DURABILITY.md.
The short version:

Method 1 — one id, as today. It has real virtues. "Verified" has exactly one meaning. One build
can produce an accepted proof, and that is the entire trust surface. Nothing is classified, so
nothing can be misclassified. "Your proofs may be retired when the guest improves" is an honest thing
to tell a contributor.

Method 2 — an accepted set, carried the day we are forced to move. A consensus bug, a security
fix, or a speed change worth the disruption will eventually force a new id, and the catalogue is
written off that day regardless. That is the moment it costs nothing extra to also make it the last
time. Two constraints:

1. the set starts at the id being moved to, not at the beginning of the lineage;
2. an id joins only if it is stricter than or equal to those already in it — everything the new
   guest accepts, the existing one would also have accepted.

Soft-fork shaped: new-valid ⊆ old-valid.

Why constraint 1 is load-bearing. The standing objection to any accepted set is that its security
is that of its weakest member, and being append-only it can never withdraw one. Starting at the id
shipping that day makes the weakest member the guest already in production — so the set can never
be weaker than the status quo. It also excludes, by construction rather than by judgement, the 10 of
our 17 ids that predate rules we added in the first three weeks.

The part we are least sure of, stated as such. Most guest changes are neither stricter nor looser
— they are equal, speed work computing the identical statement, and those are exactly the ones
worth preserving proofs across. Equality is the harder claim. One of ours, 1d6c3792, genuinely left
Core's consensus code untouched but relocated three values so the aggregate receives them from
chunks rather than recomputing them. Establishing that it preserved the statement took two same-run
differentials over 8,006 inputs plus a 16-chunk end-to-end on a near-tip block — and within the same
change one relocation was deliberately not made, because getting it wrong would have been fail-open.

"No rule changed" was a finding, not an observation. So we think the relation has to be tested
by differential rather than asserted from a diff — but we do not know what corpus would convince
anyone.

What we would most like answered

1. Is "starts at the id we are moving to, and only ever tightens" sound? It is the load-bearing
   claim and we would rather it failed here than in production.
2. What would convince you a change did not loosen anything? Differential over what corpus, and
   how large? Random blocks are cheap and prove little; our adversarial fixtures are targeted but
   narrow.
3. Is there prior art for upgrading a zk circuit without invalidating the back catalogue?
4. Composition is pinned inside our circuit, so the accepted set would have to live in the
   guest rather than only in the verifier. Does that change your answer to (1)?
5. Is Method 1 simply right? We are not assuming Method 2 wins.

One correction worth having before replying, because we got it wrong ourselves: the soft-fork analogy
does not transfer in its naive form. Bitcoin's version is safe because permissive old nodes are
covered by a strict enforcing majority; a proof system has no such majority, so an accept-everything
set just invites picking the most permissive entry. The two constraints above are what answer that —
without them the analogy misleads.