feat: smithy for virtual fields (#71)

* feat: smithy for virtual fields

* use union for Transform

* zero-based plus GetSegments

Author: ajewellamz

DynamoDbEncryptionMiddlewareInternal/Model/AwsCryptographyDynamoDbEncryptionTypes.dfy

@@ -67,7 +67,8 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
  nameonly version: VersionNumber ,
  nameonly keyring: AwsCryptographyMaterialProvidersTypes.IKeyring ,
  nameonly standardBeacons: Option<StandardBeaconList> ,
- nameonly compoundBeacons: Option<CompoundBeaconList>
+ nameonly compoundBeacons: Option<CompoundBeaconList> ,
+ nameonly virtualFields: Option<VirtualFieldList>
  )
  type BeaconVersionList = x: seq<BeaconVersion> | IsValid_BeaconVersionList(x) witness *
  predicate method IsValid_BeaconVersionList(x: seq<BeaconVersion>) {
@@ -771,6 +772,31 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
  )
  datatype GetItemOutputTransformOutput = | GetItemOutputTransformOutput (
  nameonly transformedOutput: ComAmazonawsDynamodbTypes.GetItemOutput
+ )
+ datatype GetPrefix = | GetPrefix (
+ nameonly length: int32
+ )
+ datatype GetSegment = | GetSegment (
+ nameonly split: Char ,
+ nameonly index: int32
+ )
+ datatype GetSegments = | GetSegments (
+ nameonly split: Char ,
+ nameonly low: int32 ,
+ nameonly high: int32
+ )
+ datatype GetSubstring = | GetSubstring (
+ nameonly low: int32 ,
+ nameonly high: int32
+ )
+ datatype GetSuffix = | GetSuffix (
+ nameonly length: int32
+ )
+ datatype Insert = | Insert (
+ nameonly literal: string
+ )
+ datatype Lower = | Lower (
+ 
  )
  datatype NonSensitivePart = | NonSensitivePart (
  nameonly name: string ,
@@ -902,10 +928,42 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
  )
  datatype UpdateTableOutputTransformOutput = | UpdateTableOutputTransformOutput (
  nameonly transformedOutput: ComAmazonawsDynamodbTypes.UpdateTableOutput
+ )
+ datatype Upper = | Upper (
+ 
  )
  type VersionNumber = x: int32 | IsValid_VersionNumber(x) witness *
  predicate method IsValid_VersionNumber(x: int32) {
  ( 1 <= x  )
+}
+ datatype VirtualField = | VirtualField (
+ nameonly name: string ,
+ nameonly parts: VirtualPartList
+ )
+ type VirtualFieldList = x: seq<VirtualField> | IsValid_VirtualFieldList(x) witness *
+ predicate method IsValid_VirtualFieldList(x: seq<VirtualField>) {
+ ( 1 <= |x|  )
+}
+ datatype VirtualPart = | VirtualPart (
+ nameonly loc: TerminalLocation ,
+ nameonly trans: Option<VirtualTransformList>
+ )
+ type VirtualPartList = x: seq<VirtualPart> | IsValid_VirtualPartList(x) witness *
+ predicate method IsValid_VirtualPartList(x: seq<VirtualPart>) {
+ ( 1 <= |x|  )
+}
+ datatype VirtualTransform =
+ | upper(upper: Upper)
+ | lower(lower: Lower)
+ | insert(insert: Insert)
+ | prefix(prefix: GetPrefix)
+ | suffix(suffix: GetSuffix)
+ | substring(substring: GetSubstring)
+ | segment(segment: GetSegment)
+ | segments(segments: GetSegments)
+ type VirtualTransformList = x: seq<VirtualTransform> | IsValid_VirtualTransformList(x) witness *
+ predicate method IsValid_VirtualTransformList(x: seq<VirtualTransform>) {
+ ( 1 <= |x|  )
 }
  datatype Error =
  // Local Error structures are listed here
