In this chapter we will prove that the C program, hash.c, correctly implements the functional model in hashfun.v. That proof, composed with the proof in hashfun.v that the functional model behaves correctly as a key-value map with string keys, demonstrates the correct behavior of hash.c.

The usual boilerplate

Now we import some VST libraries that don't come standard with VST.floyd.proofauto.

Now we import the functional model.

Function specifications

Imports from the C string library (see Verif_strlib)

String functions: copy, hash

Data structures for hash table

Some abbreviations for C struct types that we use frequently

A list_cell has four parts:

• a linked list cons cell with a key-pointer kp, integer count, and pointer to the next element of the linked list;
• the key-pointer points to a string (null-terminated array of char) containing the key;
• the cons cell was obtained by malloc, and must be freeable by free, and so there's a malloc_token giving that capability;
• the key-string also has a malloc-token so that it can be freed

Exercise: 1 star, standard (listcell_fold)

Exercise: 2 stars, standard (listrep_hints)

A listbox is a pointer to a pointer to a cons cell.

Exercise: 2 stars, standard (hashtable_rep_hints)

If you look at struct hashtable, you'll see that it has just one field, which is the array of bucket-pointers. Therefore, data_at Ews thashtable (map snd bl) should be synonymous with field_at Ews thashtable (DOT _buckets) (map snd bl) p. Here and elsewhere in the proof of lemmas in Verif_hash, we'll want to "unfold" the data_at into a field_at, which we can do as follows:

The argument of unfold_data_at is a pattern specifying which of the data_ats in the current proof goal to unfold. In this case, there's just one, so we can leave most of the pattern-arguments as underscores (wildcards).

Function specifications for hash table

Putting all the funspecs together

Proofs of the functions hash, copy_string, new_cell

Before attempting to prove body_hash, do Verif_strlib at least through body_strlen.

Exercise: 3 stars, standard (body_hash)

