From 70c164329565c7cf47fd2b78d385dcdeca64b396 Mon Sep 17 00:00:00 2001
From: Matthew Jones <mmtj@amazon.com>
Date: Thu, 24 Oct 2019 15:23:56 -0700
Subject: [PATCH] Make Main.dfy verify

---
 Makefile              | 1 +
 src/SDK/ToyClient.dfy | 2 ++
 2 files changed, 3 insertions(+)

diff --git a/Makefile b/Makefile
index 8db0b9986..91ec80285 100644
--- 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
index eb0796417..26ad8f955 100644
--- 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 {