#!/usr/bin/env python3
"""Portable, stdlib-only replay of C1433–C1482 arithmetic and provenance.

The declared six source pairs are transcribed here independently of model/*.json.
Decimal reversal uses integer division/remainders, not research.py's string method.
Only original source durations are reversed. Counts describe verification groups,
not independent discoveries, probability evidence, or historical authentication.

Usage: python verify_cycle.py [--allow-pending] [--require-50]
"""
from __future__ import annotations

import argparse
from datetime import datetime, timezone
from fractions import Fraction
import hashlib
import json
from pathlib import Path
import sys

ROOT = Path(__file__).resolve().parent
F = Fraction
SOURCES = {
    'MT_regular': (4106, 2456, 'Noah', 'Creation'),
    'MT_cumulative': (14006, 4836, 'Shem', 'Creation'),
    'LXX_regular': (5486, 3236, 'Noah', 'Creation'),
    'LXX_cumulative': (14896, 5746, 'Shem', 'Creation'),
    'SP_regular': (4406, 3106, 'Noah', 'Fall'),
    'SP_cumulative': (13396, 4716, 'Shem', 'Fall'),
}
CHECKS = []
MODELS = []


def encode(value):
    if isinstance(value, Fraction):
        return value.numerator if value.denominator == 1 else str(value)
    if isinstance(value, dict):
        return {str(k): encode(v) for k, v in value.items()}
    if isinstance(value, (tuple, list)):
        return [encode(v) for v in value]
    return value


def check(name, actual, expected=True):
    actual, expected = encode(actual), encode(expected)
    passed = actual == expected
    CHECKS.append({'name': name, 'pass': passed, 'actual': actual, 'expected': expected})
    return passed


def read_json(path):
    return json.loads(path.read_text(encoding='utf-8'))


def model(name, expected, subset=False):
    actual = read_json(ROOT / 'model' / (name + '.json'))
    if subset:
        actual = {key: actual.get(key) for key in expected}
    MODELS.append(name + '.json')
    check('model/' + name, actual, expected)


def digest(value):
    # Matches research.digest: compact sorted JSON, Unicode preserved, UTF-8.
    raw = json.dumps(value, sort_keys=True, separators=(',', ':'), ensure_ascii=False)
    return hashlib.sha256(raw.encode('utf-8')).hexdigest()


def numeric_reverse(n):
    if not isinstance(n, int) or isinstance(n, bool) or n <= 0:
        raise ValueError('Original positive integer duration required')
    place = 1
    while n % 10 == 0:
        n //= 10
        place *= 10
    reversed_core = 0
    while n:
        n, digit = divmod(n, 10)
        reversed_core = reversed_core * 10 + digit
    return place * reversed_core


def original_core(n):
    places = 0
    while n % 10 == 0:
        n //= 10
        places += 1
    return n, places


def build_path(legs, anchor):
    result = [anchor]
    for span in legs:
        result.append(result[-1] + numeric_reverse(span))
    return result


def key(q, x, factor=F(25, 23)):
    return F(q) + factor * (x-q)


