buffer.assume.noalias

← buffer dialect

Refine an existing buffer root with an explicit noalias contract. The result preserves the same storage identity, extent, memory-space, alignment, and nullability facts, and marks the root identity as comparable for disjointness proofs. External buffer arguments do not gain this proof by default. The promise separates distinct scoped roots in the same execution. Repeated executions may bind a root to different storage; noalias alone does not establish disjointness across executions.

Operation contract

Property	Value
Semantic phase	executable
Traits	Pure, FactIdentity

Signature

Kind	Name	Type	Cardinality	Description
Operand	buffers	buffer	variadic	Buffer roots to refine.
Result	results	buffer	variadic	Same buffer roots with noalias scopes.

Verification constraints

• VariadicValuesMatch(buffers, results)

Examples

%unique = buffer.assume.noalias %buffer : buffer

%lhs_unique, %rhs_unique = buffer.assume.noalias %lhs, %rhs : buffer, buffer