From 3fee2ec01f0779936019a1bfe6f8499958a7515b Mon Sep 17 00:00:00 2001
From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com>
Date: Mon, 21 Nov 2022 08:16:28 -0500
Subject: [PATCH] Added more DLS lemmas.

---
 .../proof/single_core_proofs/scp_list_predicates.h       | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

diff --git a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
index 11e2b6c1a..f91beb509 100644
--- a/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
+++ b/verification/verifast/proof/single_core_proofs/scp_list_predicates.h
@@ -230,9 +230,7 @@ predicate xLIST(
 	length(cells) == length(vals) &*&
 	uxNumberOfItems + 1 == length(cells) &*&
 	DLS(xListEnd, ?endprev, xListEnd, endprev, cells, vals, l);
-@*/
 
-#ifdef VERIFAST_TODO
 lemma void xLIST_distinct_cells(struct xLIST *l)
 requires xLIST(l, ?n, ?idx, ?end, ?cells, ?vals);
 ensures xLIST(l, n, idx, end, cells, vals) &*& distinct(cells) == true;
@@ -285,8 +283,6 @@ ensures DLS(n, m, n, m, cells, vals, l) &*& n != m;
 	close DLS(n, m, n, m, cells, vals, l);
 }
 
-#endif /* VERIFAST_TODO */
-/*@
 lemma void dls_last_mem(
 	struct xLIST_ITEM *n,
 	struct xLIST_ITEM *nprev,
@@ -342,8 +338,7 @@ ensures DLS(n, nprev, x, ?xprev, take(i, cells), take(i, vals), l) &*& DLS(x, xp
 		close DLS(n, nprev, x, xprev, take(i, cells), take(i, vals), l);
 	}
 }
-@*/
-#ifdef VERIFAST_TODO
+
 lemma void join(
 	struct xLIST_ITEM *n1,
 	struct xLIST_ITEM *nprev1,
@@ -380,7 +375,9 @@ ensures DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2)
 		close DLS(n1, nprev1, mnext2, m2, append(cells1, cells2), append(vals1, vals2), l);
 	}
 }
+@*/
 
+#ifdef VERIFAST_TODO
 lemma void idx_remains_in_list<t>(
 	list<t> cells,
 	t idx,