Can static variables play the role of ghost variables (as in SPARK‑Ada)?

[Yannick Duchêne]

A question came to my mind when I wanted to write some assertions, I failed to (not in ATS, but I project the question to ATS).

Say I have something named A, from which I derive things named B, C, etc (there are a few). I have functions, which, from B, C, etc, retrieves things which belongs to A, and I want to assert this latter property. These functions don't need an A as an argument, which made me think this would require what SPARK names “ghost variable”: needed for a proof, but not needed for the execution, which make it close to ATS's static variables.

While close to ATS's static variables as I understand it, it's directly related to dynamic variables, as it is as if a dynamic value was there during a proof, but is not there during the execution.

Is this one of the purpose of static variables too? Is this feasible with static variables?

To go further, if this A is to be freed early, can I keep a “virtual” copy of it (in a static variable) for proofs?

I feel the answer is rather No, while I'm not sure, thus the question.

If the answer is really No, may be an option with this kind of cases, is to show B, C, etc, are other forms or representations of A (before freeing A), may be via proving the existence of a reciprocal function, but that's not the same question.

P.S. For the short story, if I failed to write these assertions, that's because it would require to keep alive some data which are is not strictly needed anymore, and I decided to avoid this waste and encumbrance of extraneous arguments, thinking I will be back to this when re-writing into ATS, with the hope it will be better suited to this.

[Yannick Duchêne]

Same question with the components of a type or of a value: when a tuple has a component which is only needed for proofs and not needed for computation (I actually have tuples like this, which a component only used in assertions).

[gmhwxi]

Yes, static variables can play the role of ghost variables in Spark Ada.
You should be able to gradually figure out how this actually works. If you have
a concrete case, I will be happy to discuss it with you.

>>To go further, if this A is to be freed early, can I keep a “virtual” copy of it (in a static variable) for proofs?

Yes, you can. Again, if you have a concrete case, I will be happy to discuss it with you.

[Yannick Duchêne]

Le dimanche 12 avril 2015 03:00:31 UTC+2, gmhwxi a écrit :

Yes, static variables can play the role of ghost variables in Spark Ada.
You should be able to gradually figure out how this actually works. If you have
a concrete case, I will be happy to discuss it with you.

That's already enough to let me know I'm not on a track which would make me miss the ATS target.

As there was an invitation to this, here is a example, a simplification of the real case: A would be a list of integral numbers, a function would group them into successive items and collapse these groups into ranges, defined with lower and upper inclusive bounds, which would produce the B previously mentioned,  a list of tuples of the form (first, last). A would disappear, and only B would be kept. By some mean, some function would return index into B with an offset. Given such an index and an offset, a item of A can be retrieved, but A does not exist anymore.

I tried to simply the case as much as possible, this is not the real case, just close enough to it.

Among the idea of the ghost variable to prove items from B are also items of A (and can also be iterated in the same order), I though about a reciprocal function, to reconstruct an A from B, and prove that function is correct.

[gmhwxi]

Here is my understanding of the situation:

You have two functions foo1 and foo2. And you want to prove that

foo1(A, ...) = foo2(B, ...)

foo1 in this case is list_get_at.

In general, proving that two functions are equivalent can be quite involved.
You may want to study the examples in ATSLIB/gflist:

https://github.com/githwxi/ATS-Postiats/blob/master/libats/SATS/gflist.sats
https://github.com/githwxi/ATS-Postiats/blob/master/libats/DATS/gflist.dats

I think it is necessary to adopt a "programmer-centric" style for this kind of
task. That is, feel free to introduce lemmas as you see fit, but do not spend
time on proving them. At least, not at the beginning.