Move shared-access predicate invariants to preconditions

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/conversion/ProgramConverter.kt

@@ -413,6 +413,7 @@ class ProgramConverter(
                     addAll(it.pureInvariants())
                     addAll(it.accessInvariants())
                     addAll(it.provenInvariants())
+                    addIfNotNull(it.sharedPredicateAccessInvariant())
                     if (it.isUnique) {
                         addIfNotNull(it.type.uniquePredicateAccessInvariant()?.fillHole(it))
                     }

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/callables/FullNamedFunctionSignature.kt

@@ -115,13 +115,12 @@ fun FullNamedFunctionSignature.toViperFunction(
             "Postcondition tries to acquire permissions, which is not allowed in a function"
         )
     }
-    val preconditions = formalArgs.mapNotNull { it.sharedPredicateAccessInvariant() } + getPreconditions()
     return UserFunction(
         name,
         formalArgs.map { it.toLocalVarDecl() },
         // TODO: Be explicit about the return types of functions instead of boxing them into a Ref
         Type.Ref,
-        preconditions.pureToViper(toBuiltin = true),
+        getPreconditions().pureToViper(toBuiltin = true),
         postconditions.pureToViper(toBuiltin = true),
         body,
         declarationSource.asPosition

formver.compiler-plugin/core/src/org/jetbrains/kotlin/formver/core/embeddings/expression/ControlFlow.kt

@@ -224,10 +224,12 @@ data class FunctionCall(val function: NamedFunctionSignature, val args: List<Exp
     override val subexpressions: List<ExpEmbedding>
         get() = args
 
-    override fun toViper(ctx: LinearizationContext): Exp = function.toFuncApp(
-        args.map { it.toViper(ctx) },
-        ctx.source.asPosition
-    )
+    override fun toViper(ctx: LinearizationContext): Exp {
+        return function.toFuncApp(
+            args.map { it.toViper(ctx) },
+            ctx.source.asPosition
+        )
+    }
 
     override fun <R> accept(v: ExpVisitor<R>): R =
         v.visitFunctionCall(this)
@@ -276,13 +278,6 @@ data class FunctionExp(
     override val type: TypeEmbedding = body.type
 
     override fun toViperMaybeStoringIn(result: VariableEmbedding?, ctx: LinearizationContext) {
-        signature?.formalArgs?.forEach { arg ->
-            // Ideally, we would want to assume these rather than inhale them to prevent inconsistencies with
-            // permissions. Unfortunately, Silicon for some reason does not allow Assumes.
-            listOfNotNull(arg.sharedPredicateAccessInvariant()).forEach { invariant ->
-                ctx.addStatement { Stmt.Inhale(invariant.toViperBuiltinType(ctx), ctx.source.asPosition) }
-            }
-        }
         body.toViperMaybeStoringIn(result, ctx)
         ctx.addLabel(returnLabel.toViper(ctx))
     }

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

@@ -244,6 +244,12 @@ public void testAllFilesPresentInPure_functions() {
         KtTestUtil.assertAllTestsPresentByMetadataWithExcluded(this.getClass(), new File("formver.compiler-plugin/testData/diagnostics/verification/pure_functions"), Pattern.compile("^(.+)\\.kt$"), null, true);
       }
 
+      @Test
+      @TestMetadata("heap_dependent_specifications.kt")
+      public void testHeap_dependent_specifications() {
+        runTest("formver.compiler-plugin/testData/diagnostics/verification/pure_functions/heap_dependent_specifications.kt");
+      }
+
       @Test
       @TestMetadata("pure_function_rely_on_branch.kt")
       public void testPure_function_rely_on_branch() {

formver.compiler-plugin/testData/diagnostics/conversion/classes/field_getters.fir.diag.txt

@@ -6,11 +6,11 @@ field bf$b: Ref
 method f$testPrimitiveFieldGetter$TF$T$PrimitiveFields$T$Unit(p$pf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$c$PrimitiveFields())
+  requires acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$a: Ref
   var l0$b: Ref
-  inhale acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   unfold acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   l0$a := p$pf.bf$a
   l0$b := havoc$T$Int()
@@ -30,6 +30,7 @@ field bf$g: Ref
 method f$testReferenceFieldGetter$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$c$ReferenceFields())
+  requires acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$f: Ref
@@ -38,7 +39,6 @@ method f$testReferenceFieldGetter$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   var l0$fb: Ref
   var l0$ga: Ref
   var l0$gb: Ref
-  inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   unfold acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   l0$f := p$rf.bf$f
   l0$g := havoc$T$PrimitiveFields()
@@ -64,6 +64,7 @@ field bf$g: Ref
 method f$testCascadingFieldGetter$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$c$ReferenceFields())
+  requires acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$fa: Ref
@@ -72,7 +73,6 @@ method f$testCascadingFieldGetter$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   var l0$ga: Ref
   var anon$1: Ref
   var l0$gb: Ref
-  inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   unfold acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   anon$0 := p$rf.bf$f
   unfold acc(p$c$PrimitiveFields$shared(anon$0), wildcard)

formver.compiler-plugin/testData/diagnostics/conversion/classes/field_getters_unique_shared.fir.diag.txt

@@ -10,14 +10,14 @@ field bf$uniqueVar: Ref
 method f$testPrimitiveFieldGetterUnique$TF$T$PrimitiveFields$T$Unit(p$pf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$c$PrimitiveFields())
+  requires acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   requires acc(p$c$PrimitiveFields$unique(p$pf), write)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$sharedVal: Ref
   var l0$sharedVar: Ref
   var l0$uniqueVal: Ref
   var l0$uniqueVar: Ref
-  inhale acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   unfold acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   l0$sharedVal := p$pf.bf$sharedVal
   l0$sharedVar := havoc$T$Int()
@@ -40,13 +40,13 @@ field bf$uniqueVar: Ref
 method f$testPrimitiveFieldGetterShared$TF$T$PrimitiveFields$T$Unit(p$pf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$c$PrimitiveFields())
+  requires acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$sharedVal: Ref
   var l0$sharedVar: Ref
   var l0$uniqueVal: Ref
   var l0$uniqueVar: Ref
-  inhale acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   unfold acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   l0$sharedVal := p$pf.bf$sharedVal
   l0$sharedVar := havoc$T$Int()
@@ -69,14 +69,14 @@ field bf$uniqueVar: Ref
 method f$testReferenceFieldGetterUnique$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$c$ReferenceFields())
+  requires acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   requires acc(p$c$ReferenceFields$unique(p$rf), write)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$sharedVal: Ref
   var l0$sharedVar: Ref
   var l0$uniqueVal: Ref
   var l0$uniqueVar: Ref
-  inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   unfold acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   l0$sharedVal := p$rf.bf$sharedVal
   l0$sharedVar := havoc$T$PrimitiveFields()
@@ -99,13 +99,13 @@ field bf$uniqueVar: Ref
 method f$testReferenceFieldGetterShared$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$c$ReferenceFields())
