diff --git a/Medusa/Medusa/Fp/Basic.lean b/Medusa/Medusa/Fp/Basic.lean index 99b542da6c..9f35f5ee72 100644 --- a/Medusa/Medusa/Fp/Basic.lean +++ b/Medusa/Medusa/Fp/Basic.lean @@ -114,6 +114,9 @@ def eval (assign : Std.HashMap Nat BVExpr.PackedBitVec) : FpExpr e → PackedFlo | .add => add (eval assign lhs) (eval assign rhs) .RNE end FpExpr +-- TODO: put this stuff in a namespace. +#check add + inductive FpBinaryPredKind | eq deriving Hashable, DecidableEq, Repr diff --git a/Medusa/Medusa/Fp/FpGeneralize.lean b/Medusa/Medusa/Fp/FpGeneralize.lean index b570571f79..4ec95f5cf2 100644 --- a/Medusa/Medusa/Fp/FpGeneralize.lean +++ b/Medusa/Medusa/Fp/FpGeneralize.lean @@ -808,9 +808,8 @@ def evalFpGeneralize : Tactic section Examples set_option warn.sorry false -#guard_msgs in theorem demo (x y : BitVec 8) : (0#8 - x ||| y) + y = (y ||| 0#8 - x) + y := by - -- fp_generalize + fp_generalize sorry diff --git a/Medusa/Medusa/Fp/Reflect.lean b/Medusa/Medusa/Fp/Reflect.lean index 6260bfba5d..dfae404b25 100644 --- a/Medusa/Medusa/Fp/Reflect.lean +++ b/Medusa/Medusa/Fp/Reflect.lean @@ -49,8 +49,28 @@ structure ParsedFpExpr where abbrev ParsedFpLogicalExpr := ParsedLogicalExpr ParsedFpExpr GenFpLogicalExpr +#check PackedFloat 10 20 + +structure PackedFloatTyExpr where + m : Expr + e : Expr + +def getPackedFloatTy? (e : Expr) : MetaM (Option (PackedFloatTyExpr)) := do + let eType ← inferType e + match_expr eType with + | PackedFloat m e => return some {m, e} + | _ => return none + -- | TODO: Allow ParseExprM to throw errors, instead of returning an Option in many cases. -partial def toBVExpr (expr : Expr) (width: Nat) : ParseExprM (Option (FpExprWrapper)) := do +partial def toFpExpr (expr : Expr) (width: Nat) : ParseExprM (Option (FpExprWrapper)) := do + let t ← inferType expr + let some packedFloatTy ← getPackedFloatTy? expr | throwError m!"Could not determine the packed float type of {expr} : {t}" + match_expr expr with + | add a b => throwError "found 'add' node" + | _ => + -- logInfo m!"failed to convert {expr} into an FpExpr." + return none +/- go expr where go (x : Expr) : ParseExprM (Option (FpExprWrapper)) := do @@ -181,30 +201,39 @@ partial def toBVExpr (expr : Expr) (width: Nat) : ParseExprM (Option (FpExprWrap return some {bvExpr := newExpr, width := pbv.w} | some var => let newExpr : FpExpr pbv.w := FpExpr.var var return some {bvExpr := newExpr, width := pbv.w} +-/ def parseExprs (lhsExpr rhsExpr : Expr) (width : Nat): ParseExprM (Option ParsedFpLogicalExpr) := do - let some lhsRes ← toBVExpr lhsExpr width | throwError "Could not extract lhs: {lhsExpr}" - + logInfo "C1.A" + let some lhsRes ← toFpExpr lhsExpr width | throwError "Could not extract lhs: {lhsExpr}" let state ← get let lhs: ParsedFpExpr := {bvExpr := lhsRes.bvExpr, width := lhsRes.width, symVars := state.symVarToVal, inputVars := state.inputVarIdToVariable} + throwError "C1.B" - let some rhsRes ← toBVExpr rhsExpr width | throwError "Could not extract rhs: {rhsExpr}" + let some rhsRes ← toFpExpr rhsExpr width | throwError "Could not extract rhs: {rhsExpr}" let state ← get + logInfo "C1.C" + let rhsInputVars := state.inputVarIdToVariable.filter fun k _ => !lhs.inputVars.contains k let rhsSymVars := state.symVarToVal.filter fun k _ => !lhs.symVars.contains k + throwError "C1.D" + let rhs: ParsedFpExpr := {bvExpr := rhsRes.bvExpr, width := rhsRes.width, symVars := rhsSymVars, inputVars := rhsInputVars} + logInfo "C1.E" trace[Generalize] m! "lhs width: {lhsRes.width}; rhs width: {rhsRes.width}" if h : lhsRes.width = rhsRes.width then + throwError "C1.F" let rhsExpr := h ▸ rhsRes.bvExpr -- | TODO: why do we need it to be a 'BoolExpr'? We should have an interface -- that asks for it to be converted to a 'BoolExpr'. let bvLogicalExpr := BoolExpr.literal (FpPredicate.bin lhsRes.bvExpr FpBinaryPredKind.eq rhsExpr) trace[Generalize] m! "BVLogicalExpr: {bvLogicalExpr}" return some {lhs := lhs, rhs := rhs, state := state, logicalExpr := bvLogicalExpr} + throwError "C1.G" return none @@ -253,23 +282,23 @@ def toExpr (_ParsedFpExpr : ParsedFpLogicalExpr) (bvLogicalExpr: GenFpLogicalExp | .beq => return mkApp4 (.const ``BEq.beq [levelZero]) (mkConst ``Bool) (beqBoolInstExpr) (← go lhs) (← go rhs) | _ => throwError m! "Unsupported operation in toExpr" -/- def toBVExpr' (bvExpr : FpExpr w) : GeneralizerStateM (BVExpr w) := do +/- def toFpExpr' (bvExpr : FpExpr w) : GeneralizerStateM (BVExpr w) := do match bvExpr with | .var idx => return BVExpr.var idx | .const val => return BVExpr.const val - | .bin lhs op rhs => return BVExpr.bin (← toBVExpr' lhs) op (← toBVExpr' rhs) - | .un op expr => return BVExpr.un op (← toBVExpr' expr) - | .append lhs rhs h => return BVExpr.append (← toBVExpr' lhs) (← toBVExpr' rhs) h - | .replicate n expr h => return BVExpr.replicate n (← toBVExpr' expr) h - | .shiftLeft lhs rhs => return BVExpr.shiftLeft (← toBVExpr' lhs) (← toBVExpr' rhs) - | .shiftRight lhs rhs => return BVExpr.shiftRight (← toBVExpr' lhs) (← toBVExpr' rhs) - | .arithShiftRight lhs rhs =>return BVExpr.arithShiftRight (← toBVExpr' lhs) (← toBVExpr' rhs) + | .bin lhs op rhs => return BVExpr.bin (← toFpExpr' lhs) op (← toFpExpr' rhs) + | .un op expr => return BVExpr.un op (← toFpExpr' expr) + | .append lhs rhs h => return BVExpr.append (← toFpExpr' lhs) (← toFpExpr' rhs) h + | .replicate n expr h => return BVExpr.replicate n (← toFpExpr' expr) h + | .shiftLeft lhs rhs => return BVExpr.shiftLeft (← toFpExpr' lhs) (← toFpExpr' rhs) + | .shiftRight lhs rhs => return BVExpr.shiftRight (← toFpExpr' lhs) (← toFpExpr' rhs) + | .arithShiftRight lhs rhs =>return BVExpr.arithShiftRight (← toFpExpr' lhs) (← toFpExpr' rhs) | _ => throwError m! "Unsupported operation provided: {bvExpr}" def toBVLogicalExpr (bvLogicalExpr: GenFpLogicalExpr) : GeneralizerStateM BVLogicalExpr := do match bvLogicalExpr with - | .literal (GenBVPred.bin lhs op rhs) => return BoolExpr.literal (BVPred.bin (← toBVExpr' lhs) op (← toBVExpr' rhs)) + | .literal (GenBVPred.bin lhs op rhs) => return BoolExpr.literal (BVPred.bin (← toFpExpr' lhs) op (← toFpExpr' rhs)) | .const b => return BoolExpr.const b | .not boolExpr => return BoolExpr.not (← toBVLogicalExpr boolExpr) | .gate gate lhs rhs => return BoolExpr.gate gate (← toBVLogicalExpr lhs) (← toBVLogicalExpr rhs) diff --git a/Medusa/Medusa/Generalize.lean b/Medusa/Medusa/Generalize.lean index 20192c1820..cd1c24b54f 100644 --- a/Medusa/Medusa/Generalize.lean +++ b/Medusa/Medusa/Generalize.lean @@ -539,7 +539,6 @@ def parseAndGeneralize [H : HydrableParseAndGeneralize parsedExpr genLogicalExpr let some width ← H.getWidth w | throwError m! "Could not determine the rewrite width from {w}" let startTime ← Core.liftIOCore IO.monoMsNow - -- Parse the input expression let widthId : Nat := 9481 let widthName := (Name.mkSimple "w") @@ -550,7 +549,7 @@ def parseAndGeneralize [H : HydrableParseAndGeneralize parsedExpr genLogicalExpr symVarIdToVariable := initialState.symVarIdToVariable.insert widthId widthVariable , displayNameToVariable := initialState.displayNameToVariable.insert widthName widthVariable , originalWidth := width} - + -- | seems to crash here. let some parsedLogicalExpr ← (H.parseExprs lhsExpr rhsExpr width).run' initialState | throwError "Unsupported expression provided" @@ -565,22 +564,25 @@ def parseAndGeneralize [H : HydrableParseAndGeneralize parsedExpr genLogicalExpr let mut variableDisplayNames : Std.HashMap Nat Name := Std.HashMap.emptyWithCapacity for (id, var) in allVariables.toList do variableDisplayNames := variableDisplayNames.insert id var.name - + throwError "F" trace[Generalize] m! "All vars: {variableDisplayNames}" match generalizeRes with - | some res => match context with - | GeneralizeContext.Command => let pretty := H.prettify res variableDisplayNames - pure m! "Raw generalization result: {res} \n Input expression: {hExpr} has generalization: {pretty}" - | GeneralizeContext.Tactic name => pure m! "{H.prettifyAsTheorem name res variableDisplayNames}" + | some res => + throwError "G" + match context with + | GeneralizeContext.Command => + let pretty := H.prettify res variableDisplayNames + pure m! "Raw generalization result: {res} \n Input expression: {hExpr} has generalization: {pretty}" + | GeneralizeContext.Tactic name => + pure m! "{H.prettifyAsTheorem name res variableDisplayNames}" | none => throwError m! "Could not generalize {bvLogicalExpr}" - | _ => throwError m!"The top level constructor is not an equality predicate in {hExpr}" open Lean Lean.Elab Command Term in -def generalizeCommand +def generalizeCommand (H : HydrableParseAndGeneralize parsedExpr genLogicalExpr genExpr) (stx : Syntax) : CommandElabM Unit := do - withoutModifyingEnv <| runTermElabM fun _ => + withoutModifyingEnv <| runTermElabM fun _ => Term.withDeclName `_reduceWidth do let hExpr ← Term.elabTerm stx none trace[Generalize] m! "hexpr: {hExpr}" @@ -592,7 +594,8 @@ def generalizeTactic (H : HydrableParseAndGeneralize parsedExpr genLogicalExpr genExpr) (expr : Expr) : TacticM Unit := do let name ← mkAuxDeclName `generalized - let msg ← withoutModifyingEnv <| withoutModifyingState do + -- let msg ← withoutModifyingEnv <| withoutModifyingState do + let msg ← do Lean.Elab.Tactic.withMainContext do -- | TODO: should we add a unification check, that allows the user -- to prove the more general version?