verify_sat_boundary.py

#!/usr/bin/env python3
"""Finite corroboration, not a formal proof or a Python resource-cost claim."""
from dataclasses import dataclass
from itertools import combinations, permutations, product
from math import comb
from random import Random
from pathlib import Path
import hashlib
import json


def models(clauses, n):
    return {a for a in range(1 << n)
            if all(any(bool(a & (1 << (abs(l)-1))) == (l > 0) for l in c)
                   for c in clauses)}


def split_clause(c, nextvar, horn=False):
    c = tuple(c)
    if horn:
        assert sum(l > 0 for l in c) <= 1
        c = tuple(l for l in c if l < 0) + tuple(l for l in c if l > 0)
    if len(c) <= 3:
        return (c,), nextvar
    z = list(range(nextvar, nextvar + len(c)-3))
    out = [(c[0], c[1], z[0])]
    out += [(-z[j-1], c[j+1], z[j]) for j in range(1, len(z))]
    out += [(-z[-1], c[-2], c[-1])]
    return tuple(out), nextvar + len(z)


def synth_relation(b, relation):
    # Unsplit canonical CNF, used independently from the finite tables.
    return tuple(tuple((-(i+1) if a >> i & 1 else i+1) for i in range(b))
                 for a in range(1 << b) if not (relation >> a & 1))


def clause_mask(b, c):
    return sum(1 << a for a in models((c,), b))


def cnf_closure(b, horn=False):
    clauses = []
    for n in range(0, b+1 if horn else min(2, b)+1):
        for variables in combinations(range(1, b+1), n):
            for signs in product((-1, 1), repeat=n):
                c = tuple(v*s for v, s in zip(variables, signs))
                if not horn or sum(l > 0 for l in c) <= 1:
                    clauses.append(clause_mask(b, c))
    rels = {(1 << (1 << b))-1}
    for c in clauses:
        rels |= {r & c for r in rels}
    return rels


def affine_relations(b):
    rels = {(1 << (1 << b))-1}
    for row in range(1 << b):
        for rhs in (0, 1):
            c = sum(1 << a for a in range(1 << b)
                    if (a & row).bit_count() % 2 == rhs)
            rels |= {r & c for r in rels}
    return rels


def horn_protocol(b, left, right):
    """Communication accounting only; enumerating local models is free here."""
    forced = 0
    idle = 0
    turns = 0
    additions = 0
    bits = 0
    coordinate_bits = (max(1,b)-1).bit_length()
    while True:
        relation = left if turns % 2 == 0 else right
        eligible = [a for a in range(1<<b) if relation >> a & 1 and a & forced == forced]
        turns += 1
        bits += 2  # message type: failure, no change, or additions
        if not eligible:
            result = False
            break
        least = (1<<b)-1
        for a in eligible:
            least &= a
        assert relation >> least & 1  # meet closure, not true for arbitrary CNF
        new = (least ^ forced).bit_count()
        if not new:
            idle += 1
            if idle == 2:
                result = True
                break
        else:
            idle = 0
            additions += new
            bits += (coordinate_bits+1)*new+1  # delimited coordinate list
        forced = least
    assert turns <= 2*b+2 and additions <= b
    assert bits <= b*coordinate_bits+6*b+4
    return result, turns, bits


# Tables indexed by fixed slots. Relation bits use the sorted list of slots.
def lookup(mask, slots, assign):
    index = sum(assign[i] << j for j, i in enumerate(slots))
    return bool(mask >> index & 1)


def update(op, items):
    kind = op[0]
    if kind == 'E':
        slots = tuple(op[1])
        return slots, (1 << (1 << len(slots)))-1
    if kind == 'J':
        (s, a), (t, b) = items
        if s != t:
            raise ValueError('sort')
        return s, a & b
    s, r = items[0]
    if kind == 'I':
        if op[1] in s:
            raise ValueError('introduce')
        t = tuple(sorted(s + (op[1],)))
    elif kind == 'F':
        if op[1] not in s:
            raise ValueError('forget')
        t = tuple(i for i in s if i != op[1])
    elif kind == 'C':
        if not all(abs(l)-1 in s for l in op[1]):
            raise ValueError('clause')
        t = s
    elif kind == 'R':
        if tuple(sorted(op[1])) != tuple(range(len(op[1]))) or any(i >= len(op[1]) for i in s):
            raise ValueError('permutation')
        t = tuple(sorted(op[1][i] for i in s))
    else:
        raise ValueError('opcode')
    out = 0
    for a in range(1 << len(t)):
        assignment = {i: (a >> j) & 1 for j, i in enumerate(t)}
        if kind == 'F':
            ok = any(lookup(r, s, assignment | {op[1]: v}) for v in (0,1))
        elif kind == 'I':
            ok = lookup(r, s, assignment)
        elif kind == 'R':
            ok = lookup(r, s, {i: assignment[op[1][i]] for i in s})
        else:
            ok = lookup(r, s, assignment) and any(assignment[abs(l)-1] == (l > 0) for l in op[1])
        if ok:
            out |= 1 << a
    return t, out


