check_annotations.py

back to table · edit · history · where entries came from · files · download

1306 bytes, as of the version from 2026-10-24 20:04 (current). Recorded here, not run.

"""Check stored equality targets and source ordering for T464.

Run with Python 3: python3 check_annotations.py stored-document.json
The JSON document must be freshly fetched from NumberDB's table API.
"""
import json
from pathlib import Path
import re
import sys

def check(document):
    raw=document['Numbers']
    entries = {(str(r['params']['loops']),str(r['params']['index'])):r for r in raw} if isinstance(raw,list) else {(str(a),str(b)):(v if isinstance(v,dict) else {'number':v}) for a,rs in raw.items() for b,v in rs.items()}
    assert len(entries)==852
    assert list(entries)==sorted(entries,key=lambda k:tuple(map(int,k)))
    assert entries[('1','1')]['number']=='1'
    links=0
    for key,row in entries.items():
        if 'equals' not in row: continue
        target=re.fullmatch(r'HREF\{#(\d+),(\d+)\}',row['equals'])
        assert target, (key,row['equals'])
        earlier=target[1],target[2]
        assert tuple(map(int,earlier))<tuple(map(int,key))
        assert entries[earlier]['number']==row['number']
        links+=1
    assert links==553
    return {'entries':len(entries),'equalities_checked':links,'numeric_parameter_order':True,'one_loop_written_exactly':True}

if __name__=='__main__':
    print(json.dumps(check(json.loads(Path(sys.argv[1]).read_text())),indent=2))