Meaning of several annotations

[Sophie Lathouwers]

Hi VeriFast team,

Firstly, thanks Bart for the answers to my previous questions! I have been looking into some more examples for Verifast and came across some more things that I didn't quite understand. I tried looking into the code and tutorial and managed to figure out most of the things, nonetheless I still have some questions about annotations that I don't quite understand yet. I'll provide these in a list below in the hopes of making it somewhat structured:

• 1. There is an array_slice_deep(array, start, end, predicate, info, elements, values). I think I understand the array_slice() predefined predicate, but I'm not sure how this one differs/what it means.

• 2. In the tutorial I learned about patterns and that you can give a name (e.g. ?theBalance) to the value of a variable which you can then for example reuse in the postcondition to state that the value did not change. But what happens if you use ?theBalance instead of theBalance in the postcondition or a loop invariant? Is the value of theBalance then simply redefined or does it also check that the value did not change? For example (from NewEidCard.java, selectByPath method):

for (...)

//@ invariant ... &*& [1/2]randomBuffer |-> ?theRandomBuffer &*& ...;

{
  ...
}
Would this loop invariant only check for the relevant permissions or would it also check (for iterations 2+) whether randomBuffer stays the same value namely theRandomBuffer?

Similarly, what would be the meaning of a pattern be in a postcondition? (e.g. "ensures objectDirectoryFile |-> ?theObjectDirectoryFile" in NewEidCard.java) Does this simply mean that we can refer to this value/object in following annotations?

• 3. What does "is_transient_byte_array(..)" mean? This seems to be a predefined fixpoint.

• 4. The class NewEidPoints (in examples/java/Java Card/NewEidCard/) has the following annotation "//@ javacard.framework.Applet applet;". Is this the definition of a ghost variable called applet?
  

• 5. What is the meaning of "system()"? I found it in the NewEidCard class ("install" method) but I wasn't able to find some kind of predefined fixpoint or predicate that it refers to.

• 6. Some expressions are annotated with "truncating", does this drop/remove any decimal places of that expression?

• 7. What does the expression "produce_call_below_perm_()" mean? I was only able to find it in the code, where it seems to produce the chunk call_below_perm__symb. But I wasn't quite able to figure out what that means...

• 8. What does the annotation "produce_lemma_function_pointer_chunk()" mean? For example "produce_lemma_function_pointer_chunk(my_ArrayBlockingQueue_take) : ArrayBlockingQueue_take(client_inv(queue), queue, my_unsep_pred(queue), P, Q)() { call(); };" in examples/java/prodcons/client.java

Kind regards,
Sophie

[Bart Jacobs]

Dear Sophie,

On 18/11/2020 14:58, Sophie Lathouwers wrote:

Hi VeriFast team,

Firstly, thanks Bart for the answers to my previous questions! I have been looking into some more examples for Verifast and came across some more things that I didn't quite understand. I tried looking into the code and tutorial and managed to figure out most of the things, nonetheless I still have some questions about annotations that I don't quite understand yet. I'll provide these in a list below in the hopes of making it somewhat structured:

• 1. There is an array_slice_deep(array, start, end, predicate, info, elements, values). I think I understand the array_slice() predefined predicate, but I'm not sure how this one differs/what it means.

This predicate's meaning is built into VeriFast but it could be defined as

predicate array_slice_deep<T, A, V>(T[] array, int start, int end, predicate(A, T; V) p, A info; list<T> elements, list<V> values) =
    start == end ?
        elements == nil &*& values == nil
    :
        array[start] |-> ?element &*& p(info, element, ?value) &*&
        array_slice_deep(array, start + 1, end, p, info, ?elements1, ?values1) &*&
        elements == cons(element, elements1) &*& values == cons(value, values1);