+  requires acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$sharedVal: Ref
   var l0$sharedVar: Ref
   var l0$uniqueVal: Ref
   var l0$uniqueVar: Ref
-  inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   unfold acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   l0$sharedVal := p$rf.bf$sharedVal
   l0$sharedVar := havoc$T$PrimitiveFields()

formver.compiler-plugin/testData/diagnostics/conversion/classes/field_setters_unique_shared.fir.diag.txt

@@ -6,10 +6,10 @@ field bf$unique: Ref
 method f$testPrimitiveFieldSetterUnique$TF$T$PrimitiveFields$T$Unit(p$pf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$c$PrimitiveFields())
+  requires acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   requires acc(p$c$PrimitiveFields$unique(p$pf), write)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  inhale acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   label lbl$ret$0
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
@@ -22,9 +22,9 @@ field bf$unique: Ref
 method f$testPrimitiveFieldSetterShared$TF$T$PrimitiveFields$T$Unit(p$pf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$pf), df$rt$c$PrimitiveFields())
+  requires acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  inhale acc(p$c$PrimitiveFields$shared(p$pf), wildcard)
   label lbl$ret$0
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
@@ -46,12 +46,12 @@ method con$c$PrimitiveFields$T$Int$T$Int$T$PrimitiveFields(p$shared: Ref, p$uniq
 method f$testReferenceFieldSetterUnique$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$c$ReferenceFields())
