| 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* | |