verify.py

#!/usr/bin/env python3
"""Verify the archived evidence without invoking a solver or changing files."""

import gzip
import hashlib
from html.parser import HTMLParser
import json
from pathlib import Path
import sys
from urllib.parse import unquote, urlsplit

sys.dont_write_bytecode = True
ROOT = Path(__file__).resolve().parent
PUBLIC_SHA256 = "17daa755934cd63d1910ff772968d2901057ada5b89db1c8900ed29c27de2e2f"
REPORT_SHA256 = "f0635189a62c78e69d36f11d562751153924ee8afec22d0dc530b8d9da25bb9b"
INDEX_SHA256 = "263094f5e18e336d317772e922322c6919c69dc6838329186268b648978e4b26"
COHORTS = ("before", "auto", "configured")
BRACKETS = {
    "knapsack": ((33, 34), (2304, 2336), (2304, 2336)),
    "assignment": ((17, 18), (64, 66), (31, 32)),
    "facility_location": ((8, 9), (44, 45), (54, 56)),
    "bin_packing": ((17, 18), (47, 48), (30, 31)),
    "production": ((11, 12), (27, 29), (28, 29)),
    "native_tsp": ((21, 22), (21, 22), (21, 22)),
    "weighted_queens": ((23, 24), (23, 24), (23, 24)),
}


def require(condition, message):
    if not condition:
        raise ValueError(message)


def digest(data):
    return hashlib.sha256(data).hexdigest()


def encoded_json(value):
    return (json.dumps(value, indent=2, allow_nan=False) + "\n").encode("utf-8")


class LocalLinks(HTMLParser):
    def __init__(self):
        super().__init__()
        self.links = set()

    def handle_starttag(self, tag, attrs):
        for name, value in attrs:
            if name in ("href", "src", "poster") and value:
                self.links.add(value)


def verify_files():
    manifest = json.loads((ROOT / "provenance/immutable-files.json").read_text())
    require(manifest["schema_version"] == 1, "Unknown immutable manifest schema")
    files = manifest["files"]
    require(len(files) == 730, "Immutable file count differs")
    for name, expected in files.items():
        path = (ROOT / name).resolve()
        require(ROOT in path.parents, "Manifest path escapes the repository")
        require(path.is_file(), "Missing immutable file: " + name)
        data = path.read_bytes()
        require(len(data) == expected["bytes"] and digest(data) == expected["sha256"],
                "Immutable file changed: " + name)
    report_files = [p for p in (ROOT / "report").rglob("*") if p.is_file()]
    require(len(report_files) == 705, "Report file count differs")
    require(sum(p.stat().st_size for p in report_files) == 57982908,
            "Report byte count differs")
    index = ROOT / "report/index.html"
    require(digest(index.read_bytes()) == INDEX_SHA256, "Reference HTML hash differs")
    links = LocalLinks()
    links.feed(index.read_text())
    local = set()
    for value in links.links:
        url = urlsplit(value)
        if url.scheme or url.netloc or not url.path:
            continue
        target = (index.parent / unquote(url.path)).resolve()
        require((ROOT / "report") in target.parents,
                "Reference page link escapes the report: " + value)
        require(target.is_file(), "Missing reference page link: " + value)
        local.add(target)
    return len(files), len(local)