In the PROP part of your loop invariant, you'll want to maintain 0 ≤ i ≤ Zlength contents. In the LOCAL part of your loop invariant, try to use something like
    temp _c (Vbyte (Znth i (contents ++ [Byte.zero]))

instead of
    temp _c (Znth i (map Vbyte (...)))

The reason is that temp _c (Vint x) or temp _c (Vbyte y) is much easier for Floyd to handle than temp _c X where X is a general formula of type val. Late in the proof of the loop body, the lemma hashfun_snoc will be useful.

Exercise: 3 stars, standard (body_copy_string)

Exercise: 3 stars, standard (body_new_cell)

Proof of the new_table function

Auxiliary lemmas about data-structure predicates

Exercise: 2 stars, standard (iter_sepcon_hints)

Exercise: 2 stars, standard (iter_sepcon_split3)

Exercise: 3 stars, standard (body_new_table)

The loop invariant in this function describes a partially initialized array. The best way to do that is with something like,
  data_at Ews thashtable
      (list_repeat (Z.to_nat i) nullval ++
       list_repeat (Z.to_nat (N-i)) Vundef) p.

Then at some point you'll have to prove something about,
   data_at Ews thashtable
      (list_repeat (Z.to_nat (i + 1)) nullval ++
       list_repeat (Z.to_nat (N - (i + 1))) Vundef) p

In particular, you'll have to split up
   list_repeat (Z.to_nat (i + 1)) nullval

into
   list_repeat (Z.to_nat i) nullval ++ list_repeat (Z.to_nat 1) nullval.

The best way to do that is rewrite <- list_repeat_app'.

Proof of the get function

Exercise: 2 stars, standard (listrep_traverse)

Consider this loop in the get function:

  while (p) {
    if (strcmp(p->key, s)==0)
      return p->count;
    p=p->next;
  }

We will reason about linked-list traversal in separation logic using "Magic Wand as Frame" https://www.cs.princeton.edu/~appel/papers/wand-frame.pdf When the loop is partway down the linked list, we can view the original list up to the current position as a "linked-list data structure with a hole"; and the current position points to a linked-list data structure that fills the hole. The "data-structure-with-a-hole" we reason about with separating implication, called "magic wand": (hole −∗ data-structure) which says, if you can conjoin this data-structure-with-a-hole with something-to-fill-the-hole, then you get the original data structure:
     hole × (hole −∗ data-structure) |-- data-structure

Before the loop, we have a precondition such as,
   (listrep b₀ p₀; other_stuff)

After a few loop iterations, we have a situation like,
   (listrep b p; (listrep b p −∗ listrep b₀ p₀); other_stuff)

If the loop reaches p==NULL, then we have,
   (listrep nil nullval; (listrep nil nullval −∗ listrep b₀ p₀); other_stuff)

The listrep_traverse_× lemmas in this exercise illustrate how to start a traversal, how to perform one iteration of the traversal, and how to finish a traversal.

Hint: use sep_apply with the lemmas listcell_fold, listrep_traverse_step, wand_frame_ver, modus_ponens_wand.

Exercise: 3 stars, standard (body_get)

Use the listrep_traverse_× lemmas as appropriate.

This next command would not be part of an ordinary Verifiable C proof, it is here only to guide you through the bigger proof.

The previous line's autorewrite works only because of hypothesis H. If you clear H; autorewrite with norm you'll see that the Int.modu is not eliminated.

The purpose of this rewrite is to preserve a little bit of abstraction in the proofs. Because N_eq is in the rep_lia Hint database, the rep_lia tactic "knows" that N=109.

It is useful to put facts like this above the line, to support rep_lia in reasoning about conversions between Z and Int.

Put equations like this above the line, to support list_solve, rep_lia, and other tactics such as entailer! that call them.

Where did this proof goal come from? denote_tc_assert is a "type-checking assertion", that is, "prove that a C expression evaluates without crashing." In this case, the expression was table→buckets[b], and we have to prove here that b is in bounds of the array, and that the b'th element of the array is, in fact, initialized. The hypothesis H₁ that you proved above is generally useful, and particularly in this proof right here.

This next line would not be part of an ordinary Verifiable C proof, it is here only to guide you through the bigger proof.

We have reached the while-loop that will walk down the linked list. The pointer p₀ is the pointer to the beginning of a list that represents the sequence b₀. As the loop progresses, the loop variable p will move down the links, pointing to smaller sequences b. We represent the list segment from p₀ to p by a magic-wand formula: listrep b p −∗ listrep b₀ p₀. This means a heaplet (portion of memory) that, if you join it with a heaplet representing listrep b p, would represent the entire listrep b₀ p₀. Several of our SEP conjuncts will not be needed until after the loop is done. We can hide them away in a single SEP-conjunct FRZL FR₁ by doing this command:

The freeze tactic "frames out" several conjuncts for a while, until later we thaw FR₁.

As usual in a linked-list traversal, we want to dereference p→key but we don't have a data_at conjunct for p, we have only listrep b p. So we have to unfold the listrep; but this is useful only if we know that p≠nil. Therefore, case analysis:

This case, where b=nil, is impossible, because (if you have the right loop invariant) certain information in the SEP clause of the precondition is inconsistent with HRE: isptr p above the line. To make use of propositional information in the SEP clause, use assert_PROP:

The structure of the rest of this * bullet goes like this:

• Massage the precondition and get through the forward_call to function strcmp.
• Do forward_if (vret≠Int.zero). The argument you pass to forward_if can be a Prop, it does not need to be a full PROP/LOCAL/SEP, because:
  • One branch of the if never reaches the join point, it returns; and
  • The other branch of the if does not modify any local variables or memory, so the LOCAL and SEP parts of the assertion will be unchanged.
• • Sub-bullet: then-clause. At some point in this proof, you'll need to thaw FR₁. You'll need to use iter_sepcon_split3. Near the end of the then-clause, you'll have a goal similar (perhaps not identical) to listrep_traverse_step_example.
  • Sub-bullet: else-clause. Fairly short and straightforward proof.
  • Sub-bullet: after the if; another proof goal similar to listrep_traverse_step_example.

Here, you still have a data structure with a hole, represented by (A −∗ B), and the thing-in-the-hole, represented by A. This is similar to listrep_traverse_finish.

Proof of the incr_list function

Above, in the proof of the get function, we traverse a linked list without modifying it. The loop invariant looked like, listrep b p × (listrep b p −∗ listrep b₀ p₀). But the incr_list function modifies a linked list, perhaps inserting a new element at the end. Furthermore, the C program's loop variable struct cell **r is a pointer to a pointer to a list cell. Our separation-logic description of this is listboxrep.

That is, r is a single-word box containing pointer p, and p is a listrep. Let's examine the loop that we want to verify:

void incr_list (struct cell **r0, char *s) {
  struct cell *p, **r;
  for(r=r0; ; r=&p->next) {
    p = *r;
    if (!p) { *r = new_cell(s,1,NULL); return; }
    if (strcmp(p->key, s)==0) {p->count++; return;}
} }

We will describe variable r something like this:
  PROP() LOCAL(temp _r r) SEP(data_at Ews (tptr tcell) q r).

That is, pointer to a single word containing q. But when we do r = &(p→next) we will have r pointing into the middle of a struct cell record, at the next field. To describe that single field all alone, we use unfold_data_at to split
  data_at Ews tcell (x,y,q) p

into four separate conjuncts:
  field_at Ews tcell [StructField _key] x p ×
  field_at Ews tcell [StructField _count] y p ×
  spacer Ews (nested_field_offset tcell [StructField _count] + sizeof tuint)
                       (nested_field_offset tcell [StructField _next]) p ×
  field_at Ews tcell [StructField _next] q p

and then we must rewrite the last conjunct into
  data_at Ews (tptr tcell) q (field_address tcell [StructField _next] p)

where the (field_address _ _ _) is an "address arithmetic" expression that describes the offset, in bytes, from p to &(p→next). The "spacer" accounts for the padding between fields. This particular one, on a 32-bit-integer, 32-bit pointer configuration, simplifies down to emp. But on a 32-bit-integer, 64-bit pointer configuration, the spacer amounts to 4 bytes of Vundef-padding. The listboxrep_traverse lemma illustrates the situation at the end of the loop body. Look at the left-hand side of the |-- entailment. Variable r points to a single word containing p (it is perhaps the _next field of the previous list cell). Variable p points to a split-up list cell, with fields _key and _count. Where is the _next field of p? We choose not to describe it in this heaplet! The right-hand-side of this heaplet says, if you provide a heaplet satisfying listboxrep at address &p→next representing the sequence dl, then the combined heaplet satisfies listboxrep at address r representing the sequence (key,count)::dl. Furthermore, this is true for any sequence dl. That provides the freedom for the program to modify the contents of p→next, or of any _next field later in the sequence.

Exercise: 3 stars, standard (listboxrep_traverse)

Sometime during the proof below, you will have data_at Ews tcell ... p that you want to expand into
       field_at Ews tcell [StructField _key] ... p
     × field_at Ews tcell [StructField _count] ... p
     × field_at Ews tcell [StructField _next] ... p].

