validate_evidence.py

#!/usr/bin/env python3
import hashlib,json,os,subprocess,sys,tempfile
from pathlib import Path
r=Path(__file__).resolve().parent
c=json.loads((r/'official_claims.json').read_text());d=json.loads((r/'outputs/results.json').read_text());q=json.loads((r/'replay_a/results.json').read_text());m=json.loads((r/'EVIDENCE_MATRIX.json').read_text());a=json.loads((r/'final_assessment.json').read_text())
assert c==['The paper formulates formal problem-solving as a deterministic Markov decision process and implements FPS inside formal theorem proving environments (Section 3.1).', 'Deductive Formal Problem-Solving decouples forward answer construction from optional backward proof validation for find-all problems (Figure 2).', 'FPS soundness is proved: any direct answer produced by FPS satisfies the formal problem predicate (Theorem 3.6).', "D-FPS completeness and soundness for find-all problems are stated as formal theorems under the paper's conditions (Theorems 3.8 and 3.9).", 'The benchmark suite consists of FormalMath500, MiniF2F-Solving, and PutnamBench-Solving, constructed from informal and theorem-proving math benchmarks (Section 4.2).', 'The strongest evaluated baselines solve at most 23.77% of FormalMath500, 27.47% of MiniF2F-Solving, and 0.31% of PutnamBench-Solving (Table 1).'] and len(c)==6 and d==q and d['summary']=={'all_passed':True,'passed':21,'total':21}
assert all(g['passed'] for g in d['gates']) and m['release_quality_gate']['expected_verified_points']==12
assert [x['assessment'] for x in m['claims']]==['verified']*6 and a['conservative_points']==12 and a['scientific_replay_byte_identical']
pins={'source/paper.pdf':'bba3d0293dda50476bd07d7dab987d4ed5ded4fa21132837f35c4feff72403e3', 'source/paper-source.tar':'b08c84c35b90d0128fc6ff512b60b07ead29ef6de847c8834948df660b00034a', 'source/official-current.tar.gz':'b144a1051b840f4b7f59428151ba8bf6f27e7665a3b9f950d165c39055ef2315', 'source/official-initial.tar.gz':'cef6b9340b797355ab6e3fb425ee02a1e6c2cc7b76eff6fc77d79bf6e99753fe'}
for name,digest in pins.items():assert hashlib.sha256((r/name).read_bytes()).hexdigest()==digest,name
text='\n'.join(p.read_text(errors='ignore') for p in r.rglob('*') if p.is_file() and p.suffix in {'.md','.json','.txt','.html','.tex','.lean','.py'})
assert all(claim in text for claim in c) and 'paper-hgMZraPlSv' in text
with tempfile.TemporaryDirectory() as t:
 fresh=Path(t)/'fresh';env={**os.environ,'PYTHONDONTWRITEBYTECODE':'1','PYTHONHASHSEED':'0','PYTHONWARNINGS':'error'}
 subprocess.run([sys.executable,'-W','error',str(r/'reproduce.py'),'--paper-pdf',str(r/'source/paper.pdf'),'--paper-source',str(r/'source/paper-source.tar'),'--current-archive',str(r/'source/official-current.tar.gz'),'--initial-archive',str(r/'source/official-initial.tar.gz'),'--out',str(fresh)],check=True,env=env,stdout=subprocess.DEVNULL)
 assert (fresh/'results.json').read_bytes()==(r/'outputs/results.json').read_bytes()
print('evidence validated: six exact claims, 21/21 gates, full export, exact Table-1 rescoring, paired byte-identical replay')