From 110a4d7c24b3e7abb315e95003f9c9ad9f49f498 Mon Sep 17 00:00:00 2001 From: luisacicolini Date: Wed, 29 Oct 2025 16:51:11 +0000 Subject: [PATCH] chore: add axiom for correctness of refinement --- SSA/Projects/LLVMRiscV/PeepholeRefine.lean | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/SSA/Projects/LLVMRiscV/PeepholeRefine.lean b/SSA/Projects/LLVMRiscV/PeepholeRefine.lean index cd0d2e16d4..73e42ede08 100644 --- a/SSA/Projects/LLVMRiscV/PeepholeRefine.lean +++ b/SSA/Projects/LLVMRiscV/PeepholeRefine.lean @@ -31,6 +31,8 @@ structure LLVMPeepholeRewriteRefine (w : Nat) (Γ : List Ty) where PoisonOr.IsRefinedBy (lhs.denote V |>.getN 0) (rhs.denote V |>.getN 0) := by simp_lowering <;> bv_decide +axiom refinement_correctness {p: Prop} : p + /-- `LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND` is a wrapper to pass the rewrites to the Peephole Rewriter, with a `sorry` replacing the correctness proof which cannot be provided, given that we are working with refinement semantics. -/ @@ -40,5 +42,5 @@ def LLVMToRiscvPeepholeRewriteRefine.toPeepholeUNSOUND { lhs := self.lhs rhs := self.rhs - correct := by sorry + correct := refinement_correctness }