Skip to content

Commit

Permalink
Use array predicates to clarify array utils
Browse files Browse the repository at this point in the history
  • Loading branch information
@peterohanley
peterohanley committed Dec 20, 2024
1 parent 543d7e1 commit 7bc3ebe
Showing 1 changed file with 75 additions and 70 deletions.
145 changes: 75 additions & 70 deletions components/include/cn_array_utils.h
View file
Original file line number Diff line number Diff line change
Expand Up @@ -2,10 +2,54 @@
#define CN_ARRAY_UTILS_H_

/*$
predicate (map<u64,u8>) ArrayBlock_u8 (pointer p, u64 e)
{
take pv = each(u64 i; i >= 0u64 && i < e) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) ArrayOwned_u8 (pointer p, u64 e)
{
take pv = each(u64 i; i >= 0u64 && i < e) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) ArraySliceBlock_u8 (pointer p, u64 s, u64 e)
{
take pv = each(u64 i; i >= s && i < e) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) ArraySliceOwned_u8 (pointer p, u64 s, u64 e)
{
take pv = each(u64 i; i >= s && i < e) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) CondArraySliceBlock_u8 (pointer p, boolean c, u64 s, u64 e)
{
if (c) {
take pv = ArraySliceBlock_u8(p, s, e);
return pv;
} else {
return default<map<u64,u8> >;
}
}
predicate (map<u64,u8>) CondArraySliceOwned_u8 (pointer p, boolean c, u64 s, u64 e)
{
if (c) {
take pv = ArraySliceOwned_u8(p, s, e);
return pv;
} else {
return default<map<u64,u8> >;
}
}
predicate (map<u64,u8>) ArrayOrNull_u8 (pointer p, u64 l)
{
if (!is_null(p)) {
take pv = each(u64 i; i >= 0u64 && i < l) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
take pv = ArrayOwned_u8(p, l);
return pv;
} else {
return default<map<u64,u8> >;
Expand All @@ -15,7 +59,7 @@ predicate (map<u64,u8>) ArrayOrNull_u8 (pointer p, u64 l)
predicate (map<u64,u8>) ArrayOrNull_Block_u8 (pointer p, u64 l)
{
if (!is_null(p)) {
take pv = each(u64 i; i >= 0u64 && i < l) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
take pv = ArrayBlock_u8(p, l);
return pv;
} else {
return default<map<u64,u8> >;
Expand All @@ -24,135 +68,96 @@ predicate (map<u64,u8>) 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<len){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a1 = ArrayBlock_u8(tmp, len);
at >= 0u64;
len >= 0u64;
slen >= 0u64;
at < len;
slen <= len;
at + slen <= len;
ensures
take a2 = each(u64 j; 0u64<=j && j<at){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(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<len){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a1 = ArrayOwned_u8(tmp, len);
at >= 0u64;
len >= 0u64;
slen >= 0u64;
at < len;
slen <= len;
at + slen <= len;
ensures
take a2 = each(u64 j; 0u64<=j && j<at){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(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<at){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Block<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(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;
at < len;
slen <= len;
at + slen <= len;
ensures
take a1 = each(u64 j; 0u64<=j && j<len){Block<uint8_t>(array_shift<uint8_t>(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<at){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a3 = each(u64 j; ((u64)at)<=j && j<(at+slen)){Owned<uint8_t>(array_shift<uint8_t>(tmp, j))};
take a4 = each(u64 j; ((u64)(at+slen))<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(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;
at < len;
slen <= len;
at + slen <= len;
ensures
take a1 = each(u64 j; 0u64<=j && j<len){Owned<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(a,j))};
take a1 = ArraySliceBlock_u8(a, at, at+len);
ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
ensures
take a2 = each(u64 j; 0u64 <= j && j <len) {Block<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(a,j))};
take a1 = ArraySliceOwned_u8(a, at, at+len);
ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
ensures
take a2 = each(u64 j; 0u64 <= j && j <len) {Owned<uint8_t>(array_shift<uint8_t>(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 <len) {Block<uint8_t>(array_shift<uint8_t>(b,j))};
take a2 = ArrayBlock_u8(b, len);
ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
ensures
take a1 = each(u64 j; at <= j && j <(at+len)) {Block<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(b,j))};
take a2 = ArraySliceBlock_u8(b, s, e);
ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,oset));
ensures
take a1 = each(u64 j; (oset + s) <= j && j <(oset+e)) {Block<uint8_t>(array_shift<uint8_t>(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 <len) {Owned<uint8_t>(array_shift<uint8_t>(b,j))};
take a2 = ArrayOwned_u8(b, len);
ptr_eq(array_shift<uint8_t>(b,0u64), array_shift<uint8_t>(a,at));
ensures
take a1 = each(u64 j; at <= j && j <(at+len)) {Owned<uint8_t>(array_shift<uint8_t>(a,j))};
predicate (map<u64,u8>) ArrayBlock_u8 (pointer p, u64 e)
{
take pv = each(u64 i; i >= 0u64 && i < e) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) ArraySliceBlock_u8 (pointer p, u64 s, u64 e)
{
take pv = each(u64 i; i >= s && i < e) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) ArraySliceOwned_u8 (pointer p, u64 s, u64 e)
{
take pv = each(u64 i; i >= s && i < e) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
}
predicate (map<u64,u8>) CondArraySliceBlock_u8 (pointer p, boolean c, u64 s, u64 e)
{
if (c) {
take pv = each(u64 i; i >= s && i < e) {Block<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
} else {
return default<map<u64,u8> >;
}
}
predicate (map<u64,u8>) CondArraySliceOwned_u8 (pointer p, boolean c, u64 s, u64 e)
{
if (c) {
take pv = each(u64 i; i >= s && i < e) {Owned<uint8_t>(array_shift<uint8_t>(p,i))};
return pv;
} else {
return default<map<u64,u8> >;
}
}
take a1 = ArraySliceOwned_u8(a, at, at+len);
lemma TransmuteArray_Block_u16_u8(pointer a, u64 l)
requires
Expand All @@ -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<uint8_t>(array_shift<uint8_t>(a,i))};
take aib = each(u64 i; i >= ol && i < l) {Block<uint8_t>(array_shift<uint8_t>(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<uint8_t>(array_shift<uint8_t>(a,i))};
take aob = ArrayBlock_u8(a, l);
$*/

#endif // CN_ARRAY_UTILS_H_

0 comments on commit 7bc3ebe

Please sign in to comment.