Add support for abstract/free types #594
Conversation
Represent abstract types as roughly equivalent to a struct with one
integer field. The integer describes a unique reference to an object of the
abstract type -- like a pointer. This field is implemented as a
different index type to regular record fields to ensure type safety.
In implementing this new index type, I have erred on the side of emulating
regular struct behaviour.
I chose struct-like this representation over the Abstr type in terms/types.ml
because it gives counterexamples, while Abstr did not when I tried it.
As an example, the test in tests/regression/falsifiable/abstract_type.lus
defines an abstract type `COUNTER`. It also defines imported (FFI) operations
for retrieving the count and incrementing the counter, which returns a
new counter with a one-higher count. For properties that fail, the
counterexamples for the abstract type look like arbitrary numbers, but
the important thing is that each number uniquely maps to an abstract
state describing the counter's internals.
For this test, I get the following counterexample. The initial counter is given a reference of 2, but the operation `get_counter` maps reference 2 to the actual count of 0. Then, incrementing counter referenced by 2 returns a new counter reference of 8. Asking this new counter for its count returns the actual incremented count of 1.
```
<Failure> Property (true -> (get_counter(c) = get_counter((pre c)))) is invalid by bounded model checking for k=1 after 0.186s.
Counterexample:
Node test ()
== Inputs ==
init.COUNTER 2 2
== Outputs ==
c.COUNTER 2 8
Function get_counter (test[l17c40])
== Inputs ==
in.COUNTER 4 2
== Outputs ==
out 7 0
Function increment (test[l16c14])
== Inputs ==
in.COUNTER 3 2
== Outputs ==
out.COUNTER 6 8
Function get_counter (test[l17c23])
== Inputs ==
in.COUNTER 2 8
== Outputs ==
out 0 1
```
|
Hi Amos, Could you please provide some context of why this feature is useful for you, and why you consider this feature might be useful for other Kind 2 users? Thank you for your interest in Kind 2. Daniel |
|
Hi Daniel, We don't need this feature right now, but we do expect to need it at some point in the future. Our use case is that we have some hardware-accelerated array functions, such as matrix multiplication and convolution. These arrays are stored on the GPU, so we can't use the ordinary Lustre array type. Instead, we plan to define the arrays as foreign types and axiomitise contracts for the operations on them. We haven't worked out all the details, such as how to deal with freeing old arrays. Perhaps, for our use case, this will require some linearity constraints on how foreign values are used so that we can mutate in-place. I believe that Heptagon supports something similar – but I hope that we will be able to implement this as a separate program analysis. That way we can use Kind2 to reason about the high-level abstract version without mutation, and then trust that if we implement it with mutation it will behave the same. That said, I mainly implemented this because I was surprised how easy it was, and I personally found it useful to get a better understanding of the codebase. I saw that the parser supported it, and figured it was planned but had just not been implemented yet. If you'd prefer to park it until we have a more pressing need then I won't be offended. I also have a tiny bugfix by the way: the json output of the interpreter sometimes produces malformed output with multiple commas in a row. But I made the mistake of asking for permission from The Hierarchy before opening the PR… Hopefully I'll be able to send it through soon. Thanks for all your work on Kind2. It's a great piece of software. |
|
Hi Amos, Sorry for not getting back to you sooner. We took a look at your proposal, and we liked it. Thank you very much for your contribution to the project. Daniel |
|
Great! Thanks Daniel. |
Hi,
This PR adds support for abstract or free types, written as types with no right-hand side equation. These abstract types can be given a semantics by defining operations on them as imported functions or nodes with no definitions, and giving these operations a contract.
I chose to represent abstract types as roughly equivalent to a struct with one
integer field. The integer describes a unique reference to an object of the
abstract type -- like a pointer. This field is implemented as a
different index type to regular record fields to ensure type safety.
In implementing this new index type, I have erred on the side of emulating
regular struct behaviour.
I chose this struct-like representation over the Abstr type in terms/types.ml
because it gives counterexamples, while Abstr did not when I tried it.
As an example, the test in tests/regression/falsifiable/abstract_type.lus
defines an abstract type
COUNTER. It also defines imported (FFI) operationsfor retrieving the count and incrementing the counter, which returns a
new counter with a one-higher count. For properties that fail, the
counterexamples for the abstract type look like arbitrary numbers, but
the important thing is that each number uniquely maps to an abstract
state describing the counter's internals.
For this test, I get the following counterexample. The initial counter is given a reference of 2, but the operation
get_countermaps reference 2 to the actual count of 0. Then, incrementing counter referenced by 2 returns a new counter reference of 8. Asking this new counter for its count returns the actual incremented count of 1.