CONSTANTS
    PROGRAM_SIZE = 100
    PROVER_STAKE = 2
    VERIFIER_PAYMENT = 1

SPECIFICATION Spec

INVARIANT Safe
INVARIANT InvalidProofSafety