@dataclass(frozen=True)
class Flat:
    n: int
    boundary: tuple  # pairs (slot, literal-variable-ID)
    clauses: tuple


def flat_step(op, fs):
    if op[0] == 'E':
        return Flat(len(op[1]), tuple((s, i+1) for i, s in enumerate(op[1])), ())
    f = fs[0]
    b = dict(f.boundary)
    if op[0] == 'I':
        b[op[1]] = f.n+1
        return Flat(f.n+1, tuple(sorted(b.items())), f.clauses)
    if op[0] == 'F':
        del b[op[1]]
        return Flat(f.n, tuple(sorted(b.items())), f.clauses)
    if op[0] == 'C':
        c = tuple((1 if l > 0 else -1)*b[abs(l)-1] for l in op[1])
        return Flat(f.n, f.boundary, f.clauses+(c,))
    if op[0] == 'R':
        return Flat(f.n, tuple(sorted((op[1][s],v) for s,v in f.boundary)), f.clauses)
    if op[0] == 'J':
        g = fs[1]
        remap = {v: b[s] for s, v in g.boundary}
        n = f.n
        for v in range(1, g.n+1):
            if v not in remap:
                n += 1
                remap[v] = n
        gc = tuple(tuple((1 if l > 0 else -1)*remap[abs(l)] for l in c) for c in g.clauses)
        return Flat(n, f.boundary, f.clauses+gc)
    raise ValueError(op)


def flat_relation(f):
    b = tuple(sorted(f.boundary))
    out = 0
    for a in models(f.clauses, f.n):
        image = sum(((a >> (v-1)) & 1) << j for j, (_,v) in enumerate(b))
        out |= 1 << image
    return tuple(s for s, _ in b), out


@dataclass(frozen=True, eq=False)
class Node:
    op: tuple
    args: tuple
    tag: tuple


def node(op, *args):
    return Node(op, args, update(op, [x.tag for x in args]))


def decode(n):
    return flat_step(n.op, [decode(x) for x in n.args])


def postfix(n):
    return [op for child in n.args for op in postfix(child)] + [n.op]


def abstract_stack(program):
    st = []
    for op in program:
        arity = 0 if op[0] == 'E' else 2 if op[0] == 'J' else 1
        if len(st) < arity:
            return None
        try:
            args = st[-arity:] if arity else []
            v = update(op, args)
        except ValueError:
            return None
        if arity:
            del st[-arity:]
        st.append(v)
    return st


def abstract_program(program):
    st = abstract_stack(program)
    return st is not None and len(st) == 1 and st[0] == ((), 1)


