From 52e26c1b80b8b67a1e8f586c3c6d41e74e104686 Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 09:58:54 -0500 Subject: [PATCH 1/3] Construct conditioned positive-definite dirty circuit witnesses --- research/spd-dirty-circuit-witness/NOTICE.md | 21 ++ research/spd-dirty-circuit-witness/PROOF.md | 108 ++++++++ research/spd-dirty-circuit-witness/README.md | 60 +++++ .../spd-dirty-circuit-witness/RESULT.json | 70 +++++ .../spd-dirty-circuit-witness/SOURCES.json | 53 ++++ research/spd-dirty-circuit-witness/TASK.json | 95 +++++++ .../spd-dirty-circuit-witness/VERIFY.json | 34 +++ research/spd-dirty-circuit-witness/literal.py | 97 +++++++ .../vendor/fields.py | 140 ++++++++++ .../vendor/linear_words.py | 250 ++++++++++++++++++ research/spd-dirty-circuit-witness/verify.py | 188 +++++++++++++ research/spd-dirty-circuit-witness/witness.py | 69 +++++ .../wrong-order.json | 76 ++++++ 13 files changed, 1261 insertions(+) create mode 100644 research/spd-dirty-circuit-witness/NOTICE.md create mode 100644 research/spd-dirty-circuit-witness/PROOF.md create mode 100644 research/spd-dirty-circuit-witness/README.md create mode 100644 research/spd-dirty-circuit-witness/RESULT.json create mode 100644 research/spd-dirty-circuit-witness/SOURCES.json create mode 100644 research/spd-dirty-circuit-witness/TASK.json create mode 100644 research/spd-dirty-circuit-witness/VERIFY.json create mode 100644 research/spd-dirty-circuit-witness/literal.py create mode 100644 research/spd-dirty-circuit-witness/vendor/fields.py create mode 100644 research/spd-dirty-circuit-witness/vendor/linear_words.py create mode 100644 research/spd-dirty-circuit-witness/verify.py create mode 100644 research/spd-dirty-circuit-witness/witness.py create mode 100644 research/spd-dirty-circuit-witness/wrong-order.json diff --git a/research/spd-dirty-circuit-witness/NOTICE.md b/research/spd-dirty-circuit-witness/NOTICE.md new file mode 100644 index 0000000000..04f89cf1f2 --- /dev/null +++ b/research/spd-dirty-circuit-witness/NOTICE.md @@ -0,0 +1,21 @@ +# Attribution and frozen source + +New proof, degree adapter, literal replay and checks: Ali Romman, with substantial +OpenAI Codex assistance. Apache-2.0. + +The two files in vendor and wrong-order.json are unchanged copies from +[PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), head +`48976daa4dce59b4867ef046da72a370e389925d`. The source is prepared for zxv with +substantial OpenAI Codex assistance, under Apache-2.0. This PR is pending and +is not part of our main base. SOURCES.json records each original path, Git blob +and SHA256. The replay checks the copied bytes. References inside the unchanged +vendor files refer to the predecessor's proof, not to a claim of our authorship. + +Retain its weighted-automata/PIT credit to Stefan Kiefer and Ran Raz / Amir +Shpilka. The echo lineage credits androolloyd, Chafik Boukhalfa / chafreaky +[PR #628](https://github.com/CrocSwap/integer-mult-bounds/pull/628), and Ali Romman +[PR #621](https://github.com/CrocSwap/integer-mult-bounds/pull/621). +The source also retains Cinna Davis, ToikY, Sagar Thakrar, roger-sato, Charles +Bethin, Ross Richardson and the wider dirty-phase/tensor lineage. Their results +are not new results of this package. No identities are inferred from a PR's +submitter account. The source README and proof are pinned provenance. diff --git a/research/spd-dirty-circuit-witness/PROOF.md b/research/spd-dirty-circuit-witness/PROOF.md new file mode 100644 index 0000000000..b4af353647 --- /dev/null +++ b/research/spd-dirty-circuit-witness/PROOF.md @@ -0,0 +1,108 @@ +# Positive-definite separation of complete dirty circuits + +## Statement + +Use the complete linear register grammar from zxv's [PR #5235](https://github.com/CrocSwap/integer-mult-bounds/pull/5235), +head `48976daa4dce59b4867ef046da72a370e389925d`. All input and returned roles +are independent. Coefficients are central elements of Q or Q(i). Symbols have +no inverse, commutation, Clifford or other relations. Compare two finite +programs, or compare one program with an explicit polynomial endpoint. + +Let F be their matrix of noncommutative polynomial differences. If F is +nonzero, let D be the largest word degree with a nonzero coefficient in any +entry. For every rational 0 < e <= 1/4, there are real symmetric rational +matrices A_a of dimension D+1 such that: + +- every spectrum is contained in [1-2e,1]; +- each matrix is positive definite, has operator norm at most 1, and has + spectral condition number at most 1/(1-2e) <= 2; +- the literal complete endpoint difference is nonzero for one input role + equal to a coordinate vector and all other roles equal to zero. + +Thus identity on this class, in every payload dimension, is equivalent to +free-polynomial identity. Taking e arbitrarily small also gives witnesses +arbitrarily close to I in operator norm. This statement gives no lower bound +on numerical detectability. The nonzero discrepancy can be exponentially small. + +## Construction and proof + +Choose an entry (o,i) and a degree-D word w=a_1...a_D with coefficient c != 0. +Number the path vertices 0,...,D. Let S_a contain both symmetric entries +(j-1,j) and (j,j-1) exactly when a_j=a. All other entries are zero. Put + + A_a = (1-e)I + (e/2) S_a. + +Each S_a is real symmetric and has absolute row sum at most 2. For every real +vector x, the inequality 2|x_j x_k| <= x_j^2+x_k^2 gives +|x^T S_a x| <= 2||x||_2^2. The spectral interval for A_a is therefore +[1-2e,1]. The same statement applies on complex payload space. + +In a product of k <= D such matrices, a path from vertex 0 to vertex D must +make D steps. Each factor can stay at its vertex or move one edge. If k= 0 else "")+str(self.imag)+"i" + + __repr__ = __str__ + + +def scalars(problem): + p = problem.get("field", "Q") + if p == "Q": + return Fraction + if p == "Qi": + return Gaussian + if type(p) is not int: + raise ValueError("field must be Q, Qi or a prime at most 2^31-1") + return prime_scalars(p) + + +@lru_cache(maxsize=32) +def prime_scalars(p): + if not 2 <= p <= 2**31-1 or any(p % d == 0 for d in range(2, isqrt(p)+1)): + raise ValueError("field must be Q, Qi or a prime at most 2^31-1") + + class Prime: + def __init__(self, x=0): + if isinstance(x, Prime): + self.value = x.value + else: + q = Fraction(x) + self.value = q.numerator*pow(q.denominator, -1, p) % p + + def __add__(self, other): + return Prime(self.value+Prime(other).value) + + __radd__ = __add__ + + def __mul__(self, other): + return Prime(self.value*Prime(other).value) + + __rmul__ = __mul__ + + def __neg__(self): + return Prime(-self.value) + + def __sub__(self, other): + return self+-Prime(other) + + def __rsub__(self, other): + return Prime(other)+-self + + def __truediv__(self, other): + return Prime(self.value*pow(Prime(other).value, -1, p)) + + def __rtruediv__(self, other): + return Prime(other)/self + + def __eq__(self, other): + return self.value == Prime(other).value + + def __bool__(self): + return bool(self.value) + + def __str__(self): + return str(self.value) + + __repr__ = __str__ + + return Prime diff --git a/research/spd-dirty-circuit-witness/vendor/linear_words.py b/research/spd-dirty-circuit-witness/vendor/linear_words.py new file mode 100644 index 0000000000..4a877e1ab9 --- /dev/null +++ b/research/spd-dirty-circuit-witness/vendor/linear_words.py @@ -0,0 +1,250 @@ +"""Exact free-algebra certificates for complete dirty linear programs. + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. +Reachable-space equivalence is classical; see PROOF.md for attribution. +""" +from collections import deque +from fractions import Fraction as Q +import argparse +import hashlib +import json +from pathlib import Path +import sys +sys.path.insert(0, str(Path(__file__).resolve().parent)) +from fields import scalars + + +def need(test, message): + if not test: + raise ValueError(message) + + +def number(value, scalar=Q): + need(type(value) in (int, str), "coefficient must be an integer or exact scalar string") + return scalar(value) + + +def index(value, n): + need(type(value) is int and 0 <= value < n, "role index out of range") + return value + + +def add(a, b, scale=Q(1)): + out = a.copy() + for j, x in b.items(): + out[j] = out.get(j, Q(0)) + scale*x + if not out[j]: + del out[j] + return out + + +def scaled(a, c): + return {j: c*x for j, x in a.items() if c*x} + + +def digest(problem): + return hashlib.sha256(json.dumps(problem, sort_keys=True, separators=(",", ":")).encode()).hexdigest() + + +class Machine: + def __init__(self, roles, scalar=Q): + self.roles = roles + self.scalar = scalar + self.states = roles + self.edges = {} + self.final = {i: i for i in range(roles)} + self.initial = [{i: scalar(1)} for i in range(roles)] + + def atom(self, symbol, row): + need(type(symbol) is str and bool(symbol), "nonempty operator symbol required") + j = self.states + self.states += 1 + self.edges.setdefault(symbol, {})[j] = row.copy() + return {j: self.scalar(1)} + + def step(self, row, symbol): + out = {} + edges = self.edges.get(symbol, {}) + for i, c in row.items(): + out = add(out, edges.get(i, {}), c) + return out + + def terminal(self, row): + out = {} + for i, c in row.items(): + if i in self.final: + j = self.final[i] + out[j] = out.get(j, Q(0)) + c + if not out[j]: + del out[j] + return out + + +def program_machine(roles, instructions, shifted=False, scalar=Q): + need(type(instructions) is list, "program must be a list") + m = Machine(roles, scalar) + rows = m.initial + for op in instructions: + need(type(op) is dict and type(op.get("op")) is str, "instruction object required") + kind = op["op"] + allowed = { + "add": {"op", "src", "dst", "coefficient"}, + "query": {"op", "src", "dst", "symbol", "coefficient"}, + "apply": {"op", "dst", "symbol"}, + "scale": {"op", "dst", "coefficient"}, + "swap": {"op", "src", "dst"}, + } + need(kind in allowed and not (op.keys()-allowed[kind]), "unknown instruction or key") + dst = index(op.get("dst"), roles) + if kind in ("add", "query", "swap"): + src = index(op.get("src"), roles) + if kind == "swap": + rows[src], rows[dst] = rows[dst], rows[src] + elif kind == "scale": + rows[dst] = scaled(rows[dst], number(op["coefficient"], scalar)) + elif kind == "add": + rows[dst] = add(rows[dst], rows[src], number(op.get("coefficient", 1), scalar)) + else: + old = rows[dst if kind == "apply" else src].copy() + atom = m.atom(op.get("symbol"), old) + image = add(old, atom) if shifted else atom + if kind == "apply": + rows[dst] = image + else: + rows[dst] = add(rows[dst], image, number(op.get("coefficient", 1), scalar)) + return m + + +def target_machine(roles, target, shifted=False, scalar=Q): + need(type(target) is dict and not (target.keys()-{"identity", "terms"}), "invalid target") + need(type(target.get("identity", True)) is bool, "identity must be Boolean") + need(type(target.get("terms", [])) is list, "terms must be a list") + m = Machine(roles, scalar) + out = [{i: scalar(1)} if target.get("identity", True) else {} for i in range(roles)] + for term in target.get("terms", []): + need(type(term) is dict and not (term.keys()-{"out", "in", "word", "coefficient"}), "invalid target term") + i, j = index(term.get("out"), roles), index(term.get("in"), roles) + word = term.get("word") + need(type(word) is list, "word must be an ordered symbol list") + row = {j: scalar(1)} + for a in reversed(word): + atom = m.atom(a, row) + row = add(row, atom) if shifted else atom + out[i] = add(out[i], row, number(term.get("coefficient", 1), scalar)) + m.initial = out + return m + + +def compile_problem(problem, shifted=False): + need(type(problem) is dict and not (problem.keys()-{"field", "roles", "program", "reference", "target"}), "invalid problem keys") + scalar = scalars(problem) + n = problem.get("roles") + need(type(n) is int and n > 0, "positive role count required") + need(("reference" in problem) != ("target" in problem), "provide exactly one reference or target") + a = program_machine(n, problem["program"], shifted, scalar) + b = (program_machine(n, problem["reference"], shifted, scalar) if "reference" in problem + else target_machine(n, problem["target"], shifted, scalar)) + m = Machine(n, scalar) + m.states = a.states+b.states + shift = lambda row: {j+a.states: x for j, x in row.items()} + m.initial = [add(x, shift(y), Q(-1)) for x, y in zip(a.initial, b.initial)] + m.final = dict(a.final) + m.final.update({j+a.states: v for j, v in b.final.items()}) + m.edges = {s: dict(rows) for s, rows in a.edges.items()} + for s, rows in b.edges.items(): + m.edges.setdefault(s, {}).update({j+a.states: shift(v) for j, v in rows.items()}) + return m + + +class Span: + """Incremental elimination with coordinates in the original reachable rows.""" + def __init__(self): + self.rows = [] + self.echelon = [] + + def reduce(self, row): + row = row.copy() + coords = {} + for pivot, basis, rep in self.echelon: + c = row.get(pivot, Q(0)) + if c: + row = add(row, basis, -c) + coords = add(coords, rep, c) + return row, coords + + def insert(self, row): + rest, coords = self.reduce(row) + if not rest: + return False + j = len(self.rows) + self.rows.append(row) + pivot = min(rest) + c = 1/rest[pivot] + rep = scaled(add({j: Q(1)}, coords, Q(-1)), c) + self.echelon.append((pivot, scaled(rest, c), rep)) + self.echelon.sort(key=lambda item: item[0]) + return True + + def coordinates(self, row): + rest, coords = self.reduce(row) + need(not rest, "internal invariant space is not closed") + return coords + + +def packed(row): + return {str(j): str(x) for j, x in sorted(row.items())} + + +def decide(problem, shifted=False): + m = compile_problem(problem, shifted) + alphabet = sorted(m.edges) + span, paths, queue = Span(), [], deque() + + def consider(row, output, word): + terminal = m.terminal(row) + if terminal: + j = min(terminal) + return {"schema": "dirty-linear-certificate/v1", "problem_sha256": digest(problem), + "equivalent": False, "shifted": shifted, "states": m.states, + "output": output, "input": j, "word": word, + "coefficient": str(terminal[j]), "matrix_dimension": len(word)+1} + if span.insert(row): + paths.append({"output": output, "word": word}) + queue.append(len(paths)-1) + return None + + for i, row in enumerate(m.initial): + bad = consider(row, i, []) + if bad: + return bad + while queue: + k = queue.popleft() + for a in alphabet: + p = paths[k] + bad = consider(m.step(span.rows[k], a), p["output"], p["word"]+[a]) + if bad: + return bad + return {"schema": "dirty-linear-certificate/v1", "problem_sha256": digest(problem), + "equivalent": True, "shifted": shifted, "states": m.states, + "paths": paths, "initial": [packed(span.coordinates(row)) for row in m.initial], + "closure": {a: [packed(span.coordinates(m.step(row, a))) for row in span.rows] + for a in alphabet}} + + +def main(): + ap = argparse.ArgumentParser(description=__doc__) + ap.add_argument("problem", type=Path) + ap.add_argument("--invertible", action="store_true", help="use X=I+Y to construct unipotent witnesses") + ap.add_argument("--output", type=Path, help="new certificate path; never overwritten") + args = ap.parse_args() + cert = decide(json.loads(args.problem.read_text()), args.invertible) + data = json.dumps(cert, indent=2, sort_keys=True)+"\n" + if args.output: + with args.output.open("x") as stream: + stream.write(data) + else: + print(data, end="") + + +if __name__ == "__main__": + main() diff --git a/research/spd-dirty-circuit-witness/verify.py b/research/spd-dirty-circuit-witness/verify.py new file mode 100644 index 0000000000..c302070078 --- /dev/null +++ b/research/spd-dirty-circuit-witness/verify.py @@ -0,0 +1,188 @@ +"""Exact differential and literal checks for the bounded-condition witness. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +""" +import argparse +from copy import deepcopy +from fractions import Fraction as Q +import hashlib +import json +from pathlib import Path +import random +import sys + +HERE = Path(__file__).resolve().parent +sys.path.insert(0, str(HERE)) +from witness import produce +from literal import check, endpoint, action, require +from fields import scalars + + +def expanded(problem): + scalar = scalars(problem) + initial = [{(j, ()): scalar(1)} for j in range(problem['roles'])] + + def combine(a, b, c): + out = a.copy() + for key, x in b.items(): + out[key] = out.get(key, scalar(0))+c*x + return {key: x for key, x in out.items() if x} + + def run(ops): + rows = [row.copy() for row in initial] + for op in ops: + d, kind = op['dst'], op['op'] + if kind == 'swap': + s = op['src']; rows[d], rows[s] = rows[s], rows[d] + elif kind == 'scale': + rows[d] = combine({}, rows[d], scalar(op['coefficient'])) + else: + value = rows[d if kind == 'apply' else op['src']].copy() + if kind in ('apply', 'query'): + value = {(j, (op['symbol'],)+word): x for (j, word), x in value.items()} + rows[d] = value if kind == 'apply' else combine(rows[d], value, scalar(op.get('coefficient', 1))) + return rows + + left = run(problem['program']) + if 'reference' in problem: + right = run(problem['reference']) + else: + t = problem['target'] + right = [row.copy() if t.get('identity', True) else {} for row in initial] + for term in t.get('terms', []): + d = term['out'] + right[d] = combine(right[d], {(term['in'], tuple(term['word'])): scalar(term.get('coefficient', 1))}, scalar(1)) + return [combine(a, b, scalar(-1)) for a, b in zip(left, right)] + + +def reject(fn): + try: + fn() + except (ValueError, KeyError, TypeError): + return + raise ValueError('control accepted') + + +def fixtures(): + rng = random.Random(5260) + count = negative = positive = 0 + for field in ('Q', 'Qi'): + for size in range(1, 5): + for trial in range(30): + ops = [] + for _ in range(12): + kind = rng.choice(('add', 'query', 'scale', 'swap', 'apply')) + op = {'op': kind, 'dst': rng.randrange(size)} + if kind in ('add', 'query', 'swap'): op['src'] = rng.randrange(size) + if kind in ('query', 'apply'): op['symbol'] = rng.choice(('X', 'Y', 'Z')) + if kind in ('add', 'query', 'scale'): + op['coefficient'] = rng.choice(('0', '1', '-1', '2/3', '1+i') if field == 'Qi' else ('0', '1', '-1', '2/3')) + ops.append(op) + problem = {'roles': size, 'field': field, 'program': ops, + 'reference': ops if trial % 5 == 0 else []} + polynomial = expanded(problem) + degrees = [len(word) for row in polynomial for _, word in row] + cert = produce(problem) + require(cert['equivalent'] == (not degrees), 'equivalence differs from expansion') + if degrees: + require(len(cert['word']) == max(degrees), 'wrong top degree') + actual = polynomial[cert['output']][(cert['input'], tuple(cert['word']))] + require(str(actual) == cert['coefficient'], 'wrong top coefficient') + for epsilon in (Q(1, 4), Q(1, 64)): + check(problem, produce(problem, epsilon)) + negative += 1 + else: + positive += 1 + count += 1 + return {'differential_circuits': count, 'negative_circuits': negative, + 'equivalent_circuits': positive, 'literal_replays': 2*negative} + + +def controls(): + # A shortest constant witness fails at X=3I/4, but the degree-one path succeeds. + p = {'roles': 1, 'program': [{'op': 'apply', 'dst': 0, 'symbol': 'X'}], + 'target': {'identity': False, 'terms': [{'out': 0, 'in': 0, 'word': [], 'coefficient': '3/4'}]}} + c = produce(p) + require(c['word'] == ['X'] and check(p, c) == '1/8', 'highest-degree control') + require(endpoint(p, [[Q(1)]], [], Q(1, 4)) == [[Q(0)]], 'constant witness must fail') + for key, value in [('word', []), ('coefficient', '-1'), ('input', 1), ('output', 1), + ('epsilon', '0'), ('epsilon', '1/2'), ('dimension', 1), + ('spectral_interval', ['0', '1']), ('problem_sha256', '0'*64), + ('equivalent', True)]: + mutant = deepcopy(c); mutant[key] = value + reject(lambda: check(p, mutant)) + reject(lambda: produce(dict(p, field=2))) + reject(lambda: produce(p, 0)) + # A returned dirty helper can fail while the requested data role is unchanged. + dirty = {'roles': 2, 'program': [{'op': 'query', 'src': 1, 'dst': 1, 'symbol': 'X'}], 'reference': []} + d = produce(dirty); require((d['output'], d['input']) == (1, 1), 'dirty role omitted'); check(dirty, d) + # A commutator must not vanish under the symmetric path substitution. + comm = {'roles': 1, 'program': [], 'target': {'terms': [ + {'out': 0, 'in': 0, 'word': ['X', 'Y']}, + {'out': 0, 'in': 0, 'word': ['Y', 'X'], 'coefficient': -1}]}} + check(comm, produce(comm)) + return 15 + + +def stress(): + ops = [] + for _ in range(64): + ops.extend([{'op': 'scale', 'dst': 1, 'coefficient': 0}, + {'op': 'query', 'src': 0, 'dst': 1, 'symbol': 'X'}, + {'op': 'query', 'src': 0, 'dst': 1, 'symbol': 'Y'}, + {'op': 'swap', 'src': 0, 'dst': 1}]) + p = {'roles': 2, 'program': ops, 'target': {'identity': False}} + cert = produce(p) + require(len(cert['word']) == 64, 'stress degree') + difference = check(p, cert) + require(Q(difference) == Q(1, 8)**64, 'stress endpoint') + return {'expanded_top_words': 2**64, 'degree': 64, 'dimension': cert['dimension'], + 'states': cert['statistics']['states'], + 'maximum_layer_dimension': max(cert['statistics']['layer_dimensions']), + 'sum_layer_dimensions': sum(cert['statistics']['layer_dimensions']), + 'discrepancy': difference} + + +def spectral_checks(): + cases = 0 + for length in range(16): + word = ['X' if j % 3 else 'Y' for j in range(length)] + for epsilon in (Q(1, 4), Q(1, 64)): + for symbol in ('X', 'Y', 'Z'): + n = length+1 + columns = [action([Q(int(i == j)) for i in range(n)], symbol, word, epsilon) for j in range(n)] + require(all(columns[j][i] == columns[i][j] for i in range(n) for j in range(n)), 'not symmetric') + for i in range(n): + radius = sum(abs(columns[j][i]) for j in range(n) if j != i) + require(columns[i][i]-radius >= 1-2*epsilon and columns[i][i]+radius <= 1, 'spectral enclosure') + cases += 1 + return cases + + +def main(): + ap = argparse.ArgumentParser() + ap.add_argument('--write', action='store_true') + ap.add_argument('--small', action='store_true') + args = ap.parse_args() + report = {'fixtures': fixtures(), 'controls': controls(), 'spectral_matrices': spectral_checks()} + if args.small: + print(json.dumps(report, sort_keys=True)); return + report['stress'] = stress() + example = json.loads((HERE/'wrong-order.json').read_text()) + cert = produce(example) + report['source_example'] = {'certificate': cert, 'discrepancy': check(example, cert)} + sources = json.loads((HERE/'SOURCES.json').read_text()) + for f in ('fields.py', 'linear_words.py', 'wrong-order.json'): + row = next(r for r in sources['files'] if r['path'].endswith('/'+f)) + require(hashlib.sha256(((HERE/'vendor'/f) if f.endswith('.py') else (HERE/f)).read_bytes()).hexdigest() == row['sha256'], 'vendor drift') + names = sorted(p for p in HERE.rglob('*') if p.is_file() and '__pycache__' not in p.parts and p.name != 'RESULT.json') + report['files'] = {p.relative_to(HERE).as_posix(): hashlib.sha256(p.read_bytes()).hexdigest() for p in names} + if args.write: + (HERE/'RESULT.json').write_text(json.dumps(report, indent=2, sort_keys=True)+'\n') + else: + require(report == json.loads((HERE/'RESULT.json').read_text()), 'receipt drift') + print('PASS_SPD_DIRTY_WITNESS ' + json.dumps({k: v for k, v in report.items() if k != 'files'}, sort_keys=True)) + + +if __name__ == '__main__': + main() diff --git a/research/spd-dirty-circuit-witness/witness.py b/research/spd-dirty-circuit-witness/witness.py new file mode 100644 index 0000000000..fbe2d22f2d --- /dev/null +++ b/research/spd-dirty-circuit-witness/witness.py @@ -0,0 +1,69 @@ +"""Construct well-conditioned counterexamples for dirty linear programs. + +Ali Romman, with substantial OpenAI Codex assistance. Apache-2.0. +The unchanged compiler in vendor is prepared for zxv; see NOTICE.md. +""" +import argparse +from fractions import Fraction as Q +import json +from pathlib import Path +import sys + +sys.path.insert(0, str(Path(__file__).resolve().parent / 'vendor')) +from linear_words import Span, compile_problem, digest, need + + +def top_coefficient(problem): + """Keep a separate reachable space for each exact word length.""" + need(problem.get('field', 'Q') in ('Q', 'Qi'), 'ordered witness requires Q or Qi') + machine = compile_problem(problem) + alphabet = sorted(machine.edges) + candidates = [(row, output, []) for output, row in enumerate(machine.initial)] + last = None + widths = [] + for degree in range(machine.states): + span = Span() + paths = [] + for row, output, word in candidates: + if span.insert(row): + paths.append((output, word)) + terminal = machine.terminal(row) + if terminal: + source = min(terminal) + last = {'output': output, 'input': source, 'word': word, + 'coefficient': str(terminal[source])} + widths.append(len(paths)) + if not paths: + break + candidates = [(machine.step(row, symbol), output, word + [symbol]) + for row, (output, word) in zip(span.rows, paths) + for symbol in alphabet] + need(all(not row for row, _, _ in candidates) or widths[-1] == 0, + 'coefficient machine is not acyclic') + return last, {'states': machine.states, 'layer_dimensions': widths, + 'alphabet': alphabet} + + +def produce(problem, epsilon=Q(1, 4)): + epsilon = Q(epsilon) + need(0 < epsilon <= Q(1, 4), 'epsilon must be in (0,1/4]') + top, stats = top_coefficient(problem) + result = {'schema': 'spd-dirty-witness/v1', 'problem_sha256': digest(problem), + 'equivalent': top is None, 'statistics': stats} + if top is not None: + result.update(top) + result.update({'epsilon': str(epsilon), 'dimension': len(top['word']) + 1, + 'spectral_interval': [str(1-2*epsilon), '1']}) + return result + + +def main(): + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('problem', type=Path) + parser.add_argument('--epsilon', default='1/4') + args = parser.parse_args() + print(json.dumps(produce(json.loads(args.problem.read_text()), Q(args.epsilon)), indent=2)) + + +if __name__ == '__main__': + main() diff --git a/research/spd-dirty-circuit-witness/wrong-order.json b/research/spd-dirty-circuit-witness/wrong-order.json new file mode 100644 index 0000000000..85482942f0 --- /dev/null +++ b/research/spd-dirty-circuit-witness/wrong-order.json @@ -0,0 +1,76 @@ +{ + "roles": 4, + "program": [ + { + "op": "query", + "src": 0, + "dst": 2, + "symbol": "A0", + "coefficient": 1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": 1 + }, + { + "op": "query", + "src": 3, + "dst": 1, + "symbol": "A2", + "coefficient": 1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": -1 + }, + { + "op": "query", + "src": 0, + "dst": 2, + "symbol": "A0", + "coefficient": -1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": 1 + }, + { + "op": "query", + "src": 3, + "dst": 1, + "symbol": "A2", + "coefficient": -1 + }, + { + "op": "query", + "src": 2, + "dst": 3, + "symbol": "A1", + "coefficient": -1 + } + ], + "target": { + "identity": true, + "terms": [ + { + "out": 1, + "in": 0, + "word": [ + "A0", + "A1", + "A2" + ], + "coefficient": 1 + } + ] + } +} From 46bdee8dff4254afd2ed773e7f6c263156c6f84d Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 10:29:22 -0500 Subject: [PATCH 2/3] Retain the compiler proof and attribution with its frozen source --- .../vendor/UPSTREAM-PROOF.md | 191 ++++++++++++++++++ .../vendor/UPSTREAM-README.md | 133 ++++++++++++ 2 files changed, 324 insertions(+) create mode 100644 research/spd-dirty-circuit-witness/vendor/UPSTREAM-PROOF.md create mode 100644 research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md diff --git a/research/spd-dirty-circuit-witness/vendor/UPSTREAM-PROOF.md b/research/spd-dirty-circuit-witness/vendor/UPSTREAM-PROOF.md new file mode 100644 index 0000000000..3a405e327a --- /dev/null +++ b/research/spd-dirty-circuit-witness/vendor/UPSTREAM-PROOF.md @@ -0,0 +1,191 @@ +# Compact universal certificates for dirty linear circuits + +## Result and provenance + +Let K be a field, let r registers contain arbitrary independent vectors in one +K-vector space V, and let X_a be finitely many **independent unary operator +symbols**. A program uses scalar ADD, SCALE, SWAP, unary APPLY, and queries +`v_d += c X_a v_s`. Source and destination may coincide. Coefficients are +central elements of K. Retain every input and every returned register, +including borrowed dirty registers. There are no implicit zero inputs. + +**Bridge theorem.** A program with q unary occurrences has a coefficient +representation with exactly r+q states, independent of its expanded word count. +For two programs, put D=2r+q_left+q_right. Their complete endpoints are equal +under every K-linear operator substitution, in every dimension, if and only if +their difference has a certificate consisting of at most D reachable rows, +initial-span coordinates, closure coordinates, and zero final projections. +Such a certificate can be found with polynomially many exact field operations. +If the endpoints differ, the search finds a shortest nonzero coefficient word +w. Matrices of dimension |w|+1 with entries zero or one realize that coefficient +as an actual endpoint discrepancy, including the offending dirty input/output. + +The same procedure applied after substituting X_a=I+Y_a supplies a discrepancy +using **simultaneously upper triangular unipotent**, hence invertible, operators. +In either version |w| is at most the maximum unary dependency depth of the two +programs, and at most D-1. For a program compared with an explicit polynomial +target, replace q_right by the sum of its displayed term lengths. + +This is a project-specific compilation and certificate bridge to **classical** +weighted-automata equivalence and noncommutative polynomial identity testing. +No new general PIT algorithm, free-algebra separation theorem, or tensor +independence theorem is claimed. Primary references are Stefan Kiefer, +[Notes on Equivalence and Minimization of Weighted Automata, §§1–2 (2020)](https://arxiv.org/abs/2009.01217), +and Ran Raz and Amir Shpilka, +[Deterministic Polynomial Identity Testing in Non Commutative Models (2005)](https://www.cs.tau.ac.il/~shpilka/publications/RazShpilka_PIT.pdf). +The new artifact specializes these methods to the project's complete dirty +register contract, gives a compact compiler and separately transcribed checker, +and binds them to a real scheduler and constructive failure diagnostics. + +The existing [free-word tensor-lift audit](../free-word-tensor-lift-audit/README.md) +already proves a particular provider's lift with explicit reduced free-group +words. The [universal dirty-phase identities](../universal-dirty-phase-identities/README.md) +already replace numerical tests for their typed local identities. Neither result +is claimed here. This method avoids word expansion for its own independent-symbol, +equal-space linear grammar; it does **not** replace their relation-aware or +rectangular-block arguments. + +## 1. Register compilation without word expansion + +Create r leaf atoms x_0,...,x_(r-1). Maintain each register as a scalar linear +combination of atoms. Scalar instructions update these combinations directly. +For each unary occurrence on expression e, create one fresh atom z_j=X_a e +and record its label a and its scalar dependency row e. APPLY replaces its +register expression by z_j. A query adds c z_j to its destination expression. +Take e from the pre-instruction source, also for self queries. Thus the number +of atoms is exactly r+q. Their dependencies always point to earlier atoms. +No symbolic polynomial, fresh clean vector, or physical helper is created by +this representation: atoms are compiler records only. + +Write U for the final r register rows. For each symbol a, form the state matrix +T_a: row j is atom j's dependency row if its label is a, and zero otherwise. +Let V map each original leaf to its corresponding input coordinate and all +unary atoms to zero. Induction on the acyclic dependencies gives + + coefficient of word a1 ... ak in endpoint (o,i) + = (U T_a1 ... T_ak V)_(o,i). + +Words use ordinary matrix-product order: [B,A] denotes BA, which applies A +first. Empty words supply scalar multiples of the identity on payloads. +Subtract two programs by a direct sum of their state spaces, concatenate +their initial rows with a minus sign on the second, and stack their final maps. +Inputs remain shared *semantically* through V; the compiler's two copies of +the leaf indices do not introduce independent copies of the actual data. + +The compiler supports rational coefficients, Gaussian rationals Q(i), and prime fields. +The executable's finite fields are F_p for primes p<=2^31-1; a displayed +fraction is admitted only if its denominator is invertible. The written +argument applies over any field. There is no numerical tolerance. + +## 2. The certificate and its small checker + +Let B have b<=D rows in the difference representation. A positive certificate +gives paths identifying these reachable rows and scalar coordinates H,C_a such +that + + U = H B, B T_a = C_a B for every symbol a, B V = 0. + +These **finite equalities** are the whole acceptance condition. They imply +U T_w lies in the row span of B for every word w, by induction on word length. +Hence U T_w V=0 for all words. Free words are a basis of K< X_a >, so the +complete matrix polynomial is zero. Evaluation in End_K(V) preserves sums, +ordered products and scalar coefficients, proving universal substitution. +No independence or minimality of B is needed for soundness. + +Conversely, if the polynomial is zero, the reachable row space +span{U_o T_w} is finite-dimensional, stable under every T_a, and annihilated by +V. Choose a reachable basis. Its initial and closure coordinates give exactly +the displayed certificate. This proves completeness for the declared grammar. + +`linear_words.py` computes that basis by incremental exact elimination. +`check_certificate.py` imports no producer code and does no elimination or +search: it separately reconstructs the dependency representation, rebuilds +the path rows, and checks all three equations. Both share `fields.py`, which +is explicitly part of the trusted arithmetic surface. Neither is a proof +assistant kernel. Source transcription, Python and the arithmetic/compiler +implementations remain trusted; bounded differential tests address faults. + +There are at most D accepted basis rows and |alphabet|D successor tests. +A dense implementation needs O(|alphabet|D^3 + L D) field operations for a +length-L pair of programs, plus parsing the target. Coordinate storage has at +most O(|alphabet|D^2+rD) field elements. These are arithmetic bounds; exact +scalar sizes and dense/sparse constants affect runtime. The reference checker +may recompute path rows and is polynomial, rather than performance optimized. + +## 3. Shortest distinguishing words and literal counterexamples + +Initialize a FIFO queue with independent rows of U. For each queued row U_o T_w, +test its output projection, and enqueue independent successor rows U_o T_w T_a. +All path rows of length at most k are spanned by accepted path rows of length +at most k. This follows by induction, including every rejected dependent row: +its expression uses earlier rows with no greater length, whose successors +span its successors. FIFO order therefore finds a word of least length among +all nonzero coefficients. Dimension increases at most D times. In the acyclic +representation, a word longer than either program's unary dependency depth is +already zero. The checker validates nonzeroness, **not a minimality certificate**; +shortestness is a property of the proved search algorithm. + +Suppose coefficient c != 0 occurs in output o, input i, word w=a1...ak. +On a space with basis e_0,...,e_k set + + N_a = sum_{j: a_(j+1)=a} E_(j,j+1). + +Every factor advances exactly one coordinate. Thus a word u has matrix entry +(0,k) equal to one exactly when u=w, and zero otherwise. Longer words vanish; +shorter words cannot reach coordinate k. Consequently the actual endpoint +discrepancy on input role i with payload e_k has output-role-o coordinate e_0 +equal to c. All other roles can be zero in this concrete witness; they were +independent during the universal check. If k=0, use one-dimensional zero +operators and the empty-word coefficient. Matrices for symbols absent from +w are zero too. This proves finite-dimensional separation constructively. + +For invertible generators run the algorithm on Q(Y)=P(I+Y). Substitution +X->I+Y is a free-algebra automorphism, with inverse Y->X-I, over every field. +It preserves nonzeroness and does not increase degree. Apply the preceding +construction to Q, and evaluate the original circuit at X_a=I+N_a. These +matrices are unipotent with finite inverse I-N_a+N_a^2-...; they share one +triangular flag. This proves the invertible version without assuming that a +separately named inverse symbol denotes this inverse. + +The degree+1 bound is sharp for this **unipotent witness class**: P(X)=(I-X)^d +vanishes on every unipotent operator of dimension at most d, whereas the +(d+1)-dimensional Jordan witness is nonzero. This is not a claim that d+1 is +the least dimension of an arbitrary invertible counterexample. + +## 4. Tensor substitution and dirty boundaries + +If a positive certificate is accepted, substitute X_a=G_a^(tensor f) for any +chosen endomorphisms G_a and any positive integer f. Polynomial evaluation +gives the endpoint identity on the enlarged payload space. Scalar c remains +c times its identity. For example X-I becomes G^(tensor f)-I; it does not +become (G-I)^(tensor f), and cX does not become (cG)^(tensor f). +The *evaluated unary word* tensors multiplicatively; the whole linear sum +must still be evaluated term by term. The certificate never tensorizes a sum. + +Complete role coverage means a borrowed field must return its arbitrary +input functional. A target with `identity:true` supplies that requirement +automatically for every unspecified block. Losing dirt is a nonzero endpoint +residual even when the intended visible target increment is correct. +External source/target aliasing changes the independent-role contract and +requires a new problem transcription. Reusing a role inside the word is legal. + +A negative result disproves universality for **independent** operators. It +does not disprove an identity under commutation, inverse, involution, +Clifford, fixed-dimension, reachable-state or nonlinear leaf constraints. +Such constraints are not silently added. Physical native implementation, +precision, rounded restoration, hosting, stock, compiler uniformity and the +complete paid/outer invoice all remain separate obligations. + +## 5. Bound application + +The adapter imports the exact pinned `echo.py` from the credited multiway dirty +echo package and translates its emitted `(src,dst,factor,sign)` instructions +literally into queries. Its reference is identity on all roles plus +`target += sign A_(n-1)...A_0 source`. Source and every borrowed input are +retained. Each accepted finite schedule now has an inspectable universal +coefficient certificate, extending beyond its earlier fixed matrix controls. +The echo theorem and scheduler are predecessor work, not newly discovered. +The tested schedule range is in README.md; no finite range substitutes for +that predecessor's arbitrary-n written induction or rounded-leaf argument. + +Prepared for zxv with substantial OpenAI Codex assistance. Apache-2.0. diff --git a/research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md b/research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md new file mode 100644 index 0000000000..be4e5981e5 --- /dev/null +++ b/research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md @@ -0,0 +1,133 @@ +# Compact universal certificates for dirty linear circuits + +**A reusable algebraic bridge and exact checker; no new κ.** A linear register +program with r arbitrary inputs and q noncommuting unary calls compiles into +r+q coefficient states. Exact subspace closure certifies its complete endpoint +for **every operator substitution and payload dimension**, without expanding +its noncommutative words. Failure returns a distinguishing word, its dirty +input/output roles, and explicit finite matrix counterexamples. An optional +change of variables makes every counterexample generator invertible. + +This addresses the gap between small matrix experiments and universal recursive +substitution. The weighted-automata and noncommutative PIT algorithms are +classical and credited in [PROOF.md](PROOF.md). The contribution is the compact +register compiler, complete-boundary certificate contract, separate checker, +constructive diagnostics and source-bound application. No new general PIT +algorithm or first universal algebra check in this project is claimed. + +## Result and use + +The [bridge theorem](PROOF.md) gives a polynomial exact-field procedure and a +finite certificate of initial-span coverage, operator closure and zero final +projections. The checker performs no search or Gaussian elimination and imports +no producer code. A shortest nonzero coefficient word of length k produces an +explicit (k+1)-dimensional counterexample. With `--invertible`, all generators +are simultaneously triangular unipotent matrices. The checker validates the +discrepancy; shortestness follows from the search proof. + +The [one-page guide](../../docs/research/universal-dirty-circuit-guide.md) gives +the grammar and acceptance boundary. The tools use only the standard library: + +```sh +python3 -I -B research/universal-dirty-certificates/linear_words.py \ + research/universal-dirty-certificates/examples/dirty-echo3.json \ + --output /tmp/my-new-dirty-certificate.json +python3 -I -B research/universal-dirty-certificates/check_certificate.py \ + research/universal-dirty-certificates/examples/dirty-echo3.json \ + /tmp/my-new-dirty-certificate.json +``` + +Output paths must be new. Add `--matrices` to the checker to print sparse +concrete matrices for a negative certificate. API users can call +`linear_words.decide(problem, shifted=False)` and +`check_certificate.check(problem, certificate)`. + +The committed wrong-order fixture is rejected using `A0=I+E01`, `A1=I+E12`, +`A2=I` in dimension three. Source payload e2 and zero other inputs produce +target discrepancy −1 in coordinate zero. Every generator is invertible. +Scalar substitutions miss the analogous commutator failure. + +## Source-bound evidence + +The adapter translates the actual emitted instructions of the authenticated +`research/cyclic-dirty-commutator-audit/echo.py`. The reference is identity on +every role plus `y += sign A_(n-1)...A_0 x`. The echo construction, schedule and +arbitrary-n/rounded proofs are predecessor work. New certificates cover the +tested emitted schedules for arbitrary substituted linear maps; the rounded +backend and its cost theorem are not replayed. + +- 210 complete source-echo identities: 1,2,3,5,8,12,16 factors; fanouts 2,3,8; + both signs; Q, Q(i), F2, F3, F5. At most 284 states and 38 invariant rows. +- 120 differential circuits against separately implemented explicit-word + expansion, including self reads, rational coefficients, swaps and zero maps. + Each planted discrepancy has a literal full-column matrix replay. +- Cleanup, source, coefficient and order mutations; malformed certificates; + finite-field controls; scalar commutator blindness; the tensor-of-sum trap; + and the sharp unipotent-degree witness family. +- **2^64 distinct endpoint words** in one stress circuit: 130 states and 65 + certificate rows. Initial production/check took about 1.3 seconds on the + Python 3.14 host. This measurement does not predict arbitrary supplier replay. + +Committed examples contain problems and inspectable certificates. Default +verification is read-only and checks exact certificate reproduction. Environment +and measured replays appear in [VALIDATION.json](VALIDATION.json). + +```sh +python3 -B scripts/research_package.py --package research/universal-dirty-certificates --check-only +python3 -B scripts/research_package.py --package research/universal-dirty-certificates +``` + +Direct verification also supports `-I -O -B`. Generic CI targets Python 3.12; +local interpreter versions are recorded separately. No historical heavy suite, +native supplier replay or Lean build is required. + +## Limits and trust + +Supported fields are Q, Q(i), and F_p, prime p<=2^31-1; fractions need invertible +denominators. Every input/returned role is retained. Equal payload dimensions +and **independent** operator symbols are required. A negative verdict need not +survive additional inverse, commutation, Clifford or reachable-state constraints. +The existing relation-aware free-group tensor audit remains appropriate there. + +The proof is written mathematics with exact executable certificates, not a +proof-assistant formalization or independent human review. The checker has a +separately transcribed compiler and shares `fields.py` with the producer. These, +Python and source transcription are trusted; differential expansion and literal +matrix execution are additional checks, not independent reviewers. + +Universal acceptance permits termwise tensor substitution with scalar +coefficients fixed. It does not tensorize a sum. Affine constants, rectangular +types, nonlinear leaves, physical aliasing, native implementation, precision, +rounded restoration, stock, hosting, tapes and the complete paid/outer invoice +remain separate. No supplier admission or selected-frontier change is claimed. + +## Open next questions + +- Bind another contributor's independent-symbol program with a literal source + adapter and complete endpoint. Compare its certificate against an existing + symbolic replay. Types and generator relations must match first. +- Add a relation-aware frontend for one named inverse/commutation model, starting + with a sound normalization theorem and boundary controls. Independent symbols + are only a conservative test of a relation-constrained implementation. +- Profile rational coefficient growth and repeated path traversal on a larger + real adapter, preserving exactly the same closure equations. The arithmetic + bound does not guarantee scalable replay of every 632-role supplier. + +## Credit and coordination + +Prepared for **zxv** with substantial **OpenAI Codex assistance**; Apache-2.0. +Classical weighted-automata/PIT credit belongs to the cited authors. The echo +package is prepared for **androolloyd**, following **Chafik Boukhalfa / chafreaky +PR628**, **Ali Romman PR621** and the retained inverse/precision lineage. +**Cinna Davis PR4100/4088**, **ToikY's free-word tensor-lift audit**, **Sagar +Thakrar PR3687**, **roger-sato PR3693**, and the universal dirty-phase audit +following **Charles Bethin PR1278** retain their prior results and credit. +Ross Richardson's cut58 and the two-register short-mixing work retain their +distinct tensor-separation arguments. Only the small echo scheduler is imported. + +[SOURCES.json](SOURCES.json) pins the base, catalogue, selected record, live +scheduler and relevant provenance. [TASK.json](TASK.json) records the explicit +scope change and bounded obligations. The canonical +[claim](https://github.com/CrocSwap/integer-mult-bounds/discussions/1166#discussioncomment-19145795) +records overlap and publication status. Cache misses do not establish novelty; +unpublished work and arbitrary historical diffs remain outside the checked scope. From f45b6cb9f17f1a53bb2fff6c176ffb6f8c379a5c Mon Sep 17 00:00:00 2001 From: Ali Romman <226877337+aliromman@users.noreply.github.com> Date: Fri, 23 Oct 2026 10:29:24 -0500 Subject: [PATCH 3/3] Bind frozen predecessor sources to published ancestor objects --- research/spd-dirty-circuit-witness/NOTICE.md | 4 +- research/spd-dirty-circuit-witness/README.md | 7 ++- .../spd-dirty-circuit-witness/RESULT.json | 8 ++- .../spd-dirty-circuit-witness/SOURCES.json | 55 ++++++++++++++----- 4 files changed, 54 insertions(+), 20 deletions(-) diff --git a/research/spd-dirty-circuit-witness/NOTICE.md b/research/spd-dirty-circuit-witness/NOTICE.md index 04f89cf1f2..2b9c6ba72e 100644 --- a/research/spd-dirty-circuit-witness/NOTICE.md +++ b/research/spd-dirty-circuit-witness/NOTICE.md @@ -8,7 +8,9 @@ The two files in vendor and wrong-order.json are unchanged copies from `48976daa4dce59b4867ef046da72a370e389925d`. The source is prepared for zxv with substantial OpenAI Codex assistance, under Apache-2.0. This PR is pending and is not part of our main base. SOURCES.json records each original path, Git blob -and SHA256. The replay checks the copied bytes. References inside the unchanged +and SHA256, and binds the retained copies to an ancestor in this publication +history. The original proof and README are also retained in vendor. The replay +checks the copied runtime bytes; metadata checks bind all retained sources. References inside the unchanged vendor files refer to the predecessor's proof, not to a claim of our authorship. Retain its weighted-automata/PIT credit to Stefan Kiefer and Ran Raz / Amir diff --git a/research/spd-dirty-circuit-witness/README.md b/research/spd-dirty-circuit-witness/README.md index 388b18c57c..835adc8697 100644 --- a/research/spd-dirty-circuit-witness/README.md +++ b/research/spd-dirty-circuit-witness/README.md @@ -40,7 +40,12 @@ no independent human or formal proof-kernel acceptance is claimed. The package starts at main ff3cc58e370d0f678e529246f8c73e8094e18fcf, priority revision 7. Two vendor files and the example are frozen copies from pending head 48976daa4dce59b4867ef046da72a370e389925d. [SOURCES.json](SOURCES.json) -records this dependency explicitly. No dependency is silently promoted to main. +records original upstream locations and pins the exact retained copies in this +publication history. The original proof and attribution are retained with the +compiler. No pending upstream Git object is required by a fresh checkout. +The first hosted replay failed before mathematical execution because that +pending Git object was absent. The source-history repair preserves all bytes +and all mathematical checks. No dependency is promoted to main. The full-history wrapper was not run in the shallow checkout. No selected cold replay, native/Lean/Docker run, physical implementation or kappa change is claimed. diff --git a/research/spd-dirty-circuit-witness/RESULT.json b/research/spd-dirty-circuit-witness/RESULT.json index 1f84518bf6..8eea970dd9 100644 --- a/research/spd-dirty-circuit-witness/RESULT.json +++ b/research/spd-dirty-circuit-witness/RESULT.json @@ -1,13 +1,15 @@ { "controls": 15, "files": { - "NOTICE.md": "8f341e0ee30f8ce5370501c16d240a0aed5010a5c99c1f8975a3b9fa0e006887", + "NOTICE.md": "0f1d9ac19527fb5d3176083e7b4540e1248d9ec96c00073c9e0d1461fa5f8453", "PROOF.md": "b11c7bd44ceb7783e1e58d1f32e6a5c979f8be02b7ed91f7203a86cfbf7a19d9", - "README.md": "d4767132f4a6349742d2b61c2b16b84df80631a1d3c7d486946c23cb620bd9a5", - "SOURCES.json": "f2d2f71029276fdb1334bc872d018c30422715b041d5ab8628fbc9b4dc7d718e", + "README.md": "1df8ea3df8a2765aed1be207525ced7e682458b46ab8ba6bc106ab7a02c7c9f1", + "SOURCES.json": "ad1e637bafbf61a6fe9cf9d80528a1be9a55ee220e0a0424cd931d2d17baf481", "TASK.json": "318d8c21d6b7b88793bdb34446a492598cfcca8b99107ee76c77108adf80a385", "VERIFY.json": "d26d07c535953e4f972577c1e3b9a7bf58539254cb10661a0160876f465c4b3e", "literal.py": "89f1b1e039119627ac512be9407e456fdb513adbe5104027a6d65865e1f598b9", + "vendor/UPSTREAM-PROOF.md": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7", + "vendor/UPSTREAM-README.md": "fb8d94a58b6c0448aa893e65f263b9d71639b1aa79cd10f054d0dc740a570dca", "vendor/fields.py": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7", "vendor/linear_words.py": "fe825cf7c886de61bb5ec5a02171c5a392a7bddc185280726f4c359b3f289584", "verify.py": "eed7802377767720f7f6a677d0d07e1d7889b0e3e567ee6a13831f1500a1c83d", diff --git a/research/spd-dirty-circuit-witness/SOURCES.json b/research/spd-dirty-circuit-witness/SOURCES.json index 1a3adcdc60..0cc889cda1 100644 --- a/research/spd-dirty-circuit-witness/SOURCES.json +++ b/research/spd-dirty-circuit-witness/SOURCES.json @@ -15,39 +15,64 @@ "sha256": "f7a48bfa2659b88378282a8eee7d9fe52cdf505594124c4d1686b58510fffd72" }, { - "path": "research/universal-dirty-certificates/fields.py", + "path": "research/spd-dirty-circuit-witness/vendor/fields.py", "usage": "provenance", - "pin": "head:48976daa4dce59b4867ef046da72a370e389925d:research/universal-dirty-certificates/fields.py", + "pin": "head:46bdee8dff4254afd2ed773e7f6c263156c6f84d:research/spd-dirty-circuit-witness/vendor/fields.py", "git_blob": "f1b6dc83e26bd9fd9ec67ded3fedb330ef89598d", - "sha256": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7" + "sha256": "0829ad6ed3775ba6e3d11cf04cfb3513ac763549b730aaed74958b1238e660d7", + "upstream": { + "commit": "48976daa4dce59b4867ef046da72a370e389925d", + "path": "research/universal-dirty-certificates/fields.py", + "url": "https://github.com/zxv/integer-mult-bounds/blob/48976daa4dce59b4867ef046da72a370e389925d/research/universal-dirty-certificates/fields.py" + } }, { - "path": "research/universal-dirty-certificates/linear_words.py", + "path": "research/spd-dirty-circuit-witness/vendor/linear_words.py", "usage": "provenance", - "pin": "head:48976daa4dce59b4867ef046da72a370e389925d:research/universal-dirty-certificates/linear_words.py", + "pin": "head:46bdee8dff4254afd2ed773e7f6c263156c6f84d:research/spd-dirty-circuit-witness/vendor/linear_words.py", "git_blob": "4a877e1ab9a87a0f01eb13e28ddf309c2060bd5e", - "sha256": "fe825cf7c886de61bb5ec5a02171c5a392a7bddc185280726f4c359b3f289584" + "sha256": "fe825cf7c886de61bb5ec5a02171c5a392a7bddc185280726f4c359b3f289584", + "upstream": { + "commit": "48976daa4dce59b4867ef046da72a370e389925d", + "path": "research/universal-dirty-certificates/linear_words.py", + "url": "https://github.com/zxv/integer-mult-bounds/blob/48976daa4dce59b4867ef046da72a370e389925d/research/universal-dirty-certificates/linear_words.py" + } }, { - "path": "research/universal-dirty-certificates/PROOF.md", + "path": "research/spd-dirty-circuit-witness/vendor/UPSTREAM-PROOF.md", "usage": "provenance", - "pin": "head:48976daa4dce59b4867ef046da72a370e389925d:research/universal-dirty-certificates/PROOF.md", + "pin": "head:46bdee8dff4254afd2ed773e7f6c263156c6f84d:research/spd-dirty-circuit-witness/vendor/UPSTREAM-PROOF.md", "git_blob": "3a405e327a7fd5d59a570d7f9920f1ce7f229a76", - "sha256": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7" + "sha256": "ef4cfcfd65b1dde1f11eedace0ed90a1b47a2cc100daaf778fbecbff3ec685a7", + "upstream": { + "commit": "48976daa4dce59b4867ef046da72a370e389925d", + "path": "research/universal-dirty-certificates/PROOF.md", + "url": "https://github.com/zxv/integer-mult-bounds/blob/48976daa4dce59b4867ef046da72a370e389925d/research/universal-dirty-certificates/PROOF.md" + } }, { - "path": "research/universal-dirty-certificates/README.md", + "path": "research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md", "usage": "provenance", - "pin": "head:48976daa4dce59b4867ef046da72a370e389925d:research/universal-dirty-certificates/README.md", + "pin": "head:46bdee8dff4254afd2ed773e7f6c263156c6f84d:research/spd-dirty-circuit-witness/vendor/UPSTREAM-README.md", "git_blob": "be4e5981e57bdd2aa8d2ba8c36479594cf38b5d2", - "sha256": "fb8d94a58b6c0448aa893e65f263b9d71639b1aa79cd10f054d0dc740a570dca" + "sha256": "fb8d94a58b6c0448aa893e65f263b9d71639b1aa79cd10f054d0dc740a570dca", + "upstream": { + "commit": "48976daa4dce59b4867ef046da72a370e389925d", + "path": "research/universal-dirty-certificates/README.md", + "url": "https://github.com/zxv/integer-mult-bounds/blob/48976daa4dce59b4867ef046da72a370e389925d/research/universal-dirty-certificates/README.md" + } }, { - "path": "research/universal-dirty-certificates/examples/wrong-order.json", + "path": "research/spd-dirty-circuit-witness/wrong-order.json", "usage": "provenance", - "pin": "head:48976daa4dce59b4867ef046da72a370e389925d:research/universal-dirty-certificates/examples/wrong-order.json", + "pin": "head:46bdee8dff4254afd2ed773e7f6c263156c6f84d:research/spd-dirty-circuit-witness/wrong-order.json", "git_blob": "85482942f052694a3a6d15d364d18823b51e1b00", - "sha256": "137def9876c1195456a312b8c232d656ff063cc5caae645be6afc3d06709742c" + "sha256": "137def9876c1195456a312b8c232d656ff063cc5caae645be6afc3d06709742c", + "upstream": { + "commit": "48976daa4dce59b4867ef046da72a370e389925d", + "path": "research/universal-dirty-certificates/examples/wrong-order.json", + "url": "https://github.com/zxv/integer-mult-bounds/blob/48976daa4dce59b4867ef046da72a370e389925d/research/universal-dirty-certificates/examples/wrong-order.json" + } } ] }