docs: extract the deployed V5 tag-67 protocol and event ledger - #9
Open
DJBarker87 wants to merge 4 commits into
Open
docs: extract the deployed V5 tag-67 protocol and event ledger#9DJBarker87 wants to merge 4 commits into
DJBarker87 wants to merge 4 commits into
Conversation
Forensic extraction of the interactive protocol actually implemented by the tag-67 production verifier, written so a cryptographer can build a fresh finite-event soundness certificate without reading the tree. Covers the exact transcript (38 absorbs, 42 squeeze sites), 43 candidate events framed as "what false proof passes if this predicate is removed", a dependency graph, the theorem boundaries found by marker search, every challenge and its zero-behaviour, the 19-lane gamma batching, the FRI schedule, and the minimal theorem set. Records three non-events a certificate must not credit: the composite sum is discarded via black_box, selector leastness is not checked on chain, and ZeroMix/ZeroAlpha are declared but never raised. Assumes nothing transfers from the q18/Profile-23 certificate. Part 10 classifies every old term; only the six work thresholds are proved identical. No probability or security level is computed anywhere. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PJ3PcFLjxq9MAVTfoWk5K2
Resolves N5, N6 and half of N7, and corrects P4.4. P4.4 was wrong. The "nonzero QM31 alpha has an inverse" expect at v5_relation_stress.rs:270 sits inside build_v5_relation_stress_tail_for_ initial_claim, which is #[cfg(not(target_os = "solana"))] — a host builder, not the deployed verifier. Confirmed no inverse in either the deployed relation path or WeightAccumulator::fold. Q-ZERO is therefore purely an algebraic question, with no panic or liveness component. N6 resolved: v5_reserved_tail_is_zero reads 400 bytes as 50 LE u64 words and rejects any nonzero word. A LE u64 is zero iff its eight bytes are, and 400 = 50*8 exactly under a pinned length check, so the predicate is exactly byte-wise all-zero. E05 needs no extra lemma. N5 resolved, and it changes the picture: "four opening points" is a misnomer. Claims 0-2 are multilinear evaluations at z, successor(z) and xor12(z); claim 3 is a covector dot product, not an evaluation at any point. The gamma batch weights all four positionally, which is recorded as new open question Q-FUNC. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PJ3PcFLjxq9MAVTfoWk5K2
My N3 was a false negative. I searched for a certificate JSON and a certificates/ directory and missed nine Lean files (~5,400 lines) under AspisFormal/AspisFormal/ that address V5 hiding directly. No sorry, no native_decide. What they establish is narrower than their existence suggests, and the correction cuts the other way from a reassurance: - V5ConditionalHidingCapstoneV3 proves conditional_complete_joint_hiding_v3 for an abstract model, and states in its own header that it must not be cited as a deployed zero-knowledge proof. Nine UnmetDeployment items are Prop definitions, never theorems. - V5ComponentBCorrelatedResidualCoverage proves a NEGATIVE: applicable_schedule_universal_rank76_is_false. A universal rank-76 coverage theorem is impossible without an additional point-rejection predicate. The counterexample sits at the Boolean row976Point under Component A's real sampleQueries schedule with distinct fibres, where the residual map has rank <= 73. - The obstruction survives every nonzero eta, so the runtime nonzero-eta sampler does not rescue it. It is explicitly not yet a witness attack. Records the decisive follow-up as Q-GOOD-RANK: the deployed verifier does have a point-rejection predicate (the GoodA/GoodB gate), but nothing in the tree links it to row976Point. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PJ3PcFLjxq9MAVTfoWk5K2
…rexample Executed the deployed gate (candidate_is_good / evaluate_candidate, built --features no-entrypoint) on the exact Lean counterexample inputs: the Boolean row976Point and Component A's sampleQueries schedule. candidate_is_good(row976Point, sampleQueries) = Some(false) Controls make the result meaningful rather than incidental: random points under sampleQueries[0..17] 2000/2000 good row976Point under random q18 schedules 0/2000 good random point + random schedule 2000/2000 good random BOOLEAN point + random schedule 0/2000 good The counterexample's own schedule accepts every random point tried, so the rejection is a property of the point, and it generalises to the whole Boolean class. Attribution over 500 trials: det GoodA and det GoodB both vanish every time, independent of schedule. So the "additional point-rejection predicate" that applicable_schedule_universal_rank76_is_false says a universal rank-76 theorem requires does exist in the deployed verifier, and it rejects the obstruction direction of V5ComponentBLegalWitnessDifference. This is computation, not proof, and it is not deployed hiding: it removes one counterexample class, says nothing about non-Boolean Good-accepted points, and leaves the capstone's eight UnmetDeployment items untouched. The outstanding obligation is now one stated lemma: GoodA and GoodB are singular at every Boolean point under every injective q18 schedule. Also records that cargo build fails at HEAD — Cargo.toml lists six workspace members under protocol/, never committed and not gitignored. Co-Authored-By: Claude Opus 5 <noreply@anthropic.com> Claude-Session: https://claude.ai/code/session_01PJ3PcFLjxq9MAVTfoWk5K2
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Forensic extraction of the interactive protocol actually implemented by the
tag-67 production verifier, written so a cryptographer can build a fresh
finite-event soundness certificate without reading the tree.
Covers the exact transcript (38 absorbs, 42 squeeze sites), 43 candidate
events framed as "what false proof passes if this predicate is removed",
a dependency graph, the theorem boundaries found by marker search, every
challenge and its zero-behaviour, the 19-lane gamma batching, the FRI
schedule, and the minimal theorem set.
Records three non-events a certificate must not credit: the composite sum
is discarded via black_box, selector leastness is not checked on chain,
and ZeroMix/ZeroAlpha are declared but never raised.
Assumes nothing transfers from the q18/Profile-23 certificate. Part 10
classifies every old term; only the six work thresholds are proved
identical. No probability or security level is computed anywhere.