From b726a86d56568e91c453fe524033acea309e42e3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 12 Jul 2026 12:41:00 +0100 Subject: [PATCH 1/3] feat(interpret): prove interpretOp' monotone for the riscv dialect RISC-V operands are registers, which carry no poison, so refinement on them is equality: an operand array of registers is refined only by itself (`RuntimeValue.eq_of_arrayIsRefinedBy_of_regs`). That discharges all 110 riscv opcodes at once, without reasoning about any of them individually: either every operand is a register, and then the refined operands are the original ones, so both sides interpret to the very same result; or some operand is not a register, and every opcode that reads its operands fails to interpret, while the opcodes that ignore their operands (`li`, `lui`) again produce the very same result on both sides. Dispatch the `riscv` case of `interpretOp'_monotone` to it. The other dialects remain `sorry`. --- Veir/Interpreter/Lemmas.lean | 72 +++++++++++++++++++++++++++++++++++- 1 file changed, 71 insertions(+), 1 deletion(-) diff --git a/Veir/Interpreter/Lemmas.lean b/Veir/Interpreter/Lemmas.lean index f6b356120..b4c0b9a04 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -1,6 +1,7 @@ import Veir.Interpreter.Basic import Veir.Dominance import Veir.Interpreter.Refinement.Basic +import Veir.Interpreter.Refinement.Lemmas import Veir.Verifier namespace Veir @@ -516,6 +517,70 @@ theorem exists_interpretOp'_eq_some {ctx : WfIRContext OpCode} {op : OperationPt (mem : MemoryState) : ∃ res, op.interpret ctx.raw operands mem = some res := by sorry +/-- The relation `interpretOp'_monotone` establishes between two interpretation results. -/ +abbrev InterpretResultIsRefinedBy : + Array RuntimeValue × MemoryState × Option ControlFlowAction → + Array RuntimeValue × MemoryState × Option ControlFlowAction → Prop := + fun r₁ r₂ => r₁.1 ⊒ r₂.1 ∧ r₁.2.1 = r₂.2.1 ∧ + ControlFlowAction.optionIsRefinedBy r₁.2.2 r₂.2.2 + +/-- `InterpretResultIsRefinedBy` is reflexive, so an interpretation result always refines itself. -/ +@[grind .] +theorem interpretResult_isRefinedBy_refl + (x : Interp (Array RuntimeValue × MemoryState × Option ControlFlowAction)) : + Interp.isRefinedBy InterpretResultIsRefinedBy x x := by + rcases x with _ | (x | _) <;> grind [Interp.isRefinedBy] + +/-- +A register runtime value can only be refined by itself, so operand arrays that consist purely of +registers are refined only by themselves. This makes every dialect whose operands are registers +(`riscv`, `riscv_cf`, `riscv_stack`, `rv64`) monotone for free: the refined operands are the +original ones, so both sides interpret to the very same result. +-/ +theorem RuntimeValue.eq_of_arrayIsRefinedBy_of_regs {a b : Array RuntimeValue} + (h : a ⊒ b) (hregs : ∀ v ∈ a, ∃ r, v = .reg r) : b = a := by + obtain ⟨hsize, helem⟩ := h + apply Array.ext hsize.symm + intro i hib hia + obtain ⟨r, hr⟩ := hregs a[i] (Array.getElem_mem hia) + have hrefines := helem i hia + rw [getElem!_pos a i hia, getElem!_pos b i hib, hr] at hrefines + rw [hr] + exact RuntimeValue.reg_of_isRefinedBy hrefines + +/-- +`Riscv.interpretOp'` is monotone in its operands. + +RISC-V operands are registers, which carry no poison, so refinement on them is equality: either +every operand is a register -- and then the refined operands are the original ones and both sides +interpret to the very same result -- or some operand is not a register, and every opcode that +reads its operands fails to interpret (opcodes that ignore their operands, such as `li`, again +produce the very same result on both sides). +-/ +theorem Riscv.interpretOp'_monotone {operands operands' : Array RuntimeValue} : + operands ⊒ operands' → + Interp.isRefinedBy InterpretResultIsRefinedBy + (Riscv.interpretOp' opType properties resultTypes operands blockOperands mem) + (Riscv.interpretOp' opType properties resultTypes operands' blockOperands mem) := by + intro h + by_cases hregs : ∀ v ∈ operands, ∃ r, v = .reg r + · have hb : operands' = operands := RuntimeValue.eq_of_arrayIsRefinedBy_of_regs h hregs + subst hb + apply interpretResult_isRefinedBy_refl + · cases opType <;> + simp only [Riscv.interpretOp'] <;> + first + | apply interpretResult_isRefinedBy_refl + | (split + · exfalso + rename_i heq + refine hregs (fun v hv => ?_) + have hv' : v ∈ operands.toList := hv.val + rw [heq] at hv' + simp at hv' + grind + · simp [Interp.isRefinedBy]) + set_option warn.sorry false in theorem interpretOp'_monotone (opType : OpCode) (properties : propertiesOf opType) (resultTypes : Array TypeAttr) @@ -526,7 +591,12 @@ theorem interpretOp'_monotone ControlFlowAction.optionIsRefinedBy r₁.2.2 r₂.2.2) (interpretOp' opType properties resultTypes operands blockOperands mem) (interpretOp' opType properties resultTypes operands' blockOperands mem) := by - sorry + intro h + cases opType + case riscv => + simp only [interpretOp'] + exact Riscv.interpretOp'_monotone h + all_goals sorry set_option warn.sorry false in /-- From 3bae2e43732f8af95ed2892d4db76fcdbb7c5fd7 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 12 Jul 2026 19:31:11 +0100 Subject: [PATCH 2/3] Gold a proof using `grind` --- Veir/Interpreter/Lemmas.lean | 9 +-------- 1 file changed, 1 insertion(+), 8 deletions(-) diff --git a/Veir/Interpreter/Lemmas.lean b/Veir/Interpreter/Lemmas.lean index b4c0b9a04..3cad68029 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -539,14 +539,7 @@ original ones, so both sides interpret to the very same result. -/ theorem RuntimeValue.eq_of_arrayIsRefinedBy_of_regs {a b : Array RuntimeValue} (h : a ⊒ b) (hregs : ∀ v ∈ a, ∃ r, v = .reg r) : b = a := by - obtain ⟨hsize, helem⟩ := h - apply Array.ext hsize.symm - intro i hib hia - obtain ⟨r, hr⟩ := hregs a[i] (Array.getElem_mem hia) - have hrefines := helem i hia - rw [getElem!_pos a i hia, getElem!_pos b i hib, hr] at hrefines - rw [hr] - exact RuntimeValue.reg_of_isRefinedBy hrefines + grind [arrayIsRefinedBy, reg_of_isRefinedBy, Array.getElem_mem] /-- `Riscv.interpretOp'` is monotone in its operands. From 107ad9e529cf12edaa2e16bcd83ac09c67a3dcb8 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 12 Jul 2026 21:20:51 +0100 Subject: [PATCH 3/3] Clean up proofs --- Veir/Interpreter/Lemmas.lean | 62 +++++++++++++++++++++++++----------- 1 file changed, 44 insertions(+), 18 deletions(-) diff --git a/Veir/Interpreter/Lemmas.lean b/Veir/Interpreter/Lemmas.lean index 3cad68029..7e7268db4 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -541,14 +541,51 @@ theorem RuntimeValue.eq_of_arrayIsRefinedBy_of_regs {a b : Array RuntimeValue} (h : a ⊒ b) (hregs : ∀ v ∈ a, ∃ r, v = .reg r) : b = a := by grind [arrayIsRefinedBy, reg_of_isRefinedBy, Array.getElem_mem] +@[grind =] +theorem Interp.pure_def {α : Type} (a : α) : (pure a : Interp α) = some (.ok a) := rfl + +@[grind =] +theorem Interp.bind_def {α β : Type} (x : Interp α) (f : α → Interp β) : + (x >>= f) = match x with + | none => none + | some .ub => some .ub + | some (.ok a) => f a := rfl + +/-- +A RISC-V operation that interprets successfully produces register results and no control flow +action: a single register for the arithmetic and load opcodes, and no result at all for the stores. +Note that the memory is *not* preserved -- loads grow it via `ensureSize` and stores write to it. +-/ +theorem Riscv.interpretOp'_ok_results {vals : Array RuntimeValue} {mem' : MemoryState} + {act : Option ControlFlowAction} + (h : Riscv.interpretOp' opType properties resultTypes operands blockOperands mem + = some (.ok (vals, mem', act))) : + ((∃ r, vals = #[.reg r]) ∨ vals = #[]) ∧ act = none := by + cases opType <;> simp only [Riscv.interpretOp'] at h <;> grind + +/-- +A non-register operand is either fatal or irrelevant: every RISC-V opcode that reads its operands +pattern-matches them as registers and fails to interpret otherwise, and the opcodes that ignore +their operands (`li`, `lui`) interpret to the very same result whatever the operands are. +-/ +theorem Riscv.interpretOp'_eq_none_or_eq_of_not_regs {operands operands' : Array RuntimeValue} + (hregs : ¬ ∀ v ∈ operands, ∃ r, v = .reg r) : + Riscv.interpretOp' opType properties resultTypes operands blockOperands mem = none ∨ + Riscv.interpretOp' opType properties resultTypes operands blockOperands mem + = Riscv.interpretOp' opType properties resultTypes operands' blockOperands mem := by + cases opType <;> + simp only [Riscv.interpretOp'] <;> + first + | (right; trivial) + | (left; split <;> grind [Array.mem_def]) + /-- `Riscv.interpretOp'` is monotone in its operands. RISC-V operands are registers, which carry no poison, so refinement on them is equality: either every operand is a register -- and then the refined operands are the original ones and both sides -interpret to the very same result -- or some operand is not a register, and every opcode that -reads its operands fails to interpret (opcodes that ignore their operands, such as `li`, again -produce the very same result on both sides). +interpret to the very same result -- or some operand is not a register, and +`Riscv.interpretOp'_eq_none_or_eq_of_not_regs` applies. -/ theorem Riscv.interpretOp'_monotone {operands operands' : Array RuntimeValue} : operands ⊒ operands' → @@ -557,22 +594,11 @@ theorem Riscv.interpretOp'_monotone {operands operands' : Array RuntimeValue} : (Riscv.interpretOp' opType properties resultTypes operands' blockOperands mem) := by intro h by_cases hregs : ∀ v ∈ operands, ∃ r, v = .reg r - · have hb : operands' = operands := RuntimeValue.eq_of_arrayIsRefinedBy_of_regs h hregs - subst hb + · obtain rfl := RuntimeValue.eq_of_arrayIsRefinedBy_of_regs h hregs apply interpretResult_isRefinedBy_refl - · cases opType <;> - simp only [Riscv.interpretOp'] <;> - first - | apply interpretResult_isRefinedBy_refl - | (split - · exfalso - rename_i heq - refine hregs (fun v hv => ?_) - have hv' : v ∈ operands.toList := hv.val - rw [heq] at hv' - simp at hv' - grind - · simp [Interp.isRefinedBy]) + · rcases Riscv.interpretOp'_eq_none_or_eq_of_not_regs (operands' := operands') hregs with heq | heq + · rw [heq]; simp [Interp.isRefinedBy] + · rw [heq]; apply interpretResult_isRefinedBy_refl set_option warn.sorry false in theorem interpretOp'_monotone