break-golf

Ein Board für Kryptoanalyse-Ergebnisse, die bewiesen, nicht ausgeführt werden.

Eine Challenge legt zwei Welten und die Aussage fest, die du beweisen musst. Du schreibst einen Gegner und einen Beweis, dass er sie unterscheidet. Der Gewinn ist der Beweis: nichts wird ausgeführt, gesampelt oder nachgespielt, und kein Mensch liest die Einreichung, um zu entscheiden, ob sie zählt.

Status: der Verifier läuft. Ein verify:-Issue wird in CI gegen den festgelegten Typ der Challenge ausgearbeitet und mit #print axioms geprüft; das Urteil kommt als Kommentar zurück. Einträge werden weiterhin von Hand in scoring/ledger.json hinzugefügt.

Dies ist ein eigenständiges Lake-Projekt. Es bezieht die Mathematik als Git-Abhängigkeit, die auf eine Revision festgelegt ist, sodass ein Board gegen eine feste Aussage des Modus verifiziert:

require RandomSystems from git
  "https://github.com/MarcIlunga/random-systems.git" @ "08aec7a7"

Die Build-Zeit ist ein Cache, kein Problem: Mathlibs Oleans kommen über lake exe cache get von seinem CDN, und die ~400 MB an Oleans für festgelegte Revisionen und Challenges liegen im Actions-Cache, verschlüsselt nach dem Manifest und unseren eigenen Quellen.

Aufbau

Pfad	Was es ist
challenges/<name>/Challenge.lean	Vertrauenswürdig. Legt die exakten Typen fest, die eine Einreichung erfüllen muss. Nicht Teil eines Uploads.
challenges/<name>/Cost.lean	Plattformgeneriert pro Einreichung aus den Zahlen des Formulars.
challenges/<name>/config.json	Bewertung, Par, erlaubte Axiome, Timeout. Die einzige Datei, die du bearbeitest, um eine Challenge hinzuzufügen.
challenges/<name>/Solve.template.lean	Das Skelett, das ein Einreicher ausfüllt.
tools/manifest.py	Leitet docs/data/manifest.json aus challenges/ ab.
tools/ledger.py	Leitet docs/data/ledger.json aus scoring/ledger.json ab, bewertet und sortiert die Einträge.
tools/record.py	Fügt eine verifizierte Einreichung dem Ledger hinzu. Lehnt alles ab, was nicht proved ist.
tools/verify.py	Verifiziert eine Einreichung: Challenge-ID als argv[1], Body auf stdin, JSON-Urteil auf stdout. Gleiche Schnittstelle wie bei lean-golf.
tools/lint_challenges.py	Jede Challenge-Konfiguration enthält, was das Board und der Verifier benötigen.
tools/check_site.py	Die statische Seite kann ihre eigenen generierten Daten laden und rendern.
scoring/ledger.json	Die Datensatzmenge.
docs/	Die GitHub-Pages-Seite. Statisch; liest nur die beiden generierten Dateien.
examples/	Test-Fixtures: eine Einreichung, die verifiziert und nichts gewinnt, und ihr überfordernder Zwilling.

python3 tools/manifest.py          # rewrite the manifest
python3 tools/manifest.py --check  # fail if stale
python3 tools/ledger.py            # rescore and sort the records
python3 tools/lint_challenges.py   # configs are complete
python3 tools/check_site.py        # the site can render what the tools generate

printf '%s' "$BODY" | python3 tools/verify.py spoc128    # one submission

CI

verify.yml läuft bei Push und Pull Request: die --check-Gates, der Config-Lint, der Site-Check und eine Reihe von Einreichungen, die der Verifier akzeptieren und ablehnen muss — ein sorry, ein native_decide, eine unbekannte Challenge, ein Null-Vorteil, ein Body ohne Lean-Block. workflow_dispatch verifiziert eine Einreichung auf Anfrage, ohne ein Issue zu öffnen.

submission.yml behandelt ein verify:-Issue in zwei Jobs. Der erste parst nicht vertrauenswürdige Eingaben und hält keine Schreib-Scopes; der zweite lädt sein Urteil herunter und postet den Kommentar. Diese Aufteilung stammt von lean-golf und ist der Grund, warum ein Issue- Body kein Token erreichen kann.

Der Einreicher schreibt nie die Aussage

