IR Verifier

Extensible verification system for validating PyPTO IR correctness through pluggable property verifiers with diagnostic reporting and Pass integration.

Overview

Component	Description
PropertyVerifier (C++)	Base class for verification rules
PropertyVerifierRegistry (C++)	Singleton mapping IRProperty → PropertyVerifier factories with verify/report API
Diagnostic	Structured error/warning report with severity, location, and message
VerificationError	Exception thrown when verification fails

Key Features

• Pluggable Rule System: Extend with custom verification rules
• Property-Based Verification: Opt-in property sets — verify exactly what you need
• Structural Properties: TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, and ManualDepsOnSubmitOnly are verified before/after each pass by VerificationInstrument; at pipeline start PassPipeline verifies only the lightweight subset shared with GetVerifiedProperties()
• Dual Verification Modes: Collect diagnostics or throw on first error
• Pass Integration: Use as a Pass in optimization pipelines
• Comprehensive Diagnostics: Collect all issues with source locations

Architecture

Structural vs Pipeline Properties

Category	Examples	Behavior
Structural	TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, ManualDepsOnSubmitOnly	Always true. Verified before/after each pass by VerificationInstrument; the subset shared with GetVerifiedProperties() is also checked at pipeline start. Never in PassProperties.
Pipeline	SSAForm, NoNestedCalls, HasMemRefs, ...	Produced/invalidated by passes. Verified per pass-declared contracts.

GetStructuralProperties() returns {TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, ManualDepsOnSubmitOnly}. These are verified before/after each pass by VerificationInstrument. At pipeline start, PassPipeline::Run() verifies only the lightweight subset shared with GetVerifiedProperties() (GetStructuralProperties().Intersection(GetVerifiedProperties())) — so e.g. ArrayNotEscaped is checked before/after each pass but not at pipeline start. Since no pass declares them in required/produced/invalidated, VerificationInstrument unions them with the pass's declared properties to ensure no pass breaks these fundamental invariants.

Verification Rule System

The verifier uses a plugin architecture where each PropertyVerifier subclass is an independent rule:

• Rules run in registration order across all functions
• Each rule operates independently — one rule's failure doesn't affect others
• Rules receive ProgramPtr and internally decide whether to iterate over functions or check program-level properties
• Rules can be selectively included via IRPropertySet

Diagnostic System

Field	Type	Purpose
severity	DiagnosticSeverity	Error or Warning
rule_name	string	Which rule detected the issue
error_code	int	Numeric error identifier
message	string	Human-readable description
span	Span	Source location information

Integration with Pass System

1. Automatic property verification: PassPipeline uses PropertyVerifierRegistry to check produced properties after each pass (controlled by VerificationLevel in PassContext). The lightweight subset of structural properties shared with GetVerifiedProperties() is checked at pipeline start. See Pass Manager.
2. VerificationInstrument: A PassInstrument that verifies properties via PassContext. Before each pass, it checks the pass's declared required properties. After each pass, it checks the pass's declared produced properties plus all structural properties — ensuring no pass breaks fundamental IR invariants.

The run_verifier() utility creates a standalone Pass for ad-hoc use in custom pipelines, but it is not part of the default optimization strategies.

Built-in Rules

