Support Kotlin object declarations as Viper Algebraic Data Types

[pawinkler]

Goal

Allow Kotlin object declarations annotated with @ADT to be encoded as Viper ADTs instead of heap-based objects, enabling them to be treated as pure value types in verification.

Motivating example

@ADT object Red
@ADT object Green
@ADT object Blue

@AlwaysVerify
fun colorIsNotGreen(@ADT c: Red) {
    verify(c != Green)
}

The objects Red, Green, Blue are distinct constant values with no heap representation. Verification should be able to reason about their equality and inequality directly.

What needs to be supported

• @ADT annotation on object declarations
• @ADT on parameters and local variables to indicate they hold an ADT-typed value (required because Viper needs the type to be declared as ADT rather than Ref and increases user awareness about deviating semantics)
• Encoding as a Viper ADT with a single nullary constructor per object
• Equality/inequality reasoning between values of the same ADT type
• Cross-type inequality: values of different ADT types are always unequal

Restrictions to enforce

• Only object declarations (not class, open class, interface)
• No fields, no member functions, no supertypes, no subclassing

Known challenges

• Upstream Silicon bug: DomainInstances.down1Types in Viper Silver lacks a case for AdtType, causing a MatchError whenever a method has an ADT-typed formal argument; a fix and rebuild of the local Silicon jar avoids crashing, but verification still does not succeed, reasoining is unclear.