sciencehub-team/noncoordinate-polynomialPublic

class Dual:
    """A number a + b·ε with ε² = 0. Evaluating a polynomial at x + ε gives its derivative at x in b, exactly."""

    def __init__(self, a, b=0):
        self.a, self.b = Fraction(a), Fraction(b)

    @staticmethod
    def _lift(other):
        return other if isinstance(other, Dual) else Dual(other)

    def __add__(self, other):
        other = Dual._lift(other)
        return Dual(self.a + other.a, self.b + other.b)

    __radd__ = __add__

    def __neg__(self):
        return Dual(-self.a, -self.b)

    def __sub__(self, other):
        return self + (-Dual._lift(other))

    def __rsub__(self, other):
        return Dual._lift(other) - self

    def __mul__(self, other):
        other = Dual._lift(other)
        return Dual(self.a * other.a, self.a * other.b + self.b * other.a)

    __rmul__ = __mul__

    def __pow__(self, n: int):
        result = Dual(1)
        for _ in range(n):
            result = result * self
        return result

def S(h, u, v, w):
    """The quotient (x² + y³)/h, as `S` in Identities.lean."""
    return 2 * u**3 * v + 3 * u**4 * w + h * (v**2 - 3 * u**2 * w**2) + h**2 * w**3

def P(x, y, s):
    """The correction term p, as `P` in Identities.lean. Not the critical point P of the text."""
    return -2 * s**2 * x + 3 * s * y**2 - 3 * s**3 * y

def construction(h, u, v, w) -> dict:
    """x, y, s, p and F at one point, in the order of Identities.lean."""
    x = u**3 + h * v
    y = -(u**2) + h * w
    s = S(h, u, v, w)
    p = P(x, y, s)
    return {"x": x, "y": y, "s": s, "p": p, "F": h - p - 1}

def gradient(point) -> list:
    """The four partial derivatives of F at a point, exact over the rationals."""
    partials = []
    for i in range(4):
        seeded = [Dual(c, 1 if j == i else 0) for j, c in enumerate(point)]
        partials.append(construction(*seeded)["F"].b)
    return partials

def load_evidence(path: Path = EVIDENCE) -> str:
    """The record of a Lean proof check run as Markdown, or a sentence saying why there is none to show."""
    try:
        evidence = json.loads(path.read_text(encoding="utf-8"))
    except FileNotFoundError:
        return EVIDENCE_MISSING
    except (OSError, ValueError) as error:
        return f"`{path}` cannot be read: {error}."
    try:
        return evidence_summary(evidence)
    except (AttributeError, KeyError, TypeError, ValueError, StopIteration):
        return f"`{path}` is not a record of the kind this notebook reads."

def scrub(text: str) -> str:
    """Text from a run record with the owner of ScienceHub's CI repository and image replaced by OWNER."""
    keep = {"ghcr.io", "github.com", "api.github.com", "docker.io", "v2", "repos"}

    def owner(match):
        return match.group(0) if match.group(1) in keep else "OWNER/"

    return re.sub(r"([\w.-]+)/(?=sciencehub(?:-lean)?\b)", owner, text)

def plural(count: int, word: str) -> str:
    return f"{count} {word}" + ("" if count == 1 else "s")

def finished(stamp: str) -> str:
    """An ISO time as a date like 28 Oct 2026."""
    from datetime import datetime

    moment = datetime.fromisoformat(str(stamp).replace("Z", "+00:00"))
    return f"{moment.day} {moment.strftime('%b %Y')}"

def image_digest(image) -> str:
    """The image's digest alone, from a record that gives a digest or, in its first format, a full reference."""
    if isinstance(image, dict):
        image = image.get("digest") or image["ref"]
    digest = str(image).rsplit("@", 1)[-1]
    if not digest.startswith("sha256:"):
        raise ValueError(digest)
    return digest

