#!/usr/bin/env python3
"""Independent engineering-guide labs. Python 3.10+, standard library only.

Usage: python3 guide_labs.py <lab> | python3 guide_labs.py test

These finite models show contracts, state transitions, and counterexamples. They
do not implement Kafka, Redis, Lucene, ZooKeeper, MinIO, Flink, or OpenObserve.
SQLite exercises use one local database; coding examples use exact integers.
Production storage, networking, authorization, and release behavior need their
own integration/fault tests. No lab makes network calls or uses private data.
"""
from __future__ import annotations

import argparse
from collections import Counter, deque
from concurrent.futures import ThreadPoolExecutor
import heapq
import itertools
import json
import math
from pathlib import Path
import random
import sqlite3
import subprocess
import sys
import tempfile
import threading

CHECKS = 0


def check(condition, message="model invariant failed"):
    """Count a test obligation; unlike assert, remains active with python -O."""
    global CHECKS
    CHECKS += 1
    if not condition:
        raise AssertionError(message)


def rejects(error, operation):
    try:
        operation()
    except error:
        check(True)
        return
    raise AssertionError("expected " + error.__name__)


def integer(value, *, minimum=None):
    """Public numeric boundary: bool is not accepted as an integer input."""
    if type(value) is not int or (minimum is not None and value < minimum):
        raise ValueError("integer outside supported domain")


def sum_first(values, n, *, verify=False):
    """Pre: integer values, integer 0<=n<=len(values). Post: exact prefix sum;
    no mutation. Normal path O(n); optional invariant checks are diagnostic."""
    integer(n, minimum=0)
    if n > len(values) or any(type(v) is not int for v in itertools.islice(values, n)):
        raise ValueError("valid integer prefix required")
    i, total = 0, 0
    # Invariant: 0<=i<=n and total=sum(values[:i]). Bound: n-i.
    while i < n:
        if verify:
            check(total == sum(values[:i]) and 0 <= i <= n)
        total += values[i]
        i += 1
    if verify:
        check(total == sum(values[:n]))
    return total


def divide_nonnegative(a, b, *, verify=False):
    """Pre: integer a>=0,b>0. Post: a=q*b+r and 0<=r<b."""
    integer(a, minimum=0)
    integer(b, minimum=1)
    q, r = 0, a
    # Invariant: a=q*b+r and r>=0. Bound: natural r, decreases by b.
    while r >= b:
        if verify:
            check(a == q*b+r and r >= 0)
        r, q = r-b, q+1
    check(a == q*b+r and 0 <= r < b)
    return q, r


def binary_search(values, target):
    """Pre: nondecreasing comparable values. Post: first target index, or None.
    This public demo validates sortedness O(n); search itself is O(log n)."""
    if any(a > b for a, b in zip(values, values[1:])):
        raise ValueError("sorted sequence required")
    lo, hi = 0, len(values)
    # Invariant: all indices <lo are <target; all >=hi are >=target.
    # Bound: hi-lo, nonnegative and strictly decreases while lo<hi.
    while lo < hi:
        mid = (lo+hi)//2
        if values[mid] < target:
            lo = mid+1
        else:
            hi = mid
    return lo if lo < len(values) and values[lo] == target else None


def max_window(values, k):
    """Pre: integers, 1<=k<=n. Post: maximum sum of a length-k window."""
    integer(k, minimum=1)
    if k > len(values) or any(type(v) is not int for v in values):
        raise ValueError("nonempty integer window required")
    running = best = sum(values[:k])
    # Invariant: running is the current k-window sum, best covers prior windows.
    # Bound: remaining right endpoints.
    for right in range(k, len(values)):
        running += values[right]-values[right-k]
        best = max(best, running)
    return best


def power(base, exponent, *, verify=False):
    """Pre: integer base, integer exponent>=0. Post: exact base**exponent.
    O(log exponent) multiplications, not O(log exponent) bit-operation cost."""
    integer(base)
    integer(exponent, minimum=0)
    x, y, result = base, exponent, 1
    # Invariant: result*x**y == base**exponent. Bound: natural y.
    while y:
        if verify:
            check(result * x**y == base**exponent)
        if y % 2:
            result *= x
        x, y = x*x, y//2
    return result


def partition_colors(values):
    """Pre: list containing only 0,1,2. Post: sorted permutation, in place."""
    if not isinstance(values, list) or any(type(v) is not int or v not in (0,1,2) for v in values):
        raise ValueError("mutable list of three valid integer colors required")
    original = Counter(values)
    lo, mid, hi = 0, 0, len(values)-1
    # Invariant: 0s[:lo],1s[lo:mid],unknown[mid:hi+1],2s[hi+1:]; permutation.
    # Bound: hi-mid+1, decreases exactly once per step.
    while mid <= hi:
        if values[mid] == 0:
            values[lo], values[mid] = values[mid], values[lo]
            lo, mid = lo+1, mid+1
        elif values[mid] == 1:
            mid += 1
        else:
            values[mid], values[hi] = values[hi], values[mid]
            hi -= 1
    check(Counter(values) == original and values == sorted(values))
    return values


