// Mystery Cookie - Detective work with Detective Blue
// Teaching verification through mystery solving

program MysteryCookie {

  // The case: Someone ate the cookie!
  case CookieMystery {
    crime: "Cookie stolen from jar"
    time: "This morning"
  }

  // The suspects
  suspects MySuspects {
    Whiskers the Cat: likes Fish
    Buddy the Dog: likes Cookies
    Hoppy the Bunny: likes Carrots
  }

  // The clues we found
  clues MyClues {
    clue1: "Crumbs lead to dog bed"
    clue2: "Cookie jar lid on floor"
    clue3: "Chocolate on Buddy's nose"
  }

  // Ask Blue to investigate!
  Blue do investigate CookieMystery
  Blue do analyze MySuspects with MyClues

  // Blue deduces the answer
  evidence BlueFindings {
    "Crumbs lead to dog bed" points_to Buddy
    "Buddy likes Cookies" points_to Buddy
    "Chocolate on nose" proves Buddy
  }

  // Verify the conclusion
  Blue do verify BlueFindings

  show "Case solved!"
  show Blue.conclusion
  show Blue.confidence + "% certain"

}

// What the child sees (blocks):
// ┌─────────────────────┐
// │ 🔍 Create Case      │
// │ "Cookie stolen!"    │
// └─────────────────────┘
// ┌─────────────────────┐
// │ 🐱🐶🐰 Suspects     │
// └─────────────────────┘
// ┌─────────────────────┐
// │ 🔎 Clues            │
// │ • Crumbs → dog bed  │
// │ • Jar lid on floor  │
// │ • Chocolate nose    │
// └─────────────────────┘
// ┌─────────────────────┐
// │ 🔵 Blue do          │
// │ [Investigate]       │
// └─────────────────────┘
// ┌─────────────────────┐
// │ 🔵 Blue do [Verify] │
// └─────────────────────┘

// Hidden learning: Formal Verification!
// Clues are like assertions/invariants
// "points_to" is like logical implication
// "proves" is like formal proof
// This is how we verify code is correct!
