break-golf

Um quadro para resultados de criptoanálise que são provados, não executados.

Um desafio fixa dois mundos e a afirmação que você deve provar. Você escreve um adversário e uma prova de que ele os distingue. A vitória é a prova: nada é executado, amostrado ou reproduzido, e nenhum humano lê a submissão para decidir se ela conta.

Status: o verificador funciona. Uma issue verify: é elaborada no CI contra o tipo fixado do desafio e auditada com #print axioms; o veredito volta como um comentário. Os registros ainda são adicionados a scoring/ledger.json manualmente.

Este é um projeto Lake autônomo. Ele toma a matemática como uma dependência git fixada a uma revisão, de modo que um quadro verifica contra uma afirmação fixa do modo:

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

O tempo de build é um cache, não um problema: os oleans do Mathlib vêm do seu CDN via lake exe cache get, e os ~400 MB de oleans de revisão fixada e de desafios ficam no cache do Actions com chave baseada no manifesto e nas nossas próprias fontes.

Estrutura

Caminho	O que é
challenges/<name>/Challenge.lean	Confiável. Fixa os tipos exatos que uma submissão deve habitar. Não faz parte de nenhum upload.
challenges/<name>/Cost.lean	Gerado pela plataforma por submissão a partir dos números do formulário.
challenges/<name>/config.json	Pontuação, par, axiomas permitidos, timeout. O único ficheiro que editas para adicionar um desafio.
challenges/<name>/Solve.template.lean	O esqueleto que o submissor preenche.
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, pontuando e ordenando os registos.
tools/record.py	Adiciona uma submissão verificada ao ledger. Recusa tudo o que não esteja proved.
tools/verify.py	Verifica uma submissão: id do desafio como argv[1], corpo em stdin, veredicto JSON em stdout. A mesma interface do lean-golf.
tools/lint_challenges.py	Cada configuração de desafio contém o que o quadro e o verificador precisam.
tools/check_site.py	O site estático consegue carregar e renderizar os seus próprios dados gerados.
scoring/ledger.json	O conjunto de registos.
docs/	O site do GitHub Pages. Estático; lê apenas os dois ficheiros gerados.
examples/	Fixtures de teste: uma submissão que verifica e não ganha nada, e a sua gémea que reivindica em excesso.

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 é executado em push e pull request: os gates --check, o lint de configuração, a verificação do site e uma bateria de submissões que o verificador deve aceitar e deve rejeitar — um sorry, um native_decide, um desafio desconhecido, uma vantagem zero, um corpo sem bloco Lean. workflow_dispatch verifica uma submissão sob demanda sem abrir uma issue.

submission.yml trata uma issue verify: em dois jobs. O primeiro analisa a entrada não confiável e não possui escopos de escrita; o segundo baixa o seu veredito e publica o comentário. Essa divisão é do lean-golf e é a razão pela qual o corpo de uma issue não consegue alcançar um token.

O submissor nunca escreve o enunciado

Uma submissão é uma declaração que habita um tipo fixado pelo desafio:

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

Uma estrutura em vez de três nomes soltos, porque os nomes soltos colidem: um Solve.lean que importa um Challenge.lean que já declara strategy/verdict/attackWins falha com "has already been declared". Tornar a submissão um valor de um tipo confiável elimina a colisão e reduz a verificação de tipos do verificador a um único #check.

Por que é seguro o submissor escolher a pontuação

Duas coisas têm de se verificar, e nenhuma delas é assumida por confiança.

Os números fazem parte da proposição. A plataforma escreve-os em Cost.lean, Challenge.lean constrói score a partir deles, e score aparece dentro do tipo de Solution.wins. Alterar um número altera o que tem de ser provado.

A submissão tem de habitar o nosso tipo. O passo de auditoria importa o desafio confiável juntamente com a submissão e elabora

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

uma submissão que declara seu próprio Challenge.SpoC128.Solution colide com o nosso, e uma que usa qualquer outro tipo falha na verificação de tipos. Sem esta etapa, uma submissão que simplesmente nunca importa o desafio pode definir uma estrutura trivial com o mesmo nome e ser "provada" com 0 bits — essa brecha era real, e ambos os ataques agora são casos de CI.

A contagem de consultas não precisa de prova separada. Não é uma afirmação sobre um adversário finalizado; é um argumento de construtor. Attack.distinguisher q é DDD.ofDDE strategy q verdict, truncado em q por construção, e Attack.silent_past prova que ele não emite nada além disso. Não há como gastar mais do que um orçamento, então não há nada a verificar.

budget, advNum e advDen vêm do formulário de submissão, e não são confiáveis. Não precisam ser: a plataforma os substitui em Cost.lean, Challenge.lean constrói score a partir deles, e score aparece dentro de Solution.wins. Os números, portanto, fazem parte da proposição, não de uma afirmação sobre ela.

Verificado contra o ataque real SpoC-128:

Afirmação	Resultado
budget = 3, vantagem 1	compila — a afirmação honesta
budget = 1, vantagem 1	falha — Wins 1 1 é um teorema diferente e mais forte
budget = 3, vantagem 2	falha — nada pode exceder a vantagem 1

E não há incentivo para subestimar: score = log₂(budget / advantage^e), então uma vantagem declarada menor ou um orçamento declarado maior aumenta a pontuação. Ambas as direções são piores. O único movimento é a afirmação mais justa que você consegue realmente provar.

Mais quatro rejeições que o verificador faz sem ler nada:

A trapaça	O veredito
enfraquecer a afirmação	incompatibilidade de tipos com o Solution fixado
adicionar uma hipótese conveniente	o mesmo
usar sorry na prova	sorryAx não está em permitted_axioms
native_decide / aumentar maxHeartbeats	rejeitado de imediato

Pontuação

Nada é fixado antecipadamente. Em um esquema que ninguém estudou, qual vantagem é alcançável a que custo é a questão de pesquisa, então qualquer meta é um palpite — e uma meta definida alta demais pontua um distinguidor genuíno de 2⁻³⁰ como zero. O placar mede o resultado:

score = log₂( budget / advantage^e )

Vantagem de consultas por unidade; seu logaritmo na base dois é o nível de segurança em bits que o ataque refuta. Menor é melhor. Subestimar sua vantagem aumenta a pontuação, então não há nada a ganhar alegando menos do que você pode provar.