Skip to content
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.

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

chore: Fix nightly build (aside from verification) #1029

Merged
merged 16 commits into from
Jun 4, 2024
Merged
Show file tree
Hide file tree
Changes from all commits
Commits
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
1 change: 1 addition & 0 deletions .github/actions/polymorph_codegen/action.yml
Original file line number Diff line number Diff line change
Expand Up @@ -116,6 +116,7 @@ runs:
make -C submodules/MaterialProviders/AwsCryptographicMaterialProviders setup_prettier
make -C submodules/MaterialProviders/ComAmazonawsKms setup_prettier
make -C submodules/MaterialProviders/ComAmazonawsDynamodb setup_prettier
make -C submodules/MaterialProviders/TestVectorsAwsCryptographicMaterialProviders setup_prettier

- name: Regenerate Java code using smithy-dafny
# npx seems to be unavailable on Windows GHA runners,
Expand Down
9 changes: 9 additions & 0 deletions .github/workflows/ci_examples_java.yml
Original file line number Diff line number Diff line change
Expand Up @@ -60,6 +60,15 @@ jobs:
# A && B || C is the closest thing to an if .. then ... else ... or ?: expression the GitHub Actions syntax supports.
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}

- name: Regenerate code using smithy-dafny if necessary
if: ${{ github.event_name == 'schedule' || inputs.nightly }}
uses: ./.github/actions/polymorph_codegen
with:
dafny: ${{ env.DAFNY_VERSION }}
library: DynamoDbEncryption
diff-generated-code: false
update-and-regenerate-mpl: true

- name: Build and locally deploy dependencies for examples
shell: bash
working-directory: ./DynamoDbEncryption
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci_test_java.yml
Original file line number Diff line number Diff line change
Expand Up @@ -55,7 +55,7 @@ jobs:
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}

- name: Regenerate code using smithy-dafny if necessary
if: ${{ inputs.nightly }}
if: ${{ github.event_name == 'schedule' || inputs.nightly }}
uses: ./.github/actions/polymorph_codegen
with:
dafny: ${{ env.DAFNY_VERSION }}
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci_test_net.yml
Original file line number Diff line number Diff line change
Expand Up @@ -60,7 +60,7 @@ jobs:
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.2.0' }}

- name: Regenerate code using smithy-dafny if necessary
if: ${{ inputs.nightly }}
if: ${{ github.event_name == 'schedule' || inputs.nightly }}
uses: ./.github/actions/polymorph_codegen
with:
dafny: ${{ env.DAFNY_VERSION }}
Expand Down
2 changes: 1 addition & 1 deletion .github/workflows/ci_verification.yml
Original file line number Diff line number Diff line change
Expand Up @@ -53,7 +53,7 @@ jobs:
dafny-version: ${{ (github.event_name == 'schedule' || inputs.nightly) && 'nightly-latest' || '4.6.0' }}

- name: Regenerate code using smithy-dafny if necessary
if: ${{ inputs.nightly }}
if: ${{ github.event_name == 'schedule' || inputs.nightly }}
uses: ./.github/actions/polymorph_codegen
with:
dafny: ${{ env.DAFNY_VERSION }}
Expand Down
Original file line number Diff line number Diff line change
Expand Up @@ -22,6 +22,43 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry

predicate method {:extern} IsLegacyInput(input: Types.DecryptItemInput)

// The following functions are for the benefit of the extern implementation to call,
// avoiding direct references to generic datatype constructors
// since their calling pattern is different between different versions of Dafny
// (i.e. after 4.2, explicit type descriptors are required).

static function method CreateBuildSuccess(value: Option<InternalLegacyOverride>): Result<Option<InternalLegacyOverride>, Types.Error> {
Success(value)
}

static function method CreateBuildFailure(error: Types.Error): Result<Option<InternalLegacyOverride>, Types.Error> {
Failure(error)
}

