Skip to content

Commit 6067d3e

Browse files
rishav-karanjitrishav-karanjit
authored
chore: remove mac os from CI and refactor base64Lemmas (#1325)
1 parent 1a43584 commit 6067d3e

8 files changed

Lines changed: 47 additions & 12 deletions

‎.github/workflows/library_dafny_verification.yml‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,11 @@ jobs:
2828
AwsCryptographicMaterialProviders,
2929
StandardLibrary,
3030
]
31-
os: [macos-latest-large]
31+
os: [
32+
ubuntu-22.04,
33+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
34+
# macos-latest-large
35+
]
3236
runs-on: ${{ matrix.os }}
3337
defaults:
3438
run:

‎.github/workflows/library_go_tests.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,8 @@ jobs:
3636
# Windows source code is tested downstream (ex. ESDK-Python CI).
3737
# windows-latest,
3838
ubuntu-22.04,
39-
macos-13,
39+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
40+
# macos-13,
4041
]
4142
runs-on: ${{ matrix.os }}
4243
defaults:

‎.github/workflows/library_interop_tests.yml‎

Lines changed: 4 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -23,7 +23,8 @@ jobs:
2323
# https://taskei.amazon.dev/tasks/CrypTool-5283
2424
# windows-latest,
2525
ubuntu-22.04,
26-
macos-13,
26+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
27+
# macos-13,
2728
]
2829
language: [java, net, python, rust, go]
2930
# https://taskei.amazon.dev/tasks/CrypTool-5284
@@ -209,7 +210,8 @@ jobs:
209210
# TODO just test on mac and ubuntu for now
210211
# windows-latest,
211212
ubuntu-22.04,
212-
macos-13,
213+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
214+
# macos-13,
213215
]
214216
encrypting_language: [java, net, python, rust, go]
215217
decrypting_language: [java, net, python, rust, go]

‎.github/workflows/library_java_tests.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,8 @@ jobs:
3131
# TODO just test on mac for now
3232
# windows-latest,
3333
ubuntu-22.04,
34-
macos-13,
34+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
35+
# macos-13,
3536
]
3637
java-versions: [8, 11, 16, 17]
3738
runs-on: ${{ matrix.os }}

‎.github/workflows/library_net_tests.yml‎

Lines changed: 6 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,12 @@ jobs:
2929
TestVectorsAwsCryptographicMaterialProviders,
3030
]
3131
dotnet-version: ["6.0.x"]
32-
os: [windows-latest, ubuntu-22.04, macos-13]
32+
os: [
33+
windows-latest,
34+
ubuntu-22.04,
35+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
36+
# macos-13,
37+
]
3338
runs-on: ${{ matrix.os }}
3439
defaults:
3540
run:

‎.github/workflows/library_python_tests.yml‎

Lines changed: 2 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -36,7 +36,8 @@ jobs:
3636
# Windows source code is tested downstream (ex. ESDK-Python CI).
3737
# windows-latest,
3838
ubuntu-22.04,
39-
macos-13,
39+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
40+
# macos-13,
4041
]
4142
runs-on: ${{ matrix.os }}
4243
defaults:

‎.github/workflows/library_rust_tests.yml‎

Lines changed: 5 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -29,7 +29,11 @@ jobs:
2929
TestVectorsAwsCryptographicMaterialProviders,
3030
]
3131
# removed windows-latest because somehow it can't build aws-lc in CI
32-
os: [ubuntu-22.04, macos-13]
32+
os: [
33+
ubuntu-22.04,
34+
# TODO: Re-enable macOS after https://t.corp.amazon.com/P205755286
35+
# macos-13
36+
]
3337
runs-on: ${{ matrix.os }}
3438
permissions:
3539
id-token: write

‎StandardLibrary/src/Base64Lemmas.dfy‎

Lines changed: 21 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -54,11 +54,10 @@ module Base64Lemmas {
5454
requires Is1Padding(s[(|s| - 4)..])
5555
ensures Encode(DecodeValid(s)) == s
5656
{
57+
DecodeValidEncode1PaddingHelper(s);
5758
calc {
5859
Encode(DecodeValid(s));
5960
==
60-
assert |DecodeValid(s)| % 3 == 2;
61-
assert 2 <= |DecodeValid(s)|;
6261
EncodeUnpadded(DecodeValid(s)[..(|DecodeValid(s)| - 2)]) + Encode1Padding(DecodeValid(s)[(|DecodeValid(s)| - 2)..]);
6362
== { DecodeValidUnpaddedPartialFrom1PaddedSeq(s); }
6463
assert IsUnpaddedBase64String(s[..(|s| - 4)]) by {
@@ -76,6 +75,16 @@ module Base64Lemmas {
7675
}
7776
}
7877

78+
lemma DecodeValidEncode1PaddingHelper(s: seq<char>)
79+
requires IsBase64String(s)
80+
requires |s| >= 4
81+
requires Is1Padding(s[(|s| - 4)..])
82+
{
83+
assert |DecodeValid(s)| % 3 == 2;
84+
assert 2 <= |DecodeValid(s)|;
85+
}
86+
87+
7988
lemma DecodeValidUnpaddedPartialFrom2PaddedSeq(s: seq<char>)
8089
requires IsBase64String(s)
8190
requires |s| >= 4
@@ -96,11 +105,10 @@ module Base64Lemmas {
96105
requires Is2Padding(s[(|s| - 4)..])
97106
ensures Encode(DecodeValid(s)) == s
98107
{
108+
DecodeValid2PaddingPropertiesHelper(s);
99109
calc {
100110
Encode(DecodeValid(s));
101111
==
102-
assert |DecodeUnpadded(s[..|s|-4])| % 3 == 0;
103-
assert |DecodeValid(s)| % 3 == 1;
104112
EncodeUnpadded(DecodeValid(s)[..(|DecodeValid(s)| - 1)]) + Encode2Padding(DecodeValid(s)[(|DecodeValid(s)| - 1)..]);
105113
== { DecodeValidUnpaddedPartialFrom2PaddedSeq(s); }
106114
EncodeUnpadded(DecodeUnpadded(s[..(|s| - 4)])) + Encode2Padding(DecodeValid(s)[(|DecodeValid(s)| - 1)..]);
@@ -115,6 +123,15 @@ module Base64Lemmas {
115123
}
116124
}
117125

126+
lemma DecodeValid2PaddingPropertiesHelper(s: seq<char>)
127+
requires IsBase64String(s)
128+
requires |s| >= 4
129+
requires Is2Padding(s[(|s| - 4)..])
130+
{
131+
assert |DecodeUnpadded(s[..|s|-4])| % 3 == 0;
132+
assert |DecodeValid(s)| % 3 == 1;
133+
}
134+
118135
lemma DecodeValidEncode(s: seq<char>)
119136
requires IsBase64String(s)
120137
ensures Encode(DecodeValid(s)) == s

0 commit comments

Comments
 (0)