def linear_search(values, target):
    """Post: first matching index or None; input unchanged. Pure equality on
    the supplied sequence is assumed. Bound: remaining finite indices."""
    for i,value in enumerate(values):
        # Invariant: target does not occur in values[:i].
        if value==target:return i
    return None


def maximum_index(values):
    """Nonempty integer sequence; post: first index of its maximum."""
    if not values or any(type(v) is not int for v in values):
        raise ValueError('nonempty integer sequence required')
    best=0
    for i in range(1,len(values)):
        # Invariant: best indexes the first maximum of the processed prefix.
        if values[i]>values[best]:best=i
    return best


def euclid(a,b):
    """Nonnegative integers; post: gcd(a,b), with gcd(0,0)=0 convention."""
    integer(a,minimum=0);integer(b,minimum=0)
    x,y=a,b
    while y:  # invariant gcd(x,y)=gcd(a,b); natural bound y strictly decreases
        x,y=y,x%y
    return x


def matrix_search(matrix, target):
    """Pre: rectangular matrix with nondecreasing rows/columns. Post: a valid
    matching coordinate or None. Demo validates O(mn); core search is O(m+n)."""
    n = len(matrix[0]) if matrix else 0
    if any(len(row) != n for row in matrix):
        raise ValueError("rectangular matrix required")
    if any(a > b for row in matrix for a,b in zip(row,row[1:])):
        raise ValueError("rows not sorted")
    if any(matrix[r][c] > matrix[r+1][c] for r in range(len(matrix)-1) for c in range(n)):
        raise ValueError("columns not sorted")
    r, c = 0, n-1
    # Invariant: every remaining match lies in rows[r:],columns[:c+1].
    # Bound: (m-r)+(c+1), with explicit bounds supporting absence.
    while r < len(matrix) and c >= 0:
        if matrix[r][c] == target:
            return r, c
        if matrix[r][c] > target:
            c -= 1
        else:
            r += 1
    return None


def common_three(a, b, c):
    """Pre: sorted comparable sequences. Post: one common value or None.
    Ties/duplicates/empty inputs are allowed; inputs remain unchanged."""
    if any(x > y for seq in (a,b,c) for x,y in zip(seq,seq[1:])):
        raise ValueError("sorted lists required")
    i=j=k=0
    # Invariant: remaining tails contain all still-possible common values.
    # Bound: remaining total tail length; advance a weak minimum.
    while i < len(a) and j < len(b) and k < len(c):
        if a[i] == b[j] == c[k]:
            return a[i]
        if a[i] <= b[j] and a[i] <= c[k]:
            i += 1
        elif b[j] <= a[i] and b[j] <= c[k]:
            j += 1
        else:
            k += 1
    return None


def wp_assignment(variable, expression, postcondition):
    """Restricted pure Python predicate model: substitute evaluated expression
    into a copied state. No parsing/eval of untrusted code and no loops in S."""
    def precondition(state):
        try:
            after = dict(state)
            after[variable] = expression(state)
            return bool(postcondition(after))
        except (ZeroDivisionError, KeyError, ValueError, TypeError):
            return False  # normal defined execution is required
    return precondition


def gf_multiply(a, b):
    """Internal GF(256) multiply; pre: 8-bit field values. Polynomial 0x11d.
    Eight iterations consume b's bits; this is field arithmetic, not integers."""
    result=0
    for _ in range(8):
        if b & 1:
            result ^= a
        b >>= 1
        a <<= 1
        if a & 256:
            a ^= 0x11d
    return result


def gf_power(a, exponent):
    """Internal exponentiation, nonnegative integer exponent; bound exponent."""
    result=1
    while exponent:
        if exponent & 1:
            result=gf_multiply(result,a)
        a=gf_multiply(a,a)
        exponent >>= 1
    return result


def erasure_encode(data, total):
    """Educational non-systematic Reed-Solomon evaluation code over GF(256).
    Pre: 1<=k=len(data)<=total<=255. Post: total distinct indexed coded shards.
    A shard is one field byte for this one-stripe demo, not a production file."""
    integer(total, minimum=1)
    if not isinstance(data, bytes) or not 1 <= len(data) <= total <= 255:
        raise ValueError("supported byte stripe and total required")
    shards=[]
    for x in range(1,total+1):
        value=0
        for coefficient in reversed(data):
            value=gf_multiply(value,x)^coefficient
        shards.append((x,value))
    return shards


