We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
1 parent 30235cd commit 061fe9bCopy full SHA for 061fe9b
DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy
@@ -496,9 +496,9 @@ module DynamoToStruct {
496
497
function method ListAttrToBytes(l: ListAttributeValue, depth : nat): (ret: Result<seq<uint8>, string>)
498
ensures ret.Success? ==>
499
- && U32ToBigEndian(|l|).Success?
500
- && LENGTH_LEN <= |ret.value|
501
- && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value
+ && U32ToBigEndian(|l|).Success?
+ && LENGTH_LEN <= |ret.value|
+ && ret.value[..LENGTH_LEN] == U32ToBigEndian(|l|).value
502
{
503
var count :- U32ToBigEndian(|l|);
504
var body :- CollectList(l, depth);
0 commit comments