// The program input for lottery/src/main.leo [play]