From dec93a2d8862904b659e362fbc9c5b88709a66cc Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 6 Nov 2023 11:16:28 -0800 Subject: [PATCH 1/2] Avoid stacking newtype definition to avoid bug fixed by dafny #4569 --- DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy index 986846fc1..700318273 100644 --- a/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy +++ b/DynamoDbEncryption/dafny/DynamoDbEncryption/src/SearchInfo.dfy @@ -30,7 +30,7 @@ module SearchableEncryptionInfo { //= specification/searchable-encryption/search-config.md#version-number //= type=implication //# A version number MUST be `1`. - newtype VersionNumber = x : uint64 | x == 1 witness 1 + newtype VersionNumber = x : int | x == 1 witness 1 type ValidSearchInfo = x : SearchInfo | x.ValidState() witness * From 0b8988b5c53152cd811290867e84efe246eadbdc Mon Sep 17 00:00:00 2001 From: Robin Salkeld Date: Mon, 6 Nov 2023 13:24:10 -0800 Subject: [PATCH 2/2] fix: Avoid stacking newtype definition to avoid bug fixed by Dafny PR #4569