feat: simplify structured encryption (#866)

* feat: simplify structured encryption

Author: ajewellamz

DynamoDbEncryption/.gitignore

@@ -3,3 +3,5 @@ ImplementationFromDafny.cs
 TestsFromDafny.cs
 **/bin
 **/obj
+node_modules
+project.properties

DynamoDbEncryption/Makefile

@@ -77,3 +77,8 @@ SERVICE_DEPS_DynamoDbEncryptionTransforms := \
 
 format_net:
 	pushd runtimes/net && dotnet format DynamoDbEncryption.csproj && popd
+
+polymorph:
+	export DAFNY_VERSION=4.2
+	npm i --no-save prettier@3 [email protected]
+	make polymorph_code_gen PROJECT_DEPENDENCIES=

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -347,8 +347,8 @@ list ConstructorPartList {
 //= specification/searchable-encryption/virtual.md#virtual-field-initialization
 //= type=implication
 //# On initialization of a Virtual Field, the caller MUST provide:
-//#  * A name -- a string
-//#  * A list of [Virtual Parts](#virtual-part-initialization)
+//# - A name -- a string
+//# - A list of [Virtual Parts](#virtual-part-initialization)
 
 @javadoc("The configuration for a Virtual Field. A Virtual Field is a field constructed from parts of other fields for use with beacons, but never itself stored on items.")
 structure VirtualField {
@@ -442,8 +442,8 @@ structure GetSuffix {
 //= specification/searchable-encryption/virtual.md#getsubstring-transform-initialization
 //= type=implication
 //# On initialization of a GetSubstring Transform, the caller MUST provide:
-//#  * low : an integer [position](#position-definition)
-//#  * high : an integer [position](#position-definition)
+//# - low : an integer [position](#position-definition)
+//# - high : an integer [position](#position-definition)
 
 // return range of characters, 0-based counting
 // low is inclusive, high is exclusive
@@ -464,8 +464,8 @@ structure GetSubstring {
 //= specification/searchable-encryption/virtual.md#getsegment-transform-initialization
 //= type=implication
 //# On initialization of a GetSegment Transform, the caller MUST provide:
-//#  * split : an character
-//#  * index : an integer [position](#position-definition)
+//# - split : an character
+//# - index : an integer [position](#position-definition)
 
 // split string on character, then return one piece.
 // 'index' has the same semantics as 'low' in GetSubstring
@@ -482,9 +482,9 @@ structure GetSegment {
 //= specification/searchable-encryption/virtual.md#getsegments-transform-initialization
 //= type=implication
 //# On initialization of a GetSegments Transform, the caller MUST provide:
-//#  * split : an character
-//#  * low : an integer [position](#position-definition)
-//#  * high : an integer [position](#position-definition)
+//# - split : an character
+//# - low : an integer [position](#position-definition)
+//# - high : an integer [position](#position-definition)
 
 // split string on character, then return range of pieces.
 // 'low' and 'high' have the same semantics as GetSubstring
@@ -504,14 +504,14 @@ structure GetSegments {
 //= specification/searchable-encryption/virtual.md#virtual-transform-initialization
 //= type=implication
 //# On initialization of a Virtual Transform, the caller MUST provide exactly one of
-//#  * an [Upper](#upper-transform-initialization) transform
-//#  * a [Lower](#lower-transform-initialization) transform
-//#  * an [Insert](#insert-transform-initialization) transform
-//#  * a [GetPrefix](#getprefix-transform-initialization) transform
-//#  * a [GetSuffix](#getsuffix-transform-initialization) transform
-//#  * a [GetSubstring](#getsubstring-transform-initialization) transform
-//#  * a [GetSegment](#getsegment-transform-initialization) transform
-//#  * a [GetSegments](#getsegments-transform-initialization) transform
+//# - an [Upper](#upper-transform-initialization) transform
+//# - a [Lower](#lower-transform-initialization) transform
+//# - an [Insert](#insert-transform-initialization) transform
+//# - a [GetPrefix](#getprefix-transform-initialization) transform
+//# - a [GetSuffix](#getsuffix-transform-initialization) transform
+//# - a [GetSubstring](#getsubstring-transform-initialization) transform
+//# - a [GetSegment](#getsegment-transform-initialization) transform
+//# - a [GetSegments](#getsegments-transform-initialization) transform
 
 union VirtualTransform {
   upper: Upper,
@@ -566,10 +566,10 @@ structure SharedSet {
 //= type=implication
 //# On initialization of a Beacon Style, the caller MUST provide exactly one of
 //# 
-//#  * a [PartOnly](#partonly-initialization)
-//#  * a [Shared](#shared-initialization)
-//#  * an [AsSet](#asset-initialization)
-//#  * a [SharedSet](#sharedset-initialization)
+//# - a [PartOnly](#partonly-initialization)
+//# - a [Shared](#shared-initialization)
+//# - an [AsSet](#asset-initialization)
+//# - a [SharedSet](#sharedset-initialization)
 
 union BeaconStyle {
   partOnly: PartOnly,
@@ -581,8 +581,8 @@ union BeaconStyle {
 //= specification/searchable-encryption/beacons.md#encrypted-part-initialization
 //= type=implication
 //# On initialization of a [encrypted part](#encrypted-part-initialization), the caller MUST provide:
-//#  * A name -- a string, the name of a standard beacon
-//#  * A prefix -- a string
+//# - A name -- a string, the name of a standard beacon
+//# - A prefix -- a string
 
 @javadoc("A part of a Compound Beacon that contains a beacon over encrypted data.")
 structure EncryptedPart {
@@ -597,8 +597,8 @@ structure EncryptedPart {
 //= specification/searchable-encryption/beacons.md#signed-part-initialization
 //= type=implication
 //# On initialization of a [signed part](#signed-part-initialization), the caller MUST provide:
-//#  * A name -- a string
-//#  * A prefix -- a string
+//# - A name -- a string
+//# - A prefix -- a string
 
 //= specification/searchable-encryption/beacons.md#signed-part-initialization
 //= type=implication
@@ -620,7 +620,7 @@ structure SignedPart {
 //= specification/searchable-encryption/beacons.md#constructor-initialization
 //= type=implication
 //# On initialization of a constructor, the caller MUST provide:
-//# * A non-empty list of [Constructor parts](#constructor-part-initialization)
+//# - A non-empty list of [Constructor parts](#constructor-part-initialization)
 
 @javadoc("The configuration for a particular Compound Beacon construction.")
 structure Constructor {
@@ -632,8 +632,8 @@ structure Constructor {
 //= specification/searchable-encryption/beacons.md#constructor-part-initialization
 //= type=implication
 //# On initialization of a constructor part, the caller MUST provide:
-//#  * A name -- a string
-//#  * A required flag -- a boolean
+//# - A name -- a string
+//# - A required flag -- a boolean
 
 @javadoc("A part of a Compound Becaon Construction.")
 structure ConstructorPart {
@@ -648,13 +648,13 @@ structure ConstructorPart {
 //= specification/searchable-encryption/beacons.md#standard-beacon-initialization
 //= type=implication
 //# On initialization of a Standard Beacon, the caller MUST provide:
-//#  * A name -- a string
-//#  * A `length` -- a [beacon length](#beacon-length)
+//# - A name -- a string
+//# - A `length` -- a [beacon length](#beacon-length)
 
 //= specification/searchable-encryption/beacons.md#standard-beacon-initialization
 //= type=implication
 //# On initialization of a Standard Beacon, the caller MAY provide:
-//# * a [terminal location](virtual.md#terminal-location) -- a string
+//# - a [terminal location](virtual.md#terminal-location) -- a string
 
 @javadoc("The configuration for a Standard Beacon.")
 structure StandardBeacon {
@@ -673,15 +673,15 @@ structure StandardBeacon {
 //= specification/searchable-encryption/beacons.md#compound-beacon-initialization
 //= type=implication
 //# On initialization of a Compound Beacon, the caller MUST provide:
-//#  * A name -- a string
-//#  * A split character -- a character
+//# - A name -- a string
+//# - A split character -- a character
 
 //= specification/searchable-encryption/beacons.md#compound-beacon-initialization
 //= type=implication
 //# On initialization of a Compound Beacon, the caller MAY provide:
-//#  * A list of [encrypted parts](#encrypted-part-initialization)
-//#  * A list of [signed parts](#signed-part-initialization)
-//#  * A list of constructors
+//# - A list of [encrypted parts](#encrypted-part-initialization)
+//# - A list of [signed parts](#signed-part-initialization)
+//# - A list of constructors
 
 @javadoc("The configuration for a Compound Beacon.")
 structure CompoundBeacon {
@@ -740,8 +740,8 @@ structure MultiKeyStore {
 //= specification/searchable-encryption/search-config.md#beacon-key-source
 //= type=implication
 //# On initialization of a Beacon Key Source, the caller MUST provide exactly one of
-//#  * a [Single Key Store](#single-key-store-initialization)
-//#  * a [Multi Key Store](#multi-key-store-initialization)
+//# - a [Single Key Store](#single-key-store-initialization)
+//# - a [Multi Key Store](#multi-key-store-initialization)
 
 union BeaconKeySource {
   single : SingleKeyStore,
@@ -791,8 +791,8 @@ structure BeaconVersion {
 //= specification/searchable-encryption/search-config.md#initialization
 //= type=implication
 //# On initialization of the Search Config, the caller MUST provide:
-//#  - A list of [beacon versions](#beacon-version-initialization)
-//#  - The [version number](#version-number) of the [beacon versions](#beacon-version) to be used for writing.
+//# - A list of [beacon versions](#beacon-version-initialization)
+//# - The [version number](#version-number) of the [beacon versions](#beacon-version-initialization) to be used for writing.
 
 @javadoc("The configuration for searchable encryption.")
 structure SearchConfig {
@@ -855,7 +855,7 @@ operation CreateDynamoDbEncryptionBranchKeyIdSupplier {
 
 //= specification/dynamodb-encryption-client/ddb-encryption-branch-key-id-supplier.md#input
 //= type=implication
-//# This operation MUST take in a [DynamoDbKeyBranchKeyIdSupplier](#dynamodb-key-branch-key-id-supplier) as input.
+//# This operation MUST take in a [DynamoDbKeyBranchKeyIdSupplier](#dynamodbkeybranchkeyidsupplier) as input.
 @javadoc("Inputs for creating a Branch Key Supplier from a DynamoDB Key Branch Key Id Supplier")
 structure CreateDynamoDbEncryptionBranchKeyIdSupplierInput {
   @required

DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy

@@ -48,7 +48,7 @@ module SearchConfigToInfo {
 
     //= specification/searchable-encryption/search-config.md#initialization
     //= type=implication
-    //# Initialization MUST fail if the length of the list of [beacon versions](#beacon-version) is not 1.
+    //# Initialization MUST fail if the length of the list of [beacon versions](#beacon-version-initialization) is not 1.
     ensures outer.search.Some? && |outer.search.value.versions| != 1 ==> output.Failure?
   {
     if outer.search.None? {
@@ -738,7 +738,7 @@ module SearchConfigToInfo {
 
     //= specification/searchable-encryption/beacons.md#initialization-failure
     //= type=implication
-    //# Initialization MUST fail if any [constructor](#constructor) is configured with a field name
+    //# Initialization MUST fail if any [constructor](#constructor-initialization) is configured with a field name
     //# that is not a defined [part](#part).
     ensures ret.Success? && 0 < |c| ==>
               exists p : CB.BeaconPart | p in parts :: p.getName() == c[0].name
@@ -773,14 +773,14 @@ module SearchConfigToInfo {
     ensures ret.Success? ==> |ret.value| == origSize
     //= specification/searchable-encryption/beacons.md#initialization-failure
     //= type=implication
-    //# Initialization MUST fail if any [constructor](#constructor) is configured without at least one
+    //# Initialization MUST fail if any [constructor](#constructor-initialization) is configured without at least one
     //# required part.
     ensures ret.Success? && 0 < |constructors| ==>
               0 < SeqCount((p : ConstructorPart) => p.required, constructors[0].parts)
 
     //= specification/searchable-encryption/beacons.md#initialization-failure
     //= type=implication
-    //# Initialization MUST fail if two [constructors](#constructor) are configured
+    //# Initialization MUST fail if two [constructors](#constructor-initialization) are configured
     //# with the same set of required parts.
     ensures ret.Success? && 0 < |constructors| ==>
               && MakeConstructor(constructors[0], parts).Success?

DynamoDbEncryption/dafny/DynamoDbEncryption/src/DynamoToStruct.dfy

@@ -21,16 +21,12 @@ module DynamoToStruct {
 
   type Error = AwsCryptographyDbEncryptionSdkDynamoDbTypes.Error
 
-  type StructuredDataTerminalType = x : StructuredData | x.content.Terminal? witness *
-  type TerminalDataMap = map<AttributeName, StructuredDataTerminalType>
+  type TerminalDataMap = map<AttributeName, StructuredDataTerminal>
 
   // This file exists for these two functions : ItemToStructured and StructuredToItem
   // which provide conversion between an AttributeMap and a StructuredDataMap
 
   // Convert AttributeMap to StructuredDataMap
-  //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
-  //= type=implication
-  //# - MUST be a [Structured Data Map](../structured-encryption/structures.md#structured-data-map).
   function method {:opaque} ItemToStructured(item : AttributeMap) : (ret : Result<TerminalDataMap, Error>)
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
@@ -39,30 +35,19 @@ module DynamoToStruct {
     //# for each attribute on the DynamoDB Item, and no others.
     ensures ret.Success? ==> ret.value.Keys == item.Keys
 
-    //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
-    //= type=implication
-    //# - MUST NOT have [Structured Data Attributes](../structured-encryption/structures.md#structured-data-attributes).
-    ensures ret.Success? ==> forall v <- ret.value.Values :: v.content.Terminal?
-
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
     //= type=implication
     //# - The [Terminal Type ID](../structured-encryption/structures.md#terminal-type-id) for each attribute MUST
     //# be the [Type ID](./ddb-attribute-serialization.md#type-id) of the [serialization](./ddb-attribute-serialization.md) of this Attribute Value.
-    ensures ret.Success? ==> forall kv <- ret.value.Items :: kv.1.content.Terminal.typeId == AttrToTypeId(item[kv.0])
-
-    //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
-    //= type=implication
-    //# - The Structured Data Terminal MUST be located at the top level of the Structured Data,
-    //# string indexed by the Attribute Name.
-    ensures ret.Success? ==> forall kv <- ret.value.Items :: kv.0 in ret.value.Keys && ret.value[kv.0].content.Terminal?
+    ensures ret.Success? ==> forall kv <- ret.value.Items :: kv.1.typeId == AttrToTypeId(item[kv.0])
 
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-ddb-item-to-structured-data
     //= type=implication
     //# - The [Terminal Value](../structured-encryption/structures.md#terminal-value) for each attribute MUST
     //# be the [Value](./ddb-attribute-serialization.md#type-id) of the [serialization](./ddb-attribute-serialization.md) of this Attribute Value.
     ensures ret.Success? ==> forall kv <- ret.value.Items ::
                 && TopLevelAttributeToBytes(item[kv.0]).Success?
-                && kv.1.content.Terminal.value == TopLevelAttributeToBytes(item[kv.0]).value
+                && kv.1.value == TopLevelAttributeToBytes(item[kv.0]).value
 
   {
     var structuredMap := map k <- item :: k := AttrToStructured(item[k]);
@@ -71,10 +56,7 @@ module DynamoToStruct {
   }
 
   // Convert StructuredDataMap to AttributeMap
-  //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-structured-data-to-ddb-item
-  //= type=implication
-  //# - MUST be a [Structured Data Map](../structured-encryption/structures.md#structured-data-map).
-  function method {:opaque} StructuredToItem(s : StructuredDataMap) : (ret : Result<AttributeMap, Error>)
+  function method {:opaque} StructuredToItem(s : TerminalDataMap) : (ret : Result<AttributeMap, Error>)
     //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-structured-data-to-ddb-item
     //= type=implication
     //# - MUST contain an Attribute for every [Structured Data Terminal](../structured-encryption/structures.md#structured-data-terminal)
@@ -125,12 +107,12 @@ module DynamoToStruct {
   }
 
   // Prove round trip. A work in progress
-  lemma RoundTripFromStructured(s : StructuredData)
-    ensures  StructuredToAttr(s).Success? && s.content.Terminal.typeId == SE.BINARY ==>
+  lemma RoundTripFromStructured(s : StructuredDataTerminal)
+    ensures  StructuredToAttr(s).Success? && s.typeId == SE.BINARY ==>
                && AttrToStructured(StructuredToAttr(s).value).Success?
-    ensures  StructuredToAttr(s).Success? && s.content.Terminal.typeId == SE.BOOLEAN ==>
+    ensures  StructuredToAttr(s).Success? && s.typeId == SE.BOOLEAN ==>
                && AttrToStructured(StructuredToAttr(s).value).Success?
-    ensures  StructuredToAttr(s).Success? && s.content.Terminal.typeId == SE.NULL ==>
+    ensures  StructuredToAttr(s).Success? && s.typeId == SE.NULL ==>
                && AttrToStructured(StructuredToAttr(s).value).Success?
   {
     reveal AttrToStructured();
@@ -161,34 +143,18 @@ module DynamoToStruct {
     AttrToBytes(a, false)
   }
 
-  function method  {:opaque} AttrToStructured(item : AttributeValue) : (ret : Result<StructuredData, string>)
-    ensures ret.Success? ==> ret.value.content.Terminal?
-    ensures ret.Success? ==> ret.value.content.Terminal.typeId == AttrToTypeId(item)
+  function method  {:opaque} AttrToStructured(item : AttributeValue) : (ret : Result<StructuredDataTerminal, string>)
+    ensures ret.Success? ==> ret.value.typeId == AttrToTypeId(item)
     ensures ret.Success? ==>
               && TopLevelAttributeToBytes(item).Success?
-              && ret.value.content.Terminal.value == TopLevelAttributeToBytes(item).value
+              && ret.value.value == TopLevelAttributeToBytes(item).value
   {
     var body :- TopLevelAttributeToBytes(item);
-    Success(StructuredData(content := Terminal(StructuredDataTerminal(value := body, typeId := AttrToTypeId(item))), attributes := None))
+    Success(StructuredDataTerminal(value := body, typeId := AttrToTypeId(item)))
   }
 
-  function method  {:opaque} StructuredToAttr(s : StructuredData) : (ret : Result<AttributeValue, string>)
-    //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-structured-data-to-ddb-item
-    //= type=implication
-    //# - This [Structured Data Map](../structured-encryption/structures.md#structured-data-map),
-    //# if not empty,
-    //# MUST only contain [Structured Data Terminals](../structured-encryption/structures.md#structured-data-terminal).
-    ensures ret.Success? ==> s.content.Terminal?
-
-    //= specification/dynamodb-encryption-client/ddb-item-conversion.md#convert-structured-data-to-ddb-item
-    //= type=implication
-    //# - MUST NOT have [Structured Data Attributes](../structured-encryption/structures.md#structured-data-attributes).
-    ensures ret.Success? ==> s.attributes.None?
+  function method  {:opaque} StructuredToAttr(s : StructuredDataTerminal) : (ret : Result<AttributeValue, string>)
   {
-    :- Need(s.attributes.None?, "attributes must be None");
-    :- Need(s.content.Terminal?, "StructuredData to AttributeValue only works on Terminal data");
-
-    var Terminal(s) := s.content;
     :- Need(|s.typeId| == 2, "Type ID must be two bytes");
     var attrValueAndLength :- BytesToAttr(s.value, s.typeId, false);
     :- Need(attrValueAndLength.len == |s.value|, "Mismatch between length of encoded data and length of data");