You can do this with unfold_data_at (pattern) where pattern is something like (data_at _ _ _ p) indicating which SEP conjunct you want to expand. After that, you will want to rewrite by field_at_data_at ...

In a 32-bit configuration, where the spacer is equivalent to emp, this specialized version of listboxrep_traverse is useful.

Exercise: 4 stars, standard (body_incr_list)

This proof uses "magic wand as frame" to traverse and update a (linked list) data structure. This pattern is a bit more complex than the wand-as-frame pattern used in body_get, which did not update the data structure. You will still use "data-structure-with-a-hole" and "what-is-in-the-hole"; but now the "data-structure-with-a-hole" must be able to accept the future hole-filler, not the one that is in the hole right now. The key lemmas to use are, wand_refl_cancel_right, wand_frame_elim', and wand_frame_ver. When using wand_frame_ver, you will find listboxrep_traverse or listboxrep_traverse32 to be useful.

field_compatible

Let's discuss how to address individual fields of structs, or individual slots of arrays. First, data_at sh (Tstruct _ _) is equivalent to the conjunction of individual field_at predicates for each of the fields. (Something similar holds for arrays.)

Second, field_at sh t gfs z p is equivalent to data_at sh (tptr t) z (field_address t gfs p), that is, field_address is a way to describe the offset (in bytes) from the base of a struct to the address of a field of that struct (or similarly to an element of an array).

The _next field of struct cell is the third field, after two integer fields. If there is no padding between those fields (which is the case here), then the distance from the base of the struct to the base of the _next field should be 2*sizeof(tint).

But the converse does not hold:

If we assume an extra premise, we can prove this, however:

Why is that? The answer is in the definition of field_address:

