← Phase 1 / 19 · Delta-Only Algorithm1 Verifier
An engineering efficiency strategy document: there is no need to rerun all old filters like L-value merge, 2-descent, $E'$ descent, and $\mathcal S$ right from the start, because every curve in the old output has already passed the old Algorithm 1. Since there is only one commit from old to current, and the theorem predicate diff of Algorithm 1 has no other loosen/tighten gates, for known old PASS rows, the new membership is exactly equal to the intersection of the "strict-isogeny gate $\land$ $a_3$ gate"—this is a delta-only proof replay, eliminating the need to redo unchanged proof obligations. The input fields are minimized to just three: cremona_label, a3, and isogeny_degrees. The success gate is explicitly defined: inputting the old version's 40,749 curves, the expected PASS=36,687, FAIL=4,062, and it requires outputting a full failure histogram (P_ISOGENY_3/5/7, A3_ABS_3, multi-failure), termed the "first 500K semantic-cause census." The document equally emphasizes what to do upon failure: if the delta-only verifier cannot obtain the official current set, it means at least one of five things (missed semantic differences, different LMFDB release, old and new outputs are not from the same data snapshot, metadata mapping error, or the implementation has unrecorded side effects) is true; at this point, one should stop and not proceed directly to a full replay.
Relationship with other documents, try to use the words from its own document, not my interpretation.
"It should stop at this point, and not proceed directly to full replay." — Excerpt from the end of the "Meaning of failure" paragraph in this text.
Loading...