Skip to content

Commit 7062a5c

Browse files
rishav-karanjitrishav-karanjit
committed
Merge branch 'main' into Golang/reviewed
2 parents 3232a23 + 8179af4 commit 7062a5c

34 files changed

+151
-91
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/dafny/DynamoDbEncryptionTransforms/src/DdbMiddlewareConfig.dfy

+5-3
Original file line numberDiff line numberDiff line change
@@ -47,9 +47,11 @@ module DdbMiddlewareConfig {
4747
function SearchModifies(config: Config) : set<object>
4848
{
4949
//set x, y | y in config.tableEncryptionConfigs && x in OneSearchModifies(config.tableEncryptionConfigs[y]) :: x
50-
set versions <- set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions,
51-
keyStore <- set version <- versions :: version.keySource.store,
52-
obj <- keyStore.Modifies | obj in keyStore.Modifies :: obj
50+
set
51+
versions <- (set configValue <- config.tableEncryptionConfigs.Values | configValue.search.Some? :: configValue.search.value.versions),
52+
keyStore <- (set version <- versions :: version.keySource.store),
53+
obj <- keyStore.Modifies
54+
{:nowarn} :: obj
5355

5456
}
5557

‎DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/src/Index.dfy

+1-1
Original file line numberDiff line numberDiff line change
@@ -130,7 +130,7 @@ module {:extern "software.amazon.cryptography.dbencryptionsdk.dynamodb.transform
130130
+ (if tableConfig.cmm.Some? then tableConfig.cmm.value.Modifies else {})
131131
+ (if tableConfig.legacyOverride.Some? then tableConfig.legacyOverride.value.encryptor.Modifies else {})
132132
)
133-
:: o;
133+
{:nowarn} :: o; // ignore warning for missing trigger on quantifier
134134

135135
var allLogicalTableNames := {};
136136
var i := 0;

0 commit comments

Comments
 (0)