From be9de4d5704a4355065659e126e2f90bfc7f2cee Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 23 Nov 2022 11:28:27 -0500 Subject: [PATCH] Added lemma `DLS_nonEndItem_next_close` to help closing DLS opened with `DLS_nonEndItem_next_open`. --- .../scp_list_predicates_extended.h | 135 ++++++++++++++---- .../verifast/proof/verifast_lists_extended.h | 55 +++++++ 2 files changed, 160 insertions(+), 30 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 c09234dfb..020f55e05 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 @@ -74,26 +74,29 @@ requires length(gCells) > 1 &*& pxItem != gEnd; -ensures // DLS prefix - DLS(gEnd, gEndPrev, pxItem, ?pxItem_prev, - take(index_of(pxItem, gCells), gCells), - take(index_of(pxItem, gCells), gVals), - pxList) - &*& - // item of interest - xLIST_ITEM(pxItem, nth(index_of(pxItem, gCells), gVals), - ?pxItem_next, pxItem_prev, pxList) - &*& - // DLS suffix - (pxItem != gEndPrev - ? DLS(pxItem_next, pxItem, gEnd, gEndPrev, - drop(1, drop(index_of(pxItem, gCells), gCells)), - drop(1, drop(index_of(pxItem, gCells), gVals)), - pxList) - : true - ) - &*& - mem(pxItem_next, gCells) == true; +ensures + // DLS prefix + DLS(gEnd, gEndPrev, pxItem, ?pxItem_prev, + take(index_of(pxItem, gCells), gCells), + take(index_of(pxItem, gCells), gVals), + pxList) + &*& + // item of interest + xLIST_ITEM(pxItem, ?gItemVal, ?pxItem_next, pxItem_prev, pxList) &*& + gItemVal == nth(index_of(pxItem, gCells), gVals) + &*& + // DLS suffix + (pxItem != gEndPrev + ? DLS(pxItem_next, pxItem, gEnd, gEndPrev, + drop(1, drop(index_of(pxItem, gCells), gCells)), + drop(1, drop(index_of(pxItem, gCells), gVals)), + pxList) + : (pxItem_next == gEnd &*& + index_of(pxItem, gCells) == length(gCells) - 1 + ) + ) + &*& + mem(pxItem_next, gCells) == true; { int pxItemIndex_0 = index_of(pxItem, gCells); @@ -123,6 +126,10 @@ ensures // DLS prefix // `mem( pxItem->pxNext, gCells) == true )` // which requires accessing `pxItem->pxNext` if(pxItem == gEndPrev) { + assert( drop(pxItemIndex_0, gCells) == cons(pxItem, nil) ); + drop_index_equals_singleton_implies_last_element(gCells, pxItem); + assert( pxItemIndex_0 == length(gCells) - 1 ); + // `pxItem` is last element in DLS suffix // -> `pxItem_next` is head fo DLS prefix // open DLS prefix @@ -162,6 +169,79 @@ ensures // DLS prefix close xLIST_ITEM(pxItem, gItemVal, pxItem_next, pxItem_prev, pxList); } } + + +lemma void DLS_nonEndItem_next_close(struct xLIST* pxList, struct xLIST_ITEM* pxItem, + list gCells, + list gVals) +requires + length(gCells) == length(gVals) &*& + length(gCells) > 1 + &*& + // DLS prefix + DLS(?gEnd, ?gEndPrev, pxItem, ?gItem_prev, ?gCellsPrefix, ?gValsPrefix, + pxList) + &*& + mem(pxItem, gCells) == true &*& + gCellsPrefix == take(index_of(pxItem, gCells), gCells) &*& + gValsPrefix == take(index_of(pxItem, gCells), gVals) + &*& + // item of interest + pxItem != gEnd &*& + xLIST_ITEM(pxItem, ?gItemVal, ?gItem_next, gItem_prev, pxList) &*& + mem(gItemVal, gVals) == true &*& + gItemVal == nth(index_of(pxItem, gCells), gVals) + &*& + // DLS suffix + (pxItem != gEndPrev + ? DLS(gItem_next, pxItem, gEnd, gEndPrev, + drop(1, drop(index_of(pxItem, gCells), gCells)), + drop(1, drop(index_of(pxItem, gCells), gVals)), + pxList) + : (gItem_next == gEnd &*& + index_of(pxItem, gCells) == length(gCells) - 1 + ) + ) + &*& + mem(gItem_next, gCells) == true; +ensures + DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, pxList); +{ + int gItemIndex = index_of(pxItem, gCells); + head_drop_n_equals_nths(gCells, gItemIndex); + head_drop_n_equals_nths(gVals, gItemIndex); + + if( pxItem != gEndPrev ) { + assert( drop(gItemIndex, gVals) == cons(_, _) ); + assert( xLIST_ITEM(pxItem, ?gV, _, gItem_prev, pxList) ); + nth_index(gCells, pxItem); + close DLS(pxItem, gItem_prev, gEnd, gEndPrev, + drop(gItemIndex, gCells), drop(gItemIndex, gVals), + pxList); + join(gEnd, gEndPrev, pxItem, gItem_prev, gCellsPrefix, gValsPrefix, + pxItem, gItem_prev, gEnd, gEndPrev, drop(gItemIndex, gCells), drop(gItemIndex, gVals)); + } else { + assert( xLIST_ITEM(pxItem, ?gV, ?gNext, gItem_prev, pxList) ); + assert( xLIST_ITEM(pxItem, gV, gEnd, gItem_prev, pxList) ); + close DLS(pxItem, gItem_prev, gEnd, gEndPrev, cons(pxItem, nil), cons(gItemVal, nil), pxList); + join(gEnd, gEndPrev, pxItem, gItem_prev, gCellsPrefix, gValsPrefix, + pxItem, gItem_prev, gEnd, gEndPrev, cons(pxItem, nil), cons(gItemVal, nil)); + assert( DLS(gEnd, gEndPrev, gEnd, gEndPrev, ?gCellsRes, ?gValsRes, pxList)); + + assert( gCellsPrefix == take(index_of(pxItem, gCells), gCells) ); + assert( gValsPrefix == take(index_of(pxItem, gCells), gVals) ); + assert( gCellsRes == append(gCellsPrefix, cons(pxItem, nil)) ); + assert( gValsRes == append(gValsPrefix, cons(gItemVal, nil)) ); + + + drop_cons(gCells, index_of(pxItem, gCells)); + drop_cons(gVals, index_of(pxItem, gCells)); + nth_index(gCells, pxItem); + + assert( gCellsRes == gCells ); + assert( gValsRes == gVals ); + } +} @*/ /* By verifying the following function, we can validate that the above lemmas @@ -189,12 +269,12 @@ void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem) DLS_nonEndItem_next_open(gList, gTaskItem_0); } @*/ - pxTaskItem = pxTaskItem->pxNext; + + pxTaskItem = pxTaskItem->pxNext; //@ struct xLIST_ITEM* pxItem_1 = pxTaskItem; - //@ assert( mem(pxItem_1, gCells) == true ); - + //@ close xLIST_ITEM(gTaskItem_0, ?gTaskItemVal, _, _, gList); /*@ if( gTaskItem_0 == gEnd ) { @@ -204,17 +284,12 @@ void lemma_validation__DLS_item_next(struct xLIST_ITEM* pxTaskItem) // why is this necessary? assert( gCells == cons( _, _) ); assert( gVals == cons(_, _) ); - - // 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); + DLS_nonEndItem_next_close(gList, gTaskItem_0, gCells, gVals); } @*/ -;; + //@ assert( mem(pxItem_1, gCells) == true ); } diff --git a/verification/verifast/proof/verifast_lists_extended.h b/verification/verifast/proof/verifast_lists_extended.h index 4d019ab54..adf29a0f0 100644 --- a/verification/verifast/proof/verifast_lists_extended.h +++ b/verification/verifast/proof/verifast_lists_extended.h @@ -33,6 +33,61 @@ ensures head(drop(n, xs)) == nth(n, xs); assert( head(drop(_n, _xs)) == nth(_n, _xs) ); + // ADMIT LEMMA, PROVE LATER + assume(false); +} + +// TODO: prove +lemma void drop_index_equals_singleton_implies_last_element(list xs, t x) +requires drop(index_of(x, xs), xs) == cons(x, nil); +ensures index_of(x, xs) == length(xs) - 1; +{ + // 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 _x = 7; + + int i = index_of(_x, _xs); + list d = drop(index_of(x, xs), _xs); + + assert( index_of(_x, _xs) == length(_xs) - 1 ); + + // ADMIT LEMMA, PROVE LATER + assume(false); +} + +// TODO: prove +lemma void drop_cons(list xs, int n) +requires n < length(xs); +ensures drop(n, xs) == cons(nth(n, xs), drop(n+1, 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 = 3; + + list dn = drop(_n, _xs); + int nthn = nth(_n, _xs); + list dnp1 = drop(_n + 1, _xs); + + assert( drop(_n, _xs) == cons(nth(_n, _xs), drop(_n+1, _xs)) ); + + // ADMIT LEMMA, PROVE LATER + assume(false); +} + +// TODO: prove +lemma void nth_index(list xs, t x) +requires mem(x, xs) == true; +ensures nth(index_of(x, xs), xs) == x; +{ + // 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 _x = 4; + + int i = index_of(_x, _xs); + int nthi = nth(index_of(_x, _xs), _xs); + + assert( nth(index_of(_x, _xs), _xs) == _x ); + // ADMIT LEMMA, PROVE LATER assume(false); }