subset type tweak to avoid depending on runtime library changes

aws · Feb 24, 2024 · eaf06aa · eaf06aa
1 parent 7d6e4c4
commit eaf06aa
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy b/TestVectorsAwsCryptographicMaterialProviders/dafny/KeyVectors/src/KeyDescription.dfy
@@ -218,8 +218,8 @@ module {:options "-functionSyntax:4"} KeyDescription {
          // SYMMETRIC_DEFAULT is not supported because RSA is asymmetric only
        ]
 
-  type KeyDescriptionVersion = v: nat | KeyDescriptionVersion?(v)  witness 1
-  predicate KeyDescriptionVersion?(v: nat)
+  type KeyDescriptionVersion = v: int | KeyDescriptionVersion?(v)  witness 1
+  predicate KeyDescriptionVersion?(v: int)
   {
     || v == 1
     || v == 2