From 7bc3ebe3c6eb3ff3519ae1ab14b7974f740d4a21 Mon Sep 17 00:00:00 2001 From: Gus O'Hanley Date: Fri, 20 Dec 2024 17:38:16 -0600 Subject: [PATCH] Use array predicates to clarify array utils --- components/include/cn_array_utils.h | 145 ++++++++++++++-------------- 1 file changed, 75 insertions(+), 70 deletions(-) diff --git a/components/include/cn_array_utils.h b/components/include/cn_array_utils.h index e521905a..12857425 100644 --- a/components/include/cn_array_utils.h +++ b/components/include/cn_array_utils.h @@ -2,10 +2,54 @@ #define CN_ARRAY_UTILS_H_ /*$ +predicate (map) ArrayBlock_u8 (pointer p, u64 e) +{ + take pv = each(u64 i; i >= 0u64 && i < e) {Block(array_shift(p,i))}; + return pv; +} + +predicate (map) ArrayOwned_u8 (pointer p, u64 e) +{ + take pv = each(u64 i; i >= 0u64 && i < e) {Owned(array_shift(p,i))}; + return pv; +} + +predicate (map) ArraySliceBlock_u8 (pointer p, u64 s, u64 e) +{ + take pv = each(u64 i; i >= s && i < e) {Block(array_shift(p,i))}; + return pv; +} + +predicate (map) ArraySliceOwned_u8 (pointer p, u64 s, u64 e) +{ + take pv = each(u64 i; i >= s && i < e) {Owned(array_shift(p,i))}; + return pv; +} + +predicate (map) CondArraySliceBlock_u8 (pointer p, boolean c, u64 s, u64 e) +{ + if (c) { + take pv = ArraySliceBlock_u8(p, s, e); + return pv; + } else { + return default >; + } +} + +predicate (map) CondArraySliceOwned_u8 (pointer p, boolean c, u64 s, u64 e) +{ + if (c) { + take pv = ArraySliceOwned_u8(p, s, e); + return pv; + } else { + return default >; + } +} + predicate (map) ArrayOrNull_u8 (pointer p, u64 l) { if (!is_null(p)) { - take pv = each(u64 i; i >= 0u64 && i < l) {Owned(array_shift(p,i))}; + take pv = ArrayOwned_u8(p, l); return pv; } else { return default >; @@ -15,7 +59,7 @@ predicate (map) ArrayOrNull_u8 (pointer p, u64 l) predicate (map) ArrayOrNull_Block_u8 (pointer p, u64 l) { if (!is_null(p)) { - take pv = each(u64 i; i >= 0u64 && i < l) {Block(array_shift(p,i))}; + take pv = ArrayBlock_u8(p, l); return pv; } else { return default >; @@ -24,7 +68,7 @@ predicate (map) ArrayOrNull_Block_u8 (pointer p, u64 l) lemma SplitAt_Block_u8(pointer tmp, u64 len, u64 at, u64 slen) requires - take a1 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; + take a1 = ArrayBlock_u8(tmp, len); at >= 0u64; len >= 0u64; slen >= 0u64; @@ -32,13 +76,13 @@ lemma SplitAt_Block_u8(pointer tmp, u64 len, u64 at, u64 slen) slen <= len; at + slen <= len; ensures - take a2 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; - take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Block(array_shift(tmp, j))}; - take a4 = each(u64 j; ((u64)(at+slen))<=j && j(array_shift(tmp, j))}; + take a2 = ArraySliceBlock_u8(tmp, 0u64, at); + take a3 = ArraySliceBlock_u8(tmp, at, at+slen); + take a4 = ArraySliceBlock_u8(tmp, at+slen, len); lemma SplitAt_Owned_u8(pointer tmp, u64 len, u64 at, u64 slen) requires - take a1 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; + take a1 = ArrayOwned_u8(tmp, len); at >= 0u64; len >= 0u64; slen >= 0u64; @@ -46,15 +90,15 @@ lemma SplitAt_Owned_u8(pointer tmp, u64 len, u64 at, u64 slen) slen <= len; at + slen <= len; ensures - take a2 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; - take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Owned(array_shift(tmp, j))}; - take a4 = each(u64 j; ((u64)(at+slen))<=j && j(array_shift(tmp, j))}; + take a2 = ArraySliceOwned_u8(tmp, 0u64, at); + take a3 = ArraySliceOwned_u8(tmp, at, at+slen); + take a4 = ArraySliceOwned_u8(tmp, at+slen, len); lemma UnSplitAt_Block_u8(pointer tmp, u64 len, u64 at, u64 slen) requires - take a2 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; - take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Block(array_shift(tmp, j))}; - take a4 = each(u64 j; ((u64)(at+slen))<=j && j(array_shift(tmp, j))}; + take a2 = ArraySliceBlock_u8(tmp, 0u64, at); + take a3 = ArraySliceBlock_u8(tmp, at, at+slen); + take a4 = ArraySliceBlock_u8(tmp, at+slen, len); at >= 0u64; len >= 0u64; slen >= 0u64; @@ -62,13 +106,13 @@ lemma UnSplitAt_Block_u8(pointer tmp, u64 len, u64 at, u64 slen) slen <= len; at + slen <= len; ensures - take a1 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; + take a1 = ArrayBlock_u8(tmp, len); lemma UnSplitAt_Owned_u8(pointer tmp, u64 len, u64 at, u64 slen) requires - take a2 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; - take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Owned(array_shift(tmp, j))}; - take a4 = each(u64 j; ((u64)(at+slen))<=j && j(array_shift(tmp, j))}; + take a2 = ArraySliceOwned_u8(tmp, 0u64, at); + take a3 = ArraySliceOwned_u8(tmp, at, at+slen); + take a4 = ArraySliceOwned_u8(tmp, at+slen, len); at >= 0u64; len >= 0u64; slen >= 0u64; @@ -76,83 +120,44 @@ lemma UnSplitAt_Owned_u8(pointer tmp, u64 len, u64 at, u64 slen) slen <= len; at + slen <= len; ensures - take a1 = each(u64 j; 0u64<=j && j(array_shift(tmp, j))}; + take a1 = ArrayOwned_u8(tmp, len); lemma ViewShift_Block_u8(pointer a, pointer b, u64 at, u64 len) requires - take a1 = each(u64 j; at <= j && j <(at+len)) {Block(array_shift(a,j))}; + take a1 = ArraySliceBlock_u8(a, at, at+len); ptr_eq(array_shift(b,0u64), array_shift(a,at)); ensures - take a2 = each(u64 j; 0u64 <= j && j (array_shift(b,j))}; + take a2 = ArrayBlock_u8(b, len); lemma ViewShift_Owned_u8(pointer a, pointer b, u64 at, u64 len) requires - take a1 = each(u64 j; at <= j && j <(at+len)) {Owned(array_shift(a,j))}; + take a1 = ArraySliceOwned_u8(a, at, at+len); ptr_eq(array_shift(b,0u64), array_shift(a,at)); ensures - take a2 = each(u64 j; 0u64 <= j && j (array_shift(b,j))}; + take a2 = ArrayOwned_u8(b, len); lemma UnViewShift_Block_u8(pointer a, pointer b, u64 at, u64 len) requires - take a2 = each(u64 j; 0u64 <= j && j (array_shift(b,j))}; + take a2 = ArrayBlock_u8(b, len); ptr_eq(array_shift(b,0u64), array_shift(a,at)); ensures - take a1 = each(u64 j; at <= j && j <(at+len)) {Block(array_shift(a,j))}; + take a1 = ArraySliceOwned_u8(a, at, at+len); // TODO this lemma takes an absolute start and end rather than an absolute start // and a length. This should show in the name. lemma UnViewShift_Block_At_u8(pointer a, pointer b, u64 oset, u64 s, u64 e) requires - take a2 = each(u64 j; s <= j && j < e) {Block(array_shift(b,j))}; + take a2 = ArraySliceBlock_u8(b, s, e); ptr_eq(array_shift(b,0u64), array_shift(a,oset)); ensures - take a1 = each(u64 j; (oset + s) <= j && j <(oset+e)) {Block(array_shift(a,j))}; - + take a1 = ArraySliceBlock_u8(a, oset+s, oset+e); lemma UnViewShift_Owned_u8(pointer a, pointer b, u64 at, u64 len) requires - take a2 = each(u64 j; 0u64 <= j && j (array_shift(b,j))}; + take a2 = ArrayOwned_u8(b, len); ptr_eq(array_shift(b,0u64), array_shift(a,at)); ensures - take a1 = each(u64 j; at <= j && j <(at+len)) {Owned(array_shift(a,j))}; - -predicate (map) ArrayBlock_u8 (pointer p, u64 e) -{ - take pv = each(u64 i; i >= 0u64 && i < e) {Block(array_shift(p,i))}; - return pv; -} - -predicate (map) ArraySliceBlock_u8 (pointer p, u64 s, u64 e) -{ - take pv = each(u64 i; i >= s && i < e) {Block(array_shift(p,i))}; - return pv; -} - -predicate (map) ArraySliceOwned_u8 (pointer p, u64 s, u64 e) -{ - take pv = each(u64 i; i >= s && i < e) {Owned(array_shift(p,i))}; - return pv; -} - -predicate (map) CondArraySliceBlock_u8 (pointer p, boolean c, u64 s, u64 e) -{ - if (c) { - take pv = each(u64 i; i >= s && i < e) {Block(array_shift(p,i))}; - return pv; - } else { - return default >; - } -} - -predicate (map) CondArraySliceOwned_u8 (pointer p, boolean c, u64 s, u64 e) -{ - if (c) { - take pv = each(u64 i; i >= s && i < e) {Owned(array_shift(p,i))}; - return pv; - } else { - return default >; - } -} + take a1 = ArraySliceOwned_u8(a, at, at+len); lemma TransmuteArray_Block_u16_u8(pointer a, u64 l) requires @@ -175,10 +180,10 @@ lemma UnTransmuteArray_Owned_u16_u8(pointer a, u64 l) lemma ForgetPartialInit_u8(pointer a, u64 l, u64 ol) requires ol <= l; - take aio = each(u64 i; i >= 0u64 && i < ol) {Owned(array_shift(a,i))}; - take aib = each(u64 i; i >= ol && i < l) {Block(array_shift(a,i))}; + take aio = ArrayOwned_u8(a, ol); + take aib = ArraySliceBlock_u8(a, ol, l); ensures - take aob = each(u64 i; i >= 0u64 && i < l) {Block(array_shift(a,i))}; + take aob = ArrayBlock_u8(a, l); $*/ #endif // CN_ARRAY_UTILS_H_