break-golf

Un tableau de résultats de cryptanalyse qui sont prouvés, et non exécutés.

Un défi fixe deux mondes et l'énoncé que vous devez prouver. Vous écrivez un adversaire et une preuve qu'il les distingue. La victoire est la preuve : rien n'est exécuté, échantillonné ou rejoué, et aucun humain ne lit la soumission pour décider si elle compte.

Statut : le vérificateur s'exécute. Une issue verify: est élaborée en CI par rapport au type épinglé du défi et auditée avec #print axioms ; le verdict revient sous forme de commentaire. Les records sont toujours ajoutés à scoring/ledger.json à la main.

Il s'agit d'un projet Lake autonome. Il prend les mathématiques comme dépendance git épinglée à une révision, de sorte qu'un tableau vérifie par rapport à un énoncé fixe du mode :

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

Le temps de compilation est un cache, pas un problème : les oleans de Mathlib proviennent de son CDN via lake exe cache get, et les ~400 Mo d'oleans de révision épinglée et de challenge résident dans le cache Actions indexé sur le manifeste et nos propres sources.

Arborescence

Chemin	Ce que c'est
challenges/<name>/Challenge.lean	De confiance. Fixe les types exacts qu'une soumission doit habiter. Ne fait partie d'aucun envoi.
challenges/<name>/Cost.lean	Généré par la plateforme pour chaque soumission à partir des chiffres du formulaire.
challenges/<name>/config.json	Notation, par, axiomes autorisés, délai d'expiration. Le seul fichier à modifier pour ajouter un challenge.
challenges/<name>/Solve.template.lean	Le squelette que le soumissionnaire remplit.
tools/manifest.py	Dérive docs/data/manifest.json depuis challenges/.
tools/ledger.py	Dérive docs/data/ledger.json depuis scoring/ledger.json, en notant et en triant les enregistrements.
tools/record.py	Ajoute une soumission vérifiée au registre. Refuse tout ce qui n'est pas proved.
tools/verify.py	Vérifie une soumission : identifiant du challenge comme argv[1], corps sur stdin, verdict JSON sur stdout. Même interface que celle de lean-golf.
tools/lint_challenges.py	Chaque configuration de challenge contient ce dont le tableau et le vérificateur ont besoin.
tools/check_site.py	Le site statique peut charger et afficher ses propres données générées.
scoring/ledger.json	L'ensemble des enregistrements.
docs/	Le site GitHub Pages. Statique ; ne lit que les deux fichiers générés.
examples/	Fixtures de test : une soumission qui se vérifie et ne gagne rien, et son jumeau qui revendique trop.

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 s'exécute sur push et pull request : les barrières --check, le lint de configuration, la vérification du site, et une batterie de soumissions que le vérificateur doit accepter et doit rejeter — un sorry, un native_decide, un défi inconnu, un avantage nul, un corps sans bloc Lean. workflow_dispatch vérifie une soumission à la demande sans ouvrir d'issue.

submission.yml traite une issue verify: en deux jobs. Le premier analyse l'entrée non fiable et ne détient aucun scope d'écriture ; le second télécharge son verdict et publie le commentaire. Cette séparation est celle de lean-golf et c'est la raison pour laquelle un corps d'issue ne peut pas atteindre un token.

Le soumissionnaire n'écrit jamais l'énoncé

Une soumission est une déclaration habitant un type que le défi fixe :

-- 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     := …

Une seule structure plutôt que trois noms isolés, car les noms isolés entrent en collision : un Solve.lean qui importe un Challenge.lean déclarant déjà strategy/verdict/attackWins échoue avec « has already been declared ». Faire de la soumission une valeur d'un type de confiance élimine la collision et réduit la vérification de type du vérificateur à un seul #check.

Pourquoi il est sûr que le soumissionnaire choisisse le score

Deux choses doivent tenir, et aucune n'est acceptée sur parole.

Les nombres font partie de la proposition. La plateforme les écrit dans Cost.lean, Challenge.lean construit score à partir d'eux, et score apparaît dans le type de Solution.wins. Modifier un nombre modifie ce qui doit être prouvé.

La soumission doit habiter notre type. L'étape d'audit importe le défi de confiance aux côtés de la soumission et élabore

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

donc une soumission qui déclare son propre Challenge.SpoC128.Solution entre en collision avec le nôtre, et une soumission qui utilise tout autre type échoue à la vérification de type. Sans cette étape, une soumission qui n'importe tout simplement jamais le challenge peut définir une structure triviale du même nom et être « prouvée » à 0 bit — cette faille était réelle, et les deux attaques sont désormais des cas de CI.

Le nombre de requêtes n'a pas besoin de preuve séparée. Ce n'est pas une affirmation sur un adversaire fini ; c'est un argument de constructeur. Attack.distinguisher q est DDD.ofDDE strategy q verdict, tronqué à q par construction, et Attack.silent_past prouve qu'il n'émet rien au-delà. Il n'y a aucun moyen de dépasser un budget, donc il n'y a rien à vérifier.

budget, advNum et advDen proviennent du formulaire de soumission, et ils ne sont pas dignes de confiance. Ils n'ont pas besoin de l'être : la plateforme les substitue dans Cost.lean, Challenge.lean construit score à partir d'eux, et score apparaît à l'intérieur de Solution.wins. Les nombres font donc partie de la proposition, et non d'une affirmation à son sujet.

Vérifié contre la véritable attaque SpoC-128 :

Affirmation	Résultat
budget = 3, avantage 1	compile — l'affirmation honnête
budget = 1, avantage 1	échoue — Wins 1 1 est un théorème différent et plus fort
budget = 3, avantage 2	échoue — rien ne peut dépasser l'avantage 1

Et il n'y a aucun intérêt à sous-estimer : score = log₂(budget / advantage^e), donc un avantage déclaré plus petit ou un budget déclaré plus grand augmente le score. Les deux directions sont pires. Le seul choix est l'affirmation la plus serrée que vous pouvez réellement prouver.

Quatre autres rejets que le vérificateur effectue sans rien lire :

La triche	Le verdict
affaiblir l'affirmation	incompatibilité de type avec le Solution épinglé
ajouter une hypothèse commode	idem
sorry la preuve	sorryAx n'est pas dans permitted_axioms
native_decide / maxHeartbeats augmenté	rejeté d'emblée

Notation

Rien n'est fixé à l'avance. Sur un schéma que personne n'a étudié, quel avantage est atteignable à quel coût est la question de recherche, donc toute cible est une conjecture — et une cible fixée trop haut note un authentique distingueur 2⁻³⁰ comme zéro. Le tableau mesure plutôt le résultat :

score = log₂( budget / advantage^e )