Skip to content

Commit cc7416b

Browse files
ajewellamzajewellamz
committed
m
2 parents f2e3d22 + 10a5068 commit cc7416b

30 files changed

+46
-58
lines changed

‎.github/workflows/ci_codegen.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -39,7 +39,7 @@ jobs:
3939
# and to translate version strings such as "nightly-latest"
4040
# to an actual DAFNY_VERSION.
4141
- name: Setup Dafny
42-
uses: dafny-lang/[email protected]
42+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
4343
with:
4444
dafny-version: ${{ inputs.dafny }}
4545

‎.github/workflows/ci_examples_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ jobs:
5353
java-version: ${{ matrix.java-version }}
5454

5555
- name: Setup Dafny
56-
uses: dafny-lang/[email protected]
56+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5757
with:
5858
dafny-version: ${{ inputs.dafny }}
5959

‎.github/workflows/ci_examples_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -46,7 +46,7 @@ jobs:
4646
dotnet-version: ${{ matrix.dotnet-version }}
4747

4848
- name: Setup Dafny
49-
uses: dafny-lang/[email protected]
49+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5050
with:
5151
dafny-version: ${{ inputs.dafny }}
5252

‎.github/workflows/ci_test_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
submodules: recursive
4848

4949
- name: Setup Dafny
50-
uses: dafny-lang/[email protected]
50+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5151
with:
5252
dafny-version: ${{ inputs.dafny }}
5353

‎.github/workflows/ci_test_latest_released_mpl_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -54,7 +54,7 @@ jobs:
5454
java-version: ${{ matrix.java-version }}
5555

5656
- name: Setup Dafny
57-
uses: dafny-lang/[email protected]
57+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5858
with:
5959
dafny-version: ${{ needs.getVersion.outputs.version }}
6060

‎.github/workflows/ci_test_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
dotnet-version: ${{ matrix.dotnet-version }}
4848

4949
- name: Setup Dafny
50-
uses: dafny-lang/[email protected]
50+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5151
with:
5252
dafny-version: ${{ inputs.dafny }}
5353

‎.github/workflows/ci_test_vector_java.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ jobs:
5656
submodules: recursive
5757

5858
- name: Setup Dafny
59-
uses: dafny-lang/[email protected]
59+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
6060
with:
6161
dafny-version: ${{ inputs.dafny }}
6262

‎.github/workflows/ci_test_vector_net.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ jobs:
5252
submodules: recursive
5353

5454
- name: Setup Dafny
55-
uses: dafny-lang/[email protected]
55+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5656
with:
5757
dafny-version: ${{ inputs.dafny }}
5858

‎.github/workflows/dafny_interop_examples_java.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
fetch-depth: 0
4848

4949
- name: Setup MPL Dafny
50-
uses: dafny-lang/[email protected]
50+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5151
with:
5252
dafny-version: ${{ inputs.mpl-dafny }}
5353

@@ -73,7 +73,7 @@ jobs:
7373
make build_java CORES=$CORES
7474
7575
- name: Setup DBESDK Dafny
76-
uses: dafny-lang/[email protected]
76+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
7777
with:
7878
dafny-version: ${{ inputs.dbesdk-dafny}}
7979

‎.github/workflows/dafny_interop_examples_net.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
dotnet-version: ${{ matrix.dotnet-version }}
4848

4949
- name: Setup MPL Dafny
50-
uses: dafny-lang/[email protected]
50+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5151
with:
5252
dafny-version: ${{ inputs.mpl-dafny }}
5353

@@ -80,7 +80,7 @@ jobs:
8080
make transpile_net CORES=$CORES
8181
8282
- name: Setup DBESDK Dafny
83-
uses: dafny-lang/[email protected]
83+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
8484
with:
8585
dafny-version: ${{ inputs.dbesdk-dafny}}
8686

‎.github/workflows/dafny_interop_java.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
fetch-depth: 0
4848

4949
- name: Setup MPL Dafny
50-
uses: dafny-lang/[email protected]
50+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5151
with:
5252
dafny-version: ${{ inputs.mpl-dafny }}
5353

@@ -73,7 +73,7 @@ jobs:
7373
make build_java CORES=$CORES
7474
7575
- name: Setup DBESDK Dafny
76-
uses: dafny-lang/[email protected]
76+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
7777
with:
7878
dafny-version: ${{ inputs.dbesdk-dafny}}
7979

‎.github/workflows/dafny_interop_test_net.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -47,7 +47,7 @@ jobs:
4747
dotnet-version: ${{ matrix.dotnet-version }}
4848

