From def81076debfe7602633f2a29f15d5c7c4723313 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Henrik=20B=C3=B6ving?= Date: Sun, 20 Oct 2024 23:01:21 +0200 Subject: [PATCH] feat: bv_decide introduces uninterpreted symbols everywhere (#5781) Co-authored-by: Tobias Grosser --- .../Frontend/BVDecide/ReifiedBVExpr.lean | 396 +++++++++--------- .../Frontend/BVDecide/ReifiedBVLogical.lean | 102 +++-- .../Frontend/BVDecide/ReifiedBVPred.lean | 106 +++-- tests/lean/run/bv_uninterpreted.lean | 22 + 4 files changed, 354 insertions(+), 272 deletions(-) create mode 100644 tests/lean/run/bv_uninterpreted.lean diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean index 66acea9ef3..3df04f1648 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVExpr.lean @@ -65,202 +65,218 @@ def getNatOrBvValue? (ty : Expr) (expr : Expr) : M (Option Nat) := do | _ => return none /-- -Reify an `Expr` that's a `BitVec`. +Construct an uninterpreted `BitVec` atom from `x`. +-/ +def bitVecAtom (x : Expr) : M (Option ReifiedBVExpr) := do + let t ← instantiateMVars (← whnfR (← inferType x)) + let_expr BitVec widthExpr := t | return none + let some width ← getNatValue? widthExpr | return none + let atom ← mkAtom x width + return some atom + +/-- +Reify an `Expr` that's a constant-width `BitVec`. +Unless this function is called on something that is not a constant-width `BitVec` it is always +going to return `some`. -/ partial def of (x : Expr) : M (Option ReifiedBVExpr) := do - match_expr x with - | BitVec.ofNat _ _ => goBvLit x - | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr - | HOr.hOr _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr - | HXor.hXor _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr - | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr - | HMul.hMul _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr - | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr - | HMod.hMod _ _ _ _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr - | Complement.complement _ _ innerExpr => - unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr - | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr => - let distance? ← getNatOrBvValue? β distanceExpr - if distance?.isSome then - shiftConstReflection - β - distanceExpr + goOrAtom x +where + /-- + Reify `x`, returns `none` if the reification procedure failed. + -/ + go (x : Expr) : M (Option ReifiedBVExpr) := do + match_expr x with + | BitVec.ofNat _ _ => goBvLit x + | HAnd.hAnd _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.BitVec.and_congr + | HOr.hOr _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .or ``Std.Tactic.BVDecide.Reflect.BitVec.or_congr + | HXor.hXor _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.BitVec.xor_congr + | HAdd.hAdd _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .add ``Std.Tactic.BVDecide.Reflect.BitVec.add_congr + | HMul.hMul _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .mul ``Std.Tactic.BVDecide.Reflect.BitVec.mul_congr + | HDiv.hDiv _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .udiv ``Std.Tactic.BVDecide.Reflect.BitVec.udiv_congr + | HMod.hMod _ _ _ _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .umod ``Std.Tactic.BVDecide.Reflect.BitVec.umod_congr + | Complement.complement _ _ innerExpr => + unaryReflection innerExpr .not ``Std.Tactic.BVDecide.Reflect.BitVec.not_congr + | HShiftLeft.hShiftLeft _ β _ _ innerExpr distanceExpr => + let distance? ← getNatOrBvValue? β distanceExpr + if distance?.isSome then + shiftConstReflection + β + distanceExpr + innerExpr + .shiftLeftConst + ``BVUnOp.shiftLeftConst + ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr + else + shiftReflection + β + distanceExpr + innerExpr + .shiftLeft + ``BVExpr.shiftLeft + ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr + | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr => + let distance? ← getNatOrBvValue? β distanceExpr + if distance?.isSome then + shiftConstReflection + β + distanceExpr + innerExpr + .shiftRightConst + ``BVUnOp.shiftRightConst + ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr + else + shiftReflection + β + distanceExpr + innerExpr + .shiftRight + ``BVExpr.shiftRight + ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr + | BitVec.sshiftRight _ innerExpr distanceExpr => + let some distance ← getNatValue? distanceExpr | return none + shiftConstLikeReflection + distance innerExpr - .shiftLeftConst - ``BVUnOp.shiftLeftConst - ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeftNat_congr - else - shiftReflection - β - distanceExpr - innerExpr - .shiftLeft - ``BVExpr.shiftLeft - ``Std.Tactic.BVDecide.Reflect.BitVec.shiftLeft_congr - | HShiftRight.hShiftRight _ β _ _ innerExpr distanceExpr => - let distance? ← getNatOrBvValue? β distanceExpr - if distance?.isSome then - shiftConstReflection - β - distanceExpr - innerExpr - .shiftRightConst - ``BVUnOp.shiftRightConst - ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRightNat_congr - else - shiftReflection - β - distanceExpr - innerExpr - .shiftRight - ``BVExpr.shiftRight - ``Std.Tactic.BVDecide.Reflect.BitVec.shiftRight_congr - | BitVec.sshiftRight _ innerExpr distanceExpr => - let some distance ← getNatValue? distanceExpr | return ← ofAtom x - shiftConstLikeReflection - distance - innerExpr - .arithShiftRightConst - ``BVUnOp.arithShiftRightConst - ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr - | BitVec.zeroExtend _ newWidthExpr innerExpr => - let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x - let some inner ← ofOrAtom innerExpr | return none - let bvExpr := .zeroExtend newWidth inner.bvExpr - let expr := - mkApp3 - (mkConst ``BVExpr.zeroExtend) + .arithShiftRightConst + ``BVUnOp.arithShiftRightConst + ``Std.Tactic.BVDecide.Reflect.BitVec.arithShiftRight_congr + | BitVec.zeroExtend _ newWidthExpr innerExpr => + let some newWidth ← getNatValue? newWidthExpr | return none + let some inner ← goOrAtom innerExpr | return none + let bvExpr := .zeroExtend newWidth inner.bvExpr + let expr := + mkApp3 + (mkConst ``BVExpr.zeroExtend) + (toExpr inner.width) + newWidthExpr + inner.expr + let proof := do + let innerEval ← mkEvalExpr inner.width inner.expr + let innerProof ← inner.evalsAtAtoms + return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr) + newWidthExpr + (toExpr inner.width) + innerExpr + innerEval + innerProof + return some ⟨newWidth, bvExpr, proof, expr⟩ + | BitVec.signExtend _ newWidthExpr innerExpr => + let some newWidth ← getNatValue? newWidthExpr | return none + let some inner ← goOrAtom innerExpr | return none + let bvExpr := .signExtend newWidth inner.bvExpr + let expr := + mkApp3 + (mkConst ``BVExpr.signExtend) + (toExpr inner.width) + newWidthExpr + inner.expr + let proof := do + let innerEval ← mkEvalExpr inner.width inner.expr + let innerProof ← inner.evalsAtAtoms + return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr) + newWidthExpr + (toExpr inner.width) + innerExpr + innerEval + innerProof + return some ⟨newWidth, bvExpr, proof, expr⟩ + | 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 proof := do + let lhsEval ← mkEvalExpr lhs.width lhs.expr + let lhsProof ← lhs.evalsAtAtoms + let rhsProof ← rhs.evalsAtAtoms + let rhsEval ← mkEvalExpr rhs.width rhs.expr + return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr) + (toExpr lhs.width) (toExpr rhs.width) + lhsExpr lhsEval + rhsExpr rhsEval + lhsProof rhsProof + return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩ + | 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) - newWidthExpr - inner.expr - let proof := do - let innerEval ← mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms - return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.zeroExtend_congr) - newWidthExpr - (toExpr inner.width) - innerExpr - innerEval - innerProof - return some ⟨newWidth, bvExpr, proof, expr⟩ - | BitVec.signExtend _ newWidthExpr innerExpr => - let some newWidth ← getNatValue? newWidthExpr | return ← ofAtom x - let some inner ← ofOrAtom innerExpr | return none - let bvExpr := .signExtend newWidth inner.bvExpr - let expr := - mkApp3 - (mkConst ``BVExpr.signExtend) - (toExpr inner.width) - newWidthExpr - inner.expr - let proof := do - let innerEval ← mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms - return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.signExtend_congr) - newWidthExpr - (toExpr inner.width) - innerExpr - innerEval - innerProof - return some ⟨newWidth, bvExpr, proof, expr⟩ - | HAppend.hAppend _ _ _ _ lhsExpr rhsExpr => - let some lhs ← ofOrAtom lhsExpr | return none - let some rhs ← ofOrAtom 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 proof := do - let lhsEval ← mkEvalExpr lhs.width lhs.expr - let lhsProof ← lhs.evalsAtAtoms - let rhsProof ← rhs.evalsAtAtoms - let rhsEval ← mkEvalExpr rhs.width rhs.expr - return mkApp8 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.append_congr) - (toExpr lhs.width) (toExpr rhs.width) - lhsExpr lhsEval - rhsExpr rhsEval - lhsProof rhsProof - return some ⟨lhs.width + rhs.width, bvExpr, proof, expr⟩ - | BitVec.replicate _ nExpr innerExpr => - let some inner ← ofOrAtom innerExpr | return none - let some n ← getNatValue? nExpr | return ← ofAtom x - let bvExpr := .replicate n inner.bvExpr - let expr := mkApp3 (mkConst ``BVExpr.replicate) - (toExpr inner.width) - (toExpr n) - inner.expr - let proof := do - let innerEval ← mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms - return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr) (toExpr n) + inner.expr + let proof := do + let innerEval ← mkEvalExpr inner.width inner.expr + let innerProof ← inner.evalsAtAtoms + return mkApp5 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.replicate_congr) + (toExpr n) + (toExpr inner.width) + innerExpr + innerEval + innerProof + return some ⟨inner.width * n, bvExpr, proof, expr⟩ + | BitVec.extractLsb' _ startExpr lenExpr innerExpr => + let some start ← getNatValue? startExpr | return none + let some len ← getNatValue? lenExpr | return none + let some inner ← goOrAtom innerExpr | return none + let bvExpr := .extract start len inner.bvExpr + let expr := mkApp4 (mkConst ``BVExpr.extract) (toExpr inner.width) - innerExpr - innerEval - innerProof - return some ⟨inner.width * n, bvExpr, proof, expr⟩ - | BitVec.extractLsb' _ startExpr lenExpr innerExpr => - let some start ← getNatValue? startExpr | return ← ofAtom x - let some len ← getNatValue? lenExpr | return ← ofAtom x - let some inner ← ofOrAtom innerExpr | return none - let bvExpr := .extract start len inner.bvExpr - let expr := mkApp4 (mkConst ``BVExpr.extract) - (toExpr inner.width) - startExpr - lenExpr - inner.expr - let proof := do - let innerEval ← mkEvalExpr inner.width inner.expr - let innerProof ← inner.evalsAtAtoms - return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr) startExpr lenExpr - (toExpr inner.width) + inner.expr + let proof := do + let innerEval ← mkEvalExpr inner.width inner.expr + let innerProof ← inner.evalsAtAtoms + return mkApp6 (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.extract_congr) + startExpr + lenExpr + (toExpr inner.width) + innerExpr + innerEval + innerProof + return some ⟨len, bvExpr, proof, expr⟩ + | BitVec.rotateLeft _ innerExpr distanceExpr => + rotateReflection + distanceExpr innerExpr - innerEval - innerProof - return some ⟨len, bvExpr, proof, expr⟩ - | BitVec.rotateLeft _ innerExpr distanceExpr => - rotateReflection - distanceExpr - innerExpr - .rotateLeft - ``BVUnOp.rotateLeft - ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr - | BitVec.rotateRight _ innerExpr distanceExpr => - rotateReflection - distanceExpr - innerExpr - .rotateRight - ``BVUnOp.rotateRight - ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr - | _ => ofAtom x -where - ofAtom (x : Expr) : M (Option ReifiedBVExpr) := do - let t ← instantiateMVars (← whnfR (← inferType x)) - let_expr BitVec widthExpr := t | return none - let some width ← getNatValue? widthExpr | return none - let atom ← mkAtom x width - return some atom + .rotateLeft + ``BVUnOp.rotateLeft + ``Std.Tactic.BVDecide.Reflect.BitVec.rotateLeft_congr + | BitVec.rotateRight _ innerExpr distanceExpr => + rotateReflection + distanceExpr + innerExpr + .rotateRight + ``BVUnOp.rotateRight + ``Std.Tactic.BVDecide.Reflect.BitVec.rotateRight_congr + | _ => return none - ofOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do - let res ← of x + /-- + Reify `x` or abstract it as an atom. + Unless this function is called on something that is not a fixed-width `BitVec` it is always going + to return `some`. + -/ + goOrAtom (x : Expr) : M (Option ReifiedBVExpr) := do + let res ← go x match res with | some exp => return some exp - | none => ofAtom x + | none => bitVecAtom x shiftConstLikeReflection (distance : Nat) (innerExpr : Expr) (shiftOp : Nat → BVUnOp) (shiftOpName : Name) (congrThm : Name) : M (Option ReifiedBVExpr) := do - let some inner ← ofOrAtom innerExpr | return none + let some inner ← goOrAtom innerExpr | return none let bvExpr : BVExpr inner.width := .un (shiftOp distance) inner.bvExpr let expr := mkApp3 @@ -278,24 +294,22 @@ where rotateReflection (distanceExpr : Expr) (innerExpr : Expr) (rotateOp : Nat → BVUnOp) (rotateOpName : Name) (congrThm : Name) : M (Option ReifiedBVExpr) := do - -- Either the shift values are constant or we abstract the entire term as atoms - let some distance ← getNatValue? distanceExpr | return ← ofAtom x + let some distance ← getNatValue? distanceExpr | return none shiftConstLikeReflection distance innerExpr rotateOp rotateOpName congrThm shiftConstReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : Nat → BVUnOp) (shiftOpName : Name) (congrThm : Name) : M (Option ReifiedBVExpr) := do - -- Either the shift values are constant or we abstract the entire term as atoms - let some distance ← getNatOrBvValue? β distanceExpr | return ← ofAtom x + let some distance ← getNatOrBvValue? β distanceExpr | return none shiftConstLikeReflection distance innerExpr shiftOp shiftOpName congrThm shiftReflection (β : Expr) (distanceExpr : Expr) (innerExpr : Expr) (shiftOp : {m n : Nat} → BVExpr m → BVExpr n → BVExpr m) (shiftOpName : Name) (congrThm : Name) : M (Option ReifiedBVExpr) := do - let_expr BitVec _ ← β | return ← ofAtom x - let some inner ← of innerExpr | return none - let some distance ← of distanceExpr | return none + let_expr BitVec _ ← β | return none + let some inner ← goOrAtom innerExpr | return none + let some distance ← goOrAtom distanceExpr | return none let bvExpr : BVExpr inner.width := shiftOp inner.bvExpr distance.bvExpr let expr := mkApp4 @@ -314,8 +328,8 @@ where binaryReflection (lhsExpr rhsExpr : Expr) (op : BVBinOp) (congrThm : Name) : M (Option ReifiedBVExpr) := do - let some lhs ← ofOrAtom lhsExpr | return none - let some rhs ← ofOrAtom rhsExpr | return none + let some lhs ← goOrAtom lhsExpr | return none + let some rhs ← goOrAtom rhsExpr | return none if h : rhs.width = lhs.width then let bvExpr : BVExpr lhs.width := .bin lhs.bvExpr op (h ▸ rhs.bvExpr) let expr := mkApp4 (mkConst ``BVExpr.bin) (toExpr lhs.width) lhs.expr (toExpr op) rhs.expr @@ -335,7 +349,7 @@ where unaryReflection (innerExpr : Expr) (op : BVUnOp) (congrThm : Name) : M (Option ReifiedBVExpr) := do - let some inner ← ofOrAtom innerExpr | return none + let some inner ← goOrAtom innerExpr | return none let bvExpr := .un op inner.bvExpr let expr := mkApp3 (mkConst ``BVExpr.un) (toExpr inner.width) (toExpr op) inner.expr let proof := unaryCongrProof inner innerExpr (mkConst congrThm) @@ -347,7 +361,7 @@ where return mkApp4 congrProof (toExpr inner.width) innerExpr innerEval innerProof goBvLit (x : Expr) : M (Option ReifiedBVExpr) := do - let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← ofAtom x + let some ⟨width, bvVal⟩ ← getBitVecValue? x | return ← bitVecAtom x let bvExpr : BVExpr width := .const bvVal let expr := mkApp2 (mkConst ``BVExpr.const) (toExpr width) (toExpr bvVal) let proof := do diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean index 4a80fb3e09..39c014e3ac 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVLogical.lean @@ -44,40 +44,75 @@ def mkTrans (x y z : Expr) (hxy hyz : Expr) : Expr := def mkEvalExpr (expr : Expr) : M Expr := do return mkApp2 (mkConst ``BVLogicalExpr.eval) (← M.atomsAssignment) expr +/-- +Construct a `ReifiedBVLogical` from `ReifiedBVPred` by wrapping it as an atom. +-/ +def ofPred (bvPred : ReifiedBVPred) : M (Option ReifiedBVLogical) := do + let boolExpr := .literal bvPred.bvPred + let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr + let proof := bvPred.evalsAtAtoms + return some ⟨boolExpr, proof, expr⟩ + +/-- +Construct an uninterrpeted `Bool` atom from `t`. +-/ +def boolAtom (t : Expr) : M (Option ReifiedBVLogical) := do + let some pred ← ReifiedBVPred.boolAtom t | return none + ofPred pred + +/-- +Reify an `Expr` that is a boolean expression containing predicates about `BitVec` as atoms. +Unless this function is called on something that is not a `Bool` it is always going to return `some`. +-/ partial def of (t : Expr) : M (Option ReifiedBVLogical) := do - match_expr t with - | Bool.true => - let boolExpr := .const true - let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true) - let proof := return mkRefl (mkConst ``Bool.true) - return some ⟨boolExpr, proof, expr⟩ - | Bool.false => - let boolExpr := .const false - let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false) - let proof := return mkRefl (mkConst ``Bool.false) - return some ⟨boolExpr, proof, expr⟩ - | Bool.not subExpr => - let some sub ← of subExpr | return none - let boolExpr := .not sub.bvExpr - let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr - let proof := do - let subEvalExpr ← mkEvalExpr sub.expr - let subProof ← sub.evalsAtAtoms - return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof - return some ⟨boolExpr, proof, expr⟩ - | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr - | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr - | BEq.beq α _ lhsExpr rhsExpr => - match_expr α with - | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr - | BitVec _ => goPred t - | _ => return none - | _ => goPred t + goOrAtom t where + /-- + Reify `t`, returns `none` if the reification procedure failed. + -/ + go (t : Expr) : M (Option ReifiedBVLogical) := do + match_expr t with + | Bool.true => + let boolExpr := .const true + let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.true) + let proof := pure <| mkRefl (mkConst ``Bool.true) + return some ⟨boolExpr, proof, expr⟩ + | Bool.false => + let boolExpr := .const false + let expr := mkApp2 (mkConst ``BoolExpr.const) (mkConst ``BVPred) (toExpr Bool.false) + let proof := pure <| mkRefl (mkConst ``Bool.false) + return some ⟨boolExpr, proof, expr⟩ + | Bool.not subExpr => + let some sub ← goOrAtom subExpr | return none + let boolExpr := .not sub.bvExpr + let expr := mkApp2 (mkConst ``BoolExpr.not) (mkConst ``BVPred) sub.expr + let proof := do + let subEvalExpr ← mkEvalExpr sub.expr + let subProof ← sub.evalsAtAtoms + return mkApp3 (mkConst ``Std.Tactic.BVDecide.Reflect.Bool.not_congr) subExpr subEvalExpr subProof + return some ⟨boolExpr, proof, expr⟩ + | Bool.and lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .and ``Std.Tactic.BVDecide.Reflect.Bool.and_congr + | Bool.xor lhsExpr rhsExpr => gateReflection lhsExpr rhsExpr .xor ``Std.Tactic.BVDecide.Reflect.Bool.xor_congr + | BEq.beq α _ lhsExpr rhsExpr => + match_expr α with + | Bool => gateReflection lhsExpr rhsExpr .beq ``Std.Tactic.BVDecide.Reflect.Bool.beq_congr + | BitVec _ => goPred t + | _ => return none + | _ => goPred t + + /-- + Reify `t` or abstract it as an atom. + Unless this function is called on something that is not a `Bool` it is always going to return `some`. + -/ + goOrAtom (t : Expr) : M (Option ReifiedBVLogical) := do + match ← go t with + | some boolExpr => return some boolExpr + | none => boolAtom t + gateReflection (lhsExpr rhsExpr : Expr) (gate : Gate) (congrThm : Name) : M (Option ReifiedBVLogical) := do - let some lhs ← of lhsExpr | return none - let some rhs ← of rhsExpr | return none + let some lhs ← goOrAtom lhsExpr | return none + let some rhs ← goOrAtom rhsExpr | return none let boolExpr := .gate gate lhs.bvExpr rhs.bvExpr let expr := mkApp4 @@ -99,11 +134,8 @@ where return some ⟨boolExpr, proof, expr⟩ goPred (t : Expr) : M (Option ReifiedBVLogical) := do - let some bvPred ← ReifiedBVPred.of t | return none - let boolExpr := .literal bvPred.bvPred - let expr := mkApp2 (mkConst ``BoolExpr.literal) (mkConst ``BVPred) bvPred.expr - let proof := bvPred.evalsAtAtoms - return some ⟨boolExpr, proof, expr⟩ + let some pred ← ReifiedBVPred.of t | return none + ofPred pred end ReifiedBVLogical diff --git a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean index e98f2fb94b..108b2ebc15 100644 --- a/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean +++ b/src/Lean/Elab/Tactic/BVDecide/Frontend/BVDecide/ReifiedBVPred.lean @@ -37,54 +37,68 @@ structure ReifiedBVPred where namespace ReifiedBVPred /-- -Reify an `Expr` that is a proof of a predicate about `BitVec`. +Construct an uninterpreted `Bool` atom from `t`. -/ -def of (t : Expr) : M (Option ReifiedBVPred) := do - match_expr t with - | BEq.beq α _ lhsExpr rhsExpr => - let_expr BitVec _ := α | return none - binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr - | BitVec.ult _ lhsExpr rhsExpr => - binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr - | BitVec.getLsbD _ subExpr idxExpr => - let some sub ← ReifiedBVExpr.of subExpr | return none - let some idx ← getNatValue? idxExpr | return none - let bvExpr : BVPred := .getLsbD sub.bvExpr idx - let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr - let proof := do - let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr - let subProof ← sub.evalsAtAtoms - return mkApp5 - (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr) - idxExpr - (toExpr sub.width) - subExpr - subEval - subProof - return some ⟨bvExpr, proof, expr⟩ - | _ => - /- - Idea: we have t : Bool here, let's construct: - BitVec.ofBool t : BitVec 1 - as an atom. Then construct the BVPred corresponding to - BitVec.getLsb (BitVec.ofBool t) 0 : Bool - We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred. - -/ - let ty ← inferType t - let_expr Bool := ty | return none - let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 - let bvExpr : BVPred := .getLsbD atom.bvExpr 0 - let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0) - let proof := do - let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr - let atomProof ← atom.evalsAtAtoms - return mkApp3 - (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr) - t - atomEval - atomProof - return some ⟨bvExpr, proof, expr⟩ +def boolAtom (t : Expr) : M (Option ReifiedBVPred) := do + /- + Idea: we have t : Bool here, let's construct: + BitVec.ofBool t : BitVec 1 + as an atom. Then construct the BVPred corresponding to + BitVec.getLsb (BitVec.ofBool t) 0 : Bool + We can prove that this is equivalent to `t`. This allows us to have boolean variables in BVPred. + -/ + let ty ← inferType t + let_expr Bool := ty | return none + let atom ← ReifiedBVExpr.mkAtom (mkApp (mkConst ``BitVec.ofBool) t) 1 + let bvExpr : BVPred := .getLsbD atom.bvExpr 0 + let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr 1) atom.expr (toExpr 0) + let proof := do + let atomEval ← ReifiedBVExpr.mkEvalExpr atom.width atom.expr + let atomProof ← atom.evalsAtAtoms + return mkApp3 + (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.ofBool_congr) + t + atomEval + atomProof + return some ⟨bvExpr, proof, expr⟩ + +/-- +Reify an `Expr` that is a predicate about `BitVec`. +Unless this function is called on something that is not a `Bool` it is always going to return `some`. +-/ +partial def of (t : Expr) : M (Option ReifiedBVPred) := do + match ← go t with + | some pred => return some pred + | none => boolAtom t where + /-- + Reify `t`, returns `none` if the reification procedure failed. + -/ + go (t : Expr) : M (Option ReifiedBVPred) := do + match_expr t with + | BEq.beq α _ lhsExpr rhsExpr => + let_expr BitVec _ := α | return none + binaryReflection lhsExpr rhsExpr .eq ``Std.Tactic.BVDecide.Reflect.BitVec.beq_congr + | BitVec.ult _ lhsExpr rhsExpr => + binaryReflection lhsExpr rhsExpr .ult ``Std.Tactic.BVDecide.Reflect.BitVec.ult_congr + | BitVec.getLsbD _ subExpr idxExpr => + let some sub ← ReifiedBVExpr.of subExpr | return none + let some idx ← getNatValue? idxExpr | return none + let bvExpr : BVPred := .getLsbD sub.bvExpr idx + let expr := mkApp3 (mkConst ``BVPred.getLsbD) (toExpr sub.width) sub.expr idxExpr + let proof := do + let subEval ← ReifiedBVExpr.mkEvalExpr sub.width sub.expr + let subProof ← sub.evalsAtAtoms + return mkApp5 + (mkConst ``Std.Tactic.BVDecide.Reflect.BitVec.getLsbD_congr) + idxExpr + (toExpr sub.width) + subExpr + subEval + subProof + return some ⟨bvExpr, proof, expr⟩ + | _ => return none + binaryReflection (lhsExpr rhsExpr : Expr) (pred : BVBinPred) (congrThm : Name) : M (Option ReifiedBVPred) := do let some lhs ← ReifiedBVExpr.of lhsExpr | return none diff --git a/tests/lean/run/bv_uninterpreted.lean b/tests/lean/run/bv_uninterpreted.lean new file mode 100644 index 0000000000..b341a57db8 --- /dev/null +++ b/tests/lean/run/bv_uninterpreted.lean @@ -0,0 +1,22 @@ +import Std.Tactic.BVDecide + +-- Demonstrate some arbitrary width reasoning +example {x y z : BitVec w} : + (x &&& y) ||| (x &&& z) ||| (y &&& z) ||| x ||| y ||| z + = + ~~~ ((~~~ x) &&& (~~~ y) &&& (~~~ z)) := by + ext + simp + bv_decide + +@[irreducible] +def ufBv (x : BitVec w) : BitVec w := x + +example (x y : BitVec 16) : (ufBv x) + (ufBv y) = (ufBv y) + (ufBv x) := by bv_decide + +@[irreducible] +def ufBool (x : Bool) : Bool := x + +example (x y : BitVec 16) (z : Bool) : ((ufBool (x < y)) ∧ z) ↔ (z ∧ ufBool (x < y)) := by bv_decide + +example (x y z : BitVec 16) (h1 : x < z) (h2 : z < (ufBv y)) : x < (ufBv y) := by bv_decide