Certify exact distances for six previously unresolved PBB codes - #2
Certify exact distances for six previously unresolved PBB codes#2Jphilbrick10 wants to merge 8 commits into
Conversation
Six entries marked d_is_exact:false are certified exact. IBM's published d is UNCHANGED on all six -- this confirms the existing values rather than revising them. 362 rows untouched. logicals_optimal / logicals_incumbent / logicals_failed are deliberately left as the MILP left them: the method bounds the minimum weight over all of N(S)\S in a single sweep and does not resolve logical operators individually. Evidence: two completed replicas per closure on provably distinct information sets; 9_6_0172 additionally reproduced by an independently implemented runner (582 shards, 49,256,436,180 candidates, zero violations). See the PR body for the lower-bound disclosure and three questions for maintainers.
|
|
|
@CLAassistant check |
…witnesses * Every row's d_exactness_source.release now names the actual immutable bundle, oneq-ibm-distance-closures-v1.0.1 (the previous string named the REVOKED v1.0.0 -- and misspelled it -- precisely the provenance drift this contribution is supposed to prevent; caught by external review). * artifact_sha256 pinned (ed04f1b1...); issuer public-key prefix included. * Witness supports are now INLINE per row (|support| == d, checkable from the visible diff -- a hash alone proves identity only after the object is available). * Per-set enumeration data added: pivot_qubits, deficiency, contribution, levels_swept per information set, so the candidate totals and the bound sum(max(0, p+1-deficiency)) recompute from the row alone. * Replica wording tightened: distinct_information_set_replicas (2 per code) is now separate from independent_runner_reproductions (1 for 9_6_0172, 0 elsewhere) -- distinct information sets are not independent implementations. * exactness_verified_at / exactness_time_s_per_replica added; the historical verified_at / time_s / MILP fields remain untouched, with an explicit note deferring field-ownership semantics to the maintainers. * lower_bound_is_machine_checkable: false stated per row. A 69-check validation report (row parity, six-row scope, d unchanged, flag coherence, bound + candidate recomputation per set, hash formats, witness sizes, replica distinctness) accompanies this PR as a comment.
|
Validation report for |
…lease https://github.com/coherence-energy-labs/oneq-distance-closures/releases/tag/v1.0.1 Archive SHA-256 unchanged (ed04f1b1...) -- the bundle published is byte-identical to the one every row already pinned.
|
The evidence is now publicly published: https://github.com/coherence-energy-labs/oneq-distance-closures (release v1.0.1, archive SHA-256 |
…radiction
Second external review found three defects in the metadata; all fixed here.
The verifier fail-open it also found is fixed in the evidence repository and
described below.
1. ISSUER FIELD WAS MALFORMED, and it was ours. Every row carried
"issuer_pubkey_prefix": "{'schema': 'oneq" -- the first sixteen characters
of a Python dict repr. Our enrichment script read `pubkey_hex` where the
registry field is `pubkey`, and an `or str(issuers)[:16]` fallback caught
the miss silently. Replaced with the real values, both of them:
"issuer_pubkey": "1eace2ebc1edd8795ad5d499f1d4df40dd4e3a8269ed411b3b52d6633afcf664"
"issuer_fingerprint": "1eace2ebc1edd879"
The validator now checks 64-hex form, fingerprint-prefixes-pubkey, presence
in the ACTIVE set of the release's ISSUERS.json, and absence from the
revoked list. The first 69 checks passed this row because none of them
looked at the field: a validator tests only what it is told to test, and
the gap was in the checklist, not in the arithmetic. Now 103 checks.
2. WITNESS ENCODING DECLARED. Each row states that witness_support entries are
[qubit_index, pauli_code] with 1=X, 2=Z, 3=Y. A visible witness is only
self-describing once its encoding is written down.
3. d_method CONTRADICTION RESOLVED. The note claimed d_method was "deliberately
untouched" while the diff changed it. Convention now stated explicitly
(Option A): d_method records the method that ESTABLISHED EXACTNESS;
verified_at, time_s and the MILP-specific fields remain historical. The
maintainers may prefer the opposite (question 7) -- the row now says which
convention it uses instead of being ambiguous.
VERIFIER FAIL-OPEN (evidence repo, more serious). `_trusted_pubkeys()` returned
an empty set for a missing OR malformed ISSUERS.json, and the caller read
`if trusted and key not in trusted` -- so an empty registry DISABLED issuer
pinning and the certificate was verified against the key inside itself.
Deleting a file bought an attacker the trust the file existed to withhold.
Now fails CLOSED: no valid registry -> refuse; revoked key -> refuse; unpinned
key -> refuse. The loader validates schema, 64-hex keys, active/revoked
disjointness and duplicates, and is fail-closed on unparseable input. Fixed in
all seven live copies. Proven both directions: valid bundle still 6/6
PROMOTABLE; with ISSUERS.json deleted, 0/6.
The stranger challenge now ships SEVEN forgeries: the original four plus
missing / malformed / revoked issuer registry. Self-tested green -- VALID
accepted, 7/7 rejected.
|
Updated validation: 103 checks, all passing (was 69 -- the new checks are the issuer-registry ones whose absence let a malformed issuer field through). Rerunnable by anyone: |
…n verifier Self-audit after the trust-root fix caught the gap the fix itself opened. The verifier was corrected in the repository DIRECTORY, but the PUBLISHED ARCHIVE -- the artifact whose SHA-256 these rows pin -- still contained the vulnerable code. One version number, two different contents: the exact provenance drift this contribution exists to prevent, committed while fixing a security defect. An immutable release is superseded, never edited. All six rows now cite: release: oneq-ibm-distance-closures-v1.0.2 artifact_sha256: 4ac50d664ca066588ec5122b1c1239eeb57a35405d8f9962d572b21b8892cdc6 artifact_url: .../releases/tag/v1.0.2 Verified end to end: the published archive was downloaded, its hash matches the pin byte for byte, its bundled verifier is confirmed fail-closed, and running it fresh reports 6/6 PROMOTABLE. v1.0.1 stays downloadable for provenance and is titled SUPERSEDED -- it must not be used to verify. The certificates are unchanged and were never affected. 103/103 validation checks pass against v1.0.2.
|
Correction: the rows now cite v1.0.2, not v1.0.1. A self-audit after the trust-root fix found that the fix had been applied to the repository directory while the published archive — the artifact whose SHA-256 these rows pin — still contained the fail-open verifier. One version number, two different contents. That is precisely the provenance drift this contribution exists to prevent, and it was introduced while fixing a security defect. An immutable release is superseded, not edited:
Verified end to end just now: the published archive downloaded, hash matched the pin byte for byte, bundled verifier confirmed fail-closed, fresh run reports 6/6 PROMOTABLE. The certificates are unchanged and were never affected — they always carried the correct active signing key. 103/103 validation checks pass against v1.0.2. |
…clone An external stranger audit ran the challenge as a newcomer would and it FAILED -- VALID_accepted: false -- because the tree pin was computed over CRLF bytes while git stores LF, so no clean clone could ever match. 57 of 57 files also failed the repo's own SHA256SUMS, the v1.0.2 archive failed its own manifest on two files (one the verifier), CLAIMS.json self-identified as v1.0.1, and cryptography was undeclared. v1.0.3 fixes all of it and, critically, VALIDATES THE PIN FROM A FRESH CLONE before publishing it -- the step whose absence caused three consecutive releases to ship artifacts that contradicted their own descriptions. CI now clean-clones and checks manifest, verifier, challenge, pin and archive parity on every push. The mathematics was never affected: the auditor independently re-verified every witness with their own GF(2) implementation across both replicas of all six codes, plus the candidate arithmetic to the digit. What was broken was the machinery for checking it.
|
Final correction — v1.0.3, and CI so this is the last one. A full external stranger audit (clean clone, documented commands only, independent GF(2) re-verification) found the verification layer broken in the place we invited you to look first: v1.0.3 — https://github.com/coherence-energy-labs/oneq-distance-closures/releases/tag/v1.0.3 · SHA-256 Verified from a fresh clone, which is the step whose absence caused all of this: 58/58 manifest OK, challenge The mathematics was never affected. The auditor re-derived every witness with their own linear algebra across both replicas of all six codes, and the candidate counts to the digit — all passed. What was broken was the machinery for checking it, and it is fixed. The six rows now cite v1.0.3; 103/103 checks pass. No further corrections are expected from this lane. |
…d download The rows previously pinned 8df0c8a6, and that build no longer existed: the v1.0.3 ASSET was rebuilt three times under its own tag as CI caught successive defects. The first build had already been referenced by these rows, so replacing it in place broke the rule this project states in its own commit messages -- an immutable release is superseded, never edited. A maintainer verifying the pinned hash would have downloaded bytes available nowhere. v1.0.4 was minted once, uploaded once AFTER CI went green, and confirmed from a fresh clone and a fresh download: pin 94b455ea matches the published asset byte-for-byte, manifest 58/58, challenge ALL CHECKS AS EXPECTED. Two hardening fixes travel with it. validate_pr_rows.py now compares each row's artifact_sha256 against the PUBLISHED pin rather than checking hex shape alone -- the absence of that single check is why 103/103 passed while the rows pointed at vanished bytes -- and its expected-release string is derived from the bundle path rather than hardcoded, which is the same drift one level up. 115/115 checks pass.
|
Current state — v1.0.4, and this is the last correction comment. The previous pin referred to a build that no longer existed: v1.0.3's asset was rebuilt three times under its own tag as CI caught successive defects, after these rows had already referenced the first build. That broke the rule this project states in its own commit messages — an immutable release is superseded, never edited — so v1.0.4 was minted once, uploaded once after CI went green, and confirmed from a fresh clone and a fresh download before these rows were touched.
Two hardening fixes travel with it, both closing the class rather than the instance: The PR body has been updated to a single coherent description; the corrections history lives in the commits. The mathematics has been untouched throughout. The certificates have never changed, and an external auditor independently re-verified every witness with their own GF(2) implementation across both replicas of all six codes, plus the candidate arithmetic to the digit. Every defect found in three review rounds was in the machinery for checking the result, never in the result. That machinery is now watched by CI that clean-clones on every push. Ready for maintainer review; the seven schema questions in the body are the only open items. |
This PR previously stated that the lower bound is an exhaustive-absence claim with no succinct machine-checkable proof object, verifiable only by re-executing our enumeration. That is no longer true, and each row now carries the certificate rather than the caveat. For every closure, an LRAT proof of UNSAT for 'a logical operator of qubit weight <= d-1 exists', produced by CaDiCaL and checked by lrat-check from the drat-trim project -- a different program by different authors. All twelve proofs report 'c VERIFIED'; each was also checked by hand. phase2_65 n=108 d=8 18.2s phase2_64 n=108 d=8 39.0s 12_6_0201 n=144 d=8 321.4s 9_6_0172 n=108 d=10 615.9s 12_6_0199 n=144 d=12 399.2s 0571f767.. n=108 d=10 1524.1s Together with the inline witness at weight d, this proves d exactly with no appeal to re-running anything of ours. For scale, 12_6_0199 needed 8.15e12 enumerated candidates and 6.4 GPU-hours per replica for the same statement. Encoding: XOR chains for commutation, an OR over logical representatives for non-membership in S, sequential-counter cardinality for the weight bound, and two orbit-anchored instances (the translation group acts freely block-wise, so every nonzero operator has a translate touching block-1 qubit 0 or lies in block 2 touching block-2 qubit 0). BOTH anchors UNSAT proves absence. Validated before being believed: SAT at W=d, with the model re-verified outside the solver, proves the encoding can still FIND a logical -- a one-sided test would be passed by an encoding that is UNSAT for everything -- and UNSAT at W=d-1 agrees with the enumeration. A seeded-counterexample suite separately proves the search classifies a real logical as logical and a real stabilizer as a stabilizer, defending the one branch whose failure would silently inflate a bound. Evidence: release v1.0.5, sha256 e3b5cf0c..., certificates_lrat/ ships the CNFs (5 MB) and every proof's SHA-256; the 17.3 GB of proofs are regenerable in minutes, which is a stronger check than re-reading bytes we produced. 115/115 validation checks pass.
|
The lower bounds are now machine-checkable. This PR previously said the lower bound is an exhaustive-absence claim with no succinct proof object, verifiable only by re-executing our enumeration. That sentence has been replaced by the certificates. Each closure ships an LRAT proof of UNSAT for "a logical operator of qubit weight ≤ d−1 exists", produced by CaDiCaL and checked by
For scale, Evidence: v1.0.5, Two honest notes. Before believing any of this we fixed two defects in that lane — a substring test that read 115/115 row checks pass. Ready for review. |
3 participants
Certify exact distances for six previously unresolved PBB codes
This PR updates six entries currently marked
d_is_exact: false. For each entry,exhaustive qubit-paired Zimmermann searches found no nontrivial logical operator
below the stated distance and produced an explicit logical witness at the stated
distance. Each closure was executed twice using deterministically reconstructible,
provably distinct information sets.
One entry,
9_6_0172, was additionally reproduced by a separately implementedrunner that does not invoke the production search or certification code. It
rebuilt the information sets from recorded pivots, recomputed the deficiencies,
and exhaustively checked all 49,256,436,180 candidates across 582 shards.
IBM's published
dis unchanged on all six. This confirms the existingvalues; it revises none of them. 362 rows are untouched.
The six rows
9_6_0172426b9d530929e62e0571f767860296530571f76786029653phase2_64d8f7c04aec559961phase2_65d9457e4965aaa67212_6_01997989eece4ce9c3cd12_6_0201a8879ca668587ffaMethod
The two symplectic columns of each physical qubit are kept adjacent through row
reduction, so every pivot qubit owns the three non-identity options {X, Z, Y}
directly. Two consequences: the bound applies to qubit weight without the
factor-2 slack column enumeration incurs (a Y is one qubit, two columns); and
Zimmermann's rank-deficient refinement admits a second information set whose
deficiency is measured from the reduction rather than assumed:
d_methodis set to a new value,qubit_paired_zimmermann. Reusingdeep_milpor
milp_exactwould attribute the result to a solver that did not produce it --happy to rename if you prefer a different convention.
Evidence (public, immutable, CI-guarded)
Release: https://github.com/coherence-energy-labs/oneq-distance-closures/releases/tag/v1.0.5
Archive:
oneq-ibm-distance-closures-v1.0.5.tar.gzSHA-256:
e3b5cf0ce7e61c1d17411321e51b7d9faf9054f44285b0f10efdf9cac4fc9778— identical to theartifact_sha256pinned in all six rows.Verify (~2 minutes):
Revalidate these six rows against your own checkout (115 checks — six-row
scope,
dunchanged, bound and candidate recomputation, hash formats, witnesssizes, replica distinctness, issuer pinning, and each row's pin against the
published archive):
Stranger Verification Challenge — the VALID bundle plus seven deliberate
forgeries (inflated bound, altered information set, substituted witness,
downgraded verifier floor, and missing / malformed / revoked issuer registry).
challenge/verify.shaccepts the valid bundle and rejects all seven. A GitHubAction clean-clones and runs manifest, verifier, challenge, tree pin and
archive-parity checks on every push, so validation never happens only on the
machine where an artifact was authored.
Lower bounds now carry machine-checkable certificates
An earlier revision of this PR said the lower bound has no succinct
machine-checkable proof object and requires re-execution. That is no longer
true, and the change is worth stating precisely.
Each closure now ships an LRAT proof of UNSAT for the statement "there
exists a logical operator of qubit weight ≤ d−1", produced by
CaDiCaL and checked by
lrat-checkfrom the drat-trim project — a
different program by different authors. Together with the inline witness at
weight d, this proves d exactly without appeal to re-running our
enumeration.
phase2_64phase2_6512_6_020112_6_01999_6_0172For scale:
12_6_0199required 8.15 × 10¹² enumerated candidates and ~6.4GPU-hours per replica. The certificate is 399 seconds of solving and minutes
of checking.
Encoding
Variables
x_q, z_qper qubit, weightw_q = x_q ∨ z_q.v ∈ N(S)): XOR chain per stabilizer row.v ∉ S):vmust anticommute with at least onelogical representative —
v ∈ N(S)lies inSiff it commutes with everylogical.
Σ w_q ≤ W, sequential-counter cardinality encoding.every nonzero operator has a translate touching block-1 qubit 0, or lies in
block 2 and touches block-2 qubit 0. Two anchored instances; both UNSAT
⇒ no operator exists.
How to check it yourself
evidence/lrat_publishable/in the release ships the CNFs (3.6 MB total)and the SHA-256 of every proof. The proofs themselves (8.76 GB) are not
shipped — regenerating them is fast and is a stronger check than re-reading our
bytes:
What this does not claim
The certificate proves no logical of qubit weight ≤ d−1 exists for the
reconstructed code, given the encoding above. It does not remove the need to
trust that the code was reconstructed faithfully from the catalogue row — which
is why
code_input_hashis recorded and the reconstruction is re-derived bythe verifier. Two defects in this lane were found and fixed before any of these
numbers were believed: a substring test that read
c NOT VERIFIEDas verified,and binary-format LRAT that the checker never parsed. The encoding was then
validated in both directions — SAT at W = d with the model re-verified
outside the solver, UNSAT at W = d−1 — because a one-sided test would be passed
by an encoding that is UNSAT for everything.
Witness encoding
witness_supportentries are[qubit_index, pauli_code]with1 = X,2 = Z,3 = Y;|support|equalsdby construction.Field conventions used (maintainers may prefer otherwise)
d_methodrecords the method that established exactness;verified_at,time_sand the MILP-specific fields remain historical, and theexactness campaign has its own
exactness_verified_at/exactness_time_s_per_replica.logicals_optimal/logicals_incumbent/logicals_failedare untouched:this proof is not per-logical, and rewriting them would misrepresent the
MILP campaign.
publication_qualityleftfalsepending your ruling.distinct_information_set_replicas, kept separate fromindependent_runner_reproductions(1 for9_6_0172, 0 elsewhere).Open questions for maintainers
d_is_exactpermit a non-per-logical proof of this form?logicals_*fields?d_exactness_sourceobject acceptable, or do you prefer asidecar file or an external reference?
publication_qualitybecometruefor exactness established this way?verified_at/time_sdescribe the new run or stay historical?d_methoddescribe the method that originally foundd, or themethod that proved exactness?
Corrections made during review
Two external review rounds found real defects, all fixed here rather than
argued with: the rows originally cited the revoked v1.0.0 evidence bundle;
witnesses were hash-only; per-set enumeration data was missing; an issuer
field carried a malformed
str(dict)[:16]value; and the bundled verifierfailed open when
ISSUERS.jsonwas missing or malformed -- it now refuses,proven by three permanent challenge cases. The validation suite grew from 69
to 103 checks, including the issuer checks whose absence let the malformed
field through.
Two external review rounds and one full stranger audit shaped this submission.
The auditor independently re-verified every witness with their own GF(2)
implementation and the candidate arithmetic to the digit -- both held. The
defects they found were in the verification machinery, not the mathematics:
a revoked release reference, hash-only witnesses, a malformed issuer field, a
verifier that failed open on a damaged trust registry, and a tree-hash pin that
no clean clone could reproduce. All corrected in v1.0.5, which is validated
from a fresh clone and guarded by CI that clean-clones on every push.