4949
- name: Setup MPL Dafny
50-
uses: dafny-lang/[email protected]
50+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5151
with:
5252
dafny-version: ${{ inputs.mpl-dafny }}
5353

@@ -80,7 +80,7 @@ jobs:
8080
make transpile_net CORES=$CORES
8181
8282
- name: Setup DBESDK Dafny
83-
uses: dafny-lang/[email protected]
83+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
8484
with:
8585
dafny-version: ${{ inputs.dbesdk-dafny}}
8686

‎.github/workflows/dafny_interop_test_vector_java.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -56,7 +56,7 @@ jobs:
5656
fetch-depth: 0
5757

5858
- name: Setup MPL Dafny
59-
uses: dafny-lang/[email protected]
59+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
6060
with:
6161
dafny-version: ${{ inputs.mpl-dafny }}
6262

@@ -83,7 +83,7 @@ jobs:
8383
make mvn_local_deploy
8484
8585
- name: Setup DBESDK Dafny
86-
uses: dafny-lang/[email protected]
86+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
8787
with:
8888
dafny-version: ${{ inputs.dbesdk-dafny}}
8989

‎.github/workflows/dafny_interop_test_vector_net.yml

+2-2
Original file line numberDiff line numberDiff line change
@@ -52,7 +52,7 @@ jobs:
5252
dotnet-version: ${{ matrix.dotnet-version }}
5353

5454
- name: Setup MPL Dafny
55-
uses: dafny-lang/[email protected]
55+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5656
with:
5757
dafny-version: ${{ inputs.mpl-dafny }}
5858

@@ -85,7 +85,7 @@ jobs:
8585
make transpile_net CORES=$CORES
8686
8787
- name: Setup DBESDK Dafny
88-
uses: dafny-lang/[email protected]
88+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
8989
with:
9090
dafny-version: ${{ inputs.dbesdk-dafny}}
9191

‎.github/workflows/library_dafny_verification.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -53,7 +53,7 @@ jobs:
5353
submodules: recursive
5454

5555
- name: Setup Dafny
56-
uses: dafny-lang/[email protected]
56+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
5757
with:
5858
dafny-version: ${{ inputs.dafny }}
5959

‎.github/workflows/library_format.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -37,7 +37,7 @@ jobs:
3737
submodules: recursive
3838

3939
- name: Setup Dafny
40-
uses: dafny-lang/[email protected]
40+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
4141
with:
4242
dafny-version: ${{ inputs.dafny }}
4343

‎.github/workflows/library_rust_tests.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -68,7 +68,7 @@ jobs:
6868
components: rustfmt
6969

7070
- name: Setup Dafny
71-
uses: dafny-lang/[email protected]
71+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
7272
with:
7373
dafny-version: nightly-2025-01-30-7db1e5f
7474

‎.github/workflows/test_vector_verification.yml

+1-1
Original file line numberDiff line numberDiff line change
@@ -43,7 +43,7 @@ jobs:
4343
submodules: recursive
4444

4545
- name: Setup Dafny
46-
uses: dafny-lang/[email protected]
46+
uses: ./submodules/MaterialProviders/.github/actions/setup_dafny/
4747
with:
4848
dafny-version: ${{ inputs.dafny }}
4949