def replay_arithmetic():
    spines, stage, gains, hinges, parts = {}, {}, [], {}, {}
    for name, (c, flood, role, head_role) in SOURCES.items():
        lower, upper = flood-1406, c-flood
        legs = [lower, upper]
        p2, p3 = build_path(legs, 1406), build_path([1400]+legs, 6)
        spines[name] = {'C': c, 'F': flood, 'hinge_role': role, 'legs': legs,
                        'path2': p2, 'path3': p3, 'source_head_role': head_role}
        stage[name] = {'tail_gain': numeric_reverse(1400)-1400,
                       'head_difference': p3[-1]-p2[-1],
                       'interior_suffix_difference': [a-b for a,b in zip(p3[1:],p2)]}
        hinges[name] = {'F': flood, 'hinge': flood+600, 'role': role, 'span': 600,
                        'construction': 'same rounded source state; no new Gear transport'}
        for span in legs:
            core, zeros = original_core(span)
            digits, remaining = [], core
            while remaining:
                remaining, digit = divmod(remaining,10)
                digits.append(digit)
            formula = 10**zeros * sum(d*(10**(len(digits)-1-i)-10**i)
                                      for i,d in enumerate(digits))
            gains.append({'spine': name, 'n': span, 'I_n': numeric_reverse(span),
                          'core': str(core), 'zeros': zeros,
                          'gain': numeric_reverse(span)-span, 'formula_gain': formula})
        partitions = {'Flood': legs, role: [lower+600,upper-600],
                      'Both': [lower,600,upper-600]}
        parts[name] = {}
        for label, original in partitions.items():
            parts[name][label] = {'source_legs': original,
                'images': [numeric_reverse(n) for n in original],
                'path2': build_path(original,1406),
                'path3': build_path([1400]+original,6)}
            check(f'original duration retained: {name}/{label}',sum(original),c-1406)
            check(f'complete path stage translation: {name}/{label}',
                  [a-b for a,b in zip(parts[name][label]['path3'][1:],
                                     parts[name][label]['path2'])], [2700]*(len(original)+1))
    model('spines',spines)
    model('stage_translation',stage)
    model('digit_gains',gains)
    model('hinges',hinges)
    model('partitions',parts)
    model('regular_partitions',{n:p for n,p in parts.items() if n.endswith('_regular')})
    model('cumulative_partitions',{n:p for n,p in parts.items() if n.endswith('_cumulative')})
    check('six source objects and eighteen named partitions',
          [len(spines),sum(len(p) for p in parts.values())],[6,18])

    congruence = {}
    for tradition in ('MT','LXX','SP'):
        r,c = spines[tradition+'_regular'],spines[tradition+'_cumulative']
        sg,hg = c['C']-r['C'],c['path2'][-1]-r['path2'][-1]
        modulus = 90 if tradition == 'SP' else 990
        congruence[tradition] = {'source_gap':sg,'head_gap':hg,'modulus':modulus,
                                'residue':hg%modulus,'same_residue':sg%modulus==hg%modulus}
    model('congruence',congruence)

    law, classes, full, upper_translations = {}, {}, {}, {}
    for name,(c,flood,role,_) in SOURCES.items():
        lower, upper = flood-1406,c-flood
        d_l = numeric_reverse(lower+600)-numeric_reverse(lower)-numeric_reverse(600)
        d_u = numeric_reverse(upper)-numeric_reverse(600)-numeric_reverse(upper-600)
        law[name] = {'dL':d_l,'dU':d_u,'alternate_change':d_l-d_u,'refined_change':-d_u}
        classes.setdefault(str((d_l,d_u)),[]).append(name)
        check('partition law alternate: '+name,
              parts[name][role]['path2'][-1]-parts[name]['Flood']['path2'][-1],d_l-d_u)
        check('partition law refined: '+name,
              parts[name]['Both']['path2'][-1]-parts[name]['Flood']['path2'][-1],-d_u)
        original = [1406,flood,flood+600,c]
        rebuilt = parts[name]['Both']['path2']
        offsets = [a-b for a,b in zip(rebuilt,original)]
        full[name] = {'source_path':original,'inverse_path':rebuilt,
                      'node_displacements':offsets,'retained_edge':rebuilt[2]-rebuilt[1]}
        upper_translations[name] = {'upper_offsets':offsets[1:],
                                   'uniform':len(set(offsets[1:]))==1}
    # JSON object order does not matter. Class member order is the model's
    # manuscript-mode presentation order, so compare these as memberships.
    model('partition_law',law)
    existing_classes = read_json(ROOT/'model/partition_classes.json')
    MODELS.append('partition_classes.json')
    check('model/partition_classes membership',
          {k:sorted(v) for k,v in existing_classes.items()},
          {k:sorted(v) for k,v in classes.items()})
    model('full_node_displacements',full)
    model('upper_branch_translations',upper_translations)

    mt, lx, sp = (spines[n+'_cumulative'] for n in ('MT','LXX','SP'))
    model('MT_SP_cumulative_preservation',{
        'source_legs_difference':[a-b for a,b in zip(mt['legs'],sp['legs'])],
        'inverse_legs_difference':[numeric_reverse(a)-numeric_reverse(b)
                                   for a,b in zip(mt['legs'],sp['legs'])],
        'head_gaps':[mt['C']-sp['C'],mt['path2'][-1]-sp['path2'][-1],
                     mt['path3'][-1]-sp['path3'][-1]],
        'intermediate_gaps':[mt['F']-sp['F'],mt['path2'][1]-sp['path2'][1]]})
    model('LXX_MT_cumulative',{
        'source_lower_gap':lx['legs'][0]-mt['legs'][0],
        'source_upper_gap':lx['legs'][1]-mt['legs'][1],
        'inverse_lower_gap':numeric_reverse(lx['legs'][0])-numeric_reverse(mt['legs'][0]),
        'inverse_upper_gap':numeric_reverse(lx['legs'][1])-numeric_reverse(mt['legs'][1]),
        'source_head_gap':lx['C']-mt['C'],
        'inverse_head_gap':lx['path2'][-1]-mt['path2'][-1]})
    model('LXX_SP_cumulative',{
        'source_gap':lx['C']-sp['C'],
        'inverse_gap':lx['path2'][-1]-sp['path2'][-1],
        'source_triangle':(lx['C']-mt['C'])+(mt['C']-sp['C']),
        'inverse_triangle':(lx['path2'][-1]-mt['path2'][-1])+(mt['path2'][-1]-sp['path2'][-1]),
        'extra_contraction':(lx['path2'][-1]-lx['C'])-(sp['path2'][-1]-sp['C'])})
    lr,sr = spines['LXX_regular'],spines['SP_regular']
    model('mode_interaction',{
        'SP_minus_LXX_regular':sr['path3'][-1]-lr['path3'][-1],
        'SP_minus_LXX_cumulative':sp['path3'][-1]-lx['path3'][-1],
        'difference_of_differences':(sr['path3'][-1]-lr['path3'][-1])-(sp['path3'][-1]-lx['path3'][-1]),
        'equivalent_mode_difference':(lx['path3'][-1]-lr['path3'][-1])-(sp['path3'][-1]-sr['path3'][-1])})

    native = read_json(ROOT/'evidence/Moses_LXX_native_complete_path.json')
    native_rows = {row['name']:row for row in native['rows']}
    check('source LXX Noah row',native_rows['Noah']['rounded_BC'],3836)
    check('source LXX Shem row',native_rows['Shem']['rounded_BC'],3336)
    check('source LXX original Noah to Shem',
          native_rows['Noah']['rounded_BC']-native_rows['Shem']['rounded_BC'],500)
    model('Shem_incidences',{
        'SP_two_stage_path':parts['SP_cumulative']['Both']['path2'],
        'SP_completed_path':parts['SP_cumulative']['Both']['path3'],
        'SP_inverse_Shem_at1406':parts['SP_cumulative']['Both']['path2'][2],
        'LXX_regular_Shem':native_rows['Shem']['rounded_BC'],
        'SP_completed_inverse_Flood':sp['path3'][2],
        'MT_cumulative_Shem':mt['F']+600,'source_state':native['source_state']})
    model('Covenant_path_scope',[
        {'role':role,'LXX':a,'Key_image':key(1866,a),'SP':b,'matches':key(1866,a)==b}
        for role,a,b in zip(('Nativity','reversed_Conquest','reversed_Flood','head'),
                             lr['path3'],sp['path3'])])

    l_head, s_head = lr['path3'][-1],sp['path3'][-1]
    prophetic = key(1406,l_head,F(70,69))
    lower_sp = SOURCES['SP_regular'][1]-1406
    route = [l_head,prophetic,prophetic-lower_sp,
             prophetic-lower_sp+2700,prophetic-lower_sp+2700+(s_head-sr['path3'][-1])]
    model('closed_Key_circuit',{'route':route,
        'edge_changes':[b-a for a,b in zip(route,route[1:])],
        'direct':key(1866,l_head),'target':s_head})
    check('C1432 direct head closure',key(1866,l_head),s_head)
    check('C1432 reciprocal closure',key(1866,s_head,F(23,25)),l_head)
    check('C1432 translated 11270 family',
          [14726-(6+numeric_reverse(5436-6)),14006-sp['path2'][1],l_head-1866],
          [23*490]*3)
    check('C1432 70-fold Covenant law',[l_head-1866,s_head-1866],[70*161,70*175])
    cap = read_json(ROOT/'evidence/cap_round_loss_identity.json')
    cap_loss = sum(row['rounded_reduction'] for row in cap['rows'])
    model('source_to_head_bridge',{
        'cap_loss':cap_loss,'accepted_Fall':13401-SOURCES['SP_cumulative'][0],
        'upper_difference':mt['legs'][1]-sp['legs'][1],
        'MT_SP_source_Flood_gap':mt['F']-sp['F'],
        'MT_SP_preserved_head_gap':mt['path3'][-1]-sp['path3'][-1],
        'Covenant_head_gain':s_head-l_head,
        'MT_LXX_regular_inverse_gap':spines['MT_regular']['path3'][-1]-l_head})
    check('C1432 cap plus accepted Fall',[cap_loss+5,mt['legs'][1]-sp['legs'][1]],[490,490])

    nearby = key(4106,prophetic)
    model('two_Key_nearby_route',{'Prophetic_head':prophetic,'radius_to4106':prophetic-4106,
        'Priestly_head_about4106':nearby,'SP_head':s_head,'head_difference':s_head-nearby,
        'paired_intervals':[[nearby,4106],[s_head,4116]]})
    model('anchor_covariance',{'original':nearby,'anchor_only':key(4116,prophetic),
        'both_input_and_anchor':key(4116,prophetic+10),
        'anchor_only_change':key(4116,prophetic)-nearby,'required_pair_translation':10})
    hgap,tgap = lx['path3'][-1]-l_head,1446-1406
    kr = F(25,23)
    model('paired_LXX_join',{'head_gap':hgap,'target_gap':tgap,
        'head_gap_required':kr*tgap/(kr-1),
        'regular_output':key(l_head,1406),'cumulative_output':key(lx['path3'][-1],1446),
        'output_difference_formula':kr*tgap+(1-kr)*hgap})
    paired = {}
    for tradition in ('MT','LXX','SP'):
        r,c = (spines[tradition+'_'+mode]['path3'][-1] for mode in ('regular','cumulative'))
        a,b = key(r,1406),key(c,1446)
        paired[tradition] = {'regular_result':a,'cumulative_result':b,
                             'difference':b-a,'predicted_difference':kr*tgap+(1-kr)*(c-r)}
    model('paired_anchor_comparison',paired)
    model('stage_Key_interaction',{
        'Covenant_two_stage_image':key(1866,lr['path2'][-1]),
        'SP_two_stage_target':sp['path2'][-1],
        'Covenant_two_stage_residual':key(1866,lr['path2'][-1])-sp['path2'][-1],
        'LXX_two_stage_regular_join':key(lr['path2'][-1],1406),
        'LXX_two_stage_cumulative_join':key(lx['path2'][-1],1446),
        'positive_stage_commutator':key(1866,lr['path2'][-1]+2700)-key(1866,lr['path2'][-1])-2700
    },subset=True)
    model('reconstruction_contract',{'sufficient_inputs':{'source_pairs':6,'named_offset':600,
          'later_anchors':[1406,6]}},subset=True)


