#!/usr/bin/env python3 """Bundle source hashes, static proof metadata and a documentary claim report. No source code or proof is executed. Uses reviewed local research outputs and a clean pinned Git checkout. Creates a fresh directory and preserves partial output on errors rather than deleting or overwriting anything. """ import argparse import hashlib import json import subprocess from datetime import datetime, timezone from pathlib import Path from audit_claim_contract import COMMIT, CONTRACTS, audit ROOT = Path(__file__).resolve().parents[2] BASE = ROOT/'research/snapshots/2026-10-08-baseline' def file_record(path, display): digest = hashlib.sha256() with path.open('rb') as stream: for chunk in iter(lambda: stream.read(1_048_576), b''): digest.update(chunk) return dict(path=display, sha256=digest.hexdigest(), bytes=path.stat().st_size) def main(): parser = argparse.ArgumentParser(description=__doc__) parser.add_argument('--source', type=Path, default=ROOT/'source/openai-math') parser.add_argument('--claim', type=Path, required=True) parser.add_argument('--output-directory', type=Path, required=True) args = parser.parse_args() source = args.source.resolve() if args.output_directory.exists(): raise FileExistsError('Output directory already exists; use a fresh edition') head = subprocess.run(['git','-C',str(source),'rev-parse','HEAD'], check=True, capture_output=True, text=True).stdout.strip() status = subprocess.run(['git','-C',str(source),'status','--porcelain','--untracked-files=normal'], check=True, capture_output=True, text=True).stdout if head != COMMIT or status: raise ValueError('Use the reviewed commit in a clean checkout; preserve and review other versions separately') inventory = json.loads((BASE/'inventory.json').read_text()) preflight = json.loads((BASE/'proof_preflight.json').read_text()) withdrawal = json.loads((BASE/'withdrawal-impact-2026-10-09-v1.json').read_text()) if inventory['metadata']['source_commit'] != head or preflight['source_commit'] != head: raise ValueError('Static reports do not match the reviewed source revision') claim = json.loads(args.claim.read_text()) claim_report = audit(claim) paths = {'README.md','CONTENTS.md','history.md','overview.tex','lean/lean-toolchain'} manuscript_paths = set() scope_paths = set() for family in inventory['families']: if family['lean_scope_path']: scope_paths.add(family['lean_scope_path']) for paper in family['papers']: manuscript_paths.add(paper['path']) paths.add(paper['readme_path']) paths |= manuscript_paths | scope_paths for config in preflight['configs']: paths.add(config['config']) for module in config['modules'].values(): paths.add(module['path']) for notice in withdrawal['notices']: paths.add(notice['notice_path']) source_files = [] for relative in sorted(paths): path = (source/relative).resolve() if not path.is_relative_to(source) or not path.is_file(): raise ValueError(f'Invalid source reference: {relative}') source_files.append(file_record(path, relative)) research_inputs = [BASE/'inventory.json', BASE/'proof_preflight.json', BASE/'withdrawal-impact-2026-10-09-v1.json', args.claim.resolve(), Path(__file__).resolve(), ROOT/'research/tools/audit_claim_contract.py'] # Hashing a clean checkout identifies bytes; it does not authenticate the # publisher or independently reproduce the Git object tree or any proof. manifest = dict(source_repository='https://github.com/openai/math', source_commit=head, generated_at_utc=datetime.now(timezone.utc).isoformat(), counts=dict(families=len(inventory['families']), manuscripts=len(manuscript_paths), selected_scope_documents=len(scope_paths), hashed_source_files=len(source_files)), source_files=source_files, research_inputs=[file_record(p, str(p)) for p in research_inputs], limitations=['SHA-256 identifies the local bytes only; no independent publisher authentication', 'Static preflight is reused; no source or proof code is executed', 'Withdrawal edges are explicit notices, not a complete theorem-dependency graph', 'Documentary linter trusts supplied statuses and references; evidence contents are not verified'], independent_proof_verification='not_run') external = [c['config'] for c in preflight['configs'] if c['external_kernel_enabled']] report = f'''# Evidence-platform prototype report Source revision `{head}`. This concrete offline report joins source fingerprints, static checker metadata, explicit withdrawal dependencies and one illustrative operational claim. It is not an independently checked proof or a completed ten-claim buyer pilot. ## Source and checker evidence - {len(inventory['families'])} families and {len(manuscript_paths)} unique manuscripts inventoried. - {len(scope_paths)} selected family-scope documents located; existence is not proof verification. - {len(source_files)} source files fingerprinted in [manifest.json](manifest.json). - {len(preflight['configs'])} checker configurations scanned in the preserved preflight; no trusted checker executed. - {len(external)} configurations enable an external kernel: {', '.join(external)}. - Independent proof verification: **not run**. ## Explicit corrections and dependencies The preserved withdrawal scan found {len(withdrawal['notices'])} proof-withdrawal notices and {len(withdrawal['edges'])} explicitly named dependency edges. A withdrawn proof does not establish that its mathematical statement is false. Notice dates and the repository history heading differ and must remain separate. ''' for notice in withdrawal['notices']: url = f'https://github.com/openai/math/blob/{head}/{notice["notice_path"]}' report += f'- [{notice["title"]}]({url}): notice says {notice["notice_date"]}; proof withdrawn.\n' report += '\n## Illustrative software claim\n\n' report += f'Claim `{claim_report["claim_id"]}` uses contract `{claim_report["contract_id"]}`. The linter reports {claim_report["documentary_gap_count"]} documentary gaps. [Full claim audit](claim-audit.json). Supplied references and statuses are unverified.\n\n' for issue in claim_report['issues']: report += f'- **{issue["code"]}**: {issue["message"]}\n' report += f'\nThe registry currently has {len(CONTRACTS)} curated source/model contracts. Complete documentation is not mathematical applicability certification. The next implementation work is precise section/line source anchors and an independently executed proof-run adapter; the next business test is a measured expert workflow comparison.\n' args.output_directory.mkdir(parents=True, exist_ok=False) archive=args.output_directory/'input-archive' archive.mkdir(exist_ok=False) archived_inputs=[] for index, entry in enumerate(manifest['research_inputs']): original=Path(entry['path']) contents=original.read_bytes() if hashlib.sha256(contents).hexdigest()!=entry['sha256']: raise ValueError('A research input changed during bundle creation; preserve this partial output and use a fresh edition') saved=archive/f'{index:02d}-{original.name}' with saved.open('xb') as stream: stream.write(contents) archived_inputs.append(dict(file_record(saved,str(saved.resolve())),original_path=str(original))) manifest['archived_research_inputs']=archived_inputs report+='\n## Preserved report inputs\n\nAll six research inputs, including the exact linter and bundle generator, are copied into [input-archive](input-archive). Their byte hashes and original paths are retained in the manifest. These snapshots remain inert reference material; no archived source or proof code is executed. Later tool edits do not replace this report\'s inputs.\n' for name, value in [('manifest.json',manifest), ('claim-audit.json',claim_report), ('curated-contracts.json',dict(source_commit=head, contracts=CONTRACTS, independent_proof_verification='not_run'))]: with (args.output_directory/name).open('x') as stream: json.dump(value, stream, indent=2, allow_nan=False) stream.write('\n') with (args.output_directory/'report.md').open('x') as stream: stream.write(report) print(json.dumps(dict(output_directory=str(args.output_directory.resolve()), **manifest['counts'], documentary_gaps=claim_report['documentary_gap_count']))) if __name__ == '__main__': main()