verify: spoc128

Challenge: spoc128
Budget (queries): 3
Advantage: 1/1
Claimed score: 1.58 bits

Notes: none

Solve.lean

/-
A submission that verifies and wins nothing.

The null adversary: ask no questions, always answer "ideal". Its signed advantage
is exactly 0, so `Wins budget 0` is *true* and provable, the file elaborates
cleanly, and `#print axioms` reports only propext, Classical.choice, Quot.sound.

It is still worth nothing. score = log2(budget / advantage^e) is infinite at
advantage 0: an attack that refutes 0 bits of security refutes nothing. The board
rejects the submission form for it (`non_positive`) rather than the Lean.

Use this to test the honest-but-worthless path: a real proof of a real statement
that is not a break.
-/
import Golf.Challenges.SpoC128DS.Challenge

namespace Solution.SpoC128DS

open RandomSystems.CR18
open RandomSystems.Golf.Instances.SpoC128DS

def solution : Challenge.SpoC128DS.Solution where
  strategy := fun _ _ => none
  verdict := fun _ => false
  wins := by
    have h : Challenge.SpoC128DS.score.advantage = 0 := by
      simp [Golf.Score.advantage, Challenge.SpoC128DS.score]
    rw [h]
    exact Golf.Attack.wins_zero_of_reject _ _ (fun _ _ _ => rfl)

end Solution.SpoC128DS

_{Opened from the break golf board. The verifier builds its own copy of
Challenge.lean; the declarations above are checked against the types pinned
there, then #print axioms is compared with the challenge's permitted list.}

Start with the provided Solve.lean and import Golf.Challenges.SpoC128DS.Challenge, then inspect Challenge.lean as described to confirm the pinned declarations. Run the verifier and check that the proof elaborates, the zero-advantage case is accepted, and #print axioms stays within the permitted list.