This says, if field_compatible t gfs p then the address of the field is (for example) offset_val (2 × sizeof tint) p, but if ¬ field_compatible t gfs p then the address is Vundef. That is, field_address t gfs p is defined only if the address p is compatible with t and gfs. What is field_compatible ? Let p be a address, and let t be a C-language type. We might ask, is it legal to put an object of type t at address p? Not always! We require all these conditions:

• isptr p: p must be a pointer value (Vptr), not an integer or undefined.
• complete_legal_cosu_type t = true: t must be complete, e.g., if typedef struct foo ×t then there must be a definition for struct foo.
• size_compatible t p: there must be at least sizeof t bytes before the maximum-possible address.
• align_compatible t p: p must be an appropriate multiple of 2, of 4, or of 8 as necessary, so that each subfield of type t is appropriately aligned as required by the data type of that subfield.
• legal_nested_field t gfs: If we ask, "is it legal to put an object of type t with field-path gfs at address p?" then we must also know that gfs is a possible field-path in type t. For example, StructField _count is a possible field-path for type tcell, but StructField _s is not-- there's no such field.
  We encapsulate all these properties of t, p, gfs in the predicate field_compatible:

_count is a field of struct cell

_s is not a field of struct cell

0 is a legal subscript of struct cell ×a[109]

108 is a legal subscript of struct cell ×a[109]

109 is not a legal subscript of struct cell ×a[109]

Sometimes in the C language we want a pointer just at the end of an array. That is, given struct cell ×a[109] we want the pointer value &a[109] . This is legal, even though this slot of the array does not exist. For this we want a variant of legal_nested_field that permits "just at the end":

108 is an an addressible subscript of struct cell ×a[109]

109 is an an addressible subscript of struct cell ×a[109]

110 is not an addressible subscript of struct cell ×a[109]

Based on these two notions,

• legal_nested_field (loadable/storable field) and
• legal_nested_field0 (addressible field),

we have, respectively field_compatible and field_compatible0.

Where does field_compatible come from?

Let's look again at this lemma:

We can apply this lemma if field_compatible... is above the line. How can we get that hypothesis above the line? Often the entailer or entailer! does this automatically, deriving it from data_at or field_at facts in the SEP clause of your left-hand side.

Proof of the incr function

  void incr_list (struct cell **r0, char *s);

  void incr (struct hashtable *table, char *s) {
    unsigned int h = hash(s);
    unsigned int b = h % N;
    incr_list (& table->buckets[b], s);
  }

The difficult part here is the function-argument, & table→buckets[b] . The precondition of the incr_list function requires just a single pointer-to-pointer-to-cell, but we have an entire array of 109 pointers-to-cell. We start with table, a pointer to a struct containing one field that's an array of 109 elements. For calling incr_list, we need to split that into two separate data structures:

• the single-element array at table→buckets+b
• all the rest of the data structure, including the other fields of struct hashtable (if there were any) and the elements 0..b-1 and b+1..108 of the array.

The wand_slice_array lemma can do this:

Here (array_with_hole sh t lo hi n al p) means

This says that data_at sh (tarray t n) al p can be split up into two pieces:

• 1. the slice from index lo to index hi-1,
• 2. everything else.

Later in the proof of body_incr, you need to handle the function-argument, & (table→buckets[b]) , where variable _b has the value h. CompCert will calculate this as table + (sizeof int)*h, which is to say,
    offset_val (sizeof (tptr tcell) × h) table

But we want to express that as [ field_address0 (tarray (tptr tcell) N) [ArraySubsc h] (field_address thashtable [StructField _buckets] table). ] As discussed above in the field_compatible section, to prove a field_address one must know that the address table is field-compatible with thashtable, and that the address table→buckets is field-compatible with the ArraySubsc h field. That's all proved in the following lemma:

The Hint database allows auto with field_compatible to make use of the field_compatible facts above the line.

Exercise: 4 stars, standard (body_incr)

The next two lines would not be part of an ordinary Verifiable C proof; they are here only to guide you through the bigger proof.

For the remainder of the proof, here are some useful lemmas: sublist_len_1, sublist_same, sublist_map, data_at_singleton_array_eq, iter_sepcon_split3, iter_sepcon_app, sublist_split, field_at_data_at, wand_slice_array_tptr_tcell