Introduce Hylo style aliasing and Hylo input

[vkuncak]

Hylo is a programming language that leverages mutable value semantics and generic programming for high-level systems programming:

https://github.com/hylo-lang/hylo

https://www.hylo-lang.org/

Stainless is a program verifier for Scala:

https://github.com/epfl-lara/stainless/

The proposal is to

1. support annotations that mimic Hylo style liveness information and thus support uninitialized fields and consumed fields and applying a more general transformation of such trees to end up with Stainless trees that represent functional code, using a modified version of the transformation to imperative code:

https://infoscience.epfl.ch/entities/publication/412f5b59-2789-4fc2-b71f-142af945bbd3

2. enable the use of Stainless to verify Hylo code. This will involve parsing JSON representation of Hylo trees into new syntax trees of Stainless with the annotations.

This may require redesigning the entire alias analysis.