def replay_bindings():
    bindings = read_json(ROOT/'model/source_bindings.json')
    MODELS.append('source_bindings.json')
    names = [item['file'] for item in bindings]
    check('source binding filenames unique',len(names),len(set(names)))
    for item in bindings:
        path = ROOT/'evidence'/item['file']
        # Never follow recorded original absolute paths: the evidence is portable.
        check('evidence exists: '+item['file'],path.is_file())
        if not path.is_file():
            continue
        data = path.read_bytes()
        check('source SHA256 and bytes: '+item['file'],
              [hashlib.sha256(data).hexdigest(),len(data)],[item['sha256'],item['bytes']])
    return len(bindings)


def replay_journal(args):
    parent = read_json(ROOT/'evidence/C1432_record.json')
    parent_payload = {k:v for k,v in parent.items() if k not in ('sha256','hash_note')}
    check('C1432 predecessor content hash',digest(parent_payload),parent['sha256'])
    journal = read_json(ROOT/'journal.json')
    check('journal count bounded',0 < len(journal) <= 50)
    if args.require_50:
        check('final cycle has exactly fifty records',len(journal),50)
    expected_predecessor = parent['sha256']
    for offset,record in enumerate(journal):
        expected_step = 1433+offset
        check(f'C{expected_step} number and predecessor',
              [record['step'],record['predecessor_sha256']],
              [expected_step,expected_predecessor])
        payload = {k:v for k,v in record.items() if k != 'sha256'}
        check(f'C{expected_step} content hash',digest(payload),record['sha256'])
        check(f'C{expected_step} completed and reassessed',
              bool(record.get('finding')) and bool(record.get('reassessment')) and
              bool(record.get('closed_utc')) and
              datetime.fromisoformat(record['closed_utc']) >= datetime.fromisoformat(record['opened_utc']) and
              all(record.get('checks',{}).values()))
        expected_predecessor = record['sha256']
    pending_path = ROOT/'pending.json'
    pending = pending_path.exists()
    if args.allow_pending and pending:
        pending_record = read_json(pending_path)
        check('allowed pending record follows completed chain',
              [pending_record['step'],pending_record['predecessor_sha256']],
              [1433+len(journal),expected_predecessor])
    else:
        check('no pending research record',pending,False)
    return len(journal),pending