static function method CreateInternalLegacyOverrideSome(value: InternalLegacyOverride): Option<InternalLegacyOverride> {
Some(value)
}

static function method CreateInternalLegacyOverrideNone(): Option<InternalLegacyOverride> {
None
}

function method CreateEncryptItemSuccess(value: Types.EncryptItemOutput): Result<Types.EncryptItemOutput, Types.Error> {
Success(value)
}

function method CreateEncryptItemFailure(error: Types.Error): Result<Types.EncryptItemOutput, Types.Error> {
Failure(error)
}

function method CreateDecryptItemSuccess(value: Types.DecryptItemOutput): Result<Types.DecryptItemOutput, Types.Error> {
Success(value)
}

function method CreateDecryptItemFailure(error: Types.Error): Result<Types.DecryptItemOutput, Types.Error> {
Failure(error)
}

}

}
Original file line number Diff line number Diff line change
@@ -1,5 +1,19 @@
package software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.legacy;

/**
* This file does *NOT* import a lot of things.
* This is because it is dealing with converting
* between different versions of the same name.
* The DynamoDbItemEncryptor module has Dafny and Java versions
* of the same type.
* This means that `EncryptItemOutput` for example
* needs to be disambiguated between the Dafny version and the Java version.
* In order to make it clearer at each call-site exactly what is happening
* the full import is used.
* IDEs tend to fight this so I'm sorry.
*/

import StandardLibraryInternal.InternalResult;
import Wrappers_Compile.Option;
import Wrappers_Compile.Result;
import com.amazonaws.services.dynamodbv2.datamodeling.encryption.DynamoDBEncryptor;
Expand All @@ -16,22 +30,9 @@
import software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToNative;
import software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.Error;
/**
* This file does *NOT* import a lot of things.
* This is because it is dealing with converting
* between different versions of the same name.
* The DynamoDbItemEncryptor module has Dafny and Java versions
* of the same type.
* This means that `EncryptItemOutput` for example
* needs to be disambiguated between the Dafny version and the Java version.
* In order to make it clearer at each call-site exactly what is happening
* the full import is used.
* IDEs tend to fight this so I'm sorry.
*/

import software.amazon.cryptography.dbencryptionsdk.structuredencryption.internaldafny.types.CryptoAction;

