refactor!: Change MultiKeyring.children to a seq<Keyring>

buildspec.yml

@@ -18,7 +18,7 @@ phases:
       # Although Dafny does have releases, we often need a newer hash than the latest release, while still needing the
       # the security of reproducible builds.
       - cd dafny
-      - git reset --hard 4ecab36652adc9ad67294e2232f1b763453c0de0
+      - git reset --hard 9d79b3cdfdaf8bea4b1455186eceeeca1c65fed1
       - cd ..
       - nuget restore dafny/Source/Dafny.sln
       - msbuild dafny/Source/Dafny.sln

src/SDK/Keyring/MultiKeyring.dfy

@@ -23,21 +23,20 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
     class MultiKeyring extends Keyring {
         const generator : Keyring?
         // TODO-RS: Make this a seq<Keyring> once https://github.com/dafny-lang/dafny/issues/406 is addressed
-        const children : array<Keyring>
-        constructor (g : Keyring?, c : array<Keyring>) ensures generator == g ensures children == c
+        const children : seq<Keyring>
+        constructor (g : Keyring?, c : seq<Keyring>) ensures generator == g ensures children == c
             requires g != null ==> g.Valid()
-            requires forall i :: 0 <= i < c.Length ==> c[i].Valid()
+            requires forall i :: 0 <= i < |c| ==> c[i].Valid()
             ensures Valid()
         {
             generator := g;
             children := c;
-            Repr := {this} + (if g != null then {g} + g.Repr else {}) + {children} + childrenRepr(c[..]);
+            Repr := {this} + (if g != null then {g} + g.Repr else {}) + childrenRepr(c);
         }
 
         predicate Valid() reads this, Repr {
-            && children in Repr
             && (generator != null ==> generator in Repr && generator.Repr <= Repr && generator.Valid())
-            && (forall j :: 0 <= j < children.Length ==> children[j] in Repr && children[j].Repr <= Repr && children[j].Valid())
+            && (forall j :: 0 <= j < |children| ==> children[j] in Repr && children[j].Repr <= Repr && children[j].Valid())
         }
 
         method OnEncrypt(materials: Materials.ValidEncryptionMaterials) returns (res: Result<Materials.ValidEncryptionMaterials>)
@@ -63,15 +62,15 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
             // Then apply each of the children in sequence
             // TODO-RS: Use folding here instead
             var i := 0;
-            while i < children.Length
+            while i < |children|
                 invariant resultMaterials.plaintextDataKey.Some?
                 invariant materials.encryptionContext == resultMaterials.encryptionContext
                 invariant materials.algorithmSuiteID == resultMaterials.algorithmSuiteID
                 invariant materials.plaintextDataKey.Some? ==> resultMaterials.plaintextDataKey == materials.plaintextDataKey
                 invariant materials.keyringTrace <= resultMaterials.keyringTrace
                 invariant materials.encryptedDataKeys <= resultMaterials.encryptedDataKeys
                 invariant materials.signingKey == resultMaterials.signingKey
-                decreases children.Length - i 
+                decreases |children| - i 
             {
                 resultMaterials :- children[i].OnEncrypt(resultMaterials);
                 i := i + 1;
@@ -104,14 +103,14 @@ module {:extern "MultiKeyringDef"} MultiKeyringDef {
                 }
             }
             var i := 0;
-            while i < children.Length
+            while i < |children|
                 invariant res.Success? ==> 
                         && materials.encryptionContext == res.value.encryptionContext
                         && materials.algorithmSuiteID == res.value.algorithmSuiteID 
                         && (materials.plaintextDataKey.Some? ==> res.value.plaintextDataKey == materials.plaintextDataKey)
                         && materials.keyringTrace <= res.value.keyringTrace
                         && materials.verificationKey == res.value.verificationKey
-                decreases children.Length - i
+                decreases |children| - i
             {
                 var onDecryptResult := children[i].OnDecrypt(materials, edks);
                 if onDecryptResult.Failure? {

src/api/dotnet/Client.cs

@@ -3,11 +3,11 @@
 using System.IO;
 using System.Collections.Generic;
 using System.Linq;
-using _System;
 using CMMDefs;
 using Dafny;
-using byteseq = Dafny.Sequence<byte>;
-using charseq = Dafny.Sequence<char>;
+using ibyteseq = Dafny.ISequence<byte>;
+using icharseq = Dafny.ISequence<char>;
+using encryptioncontext = Dafny.Map<Dafny.ISequence<byte>, Dafny.ISequence<byte>>;
 
 namespace AWSEncryptionSDK
 {
@@ -19,15 +19,15 @@ public static MemoryStream Encrypt(MemoryStream plaintext, CMM cmm, Dictionary<s
             if (algorithmSuiteID != null && !AlgorithmSuite.__default.VALID__IDS.Elements.Contains((ushort)algorithmSuiteID)) {
                 throw new ArgumentException("Invalid algorithmSuiteID: " + algorithmSuiteID.ToString());
             }
-            byteseq dafnyPlaintext = DafnyFFI.SequenceFromMemoryStream(plaintext);
+            ibyteseq dafnyPlaintext = DafnyFFI.SequenceFromMemoryStream(plaintext);
 
             // TODO: This isn't checking for nulls or any of the requirements on the Dafny method.
             // See https://github.com/dafny-lang/dafny/issues/461.
             // TODO: Might need a lock here if ANYTHING in the Dafny runtime isn't threadsafe!
             var optAlgorithmSuiteID = algorithmSuiteID != null ? STL.Option<ushort>.create_Some((ushort)algorithmSuiteID) : STL.Option<ushort>.create_None();
             var optFrameLength = frameLength != null ? STL.Option<uint>.create_Some((uint)frameLength) : STL.Option<uint>.create_None();
-            var dafnyEncryptionContext = encryptionContext != null ? STL.Option<Map<Sequence<byte>, Sequence<byte>>>.create_Some(ToDafnyEncryptionContext(encryptionContext)) : STL.Option<Map<Sequence<byte>, Sequence<byte>>>.create_None();
-            STL.Result<byteseq> result = ESDKClient.__default.Encrypt(
+            var dafnyEncryptionContext = encryptionContext != null ? STL.Option<encryptioncontext>.create_Some(ToDafnyEncryptionContext(encryptionContext)) : STL.Option<encryptioncontext>.create_None();
+            STL.Result<ibyteseq> result = ESDKClient.__default.Encrypt(
                     dafnyPlaintext,
                     cmm,
                     dafnyEncryptionContext,
@@ -40,20 +40,19 @@ public static MemoryStream Encrypt(MemoryStream plaintext, CMM cmm, Dictionary<s
 
         // TODO: Proper documentation
         public static MemoryStream Decrypt(MemoryStream cyphertext, CMM cmm) {
-            byteseq dafnyPlaintext = DafnyFFI.SequenceFromMemoryStream(cyphertext);
+            ibyteseq dafnyPlaintext = DafnyFFI.SequenceFromMemoryStream(cyphertext);
 
             // TODO: Might need a lock here if ANYTHING in the Dafny runtime isn't threadsafe!
-            STL.Result<byteseq> result = ESDKClient.__default.Decrypt(dafnyPlaintext, cmm);
+            STL.Result<ibyteseq> result = ESDKClient.__default.Decrypt(dafnyPlaintext, cmm);
 
             return DafnyFFI.MemoryStreamFromSequence(DafnyFFI.ExtractResult(result));
         }
 
-        private static Map<Sequence<byte>, Sequence<byte>> 
-            ToDafnyEncryptionContext(Dictionary<string, string> encryptionContext)
+        private static encryptioncontext ToDafnyEncryptionContext(Dictionary<string, string> encryptionContext)
         {
-            IEnumerable<Pair<byteseq, byteseq>> e = encryptionContext.Select(entry
-                => new Pair<byteseq, byteseq>(DafnyFFI.DafnyUTF8BytesFromString(entry.Key), DafnyFFI.DafnyUTF8BytesFromString(entry.Value)));
-            return Map<Sequence<byte>, Sequence<byte>>.FromElements(e.ToArray());
+            IEnumerable<Pair<ibyteseq, ibyteseq>> e = encryptionContext.Select(entry
+                => new Pair<ibyteseq, ibyteseq>(DafnyFFI.DafnyUTF8BytesFromString(entry.Key), DafnyFFI.DafnyUTF8BytesFromString(entry.Value)));
+            return encryptioncontext.FromElements(e.ToArray());
         }
     }
 }

src/api/dotnet/DafnyFFI.cs

@@ -3,42 +3,44 @@
 using System.Text;
 using STL;
 
+using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
+using icharseq = Dafny.ISequence<char>;
 using charseq = Dafny.Sequence<char>;
 
 // General-purpose utilities for invoking Dafny from C#,
 // including converting between common Dafny and C# datatypes. 
 public class DafnyFFI {
 
-    public static MemoryStream MemoryStreamFromSequence(byteseq seq) {
+    public static MemoryStream MemoryStreamFromSequence(ibyteseq seq) {
         // TODO: Find a way to safely avoid copying 
         byte[] copy = new byte[seq.Elements.Length];
         Array.Copy(seq.Elements, 0, copy, 0, seq.Elements.Length);
         return new MemoryStream(copy);
     }
 
-    public static byteseq SequenceFromMemoryStream(MemoryStream bytes) {
+    public static ibyteseq SequenceFromMemoryStream(MemoryStream bytes) {
         // TODO: Find a way to safely avoid copying 
         return byteseq.FromArray(bytes.ToArray());
     }
 
-    public static byteseq SequenceFromByteArray(byte[] bytearray) {
+    public static ibyteseq SequenceFromByteArray(byte[] bytearray) {
         return byteseq.FromArray(bytearray);
     }
 
-    public static string StringFromDafnyString(charseq dafnyString) {
+    public static string StringFromDafnyString(icharseq dafnyString) {
         // TODO: Find a way to safely avoid copying.
         // The contents of a Dafny.Sequence should never change, but since a Dafny.ArraySequence
         // currently allows direct access to its array we can't assume that's true.
         return new string(dafnyString.Elements);
     }
 
-    public static charseq DafnyStringFromString(string s) {
+    public static icharseq DafnyStringFromString(string s) {
         // This is safe since string#ToCharArray() creates a fresh array
         return charseq.FromArray(s.ToCharArray());
     }
 
-    public static byteseq DafnyUTF8BytesFromString(string s) {
+    public static ibyteseq DafnyUTF8BytesFromString(string s) {
         return byteseq.FromArray(Encoding.UTF8.GetBytes(s));
     }
 

src/api/dotnet/Keyrings.cs

@@ -8,6 +8,7 @@
 using RawRSAKeyringDef;
 using KMSUtils;
 using STL;
+using icharseq = Dafny.ISequence<char>;
 using charseq = Dafny.Sequence<char>;
 
 namespace AWSEncryptionSDK
@@ -24,17 +25,17 @@ public static Keyring MakeKMSKeyring(ClientSupplier clientSupplier,
             // This isn't checking for nulls or any other requirements.
             result.__ctor(
                 clientSupplier, 
-                Dafny.Sequence<charseq>.FromElements(keyIDs.Select(DafnyFFI.DafnyStringFromString).ToArray()),
+                Dafny.Sequence<icharseq>.FromElements(keyIDs.Select(DafnyFFI.DafnyStringFromString).ToArray()),
                 DafnyFFI.NullableToOption(generator != null ? DafnyFFI.DafnyStringFromString(generator) : null),
-                Dafny.Sequence<charseq>.FromElements(grantTokens.Select(DafnyFFI.DafnyStringFromString).ToArray()));
+                Dafny.Sequence<icharseq>.FromElements(grantTokens.Select(DafnyFFI.DafnyStringFromString).ToArray()));
             return result;
         }
         // TODO: Eventually the MultiKeyring will take a sequence instead of an array.
-        public static MultiKeyring MakeMultiKeyring(Keyring generator, Keyring[] children)
+        public static MultiKeyring MakeMultiKeyring(Keyring generator, IList<Keyring> children)
         {
             // TODO: Check for null value etc.
             MultiKeyring result = new MultiKeyring();
-            result.__ctor(generator, children);
+            result.__ctor(generator, Dafny.Sequence<Keyring>.FromArray(children.ToArray()));
             return result;
         }
         public static RawAESKeyring MakeRawAESKeyring(byte[] nameSpace, byte[] name, byte[] wrappingKey, DafnyFFI.AESWrappingAlgorithm wrappingAlgorithm)

src/extern/dotnet/AESEncryption.cs

@@ -5,7 +5,9 @@
 using Org.BouncyCastle.Crypto.Modes;
 using Org.BouncyCastle.Crypto.Parameters;
 
+using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
+using icharseq = Dafny.ISequence<char>;
 using charseq = Dafny.Sequence<char>;
 
 
@@ -14,10 +16,10 @@ namespace AESEncryption {
     public partial class AES_GCM {
 
         public static STL.Result<EncryptionOutput> AESEncrypt(EncryptionSuites.EncryptionSuite encAlg,
-                                                      byteseq iv,
-                                                      byteseq key,
-                                                      byteseq msg,
-                                                      byteseq aad) {
+                                                      ibyteseq iv,
+                                                      ibyteseq key,
+                                                      ibyteseq msg,
+                                                      ibyteseq aad) {
             try {
                 var cipher = new GcmBlockCipher(new AesEngine());
                 var param = new AeadParameters(new KeyParameter(key.Elements), (int)encAlg.tagLen * 8, iv.Elements, aad.Elements);
@@ -33,20 +35,20 @@ public static STL.Result<EncryptionOutput> AESEncrypt(EncryptionSuites.Encryptio
             }
         }
 
-        public static STL.Result<byteseq> AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, byteseq key, byteseq cipherText, byteseq authTag, byteseq iv, byteseq aad) {
+        public static STL.Result<ibyteseq> AESDecrypt(EncryptionSuites.EncryptionSuite encAlg, ibyteseq key, ibyteseq cipherText, ibyteseq authTag, ibyteseq iv, ibyteseq aad) {
             try {
                 var cipher = new GcmBlockCipher(new AesEngine());
                 var param = new AeadParameters(new KeyParameter(key.Elements), encAlg.tagLen * 8, iv.Elements, aad.Elements);
                 cipher.Init(false, param);
-                var ctx = cipherText.Concat(authTag);
+                var ctx = byteseq.Concat(cipherText, authTag);
                 var pt = new byte[cipher.GetOutputSize(ctx.Elements.Length)];
                 var len = cipher.ProcessBytes(ctx.Elements, 0, ctx.Elements.Length, pt, 0);
                 cipher.DoFinal(pt, len); //Check message authentication tag
-                return STL.Result<byteseq>.create_Success(byteseq.FromArray(pt));
+                return STL.Result<ibyteseq>.create_Success(byteseq.FromArray(pt));
             } catch(InvalidCipherTextException macEx) {
-                return STL.Result<byteseq>.create_Failure(charseq.FromArray(macEx.ToString().ToCharArray()));
+                return STL.Result<ibyteseq>.create_Failure(charseq.FromArray(macEx.ToString().ToCharArray()));
             } catch {
-                return STL.Result<byteseq>.create_Failure(charseq.FromArray("aes decrypt err".ToCharArray()));
+                return STL.Result<ibyteseq>.create_Failure(charseq.FromArray("aes decrypt err".ToCharArray()));
             }
         }
     }

src/extern/dotnet/HMAC.cs

@@ -1,6 +1,7 @@
 using System;
 using System.Numerics;
 
+using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
 
 namespace HMAC {
@@ -29,20 +30,20 @@ public HMac(Digests digest) {
             hmac = new Org.BouncyCastle.Crypto.Macs.HMac(bouncyCastleDigest);
         }
 
-        public void Init(byteseq input) {
+        public void Init(ibyteseq input) {
             // KeyParameter/ Init should not mutate input, but this is safer than using input.Elements directly
             byte[] elemCopy = (byte[]) input.Elements.Clone();
             var keyParams = new Org.BouncyCastle.Crypto.Parameters.KeyParameter(elemCopy);
             hmac.Init(keyParams);
         }
 
-        public void BlockUpdate(byteseq input) {
+        public void BlockUpdate(ibyteseq input) {
             // BlockUpdate should not mutate input, but this is safer than using input.Elements directly
             byte[] elemCopy = (byte[]) input.Elements.Clone();
             hmac.BlockUpdate(elemCopy, 0, elemCopy.Length);
         }
 
-        public byteseq GetResult() {
+        public ibyteseq GetResult() {
             byte[] output = new byte[hmac.GetMacSize()];
             hmac.DoFinal(output, 0);
             return byteseq.FromArray(output);

src/extern/dotnet/KMS.cs

@@ -7,9 +7,11 @@
 using Amazon;
 
 using KMS = Amazon.KeyManagementService;
+using IDString = Dafny.ISequence<char>;
 using DString = Dafny.Sequence<char>;
+using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
-using EncryptionContext = Dafny.Map<Dafny.Sequence<byte>, Dafny.Sequence<byte>>;
+using EncryptionContext = Dafny.Map<Dafny.ISequence<byte>, Dafny.ISequence<byte>>;
 
 namespace KMSUtils {
     public partial class __default {
@@ -25,21 +27,21 @@ public static Dictionary<String, String> EncryptionContextToString(EncryptionCon
 
         //TODO: Issue #54
         public static ResponseMetadata ConvertMetaData(Amazon.Runtime.ResponseMetadata rmd) {
-            Dafny.Map<DString, DString> metadata = Dafny.Map<DString, DString>
+            Dafny.Map<IDString, IDString> metadata = Dafny.Map<IDString, IDString>
                 .FromCollection(rmd.Metadata.Select(
-                            kvp => new Dafny.Pair<DString, DString>((DString.FromString(kvp.Key.ToString())), (DString.FromString(kvp.Value.ToString())))
+                            kvp => new Dafny.Pair<IDString, IDString>((DString.FromString(kvp.Key.ToString())), (DString.FromString(kvp.Value.ToString())))
                             ).ToList());
-            DString requestID = DString.FromString(rmd.RequestId.ToString());
+            IDString requestID = DString.FromString(rmd.RequestId.ToString());
             return new ResponseMetadata(metadata, requestID);
         }
-        public static byte[] ConvertByteSeq(byteseq bytes) {
+        public static byte[] ConvertByteSeq(ibyteseq bytes) {
             return (byte[])bytes.Elements.Clone();
         }
     }
     public partial class DefaultClientSupplier : ClientSupplier {
-        public STL.Result<KMSClient> GetClient(STL.Option<DString> region) {
+        public STL.Result<KMSClient> GetClient(STL.Option<IDString> region) {
             if (region.is_Some) {
-                string regionString = ((STL.Option_Some<DString>) region).get.ToString();
+                string regionString = ((STL.Option_Some<IDString>) region).get.ToString();
                 RegionEndpoint regionEndpoint = RegionEndpoint.GetBySystemName(regionString);
                 KMS.AmazonKeyManagementServiceClient amazonKeyManagementServiceClient = new KMS.AmazonKeyManagementServiceClient(regionEndpoint);
                 KMSClient kmsClient = new KMSClient(amazonKeyManagementServiceClient);

src/extern/dotnet/MessageHeader.cs

@@ -1,22 +1,23 @@
 using System;
 using System.Linq;
 using System.Collections.Generic;
+using ibyteseq = Dafny.ISequence<byte>;
 using byteseq = Dafny.Sequence<byte>;
 
 namespace MessageHeader {
 
   public partial class __default {
 
-    public static Dafny.Map<byteseq,byteseq> KVPairSequenceToMap(Dafny.Sequence<_System.Tuple2<byteseq,byteseq>> kvPairs) {
-        Dictionary<byteseq, byteseq> dict = kvPairs.Elements.ToDictionary(
+    public static Dafny.Map<ibyteseq,ibyteseq> KVPairSequenceToMap(Dafny.ISequence<_System.Tuple2<ibyteseq,ibyteseq>> kvPairs) {
+        Dictionary<ibyteseq, ibyteseq> dict = kvPairs.Elements.ToDictionary(
             item => item._0,
             item => item._1);
-        List<Dafny.Pair<byteseq, byteseq>> pairs = new List<Dafny.Pair<byteseq, byteseq>>();
+        List<Dafny.Pair<ibyteseq, ibyteseq>> pairs = new List<Dafny.Pair<ibyteseq, ibyteseq>>();
 
-        foreach(KeyValuePair<byteseq, byteseq> entry in dict) {
-            pairs.Add(new Dafny.Pair<byteseq, byteseq>(entry.Key, entry.Value));
+        foreach(KeyValuePair<ibyteseq, ibyteseq> entry in dict) {
+            pairs.Add(new Dafny.Pair<ibyteseq, ibyteseq>(entry.Key, entry.Value));
         }
-        return Dafny.Map<byteseq,byteseq>.FromCollection(pairs);
+        return Dafny.Map<ibyteseq,ibyteseq>.FromCollection(pairs);
     }
   }
 }