Is this a correct formalization of IOI 2024 question 2?

Stream: general

[Daniel Weber]

I'm trying to formalize the mathematical part of the solution to question 2 from IOI 2024. I haven't started with the proof yet, but since the problem is quite complex, I'm unsure if I formalized the statement correctly. Does the following formalization look valid? The question is available on https://github.com/ioi-2024/tasks/blob/main/day1/message/statements/en.pdf

import Mathlib.Data.Vector.Defs
import Mathlib.Data.Fintype.Card

def Message := {l : List Bool // l.length ∈ Set.Icc 1 1024}

def Compromised := {s : Finset (Fin 31) // s.card = 15}

def Aisha := Message → Compromised → List (Mathlib.Vector Bool 31) →
  Option (Mathlib.Vector Bool 31)

def Basma := List (Mathlib.Vector Bool 31) → Message

def Aisha.ValidPreRun (aisha : Aisha) (msg : Message) (comp : Compromised)
    (run : List (Mathlib.Vector Bool 31)) : Prop :=
  ∀ i : Fin run.length, (aisha msg comp (run.take i)).any
    (fun v ↦ ∀ j ∉ comp.val, run[i][j] = v[j])

def Aisha.ValidRun (aisha : Aisha) (msg : Message) (comp : Compromised)
    (run : List (Mathlib.Vector Bool 31)) : Prop :=
  aisha.ValidPreRun msg comp run ∧ aisha msg comp run = none

def Aisha.Small (aisha : Aisha) : Prop :=
  ∀ msg comp run, aisha.ValidPreRun msg comp run → run.length ≤ 66

def Aisha.Correct (aisha : Aisha) (basma : Basma) : Prop :=
  ∀ msg comp run, aisha.ValidRun msg comp run → basma run = msg

def Aisha.winningStrat : Aisha :=
  sorry

def Basma.winningStrat : Basma :=
  sorry

theorem IOI2024Q2 :
    Aisha.winningStrat.Small ∧
      Aisha.winningStrat.Correct Basma.winningStrat := by
  sorry