"""Portable Go/literal-oracle replay; optional retained-query/current-Proof paths."""
from pathlib import Path
import argparse,datetime,hashlib,json,os,shutil,subprocess,sys
from oracle import assess

def main():
    p=argparse.ArgumentParser(description=__doc__);p.add_argument('--output',required=True);p.add_argument('--replay-smt',action='store_true');p.add_argument('--z3',default='z3');p.add_argument('--proof',help='Optional existing Proof executable; its identity is a new replay identity, never assumed to be the archived build.');a=p.parse_args()
    base=Path(__file__).resolve().parent;out=Path(a.output).resolve();out.mkdir(parents=True,exist_ok=False)
    work=out/'work';work.mkdir()
    for name in ['baseline','corrected','weak','cmd']:shutil.copytree(base/name,work/name)
    for name in ['go.mod','cases.json']:shutil.copyfile(base/name,work/name)
    env={**os.environ,'GOPROXY':'off','GOSUMDB':'off','REQPROOF_NO_DOWNLOAD':'1'};commands=[]
    def run(name,argv,timeout=90):
        start=datetime.datetime.now(datetime.timezone.utc).isoformat()
        c=subprocess.run(argv,cwd=work,env=env,capture_output=True,timeout=timeout)
        (out/(name+'.stdout.txt')).write_bytes(c.stdout);(out/(name+'.stderr.txt')).write_bytes(c.stderr)
        commands.append({'name':name,'argv':list(map(str,argv)),'cwd':str(work),'startedAtUtc':start,'finishedAtUtc':datetime.datetime.now(datetime.timezone.utc).isoformat(),'exitCode':c.returncode,'stdoutSha256':hashlib.sha256(c.stdout).hexdigest(),'stderrSha256':hashlib.sha256(c.stderr).hexdigest()});(out/'commands.json').write_text(json.dumps(commands,indent=2)+'\n');return c
    assert run('go-version',['go','version']).returncode==0
    binary=out/'observe';assert run('build',['go','build','-trimpath','-o',str(binary),'./cmd/observe']).returncode==0
    observed=run('observe',[str(binary),str(work/'cases.json')]);assert observed.returncode==0
    assessment=assess(json.loads(observed.stdout),work/'cases.json');(out/'oracle-assessment.json').write_text(json.dumps(assessment,indent=2)+'\n')
    assert assessment['passedByVariant']=={'baseline':6,'corrected':7,'weak':6},'Expected runtime contrast changed; inspect actual raw results'
    queries=[]
    if a.replay_smt:
        assert run('z3-version',[a.z3,'--version']).returncode==0
        for variant in ['baseline','corrected','weak']:
            c=run('query-'+variant,[a.z3,'-T:15',str(base/'observed'/(variant+'.smt2'))],30)
            queries.append({'variant':variant,'exitCode':c.returncode,'firstStdoutLine':c.stdout.decode(errors='replace').splitlines()[:1],'claim':'Replay of retained SMT bytes only; not new Go source translation or runtime evidence.'})
    source=[]
    if a.proof:
        proof=Path(a.proof).resolve();proof_sha=hashlib.sha256(proof.read_bytes()).hexdigest()
        for variant in ['baseline','corrected','weak']:
            c=run('proof-'+variant,[str(proof),'verify-lemma','--solver','z3','--no-download','--no-cache','--format','json','--show-query','--timeout','15s','./'+variant],80)
            j=json.loads(c.stdout);assert j['stats']['total']==1 and len(j['results'])==1
            source.append({'variant':variant,'binarySha256':proof_sha,'exitCode':c.returncode,'stats':j['stats'],'verdict':j['results'][0]['verdict'],'claim':'New caller-supplied source-verifier identity; never retroactive authentication of archived current-tree build.'})
    report={'runtimeCasesPerVariant':7,'recordedOperationCalls':21,'runtimePassedByVariant':assessment['passedByVariant'],'inputOracle':'Literal whole index plus full input values/nilness','coverageClaim':False,'retainedQueryReplays':queries,'currentSourceVerifierReplays':source,'strongContractProvedByThisRun':bool(source) and all(s['verdict']=='PROVED' for s in source if s['variant']!='weak'),'wrapperMeaning':'Exit0 means the expected finite defect/correction/weak-source contrasts reproduced. It does not accept the faulty variants or prove the strong contract.','networkUsedByScript':False}
    (out/'replay-report.json').write_text(json.dumps(report,indent=2)+'\n');print(json.dumps(report))
if __name__=='__main__':main()