"""Small, total proof checker for passive perfect-encryption deduction.

Input data, never code, are interpreted. This proves only the stated finite
atomic-key deduction problem; it does not verify a deployed crypto protocol.
"""
import json
import re

SCHEMA = ('Return JSON with exactly "secret_unreachable" (boolean), "steps" '
          '(list of zero-based public fact indices), and "known" (list of atom names). '
          'Start with initial_known. For each step, the indexed [message,key] fact must '
          'have an already-known key and add a new message. The final known list must '
          'contain exactly the deduced atoms, without duplicates, and be closed: every '
          'public fact whose key is known must have its message known. Set '
          'secret_unreachable to whether query_secret is absent. Any valid deduction '
          'order and known-list order are accepted. No external code or tools.')


def reference(instance):
    known = set(instance['initial_known'])
    steps = []
    changed = True
    while changed:
        changed = False
        for i, (message, key) in enumerate(instance['encrypted_facts']):
            if key in known and message not in known:
                known.add(message); steps.append(i); changed = True
    return dict(secret_unreachable=instance['query_secret'] not in known,
                steps=steps, known=sorted(known))


def check(instance, certificate):
    """Return a bounded diagnostic, without consulting a reference target."""
    if not isinstance(certificate, dict) or set(certificate) != {'secret_unreachable','steps','known'}:
        return 'schema'
    if type(certificate['secret_unreachable']) is not bool:
        return 'schema'
    steps, final = certificate['steps'], certificate['known']
    if not isinstance(steps,list) or not isinstance(final,list) or len(steps)>128 or len(final)>128:
        return 'schema'
    if any(type(i) is not int for i in steps) or any(not isinstance(a,str) for a in final):
        return 'schema'
    known = set(instance['initial_known']); facts = instance['encrypted_facts']
    for i in steps:
        if not 0 <= i < len(facts):
            return 'fact_index'
        message,key = facts[i]
        if key not in known:
            return 'unavailable_key'
        if message in known:
            return 'redundant_step'
        known.add(message)
    if len(set(final)) != len(final) or set(final) != known:
        return 'known_mismatch'
    if any(key in known and message not in known for message,key in facts):
        return 'not_closed'
    if certificate['secret_unreachable'] != (instance['query_secret'] not in known):
        return 'query_mismatch'
    return 'valid'


def parse_final(text):
    # One whole final JSON fence is a formatting variant, never extract from prose.
    if not isinstance(text,str) or len(text)>50000:
        return None
    fence = re.fullmatch(r'\s*```(?:json)?\s*\n(.*?)\n```\s*',text,flags=re.S)
    try:
        def reject_duplicates(pairs):
            value = {}
            for k,v in pairs:
                if k in value:
                    raise ValueError('duplicate JSON key')
                value[k]=v
            return value
        return json.loads(fence.group(1) if fence else text,
                          object_pairs_hook=reject_duplicates)
    except (ValueError,TypeError,RecursionError):
        return None


def prompt(row):
    return json.dumps({k:row[k] for k in ['initial_known','encrypted_facts','query_secret']},
                      separators=(',',':'))


def trace(row, certificate):
    known = set(row['initial_known'])
    lines = ['Finite symbolic deduction, treating enc as perfect encryption.',
             'Initial atoms: '+', '.join(sorted(known))+'.']
    for i in certificate['steps']:
        message,key=row['encrypted_facts'][i]
        lines.append(f'Fact {i}: key {key} is available, so decrypt to obtain {message}.')
        known.add(message)
    blocked = [str(i) for i,(_,k) in enumerate(row['encrypted_facts']) if k not in known]
    lines.append('At the fixed point all other facts are blocked by unknown keys: '+', '.join(blocked)+'.')
    lines.append('The query atom is '+('absent.' if certificate['secret_unreachable'] else 'present.'))
    return '\n'.join(lines)