def erasure_decode(shards, k):
    """Pre: >=k distinct compatible valid shards of one encoded stripe.
    Post: recover its k polynomial coefficients/original bytes. Version/checksum
    compatibility is an external precondition; mixed versions are not detected."""
    integer(k,minimum=1)
    if len(shards)<k or len({x for x,_ in shards})!=len(shards):
        raise ValueError("insufficient or duplicate shard identities")
    if any(type(x) is not int or type(y) is not int or not 1<=x<=255 or not 0<=y<=255 for x,y in shards):
        raise ValueError("invalid field shard")
    rows=[[gf_power(x,i) for i in range(k)]+[y] for x,y in shards[:k]]
    # Gaussian elimination: processed columns form identity; equations equivalent.
    # Bounds: k columns and k rows, finite field inverses only for nonzero pivots.
    for column in range(k):
        pivot=next((r for r in range(column,k) if rows[r][column]),None)
        if pivot is None:
            raise ValueError("singular shard set")
        rows[column],rows[pivot]=rows[pivot],rows[column]
        inverse=gf_power(rows[column][column],254)
        rows[column]=[gf_multiply(v,inverse) for v in rows[column]]
        for r in range(k):
            if r!=column and rows[r][column]:
                factor=rows[r][column]
                rows[r]=[a^gf_multiply(factor,b) for a,b in zip(rows[r],rows[column])]
    return bytes(row[-1] for row in rows)


class Contributions:
    """Single-process transactional local dedup, no expiring keys. A mutex
    protects this shared SQLite connection. Claim + effect commit together."""
    def __init__(self):
        self.db=sqlite3.connect(":memory:",check_same_thread=False,isolation_level=None)
        self.db.executescript("CREATE TABLE seen(id TEXT PRIMARY KEY,amount INTEGER);"
                              "CREATE TABLE counter(n INTEGER);INSERT INTO counter VALUES(0);")
        self.lock=threading.Lock()

    def apply(self, identity, amount, *, fail=False):
        integer(amount,minimum=0)
        if not identity:
            raise ValueError("stable operation ID required")
        with self.lock:
            self.db.execute("BEGIN IMMEDIATE")
            try:
                old=self.db.execute("SELECT amount FROM seen WHERE id=?",(identity,)).fetchone()
                if old:
                    if old[0]!=amount:
                        raise ValueError("identity payload mismatch")
                    self.db.execute("COMMIT")
                    return False
                self.db.execute("INSERT INTO seen VALUES(?,?)",(identity,amount))
                self.db.execute("UPDATE counter SET n=n+?",(amount,))
                if fail:
                    raise RuntimeError("injected failure")
                self.db.execute("COMMIT")
                return True
            except BaseException:
                self.db.execute("ROLLBACK")
                raise


def lab_division():
    for a in range(31):
        for b in range(1,8):
            check(divide_nonnegative(a,b,verify=True)==divmod(a,b))
    rejects(ValueError,lambda: divide_nonnegative(1,0))
    rejects(ValueError,lambda: divide_nonnegative(-1,2))
    print("Integer division: invariant a=q*b+r; natural remainder decreases.")


def lab_logic():
    for p,q in itertools.product((False,True),repeat=2):
        check((not (p and q))==((not p) or (not q)))
        check((not p or q)==(not (p and not q)))
    check(all([]) and not any([]))
    check(all((not (x>5)) or x>0 for x in range(-10,11)))
    check(not all((not (x>0)) or x>5 for x in range(-10,11)))
    print("Truth tables, empty quantifier domains, and converse counterexample checked.")


