Skip to content
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.

Commit 9465722

Browse files
committedApr 29, 2025··
m
1 parent ac02188 commit 9465722

File tree

1 file changed

+3
-0
lines changed

1 file changed

+3
-0
lines changed
 

‎DynamoDbEncryption/dafny/DynamoDbEncryption/src/MemoryMath.dfy

Lines changed: 3 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,3 +1,6 @@
1+
// Copyright Amazon.com Inc. or its affiliates. All Rights Reserved.
2+
// SPDX-License-Identifier: Apache-2.0
3+
14
// When dealing with actual data in actual memory, we can be confident that
25
// none of the numbers will exceed an exabyte, so we can use uint64, rather than nat.
36
// To convince Dafny that this is true, we have the following functions

0 commit comments

Comments
 (0)
Please sign in to comment.