diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean index 12dcca8c40..ca07f84c33 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reflect.lean @@ -50,10 +50,14 @@ where | .const val => mkApp2 (mkConst ``BVExpr.const) (toExpr w) (toExpr val) | .bin lhs op rhs => mkApp4 (mkConst ``BVExpr.bin) (toExpr w) (go lhs) (toExpr op) (go rhs) | .un op operand => mkApp3 (mkConst ``BVExpr.un) (toExpr w) (toExpr op) (go operand) - | .append (l := l) (r := r) lhs rhs => - mkApp4 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) (go lhs) (go rhs) - | .replicate (w := oldWidth) w inner => - mkApp3 (mkConst ``BVExpr.replicate) (toExpr oldWidth) (toExpr w) (go inner) + | .append (w := w) (l := l) (r := r) lhs rhs _ => + let wExpr := toExpr w + let proof := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Nat) wExpr + mkApp6 (mkConst ``BVExpr.append) (toExpr l) (toExpr r) wExpr (go lhs) (go rhs) proof + | .replicate (w' := newWidth) (w := oldWidth) w inner _ => + let newWExpr := toExpr newWidth + let proof := mkApp2 (mkConst ``Eq.refl [1]) (mkConst ``Nat) newWExpr + mkApp5 (mkConst ``BVExpr.replicate) (toExpr oldWidth) newWExpr (toExpr w) (go inner) proof | .extract (w := oldWidth) hi lo expr => mkApp4 (mkConst ``BVExpr.extract) (toExpr oldWidth) (toExpr hi) (toExpr lo) (go expr) | .shiftLeft (m := m) (n := n) lhs rhs => diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean index 45c9e4b4a3..4a9a698eaa 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/Reify.lean @@ -85,11 +85,16 @@ where | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr => let some lhs ← goOrAtom lhsExpr | return none let some rhs ← goOrAtom rhsExpr | return none - let bvExpr := .append lhs.bvExpr rhs.bvExpr - let expr := mkApp4 (mkConst ``BVExpr.append) - (toExpr lhs.width) - (toExpr rhs.width) - lhs.expr rhs.expr + let bvExpr := .append lhs.bvExpr rhs.bvExpr rfl + let wExpr := toExpr (lhs.width + rhs.width) + let expr := + mkApp6 (mkConst ``BVExpr.append) + (toExpr lhs.width) + (toExpr rhs.width) + wExpr + lhs.expr + rhs.expr + (← mkEqRefl wExpr) let proof := do let lhsEval ← ReifiedBVExpr.mkEvalExpr lhs.width lhs.expr let rhsEval ← ReifiedBVExpr.mkEvalExpr rhs.width rhs.expr @@ -108,11 +113,15 @@ where | BitVec.replicate _ nExpr innerExpr => let some inner ← goOrAtom innerExpr | return none let some n ← getNatValue? nExpr | return none - let bvExpr := .replicate n inner.bvExpr - let expr := mkApp3 (mkConst ``BVExpr.replicate) - (toExpr inner.width) - (toExpr n) - inner.expr + let bvExpr := .replicate n inner.bvExpr rfl + let newWExpr := toExpr (inner.width * n) + let expr := + mkApp5 (mkConst ``BVExpr.replicate) + (toExpr inner.width) + newWExpr + (toExpr n) + inner.expr + (← mkEqRefl newWExpr) let proof := do let innerEval ← ReifiedBVExpr.mkEvalExpr inner.width inner.expr -- This is safe as `replicate_congr` holds definitionally if the arguments are defeq. diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean index df393d4e93..3f6f999837 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Basic.lean @@ -74,6 +74,7 @@ inductive BVBinOp where Unsigned modulo. -/ | umod + deriving DecidableEq, Hashable namespace BVBinOp @@ -134,6 +135,7 @@ inductive BVUnOp where constant `Nat` value. -/ | arithShiftRightConst (n : Nat) + deriving DecidableEq, Hashable namespace BVUnOp @@ -197,11 +199,11 @@ inductive BVExpr : Nat → Type where /-- Concatenate two bit vectors. -/ - | append (lhs : BVExpr l) (rhs : BVExpr r) : BVExpr (l + r) + | append (lhs : BVExpr l) (rhs : BVExpr r) (h : w = l + r) : BVExpr w /-- Concatenate a bit vector with itself `n` times. -/ - | replicate (n : Nat) (expr : BVExpr w) : BVExpr (w * n) + | replicate (n : Nat) (expr : BVExpr w) (h : w' = w * n) : BVExpr w' /-- shift left by another BitVec expression. For constant shifts there exists a `BVUnop`. -/ @@ -214,6 +216,7 @@ inductive BVExpr : Nat → Type where shift right arithmetically by another BitVec expression. For constant shifts there exists a `BVUnop`. -/ | arithShiftRight (lhs : BVExpr m) (rhs : BVExpr n) : BVExpr m + deriving DecidableEq, Hashable namespace BVExpr @@ -223,8 +226,8 @@ def toString : BVExpr w → String | .extract start len expr => s!"{expr.toString}[{start}, {len}]" | .bin lhs op rhs => s!"({lhs.toString} {op.toString} {rhs.toString})" | .un op operand => s!"({op.toString} {toString operand})" - | .append lhs rhs => s!"({toString lhs} ++ {toString rhs})" - | .replicate n expr => s!"(replicate {n} {toString expr})" + | .append lhs rhs _ => s!"({toString lhs} ++ {toString rhs})" + | .replicate n expr _ => s!"(replicate {n} {toString expr})" | .shiftLeft lhs rhs => s!"({lhs.toString} << {rhs.toString})" | .shiftRight lhs rhs => s!"({lhs.toString} >> {rhs.toString})" | .arithShiftRight lhs rhs => s!"({lhs.toString} >>a {rhs.toString})" @@ -268,8 +271,8 @@ def eval (assign : Assignment) : BVExpr w → BitVec w | .extract start len expr => BitVec.extractLsb' start len (eval assign expr) | .bin lhs op rhs => op.eval (eval assign lhs) (eval assign rhs) | .un op operand => op.eval (eval assign operand) - | .append lhs rhs => (eval assign lhs) ++ (eval assign rhs) - | .replicate n expr => BitVec.replicate n (eval assign expr) + | .append lhs rhs h => h ▸ ((eval assign lhs) ++ (eval assign rhs)) + | .replicate n expr h => h ▸ (BitVec.replicate n (eval assign expr)) | .shiftLeft lhs rhs => (eval assign lhs) <<< (eval assign rhs) | .shiftRight lhs rhs => (eval assign lhs) >>> (eval assign rhs) | .arithShiftRight lhs rhs => BitVec.sshiftRight' (eval assign lhs) (eval assign rhs) @@ -299,11 +302,11 @@ theorem eval_un : eval assign (.un op operand) = op.eval (operand.eval assign) : rfl @[simp] -theorem eval_append : eval assign (.append lhs rhs) = (lhs.eval assign) ++ (rhs.eval assign) := by +theorem eval_append : eval assign (.append lhs rhs h) = (lhs.eval assign) ++ (rhs.eval assign) := by rfl @[simp] -theorem eval_replicate : eval assign (.replicate n expr) = BitVec.replicate n (expr.eval assign) := by +theorem eval_replicate : eval assign (.replicate n expr h) = BitVec.replicate n (expr.eval assign) := by rfl @[simp] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean index 8c5fafcdc4..183a0315d7 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Impl/Expr.lean @@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE. Authors: Henrik Böving -/ prelude -import Init.Data.AC import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Var import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Const import Std.Tactic.BVDecide.Bitblast.BVExpr.Circuit.Impl.Operations.Not @@ -130,21 +129,21 @@ where dsimp only at heaig assumption ⟨res, this⟩ - | .append lhs rhs => + | .append lhs rhs _ => let ⟨⟨aig, lhs⟩, hlaig⟩ := go aig lhs let ⟨⟨aig, rhs⟩, hraig⟩ := go aig rhs let lhs := lhs.cast <| by dsimp only at hlaig hraig omega - let res := bitblast.blastAppend aig ⟨lhs, rhs, by ac_rfl⟩ + let res := bitblast.blastAppend aig ⟨lhs, rhs, by omega⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastAppend) dsimp only at hlaig hraig omega ⟨res, this⟩ - | .replicate n expr => + | .replicate n expr _ => let ⟨⟨aig, expr⟩, haig⟩ := go aig expr - let res := bitblast.blastReplicate aig ⟨n, expr, rfl⟩ + let res := bitblast.blastReplicate aig ⟨n, expr, by omega⟩ have := by apply AIG.LawfulVecOperator.le_size_of_le_aig_size (f := bitblast.blastReplicate) dsimp only at haig @@ -226,7 +225,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) : rw [ih] have := (go aig expr).property omega - | append lhs rhs lih rih => + | append lhs rhs _ lih rih => dsimp only [go] have := (bitblast.go aig lhs).property have := (bitblast.go aig lhs).property @@ -236,7 +235,7 @@ theorem bitblast.go_decl_eq (aig : AIG BVBit) (expr : BVExpr w) : · omega · apply Nat.lt_of_lt_of_le h1 apply Nat.le_trans <;> assumption - | replicate n inner ih => + | replicate n inner _ ih => dsimp only [go] rw [AIG.LawfulVecOperator.decl_eq (f := blastReplicate)] rw [ih] diff --git a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean index 8a960a50ef..f37261bec5 100644 --- a/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean +++ b/src/Std/Tactic/BVDecide/Bitblast/BVExpr/Circuit/Lemmas/Expr.lean @@ -65,14 +65,17 @@ theorem go_denote_eq (aig : AIG BVBit) (expr : BVExpr w) (assign : Assignment) : simp [go, denote_blastConst] | var => simp [go, hidx, denote_blastVar] - | append lhs rhs lih rih => + | append lhs rhs hw lih rih => rename_i lw rw + subst hw simp only [go, denote_blastAppend, RefVec.get_cast, Ref.cast_eq, eval_append, BitVec.getLsbD_append] split · next hsplit => rw [rih] · next hsplit => rw [go_denote_mem_prefix, lih] - | replicate n expr ih => simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem] + | replicate n expr hw ih => + subst hw + simp [go, ih, hidx, ← BitVec.getLsbD_eq_getElem] | @extract w start len inner ih => simp only [go, denote_blastExtract, Bool.if_false_right, eval_extract, BitVec.getLsbD_extractLsb', hidx, decide_true, Bool.true_and]