Rule Name	IRProperty	Purpose
SSAVerify	SSAForm	No multiple assignment, no name shadowing, no missing yield, scope violations, cardinality checks
TypeCheck	TypeChecked	Type kind/dtype/shape/size consistency
NoNestedCall	NoNestedCalls	No nested call expressions in args, conditions, ranges
BreakContinueCheck	BreakContinueValid	Break/continue only in sequential/while loops
UseAfterDefCheck	UseAfterDef	Every Var use dominated by a definition (param, AssignStmt, loop var, iter_arg, return_var)
NormalizedStmtStructure	NormalizedStmtStructure	Nested SeqStmts flattened and single-child SeqStmts unwrapped
NoRedundantBlocks	NoRedundantBlocks	No single-child or nested SeqStmts
SplitIncoreOrch	SplitIncoreOrch	No InCoreScopeStmt nodes remain in Opaque functions
IncoreTileOps	IncoreTileOps	InCore functions use tile ops (no tensor-level ops remain)
HasMemRefs	HasMemRefs	All TileType variables have MemRef initialized
AllocatedMemoryAddr	AllocatedMemoryAddr	All MemRefs have valid addresses within buffer limits
OutParamNotShadowed	OutParamNotShadowed	Out/InOut params not reassigned with tensor-creating ops
NoNestedInCore	NoNestedInCore	No nested InCore scopes (InCoreScopeStmt inside InCoreScopeStmt)
InOutUseValid	InOutUseValid	Variables passed as InOut/Out to user-function calls are not read after the call (RFC #1026). Group-typed function bodies are skipped pending follow-up.
PipelineLoopValid	PipelineLoopValid	Bidirectional invariant on every ForStmt: kind_ == ForKind::Pipeline ⇔ pipeline_stages attr present. Either direction failing means the pipeline loop is malformed.
ArrayNotEscaped	ArrayNotEscaped	No ArrayType appears as a function parameter or return type (checked transitively through TupleType). ArrayType is on-core scalar-register-file / C-stack storage owned by the enclosing function — letting it cross a function boundary would leak a stack pointer, so it must be created and used locally inside the function body.
ManualDepsOnSubmitOnly	ManualDepsOnSubmitOnly	No plain cross-function Call (GlobalVar callee) carries attrs["manual_dep_edges"] — manual dependency edges live in the typed Submit::deps_ field. Op calls (system.task_dummy) keep the attr as their codegen fanin contract and are exempt.
OrchestrationReferencesResolved	OrchestrationReferencesResolved	Every non-builtin Call inside a FunctionType::Orchestration function targets a Function that exists in the surrounding Program. Replaces the codegen-side ValidateOrchestrationReferences walk that used to throw at codegen time.
AssignTypeSymmetry	AssignTypeSymmetry	Every AssignStmt(var, value) satisfies structural_equal(var.type, value.type). Covers dtype, shape, and tile_view/tensor_view; additionally TileType memory_space (TensorType has no memory_space) and DistributedTensorType window_buffer; tuple-typed assignments compare every element recursively. memref_ is excluded — structural_equal treats it as an allocation detail bound to the Var, governed by HasMemRefs / AllocatedMemoryAddr. Catches passes that mutate one side of an assignment without the other (e.g. #1262 TileType memory_space, #1278 tile_view). Registered in PropertyVerifierRegistry but not yet in GetStructuralProperties() — run on demand via PropertyVerifierRegistry::verify or by adding the property to a VerificationInstrument.
AivSplitValid	AivSplitValid	Structural checks on the first-class SplitAivScopeStmt region, keyed on the node itself (so nested / multi-mode functions are checked region by region). (a) No cube compute inside a data-parallel region — each AIV lane holds only half the tile, so a matmul cannot be vector-split. (b) No vector reduce (tile.row_* / tile.col_* / tile.sum / tile.max / tile.min) that collapses the split axis — it yields a partial per-lane result (a miscompile). (c) aiv_shard / aic_gather must appear inside a region (both the tile.* and author-facing tensor.* forms), and never inside a task-parallel mode=NONE region, which has no split axis to shard. (d) The boundary memory contract: tile.aiv_shard is Acc → Vec and tile.aic_gather is Vec → Mat. Both ops are the cross-core transfer, so the operand must live on the producing lane and the result on the consuming one; the memory sides are skipped until resolved, so the same check is safe across the whole window. Produced by OutlineIncoreScopes, then invalidated-and-re-produced by ConvertTensorToTileOps and InferTileMemorySpace, and finally invalidated by LowerAutoVectorSplit (which erases the region node). PassPipeline only verifies produced properties (passes.cpp), so those re-productions are what give check (d) a live verification point — at OutlineIncoreScopes the boundary is still the space-less tensor.* form and (d) is necessarily inert. Checked ops are plain Calls with a non-null op_; Submits are correctly skipped. Fix: (a) move the cube op outside the region; (b) reduce the non-split axis, or tile.aic_gather the lanes back first; (c) use UP_DOWN / LEFT_RIGHT for data-parallel halving; (d) shard only a cube-produced value — a vector-produced one (pl.load / pl.full) is already on the AIV lane, so drop the pl.aiv_shard and let the implicit affinity-gated split halve it.
HardSyncallOccupancy	HardSyncallOccupancyValid	A hard (FFTS) system.syncall waits for every physical core of its core_type to reach the barrier, so the enclosing SPMD launch must satisfy two independent guarantees: (1) full occupancy — fill all those cores exactly (N != required → error, covering both partial and over-occupancy); and (2) sync_start=True — all blocks co-resident at once, since a non-sync_start launch may dispatch blocks in waves and deadlock the barrier even at full occupancy. Either gap deadlocks on device (AICore timeout 507018) and leaves it needing a reset. Produced by ExpandMixedKernel (which resolves each launched kernel's FunctionType — the precondition the check needs) and listed in GetVerifiedProperties(), so PassPipeline auto-verifies it right after that pass. Covers every SPMD launch site whose block count it can classify — a FunctionType::Spmd function (scope pl.spmd), a FunctionType::Group function with a core_num attr (pl.cluster()-nested pl.spmd), and a Submit with core_num (pl.spmd_submit). A width is either a compile-time literal (checked against the SoC's physical counts) or a launch-shape query — pl.system.available_cluster_count() / pl.system.available_aiv_count(), directly or through the Var it binds. A query resolves on device to the run's own geometry, so it fills its core type by construction and needs no count comparison; it is also the portable spelling, since a literal matching this SoC is wrong on any run whose device reports a different usable count — too few blocks when more cores are available, too many when fewer are (which the runtime rejects outright). Using the query for the other core type (an AIV-only launch sized by the cluster count, or a mixed launch sized by the AIV count) is rejected. Per launch site and its direct callee: standalone AIV kernel + aiv_only → required = GetCoreCount(VECTOR); standalone AIC kernel + aic_only → required = GetCoreCount(CUBE); a standalone AIV/AIC kernel with a mismatched core_type (incl. the default mix) is rejected outright — the other core type has zero participants in a single-core launch, so the barrier can never complete; Group (mixed kernel) → required = GetCoreCount(CUBE) core-groups (one AIC per group, filling all cores) for any barrier core_type, checking the hard syncalls in its AIC/AIV sub-kernels (duplicated mix reported once). Skipped when the backend is unconfigured, core_num is neither a literal nor a launch-shape query, or no SPMD site launches the kernel (occupancy is a launch-time property). Fix: launch at full occupancy with a matching core_type and sync_start=True — preferably by sizing the launch with the matching launch-shape query — or use pl.system.syncall(mode="soft", ...) (GM-polling) for partial occupancy.

SSAVerify

Error types (ssa::ErrorType):

Error Code	Name	Description
1	MULTIPLE_ASSIGNMENT	Variable assigned more than once in the same scope
2	NAME_SHADOWING	Variable name shadows an outer scope variable
3	MISSING_YIELD	ForStmt or IfStmt missing required YieldStmt
4	ITER_ARGS_RETURN_VARS_MISMATCH	iter_args count != return_vars count in ForStmt/WhileStmt
5	YIELD_COUNT_MISMATCH	YieldStmt value count != iter_args/return_vars count
6	SCOPE_VIOLATION	Variable used outside its defining scope
7	MISPLACED_YIELD	YieldStmt appears before the trailing position in its scope

TypeCheck

Error types (typecheck::ErrorType):

Error Code	Name	Description
101	TYPE_KIND_MISMATCH	Type kind mismatch (e.g., ScalarType vs TensorType)
102	DTYPE_MISMATCH	Data type mismatch
103	SHAPE_DIMENSION_MISMATCH	Shape dimension count mismatch
104	SHAPE_VALUE_MISMATCH	Shape dimension value mismatch
105	SIZE_MISMATCH	Vector size mismatch in control flow
106	IF_CONDITION_MUST_BE_SCALAR	IfStmt/WhileStmt condition must be ScalarType
107	FOR_RANGE_MUST_BE_SCALAR	ForStmt range must be ScalarType
108	CONDITION_MUST_BE_BOOL	IfStmt/WhileStmt condition dtype must be BOOL
109	TENSOR_PADDING_MISMATCH	Tensor pad metadata mismatch
110	DISTRIBUTED_WINDOW_IDENTITY_MISMATCH	Distributed tensors refer to different window buffers
111	TILE_VIEW_MISMATCH	Effective TileView metadata mismatch

NoNestedCall

Name	Description
CALL_IN_CALL_ARGS	Call expression nested in another call's arguments
CALL_IN_IF_CONDITION	Call expression in if-statement condition
CALL_IN_FOR_RANGE	Call expression in for-loop range
CALL_IN_BINARY_EXPR	Call expression in binary expression
CALL_IN_UNARY_EXPR	Call expression in unary expression

UseAfterDefCheck

Error types (use_after_def::ErrorType):

Error Code	Name	Description
401	USE_BEFORE_DEF	Variable referenced before any definition in the current scope

Scoping rules:

• Function parameters are in scope for the entire function body
• AssignStmt: LHS variable enters scope after RHS is evaluated
• ForStmt: loop_var and iter_args are in scope inside the loop body only; return_vars enter the enclosing scope after the loop
• WhileStmt: iter_args are in scope for the condition and body; return_vars enter the enclosing scope after the loop
• IfStmt:
• SSA / phi-node form (return_vars_ present): definitions inside then/else branches do not propagate to the outer scope; only return_vars enter the enclosing scope after the if
• Non-SSA "leak" form (return_vars_ absent): branch-local definitions may be visible after the if; ConvertToSSA and SSAVerify are responsible for validating the resulting form

PropertyVerifierRegistry

Header: include/pypto/ir/verifier/property_verifier_registry.h

Singleton registry mapping IRProperty values to PropertyVerifier factories. Used by PassPipeline to automatically verify properties before/after passes.

Method	Description
GetInstance()	Get singleton instance
Register(prop, factory)	Register a verifier factory for a property
GetVerifier(prop)	Create a verifier instance (nullptr if none registered)
HasVerifier(prop)	Check if a verifier is registered
VerifyProperties(properties, program)	Verify a set of properties, return diagnostics
VerifyOrThrow(properties, program)	Verify and throw VerificationError on errors
GenerateReport(diagnostics)	Static — format diagnostics into readable report

C++ API Reference

PropertyVerifier Interface

Method	Signature	Description
GetName()	std::string GetName() const	Return unique rule identifier
Verify()	void Verify(const ProgramPtr&, std::vector<Diagnostic>&)	Check program and append diagnostics

Structural and Default Properties

Function	Returns	Description
GetStructuralProperties()	{TypeChecked, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, InOutUseValid, PipelineLoopValid, ArrayNotEscaped, ManualDepsOnSubmitOnly}	Invariants verified before/after each pass by VerificationInstrument (the subset shared with GetVerifiedProperties() is also checked at pipeline start)
GetDefaultVerifyProperties()	{SSAForm, TypeChecked, NoNestedCalls, BreakContinueValid, NoRedundantBlocks, UseAfterDef, OutParamNotShadowed, NoNestedInCore, TileTypeCoherence, ArrayNotEscaped}	Default set for run_verifier()
GetVerifiedProperties()	{SSAForm, TypeChecked, MixedKernelExpanded, AllocatedMemoryAddr, BreakContinueValid, NoRedundantBlocks, InOutUseValid, CallDirectionsResolved, ManualDepsOnSubmitOnly, ReturnParamsExplicit, AivSplitValid, HardSyncallOccupancyValid}	Lightweight set for PassPipeline auto-verify

RunVerifier Pass Factory

Pass RunVerifier(const IRPropertySet& properties);

Creates a Pass that verifies the given properties using PropertyVerifierRegistry.

Python API Reference

Module: pypto.pypto_core.passes

PropertyVerifierRegistry

Method	Parameter	Returns	Description
verify(properties, program)	IRPropertySet, Program	list[Diagnostic]	Collect diagnostics
verify_or_throw(properties, program)	IRPropertySet, Program	None	Throw on error
generate_report(diagnostics)	list[Diagnostic]	str	Format diagnostics

Helper Functions

Function	Returns	Description
get_default_verify_properties()	IRPropertySet	Default properties for run_verifier()
get_structural_properties()	IRPropertySet	Structural invariant properties

run_verifier Function

Parameter	Type	Default	Description
properties	IRPropertySet \| None	None	Properties to verify (None → default set)
Returns	Pass	-	Verifier Pass object

Usage Examples

Basic Verification

from pypto.pypto_core import passes

# Verify default properties
props = passes.get_default_verify_properties()
diagnostics = passes.PropertyVerifierRegistry.verify(props, program)

if diagnostics:
    report = passes.PropertyVerifierRegistry.generate_report(diagnostics)
    print(report)

Selective Verification

# Verify only specific properties
props = passes.IRPropertySet()
props.insert(passes.IRProperty.SSAForm)
props.insert(passes.IRProperty.TypeChecked)
diagnostics = passes.PropertyVerifierRegistry.verify(props, program)

Disabling Checks

# Start from default set and remove what you don't want
props = passes.get_default_verify_properties()
props.remove(passes.IRProperty.SSAForm)
diagnostics = passes.PropertyVerifierRegistry.verify(props, program)

Error Handling with Exceptions

props = passes.get_default_verify_properties()
try:
    passes.PropertyVerifierRegistry.verify_or_throw(props, program)
    print("Program is valid")
except Exception as e:
    print(f"Verification failed: {e}")

Using in a Custom Pipeline

# Create verifier pass (defaults to get_default_verify_properties())
verify_pass = passes.run_verifier()
result = verify_pass(program)

# Or with custom properties
props = passes.get_default_verify_properties()
props.remove(passes.IRProperty.SSAForm)
verify_pass = passes.run_verifier(properties=props)
result = verify_pass(program)

Adding Custom Rules

Implementation Steps

1. Inherit from PropertyVerifier, implement GetName() and Verify()
2. Create a factory function returning PropertyVerifierPtr
3. Register with PropertyVerifierRegistry in the constructor
4. Add Python binding and type stub (optional)

Guidelines

• Use IRVisitor to traverse IR nodes systematically
• Keep rules focused — one rule checks one category of issues
• Avoid side effects — only read IR and write diagnostics
• Create descriptive diagnostics with severity, rule name, error code, message, and span

Related Components

• Pass System (00-pass_manager.md): Verifier integrates as a Pass, PropertyVerifierRegistry used by PassPipeline
• IRBuilder (../ir/06-builder.md): Construct IR that verifier validates
• Type System (../ir/02-types.md): TypeCheck rule validates against type system
• Error Handling (../02-error-handling.md): Exception hierarchy, assertion macros (CHECK, INTERNAL_CHECK_SPAN), and Diagnostic / VerificationError definitions

Testing

Test coverage in tests/ut/ir/transforms/test_verifier.py: valid/invalid program verification, property-based selection, exception vs. diagnostic modes, pass integration, diagnostic field access, report generation, structural/default property sets.

UseAfterDef-specific coverage in tests/ut/ir/transforms/test_verify_use_after_def.py: valid programs (params, chained assigns, for loop body, return_var after loop), invalid programs (use-before-def, loop var out of scope, branch def not visible outside), error code/rule name verification, structural property membership.