break-golf

Un tablero para resultados de criptoanálisis que están demostrados, no ejecutados.

Un desafío fija dos mundos y el enunciado que debes demostrar. Escribes un adversario y una prueba de que los distingue. La victoria es la prueba: nada se ejecuta, se muestrea ni se reproduce, y ningún humano lee el envío para decidir si cuenta.

Estado: el verificador se ejecuta. Un issue verify: se elabora en CI contra el tipo fijado del desafío y se audita con #print axioms; el veredicto vuelve como un comentario. Los registros todavía se añaden a scoring/ledger.json a mano.

Este es un proyecto Lake independiente. Toma las matemáticas como una dependencia git fijada a una revisión, de modo que un tablero verifica contra un enunciado fijo del modo:

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

El tiempo de compilación es una caché, no un problema: los oleans de Mathlib provienen de su CDN mediante lake exe cache get, y los ~400 MB de oleans de revisión fijada y de desafíos residen en la caché de Actions indexada por el manifiesto y nuestras propias fuentes.

Estructura

Ruta	Qué es
challenges/<name>/Challenge.lean	De confianza. Fija los tipos exactos que una entrega debe habitar. No forma parte de ninguna carga.
challenges/<name>/Cost.lean	Generado por la plataforma para cada entrega a partir de los números del formulario.
challenges/<name>/config.json	Puntuación, par, axiomas permitidos, tiempo de espera. El único archivo que editas para añadir un desafío.
challenges/<name>/Solve.template.lean	El esqueleto que rellena quien entrega.
tools/manifest.py	Deriva docs/data/manifest.json a partir de challenges/.
tools/ledger.py	Deriva docs/data/ledger.json a partir de scoring/ledger.json, puntuando y ordenando los registros.
tools/record.py	Añade una entrega verificada al registro. Rechaza cualquier cosa que no esté proved.
tools/verify.py	Verifica una entrega: id del desafío como argv[1], cuerpo por stdin, veredicto JSON por stdout. La misma interfaz que la de lean-golf.
tools/lint_challenges.py	Cada configuración de desafío contiene lo que el tablero y el verificador necesitan.
tools/check_site.py	El sitio estático puede cargar y renderizar sus propios datos generados.
scoring/ledger.json	El conjunto de registros.
docs/	El sitio de GitHub Pages. Estático; lee solo los dos archivos generados.
examples/	Fixtures de prueba: una entrega que verifica y no gana nada, y su gemela que reclama de más.

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 se ejecuta en push y pull request: las comprobaciones de --check, el lint de configuración, la comprobación del sitio y una batería de envíos que el verificador debe aceptar y debe rechazar — un sorry, un native_decide, un desafío desconocido, una ventaja cero, un cuerpo sin bloque Lean. workflow_dispatch verifica un envío bajo demanda sin abrir un issue.

submission.yml gestiona un issue verify: en dos jobs. El primero analiza la entrada no confiable y no tiene scopes de escritura; el segundo descarga su veredicto y publica el comentario. Esa separación es de lean-golf y es la razón por la que el cuerpo de un issue no puede alcanzar un token.

El remitente nunca escribe el enunciado

Un envío es una declaración que habita un tipo que el desafío fija:

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

Una sola estructura en lugar de tres nombres sueltos, porque los nombres sueltos colisionan: un Solve.lean que importa un Challenge.lean que ya declara strategy/verdict/attackWins falla con "has already been declared". Hacer que el envío sea un valor de un tipo de confianza elimina la colisión y reduce la comprobación de tipos del verificador a un único #check.

Por qué es seguro que el remitente elija la puntuación

Deben cumplirse dos cosas, y ninguna se da por sentada.

Los números forman parte de la proposición. La plataforma los escribe en Cost.lean, Challenge.lean construye score a partir de ellos, y score aparece dentro del tipo de Solution.wins. Cambiar un número cambia lo que debe demostrarse.

El envío debe habitar nuestro tipo. El paso de auditoría importa el desafío de confianza junto con el envío y elabora

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

una presentación que declara su propio Challenge.SpoC128.Solution colisiona con el nuestro, y una que usa cualquier otro tipo no pasa la verificación de tipos. Sin este paso, una presentación que simplemente nunca importa el desafío puede definir una estructura trivial del mismo nombre y ser "demostrada" a 0 bits — ese agujero era real, y ambos ataques son ahora casos de CI.

El recuento de consultas no necesita una prueba separada. No es una afirmación sobre un adversario terminado; es un argumento del constructor. Attack.distinguisher q es DDD.ofDDE strategy q verdict, truncado en q por construcción, y Attack.silent_past demuestra que no emite nada más allá de eso. No hay forma de exceder un presupuesto, así que no hay nada que verificar.

budget, advNum y advDen provienen del formulario de presentación, y no son de confianza. No necesitan serlo: la plataforma los sustituye en Cost.lean, Challenge.lean construye score a partir de ellos, y score aparece dentro de Solution.wins. Los números son, por lo tanto, parte de la proposición, no una afirmación sobre ella.

Verificado contra el ataque real SpoC-128:

Afirmación	Resultado
budget = 3, ventaja 1	compila — la afirmación honesta
budget = 1, ventaja 1	falla — Wins 1 1 es un teorema diferente y más fuerte
budget = 3, ventaja 2	falla — nada puede superar la ventaja 1

Y no hay incentivo para subestimar: score = log₂(budget / advantage^e), así que una ventaja declarada menor o un presupuesto declarado mayor aumentan la puntuación. Ambas direcciones son peores. El único movimiento es la afirmación más ajustada que realmente puedas demostrar.

Cuatro rechazos más que el verificador hace sin leer nada:

La trampa	El veredicto
debilitar la afirmación	discrepancia de tipos contra el Solution fijado
añadir una hipótesis conveniente	lo mismo
sorry en la prueba	sorryAx no está en permitted_axioms
native_decide / maxHeartbeats elevado	rechazado de plano

Puntuación

Nada está fijado de antemano. En un esquema que nadie ha estudiado, qué ventaja es alcanzable a qué coste es la pregunta de investigación, así que cualquier objetivo es una conjetura — y un objetivo fijado demasiado alto puntúa un distinguidor genuino de 2⁻³⁰ como cero. El tablero mide el resultado en su lugar:

score = log₂( budget / advantage^e )