From 9e3ea9016e01f46e2b04440378833f31339b8e06 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 23 Nov 2022 08:31:07 -0500 Subject: [PATCH] Added lemma `DLS_end_next_close` to help closing DLS opened with `DLS_end_next_open` --- .../scp_list_predicates_extended.h | 63 +++++++++++++++---- .../verifast/proof/verifast_lists_extended.h | 26 ++++++++ 2 files changed, 78 insertions(+), 11 deletions(-) diff --git a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h index 6c8b3c488..c09234dfb 100644 --- a/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h +++ b/verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h @@ -14,7 +14,7 @@ requires &*& pxItem == gEnd; ensures - xLIST_ITEM(gEnd, ?gItemVal, ?gItem_next, gEndPrev, pxList) &*& + xLIST_ITEM(gEnd, head(gVals), ?gItem_next, gEndPrev, pxList) &*& DLS(gItem_next, gEnd, gEnd, gEndPrev, drop(1, gCells), drop(1, gVals), pxList ) &*& mem(gItem_next, gCells) == true; { @@ -43,6 +43,28 @@ ensures } +lemma void DLS_end_next_close(struct xLIST* pxList, struct xLIST_ITEM* pxItem) +requires + xLIST_ITEM(?gEnd, ?gItemVal, ?gItem_next, ?gEndPrev, pxList) &*& + DLS(gItem_next, gEnd, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*& +// mem(gItem_next, gCells) == true &*& + length(gCells) == length(gVals) &*& + length(gCells) > 0 &*& + pxItem == gEnd; +ensures + DLS(gEnd, gEndPrev, gEnd, gEndPrev, + cons(gEnd, gCells), cons(gItemVal, gVals), pxList); +{ + open DLS(gItem_next, gEnd, gEnd, gEndPrev, gCells, gVals, pxList); + close DLS(gItem_next, gEnd, gEnd, gEndPrev, gCells, gVals, pxList); + dls_star_item(gItem_next, gEndPrev, gEnd); + dls_distinct(gItem_next, gEnd, gEnd, gEndPrev, gCells); + dls_last_mem(gItem_next, gEnd, gEnd, gEndPrev, gCells); + close DLS(gEnd, gEndPrev, gEnd, gEndPrev, + cons(gEnd, gCells), cons(gItemVal, gVals), pxList); +} + + lemma void DLS_nonEndItem_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem) requires DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, pxList) &*& @@ -59,7 +81,8 @@ ensures // DLS prefix pxList) &*& // item of interest - xLIST_ITEM(pxItem, ?gItemVal, ?pxItem_next, pxItem_prev, pxList) + xLIST_ITEM(pxItem, nth(index_of(pxItem, gCells), gVals), + ?pxItem_next, pxItem_prev, pxList) &*& // DLS suffix (pxItem != gEndPrev @@ -91,6 +114,9 @@ ensures // DLS prefix drop(pxItemIndex_0, gCells), drop(pxItemIndex_0, gVals), pxList); assert( xLIST_ITEM(pxItem, ?gItemVal, ?pxItem_next, pxItem_prev, pxList) ); + assert( gItemVal == head(drop(pxItemIndex_0, gVals)) ); + head_drop_n_equals_nths(gVals, pxItemIndex_0); + assert( gItemVal == nth(index_of(pxItem, gCells), gVals) ); // open DLS and xLIST_ITEM predicates to prove @@ -143,25 +169,24 @@ ensures // DLS prefix */ void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem) /*@ requires - DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?pxList) &*& + DLS(?gEnd, ?gEndPrev, gEnd, gEndPrev, ?gCells, ?gVals, ?gList) &*& mem(pxTaskItem, gCells) == true &*& gEnd == head(gCells) &*& length(gCells) == length(gVals) &*& length(gCells) > 1; @*/ /*@ ensures - DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, pxList) &*& + DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) &*& mem(pxTaskItem, gCells) == true; @*/ { - //@ int pxItemIndex_0 = index_of(pxTaskItem, gCells); - //@ struct xLIST_ITEM* pxItem = pxTaskItem; + //@ struct xLIST_ITEM* gTaskItem_0 = pxTaskItem; /*@ - if( pxItem == gEnd ) { - DLS_end_next_open(pxList, pxItem); + if( gTaskItem_0 == gEnd ) { + DLS_end_next_open(gList, gTaskItem_0); } else { - DLS_nonEndItem_next_open(pxList, pxItem); + DLS_nonEndItem_next_open(gList, gTaskItem_0); } @*/ pxTaskItem = pxTaskItem->pxNext; @@ -170,10 +195,26 @@ void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem) //@ assert( mem(pxItem_1, gCells) == true ); + //@ close xLIST_ITEM(gTaskItem_0, ?gTaskItemVal, _, _, gList); + /*@ + if( gTaskItem_0 == gEnd ) { + DLS_end_next_close(gList, gTaskItem_0); + assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, ?gCells2, ?gVals2, gList) ); + // why is this necessary? + assert( gCells == cons( _, _) ); + assert( gVals == cons(_, _) ); - // ignore post condition until closing lemmas are finished - //@ assume(false); + // gVals2 == cons (|(intbox) | (|(int) | (head gVals) + assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, _, gList) ); + assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gList) ); + } else { + assume(false); + //DLS_nonEndItem_next_close(gList, gTaskItem_0); + } + @*/ + +;; } diff --git a/verification/verifast/proof/verifast_lists_extended.h b/verification/verifast/proof/verifast_lists_extended.h index 08f1f1c46..4d019ab54 100644 --- a/verification/verifast/proof/verifast_lists_extended.h +++ b/verification/verifast/proof/verifast_lists_extended.h @@ -12,4 +12,30 @@ requires mem(x, drop(i, xs)) == true; ensures mem(x, xs) == true; @*/ + +// TODO: prove +/*@ +lemma void head_drop_n_equals_nths(list xs, int n) +requires n >= 0; +ensures head(drop(n, xs)) == nth(n, xs); +{ + // Will prove later. For now, we only validate with an example. + + list _xs = cons(1, cons(2, cons(3, cons(4, cons(5, cons(6, cons(7, nil))))))); + int _n = 4; + + list dn = drop(_n, _xs); + int hdn = head(dn); + int nthn = nth(_n, _xs); + + assert( hdn == head(drop(_n, _xs)) ); + assert( nthn == nth(_n, _xs )); + assert( head(drop(_n, _xs)) == nth(_n, _xs) ); + + + // ADMIT LEMMA, PROVE LATER + assume(false); +} +@*/ + #endif /* VERIFAST_LISTS_EXTENDED_H */ \ No newline at end of file