In other words, array_slice_deep(array, start, end, p, info, {e1, e2, e3}, {v1, v2, v3}) is equivalent to array[start..end] |-> {e1, e2, e3} &*& p(info, e1, v1) &*& p(info, e2, v2) &*& p(info, e3, v3). So, it asserts not just ownership of the array elements, but ownership of whatever the elements refer to, as well. This is useful for automation purposes: when symbolically executing an array element expression array[index] in the presence of a chunk array_slice_deep(array, start, end, p, info, es, vs) with start <= index and index < end, VeriFast consumes this chunk and produces array_slice_deep(array, start, index, p, info, take(index - start, es), take(index - start, vs)) &*& array_slice_deep(array, index + 1, end, p, info, drop(index - start + 1, es), drop(index - start + 1, vs)) &*& array[index] |-> nth(index - start, es) &*& p(info, nth(index - start, es), nth(index - start, vs)) and then unfolds the p chunk.

• 2. In the tutorial I learned about patterns and that you can give a name (e.g. ?theBalance) to the value of a variable which you can then for example reuse in the postcondition to state that the value did not change. But what happens if you use ?theBalance instead of theBalance in the postcondition or a loop invariant? Is the value of theBalance then simply redefined or does it also check that the value did not change?

If theBalance already exists in the scope, VeriFast reports an error.

• For example (from NewEidCard.java, selectByPath method):

for (...)

//@ invariant ... &*& [1/2]randomBuffer |-> ?theRandomBuffer &*& ...;

{
  ...
}
Would this loop invariant only check for the relevant permissions

Yes.

or would it also check (for iterations 2+) whether randomBuffer stays the same value namely theRandomBuffer?

No.

Similarly, what would be the meaning of a pattern be in a postcondition? (e.g. "ensures objectDirectoryFile |-> ?theObjectDirectoryFile" in NewEidCard.java) Does this simply mean that we can refer to this value/object in following annotations?

Yes. This is just so that we can refer to theObjectDirectoryFile in the remainder of the postcondition.

• 3. What does "is_transient_byte_array(..)" mean? This seems to be a predefined fixpoint.

This is Java Card-specific. It has to do with card tearing and object persistence.

• 4. The class NewEidPoints (in examples/java/Java Card/NewEidCard/) has the following annotation "//@ javacard.framework.Applet applet;". Is this the definition of a ghost variable called applet?
  

Yes; it defines a ghost field.

• 5. What is the meaning of "system()"? I found it in the NewEidCard class ("install" method) but I wasn't able to find some kind of predefined fixpoint or predicate that it refers to.

It is Java Card-specific; it is defined in bin/rt/javacard.framework.javaspec.

• 6. Some expressions are annotated with "truncating", does this drop/remove any decimal places of that expression?

No; it is used only with typecasts between integer types and with integer operators. It specifies that the expression may intentionally cause arithmetic overflow. VeriFast does not try to prove absence of arithmetic overflow; also, the result of symbolic evaluation of such an expression involves an application of a function symbol representing the truncation.

• 7. What does the expression "produce_call_below_perm_()" mean? I was only able to find it in the code, where it seems to produce the chunk call_below_perm__symb. But I wasn't quite able to figure out what that means...

This is for verifying termination. See examples/termination. When called in a function foo, this ghost command produces a call_below_perm_(foo) chunk, which conceptually gives you permission to call functions that occur before foo in the program text. ("below" refers to the order on functions where f1 < f2 if f1 occurs before f2 in the program text.)

To understand the termination verification approach, see our TOPLAS 2018 article.

• 8. What does the annotation "produce_lemma_function_pointer_chunk()" mean? For example "produce_lemma_function_pointer_chunk(my_ArrayBlockingQueue_take) : ArrayBlockingQueue_take(client_inv(queue), queue, my_unsep_pred(queue), P, Q)() { call(); };" in examples/java/prodcons/client.java

This produces a lemma function pointer chunk, which allows you to call a particular lemma function pointer (i.e. perform an indirect lemma call). This is explained in our "Solving the VerifyThis 2012 Challenges with VeriFast" paper. Section 4 in our NFM 2011 paper explains why these chunks are needed for soundness.

In this (and many other) examples, lemma function pointers are used for specifying concurrent operations; our POPL 2011 paper presents our approach to specifying concurrent operations.

Best regards,
Bart

Kind regards,
Sophie
--
You received this message because you are subscribed to the Google Groups "VeriFast" group.
To unsubscribe from this group and stop receiving emails from it, send an email to verifast+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/verifast/99f69b71-b888-42a3-847e-8ca2b209dba3n%40googlegroups.com.