# Verifiable C: Getting the front element in a linked list based queue

**URL:** <https://discourse.rocq-prover.org/t/verifiable-c-getting-the-front-element-in-a-linked-list-based-queue/1340>\
**Category:** Using Rocq\
**Created:** [June 5, 2021, 3:58pm UTC](https://discourse.rocq-prover.org/t/verifiable-c-getting-the-front-element-in-a-linked-list-based-queue/1340 "2021-06-05T15:58:20Z")\
**Posts on this page:** 1\
**Page:** 1

<div class="post-metadata">

**Author:** ![DonaldKellett](https://sea1.discourse-cdn.com/flex001/user_avatar/discourse.rocq-prover.org/donaldkellett/32/753_2.png) [@DonaldKellett](https://discourse.rocq-prover.org/u/DonaldKellett)\
**Post date:** [June 5, 2021, 3:58pm UTC](https://discourse.rocq-prover.org/t/verifiable-c-getting-the-front-element-in-a-linked-list-based-queue/1340/1 "2021-06-05T15:58:20Z")

</div>

Consider an efficient linked list based implementation of a FIFO queue `linked_list_queue.c`, achieved by keeping pointers to the both the head and last nodes (labelled `front` and `back` respectively) of the linked list so enqueueing at the back of the list can be done in `O(1)` time:

```auto
#include <stddef.h>

extern void *malloc(size_t);
extern void free(void *);
extern void exit(int);

struct node {
  int value;
  struct node *next;
};

struct queue {
  struct node *front;
  struct node *back;
};

void queue_init(struct queue *q) { q->front = q->back = NULL; }

int queue_is_empty(struct queue *q) { return !q->front; }

int queue_front(struct queue *q) { return q->front->value; }

void queue_enqueue(struct queue *q, int value) {
  struct node *t;
  t = (struct node *)malloc(sizeof(struct node));
  if (!t)
    exit(1);
  t->value = value;
  t->next = NULL;
  if (!q->back)
    q->front = q->back = t;
  else
    q->back = q->back->next = t;
}

int queue_dequeue(struct queue *q) {
  int value;
  struct node *t;
  value = q->front->value;
  if (q->front == q->back) {
    free(q->front);
    q->front = q->back = NULL;
    return value;
  }
  t = q->front->next;
  free(q->front);
  q->front = t;
  return value;
}

int main(void) { return 0; }

```

Here, we are only interested in `int queue_front(struct queue *)` which simply returns the front item of a nonempty queue.

First, we define a list representation as follows (taken from chapter `Verif_stack` in Software Foundations Volume 5):

```coq
Fixpoint listrep (il: list Z) (p: val) : mpred :=
 match il with
 | i::il' => EX y: val,
        malloc_token Ews (Tstruct _node noattr) p *
        data_at Ews (Tstruct _node noattr) (Vint (Int.repr i),y) p *
        listrep il' y
 | nil => !! (p = nullval) && emp
 end.

Arguments listrep il p : simpl never.

```

Then we define our queue ADT as follows:

```coq
Definition queue (il: list Z) (p: val) :=
  match il with
  | [] => data_at Ews (Tstruct _queue noattr) (nullval, nullval) p
  | (_ :: _) => EX front back : val,
    data_at Ews (Tstruct _queue noattr) (front, back) p *
    (listrep il front && listrep [last il 0] back)
  end.

Arguments queue il p : simpl never.

```

Our specification for `queue_front()` is as follows:

```coq
Definition queue_front_spec : ident * funspec :=
  DECLARE _queue_front
  WITH q : val, i : Z, il : list Z
  PRE [tptr (Tstruct _queue noattr)]
    PROP () PARAMS (q) SEP (queue (i :: il) q)
  POST [tint]
    PROP () RETURN (Vint (Int.repr i)) SEP (queue (i :: il) q).

```

And our `Gprog`:

```coq
Definition Gprog : funspecs :=
  ltac:(with_library prog [
    queue_front_spec
  ]).

```

Now consider the proof of this specification:

```coq
Lemma body_queue_front : semax_body Vprog Gprog f_queue_front queue_front_spec.
Proof.
  start_function.
  unfold queue; unfold listrep; fold listrep.
  Intros front back y y0; subst y0.
  forward.
  - autorewrite with norm.
    assert_PROP (isptr front) by (rewrite (data_at_isptr _ _ _ front);
      entailer!).
    entailer!.
  - autorewrite with norm.
    Fail forward.
    admit.
Admitted.

```

Before the line `Fail forward`, we have the following proof context:

```auto
1 subgoal
Espec : OracleKind
q : val
i : Z
il : list Z
Delta_specs : PTree.t funspec
Delta := abbreviate : tycontext
POSTCONDITION := abbreviate : ret_assert
front, back, y : val
MORE_COMMANDS := abbreviate : statement
______________________________________ (1/1)
semax Delta
  (PROP ( )
   LOCAL (temp _t'1 front; temp _q q)
   SEP (data_at Ews (Tstruct _queue noattr) (front, back) q;
   malloc_token Ews (Tstruct _node noattr) front *
   data_at Ews (Tstruct _node noattr) (Vint (Int.repr i), y) front *
   listrep il y &&
   (malloc_token Ews (Tstruct _node noattr) back *
    data_at Ews (Tstruct _node noattr)
      (Vint (Int.repr (last (i :: il) 0)), nullval) back)))
  (_t'2 = (_t'1->_value);
   MORE_COMMANDS) POSTCONDITION

```

At the SEP clause, we have `temp _t'1 front` and `data_at ... front` where `struct node` has a `value` field so I expected to be able to go `forward` through the assignment `_t'2 = _t'1->_value`; however, on doing so, I get the following error message:

```auto
Tactic failure: 
It is not obvious how to move forward here. One way:
Find a SEP clause of the form [data_at _ _ _ 
?p
] (or field_at, data_at_, field_at_),
then use assert_PROP to prove an equality of the form
(offset_val 0 front = field_address ?t ?gfs ?p)
or if this does not hold, prove an equality of the form
(front = field_address ?t ?gfs ?p)
, then try [forward] again. (level 990).

```

Some things I tried:

- I tried `assert_PROP (isptr front)` (with success) but this did not help with going `forward`
- I did a `Search data_at` and could not seem to find lemmas relating `data_at` with `offset_val` and/or `field_address`
- `hint` only tells me to use `deadvars!` or try `forward`

I might be missing something obvious so any hint on how to proceed would be much appreciated (or if I entered a dead end due to incorrect tactics / funspec / etc.).

For reference, here is my minimal reproducible example, simplified to include only the parts relevant to `queue_front()`. I have not explicitly tested this so feel free to inform me of any compilation errors.

`_CoqProject`:

```auto
-R . Kata
Preloaded.v
Solution.v

```

`Preloaded.v`:

```coq
(* BEGIN AST *)

(* Elided - please replace with output of [clightgen -normalize linked_list_queue.c] *)

(* END AST *)

Require Import VST.floyd.proofauto VST.floyd.library Coq.Lists.List.
Import ListNotations.
Instance CompSpecs : compspecs. make_compspecs prog. Defined.
Definition Vprog : varspecs. mk_varspecs prog. Defined.

Fixpoint listrep (il: list Z) (p: val) : mpred :=
 match il with
 | i::il' => EX y: val,
        malloc_token Ews (Tstruct _node noattr) p *
        data_at Ews (Tstruct _node noattr) (Vint (Int.repr i),y) p *
        listrep il' y
 | nil => !! (p = nullval) && emp
 end.

Arguments listrep il p : simpl never.

Definition queue (il: list Z) (p: val) :=
  match il with
  | [] => data_at Ews (Tstruct _queue noattr) (nullval, nullval) p
  | (_ :: _) => EX front back : val,
    data_at Ews (Tstruct _queue noattr) (front, back) p *
    (listrep il front && listrep [last il 0] back)
  end.

Arguments queue il p : simpl never.

Definition queue_front_spec : ident * funspec :=
  DECLARE _queue_front
  WITH q : val, i : Z, il : list Z
  PRE [tptr (Tstruct _queue noattr)]
    PROP () PARAMS (q) SEP (queue (i :: il) q)
  POST [tint]
    PROP () RETURN (Vint (Int.repr i)) SEP (queue (i :: il) q).

Definition Gprog : funspecs :=
  ltac:(with_library prog [
    queue_front_spec
  ]).

```

`Solution.v`:

```coq
Require Import Preloaded VST.floyd.proofauto VST.floyd.library.

Lemma listrep_local_prop: forall il p, listrep il p |--
        !! (is_pointer_or_null p /\ (p=nullval <-> il=nil)).
Proof. (* spoilers to SF Volume 5 *) Admitted.
#[export] Hint Resolve listrep_local_prop : saturate_local.

Lemma listrep_valid_pointer:
  forall il p,
   listrep il p |-- valid_pointer p.
Proof. (* spoilers to SF Volume 5 *) Admitted.
#[export] Hint Resolve listrep_valid_pointer : valid_pointer.

Lemma queue_local_prop: forall il p, queue il p |-- !! (isptr p).
Proof.
  intros; unfold queue.
  destruct il.
  - entailer!.
  - Intros front back; entailer!.
Qed.
#[export] Hint Resolve queue_local_prop : saturate_local.

Lemma queue_valid_pointer:
  forall il p,
   queue il p |-- valid_pointer p.
Proof.
  intros; unfold queue.
  destruct il.
  - entailer!.
  - Intros front back; entailer!.
Qed.
#[export] Hint Resolve queue_valid_pointer : valid_pointer.

Lemma body_queue_front : semax_body Vprog Gprog f_queue_front queue_front_spec.
Proof.
  start_function.
  unfold queue; unfold listrep; fold listrep.
  Intros front back y y0; subst y0.
  forward.
  - autorewrite with norm.
    assert_PROP (isptr front) by (rewrite (data_at_isptr _ _ _ front);
      entailer!).
    entailer!.
  - autorewrite with norm.
    Fail forward.
    admit.
Admitted.

```

Using VST version 2.6 with CompCert 3.7