Remove dynamic invariants (#223)

This was used for `callsInPlace` verification but is no longer
necessary.

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/conversion/ProgramConverter.kt

@@ -257,7 +257,6 @@ class ProgramConverter(val session: FirSession, override val config: PluginConfi
                         addIfNotNull(it.type.uniquePredicateAccessInvariant()?.fillHole(it))
                     }
                 }
-                addAll(subSignature.params.flatMap { it.dynamicInvariants() })
                 addAll(returnVariable.pureInvariants())
                 addAll(returnVariable.provenInvariants())
                 addAll(returnVariable.allAccessInvariants())

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/TypeEmbedding.kt

@@ -71,15 +71,6 @@ interface TypeEmbedding {
      */
     fun pureInvariants(): List<TypeInvariantEmbedding> = emptyList()
 
-    /**
-     * Invariants that should correlate the old and new value of a value of this type
-     * over a function call. When a caller gives away permissions to the callee, these
-     * dynamic invariants give properties about the modifications of the argument as
-     * part of the functions post conditions.
-     * This is exclusively necessary for CallsInPlace.
-     */
-    fun dynamicInvariants(): List<TypeInvariantEmbedding> = emptyList()
-
     /**
      * Get a nullable version of this type embedding.
      *
@@ -158,6 +149,7 @@ data class NullableTypeEmbedding(val elementType: TypeEmbedding) : TypeEmbedding
     }
 
     override fun accessInvariants(): List<TypeInvariantEmbedding> = elementType.accessInvariants().map { IfNonNullInvariant(it) }
+    override fun pureInvariants(): List<TypeInvariantEmbedding> = elementType.pureInvariants().map { IfNonNullInvariant(it) }
 
     // Note: this function will replace accessInvariants when nested unfold will be implemented
     override fun sharedPredicateAccessInvariant(): TypeInvariantEmbedding? =

plugins/formal-verification/formver.core/src/org/jetbrains/kotlin/formver/embeddings/expression/VariableEmbedding.kt

@@ -51,8 +51,6 @@ sealed interface VariableEmbedding : PureExpEmbedding, PropertyAccessEmbedding {
 
     fun allAccessInvariants() = accessInvariants() + listOfNotNull(sharedPredicateAccessInvariant())
 
-    fun dynamicInvariants(): List<ExpEmbedding> = type.dynamicInvariants().fillHoles(this)
-
     override val debugTreeView: TreeView
         get() = NamedBranchingNode("Var", PlaintextLeaf(name.mangled))
 }