def replay_reader():
    metadata = read_json(ROOT/'model/reader_integration.json')
    MODELS.append('reader_integration.json')
    before = (ROOT/'evidence/Reader_before.md').read_bytes()
    after = (ROOT/'deliverables/490d_Chronological_Families_Explanation_C1431.md').read_bytes()
    check('reviewed reader before/after hashes',
          [hashlib.sha256(before).hexdigest(),hashlib.sha256(after).hexdigest()],
          [metadata['before_sha256'],metadata['after_sha256']])
    old,new = before.decode(),after.decode()
    for start,end in [('## Local changes become','## The same spine operation'),
                      ('## Calendar Keys preserve','## What the common explanation')]:
        check('unchanged reader section: '+start,
              old[old.index(start):old.index(end)],new[new.index(start):new.index(end)])
    addition = new[new.index('## How the three inverse families connect internally'):new.index('## Calendar Keys preserve')]
    check('reader addition word count',len(addition.split()),metadata['addition_words'])
    check('reader display math balanced',new.count('\\['),new.count('\\]'))
    headings = [line for line in new.splitlines() if line.startswith('#')]
    check('reader headings unique',len(headings),len(set(headings)))


def main():
    parser = argparse.ArgumentParser(description=__doc__)
    parser.add_argument('--allow-pending',action='store_true',
                        help='Permit the current incomplete action during an interim replay.')
    parser.add_argument('--require-50',action='store_true',
                        help='Require all fifty completed records C1433 through C1482.')
    args = parser.parse_args()
    bound_count = journal_count = 0
    pending = None
    try:
        replay_arithmetic()
        bound_count = replay_bindings()
        replay_reader()
        journal_count,pending = replay_journal(args)
    except Exception as exc:
        CHECKS.append({'name':'verification execution','pass':False,
                       'actual':type(exc).__name__+': '+str(exc),'expected':'successful replay'})
    failed = [item for item in CHECKS if not item['pass']]
    non_arithmetic = ['dependency_families.json','review_summary.json']
    present = sorted(p.name for p in (ROOT/'model').glob('*.json') if p.name!='verification.json')
    unchecked = [name for name in present if name not in MODELS and name not in non_arithmetic]
    result = {
        'status':'PASS' if not failed else 'FAIL',
        'verified_utc':datetime.now(timezone.utc).isoformat(),
        'grouped_check_count':len(CHECKS),'failed_check_count':len(failed),
        'scope':'Six declared source pairs, eighteen named partitions and their complete paths; local source/Key relationships; evidence hashes and completed journal chain. Verification counts are not independent discoveries or statistical evidence.',
        'method':'Independent arithmetic digit reversal using integer divmod; exact fractions; research.digest-compatible canonical JSON hashes.',
        'second_decimal_reversal_performed':False,
        'require_50':args.require_50,'allow_pending':args.allow_pending,
        'completed_journal_records':journal_count,'pending_present':pending,
        'bound_evidence_files':bound_count,
        'arithmetic_models_checked':sorted(set(MODELS)),
        'non_arithmetic_review_files':non_arithmetic,
        'additional_model_files_not_checked':unchecked,
        'checks':CHECKS}
    (ROOT/'model/verification.json').write_text(json.dumps(result,indent=2,ensure_ascii=False)+'\n',encoding='utf-8')
    print(json.dumps({k:result[k] for k in ('status','grouped_check_count','failed_check_count',
          'completed_journal_records','bound_evidence_files','additional_model_files_not_checked')}))
    for item in failed:
        print(json.dumps(item,ensure_ascii=False),file=sys.stderr)
    return 1 if failed else 0


if __name__ == '__main__':
    raise SystemExit(main())