Improve purity checker and extend supported functions

[pawinkler]

Summary

The @Pure checker flags a wide range of functions as impure despite them having no observable side effects. This was discovered by systematically probing every common Kotlin infix, operator, and extension function in a dedicated test file. The results fall into two distinct problems:

1. Misclassification — functions that are unambiguously pure are rejected.
2. Missing support — entire categories of pure computation have no Viper translation.

Together these make @Pure too restrictive to use in realistic programs.

---

Problem 1: Misclassified as impure

These are unambiguously pure operations with no side effects, but the checker rejects them:

Function	Operator/syntax	Notes
Boolean.not	!a / .not()	Fundamental boolean negation
Int.unaryMinus	-a / .unaryMinus()	Arithmetic negation
Int.unaryPlus	+a / .unaryPlus()	Identity, trivially pure
Int.rem	a % b / .rem(b)	Remainder; same purity status as / which is accepted
Int.compareTo	.compareTo(b)	<, <=, >, >=, ==, != are accepted; compareTo is their desugaring
Boolean.and / or / xor	a and b, a or b, a xor b	&& and || are accepted; these non-short-circuit equivalents are not

Problem 2: Unsupported but required for practical use

Category	Affected operations
Bitwise Int	and, or, xor, shl, shr, ushr, inv
Bitwise Long	same set on Long
Control flow	if expressions, when expressions
Stdlib helpers	maxOf, minOf, abs, coerceAtLeast, coerceAtMost, coerceIn
Ranges	.., until, downTo, step
Pair construction	to

---

Observed inconsistency

The acceptance of && / || but rejection of and / or is particularly confusing. For pure arguments they are semantically equivalent. Similarly / is accepted but % is not, despite % being equally pure.

---

Impact

Without if expressions or unary minus, it is impossible to write even trivial pure helper functions such as absolute value or sign. The missing bitwise operators rule out any bit-manipulation logic. The missing maxOf/minOf rule out clamping and bounds checking. This severely limits the range of programs that can be verified with SnaKt.

---

Suggested improvements

• Recognise all unary operators (!, -, +) and % as pure — they are as pure as the binary arithmetic already accepted.
• Treat and/or/xor on Boolean consistently with &&/||.
• Add Viper translations for bitwise integer operations (Viper's integer type is unbounded, but bitwise ops can be axiomatised or the translation can target bitvector theories).
• Support if and when expressions inside @Pure function bodies.
• Add @Pure annotations (or equivalent built-in knowledge) for maxOf, minOf, kotlin.math.abs, and the coerce* extension functions.