bv_normalize produces a proof with metavars that cannot be checked by the kernel

[bollu]

Description

Consider the MWE:

import Lean

-- "4.12.0-nightly-2024-09-30"
#eval Lean.versionString

def mem_subset (a1 a2 b1 b2 : BitVec 64) : Bool :=
  (b2 - b1 = BitVec.ofNat 64 (2^64 - 1)) ||
  ((a2 - b1 <= b2 - b1 && a1 - b1 <= a2 - b1))

theorem mem_subset_refl : mem_subset a1 a2 a1 a2 := by
  unfold mem_subset
  -- bv_decide -- this succeeds. 
  bv_normalize
-- (kernel) declaration has metavariables 'mem_subset_refl

Context

Occurred when bumping the lean toolchain for leanprover/lnsym. I was bumping the toolchain to get the new bv_decide preprocessing fixes.

Impact

Add 👍 to issues you consider important. If others are impacted by this issue, please ask them to add 👍 to it.