+  requires acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   requires acc(p$c$ReferenceFields$unique(p$rf), write)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
   var anon$1: Ref
-  inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   anon$0 := con$c$PrimitiveFields$T$Int$T$Int$T$PrimitiveFields(df$rt$intToRef(5),
     df$rt$intToRef(6))
   anon$1 := con$c$PrimitiveFields$T$Int$T$Int$T$PrimitiveFields(df$rt$intToRef(7),
@@ -77,11 +77,11 @@ method con$c$PrimitiveFields$T$Int$T$Int$T$PrimitiveFields(p$shared: Ref, p$uniq
 method f$testReferenceFieldSetterShared$TF$T$ReferenceFields$T$Unit(p$rf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$rf), df$rt$c$ReferenceFields())
+  requires acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
   var anon$1: Ref
-  inhale acc(p$c$ReferenceFields$shared(p$rf), wildcard)
   anon$0 := con$c$PrimitiveFields$T$Int$T$Int$T$PrimitiveFields(df$rt$intToRef(9),
     df$rt$intToRef(10))
   anon$1 := con$c$PrimitiveFields$T$Int$T$Int$T$PrimitiveFields(df$rt$intToRef(11),

formver.compiler-plugin/testData/diagnostics/conversion/classes/inheritance.fir.diag.txt

@@ -7,9 +7,9 @@ field bf$y: Ref
 
 method f$c$Foo$getY$TF$T$Foo$T$Int(this$dispatch: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(this$dispatch), df$rt$c$Foo())
+  requires acc(p$c$Foo$shared(this$dispatch), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
-  inhale acc(p$c$Foo$shared(this$dispatch), wildcard)
   unfold acc(p$c$Foo$shared(this$dispatch), wildcard)
   ret$0 := this$dispatch.bf$y
   goto lbl$ret$0
@@ -27,11 +27,11 @@ field bf$z: Ref
 
 method f$c$Bar$sum$TF$T$Bar$T$Int(this$dispatch: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(this$dispatch), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(this$dispatch), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
   var anon$0: Ref
   var anon$1: Ref
-  inhale acc(p$c$Bar$shared(this$dispatch), wildcard)
   unfold acc(p$c$Bar$shared(this$dispatch), wildcard)
   unfold acc(p$c$Foo$shared(this$dispatch), wildcard)
   anon$0 := this$dispatch.bf$x
@@ -53,14 +53,16 @@ field bf$z: Ref
 
 method f$c$Foo$getY$TF$T$Foo$T$Int(this$dispatch: Ref) returns (ret: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(this$dispatch), df$rt$c$Foo())
+  requires acc(p$c$Foo$shared(this$dispatch), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$intType())
 
 
 method f$callSuperMethod$TF$T$Bar$T$Int(p$bar: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(p$bar), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
-  inhale acc(p$c$Bar$shared(p$bar), wildcard)
+  unfold acc(p$c$Bar$shared(p$bar), wildcard)
   ret$0 := f$c$Foo$getY$TF$T$Foo$T$Int(p$bar)
   goto lbl$ret$0
   label lbl$ret$0
@@ -78,9 +80,9 @@ field bf$z: Ref
 method f$accessSuperField$TF$T$Bar$T$Boolean(p$bar: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(p$bar), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$boolType())
 {
-  inhale acc(p$c$Bar$shared(p$bar), wildcard)
   ret$0 := havoc$T$Boolean()
   goto lbl$ret$0
   label lbl$ret$0
@@ -97,9 +99,9 @@ field bf$z: Ref
 
 method f$accessNewField$TF$T$Bar$T$Int(p$bar: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(p$bar), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
-  inhale acc(p$c$Bar$shared(p$bar), wildcard)
   unfold acc(p$c$Bar$shared(p$bar), wildcard)
   ret$0 := p$bar.bf$z
   goto lbl$ret$0
@@ -117,14 +119,15 @@ field bf$z: Ref
 
 method f$c$Bar$sum$TF$T$Bar$T$Int(this$dispatch: Ref) returns (ret: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(this$dispatch), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(this$dispatch), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$intType())
 
 
 method f$callNewMethod$TF$T$Bar$T$Int(p$bar: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(p$bar), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
-  inhale acc(p$c$Bar$shared(p$bar), wildcard)
   ret$0 := f$c$Bar$sum$TF$T$Bar$T$Int(p$bar)
   goto lbl$ret$0
   label lbl$ret$0
@@ -141,9 +144,9 @@ field bf$z: Ref
 
 method f$setSuperField$TF$T$Bar$T$Unit(p$bar: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$bar), df$rt$c$Bar())
+  requires acc(p$c$Bar$shared(p$bar), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  inhale acc(p$c$Bar$shared(p$bar), wildcard)
   label lbl$ret$0
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 }
@@ -160,9 +163,9 @@ field bf$z: Ref
 method f$accessSuperSuperField$TF$T$Baz$T$Int(p$baz: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$baz), df$rt$c$Baz())
+  requires acc(p$c$Baz$shared(p$baz), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$intType())
 {
-  inhale acc(p$c$Baz$shared(p$baz), wildcard)
   unfold acc(p$c$Baz$shared(p$baz), wildcard)
   unfold acc(p$c$Bar$shared(p$baz), wildcard)
   unfold acc(p$c$Foo$shared(p$baz), wildcard)

formver.compiler-plugin/testData/diagnostics/conversion/classes/inheritance_fields.fir.diag.txt

@@ -3,6 +3,7 @@ field bf$fieldNotOverride: Ref
 
 method con$c$B$T$FieldB$T$B(p$fieldOverride: Ref) returns (ret: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$fieldOverride), df$rt$c$FieldB())
+  requires acc(p$c$FieldB$shared(p$fieldOverride), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret), df$rt$c$B())
   ensures acc(p$c$B$shared(ret), wildcard)
   ensures acc(p$c$B$unique(ret), write)

formver.compiler-plugin/testData/diagnostics/conversion/classes/interface.fir.diag.txt

@@ -1,6 +1,7 @@
 /interface.kt:(84,98): info: Generated Viper text for testProperties:
 method f$testProperties$TF$T$Foo$T$Unit(p$foo: Ref) returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$foo), df$rt$c$Foo())
+  requires acc(p$c$Foo$shared(p$foo), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var anon$0: Ref
@@ -9,7 +10,6 @@ method f$testProperties$TF$T$Foo$T$Unit(p$foo: Ref) returns (ret$0: Ref)
   var anon$2: Ref
   var anon$3: Ref
   var anon$4: Ref
-  inhale acc(p$c$Foo$shared(p$foo), wildcard)
   anon$0 := ps$public$varProp(p$foo, df$rt$intToRef(0))
   anon$2 := pg$public$varProp(p$foo)
   anon$1 := anon$2
@@ -58,3 +58,4 @@ method f$createImpl$TF$T$Unit() returns (ret$0: Ref)
 }
 
 method pg$public$number(this$dispatch: Ref) returns (ret: Ref)
+

formver.compiler-plugin/testData/diagnostics/conversion/classes/manual_permissions.fir.diag.txt

@@ -6,11 +6,11 @@ field bf$b: Ref
 method f$testManualPermissionFieldGetter$TF$T$ManualPermissionFields$T$Unit(p$mpf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$mpf), df$rt$c$ManualPermissionFields())
+  requires acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
   var l0$a: Ref
   var l0$b: Ref
-  inhale acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
   unfold acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
   l0$a := p$mpf.bf$a
   l0$b := p$mpf.bf$b
@@ -27,9 +27,9 @@ field bf$b: Ref
 method f$testManualPermissionFieldSetter$TF$T$ManualPermissionFields$T$Unit(p$mpf: Ref)
   returns (ret$0: Ref)
   requires df$rt$isSubtype(df$rt$typeOf(p$mpf), df$rt$c$ManualPermissionFields())
+  requires acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
   ensures df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())
 {
-  inhale acc(p$c$ManualPermissionFields$shared(p$mpf), wildcard)
   p$mpf.bf$b := df$rt$intToRef(123)
   label lbl$ret$0
   inhale df$rt$isSubtype(df$rt$typeOf(ret$0), df$rt$unitType())