class RecordMachine:
    """Literal immutable binary records; only read/copy paths may reach old nodes.

    Python allocation and finite-table evaluation are not charged machine time.
    The audit records old target paths, labels, batch size, and immutability.
    """
    def __init__(self):
        self.heap = [(('bottom',), ())]
        self.root = 0
        self.bad = False
        self.accept = False
        self.max_radius = 0
        self.max_batch = 0

    def old(self, path):
        assert len(path) <= 2
        self.max_radius = max(self.max_radius, len(path))
        v = self.root
        for p in path:
            v = self.heap[v][1][p]
        return v

    def step(self, op):
        if self.bad:
            return
        try:
            label, _ = self.heap[self.old(())]
            kind = op[0]
            if kind == 'E':
                args = ()
                tag = update(op, [])
                tail = self.old(())
                first = label[0] == 'bottom'
            elif kind == 'J':
                if label[0] != 'stack' or label[1]:
                    raise ValueError('underflow')
                right = self.old((0,))
                left = self.old((1,0))
                tag = update(op, [self.heap[left][0][2], self.heap[right][0][2]])
                args = (left, right)
                first = self.heap[self.old((1,))][0][1]
                tail = self.old((1,1))
            else:
                if label[0] != 'stack':
                    raise ValueError('underflow')
                value = self.old((0,))
                args = (value,)
                tag = update(op, [self.heap[value][0][2]])
                tail = self.old((1,))
                first = label[1]
        except ValueError:
            self.bad = True
            self.accept = False
            return
        old_length = len(self.heap)
        # A simultaneous two-record batch, with its stack pointing to its value.
        self.heap.extend([(('value',op,tag),args), (('stack',first),(old_length,tail))])
        self.root = old_length+1
        self.max_batch = max(self.max_batch, len(self.heap)-old_length)
        self.accept = first and tag == ((),1)

    def stack_tags(self, root):
        # An uncharged independent verifier, not part of the local transition.
        result = []
        while self.heap[root][0][0] != 'bottom':
            value, root = self.heap[root][1]
            result.append(self.heap[value][0][2])
        return result[::-1]


def check_records(program):
    m = RecordMachine()
    retained = [(m.root, [])]
    for i, op in enumerate(program):
        old_heap = tuple(m.heap)
        m.step(op)
        assert tuple(m.heap[:len(old_heap)]) == old_heap
        expected = abstract_stack(program[:i+1])
        assert m.bad == (expected is None)
        assert m.accept == abstract_program(program[:i+1])
        if expected is not None:
            assert m.stack_tags(m.root) == expected
            retained.append((m.root, expected))
    for root, expected in retained:
        assert m.stack_tags(root) == expected
    assert m.max_radius <= 2 and m.max_batch <= 2
    assert all(len(pointers) <= 2 for _, pointers in m.heap)
    return m.max_radius, m.max_batch


BOTTOM = 'bottom'
BAD = 'bad'


def stack_transition(ctrl, op, top):
    """Finite control and just one old stack top determine this transition."""
    kind = op[0]
    action = 'push' if kind == 'E' else 'pop' if kind == 'J' else 'keep'
    if ctrl == BAD:
        return BAD, action, BOTTOM
    try:
        if kind == 'E':
            return (update(op,[]), ctrl is None), 'push', BOTTOM if ctrl is None else ctrl
        if ctrl is None:
            raise ValueError('underflow')
        if kind == 'J':
            if top in (None,BOTTOM):
                raise ValueError('underflow')
            return (update(op,[top[0],ctrl[0]]),top[1]), 'pop', None
        return (update(op,[ctrl[0]]),ctrl[1]), 'keep', None
    except ValueError:
        return BAD, action, BOTTOM


def check_single_edge(program):
    # Instantiate the checked compiler's three rows; base is unlabelled.
    nodes = [(None,None)]
    top = 0
    ctrl = None
    auxiliary = []
    for i, op in enumerate(program):
        label, edge = nodes[top]
        assert label == (auxiliary[-1] if auxiliary else None)
        ctrl, action, value = stack_transition(ctrl,op,label)
        if action == 'push':
            new = (value,top)
            auxiliary.append(value)
        elif action == 'keep':
            new = (label,edge)
        else:
            new = nodes[edge] if edge is not None else (None,None)
            if auxiliary:
                auxiliary.pop()
        nodes.append(new)
        top = len(nodes)-1
        # Universal decoder is supplied by Compile.lean; these are finite checks.
        decoded = []
        cursor = top
        while cursor is not None and nodes[cursor][0] is not None:
            decoded.append(nodes[cursor][0])
            cursor = nodes[cursor][1]
        assert decoded[::-1] == auxiliary
        expected = abstract_stack(program[:i+1])
        assert (ctrl == BAD) == (expected is None)
        accept = ctrl not in (None,BAD) and ctrl[1] and ctrl[0] == ((),1)
        assert accept == abstract_program(program[:i+1])
        if expected is not None:
            assert auxiliary and auxiliary[0] == BOTTOM
            assert [entry[0] for entry in auxiliary[1:]]+[ctrl[0]] == expected
            assert ctrl[1] == (len(expected) == 1)
    assert len(nodes) == len(program)+1
    return len(program)


