Skip to content

feat: implement beacon styles #441

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 6 commits into from
Sep 22, 2023
Merged

feat: implement beacon styles #441

Show file tree
Hide file tree
Changes from 5 commits
Commits
Show all changes
6 commits
Select commit Hold shift + click to select a range
bec4194
feat: implement beacon styles
ajewellamz Sep 21, 2023
14652ab
m
ajewellamz Sep 21, 2023
fe66f4a
m
ajewellamz Sep 21, 2023
e8e7928
respond to PR feedback
ajewellamz Sep 21, 2023
6c67bba
update spec
ajewellamz Sep 22, 2023
ae3e691
m
ajewellamz Sep 22, 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
20 changes: 19 additions & 1 deletion ...Encryption/dafny/DynamoDbEncryption/Model/AwsCryptographyDbEncryptionSdkDynamoDbTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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) {
Expand All @@ -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 ,
Expand Down Expand Up @@ -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
Expand Down Expand Up @@ -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>) {
Expand All @@ -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 (

)
Expand Down
58 changes: 57 additions & 1 deletion DynamoDbEncryption/dafny/DynamoDbEncryption/Model/DynamoDbEncryption.smithy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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:
Expand Down Expand Up @@ -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
Expand Down
Loading