public class InternalLegacyOverride {
public class InternalLegacyOverride extends _ExternBase_InternalLegacyOverride {

private DynamoDBEncryptor encryptor;
private Map<String, Set<EncryptionFlags>> actions;
Expand Down Expand Up @@ -69,7 +70,7 @@ public static TypeDescriptor<InternalLegacyOverride> _typeDescriptor() {
);
}

public Boolean IsLegacyInput(
public boolean IsLegacyInput(
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DecryptItemInput input
) {
//= specification/dynamodb-encryption-client/decrypt-item.md#determining-legacy-items
Expand All @@ -94,7 +95,9 @@ > EncryptItem(
) {
// Precondition: Policy MUST allow the caller to encrypt.
if (!_policy.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT()) {
return createFailure("Legacy Policy does not support encrypt.");
return CreateEncryptItemFailure(
createError("Legacy Policy does not support encrypt.")
);
}

try {
Expand Down Expand Up @@ -124,9 +127,9 @@ > EncryptItem(
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny.EncryptItemOutput(
nativeOutput
);
return Result.create_Success(dafnyOutput);
return CreateEncryptItemSuccess(dafnyOutput);
} catch (Exception ex) {
return Result.create_Failure(Error.create_Opaque(ex));
return CreateEncryptItemFailure(Error.create_Opaque(ex));
}
}

Expand All @@ -146,7 +149,9 @@ > DecryptItem(
!_policy.is_FORCE__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT() &&
!_policy.is_FORBID__LEGACY__ENCRYPT__ALLOW__LEGACY__DECRYPT()
) {
return createFailure("Legacy Policy does not support decrypt.");
return CreateDecryptItemFailure(
createError("Legacy Policy does not support decrypt.")
);
}
try {
Map<
Expand Down Expand Up @@ -175,9 +180,9 @@ > DecryptItem(
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.ToDafny.DecryptItemOutput(
nativeOutput
);
return Result.create_Success(dafnyOutput);
return CreateDecryptItemSuccess(dafnyOutput);
} catch (Exception ex) {
return Result.create_Failure(Error.create_Opaque(ex));
return CreateDecryptItemFailure(Error.create_Opaque(ex));
}
}

Expand All @@ -186,7 +191,7 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(
) {
// Check for early return (Postcondition): If there is no legacyOverride there is nothing to do.
if (encryptorConfig.dtor_legacyOverride().is_None()) {
return Result.create_Success(Option.create_None());
return CreateBuildSuccess(CreateInternalLegacyOverrideNone());
}
final software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyOverride legacyOverride =
encryptorConfig.dtor_legacyOverride().dtor_value();
Expand All @@ -198,43 +203,48 @@ public static Result<Option<InternalLegacyOverride>, Error> Build(

// Precondition: The encryptor MUST be a DynamoDBEncryptor
if (!isDynamoDBEncryptor(maybeEncryptor)) {
return createFailure("Legacy encryptor is not supported");
return CreateBuildFailure(
createError("Legacy encryptor is not supported")
);
}
// Preconditions: MUST be able to create valid encryption context
final Result<EncryptionContext, Error> maybeEncryptionContext =
final InternalResult<EncryptionContext, Error> maybeEncryptionContext =
legacyEncryptionContext(encryptorConfig);
if (maybeEncryptionContext.is_Failure()) {
return Result.create_Failure(maybeEncryptionContext.dtor_error());
if (maybeEncryptionContext.isFailure()) {
return CreateBuildFailure(maybeEncryptionContext.error());
}
// Precondition: All actions MUST be supported types
final Result<Map<String, Set<EncryptionFlags>>, Error> maybeActions =
legacyActions(legacyOverride.dtor_attributeActionsOnEncrypt());
if (maybeActions.is_Failure()) {
return Result.create_Failure(maybeEncryptionContext.dtor_error());
final InternalResult<
Map<String, Set<EncryptionFlags>>,
Error
> maybeActions = legacyActions(
legacyOverride.dtor_attributeActionsOnEncrypt()
);
if (maybeActions.isFailure()) {
return CreateBuildFailure(maybeEncryptionContext.error());
}

final InternalLegacyOverride internalLegacyOverride =
new InternalLegacyOverride(
(DynamoDBEncryptor) maybeEncryptor,
maybeActions.dtor_value(),
maybeEncryptionContext.dtor_value(),
maybeActions.value(),
maybeEncryptionContext.value(),
legacyOverride.dtor_policy()
);

return Result.create_Success(Option.create_Some(internalLegacyOverride));
return CreateBuildSuccess(
CreateInternalLegacyOverrideSome(internalLegacyOverride)
);
}

// Everything below this point is an implementation detail

public static <T> Result<T, Error> createFailure(String message) {
public static Error createError(String message) {
final DafnySequence<Character> dafnyMessage =
software.amazon.smithy.dafny.conversion.ToDafny.Simple.CharacterSequence(
message
);
final Error dafnyEx = Error.create_DynamoDbItemEncryptorException(
dafnyMessage
);
return Result.create_Failure(dafnyEx);
return Error.create_DynamoDbItemEncryptorException(dafnyMessage);
}

public static boolean isDynamoDBEncryptor(
Expand All @@ -253,7 +263,10 @@ public static DafnySequence<Character> ToDafnyString(String s) {
);
}

public static Result<EncryptionContext, Error> legacyEncryptionContext(
public static InternalResult<
EncryptionContext,
Error
> legacyEncryptionContext(
software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.internaldafny.types.DynamoDbItemEncryptorConfig config
) {
try {
Expand All @@ -272,13 +285,16 @@ public static Result<EncryptionContext, Error> legacyEncryptionContext(
.build()
: encryptionContextBuilder.build();

return Result.create_Success(encryptionContext);
return InternalResult.success(encryptionContext);
} catch (Exception ex) {
return Result.create_Failure(Error.create_Opaque(ex));
return InternalResult.failure(Error.create_Opaque(ex));
}
}

public static Result<Map<String, Set<EncryptionFlags>>, Error> legacyActions(
public static InternalResult<
Map<String, Set<EncryptionFlags>>,
Error
> legacyActions(
DafnyMap<
? extends DafnySequence<? extends Character>,
? extends CryptoAction
Expand Down Expand Up @@ -311,14 +327,14 @@ public static Result<Map<String, Set<EncryptionFlags>>, Error> legacyActions(
}
};
attributeActionsOnEncrypt.forEach(buildLegacyActions);
return Result.create_Success(legacyActions);
return InternalResult.success(legacyActions);
} catch (IllegalArgumentException ex) {
final Error dafnyEx = Error.create_DynamoDbItemEncryptorException(
ToDafnyString(ex.getMessage())
);
return Result.create_Failure(dafnyEx);
return InternalResult.failure(dafnyEx);
} catch (Exception ex) {
return Result.create_Failure(Error.create_Opaque(ex));
return InternalResult.failure(Error.create_Opaque(ex));
}
}

Expand Down
26 changes: 25 additions & 1 deletion DynamoDbEncryption/runtimes/net/DynamoDbEncryption.csproj
Original file line number Diff line number Diff line change
Expand Up @@ -31,11 +31,35 @@
<NoWarn>CS0105,CS0618</NoWarn>
</PropertyGroup>

<PropertyGroup>
<!-- This is somewhat brittle,
but having the value in a properties file
that can be shared is worth it.
See: https://learn.microsoft.com/en-us/visualstudio/msbuild/property-functions?view=vs-2022
for more details on property functions

This takes a properties file (a=b)
1. Loads the file
2. Splits on `dafnyVersion=` and takes everything to the right of that
e.g. the version + any trailing data
3. Splits on newline and takes the second element.
This SHOULD be the value of `dafnyVersion` and not contain any trailing data
-->
<projectProperties>
$([System.IO.File]::ReadAllText('$(MSBuildProjectDirectory)/../../../project.properties'))
</projectProperties>
<dropBeforeDafnyVersionProperty>
$([System.Text.RegularExpressions.Regex]::Split("$(projectProperties)", "dafnyVersion=")[1])
</dropBeforeDafnyVersionProperty>
<DafnyVersion>
$([System.Text.RegularExpressions.Regex]::Split("$(dropBeforeDafnyVersionProperty)", "\n")[1])
</DafnyVersion>
</PropertyGroup>

<ItemGroup>
<PackageReference Include="AWSSDK.DynamoDBv2" Version="3.7.303.14"/>
<PackageReference Include="AWSSDK.Core" Version="3.7.304.7"/>
<PackageReference Include="DafnyRuntime" Version="4.2.0" />
<PackageReference Include="DafnyRuntime" Version="$(DafnyVersion)" />
<ProjectReference Include="../../../submodules/MaterialProviders/AwsCryptographicMaterialProviders/runtimes/net/MPL.csproj"/>
<!--
System.Collections.Immutable can be removed once dafny.msbuild is updated with
Expand Down
1 change: 1 addition & 0 deletions project.properties
Original file line number Diff line number Diff line change
@@ -1,4 +1,5 @@
projectJavaVersion=3.5.0-SNAPSHOT
mplDependencyJavaVersion=1.4.0
dafnyVersion=4.2.0
dafnyRuntimeJavaVersion=4.2.0
smithyDafnyJavaConversionVersion=0.1
Loading