#!/usr/bin/env python3
"""Finite semantic/snapshot/service audit for construction 82.

Independent direct-owner oracle versus normalized indexes; not a native-machine
implementation, all-length proof, or timing measurement. Python strings, sets,
and copies here are finite oracle machinery only.
"""
from itertools import product
import json
import random


def words(n):
    return [''.join(x) for x in product('01', repeat=n)]


def shapes(n, k, t):
    return '0' * (n-k) + t, t + '1' + '0' * (n-k-1)


def infer_seed(beta, z):
    # Model the unary snapshot lengths, without using last-1 string search.
    position, saved, trailing = 0, None, 0
    for bit in beta:
        if bit == '1':
            saved, trailing = position, 0
        else:
            trailing += 1
        position += 1
    if saved is None or saved < 1 or saved > trailing:
        return None
    if z != '0' * (trailing+1) + beta[:saved]:
        return None
    return saved


def chart_key(beta, side):
    if side == 'L':
        return beta.lstrip('0')
    if side == 'T':
        return beta.rstrip('0')
    raise AssertionError(side)


def snapshot_key(beta):
    # A saved immutable path state; intermediate endpoints are never marked.
    state = ()
    selected = state
    for bit in beta:
        state = state + (bit,)
        if bit == '1':
            selected = state
    return ''.join(selected)


def update(indexes, b, active):
    i, jl, jt = (set(x) for x in indexes)
    if active:
        i.add(b)
        if b.startswith('1'):
            n = (len(b)-1)//2
            alpha, beta = b[1:n+1], b[n+1:]
            jl.add(alpha + chart_key(beta, 'L'))
            jt.add(alpha + snapshot_key(beta))
    return frozenset(i), frozenset(jl), frozenset(jt)


def program(rng, k):
    # Prefix-node output labels allow noninjective synchronous maps as well as
    # automorphisms. Each namespace and lane gets its own independent program.
    return {p: rng.choice('01') for j in range(1, k+1) for p in words(j)}


def transform(p, t):
    return ''.join(p[t[:j]] for j in range(1, len(t)+1))


def owner(n, k, pa, pb, z):
    # Direct long owner, independently reconstructed for the relation oracle.
    if z[:n-k] == '0'*(n-k):
        t = z[n-k:]
        return transform(pa, t) + '1' + '0'*(n-k-1)
    if z[k:] == '1'+'0'*(n-k-1):
        return '0'*(n-k) + transform(pb, z[:k])
    return z


def read(indexes, n, k, alpha, pa, pb, z):
    i, jl, jt = indexes
    if z.startswith('0'*(n-k)):
        return alpha + transform(pa, z[-k:]) + '1' in jt
    if z[k:] == '1'+'0'*(n-k-1):
        return alpha + transform(pb, z[:k]).lstrip('0') in jl
    return '1'+alpha+z in i


def finish(releases, n, rate=4):
    cursor = 0
    for tick in range(1, n+1):
        for _ in range(rate):
            if cursor < len(releases) and releases[cursor] <= tick:
                cursor += 1
    return cursor == len(releases)


