break-golf

Una board per risultati di crittanalisi che sono dimostrati, non eseguiti.

Una sfida fissa due mondi e l'enunciato che devi dimostrare. Scrivi un avversario e una dimostrazione che lo distingue. La vittoria è la dimostrazione: nulla viene eseguito, campionato o riprodotto, e nessun umano legge la sottomissione per decidere se vale.

Stato: il verificatore funziona. Una issue verify: viene elaborata in CI rispetto al tipo fissato della sfida e verificata con #print axioms; il verdetto torna come commento. I record vengono ancora aggiunti a scoring/ledger.json a mano.

Questo è un progetto Lake autonomo. Prende la matematica come dipendenza git fissata a una revisione, così una board verifica rispetto a un enunciato fisso della modalità:

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

Il tempo di build è una cache, non un problema: gli olean di Mathlib provengono dal suo CDN tramite lake exe cache get, e i ~400 MB di olean della revisione fissata e delle sfide risiedono nella cache delle Actions indicizzata sul manifest e sulle nostre stesse fonti.

Struttura

Percorso	Di cosa si tratta
challenges/<name>/Challenge.lean	Affidabile. Fissa gli esatti tipi che una submission deve abitare. Non fa parte di alcun upload.
challenges/<name>/Cost.lean	Generato dalla piattaforma per ogni submission a partire dai numeri del form.
challenges/<name>/config.json	Punteggio, par, assiomi consentiti, timeout. L'unico file che modifichi per aggiungere una sfida.
challenges/<name>/Solve.template.lean	Lo scheletro che chi invia compila.
tools/manifest.py	Deriva docs/data/manifest.json da challenges/.
tools/ledger.py	Deriva docs/data/ledger.json da scoring/ledger.json, assegnando un punteggio e ordinando i record.
tools/record.py	Aggiunge una submission verificata al ledger. Rifiuta qualsiasi cosa non sia proved.
tools/verify.py	Verifica una submission: id della sfida come argv[1], corpo su stdin, verdetto JSON su stdout. Stessa interfaccia di lean-golf.
tools/lint_challenges.py	Ogni configurazione di sfida contiene ciò che servono alla board e al verificatore.
tools/check_site.py	Il sito statico può caricare e renderizzare i propri dati generati.
scoring/ledger.json	L'insieme dei record.
docs/	Il sito GitHub Pages. Statico; legge solo i due file generati.
examples/	Fixture di test: una submission che verifica e non vince nulla, e il suo gemello che rivendica troppo.

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 viene eseguito su push e pull request: i controlli --check, il lint della configurazione, il controllo del sito e una serie di submission che il verificatore deve accettare e deve rifiutare — un sorry, un native_decide, una challenge sconosciuta, un vantaggio pari a zero, un corpo senza blocco Lean. workflow_dispatch verifica una submission su richiesta senza aprire una issue.

submission.yml gestisce una issue verify: in due job. Il primo analizza l'input non attendibile e non possiede alcuno scope di scrittura; il secondo scarica il suo verdetto e pubblica il commento. Questa suddivisione è di lean-golf ed è il motivo per cui il corpo di una issue non può raggiungere un token.

Chi invia non scrive mai l'enunciato

Una submission è una dichiarazione che abita un tipo fissato dalla challenge:

-- 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 struttura anziché tre nomi sciolti, perché i nomi sciolti entrano in collisione: un Solve.lean che importa un Challenge.lean che dichiara già strategy/verdict/attackWins fallisce con "has already been declared". Rendere la sottomissione un valore di un tipo fidato elimina la collisione e riduce il controllo dei tipi del verificatore a un singolo #check.

Perché è sicuro che sia chi invia a scegliere il punteggio

Due cose devono valere, e nessuna delle due è data per scontata.

I numeri fanno parte della proposizione. La piattaforma li scrive in Cost.lean, Challenge.lean costruisce score a partire da essi, e score compare all'interno del tipo di Solution.wins. Cambiare un numero cambia ciò che deve essere dimostrato.

La sottomissione deve abitare il nostro tipo. La fase di audit importa la challenge fidata insieme alla sottomissione ed elabora

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

una sottomissione che dichiara il proprio Challenge.SpoC128.Solution entra in collisione con il nostro, e una che usa qualsiasi altro tipo non supera il typecheck. Senza questo passaggio una sottomissione che semplicemente non importa mai la challenge può definire una struttura banale con lo stesso nome ed essere "dimostrata" a 0 bit — quella falla era reale, e entrambi gli attacchi sono ora casi CI.

Il conteggio delle query non necessita di una prova separata. Non è un'affermazione su un avversario finito; è un argomento del costruttore. Attack.distinguisher q è DDD.ofDDE strategy q verdict, troncato a q per costruzione, e Attack.silent_past dimostra che non emette nulla oltre a esso. Non c'è modo di sforare un budget, quindi non c'è nulla da verificare.

budget, advNum e advDen provengono dal modulo di sottomissione, e non sono considerati attendibili. Non è necessario che lo siano: la piattaforma li sostituisce in Cost.lean, Challenge.lean costruisce score a partire da essi, e score compare all'interno di Solution.wins. I numeri fanno quindi parte della proposizione, non sono un'affermazione su di essa.

Verificato rispetto al vero attacco SpoC-128:

Affermazione	Risultato
budget = 3, vantaggio 1	compila — l'affermazione onesta
budget = 1, vantaggio 1	fallisce — Wins 1 1 è un teorema diverso e più forte
budget = 3, vantaggio 2	fallisce — nulla può superare il vantaggio 1

E non c'è alcun incentivo a sottostimare: score = log₂(budget / advantage^e), quindi un vantaggio dichiarato più piccolo o un budget dichiarato più grande aumentano il punteggio. Entrambe le direzioni sono peggiori. L'unica mossa è l'affermazione più stretta che si riesce effettivamente a dimostrare.

Altri quattro rifiuti che il verificatore effettua senza leggere nulla:

La scorciatoia	Il verdetto
indebolire l'affermazione	type mismatch rispetto al Solution fissato
aggiungere un'ipotesi comoda	idem
sorry sulla prova	sorryAx non è in permitted_axioms
native_decide / maxHeartbeats aumentato	rifiutato senza appello

Punteggio

Nulla è fissato in anticipo. Su uno schema che nessuno ha studiato, quale vantaggio sia raggiungibile a quale costo è la domanda di ricerca, quindi qualsiasi obiettivo è una congettura — e un obiettivo fissato troppo in alto assegna zero a un genuino distinguisher 2⁻³⁰. La classifica misura invece il risultato:

score = log₂( budget / advantage^e )