import Aeneas
import Tiny
open Aeneas Aeneas.Std Result

-- Seeded bug: `avg_buggy` is meant to be floor((a+b)/2) but `a + b` overflows U32.
-- Kernel-checked witness that it panics (integer overflow) on a valid input pair.
theorem avg_buggy_overflows :
    tiny.avg_buggy 4294967295#u32 4294967295#u32 = fail Error.integerOverflow := by
  unfold tiny.avg_buggy
  simp +decide [HAdd.hAdd, Std.UScalar.add, Std.UScalar.tryMk, Std.UScalar.tryMkOpt]

-- The functional spec only holds under a no-overflow precondition (this is the property a prover arm would
-- have to find; the negation above is the disproof of the unconditional version).
theorem avg_buggy_spec_needs_pre (a b : U32) (h : a.val + b.val ≤ U32.max) :
    tiny.avg_buggy a b ⦃ r => r.val = (a.val + b.val) / 2 ⦄ := by
  unfold tiny.avg_buggy
  step*

-- A correct function: total (no panic) and correct on every input.
theorem abs_diff_correct (a b : U32) :
    tiny.abs_diff a b ⦃ r => r.val = Int.natAbs (a.val - b.val) ⦄ := by
  unfold tiny.abs_diff
  split
  · step*
  · step*