From 3221ca1704037e8743c97040b6e551d87898ebe8 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Thu, 20 Mar 2025 16:12:52 +0100 Subject: [PATCH] fix: interaction of enums and fixedInt in bv_decide (#7596) This PR fixes an interaction between the enums and fixedInt pass in bv_decide. Marked as no changelog as this feature isn't released yet. --- .../BVDecide/Frontend/Normalize/Enums.lean | 4 + src/Std/Tactic/BVDecide/Normalize/BitVec.lean | 101 ++++++++++++++++++ tests/lean/run/bv_enums.lean | 6 +- 3 files changed, 108 insertions(+), 3 deletions(-) diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean index 2f9fbee728..2493c8508d 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/Normalize/Enums.lean @@ -439,6 +439,10 @@ partial def enumsPass : Pass where if cfg.structures then (simprocs, relevantLemmas) ← addStructureSimpLemmas simprocs relevantLemmas + -- same for fixed integers + if cfg.fixedInt then + relevantLemmas := relevantLemmas.push (← intToBitVecExt.getTheorems) + let simpCtx ← Simp.mkContext (config := { failIfUnchanged := false, diff --git a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean index 306616becd..9279956b7a 100644 --- a/src/Std/Tactic/BVDecide/Normalize/BitVec.lean +++ b/src/Std/Tactic/BVDecide/Normalize/BitVec.lean @@ -8,6 +8,7 @@ import Init.Data.BitVec.Bitblast import Init.Data.AC import Std.Tactic.BVDecide.Normalize.Bool import Std.Tactic.BVDecide.Normalize.Canonicalize +import Init.Data.SInt.Basic /-! This module contains the `BitVec` simplifying part of the `bv_normalize` simp set. @@ -478,5 +479,105 @@ theorem BitVec.norm_bv_add_mul {x y : BitVec w} : ~~~(x * ~~~y) + 1#w = x + (x * theorem BitVec.norm_bv_add_mul' {x y : BitVec w} : ~~~(~~~y * x) + 1#w = x + (y * x) := by rw [BitVec.mul_comm (~~~y) x, BitVec.mul_comm y x, BitVec.norm_bv_add_mul] +@[int_toBitVec] +theorem UInt8.toBitVec_cond : + UInt8.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond UInt8.toBitVec] + +@[int_toBitVec] +theorem UInt16.toBitVec_cond : + UInt16.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond UInt16.toBitVec] + +@[int_toBitVec] +theorem UInt32.toBitVec_cond : + UInt32.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond UInt32.toBitVec] + +@[int_toBitVec] +theorem UInt64.toBitVec_cond : + UInt64.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond UInt64.toBitVec] + +@[int_toBitVec] +theorem USize.toBitVec_cond : + USize.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond USize.toBitVec] + +@[int_toBitVec] +theorem Int8.toBitVec_cond : + Int8.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond Int8.toBitVec] + +@[int_toBitVec] +theorem Int16.toBitVec_cond : + Int16.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond Int16.toBitVec] + +@[int_toBitVec] +theorem Int32.toBitVec_cond : + Int32.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond Int32.toBitVec] + +@[int_toBitVec] +theorem Int64.toBitVec_cond : + Int64.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond Int64.toBitVec] + +@[int_toBitVec] +theorem ISize.toBitVec_cond : + ISize.toBitVec (bif c then t else e) = bif c then t.toBitVec else e.toBitVec := by + rw [Bool.apply_cond ISize.toBitVec] + +@[int_toBitVec] +theorem UInt8.toBitVec_ite [Decidable c] : + UInt8.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite UInt8.toBitVec] + +@[int_toBitVec] +theorem UInt16.toBitVec_ite [Decidable c] : + UInt16.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite UInt16.toBitVec] + +@[int_toBitVec] +theorem UInt32.toBitVec_ite [Decidable c] : + UInt32.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite UInt32.toBitVec] + +@[int_toBitVec] +theorem UInt64.toBitVec_ite [Decidable c] : + UInt64.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite UInt64.toBitVec] + +@[int_toBitVec] +theorem USize.toBitVec_ite [Decidable c] : + USize.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite USize.toBitVec] + +@[int_toBitVec] +theorem Int8.toBitVec_ite [Decidable c] : + Int8.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite Int8.toBitVec] + +@[int_toBitVec] +theorem Int16.toBitVec_ite [Decidable c] : + Int16.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite Int16.toBitVec] + +@[int_toBitVec] +theorem Int32.toBitVec_ite [Decidable c] : + Int32.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite Int32.toBitVec] + +@[int_toBitVec] +theorem Int64.toBitVec_ite [Decidable c] : + Int64.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite Int64.toBitVec] + +@[int_toBitVec] +theorem ISize.toBitVec_ite [Decidable c] : + ISize.toBitVec (if c then t else e) = if c then t.toBitVec else e.toBitVec := by + rw [apply_ite ISize.toBitVec] + end Normalize end Std.Tactic.BVDecide diff --git a/tests/lean/run/bv_enums.lean b/tests/lean/run/bv_enums.lean index e62786cc57..e7fb92a5a3 100644 --- a/tests/lean/run/bv_enums.lean +++ b/tests/lean/run/bv_enums.lean @@ -229,9 +229,9 @@ inductive Direction where | goingUp structure State where - val : BitVec 16 - low : BitVec 16 - high : BitVec 16 + val : UInt16 + low : UInt16 + high : UInt16 direction : Direction def State.step (s : State) : State :=