From c9e406aad7b20bf96d929f013af4ac80a2291ea3 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 12 Jul 2026 12:41:00 +0100 Subject: [PATCH 1/4] 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 | 76 +++++++++++++++++++++++++++++++++++- 1 file changed, 74 insertions(+), 2 deletions(-) diff --git a/Veir/Interpreter/Lemmas.lean b/Veir/Interpreter/Lemmas.lean index ddaa39653..37b734823 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -2,6 +2,7 @@ module public import Veir.Verifier public import Veir.Interpreter.Refinement.Basic +public import Veir.Interpreter.Refinement.Lemmas import all Veir.Interpreter.Basic @@ -644,7 +645,72 @@ axiom interpretOp'_ne_fail {ctx : WfIRContext OpCode} {op : OperationPtr} (mem : MemoryState) : op.interpret ctx.raw operands mem ≠ .fail -axiom interpretOp'_monotone +/-- 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) (operands operands' : Array RuntimeValue) (blockOperands : Array BlockPtr) (mem : MemoryState) : operands ⊒ operands' → @@ -652,7 +718,13 @@ axiom interpretOp'_monotone (fun r₁ r₂ => r₁.1 ⊒ r₂.1 ∧ r₁.2.1 = r₂.2.1 ∧ ControlFlowAction.optionIsRefinedBy r₁.2.2 r₂.2.2) (interpretOp' opType properties resultTypes operands blockOperands mem) - (interpretOp' opType properties resultTypes operands' blockOperands mem) + (interpretOp' opType properties resultTypes operands' blockOperands mem) := by + intro h + cases opType + case riscv => + simp only [interpretOp'] + exact Riscv.interpretOp'_monotone h + all_goals sorry /-- A successful operation interpretation returns result values that conform to the declared From 06edc52642cf0e43215ac4f19349b18afcb7def7 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 12 Jul 2026 19:31:11 +0100 Subject: [PATCH 2/4] 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 37b734823..3f7be8886 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -667,14 +667,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 53f4f2ec2701290b18847ca10a026531c0d80e48 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sun, 12 Jul 2026 21:20:51 +0100 Subject: [PATCH 3/4] 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 3f7be8886..bf0877284 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -669,14 +669,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' → @@ -685,22 +722,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 From ff1411627b56b1a665f1c130ab94883dbb3ce296 Mon Sep 17 00:00:00 2001 From: Tobias Grosser Date: Sat, 22 Aug 2026 18:45:04 +0100 Subject: [PATCH 4/4] chore(interpret): port the riscv monotonicity proofs to the new `Interp` `Interp` became a three-constructor inductive instead of `Option (UBOr _)`, so success is `.ok` rather than `some (.ok _)` and failure is `.fail` rather than `none`. Adjust the case splits and statements accordingly, rename `interpretOp'_eq_none_or_eq_of_not_regs` to `..._eq_fail_or_eq_of_not_regs`, and drop `Interp.pure_def` in favour of the `Interp.pure_eq` main now provides. `Interp.bind_def` is kept: main's `bind_ok`/`bind_ub`/`bind_fail` only fire on literal constructors, and `grind` needs the full case split to see through a `do` block headed by an opaque call such as `riscvLoad`. --- Veir/Interpreter/Lemmas.lean | 26 ++++++++++++++------------ 1 file changed, 14 insertions(+), 12 deletions(-) diff --git a/Veir/Interpreter/Lemmas.lean b/Veir/Interpreter/Lemmas.lean index bf0877284..5a852dc09 100644 --- a/Veir/Interpreter/Lemmas.lean +++ b/Veir/Interpreter/Lemmas.lean @@ -657,7 +657,7 @@ abbrev InterpretResultIsRefinedBy : theorem interpretResult_isRefinedBy_refl (x : Interp (Array RuntimeValue × MemoryState × Option ControlFlowAction)) : Interp.isRefinedBy InterpretResultIsRefinedBy x x := by - rcases x with _ | (x | _) <;> grind [Interp.isRefinedBy] + cases x <;> grind [Interp.isRefinedBy] /-- A register runtime value can only be refined by itself, so operand arrays that consist purely of @@ -669,15 +669,17 @@ 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 - +/-- +`Interp`'s bind, as a case split on the scrutinee. Main's `Interp.bind_ok`/`bind_ub`/`bind_fail` +only fire on literal constructors; `grind` needs this to see through a `do` block whose head is an +opaque call such as `riscvLoad`. +-/ @[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 + | .fail => .fail + | .ub => .ub + | .ok a => f a := rfl /-- A RISC-V operation that interprets successfully produces register results and no control flow @@ -687,7 +689,7 @@ Note that the memory is *not* preserved -- loads grow it via `ensureSize` and st 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))) : + = .ok (vals, mem', act)) : ((∃ r, vals = #[.reg r]) ∨ vals = #[]) ∧ act = none := by cases opType <;> simp only [Riscv.interpretOp'] at h <;> grind @@ -696,9 +698,9 @@ A non-register operand is either fatal or irrelevant: every RISC-V opcode that r 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} +theorem Riscv.interpretOp'_eq_fail_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 = .fail ∨ Riscv.interpretOp' opType properties resultTypes operands blockOperands mem = Riscv.interpretOp' opType properties resultTypes operands' blockOperands mem := by cases opType <;> @@ -713,7 +715,7 @@ theorem Riscv.interpretOp'_eq_none_or_eq_of_not_regs {operands operands' : Array 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 -`Riscv.interpretOp'_eq_none_or_eq_of_not_regs` applies. +`Riscv.interpretOp'_eq_fail_or_eq_of_not_regs` applies. -/ theorem Riscv.interpretOp'_monotone {operands operands' : Array RuntimeValue} : operands ⊒ operands' → @@ -724,7 +726,7 @@ theorem Riscv.interpretOp'_monotone {operands operands' : Array RuntimeValue} : by_cases hregs : ∀ v ∈ operands, ∃ r, v = .reg r · obtain rfl := RuntimeValue.eq_of_arrayIsRefinedBy_of_regs h hregs apply interpretResult_isRefinedBy_refl - · rcases Riscv.interpretOp'_eq_none_or_eq_of_not_regs (operands' := operands') hregs with heq | heq + · rcases Riscv.interpretOp'_eq_fail_or_eq_of_not_regs (operands' := operands') hregs with heq | heq · rw [heq]; simp [Interp.isRefinedBy] · rw [heq]; apply interpretResult_isRefinedBy_refl