File size: 3,314 Bytes
eef9104 | 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28 29 30 31 32 33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58 59 60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83 84 85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 | # *******************************************************************************
# Copyright (c) 2026 Ahmad Ali Parr and others.
#
# This program and the accompanying materials are made available under the
# terms of the CPSC Eclipse Strict Copyleft License, Version 1.0, which is
# available in LICENSES/CPSC-ESCL-1.0.txt, or, at your option, under the
# GNU Affero General Public License, Version 3 only, which is available in
# LICENSES/AGPL-3.0.txt. Both options are strict copyleft. There is no
# classpath exception and no permissive relicensing.
#
# SPDX-License-Identifier: LicenseRef-CPSC-ESCL-1.0 OR AGPL-3.0-only
# *******************************************************************************"""Certificate binding. The digest is the witness; a gate edit breaks it."""
from __future__ import annotations
import hashlib
import json
from dataclasses import dataclass
from cpsc.analyzer import Gate
@dataclass(frozen=True)
class Certificate:
digest: str
mode: str
n: int
lean: str
payload: str
lam: float
j: float
time: float
steps: int
def matches(self, gates: list[Gate]) -> bool:
return self.digest == digest_for(gates, mode=self.mode, n=self.n, lam=self.lam, j=self.j, time=self.time, steps=self.steps)
def digest_for(gates: list[Gate], *, mode: str, n: int, lam: float, j: float, time: float, steps: int) -> str:
payload = json.dumps(
{
"gates": [[g.name, list(g.qubits), g.kind] for g in gates],
"mode": mode,
"n": n,
"lambda": lam,
"j": j,
"time": time,
"steps": steps,
},
separators=(",", ":"),
)
return hashlib.sha256(payload.encode()).hexdigest()
def _lean_kind(gate: Gate) -> str:
if gate.kind == "magnetization":
a, b = gate.qubits
return f".zz {a} {b}"
if gate.kind == "phase":
return f".loneZ {gate.qubits[0]}"
if gate.kind in {"illegal", "transverse"}:
return f".transverseFlip {gate.qubits[0]}"
if gate.kind == "parity_even":
a, b = gate.qubits
return f".parityEvenPair {a} {b}"
raise ValueError(gate.kind)
def bind_certificate(
gates: list[Gate],
*,
mode: str,
n: int,
lam: float,
j: float,
time: float,
steps: int,
) -> Certificate:
payload = json.dumps(
{
"gates": [[g.name, list(g.qubits), g.kind] for g in gates],
"mode": mode,
"n": n,
"lambda": lam,
"j": j,
"time": time,
"steps": steps,
},
separators=(",", ":"),
)
digest = digest_for(gates, mode=mode, n=n, lam=lam, j=j, time=time, steps=steps)
kinds = ", ".join(_lean_kind(g) for g in gates)
predicate = "preservesMagnetization" if mode == "ising" else "preservesSpinFlip"
lean = (
"-- emitted by cpsc.certificate; do not edit by hand\n"
f"def emittedHash : String := \"{digest}\"\n"
f"def emittedGates : List GateKind := [{kinds}]\n"
f"theorem emitted_admitted : allPreserve {predicate} emittedGates = true := by\n"
" rfl\n"
)
return Certificate(
digest=digest, mode=mode, n=n, lean=lean, payload=payload,
lam=lam, j=j, time=time, steps=steps,
)
|