class TapeMachine:
    """One scanned cell, at most one write and one head move per input token."""
    def __init__(self):
        self.tape = {}  # all blank, including position zero
        self.head = 0
        self.phase = 'ready'
        self.pending = None
        self.accept = False
        self.steps = 0
        self.max_move = 0

    def step(self, symbol):
        self.steps += 1
        cell = self.tape.get(self.head)
        before = self.head
        move = 0
        write = cell
        self.accept = False
        if self.phase == 'bad':
            return
        try:
            if self.phase == 'ready':
                if symbol == '#':
                    raise ValueError('unexpected clock')
                kind = symbol[0]
                if kind == 'E':
                    self.pending = (update(symbol, []), cell is None)
                    move = 1
                    self.phase = 'push'
                elif kind == 'J':
                    if cell is None or cell[1]:
                        raise ValueError('underflow')
                    self.pending = cell[0]
                    write = None
                    move = -1
                    self.phase = 'join'
                else:
                    if cell is None:
                        raise ValueError('underflow')
                    write = (update(symbol, [cell[0]]), cell[1])
                    self.phase = 'idle'
            else:
                if symbol != '#':
                    raise ValueError('missing clock')
                if self.phase == 'push':
                    write = self.pending
                elif self.phase == 'join':
                    if cell is None:
                        raise ValueError('underflow')
                    write = (update(('J',), [cell[0], self.pending]), cell[1])
                self.phase = 'ready'
                self.pending = None
                self.accept = write is not None and write[1] and write[0] == ((),1)
        except ValueError:
            self.phase = 'bad'
            move = 0
            write = cell
        self.tape[self.head] = write
        self.head += move
        self.max_move = max(self.max_move, abs(self.head-before))
        assert self.head >= 0


def encode(program):
    return [s for op in program for s in (op, '#')]


def reference_clock(word):
    if len(word) % 2 or any(word[i] == '#' or word[i+1] != '#' for i in range(0,len(word),2)):
        return False
    return abstract_program(word[::2])


def check_machine(word):
    m = TapeMachine()
    for i, symbol in enumerate(word):
        m.step(symbol)
        assert m.accept == reference_clock(word[:i+1])
    assert m.accept == reference_clock(word)
    assert m.steps == len(word) and m.max_move <= 1
    return m.steps