def interior_audit():
    seed_cases = query_cases = schedule_cases = 0
    rng = random.Random(23882)
    for n in range(3, 9):
        for beta in words(n):
            p = outside = trailing = 0
            started = False
            core_pos = 0
            ell = None
            for bit in beta:
                if not started and bit == '0':
                    p += 1
                    outside += 1
                    trailing += 1
                    continue
                started = True
                core_pos += 1
                if bit == '1':
                    ell, outside, trailing = core_pos, p, 0
                else:
                    outside += 1
                    trailing += 1
            if ell is None:
                continue
            positions = [j for j,b in enumerate(beta) if b == '1']
            assert p == positions[0]
            assert ell == positions[-1] - positions[0] + 1
            assert outside == n-ell and trailing == n-p-ell
            seed_cases += 1
        for ell in range(1, (n-1)//2+1):
            for p in range(n-ell+1):
                prog = program(rng,ell)
                a = '01' * (n//2) + ('0' if n%2 else '')
                possible = words(n)
                active = set(rng.sample(possible, max(1,len(possible)//3)))
                indexes = (frozenset(),)*3
                for b in active:
                    indexes = update(indexes,'1'+a+b,True)
                for t in words(ell):
                    v = transform(prog,t)
                    beta = '0'*p+v+'0'*(n-p-ell)
                    cursor = a
                    saved = cursor
                    for bit in '0'*p:
                        cursor += bit
                    for bit in v:
                        cursor += bit
                        if bit == '1':
                            saved = cursor
                    assert (saved in indexes[2]) == (beta in active)
                    assert saved == a+beta.rstrip('0')
                    query_cases += 1
    for n in range(3, 97):
        for ell in range(1,(n-1)//2+1):
            # Worst p proves every smaller initial workload by monotonicity;
            # exhaust all p separately in small widths.
            ps = range(n-ell+1) if n <= 16 else [0,n-ell]
            for p in ps:
                assert n+2+p <= 4*(n-ell)
                assert finish([1]*(n+2+p)+list(range(n-ell+1,n+1)),n)
                schedule_cases += 1
    return dict(interior_seed_scans=seed_cases, interior_queries=query_cases,
                interior_schedules=schedule_cases)


def audit():
    rng = random.Random(238)
    counts = dict(injective_words=0, bootstrap_pairs=0, retained_queries=0,
                  mixed_relation_queries=0, schedules=0, endpoint_snapshots=0)
    for n in range(1, 11):
        w = words(n)
        for side in ['L', 'T']:
            encoded = [chart_key(b, side) for b in w]
            assert len(set(encoded)) == len(w)
            for b, key in zip(w, encoded):
                assert (key.rjust(n, '0') if side == 'L' else key.ljust(n, '0')) == b
                counts['injective_words'] += 1
        for beta in w:
            assert snapshot_key(beta) == beta.rstrip('0')
            counts['endpoint_snapshots'] += 1
        if n <= 7:
            for beta in w:
                for z in w:
                    expected = [k for k in range(1, (n-1)//2+1)
                                if any(shapes(n,k,t)==(z,beta) for t in words(k))]
                    assert infer_seed(beta,z) == (expected[0] if expected else None)
                    counts['bootstrap_pairs'] += 1
    # Different cuts, maps, alpha values, source versions and support masks.
    for n in range(5, 9):
        descriptors = []
        for k in range(1, (n-1)//2+1):
            for _ in range(3):
                a = rng.choice(words(n))
                pa,pb=program(rng,k),program(rng,k)
                # Install a real identity-key A/B seed in the A program.
                seed = rng.choice(words(k))
                for j in range(1,k+1):
                    pa[seed[:j]]=seed[j-1]
                assert infer_seed(shapes(n,k,seed)[1], shapes(n,k,seed)[0]) == k
                descriptors.append((k,a,pa,pb))
        betas=words(n)
        population=['1'+a+b for _,a,_,_ in descriptors for b in betas]
        primary='0'+'0'*(2*n)
        population.append(primary)
        versions=[(frozenset(),)*3]
        for step in range(36):
            b=rng.choice(population)
            versions.append(update(versions[-1],b,step%5 != 0))
        for indexes in versions[::3]:
            for k,a,pa,pb in descriptors:
                for z in betas:
                    direct='1'+a+owner(n,k,pa,pb,z) in indexes[0]
                    got=read(indexes,n,k,a,pa,pb,z)
                    assert got==direct
                    counts['retained_queries'] += 1
                    for p,f in product([False,True],repeat=2):
                        edges=[]
                        if p: edges.append(primary)
                        if f: edges.append('1'+a+owner(n,k,pa,pb,z))
                        oracle=any(b in indexes[0] for b in edges)
                        assert oracle==((p and primary in indexes[0]) or (f and got))
                        counts['mixed_relation_queries'] += 1
        # Terminal-prefix and empty-suffix endpoints preserve distinct values.
        a='0'*n
        indexes=(frozenset(),)*3
        originals=['0'*n,'1'+'0'*(n-1),'101'+'0'*(n-3)]
        for b in originals:
            indexes=update(indexes,'1'+a+b,True)
        assert {a, a+'1', a+'101'} <= indexes[2]
        for b in betas:
            assert (a+chart_key(b,'T') in indexes[2]) == (b in originals)
    for n in range(3,258):
        for k in range(1,(n-1)//2+1):
            assert finish([1]*(n+2)+list(range(1,n+1)),n)
            assert finish([1]*(n+2)+list(range(n-k+1,n+1))+[n],n)
            # Any leading deletion of early synchronous output is a subtrace.
            for skipped in {0,k//2,k}:
                assert finish([1]*(n+2)+list(range(skipped+1,k+1)),n)
            counts['schedules'] += 2 + len({0,k//2,k})
    # Two-sided erasure loses an essential coordinate at the SAME width.
    x,y='00100','01000'
    assert x != y and x.strip('0') == y.strip('0') == '1'
    assert x.lstrip('0') != y.lstrip('0')
    assert x.rstrip('0') != y.rstrip('0')
    # In contrast, variable original width breaks even one-sided injectivity.
    assert '001'.lstrip('0') == '01'.lstrip('0')
    assert '100'.rstrip('0') == '10'.rstrip('0')
    return dict(status='passed',**counts, collision_controls=3, **interior_audit())


if __name__ == '__main__':
    print(json.dumps(audit(),indent=2,sort_keys=True))