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.

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

chore: make const policy an extern #1587

Merged
merged 11 commits into from
Feb 3, 2025
Merged

chore: make const policy an extern #1587

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
11 commits
Select commit Hold shift + click to select a range
9795176
const in extern
rishav-karanjit Jan 23, 2025
fd93806
auto commit
rishav-karanjit Jan 23, 2025
1c8972b
auto commit
rishav-karanjit Jan 23, 2025
e885058
Revert "auto commit"
rishav-karanjit Jan 23, 2025
9bbf00c
auto commit
rishav-karanjit Jan 27, 2025
37b91f8
auto commit
rishav-karanjit Jan 27, 2025
346d335
auto commit
rishav-karanjit Jan 27, 2025
3e17992
formatting
rishav-karanjit Jan 27, 2025
16a7000
Merge branch 'main' into rishav/constinExtern
rishav-karanjit Jan 27, 2025
c5bff5a
Merge branch 'main' into rishav/constinExtern
rishav-karanjit Jan 27, 2025
553474d
Merge branch 'main' into rishav/constinExtern
rishav-karanjit Feb 3, 2025
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
2 changes: 1 addition & 1 deletion DynamoDbEncryption/dafny/DynamoDbItemEncryptor/src/InternalLegacyOverride.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -13,7 +13,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencry
static method {:extern} Build(encryptorConfig: Types.DynamoDbItemEncryptorConfig)
returns (output: Result<Option<InternalLegacyOverride>, Types.Error>)

const policy: DDBE.LegacyPolicy
const {:extern} policy: DDBE.LegacyPolicy

method {:extern} EncryptItem(input: Types.EncryptItemInput)
returns (output: Result<Types.EncryptItemOutput, Types.Error>)
Expand Down
13 changes: 12 additions & 1 deletion DynamoDbEncryption/runtimes/net/Extern/InternalLegacyConfig.cs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -8,7 +8,18 @@ namespace software.amazon.cryptography.dbencryptionsdk.dynamodb.itemencryptor.in

public partial class InternalLegacyOverride
{

public software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy _policy
Copy link
Member Author

@rishav-karanjit rishav-karanjit Jan 27, 2025 •
edited
Loading

Choose a reason for hiding this comment

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

I have tried following before reaching to this as solution:

  • Directly add a constant _policy in the class: This does not work because it should also be initialized with a constant in RHS and create_FORBID__LEGACY__ENCRYPT__FORBID__LEGACY__DECRYPT is not a constant.
  • Add a default constructor: We could have added a _policy and initialize it in a default constructor but this will not work because dafny transpiles a default constructor into class InternalLegacyOverride and this will cause conflict.

So, the best solution here is to always return FORBID__LEGACY__ENCRYPT__FORBID__LEGACY__DECRYPT from the getter. This is the only place, this variable is going to be used. However, technically this variable is never used because config.internalLegacyOverride.Some? is always false for .NET (and Rust) because they don't support legacy

{
get => software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types.LegacyPolicy.create_FORBID__LEGACY__ENCRYPT__FORBID__LEGACY__DECRYPT();
set { }
}
public software.amazon.cryptography.dbencryptionsdk.dynamodb.internaldafny.types._ILegacyPolicy policy
{
get
{
return this._policy;
}
}
public static Wrappers_Compile._IResult<
Wrappers_Compile._IOption<InternalLegacyOverride>,
_IError
Expand Down
3 changes: 3 additions & 0 deletions DynamoDbEncryption/runtimes/rust/src/software_externs.rs
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -58,6 +58,9 @@ pub mod software {
}

impl InternalLegacyOverride {
pub fn policy(&self) -> Rc<LegacyPolicy> {
self.r#__i_policy.clone()
}
pub fn Build(
config: &Rc<crate::software::amazon::cryptography::dbencryptionsdk::dynamodb::itemencryptor::internaldafny::types::DynamoDbItemEncryptorConfig>,
) -> Rc<
Expand Down
Loading