Skip to content
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
29 changes: 26 additions & 3 deletions research/arxiv_tnf/verify_numbers.py
Original file line number Diff line number Diff line change
Expand Up @@ -39,6 +39,26 @@ def check(label, got, want, tol=0.02):
bad += 1


def field(d, key, label):
"""Read a cited field, or report its absence as a divergence.

A record that does not carry a field the paper cites is not a crash and not
a pass. Crashing is worse than it looks: this script died on the first
missing key, so every check below it -- including the whole W991 competitor
block -- never ran at all, and a partial verification exited looking like a
finished one. Returning None instead would route the value into check()'s
"не вычислено" branch, which increments neither counter and leaves the exit
code at zero, so a missing measurement would read exactly like a satisfied
one. Count it against the run.
"""
global bad
if not isinstance(d, dict) or key not in d:
print(f" РАСХОЖДЕНИЕ {label}: запись не содержит поля {key!r}")
bad += 1
return None
return d[key]


def paired(d, task, a, b, key="formats"):
p = d["tasks"][task][key] if key in d["tasks"][task] else d["tasks"][task]
x = np.array(p[a]); y = np.array(p[b])
Expand Down Expand Up @@ -960,9 +980,12 @@ def drop(d, task, fmt, key="formats", base="baseline"):
"same word both times" in d4["repeatability"], True, tol=0)
check("dot4: остальное названо",
"still placing" in d4["status"], True, tol=0)
check("чтения канонизированы", len(cf["die_reads_canonical"]), 6, tol=0)
check("прерванное названо, а не скрыто",
"killed" in cf["what_was_given_up_for_it"], True, tol=0)
_canon = field(cf, "die_reads_canonical", "чтения канонизированы")
if _canon is not None:
check("чтения канонизированы", len(_canon), 6, tol=0)
_given = field(cf, "what_was_given_up_for_it", "прерванное названо, а не скрыто")
if _given is not None:
check("прерванное названо, а не скрыто", "killed" in _given, True, tol=0)

# W991: the competitor table, computed from the committed oracles.
cm = rec("compare_w991.json")
Expand Down
1 change: 1 addition & 0 deletions research/gate_status_baseline.json
Original file line number Diff line number Diff line change
Expand Up @@ -78,6 +78,7 @@
"verify_lucas_exact.py": "clean",
"verify_lucas_product.py": "clean",
"verify_negation_invariant.py": "clean",
"verify_numbers.py": "findings",
"verify_oracle_exactness.py": "clean",
"verify_phi_rule.py": "clean",
"verify_quire_associativity.py": "clean",
Expand Down
11 changes: 10 additions & 1 deletion research/gate_status_ratchet.py
Original file line number Diff line number Diff line change
Expand Up @@ -99,9 +99,18 @@ def _block_gates():


def collect(timeout, jobs):
# research/arxiv_tnf/verify_numbers.py is named for one of the three roles
# above and re-derives every headline number in the paper, but it sits one
# directory down and so was never collected. Nothing else ran it either --
# not this ratchet, not gate-ratchet.yml, not paper-numbers.yml -- and it
# had been dying on a KeyError, which meant the whole W991 competitor block
# was never checked by anything. A script excluded by where it happens to
# live is exactly the implicit exclusion this module's docstring refuses to
# have; the skip list above is the auditable way to leave a gate out.
paths = sorted(glob.glob(os.path.join(HERE, "audit_*.py"))
+ glob.glob(os.path.join(HERE, "witness_*.py"))
+ glob.glob(os.path.join(HERE, "verify_*.py")))
+ glob.glob(os.path.join(HERE, "verify_*.py"))
+ glob.glob(os.path.join(HERE, "arxiv_tnf", "verify_*.py")))
todo = [p for p in paths if os.path.basename(p) not in G.SKIP]
todo += _block_gates()
out = {}
Expand Down
Loading