Make Main.dfy verify

aws · Oct 24, 2019 · 70c1643 · 70c1643
1 parent 313f647
commit 70c1643
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 0 deletions.
diff --git a/Makefile b/Makefile
@@ -15,6 +15,7 @@ SRCS = \
 	   src/Crypto/Random.dfy \
 	   src/Crypto/RSAEncryption.dfy \
 	   src/Crypto/Signature.dfy \
+	   src/Main.dfy \
 	   src/SDK/AlgorithmSuite.dfy \
 	   src/SDK/CMM/DefaultCMM.dfy \
 	   src/SDK/CMM/Defs.dfy \

diff --git a/src/SDK/ToyClient.dfy b/src/SDK/ToyClient.dfy
@@ -69,6 +69,8 @@ module ToyClientDef {
     method Encrypt(pt: seq<uint8>, ec: Materials.EncryptionContext) returns (res: Result<Encryption>)
       requires Valid()
       ensures Valid()
+      ensures res.Success? ==> |res.value.authTag| == ALGORITHM.tagLen as int
+      ensures res.Success? ==> |res.value.iv| == ALGORITHM.ivLen as int
     {
       var em :- GetEncMaterials(ec);
       if |em.plaintextDataKey.get| != 32 {