def verify_data():
    raw = gzip.decompress((ROOT / "report/downloads/gecode-final.json.gz").read_bytes())
    require(digest(raw) == PUBLIC_SHA256, "Published final data hash differs")
    for prefix in ("/Users/", "/home/", "file://"):
        require(prefix.encode() not in raw, "Local path found in published data")
    public = json.loads(raw)
    report, projection = public["report"], public["projection"]
    require(digest(encoded_json(report)) == REPORT_SHA256, "Final report hash differs")
    require(report["complete"] and all(report["provenance"]["integrity"].values()),
            "Archived report does not record completed integrity checks")
    require(len(report["models"]) == 115 and len(report["records"]) == 359,
            "Model or observation count differs")
    records = report["records"]
    require(sum(not r["probe"] for r in records) == 356,
            "Measured observation count differs")
    require(sum(r["probe"] for r in records) == 3, "Runtime-loader probe count differs")
    keys = [(r["case"], r["cohort"], r["repetition"]) for r in records]
    require(len(keys) == len(set(keys)), "Duplicate archived observation")

    sys.path.insert(0, str(ROOT / "experiments/optimize"))
    import final_instances as generator

    models = {item["id"]: item for item in report["models"]}
    require(len(models) == 115, "Duplicate frozen model identifier")
    for identity, item in models.items():
        model = item["model"]
        require(digest(encoded_json(model)) == item["json_sha256"],
                "Frozen model JSON hash differs: " + identity)
        text = generator.encode_txt(model)
        require(digest(text.encode("utf-8")) == item["txt_sha256"],
                "Frozen model TXT hash differs: " + identity)

    witnesses = 0
    for row in records:
        require(row["case"] in models, "Observation refers to an unknown model")
        result = row["backend_result"]
        require(result["start_submitted"] is False, "Archived observation used a start")
        require(result["status"] == row["status"], "Status projection differs")
        require(row["passed"] == (row["status"] == "optimal" and row["solve_seconds"] <= 10),
                "Passing observation projection differs")
        if result["has_solution"]:
            checked = generator.validate_assignment(models[row["case"]]["model"],
                                                      result["assignment"])
            require(checked["valid"], "Saved original witness is invalid: " + row["case"])
            require(checked["objective"] == result["objective"] == row["objective"],
                    "Original witness objective differs: " + row["case"])
            require(row["primal_checked"] and result["solution_validated"],
                    "Saved witness validation flags differ")
            witnesses += 1
        else:
            require(not result["assignment"] and result["objective"] is None,
                    "Absent solution includes witness values")

    families = {f["id"]: f for f in projection["families"]}
    require(set(families) == set(BRACKETS), "Final category set differs")
    checkpoint = json.loads((ROOT / "provenance/final-checkpoint.json").read_text())
    for category, expected in BRACKETS.items():
        variants = ("uncorrelated", "correlated") if category == "knapsack" else ("single",)
        identities = {(variant, repetition) for variant in variants for repetition in (1, 2)}
        for cohort, (lower, upper) in zip(COHORTS, expected):
            bracket = report["protocol"]["extended_boundaries"][category][cohort]
            require((bracket["lower"], bracket["upper"]) == (lower, upper),
                    "Recorded bracket differs: " + category + "/" + cohort)
            require(checkpoint["brackets"][category][cohort] == bracket,
                    "Checkpoint bracket differs: " + category + "/" + cohort)
            boundary = families[category][cohort + "_boundary"]
            require(boundary["confirmed_size"] == lower and boundary["failed_upper_size"] == upper,
                    "Displayed bracket differs: " + category + "/" + cohort)
            selected = [r for r in records if not r["probe"] and
                        r["category"] == category and r["cohort"] == cohort]
            passing = [r for r in selected if r["size"] == lower]
            failing = [r for r in selected if r["size"] == upper]
            for group in (passing, failing):
                require({(r["variant"], r["repetition"]) for r in group} == identities,
                        "Incomplete bracket confirmation: " + category + "/" + cohort)
            require(all(r["passed"] for r in passing), "Lower bracket includes a failed result")
            require(all(any(not r["passed"] for r in failing if r["repetition"] == repeat)
                        for repeat in (1, 2)), "Upper bracket did not fail in both repetitions")
    return witnesses


def main():
    files, links = verify_files()
    witnesses = verify_data()
    print("Verified {} immutable files, 705 report files and {} local entry-page links.".format(files, links))
    print("Verified 115 frozen models, 356 measured observations, 3 loader probes and {} saved witnesses.".format(witnesses))
    print("All published hashes and 21 sampled size brackets agree; no solver was run.")
    print("Witness verification does not independently establish optimality.")


if __name__ == "__main__":
    try:
        main()
    except (ValueError, KeyError, OSError) as error:
        print("Verification failed: {}".format(error), file=sys.stderr)
        sys.exit(1)