def evidence_summary(evidence: dict) -> str:
    """The record as Markdown. It names the run by number and the image by digest only.

    A run that was not accepted is shown by its outcome and the reason each runtime gives;
    the table is for accepted runs, whose records have every field it reads.
    """
    if not str(evidence["schema"]).startswith("sciencehub.lean-proof-evidence/"):
        raise ValueError(evidence["schema"])
    run = evidence["run"]
    ref = run.get("ref")
    if ref == "refs/heads/main":
        where = "**The run from main.**"
    else:
        where = f"**A run not from main.** This record is from `{scrub(str(ref))}`." if ref else "**A run not from main.** This record names no ref."
    head = (
        f"{where} Run {int(run.get('run_id', run.get('id')))}"
        + (f", finished {finished(run['finished_at'])}" if run.get("finished_at") else "")
        + ", in ScienceHub's CI "
        f"repository, which is private. Outcome: **{evidence['outcome']}**."
    )
    if evidence["outcome"] != "accepted":
        lines = [head]
        unmatched = [f["path"] for f in evidence["source"]["files"] if not f["match"]]
        if unmatched:
            lines += ["", f"{len(unmatched)} file{'s' if len(unmatched) != 1 else ''} did not match its pinned SHA-256: " + ", ".join(f"`{u}`" for u in unmatched) + "."]
        for name, result in evidence["runtimes"].items():
            if result["outcome"] != "accepted":
                if result.get("stage") == "not run":
                    lines += ["", f"Under {name} the proof was not run."]
                    continue
                lines += ["", f"Under {name} the run stopped at {result.get('stage')}."]
                if result.get("reason") is not None:
                    reason = scrub(str(result["reason"]))[:1500]
                    fence = "`" * max(3, 1 + max((len(m) for m in re.findall(r"`+", reason)), default=0))
                    lines += ["", f"{fence}text", reason, fence]
        return "\n".join(lines)
    runtime = evidence["runtimes"]["runsc"]
    versions = runtime["lean"]["versions_json"]
    modules = runtime["modules"]
    files = evidence["source"]["files"]
    axioms = "; ".join(
        f"`{name}`: " + ", ".join(f"`{a}`" for a in entry["axioms"])
        for name, entry in runtime["axioms"]["theorems"].items()
    )
    default, paranoid = runtime["comparator"]["default"], runtime["comparator"]["paranoid"]
    others = ", ".join(f"{name} {r['outcome']}" for name, r in evidence["runtimes"].items() if name != "runsc")
    rows = [
        ("Image", f"`{image_digest(evidence['image'])}`"),
        ("Lean", f"{versions['lean']} (commit `{versions['lean_commit'][:7]}`)"),
        ("Mathlib", f"{versions['mathlib']} (commit `{versions['packages']['mathlib'][:7]}`)"),
        ("Files fetched", f"{sum(1 for f in files if f['match'])} of {len(files)} matched their pinned SHA-256"),
        ("Modules built", f"{sum(1 for m in modules if m['exit'] == 0)} of {len(runtime['build_order'])}, " + plural(sum(int(m["warnings"]) for m in modules), "warning")),
        ("Axioms", axioms),
        ("Comparator, default mode", f"{default['verdict']} in {default['comparator_seconds']} s"),
        ("Comparator, paranoid mode", f"{paranoid['verdict']} in {paranoid['comparator_seconds']} s: " + ", ".join(f"{k} {v}" for k, v in paranoid["kernels"].items())),
        ("The challenge as its own solution", f"{runtime['control']['verdict']} ({scrub(str(runtime['control']['reason']))})"),
        ("Challenge export", f"`{runtime['challenge']['export_sha256']}`"),
        ("Solution export", f"`{runtime['solution']['export_sha256']}`"),
    ]
    return "\n".join(
        [
            head,
            "",
            "The table shows the run in a gVisor sandbox (runsc)" + (f"; the same proof under {others}." if others else "."),
            "",
            "| | Value |",
            "| --- | --- |",
            *(f"| {label} | {value.replace('|', chr(92) + '|')} |" for label, value in rows),
            "",
            "The comparator's own sandbox is off in these runs, as in the earlier run below; separate "
            "containers, with the judge seeing only the two exports, take its place. The two export hashes "
            "are what you can compare without our runners; the steps follow.",
        ]
    )