feat: implement beacon styles (#441)

* feat: implement beacon styles

Author: ajewellamz

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy

@@ -22,6 +22,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
 
  // Begin Generated Types
 
+ datatype AsSet = | AsSet (
+ 
+ )
  type AttributeActions = map<ComAmazonawsDynamodbTypes.AttributeName, AwsCryptographyDbEncryptionSdkStructuredEncryptionTypes.CryptoAction>
  type BeaconBitLength = x: int32 | IsValid_BeaconBitLength(x) witness *
  predicate method IsValid_BeaconBitLength(x: int32) {
@@ -30,6 +33,11 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype BeaconKeySource =
  | single(single: SingleKeyStore)
  | multi(multi: MultiKeyStore)
+ datatype BeaconStyle =
+ | partOnly(partOnly: PartOnly)
+ | twinned(twinned: Twinned)
+ | asSet(asSet: AsSet)
+ | twinnedSet(twinnedSet: TwinnedSet)
  datatype BeaconVersion = | BeaconVersion (
  nameonly version: VersionNumber ,
  nameonly keyStore: AwsCryptographyKeyStoreTypes.IKeyStoreClient ,
@@ -310,6 +318,9 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  nameonly keyFieldName: string ,
  nameonly cacheTTL: int32 ,
  nameonly cache: Option<AwsCryptographyMaterialProvidersTypes.CacheType>
+ )
+ datatype PartOnly = | PartOnly (
+ 
  )
  datatype PlaintextOverride =
 	| FORCE_PLAINTEXT_WRITE_ALLOW_PLAINTEXT_READ
@@ -339,7 +350,8 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  datatype StandardBeacon = | StandardBeacon (
  nameonly name: string ,
  nameonly length: BeaconBitLength ,
- nameonly loc: Option<TerminalLocation>
+ nameonly loc: Option<TerminalLocation> ,
+ nameonly style: Option<BeaconStyle>
  )
  type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
  predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {
@@ -349,6 +361,12 @@ include "../../../../submodules/MaterialProviders/StandardLibrary/src/Index.dfy"
  predicate method IsValid_TerminalLocation(x: string) {
  ( 1 <= |x|  )
 }
+ datatype Twinned = | Twinned (
+ nameonly other: string
+ )
+ datatype TwinnedSet = | TwinnedSet (
+ nameonly other: string
+ )
  datatype Upper = | Upper (
 
  )

DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy

@@ -465,6 +465,60 @@ union VirtualTransform {
   segments : GetSegments
 }
 
+//= specification/searchable-encryption/beacons.md#partonly-initialization
+//= type=implication
+//# On initialization of a PartOnly, the caller MUST NOT provide any
+//# additional parameters to the PartOnly.
+@javadoc("Attribute must be used as part of a Compound Beacon, never alone.")
+structure PartOnly {}
+
+//= specification/searchable-encryption/beacons.md#asset-initialization
+//= type=implication
+//# On initialization of as AsSet, the caller MUST NOT provide any
+//# additional parameters to the AsSet.
+@javadoc("Attribute must be a Set. Beacon value will also be a Set.")
+structure AsSet {}
+
+//= specification/searchable-encryption/beacons.md#twinned-initialization
+//= type=implication
+//# On initialization of a Twinned, the caller MUST provide:
+//#
+//# * other : a beacon name
+@javadoc("This beacon should calculate values like another beacon, so they can be compared.")
+structure Twinned {
+  @required
+  @javadoc("Calculate beacon values as for this beacon.")
+  other : String,
+}
+
+//= specification/searchable-encryption/beacons.md#twinnedset-initialization
+//= type=implication
+//# On initialization of a TwinnedSet, the caller MUST provide:
+//#
+//# * other : a beacon name
+@javadoc("Both Twinned and AsSet.")
+structure TwinnedSet {
+  @required
+  @javadoc("Calculate beacon values as for this beacon.")
+  other : String,
+}
+
+//= specification/searchable-encryption/beacons.md#beacon-style-initialization
+//= type=implication
+//# On initialization of a Beacon Style, the caller MUST provide exactly one of
+//# 
+//#  * a [PartOnly](#partonly-initialization)
+//#  * a [Twinned](#twinned-initialization)
+//#  * an [AsSet](#asset-initialization)
+//#  * a [TwinnedSet](#twinnedset-initialization)
+
+union BeaconStyle {
+  partOnly: PartOnly,
+  twinned: Twinned,
+  asSet: AsSet,
+  twinnedSet: TwinnedSet,
+}
+
 //= specification/searchable-encryption/beacons.md#encrypted-part-initialization
 //= type=implication
 //# On initialization of a [encrypted part](#encrypted-part-initialization), the caller MUST provide:
@@ -552,7 +606,9 @@ structure StandardBeacon {
   @javadoc("The length of the calculated beacon.")
   length : BeaconBitLength,
   @javadoc("The DynamoDB document path to the value this beacon will calculate over. If not specified, the beacon will calculate values for the attribute with the name specified in 'name'.")
-  loc : TerminalLocation
+  loc : TerminalLocation,
+  @javadoc("Optional augmented behavior.")
+  style : BeaconStyle,
 }
 
 //= specification/searchable-encryption/beacons.md#compound-beacon-initialization