verify_clocked_horn.py

#!/usr/bin/env python3
"""Specification checks. Does not extract the full Horn primitive program."""
from pathlib import Path
import hashlib
import itertools
import json
import random

DATA = set('u:BFGDRE;01abcd+-')

class Invalid(Exception):
    pass


def parse(text):
    i = 0
    def take(want=None):
        nonlocal i
        if i == len(text):
            raise Invalid('truncated')
        c = text[i]
        i += 1
        if want is not None and c != want:
            raise Invalid('symbol')
        return c
    width = 0
    while i < len(text) and text[i] == 'u':
        take('u'); width += 1
    if not width:
        raise Invalid('empty header')
    take(':'); take('B')
    def key():
        out = ''
        for _ in range(width):
            c = take()
            if c not in '01':
                raise Invalid('key')
            out += c
        return out
    def declarations(stop):
        out = set()
        while i < len(text) and text[i] != stop:
            name = key(); take(';')
            if name in out:
                raise Invalid('duplicate declaration')
            out.add(name)
        return out
    boundary = declarations('F')
    programs = []
    for side, stop in (('F', 'G'), ('G', 'E')):
        take(side); take('D')
        private = declarations('R')
        if boundary & private:
            raise Invalid('boundary collision')
        take('R')
        identifiers = set()
        rules = []
        def semantic(name):
            if name not in boundary | private:
                raise Invalid('undeclared')
            return ('B' if name in boundary else side, name)
        while i < len(text) and text[i] != stop:
            ident = key()
            if ident in identifiers:
                raise Invalid('duplicate rule')
            identifiers.add(ident)
            arity = take()
            if arity not in 'abcd':
                raise Invalid('arity')
            count = 'abcd'.index(arity)
            sign = take()
            if sign == '+':
                if count > 2:
                    raise Invalid('positive arity')
                head = semantic(key())
            elif sign == '-':
                head = None
            else:
                raise Invalid('head')
            body = tuple(semantic(key()) for _ in range(count))
            take(';')
            if len(set(body)) != len(body) or head in body:
                raise Invalid('not normalized')
            rules.append((body, head))
        programs += rules
    take('E')
    if i != len(text):
        raise Invalid('trailing')
    return programs


def closure(rules):
    truth = set()
    while True:
        old = set(truth)
        for body, head in rules:
            if set(body) <= truth:
                if head is None:
                    return False
                truth.add(head)
        if truth == old:
            return True


def brute(rules):
    variables = sorted({v for body, h in rules for v in (*body, h) if v is not None})
    for mask in range(1 << len(variables)):
        true = {v for j, v in enumerate(variables) if mask & (1 << j)}
        if all(not set(body) <= true or head in true for body, head in rules):
            return True
    return False


def encode(width, boundary, left, right):
    def k(v):
        return format(v, f'0{width}b')
    def side(label, item):
        private, rules = item
        s = label + 'D' + ''.join(k(v)+';' for v in private) + 'R'
        for j, (body, head) in enumerate(rules):
            s += k(j) + 'abcd'[len(body)] + ('-' if head is None else '+'+k(head))
            s += ''.join(k(v) for v in body) + ';'
        return s
    return 'u'*width + ':B' + ''.join(k(v)+';' for v in boundary) + side('F',left) + side('G',right) + 'E'


def wrapper(word, C, steps, answer):
    # Frozen (label,next) cells; fuel shares the original reverse input.
    raw = None
    phase = 'load'
    fuel = None
    residue = C
    done = 0
    for ch in word:
        if phase == 'load':
            if ch in DATA:
                raw = (ch, raw)
            elif ch == '#':
                fuel = ('sentinel', raw)
                phase = 'run'
            else:
                return False
        elif phase == 'run':
            if ch == 't':
                if fuel is None:
                    return False
                done += done < steps
                residue -= 1
                if residue == 0:
                    fuel = fuel[1]
                    residue = C
            elif ch == '!':
                if fuel is not None or done < steps or not answer:
                    return False
                phase = 'accept'
            else:
                return False
        else:
            return False
    return phase == 'accept'


def main():
    rng = random.Random(3901)
    examples = []
    for _ in range(500):
        boundary = [0, 1]
        sides = []
        for _ in range(2):
            rules = []
            for j in range(rng.randrange(7)):
                h = rng.choice([None, 0, 1, 2])
                candidates = [v for v in range(3) if v != h]
                body = tuple(rng.sample(candidates, rng.randrange(min(len(candidates),3 if h is None else 2)+1)))
                rules.append((body,h))
            sides.append(([2],rules))
        x = encode(3,boundary,*sides)
        rules = parse(x)
        assert closure(rules) == brute(rules)
        examples.append(x)
    # Same private spelling has independent meaning on the two sides.
    separated = encode(1,[],([0],[((),0)]),([0],[((0,),None)]))
    assert closure(parse(separated))
    shared = encode(1,[0],([] ,[((),0)]),([],[((0,),None)]))
    assert not closure(parse(shared))
    empty = encode(1,[],([],[]),([],[]))
    assert closure(parse(empty))
    malformed = ['', 'u:BFD RGDRE', empty+'0', empty[1:],
                 encode(1,[0,0],([],[]),([],[])),
                 encode(1,[0],([0],[]),([],[])),
                 encode(1,[],([],[((),0)]),([],[])),
                 encode(2,[0,1],([], [((0,0),1)]),([],[])),
                 encode(2,[0],([], [((0,),0)]),([],[])),
                 encode(2,[0,1,2],([], [((0,1,2),0)]),([],[]))]
    for x in malformed:
        try:
            parse(x)
        except Invalid:
            pass
        else:
            raise AssertionError(('accepted malformed',x))
    prefix_rejections = 0
    for x in examples[:20]:
        for j in range(len(x)):
            try:
                parse(x[:j])
            except Invalid:
                prefix_rejections += 1
            else:
                raise AssertionError('accepted truncation')
    clocks = 0
    for M in range(9):
        x = 'u'*M
        for C in range(1,5):
            budget = C*(M+1)
            for runtime in range(budget+3):
                for count in range(budget+3):
                    for ans in (False,True):
                        word = x+'#'+'t'*count+'!'
                        expected = ans and runtime <= budget and count == budget
                        assert wrapper(word,C,runtime,ans) == expected
                        clocks += 1
    bad_shapes = ['t#t!', '#!t', 'u##tt!', 'u#utt!', 'u#tt!!', '!']
    for w in bad_shapes:
        assert not wrapper(w,1,0,True)
    # Quadratic runner defeats fixed linear fuel; not a language lower bound.
    assert not wrapper('u'*20+'#'+'t'*(3*21)+'!',3,400,True)
    here = Path(__file__).resolve().parent
    names = ['clocked-horn-transfer.md','verify_clocked_horn.py','persistent-horn-closure.md']
    result = {'status':'passed','random_valid_horn_pair_oracle_checks':len(examples),
              'malformed_cases':len(malformed), 'rejected_truncated_prefixes':prefix_rejections,
              'exact_fuel_wrapper_cases':clocks, 'private_name_separation':'passed',
              'quadratic_runtime_negative_control':'passed',
              'scope':'Grammar/semantic specification and fuel-wrapper finite checks. No extracted Horn primitive program, decimal clock constant, compiled scaffold, or Lean proof.',
              'sha256':{name:hashlib.sha256((here/name).read_bytes()).hexdigest() for name in names}}
    (here/'clocked-horn-output.json').write_text(json.dumps(result,indent=2)+'\n')
    print(json.dumps(result,indent=2))

if __name__ == '__main__':
    main()