From 3786fe914a6815369d3eabe0fb95a55229bd42fa Mon Sep 17 00:00:00 2001 From: Mathieu Fehr Date: Thu, 2 Jul 2026 19:13:52 +0200 Subject: [PATCH] feat(refinement): add `InterpreterState.isRefinedByAt` relation It differs to `isRefinedBy` by requiring values between states to refine each others only if they are dominated by the "refinement point". This new definition will superceed `isRefinedBy`, as it can handle things like looks that `isRefinedBy` cannot handle (as some "old" values stay in the state). --- Veir/Interpreter/Refinement/Basic.lean | 94 +++++++++++++++++++++++++- Veir/PatternRewriter/Semantics.lean | 3 +- 2 files changed, 95 insertions(+), 2 deletions(-) diff --git a/Veir/Interpreter/Refinement/Basic.lean b/Veir/Interpreter/Refinement/Basic.lean index de15cfcc4..933d1b3ad 100644 --- a/Veir/Interpreter/Refinement/Basic.lean +++ b/Veir/Interpreter/Refinement/Basic.lean @@ -1,5 +1,6 @@ import Veir.Interpreter.Basic import Veir.Data.Refinement +import Veir.Dominance /-! # Refinement of programs @@ -22,7 +23,7 @@ open Veir.Data namespace Veir -variable {OpInfo : Type} [HasOpInfo OpInfo] +variable {OpInfo : Type} [HasOpInfo OpInfo] {ctx : WfIRContext OpInfo} /-- Refinement relation between two runtime values. -/ def RuntimeValue.isRefinedBy (source target : RuntimeValue) : Prop := @@ -200,4 +201,95 @@ def InterpreterState.isRefinedBy {ctx ctx' : WfIRContext OpInfo} state.memory = state'.memory ∧ state.variables.isRefinedBy state'.variables mapping +/-! +## `InterpreterState.IsRefinedByAt` + +The `isRefinedByAt` family relates two interpreter states (a *source* `state` and a *target* +`state'`), asserting that `state'` refines `state`. Each value in scope defined in `state` is, +after renaming through the `mapping`, also defined in `state'` with a value that refines the +source value. Importantly, it does not constrain *every* defined value. It is parameterised by a +pair of `RefinementPoint`s `(s, s')` and only constrains values that are *in scope* at both +points. + +This scoping is what makes the relation usable in practice, as the variable state carries +stale values (blocks that are not dominating the current location such as prior iterations of a +loop). +-/ + +/-- +A *refinement point* provides a location for a refinement relation. + +It is either: +* `.at p`, an `InsertPoint` in a program, which is either a location just before an operation, or + at the end of a block; or +* `.blockEntry b`, a `BlockPtr` entry, just before the block's arguments. It represents the + location where the control flow has just entered the block, but before the block's arguments have + been set. +-/ +inductive RefinementPoint where + | at (p : InsertPoint) + | blockEntry (b : BlockPtr) + +instance : Coe InsertPoint RefinementPoint := ⟨.at⟩ + +def RefinementPoint.InBounds (point : RefinementPoint) (ctx : IRContext OpInfo) : Prop := + match point with + | .at p => p.InBounds ctx + | .blockEntry b => b.InBounds ctx + +@[simp, grind =] +theorem RefinementPoint.inBounds_at {p : InsertPoint} {ctx : IRContext OpInfo} : + (RefinementPoint.at p).InBounds ctx = p.InBounds ctx := rfl + +@[simp, grind =] +theorem RefinementPoint.inBounds_blockEntry {b : BlockPtr} {ctx : IRContext OpInfo} : + (RefinementPoint.blockEntry b).InBounds ctx = b.InBounds ctx := rfl + +/-- Whether `value` is *in scope* at a refinement point. For `.at p` this holds exactly when the +value dominates `p`; for `.blockEntry b` it must dominate the block entry and not be one of `b`'s +own arguments. -/ +def ValuePtr.InScopeAt (value : ValuePtr) (point : RefinementPoint) (ctx : WfIRContext OpInfo) : + Prop := + match point with + | .at p => value.dominatesIp p ctx + | .blockEntry b => + value.dominatesIp (InsertPoint.atStart! b ctx.raw) ctx ∧ value ∉ b.getArguments! ctx.raw + +@[simp, grind =] +theorem ValuePtr.inScopeAt_at : + ValuePtr.InScopeAt val (.at p) ctx = val.dominatesIp p ctx := rfl + +@[simp, grind =] +theorem ValuePtr.inScopeAt_blockEntry : + ValuePtr.InScopeAt val (.blockEntry b) ctx = + (val.dominatesIp (InsertPoint.atStart! b ctx.raw) ctx + ∧ val ∉ b.getArguments! ctx.raw) := rfl + +/-- +A refinement relation for variable states in two different contexts at different locations. +This asserts that every value in `state` and in scope, that is mapped to a value in `state'` and +in scope, have refining runtime values. +-/ +def VariableState.isRefinedByAt {ctx ctx' : WfIRContext OpInfo} + (state : VariableState ctx) (state' : VariableState ctx') + (mapping : ValueMapping ctx ctx') (s : RefinementPoint) (s' : RefinementPoint) + (_sIn : s.InBounds ctx.raw := by grind) (_s'In : s'.InBounds ctx'.raw := by grind) : Prop := + ∀ (val : ValuePtr) (valIn : val.InBounds ctx.raw), + val.InScopeAt s ctx → + (mapping ⟨val, valIn⟩).val.InScopeAt s' ctx' → + ∀ sv, state.getVar? val = some sv → + ∀ tv, state'.getVar? (mapping ⟨val, valIn⟩) = some tv → + sv ⊒ tv + +/-- +A refinement relation for intepreter states in two different locations. +This asserts that memory is equal, and that the variable states are refined at the given points. +-/ +def InterpreterState.isRefinedByAt {ctx ctx' : WfIRContext OpInfo} + (state : InterpreterState ctx) (state' : InterpreterState ctx') + (mapping : ValueMapping ctx ctx') (s : RefinementPoint) (s' : RefinementPoint) + (_sIn : s.InBounds ctx.raw := by grind) (_s'In : s'.InBounds ctx'.raw := by grind) : Prop := + state.memory = state'.memory ∧ + state.variables.isRefinedByAt state'.variables mapping s s' + end Veir diff --git a/Veir/PatternRewriter/Semantics.lean b/Veir/PatternRewriter/Semantics.lean index 85da60365..55a3bbfd9 100644 --- a/Veir/PatternRewriter/Semantics.lean +++ b/Veir/PatternRewriter/Semantics.lean @@ -147,7 +147,8 @@ def LocalRewritePattern.PreservesSemantics ∀ newState cf, interpretOp op state = some (newState, cf) → ∀ sourceValues, (op.getResults ctx.raw).mapM (newState.variables.getVar? ·) = some sourceValues → ∀ (state' : InterpreterState newCtx), state'.EquationLemmaAt (InsertPoint.before op) → - state.isRefinedBy state' (LocalRewritePattern.mapping hpattern) → + state'.DefinesDominating (InsertPoint.before op) → + state.isRefinedByAt state' (LocalRewritePattern.mapping hpattern) (.at (.before op)) (.at (.before op)) → ∃ newState', interpretOpList newOps.toList state' (by grind [ReturnOps]) = some (newState', cf) ∧ newState.memory = newState'.memory ∧