‎DynamoDbEncryption/runtimes/rust/examples/clientsupplier/regional_role_client_supplier.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ impl ClientSupplier for RegionalRoleClientSupplier {
3535

3636
let sdk_config = tokio::task::block_in_place(|| {
3737
tokio::runtime::Handle::current().block_on(async {
38-
aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
38+
aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
3939
})
4040
});
4141
let kms_config = aws_sdk_kms::config::Builder::from(&sdk_config)

‎TestVectors/dafny/DDBEncryption/src/DecryptManifest.dfy

+1-2
Original file line numberDiff line numberDiff line change
@@ -127,8 +127,7 @@ module {:options "-functionSyntax:4"} DecryptManifest {
127127
{
128128
var timeStamp :- expect Time.GetCurrentTimeStamp();
129129
print timeStamp + " Decrypt : ", inFile, "\n";
130-
var configBv :- expect FileIO.ReadBytesFromFile(inFile);
131-
var configBytes := BvToBytes(configBv);
130+
var configBytes :- expect FileIO.ReadBytesFromFile(inFile);
132131
timeStamp :- expect Time.GetCurrentTimeStamp();
133132
print timeStamp + " File Read.\n";
134133
var json :- expect API.Deserialize(configBytes);

‎TestVectors/dafny/DDBEncryption/src/EncryptManifest.dfy

+2-4
Original file line numberDiff line numberDiff line change
@@ -151,8 +151,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
151151
{
152152
var timeStamp :- expect Time.GetCurrentTimeStamp();
153153
print timeStamp + " Encrypt : ", inFile, "\n";
154-
var configBv :- expect FileIO.ReadBytesFromFile(inFile);
155-
var configBytes := BvToBytes(configBv);
154+
var configBytes :- expect FileIO.ReadBytesFromFile(inFile);
156155
timeStamp :- expect Time.GetCurrentTimeStamp();
157156
print timeStamp + " File Read.\n";
158157
var json :- expect API.Deserialize(configBytes);
@@ -212,8 +211,7 @@ module {:options "-functionSyntax:4"} EncryptManifest {
212211

213212
var final := Object(result + [("tests", Object(test))]);
214213
var jsonBytes :- expect API.Serialize(final);
215-
var jsonBv := BytesBv(jsonBytes);
216-
var x :- expect FileIO.WriteBytesToFile(outFile, jsonBv);
214+
var x :- expect FileIO.WriteBytesToFile(outFile, jsonBytes);
217215

218216
timeStamp :- expect Time.GetCurrentTimeStamp();
219217
print timeStamp + " Tests Complete.\n";

‎TestVectors/dafny/DDBEncryption/src/Index.dfy

+3-4
Original file line numberDiff line numberDiff line change
@@ -26,13 +26,12 @@ module WrappedDDBEncryptionMain {
2626
modifies keyVectors.Modifies
2727
ensures keyVectors.ValidState()
2828
{
29-
var configBv := FileIO.ReadBytesFromFile(file);
30-
if configBv.Failure? {
29+
var configBytes := FileIO.ReadBytesFromFile(file);
30+
if configBytes.Failure? {
3131
print "Failed to open ", file, " continuing anyway.\n";
3232
return Success(MakeEmptyTestVector());
3333
}
34-
var configBytes := BvToBytes(configBv.value);
35-
var json :- expect API.Deserialize(configBytes);
34+
var json :- expect API.Deserialize(configBytes.value);
3635
output := ParseTestVector(json, prev, keyVectors);
3736
if output.Failure? {
3837
print output.error, "\n";

‎TestVectors/dafny/DDBEncryption/src/TestVectors.dfy

+1-2
Original file line numberDiff line numberDiff line change
@@ -560,8 +560,7 @@ module {:options "-functionSyntax:4"} DdbEncryptionTestVectors {
560560
jsonItems := jsonItems + [item];
561561
}
562562
var jsonBytes :- expect API.Serialize(Array(jsonItems));
563-
var jsonBv := BytesBv(jsonBytes);
564-
var x := FileIO.WriteBytesToFile(fileName, jsonBv);
563+
var x := FileIO.WriteBytesToFile(fileName, jsonBytes);
565564
expect x.Success?;
566565
}
567566

‎TestVectors/dafny/DDBEncryption/src/WriteManifest.dfy

+1-2
Original file line numberDiff line numberDiff line change
@@ -401,8 +401,7 @@ module {:options "-functionSyntax:4"} WriteManifest {
401401
var final := Object(result + [("tests", Object(tests))]);
402402

403403
var jsonBytes :- expect API.Serialize(final);
404-
var jsonBv := BytesBv(jsonBytes);
405-
var x := FileIO.WriteBytesToFile(fileName, jsonBv);
404+
var x := FileIO.WriteBytesToFile(fileName, jsonBytes);
406405
expect x.Success?;
407406
return Success(true);
408407
}

‎TestVectors/dafny/DDBEncryption/src/WriteSetPermutations.dfy

+1-7
Original file line numberDiff line numberDiff line change
@@ -117,11 +117,6 @@ module {:options "-functionSyntax:4"} WriteSetPermutations {
117117
return recs1 + recs2 + recs3 + recs4;
118118
}
119119

120-
function BytesBv(bits: seq<BoundedInts.uint8>): seq<bv8>
121-
{
122-
seq(|bits|, i requires 0 <= i < |bits| => bits[i] as bv8)
123-
}
124-
125120
method WriteSetPermutations()
126121
{
127122
var configs := GetConfigs();
@@ -132,11 +127,10 @@ module {:options "-functionSyntax:4"} WriteSetPermutations {
132127
]))]);
133128

134129
var jsonBytes :- expect API.Serialize(whole);
135-
var jsonBv := BytesBv(jsonBytes);
136130

137131
var _ :- expect FileIO.WriteBytesToFile(
138132
"PermTest.json",
139-
jsonBv
133+
jsonBytes
140134
);
141135
}
142136
}

‎TestVectors/runtimes/rust/src/create_client.rs

+2-2
Original file line numberDiff line numberDiff line change
@@ -27,7 +27,7 @@ impl _CreateInterceptedDDBClient_Compile::_default {
2727

2828
let table_configs = crate::deps::aws_cryptography_dbEncryptionSdk_dynamoDb_transforms::conversions::dynamo_db_tables_encryption_config::_dynamo_db_tables_encryption_config::plain_from_dafny(config);
2929
let shared_config = DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
30-
aws_config::BehaviorVersion::v2024_03_28()));
30+
aws_config::BehaviorVersion::latest()));
3131

