VSU_triangVSU verification of the Triang module

In this chapter we construct the VSU proving that triang2.c implements the specification from Spec_triang.

Imports

• We import the standard floyd.proofauto and floyd.VSU.
• This module calls upon functions from stack2.c, so it needs to import Spec_stack.
• The module implements the TriangASI, so it needs to import Spec_triang, which defines that.
• This module uses the MallocFreeAPD, but not (directly) the MallocFreeASI. That is, it uses the mem_mgr predicate but doesn't call any of the malloc or free functions. If we had defined the APD in a separate file from the ASI, we would need to import only one of those files. As it is, we import Spec_stdlib.
• And we must import the C program, triang2.

Parameters for the VSU

As usual, we make a Section to parameterize the VSU by the imported APDs.

Exercise: 3 stars, standard (Triang_private)

Write funspecs for the two private internal functions, and list them in Triang_private. Hint: copy and adapt from Verif_triang, bringing in supporting definitions (such as decreasing) as needed. Refer to Stack_private in VSU_stack for an example.

Exercise: 2 stars, standard (body_push_increasing)

Prove the semax_body lemma for push_increasing. You'll want to copy definitions and lemmas from your solution to Verif_triang.

Exercise: 2 stars, standard (body_pop_and_add)

Prove the semax_body lemma for pop_and_add. You'll want to copy definitions and lemmas from your solution to Verif_triang.

Exercise: 3 stars, standard (body_triang)

Prove the correctness of the triang function. When you get near the end, you may come upon the proof goal, stackrep STACK nil st |-- emp This goal arises because the current assertion is, ... SEP(mem_mgr M gv; stackrep STACK nil st) but the postcondition of triang contains just, ... SEP(mem_mgr M gv) . This is a symptom of the fact that the specifications and abstractions don't actually fit together! There are three possible ways to fix the problem:

• Adjust the postcondition of triang to ...SEP(mem_mgr M gv; TT), which means that triang is permitted to have a "space leak". That is, triang may allocate things that it does not free.
• Adjust the StackAPD with one more field in its Coq record: stackrep_nil: ∀ st, stackrep STACK [] st |-- emp. This specifies that, whatever is the low-level representation of a stack, the empty stack will always use no memory. Although that is true of our stack2.c implementation, one can easily imagine other implementations of stacks in which that is not true. Therefore, this design choice limits the generality of the interface.
• Adjust the Stack API with another function, freestack, perhaps with precondition SEP(mem_mgr M gv; stackrep STACK st) and postcondition SEP(mem_mgr M gv). Then call this at the end of the triang function.
  Any one of these choices is a legitimate software-engineering design decision, but the point is that some choice must be made, otherwise this collection of modules (stack, triang) can't be verified.
  As a work-around, you can finish the verification of body_triang by assuming this axiom:

with the right definition of body_push_increasing etc. this will work:

Next Chapter: VSU_stdlib