#!/usr/bin/env python3
"""Check an unweighted matching against an explicit odd-component upper bound.

For a vertex subset S and q odd components of G-S, any matching has at
most (n-q+|S|)/2 edges, also at most floor(n/2). Equality with a feasible
candidate certifies maximum cardinality. A loose bound leaves optimality
unknown; it does not disprove the candidate. No matching/barrier constructor
or new almost-linear source algorithm is implemented.
"""
import argparse
import hashlib
import json
from pathlib import Path

MAX_VERTICES = 100_000
MAX_EDGES = 500_000


def pair(value):
    if not isinstance(value, list) or len(value) != 2 or any(isinstance(x,bool) or not isinstance(x,int) for x in value):
        raise ValueError('Every edge must be a pair of integer vertex indices')
    return min(value), max(value)


def audit(record):
    if not isinstance(record,dict):raise ValueError('Input must be an object')
    n=record.get('vertices')
    if isinstance(n,bool) or not isinstance(n,int) or not 1<=n<=MAX_VERTICES:
        raise ValueError(f'vertices must be an integer from 1 to {MAX_VERTICES}')
    supplied_edges=record.get('edges')
    if not isinstance(supplied_edges,list) or len(supplied_edges)>MAX_EDGES:
        raise ValueError(f'edges must be a list of at most {MAX_EDGES} pairs')
    edges=set(); adjacency=[[] for _ in range(n)]
    for value in supplied_edges:
        a,b=pair(value)
        if not 0<=a<b<n:raise ValueError('Graph edges must be loopless and in range')
        if (a,b) in edges:raise ValueError('Duplicate undirected graph edge')
        edges.add((a,b)); adjacency[a].append(b); adjacency[b].append(a)
    raw_barrier=record.get('barrier',[])
    if (not isinstance(raw_barrier,list) or any(isinstance(x,bool) or not isinstance(x,int) or not 0<=x<n for x in raw_barrier)
        or len(set(raw_barrier))!=len(raw_barrier)):
        raise ValueError('barrier must be a duplicate-free list of valid vertices')
    barrier=set(raw_barrier); seen=set(barrier); component_sizes=[]
    for start in range(n):
        if start in seen:continue
        seen.add(start); stack=[start]; size=0
        while stack:
            current=stack.pop(); size+=1
            for neighbor in adjacency[current]:
                if neighbor not in seen:
                    seen.add(neighbor); stack.append(neighbor)
        component_sizes.append(size)
    odd=sum(size%2 for size in component_sizes)
    numerator=n-odd+len(barrier)
    if numerator%2:raise AssertionError('Component parity invariant failed')
    bound=min(n//2,numerator//2)
    candidate=record.get('matching')
    if not isinstance(candidate,list) or len(candidate)>MAX_EDGES:raise ValueError('matching must be a bounded edge list')
    used=set(); issues=[]
    for value in candidate:
        a,b=pair(value)
        if (a,b) not in edges:
            issues.append(dict(code='MATCHING_EDGE_NOT_IN_GRAPH',edge=[a,b]))
        if a in used or b in used or a==b:
            issues.append(dict(code='MATCHING_ENDPOINT_REUSED',edge=[a,b]))
        used.update([a,b])
    feasible=not issues
    size=len(candidate) if feasible else None
    verified=feasible and size==bound
    if feasible and size>bound:raise AssertionError('A feasible matching exceeded a valid upper bound')
    digest=hashlib.sha256(json.dumps(record,sort_keys=True,separators=(',',':')).encode()).hexdigest()
    return dict(vertices=n,edges=len(edges),input_record_sha256=digest,
                matching_feasible=feasible,matching_size=size,candidate_issues=issues,
                barrier=sorted(barrier),component_sizes=component_sizes,odd_components=odd,
                cardinality_upper_bound=bound,maximum_cardinality_certificate_verified=verified,
                optimality_status='certified_by_matching_and_upper_bound' if verified else ('unknown_with_this_bound' if feasible else 'invalid_matching'),
                upper_bound_gap=bound-size if feasible else None,
                objective='unweighted_maximum_cardinality',arithmetic='exact_integer_graph_operations',
                limits=dict(vertices=MAX_VERTICES,edges=MAX_EDGES),
                source_connection=dict(family='120',source_commit='fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb',
                                       new_source_matching_algorithm_implemented=False,source_proof_verification='not_run'),
                formal_program_verification='not_run',
                interpretation='A feasible matching attaining the checked odd-component or vertex bound is maximum cardinality. A nonzero gap is inconclusive. Weight, fairness, multiway assignment and source algorithm correctness are outside this audit.')


def main():
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('input',type=Path)
    parser.add_argument('--output',type=Path)
    args=parser.parse_args()
    result=json.dumps(audit(json.loads(args.input.read_text())),indent=2,allow_nan=False)+'\n'
    if args.output:
        with args.output.open('x') as stream:stream.write(result)
    else:print(result,end='')


if __name__=='__main__':main()