@@ -955,7 +1013,9 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
  function method DefaultDynamoDbEncryptionConfig(): DynamoDbEncryptionConfig
  method DynamoDbEncryption(config: DynamoDbEncryptionConfig := DefaultDynamoDbEncryptionConfig())
  returns (res: Result<DynamoDbEncryptionClient, Error>)
-// TODO smithy->Dafny needs to generate the following
+ // TODO smithy->Dafny correctly generates something equivalent the following
+ // but as a result DynamoDbEncryption.DynamoDbEncryption and TestFixtures.GetDynamoDbEncryption
+ // take too long to verify
 ///// MANUAL UPDATE STARTS HERE
 requires
 var cmms := set cfg | cfg in config.tableEncryptionConfigs.Values && cfg.cmm.Some? :: cfg.cmm.value;

DynamoDbEncryptionMiddlewareInternal/Model/DynamoDbEncryptionMiddlewareInternal.smithy

@@ -124,6 +124,21 @@ list BeaconVersionList {
   member: BeaconVersion
 }
 
+@length(min: 1)
+list VirtualFieldList {
+  member: VirtualField
+}
+
+@length(min: 1)
+list VirtualPartList {
+  member: VirtualPart
+}
+
+@length(min: 1)
+list VirtualTransformList {
+  member: VirtualTransform
+}
+
 @length(min: 1)
 list StandardBeaconList {
   member: StandardBeacon
@@ -154,6 +169,93 @@ list ConstructorPartList {
   member: ConstructorPart
 }
 
+structure VirtualField {
+  @required
+  name : String,
+  @required
+  parts : VirtualPartList,
+}
+
+structure VirtualPart {
+  @required
+  loc : TerminalLocation,
+  trans : VirtualTransformList,
+}
+
+// Convert ASCII characters to upper case
+structure Upper {}
+
+// Convert ASCII characters to lower case
+structure Lower {}
+
+// Append this literal string
+structure Insert {
+  @required
+  literal : String
+}
+
+// return the first part of the string
+// Positive length : return that many characters from the front
+// Negative length : exclude -length characters from the end
+// e.g. GetPrefix(-1) returns all but the last character
+structure GetPrefix {
+  @required
+  length : Integer
+}
+
+// return the last part of the string
+// Positive length : return that many characters from the end
+// Negative length : exclude -length characters from the front
+// e.g. GetSuffix(-1) returns all but the first character
+structure GetSuffix {
+  @required
+  length : Integer
+}
+
+// return range of characters, 0-based counting
+// low is inclusive, high is exclusive
+// negative numbers count from the end, -1 is the end of string
+// i.e. the whole string is GetSubstring(0, -1)
+// e.g. for "123456789"
+// GetSubstring(2, 6) == GetSubstring(2, -4) == "3456"
+structure GetSubstring {
+  @required
+  low : Integer,
+  @required
+  high : Integer,
+}
+
+// split string on character, then return one piece.
+// 'index' has the same semantics as 'low' in GetSubstring
+structure GetSegment {
+  @required
+  split : Char,
+  @required
+  index : Integer
+}
+
+// split string on character, then return range of pieces.
+// 'low' and 'high' have the same semantics as GetSubstring
+structure GetSegments {
+  @required
+  split : Char,
+  @required
+  low : Integer,
+  @required
+  high : Integer,
+}
+
+union VirtualTransform {
+  upper: Upper,
+  lower: Lower,
+  insert: Insert,
+  prefix: GetPrefix,
+  suffix: GetSuffix,
+  substring : GetSubstring,
+  segment : GetSegment,
+  segments : GetSegments
+}
+
 structure SensitivePart {
   @required
   name : String,
@@ -210,6 +312,7 @@ structure BeaconVersion {
   keyring: KeyringReference, // Must be Hierarchy Keyring
   standardBeacons : StandardBeaconList,
   compoundBeacons : CompoundBeaconList,
+  virtualFields : VirtualFieldList,
 }
 
 structure SearchConfig {