feat: Global Parts List

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -44,7 +44,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  nameonly keySource: BeaconKeySource ,
  nameonly standardBeacons: StandardBeaconList ,
  nameonly compoundBeacons: Option<CompoundBeaconList> ,
- nameonly virtualFields: Option<VirtualFieldList>
+ nameonly virtualFields: Option<VirtualFieldList> ,
+ nameonly encryptedParts: Option<EncryptedPartsList> ,
+ nameonly signedParts: Option<SignedPartsList>
  )
  type BeaconVersionList = x: seq<BeaconVersion> | IsValid_BeaconVersionList(x) witness *
  predicate method IsValid_BeaconVersionList(x: seq<BeaconVersion>) {

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -722,6 +722,11 @@ structure BeaconVersion {
   compoundBeacons : CompoundBeaconList,
   @javadoc("The Virtual Fields to be calculated, supporting other searchable enryption configurations.")
   virtualFields : VirtualFieldList,
+
+  @javadoc("The list of Encrypted Parts that may be included in any compound beacon.")
+  encryptedParts : EncryptedPartsList,
+  @javadoc("The list of Signed Parts that may be included in any compound beacon.")
+  signedParts : SignedPartsList,
 }
 
 //= specification/searchable-encryption/search-config.md#initialization

DynamoDbEncryption/dafny/DynamoDbEncryption/src/Beacon.dfy

@@ -194,7 +194,6 @@ module BaseBeacon {
     }
 
     function method {:opaque} ValueToSet(value : DDB.AttributeValue, key : Bytes) : (ret : Result<DDB.AttributeValue, Error>)
-      requires asSet
       ensures ret.Success? ==> ret.value.SS?
       ensures !value.SS? && !value.NS? && !value.BS? ==> ret.Failure?
       ensures ret.Success? ==> HasNoDuplicates(ret.value.SS)
@@ -241,11 +240,20 @@ module BaseBeacon {
         //= type=implication
         //# * The resulting set MUST NOT contain duplicates.
         && (ret.value.Some? ==> HasNoDuplicates(ret.value.value.SS))
+        //= specification/searchable-encryption/beacons.md#asset-initialization
+        //= type=implication
+        //# * Writing an item MUST fail if the item contains this beacon's attribute,
+        //# and that attribute is not of type Set.
+        && var value := TermLoc.TermToAttr(loc, item, None);
+        && (value.Some? && !(value.value.SS? || value.value.NS? || value.value.BS?) ==> ret.Failure?)
     {
         var value := TermLoc.TermToAttr(loc, item, None);
         if value.None? then
           Success(None)
         else
+          //= specification/searchable-encryption/beacons.md#asset-initialization
+          //# * The Standard Beacon MUST be stored in the item as a Set,
+          //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set.
           var setValue :- ValueToSet(value.value, key);
           Success(Some(setValue))
     }
@@ -346,18 +354,13 @@ module BaseBeacon {
           BeaconizeBinarySet(value[1..], key, converted + [h])
     }
 
-    function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes)
+    function method GetBeaconValue(value : DDB.AttributeValue, key : Bytes, forContains : bool)
       : (ret : Result<DDB.AttributeValue, Error>)
-      //= specification/searchable-encryption/beacons.md#asset-initialization
-      //= type=implication
-      //# * Writing an item MUST fail if the item contains this beacon's attribute,
-      //# and that attribute is not of type Set.
-      ensures asSet && !value.SS? && !value.NS? && !value.BS? ==> ret.Failure?
     {
-      //= specification/searchable-encryption/beacons.md#asset-initialization
-      //# * The Standard Beacon MUST be stored in the item as a Set,
-      //# comprised of the [beacon values](#beacon-value) of all the elements in the original Set.
-      if asSet then
+      // in query, allow beaconization of terminals
+      if asSet && !value.S? && !value.N? && !value.B? then
+        ValueToSet(value, key)
+      else if forContains && (value.SS? || value.NS? || value.BS?) then
         ValueToSet(value, key)
       else
         var bytes :- DynamoToStruct.TopLevelAttributeToBytes(value).MapFailure(e => E(e));