Skip to content

feat: smithy for virtual fields #71

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Merged
merged 8 commits into from
Mar 27, 2023
Merged

feat: smithy for virtual fields #71

Show file tree
Hide file tree
Changes from 1 commit
Commits
Show all changes
8 commits
Select commit Hold shift + click to select a range
54ad3b9
feat: smithy for virtual fields
ajewellamz Mar 24, 2023
c612c97
use union for Transform
ajewellamz Mar 25, 2023
f01e3e4
m
ajewellamz Mar 25, 2023
60c3f68
m
ajewellamz Mar 25, 2023
e882e1b
PR feedback
ajewellamz Mar 27, 2023
61a60ca
zero-based plus GetSegments
ajewellamz Mar 27, 2023
91243ad
m
ajewellamz Mar 27, 2023
d28b4d2
m
ajewellamz Mar 27, 2023
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
41 changes: 41 additions & 0 deletions DynamoDbEncryptionMiddlewareInternal/Model/AwsCryptographyDynamoDbEncryptionTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -780,6 +780,10 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
type NonSensitivePartsList = x: seq<NonSensitivePart> | IsValid_NonSensitivePartsList(x) witness *
predicate method IsValid_NonSensitivePartsList(x: seq<NonSensitivePart>) {
( 1 <= |x| )
}
type NumberList = x: seq<int32> | IsValid_NumberList(x) witness *
predicate method IsValid_NumberList(x: seq<int32>) {
( 1 <= |x| )
}
type Prefix = x: string | IsValid_Prefix(x) witness *
predicate method IsValid_Prefix(x: string) {
Expand Down Expand Up @@ -846,6 +850,10 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
type StandardBeaconList = x: seq<StandardBeacon> | IsValid_StandardBeaconList(x) witness *
predicate method IsValid_StandardBeaconList(x: seq<StandardBeacon>) {
( 1 <= |x| )
}
type StringList = x: seq<string> | IsValid_StringList(x) witness *
predicate method IsValid_StringList(x: seq<string>) {
( 1 <= |x| )
}
type TerminalLocation = x: string | IsValid_TerminalLocation(x) witness *
predicate method IsValid_TerminalLocation(x: string) {
Expand Down Expand Up @@ -877,6 +885,14 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
datatype TransactWriteItemsOutputTransformOutput = | TransactWriteItemsOutputTransformOutput (
nameonly transformedOutput: ComAmazonawsDynamodbTypes.TransactWriteItemsOutput
)
datatype Transform =
| LOWER
| UPPER
| INSERT
| PREFIX
| SUFFIX
| SUBSTRING
| SEGMENT
datatype UpdateItemInputTransformInput = | UpdateItemInputTransformInput (
nameonly sdkInput: ComAmazonawsDynamodbTypes.UpdateItemInput
)
Expand Down Expand Up @@ -906,6 +922,31 @@ include "../../private-aws-encryption-sdk-dafny-staging/StandardLibrary/src/Inde
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 = | VirtualTransform (
nameonly transform: Transform ,
nameonly numbers: Option<NumberList> ,
nameonly strings: Option<StringList>
)
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
Expand Down
78 changes: 78 additions & 0 deletions DynamoDbEncryptionMiddlewareInternal/Model/DynamoDbEncryptionMiddlewareInternal.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -124,6 +124,31 @@ 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 StringList {
member: String
}

@length(min: 1)
list NumberList {
member: Integer
}

@length(min: 1)
list StandardBeaconList {
member: StandardBeacon
Expand Down Expand Up @@ -154,6 +179,59 @@ list ConstructorPartList {
member: ConstructorPart
}

structure VirtualField {
@required
name : String,
@required
parts : VirtualPartList,
}

structure VirtualPart {
@required
loc : TerminalLocation,
trans : VirtualTransformList,
}

@enum([
{
name: "LOWER",
value: "Lower"
},
{
name: "UPPER",
value: "Upper"
},
{
name: "INSERT",
value: "Insert"
},
{
name: "PREFIX",
value: "Prefix"
},
{
name: "SUFFIX",
value: "Suffix"
},
{
name: "SUBSTRING",
value: "Substring"
},
{
name: "SEGMENT",
value: "Segment"
},
])
string Transform

structure VirtualTransform {
@required
transform : Transform,
numbers : NumberList,
strings : StringList,
}
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The other way to model this would be via a union:

union Transform {
  upper: Upper(),
  lower: Lower(),
  insert: Insert(string str),
  prefix: Prefix(int len),
  suffix: Suffix(int len),
  substring: Substring(int start, int end),
  ...
  
}

I think this is the more "correct" way to model this, as we can exactly express the inputs to each transform.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I agree completely.



structure SensitivePart {
@required
name : String,
Expand Down
Loading