VOD: https://www.youtube.com/watch?v=IcyFhrWyzdg

Verification of Program Optimisations (Lean)

Work on https://github.com/l1mey112/bitbasher.

Agenda.

• You would probably want to go over what this project is even about before you go those things below. ✅ 2025-12-17
  • Create blog post on this.

• Work on a general theory of noUb and wf functions, so you can make conversions and rewrites super easy. ✅ 2025-12-17

• The proposition wf : f poison = poison only tells you that f doesn’t observe poison if f is nonconstant/doesn’t depend on the argument. Though, it usually does depend on the argument so is this really a misname? ✅ 2025-12-17

• The wf argument to congrApp shouldn’t be passed by the user basically ever. Calculating this should be fast too, it shouldn’t use by simp [simp_iN].

theorem congrApp {n} (f : iN n → iN n)
    {wf : f poison = poison := by opt_poison_input}
    {a a' : iN n} (h : a ~> a') : f a ~> f a'

Aftermath

• Infrastructure for opt theorems.
  • The above, and for example using a Monad as you traverse terms to ascertain whether or not UB is preserved or not. (This uses a general theory of noUb, wF, ubEquiv', ubEquiv, whatever works.)
• General typeclasses the different possible ways to raise UB. So for example x + y doesn’t introduce any MORE UB than it’s arguments, but x +nsw y does.
  • Generally you could have a theorem relating these typeclasses.

Proving.
1. Prove by rewriting based on what you already know (human).
2. Prove by the semantics of the actual program (human).
3. Automatically prove (machine).

At the moment, (1), (3). I guess we need (2).

Solving (2)

• Support argument to the conversion iN_convert_goal_bitvec a b c, then use simplification lemmas to bring things back down in terms of BitVec.

/-
(h :
  (x ≥ₛ 0) &&& (y ≥ₛ 0) &&& (z ≥ₛ 0) ~> 1 ∨
  (x <ₛ 0) &&& (y <ₛ 0) &&& (z <ₛ 0) ~> 1)
-/
def hyp {n} (a b c : BitVec n) :=
  !(a.sle 0) && !(b.sle 0) && !(c.sle 0) ∨
  (a.slt 0) && (b.slt 0) && (c.slt 0)

• When using iN_convert_goal_bitvec there should be another SimpSet to further reduce to the definition but don’t go further than BitVec.

@[opt ideal]
theorem add_zero {n} (x : iN n) : x + 0 ~> x := by
  iN_convert_goal_bitvec
  /-
  case bitvec
  n : Nat
  a✝ : BitVec n
  ⊢ bitvec a✝ + 0 ~> bitvec a✝
  -/

• When doing simp only [iN_simp] you end up with the below which isn’t really useful because you’re not going to the definition. I would want to convert ~> bitvec to something.

⊢ (bitvec a✝).pBind₂ (bitvec 0#n) iN.add? ~> bitvec a✝