Add verification tests for nullable type operations

7 new verification tests covering:
- Elvis operator with null input (proves default value is returned)
- Elvis operator with non-null input (proves passthrough)
- Nullable passthrough (proves identity preservation)
- Null literal return (proves result is null)
- Null comparison on null value (proves true)
- Non-null comparison on null value (proves false)
- Smart cast in if-else branch (proves type narrowing)

All tests pass Viper verification with z3.

Co-Authored-By: Claude Opus 4.6 <noreply@anthropic.com>

Author: jesyspa

formver.compiler-plugin/test-gen/org/jetbrains/kotlin/formver/plugin/runners/FirLightTreeFormVerPluginDiagnosticsTestGenerated.java

@@ -494,6 +494,12 @@ public void testNullability() {
       runTest("formver.compiler-plugin/testData/diagnostics/verification/nullability.kt");
     }
 
+    @Test
+    @TestMetadata("nullability_operations.kt")
+    public void testNullability_operations() {
+      runTest("formver.compiler-plugin/testData/diagnostics/verification/nullability_operations.kt");
+    }
+
     @Test
     @TestMetadata("stdlib_replacement_tests.kt")
     public void testStdlib_replacement_tests() {

formver.compiler-plugin/testData/diagnostics/verification/nullability_operations.fir.diag.txt

@@ -0,0 +1,89 @@
+/nullability_operations.kt:(124,142): info: Generated Viper text for elvisDefaultOnNull:
+method f$elvisDefaultOnNull$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+  ensures df$rt$intFromRef(ret$0) == 42
+{
+  var l0$x: Ref
+  l0$x := df$rt$nullValue()
+  if (l0$x != df$rt$nullValue()) {
+    ret$0 := l0$x
+  } else {
+    ret$0 := df$rt$intToRef(42)}
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability_operations.kt:(319,338): info: Generated Viper text for nullablePassthrough:
+method f$nullablePassthrough$TF$NT$Int(p$x: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
+  ensures ret$0 == p$x
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$nullable(df$rt$intType()))
+  ret$0 := p$x
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability_operations.kt:(472,489): info: Generated Viper text for returnNullLiteral:
+method f$returnNullLiteral$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$nullable(df$rt$intType()))
+  ensures ret$0 == df$rt$nullValue()
+{
+  ret$0 := df$rt$nullValue()
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability_operations.kt:(637,662): info: Generated Viper text for nullComparisonReturnsTrue:
+method f$nullComparisonReturnsTrue$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == true
+{
+  var l0$x: Ref
+  l0$x := df$rt$nullValue()
+  ret$0 := df$rt$boolToRef(l0$x == df$rt$nullValue())
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability_operations.kt:(848,877): info: Generated Viper text for nonNullComparisonReturnsFalse:
+method f$nonNullComparisonReturnsFalse$TF$() returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
+  ensures df$rt$boolFromRef(ret$0) == false
+{
+  var l0$x: Ref
+  l0$x := df$rt$nullValue()
+  ret$0 := sp$notBool(df$rt$boolToRef(l0$x == df$rt$nullValue()))
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability_operations.kt:(1063,1079): info: Generated Viper text for elvisWithNonNull:
+method f$elvisWithNonNull$TF$T$Int(p$x: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+  ensures df$rt$intFromRef(ret$0) == df$rt$intFromRef(p$x)
+{
+  var l0$y: Ref
+  inhale df$rt$isSubtype(df$rt$typeOf(p$x), df$rt$intType())
+  l0$y := p$x
+  if (l0$y != df$rt$nullValue()) {
+    ret$0 := l0$y
+  } else {
+    ret$0 := df$rt$intToRef(0)}
+  goto lbl$ret$0
+  label lbl$ret$0
+}
+
+/nullability_operations.kt:(1251,1268): info: Generated Viper text for smartcastInBranch:
+method f$smartcastInBranch$TF$NT$Int(p$n: Ref) returns (ret$0: Ref)
+  ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
+{
+  inhale df$rt$isSubtype(df$rt$typeOf(p$n), df$rt$nullable(df$rt$intType()))
+  if (!(p$n == df$rt$nullValue())) {
+    ret$0 := p$n
+    goto lbl$ret$0
+  }
+  ret$0 := df$rt$intToRef(0)
+  goto lbl$ret$0
+  label lbl$ret$0
+}

formver.compiler-plugin/testData/diagnostics/verification/nullability_operations.kt

@@ -0,0 +1,68 @@
+import org.jetbrains.kotlin.formver.plugin.*
+
+// Verify that elvis returns the default when input is null
+@AlwaysVerify
+fun <!VIPER_TEXT!>elvisDefaultOnNull<!>(): Int {
+    postconditions<Int> {
+        it == 42
+    }
+    val x: Int? = null
+    return x ?: 42
+}
+
+// Verify that nullable passthrough preserves identity
+@AlwaysVerify
+fun <!VIPER_TEXT!>nullablePassthrough<!>(x: Int?): Int? {
+    postconditions<Int?> {
+        it == x
+    }
+    return x
+}
+
+// Verify returning null literal
+@AlwaysVerify
+fun <!VIPER_TEXT!>returnNullLiteral<!>(): Int? {
+    postconditions<Int?> {
+        it == null
+    }
+    return null
+}
+
+// Verify null comparison on a known-null value
+@AlwaysVerify
+fun <!VIPER_TEXT!>nullComparisonReturnsTrue<!>(): Boolean {
+    postconditions<Boolean> {
+        it == true
+    }
+    val x: Int? = null
+    return x == null
+}
+
+// Verify non-null comparison on a known-null value
+@AlwaysVerify
+fun <!VIPER_TEXT!>nonNullComparisonReturnsFalse<!>(): Boolean {
+    postconditions<Boolean> {
+        it == false
+    }
+    val x: Int? = null
+    return x != null
+}
+
+// Verify elvis with non-null input passes through
+@AlwaysVerify
+fun <!VIPER_TEXT!>elvisWithNonNull<!>(x: Int): Int {
+    postconditions<Int> {
+        it == x
+    }
+    val y: Int? = x
+    return y ?: 0
+}
+
+// Verify smart cast after null check in if-else
+@AlwaysVerify
+fun <!VIPER_TEXT!>smartcastInBranch<!>(n: Int?): Int {
+    if (n != null) {
+        return n
+    }
+    return 0
+}