def lab_wp():
    post=lambda s:s['x']>10
    last=wp_assignment('x',lambda s:2*s['x'],post)
    whole=wp_assignment('x',lambda s:s['x']+1,last)
    for x in range(-10,15):
        check(whole({'x':x})==(x>4))
    division=wp_assignment('x',lambda s:10//s['d'],lambda s:s['x']>=2)
    check(not division({'d':0}) and division({'d':5}))
    print("wp(x:=x+1;x:=2*x, x>10) is x>4; undefined division is excluded.")


def lab_assignment():
    x,y=2,7
    x,y=y,x
    check((x,y)==(7,2))
    x,y=2,7
    x=y; y=x
    check((x,y)==(7,7))
    print("Simultaneous RHS evaluation swaps; naive sequential overwrite loses old x.")


def lab_guards():
    for x,y in itertools.product(range(-3,4),repeat=2):
        enabled=[]
        if x>=y:enabled.append(x)
        if y>=x:enabled.append(y)
        check(enabled and all(m==max(x,y) for m in enabled))
    check(not (3>3 or 3<3))
    print("Every enabled max branch is correct; strict guards leave equality uncovered.")


def lab_invariants():
    rng=random.Random(7)
    for n in range(15):
        values=[rng.randrange(-10,11) for _ in range(n)]
        for prefix in range(n+1):
            check(sum_first(values,prefix,verify=True)==sum(values[:prefix]))
    rejects(ValueError,lambda: sum_first([1,2],3))
    rejects(ValueError,lambda: sum_first([],True))
    print("Prefix invariant and empty/oversized/type boundaries checked.")


def lab_arithmetic():
    for base in range(-3,4):
        for exponent in range(12):
            check(power(base,exponent,verify=True)==base**exponent)
    for n in range(7):
        for colors in itertools.product((0,1,2),repeat=n):
            check(partition_colors(list(colors))==sorted(colors))
    rejects(ValueError,lambda: partition_colors([3]))
    rejects(ValueError,lambda: power(2,-1))
    for a,b in itertools.product(range(15),repeat=2):
        check(euclid(a,b)==math.gcd(a,b))
    for values in ([],[1],[2,5,5,1],[-3,-1,-7]):
        for target in range(-4,7):
            check(linear_search(values,target)==(values.index(target) if target in values else None))
        if values:check(maximum_index(values)==values.index(max(values)))
    rejects(ValueError,lambda:maximum_index([]))
    rejects(ValueError,lambda:euclid(-1,2))
    print("Power, three-color arrays, Euclid, first search, and first-maximum contracts checked.")


def lab_procedures():
    outputs=(1,2)
    a=outputs[0]; a=outputs[1]
    b=outputs[1]; b=outputs[0]
    check(a==2 and b==1)
    same=[7]
    u=v=same
    u.append(8)
    check(v==[7,8])
    swap_a=swap_b=7
    swap_a,swap_b=swap_b,swap_a
    check(swap_a==swap_b==7)  # aliased equal-value swap is not this counterexample
    print("Different copy-out values show alias ambiguity; Python lists share objects.")


def lab_termination():
    m,n=2,3
    before=(m-0)*n+(n-n)
    after=(m-1)*n+(n-0)
    check(before==after)
    corrected_before=(m-0)*(n+1)+(n-n)
    corrected_after=(m-1)*(n+1)+(n-0)
    check(corrected_after==corrected_before-1)
    i,s=0,0
    for _ in range(10):
        check(i==0 and s==0)  # finite observation of a no-progress skip loop
    print("A naive reset measure ties; weight n+1 decreases at row transitions.")


def lab_recursion():
    def recursive(n):
        integer(n,minimum=0)
        return 1 if n==0 else n*recursive(n-1)  # natural n decreases
    def iterative(n):
        integer(n,minimum=0)
        result=1
        for i in range(1,n+1):
            result*=i  # invariant result=i!; bound remaining factors
        return result
    for n in range(20):
        check(recursive(n)==iterative(n)==math.factorial(n))
    rejects(ValueError,lambda: iterative(-1))
    print("Recursive induction and iterative accumulator agree on checked integer inputs.")


def lab_optimization():
    values=list(range(30))
    slow=[sum(values[:i]) for i in range(len(values)+1)]
    fast=[0]
    for value in values:
        fast.append(fast[-1]+value)
    check(slow==fast)
    a,b,c=1e16,-1e16,1.0
    check((a+b)+c!=a+(b+c))
    print("Maintained exact prefix sums agree; float reassociation counterexample differs.")


def lab_large():
    matrix=[[1,3,5],[2,4,7],[3,6,9]]
    for target in range(11):
        location=matrix_search(matrix,target)
        present=any(target in row for row in matrix)
        check((location is not None)==present)
        if location:check(matrix[location[0]][location[1]]==target)
    check(matrix_search([],1) is None and matrix_search([[]],1) is None)
    check(common_three([1,2,4],[2,3,4],[0,4])==4)
    check(common_three([1],[2],[3]) is None)
    check(common_three([],[],[]) is None)
    check(common_three([1,1,2],[1,1],[1])==1)
    rejects(ValueError,lambda: matrix_search([[1],[2,3]],2))
    print("Sorted intersection and saddleback search handle ties, absence, and empty data.")


def lab_inversion():
    def forward(x):
        integer(x)
        return x+100 if x<0 else x+200
    def inverse(y):
        integer(y)
        if y<100:return y-100
        if y>=200:return y-200
        raise ValueError("outside forward image")
    for x in range(-200,201):
        check(inverse(forward(x))==x)
    for y in range(100,200):
        rejects(ValueError,lambda y=y:inverse(y))
    print("Inverse works on the image; unreachable output gap 100..199 is rejected.")


def lab_erasure():
    data=bytes(range(1,5))
    encoded=erasure_encode(data,6)
    for choice in itertools.combinations(encoded,4):
        check(erasure_decode(list(choice),4)==data)
    data12=bytes(range(12))
    encoded16=erasure_encode(data12,16)
    check(erasure_decode(encoded16[4:],12)==data12)
    rejects(ValueError,lambda:erasure_decode(encoded16[:9],12))
    check(math.isclose(16/12,4/3) and math.isclose(4/12,1/3))
    print("GF(256) Reed-Solomon reconstructs compatible survivors; 9 of 16 is insufficient for k=12.")


def lab_replication():
    replicas={'A':(200,'first'),'B':(150,'later request'),'C':(200,'first')}
    selected=max(replicas.values(),key=lambda x:x[0])
    check(selected[1]=='first')
    quorums=[set(x) for x in itertools.combinations(replicas,2)]
    check(all(a & b for a in quorums for b in quorums))
    print("Fixed quorums overlap; timestamp winner need not be the latest logical request.")


def lab_transactions():
    model=Contributions()
    rejects(RuntimeError,lambda:model.apply('e1',1,fail=True))
    check(model.apply('e1',1) and not model.apply('e1',1))
    with ThreadPoolExecutor(max_workers=8) as pool:
        won=list(pool.map(lambda _:model.apply('e2',2),range(20)))
    check(sum(won)==1)
    rejects(ValueError,lambda:model.apply('e1',7))
    check(model.db.execute('SELECT n FROM counter').fetchone()[0]==3)
    model.db.close()
    a=b=10
    stored=a+1; stored=b+1
    check(stored==11)  # isolated reads/writes do not make the pair atomic
    print("Local claim+effect transaction survives retries/rollback; read-then-write pair loses update.")


def lab_log():
    offsets=[100,105]
    check(offsets[-1]+1==106 and 100+len(offsets)!=106)
    high_watermark=106
    check(105<high_watermark and not 106<high_watermark)
    with tempfile.TemporaryDirectory(prefix='guide-wal-') as directory:
        database=str(Path(directory)/'events.sqlite')
        child=("import sqlite3,os,sys;d=sqlite3.connect(sys.argv[1]);"
               "d.execute('PRAGMA journal_mode=WAL');d.execute('PRAGMA synchronous=FULL');"
               "d.execute('CREATE TABLE events(id INTEGER PRIMARY KEY)');d.commit();"
               "d.execute('INSERT INTO events VALUES(1)');d.commit();"
               "d.execute('INSERT INTO events VALUES(2)');os._exit(77)")
        result=subprocess.run([sys.executable,'-c',child,database],timeout=10)
        check(result.returncode==77)
        db=sqlite3.connect(database)
        check(db.execute('SELECT id FROM events').fetchall()==[(1,)])
        db.close()
    print("Exclusive HW/next-offset rules checked; SQLite process-crash recovery kept committed row only.")


def lab_index():
    durable={1:'old'}
    reader=dict(durable)
    durable[1]='new'
    check(reader[1]=='old' and durable[1]=='new')
    reader=dict(durable)
    check(reader[1]=='new')
    state={'version':7,'value':'original'}
    def commit(base,value):
        if state['version']!=base:return False
        state.update(version=base+1,value=value)
        return True
    check(commit(7,'A') and not commit(7,'B'))
    docs={1:'red fox',2:'blue bird',3:'blue fox'}
    postings={}
    for identity,text in docs.items():
        for term in text.lower().split():postings.setdefault(term,set()).add(identity)
    check(postings['blue'] & postings['fox']=={3})
    print("Reader snapshot, conditional version update, and postings intersection checked.")


def lab_windows():
    event_time,window_end,watermark=5,10,6
    check(event_time<=watermark and watermark<window_end)
    allowed_lateness=3
    check(window_end+allowed_lateness>12)
    check(not window_end+allowed_lateness>13)
    checkpoint={'state':2,'next_offset':2}
    state=checkpoint['state']
    for _ in range(checkpoint['next_offset'],4):state+=1
    check(state==4)
    print("Late timestamp can belong to a live window; cleanup horizon and state/offset recovery differ.")


def lab_coordination():
    fence=33
    check(33>=fence)  # new grant 34 not yet installed at this resource
    fence=34
    check(not 33>=fence)
    leader={'x':2}; local={'x':1}
    check(local['x']!=leader['x'])
    print("Old token rejected after newer fence installed; local read can lag global writer.")


def lab_proxy():
    queued=0
    for _ in range(20):
        queued+=150-100
    check(queued==1000)
    capacity=1000
    admitted=queued+1<=capacity
    check(not admitted)
    print("150/s input minus 100/s service fills 1000-item buffer in 20s; further admission rejected.")


def lab_publication():
    objects={'A','B'}
    catalog={'version':1,'files':{'A','B'}}
    reader=set(catalog['files'])
    objects.add('C')
    check(catalog['files']=={'A','B'})  # upload alone does not publish
    catalog={'version':2,'files':{'C'}}
    needed=catalog['files'] | reader
    check(needed=={'A','B','C'})
    reader.clear()
    objects.intersection_update(catalog['files'] | reader)
    check(objects=={'C'})
    print("Upload, catalog commit, reader lifetime, and object cleanup are distinct transitions.")


def lab_algorithms():
    rng=random.Random(19)
    for n in range(1,12):
        values=[rng.randrange(-10,11) for _ in range(n)]
        for k in range(1,n+1):check(max_window(values,k)==max(sum(values[i:i+k]) for i in range(n-k+1)))
        ordered=sorted(values)
        for target in range(-11,12):
            expected=ordered.index(target) if target in ordered else None
            check(binary_search(ordered,target)==expected)
    rejects(ValueError,lambda:max_window([],1))
    rejects(ValueError,lambda:max_window([1],0))
    graph={'s':[('a',2),('b',1)],'b':[('a',0)],'a':[]}
    distances={'s':0}; heap=[(0,'s')]
    while heap:  # finite graph/nonnegative relaxation; stale entries skipped
        distance,node=heapq.heappop(heap)
        if distance!=distances[node]:continue
        for neighbor,weight in graph[node]:
            if weight<0:raise ValueError('Dijkstra requires nonnegative weights')
            candidate=distance+weight
            if candidate<distances.get(neighbor,math.inf):
                distances[neighbor]=candidate;heapq.heappush(heap,(candidate,neighbor))
    check(distances['a']==1)
    unweighted={'s':['a','b'],'a':['c'],'b':['c'],'c':[]}
    queue=deque(['s']); steps={'s':0}
    while queue:  # bound: each finite vertex enqueued at most once
        node=queue.popleft()
        for neighbor in unweighted[node]:
            if neighbor not in steps:steps[neighbor]=steps[node]+1;queue.append(neighbor)
    check(steps['c']==2)
    print("Fixed windows/binary search finite references; BFS and nonnegative Dijkstra checked.")


def lab_refactoring():
    def old(value):
        if type(value) is not int or value<0:raise ValueError('nonnegative integer')
        return value*2
    def validate(value):
        if type(value) is not int or value<0:raise ValueError('nonnegative integer')
    def new(value):
        validate(value);return value*2
    for value in (-1,0,2,True,'2'):
        outcomes=[]
        for operation in (old,new):
            try:outcomes.append(('value',operation(value)))
            except ValueError as error:outcomes.append(('error',str(error)))
        check(outcomes[0]==outcomes[1])
    print("Characterization tests preserve outputs and validation errors across extraction.")


def lab_patterns():
    def price(cents,strategy):
        integer(cents,minimum=0)
        result=strategy(cents)
        integer(result,minimum=0)
        return result
    check(price(1000,lambda n:n)==1000)
    check(price(1000,lambda n:n*9//10)==900)
    subscribers=[]; seen=[]
    def first(value):seen.append(('first',value));subscribers.remove(first)
    def second(value):seen.append(('second',value))
    subscribers.extend([first,second])
    for callback in list(subscribers):callback('event')  # snapshot defines current notification membership
    check(seen==[('first','event'),('second','event')] and subscribers==[second])
    print("Callable strategies and snapshot-defined Observer unsubscribe behavior checked.")


def lab_metrics():
    def ratio(good,total):
        if total<=0:return None  # no data is not a healthy zero/one
        return good/total
    check(ratio(9,10)==0.9 and ratio(90,100)==0.9)
    check(ratio(0,0) is None)
    points_before,points_after=20,30
    completed_before,completed_after=10,10
    check(points_after>points_before and completed_before==completed_after)
    print("Denominator/no-data policy explicit; rescaled points alone do not prove more outcomes.")


def lab_documentation():
    rejects(ValueError,lambda:sum_first([1,2],3))
    check(sum_first([1,2],2)==3)
    print("Explicit public validation stays active under python -O; invariant comments explain the loop.")


def pair_sum(values, target):
    """Sorted comparable numbers; post: two distinct matching indices or None."""
    if any(a>b for a,b in zip(values,values[1:])):
        raise ValueError('sorted input required')
    lo,hi=0,len(values)-1
    # Invariant: any solution remains within [lo,hi]. Bound: hi-lo.
    while lo<hi:
        total=values[lo]+values[hi]
        if total==target:return lo,hi
        if total<target:lo+=1
        else:hi-=1
    return None


def merge_sort(values):
    """Post: sorted copy/permutation; input unchanged. Recursion bound len."""
    if len(values)<2:return list(values)
    middle=len(values)//2
    a,b=merge_sort(values[:middle]),merge_sort(values[middle:])
    result=[];i=j=0
    # Invariant: result is the sorted consumed merge. Bound: unconsumed count.
    while i<len(a) and j<len(b):
        if a[i]<=b[j]:result.append(a[i]);i+=1
        else:result.append(b[j]);j+=1
    return result+a[i:]+b[j:]


def quick_sort_copy(values):
    """Educational three-way sorted copy; not an in-place sort. Recursive
    subproblems strictly shorten. Worst-case cost/stack may still be quadratic."""
    if len(values)<2:return list(values)
    pivot=values[len(values)//2]
    low=[v for v in values if v<pivot]
    equal=[v for v in values if v==pivot]
    high=[v for v in values if v>pivot]
    return quick_sort_copy(low)+equal+quick_sort_copy(high)


def fibonacci(n):
    integer(n,minimum=0)
    a,b=0,1
    for i in range(n):  # invariant (a,b)=(F_i,F_(i+1)); bound n-i
        a,b=b,a+b
    return a


def knapsack(items, capacity):
    """0/1 knapsack; positive integer weights/nonnegative values/capacity.
    Post: optimal value. O(n*capacity) time/O(capacity) auxiliary cells."""
    integer(capacity,minimum=0)
    for weight,value in items:
        integer(weight,minimum=1);integer(value,minimum=0)
    best=[0]*(capacity+1)
    for weight,value in items:
        # Descending capacities prevent reusing this same item twice.
        for c in range(capacity,weight-1,-1):
            best[c]=max(best[c],best[c-weight]+value)
    return best[capacity]


def topological(graph):
    """Pre: finite adjacency dict includes all referenced vertices. Post:
    topological order; raises ValueError for missing vertices or directed cycle."""
    if any(v not in graph for edges in graph.values() for v in edges):
        raise ValueError('unknown vertex')
    degree=dict.fromkeys(graph,0)
    for edges in graph.values():
        for v in edges:degree[v]+=1
    queue=deque(v for v in graph if degree[v]==0);result=[]
    # Invariant: emitted vertices have no unprocessed prerequisites.
    # Bound: unprocessed vertices; each is emitted once.
    while queue:
        node=queue.popleft();result.append(node)
        for v in graph[node]:
            degree[v]-=1
            if degree[v]==0:queue.append(v)
    if len(result)!=len(graph):raise ValueError('directed cycle')
    return result


def linked_cycle(next_indices, head=0):
    """Index-based singly linked list; None means end. Validates links and
    uses Floyd's meeting rule with an explicit finite poll bound for the demo."""
    n=len(next_indices)
    if not n:return False
    if type(head) is not int or not 0<=head<n or any(v is not None and (type(v) is not int or not 0<=v<n) for v in next_indices):
        raise ValueError('invalid linked index')
    slow=fast=head
    for _ in range(2*n+1):
        if fast is None or next_indices[fast] is None:return False
        slow=next_indices[slow];fast=next_indices[next_indices[fast]]
        if slow==fast:return True
    raise AssertionError('valid finite list exceeded Floyd bound')


def lab_algorithm_patterns():
    for values in ([],[1],[3,1,2,1],[-4,0,8],list(range(20))):
        original=list(values)
        check(merge_sort(values)==quick_sort_copy(values)==sorted(values))
        check(values==original)
    for target in range(-2,8):
        values=[-1,0,2,3,5]
        pair=pair_sum(values,target)
        exists=any(a+b==target for a,b in itertools.combinations(values,2))
        check((pair is not None)==exists)
        if pair:check(pair[0]!=pair[1] and values[pair[0]]+values[pair[1]]==target)
    check([fibonacci(n) for n in range(8)]==[0,1,1,2,3,5,8,13])
    check(knapsack([(2,3),(3,4),(4,5)],5)==7)
    check(knapsack([(2,3)],4)==3)  # a single item cannot be used twice
    rejects(ValueError,lambda:knapsack([(0,1)],2))
    check(topological({'a':['b'],'b':['c'],'c':[]})==['a','b','c'])
    rejects(ValueError,lambda:topological({'a':['b'],'b':['a']}))
    check(not linked_cycle([1,2,None]) and linked_cycle([1,2,1]))
    # Union-Find forest: find follows parent links toward a root.
    parent=list(range(4))
    def find(x):
        while parent[x]!=x:x=parent[x]  # forest depth decreases toward root
        return x
    def union(a,b):
        ra,rb=find(a),find(b)
        if ra==rb:return False
        parent[rb]=ra;return True
    check(union(0,1) and union(1,2) and not union(2,0))
    check(find(0)==find(2) and find(3)!=find(0))
    # Backtracking/enumeration: exponential output size is part of the cost.
    subsets=[subset for k in range(4) for subset in itertools.combinations([1,2,3],k)]
    check(len(subsets)==8 and len(list(itertools.permutations([1,2,3])))==6)
    check(heapq.nlargest(2,[1,4,2,3])==[4,3])
    # Greedy interval scheduling, sorted by earliest finishing time.
    selected=[];end=-math.inf
    for start,finish in sorted([(0,2),(1,3),(2,4),(3,5)],key=lambda p:p[1]):
        if start>=end:selected.append((start,finish));end=finish
    check(selected==[(0,2),(2,4)])
    print('Two pointers, sorting, DP, topology, linked cycles, Union-Find, enumeration, heap, and greedy patterns checked.')


def lab_privacy():
    def diagnostic(event):
        t,s=event.get('type'),event.get('status')
        return {'type':t if isinstance(t,str) and t in {'click','impression'} else 'other',
                'status':s if isinstance(s,str) and s in {'accepted','rejected'} else 'unknown'}
    event={'type':'click','status':'accepted','user_id':'synthetic-user',
           'token':'synthetic-secret','payload':'not retained'}
    projected=diagnostic(event)
    check(projected=={'type':'click','status':'accepted'})
    check(not {'user_id','token','payload'} & set(projected))
    check(diagnostic({'type':[],'status':{}})=={'type':'other','status':'unknown'})
    print('Synthetic diagnostics whitelist bounded categories and omit identifiers, secrets, and payloads.')


def lab_security():
    db=sqlite3.connect(':memory:')
    db.execute('CREATE TABLE objects(id TEXT PRIMARY KEY,owner TEXT,value TEXT)')
    db.executemany('INSERT INTO objects VALUES(?,?,?)',[('one','alice','A'),('two','bob','B')])
    def authorized_read(trusted_principal,identity):
        # Principal is supplied by an assumed trusted auth boundary, not request data.
        return db.execute('SELECT value FROM objects WHERE id=? AND owner=?',
                          (identity,trusted_principal)).fetchone()
    check(authorized_read('alice','one')==('A',))
    check(authorized_read('alice','two') is None)
    check(authorized_read('alice',"one' OR 1=1 --") is None)
    check(db.execute('SELECT COUNT(*) FROM objects').fetchone()[0]==2)
    db.close()
    print('Parameterized values plus trusted-owner scope prevent the tested injection/unauthorized lookup cases.')


def lab_compatibility():
    old={'duration_ms':1000}
    new={'duration_ms':1000,'duration_seconds':1}
    def old_reader(row):return row['duration_ms']/1000
    def new_reader(row):return row.get('duration_seconds',row['duration_ms']/1000)
    check(old_reader(old)==old_reader(new)==new_reader(old)==new_reader(new)==1)
    changed_meaning={'duration_ms':1}
    check(type(changed_meaning['duration_ms']) is int and old_reader(changed_meaning)!=1)
    print('Old/new fixtures interoperate; unchanged integer shape does not catch changed units.')


LABS={
    'division':lab_division,'logic':lab_logic,'quantifiers':lab_logic,'wp':lab_wp,
    'assignment':lab_assignment,'guards':lab_guards,'invariants':lab_invariants,
    'derivation':lab_invariants,'arithmetic':lab_arithmetic,'procedures':lab_procedures,
    'termination':lab_termination,'recursion':lab_recursion,'optimization':lab_optimization,
    'large':lab_large,'inversion':lab_inversion,'documentation':lab_documentation,
    'erasure':lab_erasure,'replication':lab_replication,'transactions':lab_transactions,
    'log':lab_log,'index':lab_index,'windows':lab_windows,'coordination':lab_coordination,
    'proxy':lab_proxy,'publication':lab_publication,'algorithms':lab_algorithms,
    'refactoring':lab_refactoring,'patterns':lab_patterns,'metrics':lab_metrics,
    'algorithm-patterns':lab_algorithm_patterns,'privacy':lab_privacy,
    'security':lab_security,'compatibility':lab_compatibility,
}


def main():
    parser=argparse.ArgumentParser(description=__doc__)
    parser.add_argument('lab',choices=['test',*LABS])
    args=parser.parse_args()
    selected=LABS.items() if args.lab=='test' else [(args.lab,LABS[args.lab])]
    for name,run in selected:
        print(f'\n[{name}]');run()
    print(f'\nPASS: {CHECKS:,} checks; {len(LABS) if args.lab=="test" else 1} lab command(s).')


if __name__=='__main__':
    main()