def run():
    out = {'scope': 'Finite Boolean and literal TM model checks. No proof assistant, no arbitrary-heap verification, no claim that Python data-structure costs satisfy record bounds.'}
    out['bounds'] = {
        'type_counts_and_pins': 'all Boolean relations at b=0,1,2,3',
        'gadgets': 'all literal sign patterns at lengths 4 through 7, plus all Horn positive-literal positions',
        'retained_dags': '1000 seeded attempts, w=2, at most 9 decoded variables and 45 postfix operations; seed 20261001',
        'postfix_words': 'all words through length 4 over the seven listed test opcodes',
        'postfix_test_alphabet': ['Empty_empty','Empty_slot0','Introduce0','Forget0','Add_x0','Add_not_x0','Join'],
        'tm': 'one scanned cell and one move at most per encoded symbol; every tested prefix; initially all blank',
        'record_model': 'two pointer fields, two fresh records, old endpoint paths of length at most two; all earlier tested stacks remain intact',
        'single_edge_model': 'one finite-control stack evaluator and the push/keep/pop scaffold rows, one appended node per unpadded opcode; prefix decoding and acceptance checked',
        'shared_implementation': 'TM and record transitions share finite relation-update tables with the abstract stack; independent CNF enumeration checks table semantics on the stated samples',
        'omitted': 'arbitrary widths/heaps/histories, simultaneous-record compiler execution, generic TM-to-scaffold instantiation, proof-assistant verification and optimality'
    }
    relation_checks = 0
    for b in range(4):
        for r in range(1 << (1 << b)):
            assert sum(1 << a for a in models(synth_relation(b,r),b)) == r
            relation_checks += 1
    out['all_relation_syntheses_b_0_to_3'] = relation_checks
    renames = 0
    for w in range(4):
        for length in range(w+1):
            for slots in combinations(range(w), length):
                for r in range(1 << (1 << length)):
                    f = Flat(length, tuple((s,i+1) for i,s in enumerate(slots)), synth_relation(length,r))
                    for pi in permutations(range(w)):
                        op = ('R',pi)
                        assert update(op, [(slots,r)]) == flat_relation(flat_step(op,[f]))
                        inverse = tuple(pi.index(i) for i in range(w))
                        assert update(('R',inverse), [update(op, [(slots,r)])]) == (slots,r)
                        renames += 1
    out['renaming_checks_all_partial_sorts_w_0_to_3'] = renames
    gadget_checks = 0
    for b in range(4,8):
        for signs in product((-1,1), repeat=b):
            c = tuple(s*(i+1) for i,s in enumerate(signs))
            clauses, nextvar = split_clause(c,b+1)
            projected = {a & ((1<<b)-1) for a in models(clauses,nextvar-1)}
            assert projected == models((c,),b)
            assert max(map(len, clauses)) <= 3
            gadget_checks += 1
        for positive in range(-1,b):
            c = tuple((i+1) if i == positive else -(i+1) for i in range(b))
            clauses, nextvar = split_clause(c,b+1,True)
            assert all(sum(l>0 for l in c) <= 1 for c in clauses)
            assert {a & ((1<<b)-1) for a in models(clauses,nextvar-1)} == models((c,),b)
            gadget_checks += 1
    out['exhaustive_clause_gadgets_lengths_4_to_7'] = gadget_checks
    counts = []
    for b in range(4):
        binary = cnf_closure(b)
        affine = affine_relations(b)
        horn = cnf_closure(b,True)
        # Independent closure characterizations for every Boolean relation.
        majority = set(); meets = set(); parity = set()
        for r in range(1 << (1<<b)):
            vals = [a for a in range(1<<b) if r >> a & 1]
            if all(r >> (a & c) & 1 for a in vals for c in vals):
                meets.add(r)
            if all(r >> ((a & c)|(a & d)|(c & d)) & 1 for a in vals for c in vals for d in vals):
                majority.add(r)
            if all(r >> (a ^ c ^ d) & 1 for a in vals for c in vals for d in vals):
                parity.add(r)
        assert binary == majority and horn == meets and affine == parity
        counts.append({'b':b,'all':1<<(1<<b),'2cnf':len(binary),'affine':len(affine),'horn':len(horn)})
    out['exhaustive_small_type_counts'] = counts
    communication_checks = []
    for b in range(4):
        relations = cnf_closure(b,True)
        checks = max_turns = max_bits = 0
        for left in relations:
            for right in relations:
                answer, turns, bits = horn_protocol(b,left,right)
                assert answer == bool(left & right)
                max_turns = max(max_turns,turns)
                max_bits = max(max_bits,bits)
                checks += 1
        communication_checks.append({'b':b,'pairs':checks,'max_turns':max_turns,'max_communicated_bits':max_bits})
    out['horn_protocol_all_relation_pairs_b_0_to_3'] = communication_checks
    out['horn_middle_layer_families'] = []
    for b in range(2,5):
        t = b//2
        layer = [a for a in range(1<<b) if a.bit_count() == t]
        relations = set()
        for x in range(1<<len(layer)):
            selected = {a for j,a in enumerate(layer) if x >> j & 1}
            clauses = [tuple(-(i+1) for i in range(b) if a >> i & 1)
                       for a in range(1<<b) if (a.bit_count() == t and a not in selected) or a.bit_count() == t+1]
            actual = models(clauses,b)
            expected = {a for a in range(1<<b) if a.bit_count() < t} | selected
            assert actual == expected
            relations.add(tuple(sorted(actual)))
        assert len(relations) == 1<<comb(b,t)
        out['horn_middle_layer_families'].append({'b':b,'distinct':len(relations)})
    # Pins distinguish all pairs for b<=3; bit arithmetic is an independent oracle.
    pins = 0
    for b in range(4):
        for r in range(1 << (1<<b)):
            for t in range(r):
                a = ((r ^ t) & -(r ^ t)).bit_length()-1
                pinclauses = tuple(((i+1) if a >> i & 1 else -(i+1),) for i in range(b))
                pin = sum(1<<v for v in models(pinclauses,b))
                assert bool(r & pin) != bool(t & pin)
                full = (1 << (1<<b))-1
                assert not r & (full ^ r)
                assert r & (full ^ t) or t & (full ^ r)
                pins += 1
    out['distinguishing_pin_pairs'] = pins
    out['disjointness_fooling_pair_checks'] = pins
    # Retained random constructor DAGs; full CNF decoding uses separate witness enumeration.
    rng = Random(20261001)
    pool = [node(('E',s)) for s in ((),(0,),(1,),(0,1))]
    checks = oldchecks = 0
    machine_steps = 0
    programs = []
    record_results = []
    single_edge_steps = 0
    for _ in range(1000):
        a = rng.choice(pool)
        s = a.tag[0]
        options = [('F',i) for i in s] + [('I',i) for i in (0,1) if i not in s]
        options += [('C',(sign*(i+1),)) for i in s for sign in (-1,1)]
        options += [('R',(1,0))]
        if len(s) == 2:
            options += [('C',c) for c in ((1,2),(-1,2),(1,-2),(-1,-2))]
        peers = [p for p in pool if p.tag[0] == s]
        op = rng.choice(options+[('J',)])
        args = (a,rng.choice(peers)) if op[0] == 'J' else (a,)
        h = node(op,*args)
        f = decode(h)
        prog = postfix(h)
        if f.n > 9 or len(prog) > 45:
            continue
        assert h.tag == flat_relation(f)
        checks += 1
        pool.append(h)
        old = rng.choice(pool)
        assert old.tag == flat_relation(decode(old))
        oldchecks += 1
        programs.append(prog)
        record_results.append(check_records(prog))
        single_edge_steps += check_single_edge(prog)
        machine_steps += check_machine(encode(prog))
    out['retained_dag_new_checks'] = checks
    out['retained_old_version_checks'] = oldchecks
    # Explicit private-name hygiene negative control, including zero boundary.
    f = Flat(1,(),((1,),)); g = Flat(1,(),((-1,),))
    assert flat_relation(flat_step(('J',),(f,g))) == ((),1)
    assert not models(f.clauses+g.clauses,1)
    # Positive-only observers miss a distinction visible to negative pins.
    assert models(((1,),),1) != models((),1)
    assert models(((1,),),1) & models(((1,),),1)
    assert not (models(((1,),),1) & models(((-1,),),1))
    out['negative_controls'] = ['private-name capture changes SAT','positive-only observations omit a pin distinction']
    alphabet = [('E',()),('E',(0,)),('I',0),('F',0),('C',(1,)),('C',(-1,)),('J',)]
    exhaustive = 0
    for length in range(5):
        for p in product(alphabet,repeat=length):
            record_results.append(check_records(p))
            single_edge_steps += check_single_edge(p)
            machine_steps += check_machine(encode(p))
            exhaustive += 1
    malformed = 0
    for p in programs[:150]:
        w = encode(p)
        variants = [w[:-1],w[:-2],['#']+w,w+['#']]
        if len(w) >= 3:
            variants += [w[:1]+w[2:], [w[0],('E',()),*w[2:]]]
        for v in variants:
            machine_steps += check_machine(v)
            malformed += 1
    out['clocked_programs_exhaustive_through_4_operations'] = exhaustive
    out['clock_mutations'] = malformed
    out['literal_tape_transitions_checked'] = machine_steps
    out['literal_record_programs_checked'] = len(record_results)
    out['single_edge_scaffold_appends_checked'] = single_edge_steps
    out['maximum_old_endpoint_radius_observed'] = max(r for r,_ in record_results)
    out['maximum_fresh_records_observed'] = max(a for _,a in record_results)
    out['universal_status'] = 'Theorems, view inequality and resource bounds are written proofs. The single-edge compiler has finite instances checked here and a prior Lean proof. This program does not certify unrestricted theorems, generic compiler correctness, or optimality.'
    root = Path(__file__).resolve().parents[3]
    paths = [
        'public/research-artifacts/foundations/sat-boundary-dynamics.md',
        'public/research-artifacts/foundations/verify_sat_boundary.py',
        'public/research-artifacts/foundations/foundational-contracts.md',
        'public/formal/persistent-stacks/lean/FPRDTransfer/RealtimeTransfer.lean',
        'public/formal/persistent-stacks/lean/FPRDTransfer/TapeZipper.lean',
        'public/formal/persistent-stacks/lean/FPRDTransfer/StackMachine.lean',
        'public/formal/persistent-stacks/lean/FPRDTransfer/Compile.lean',
    ]
    out['source_sha256'] = {p: hashlib.sha256((root/p).read_bytes()).hexdigest() for p in paths}
    return out


if __name__ == '__main__':
    print(json.dumps(run(),indent=2))