Expressing ability to construct any value from UB

Stream: general

[l1mey]

I am working on a project to formalise certain rewrite rules in an the integer subset of the LLVM IR, with poison to model UB. In the LLVM LangRef #poison-values, it states that you can replace a possible poison value with any value for that type, even a different value in each different case. I am confused on how I would express this though, as I currently have (this is a minimal working example):

/--
LLVM-style integers with poison value.
-/
inductive iN (bits : Nat) : Type where
  | bitvec : BitVec bits → iN bits
  | poison : iN bits

export iN (poison bitvec)

instance : OfNat (iN n) val where
  ofNat := iN.bitvec (BitVec.ofNat n val)

inductive Cases : (iN n) → Prop where
  | one : Cases (12 : iN n)
  | two : Cases (poison)

theorem forge12 {n} (x : iN n) (h : Cases x)
    : x = 12 := by

  cases h
  case one => rfl
  case two =>
    sorry

What could I possibly do here?

[William Sørensen]

Is this maybe related to @Tobias Grosser 's LeanMLIR work? @Alex Keizer might be able to help

[l1mey]

Not particularly related, just my own small project. I solved the problem though, I was thinking of rewrites completely wrong. A rewrite from x to y isn't an equivalence relation, it's more like a preorder. So you can have poision ~> 12, but you can't coerce 12 ~> poison. Example below:

/--
`Refines x y` means the value `x` can be refined into the concrete value `y`.
This reads like an action: `refine x into y`.
-/
inductive Refines {n} : iN n → iN n → Prop where
  /-- A bitvector refines to itself. -/
  | bv_refl (v : BitVec n) : Refines (bitvec v) (bitvec v)
  /-- Poison can be refined into any bitvector. -/
  | poison_forge (v : BitVec n) : Refines poison (bitvec v)

abbrev RefinesReversed {n} (x y : iN n) := Refines y x
abbrev RefinesIff {n} (x y : iN n) := Refines x y ∧ Refines y x

infix:50 " ~> "  => Refines
infix:50 " <~ "  => RefinesReversed
infix:50 " <~> " => RefinesIff

image.png

[l1mey]

Though, from here I've got a long road ahead making these definitions amenable to trivial proof.

[William Sørensen]

This is quote cool and good luck! I was planning on writing a compiler where one of the arguments for the compilation is that the source code is free of UB, meaning that if there is UB, and you have a compiled result you can just exfalso it, but i havent actually thought about that to any actual detail.

[William Sørensen]

but yeah would be cool to see where this project goes

[l1mey]

This definition is quite convenient. Here is a formal proof that compilers can rewrite INT32_MAX + 1 to 12:

image.png

[Alex Keizer]

This is quite similar to how we model poison in LeanMLIR!

[l1mey]

Using this definition, I've come into issues with automated proof: #general > Converting goals to be bitblasted like BVDecide. Maybe someone might be able to look at it?