Eine Einreichung ist eine Deklaration, die einen Typ bewohnt, den die Challenge festlegt:

-- Challenge.lean, trusted. The verifier builds its own copy.
def score : Golf.Score := ⟨budget, advNum, advDen⟩   -- from the submission form

structure Solution where
  strategy : game.Param → PFunDDS.DDE game.Query game.Response
  verdict  : List (game.Query × Option game.Response) → Bool
  wins     : Golf.Attack.Wins (G := game) ⟨strategy, verdict⟩ score.budget score.advantage

-- Solve.lean, the upload.
def solution : Challenge.SpoC128.Solution where
  strategy := …
  verdict  := …
  wins     := …

Eine Struktur statt drei loser Namen, weil die losen Namen kollidieren: Eine Solve.lean, die eine Challenge.lean importiert, die bereits strategy/verdict/attackWins deklariert, schlägt mit „has already been declared" fehl. Die Einreichung zu einem Wert eines vertrauenswürdigen Typs zu machen, beseitigt die Kollision und reduziert die Typprüfung des Verifiers auf ein einziges #check.

Warum es sicher ist, dass der Einreichende die Punktzahl wählt

Zwei Dinge müssen gelten, und keines davon wird auf Vertrauen hin angenommen.

Die Zahlen sind Teil der Aussage. Die Plattform schreibt sie in Cost.lean, Challenge.lean baut score daraus auf, und score erscheint im Typ von Solution.wins. Eine Zahl zu ändern, ändert, was bewiesen werden muss.

Die Einreichung muss unseren Typ bewohnen. Der Audit-Schritt importiert die vertrauenswürdige Challenge zusammen mit der Einreichung und elaboriert

example : Challenge.SpoC128.Solution := Solution.SpoC128.solution

Eine Einreichung, die ihr eigenes Challenge.SpoC128.Solution deklariert, kollidiert mit unserem, und eine, die einen anderen Typ verwendet, besteht die Typprüfung nicht. Ohne diesen Schritt kann eine Einreichung, die die Challenge einfach nie importiert, eine triviale Struktur gleichen Namens definieren und mit 0 Bit „bewiesen“ werden — dieses Loch war real, und beide Angriffe sind jetzt CI-Fälle.

Die Abfrageanzahl benötigt keinen separaten Beweis. Sie ist keine Behauptung über einen fertigen Angreifer; sie ist ein Konstruktorargument. Attack.distinguisher q ist DDD.ofDDE strategy q verdict, konstruktionsbedingt bei q abgeschnitten, und Attack.silent_past beweist, dass es nichts darüber hinaus ausgibt. Es gibt keine Möglichkeit, ein Budget zu überschreiten, also gibt es nichts zu prüfen.

budget, advNum und advDen stammen aus dem Einreichungsformular und sind nicht vertrauenswürdig. Das müssen sie auch nicht sein: Die Plattform setzt sie in Cost.lean ein, Challenge.lean baut score daraus, und score erscheint innerhalb von Solution.wins. Die Zahlen sind daher Teil der Aussage, nicht eine Behauptung über sie.

Geprüft gegen den echten SpoC-128-Angriff:

Behauptung	Ergebnis
budget = 3, Vorteil 1	kompiliert — die ehrliche Behauptung
budget = 1, Vorteil 1	schlägt fehl — Wins 1 1 ist ein anderes, stärkeres Theorem
budget = 3, Vorteil 2	schlägt fehl — nichts kann Vorteil 1 überschreiten

Und es gibt keinen Anreiz, den Wert zu niedrig anzugeben: score = log₂(budget / advantage^e), also erhöht ein kleinerer behaupteter Vorteil oder ein größeres behauptetes Budget den Score. Beide Richtungen sind schlechter. Der einzige Zug ist die engste Behauptung, die man tatsächlich beweisen kann.

Vier weitere Ablehnungen, die der Verifier vornimmt, ohne irgendetwas zu lesen:

Der Cheat	Das Urteil
die Behauptung abschwächen	Typkonflikt gegen das festgelegte Solution
eine günstige Hypothese hinzufügen	dasselbe
den Beweis mit sorry versehen	sorryAx ist nicht in permitted_axioms
native_decide / erhöhte maxHeartbeats	wird rundweg abgelehnt

Bewertung