3232
let shared_config = shared_config
3333
.to_builder()
@@ -49,7 +49,7 @@ impl _CreateInterceptedDDBClient_Compile::_default {
4949
-> Rc<_Wrappers_Compile::Result<Object<dyn IDynamoDBClient>, Rc<Error>>>
5050
{
5151
let shared_config = DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
52-
aws_config::BehaviorVersion::v2024_03_28()));
52+
aws_config::BehaviorVersion::latest()));
5353

5454
let shared_config = shared_config
5555
.to_builder()

‎releases/rust/db_esdk/examples/clientsupplier/regional_role_client_supplier.rs

+1-1
Original file line numberDiff line numberDiff line change
@@ -35,7 +35,7 @@ impl ClientSupplier for RegionalRoleClientSupplier {
3535

3636
let sdk_config = tokio::task::block_in_place(|| {
3737
tokio::runtime::Handle::current().block_on(async {
38-
aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
38+
aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
3939
})
4040
});
4141
let kms_config = aws_sdk_kms::config::Builder::from(&sdk_config)

‎releases/rust/db_esdk/src/ddb.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,11 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
3030
let shared_config = match tokio::runtime::Handle::try_current() {
3131
Ok(curr) => tokio::task::block_in_place(|| {
3232
curr.block_on(async {
33-
aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
33+
aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
3434
})
3535
}),
3636
Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
37-
aws_config::BehaviorVersion::v2024_03_28(),
37+
aws_config::BehaviorVersion::latest(),
3838
)),
3939
};
4040
let shared_config = shared_config
@@ -58,11 +58,11 @@ impl crate::r#software::amazon::cryptography::services::dynamodb::internaldafny:
5858
let shared_config = match tokio::runtime::Handle::try_current() {
5959
Ok(curr) => tokio::task::block_in_place(|| {
6060
curr.block_on(async {
61-
aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
61+
aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
6262
})
6363
}),
6464
Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
65-
aws_config::BehaviorVersion::v2024_03_28(),
65+
aws_config::BehaviorVersion::latest(),
6666
)),
6767
};
6868
let inner = aws_sdk_dynamodb::Client::new(&shared_config);

‎releases/rust/db_esdk/src/kms.rs

+4-4
Original file line numberDiff line numberDiff line change
@@ -26,11 +26,11 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def
2626
let shared_config = match tokio::runtime::Handle::try_current() {
2727
Ok(curr) => tokio::task::block_in_place(|| {
2828
curr.block_on(async {
29-
aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
29+
aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
3030
})
3131
}),
3232
Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
33-
aws_config::BehaviorVersion::v2024_03_28(),
33+
aws_config::BehaviorVersion::latest(),
3434
)),
3535
};
3636

@@ -51,11 +51,11 @@ impl crate::r#software::amazon::cryptography::services::kms::internaldafny::_def
5151
let shared_config = match tokio::runtime::Handle::try_current() {
5252
Ok(curr) => tokio::task::block_in_place(|| {
5353
curr.block_on(async {
54-
aws_config::load_defaults(aws_config::BehaviorVersion::v2024_03_28()).await
54+
aws_config::load_defaults(aws_config::BehaviorVersion::latest()).await
5555
})
5656
}),
5757
Err(_) => DAFNY_TOKIO_RUNTIME.block_on(aws_config::load_defaults(
58-
aws_config::BehaviorVersion::v2024_03_28(),
58+
aws_config::BehaviorVersion::latest(),
5959
)),
6060
};
6161

0 commit comments

Comments
 (0)