Possibly incorrect lemma in example-archive (src/example-archive/simple-examples/working/list_2.c)

[kiranandcode]

Hi, I was just going through the snippets in the example archive looking, and I realised that it might be the case that one of the lemmas assumed in one is incorrect?

cn-tutorial/src/example-archive/simple-examples/working/list_2.c

Lines 12 to 18 in c9706ff

	/*@
	lemma IntListSeqSnoc(pointer p, pointer tail)
	requires take l1 = IntListSeg(p, tail);
	take v = Owned<struct list_node>(tail);
	ensures take l2 = IntListSeg(p, v.next);
	l2 == append(l1, Seq_Cons { val: v.val, next: Seq_Nil {} });
	@*/

In particular, shouldn't v.next be constrained to not be equal to any of the next-fields inside the list segment? (because if so, then it forms a loop and the segment would be cut off early?).

Discovered this while playing around and trying to prove this lemma in CN directly with the following encoding:

void lemma_make_segment_from_parts(struct list_node *head, struct list_node *tail) 
/*@
   requires take H = Owned<struct list_node>(head);
            take LS = IntListSeg(H.next, tail);
            !(head == tail);
    ensures take LS_NEW = IntListSeg(head, tail);
            LS_NEW == Seq_Cons { val: H.val, next: LS };
@*/ {
}

void lemma_intlist_seq_snoc(struct list_node *head, struct list_node *prev_curr)
/*@
  requires take l1 = IntListSeg(head, prev_curr);
           take v = Owned<struct list_node>(prev_curr);
           v.next != prev_curr;
  ensures take l2 = IntListSeg(head, v.next);
          l2 == append(l1, Seq_Cons { val: v.val, next: Seq_Nil {} });
  @*/
{
  /*@ split_case (ptr_eq(head,prev_curr)); @*/
  if(head == prev_curr) {
    /*@ assert (l1 == Seq_Nil {}); @*/
    /*@ unfold append(l1, Seq_Cons { val: v.val, next: Seq_Nil {} }); @*/
    /*@ split_case (ptr_eq(prev_curr, v.next)); @*/
    return;
  } else {
    struct list_node *prev_curr_next = prev_curr->next;
    lemma_intlist_seq_snoc(head->next, prev_curr);
    /*@ split_case (ptr_eq(head,prev_curr)); @*/
    lemma_make_segment_from_parts(head, prev_curr_next);
    /*@ assert (true); @*/
  }
}

[kiranandcode]

Oh, I'm realising that maybe it's in example-archive because it's been archived? tentatively closing this issue accordingly, and saw that a more correct encoding was already implemented in src/examples/queue/pop_unified.c

[dc-mak]

IntListSeq is exclusive in its second argument (does not take ownership of that pointer), and so the lemma as stated should be fine. Cycles would be ruled out by the fact that Owned(p) * Owned(q) => p != q.

[cp526]

(see previous discussion in mattermost)

[dc-mak]

Can you post a link or summarise the discussion for future readers?

[cp526]

(project-internal link)

https://mattermost.galois.com/verse-ta1-ta2/pl/489kc5988jgef88upaqqq3ydso

[dc-mak]

I think this is the correct form of the lemma?
https://github.com/rems-project/cn-tutorial/blob/main/src/examples/queue/push_induction.c