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(deps): Bump to MPL 1.7, Smithy-Dafny head #1391

Closed
wants to merge 48 commits into from
Closed

chore(deps): Bump to MPL 1.7, Smithy-Dafny head #1391

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
48 commits
Select commit Hold shift + click to select a range
6d06369
chore: Bump to MPL 1.7 and localtests
lucasmcdonald3 Sep 25, 2024
ce14c7e
m
lucasmcdonald3 Sep 25, 2024
a86f24e
m
lucasmcdonald3 Sep 25, 2024
3cc75ed
m
lucasmcdonald3 Sep 25, 2024
7996a61
m
lucasmcdonald3 Sep 25, 2024
6cd82f7
m
lucasmcdonald3 Sep 25, 2024
a740c4a
m
lucasmcdonald3 Sep 25, 2024
663cbf1
m
lucasmcdonald3 Sep 25, 2024
dbc0893
m
lucasmcdonald3 Sep 25, 2024
4a386ba
m
lucasmcdonald3 Sep 25, 2024
8162cc6
m
lucasmcdonald3 Sep 25, 2024
6c06933
no patch
lucasmcdonald3 Sep 25, 2024
5a76f3e
m
lucasmcdonald3 Sep 25, 2024
dc5b482
m
lucasmcdonald3 Sep 25, 2024
d476ff5
m
lucasmcdonald3 Sep 25, 2024
6803207
m
lucasmcdonald3 Sep 25, 2024
ce41385
m
lucasmcdonald3 Sep 25, 2024
7615cdc
m
lucasmcdonald3 Sep 25, 2024
3f8ae26
m
lucasmcdonald3 Sep 25, 2024
b4959f6
m
lucasmcdonald3 Sep 25, 2024
362c3b3
m
lucasmcdonald3 Sep 25, 2024
32842c7
m
lucasmcdonald3 Sep 25, 2024
4851473
m
lucasmcdonald3 Sep 25, 2024
4498ca1
m
lucasmcdonald3 Sep 25, 2024
36b6d1b
m
lucasmcdonald3 Sep 25, 2024
58556ca
m
lucasmcdonald3 Sep 26, 2024
5f01a6e
m
lucasmcdonald3 Sep 26, 2024
ebe03ae
m
lucasmcdonald3 Sep 26, 2024
dadb50b
m
lucasmcdonald3 Sep 26, 2024
44b0666
m
lucasmcdonald3 Sep 26, 2024
bd47477
use passing one
lucasmcdonald3 Sep 26, 2024
241d9a9
m
lucasmcdonald3 Sep 26, 2024
9fd7411
fix
lucasmcdonald3 Sep 26, 2024
1d6ac49
m
lucasmcdonald3 Sep 26, 2024
c3d0cc8
m
lucasmcdonald3 Sep 26, 2024
24a1f21
m
lucasmcdonald3 Sep 26, 2024
84d6574
bump smithy-dafny to main
lucasmcdonald3 Sep 26, 2024
6292917
m
lucasmcdonald3 Sep 26, 2024
6518054
no verify it
lucasmcdonald3 Sep 27, 2024
f6fa926
patch
lucasmcdonald3 Sep 27, 2024
6c5362a
m
lucasmcdonald3 Sep 27, 2024
3271a8a
format
lucasmcdonald3 Sep 27, 2024
e45f873
m
lucasmcdonald3 Sep 27, 2024
bf913a1
m
lucasmcdonald3 Sep 27, 2024
c3d1741
m
lucasmcdonald3 Sep 27, 2024
a6fca5a
m
lucasmcdonald3 Sep 27, 2024
2166afc
playing with reads
seebees Sep 30, 2024
fa1dd02
m
lucasmcdonald3 Sep 30, 2024
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
37 changes: 36 additions & 1 deletion DynamoDbEncryption/dafny/DynamoDbEncryption/src/ConfigToInfo.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -50,6 +50,8 @@ module SearchConfigToInfo {
//= type=implication
//# Initialization MUST fail if the length of the list of [beacon versions](#beacon-version-initialization) is not 1.
ensures outer.search.Some? && |outer.search.value.versions| != 1 ==> output.Failure?

ensures ValidSearchConfig(outer.search)
{
if outer.search.None? {
return Success(None);
Expand All @@ -63,10 +65,43 @@ module SearchConfigToInfo {
}

predicate ValidBeaconVersion(config : BeaconVersion)
reads
if
&& config.keySource.multi?
&& config.keySource.multi.cache.Some?
&& config.keySource.multi.cache.value.Shared?
then
{config.keySource.multi.cache.value.Shared as object} + config.keySource.multi.cache.value.Shared.Modifies
else {}
{
config.keyStore.ValidState()
&& config.keyStore.ValidState()
&& (
&& config.keySource.multi?
&& config.keySource.multi.cache.Some?
&& config.keySource.multi.cache.value.Shared?
==>
&& config.keySource.multi.cache.value.Shared.ValidState()
)
}
predicate ValidSearchConfig(config : Option<SearchConfig>)
reads
if config.Some? then
set
c <- config.value.versions |
&& c.keySource.multi?
&& c.keySource.multi.cache.Some?
&& c.keySource.multi.cache.value.Shared?
:: c.keySource.multi.cache.value.Shared
else {},
if config.Some? then
set
c <- config.value.versions |
&& c.keySource.multi?
&& c.keySource.multi.cache.Some?
&& c.keySource.multi.cache.value.Shared?,
o <- c.keySource.multi.cache.value.Shared.Modifies
:: o
else {}
{
if config.None? then
true
Expand Down
128 changes: 82 additions & 46 deletions ...amoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -759,62 +759,98 @@ abstract module AbstractAwsCryptographyDbEncryptionSdkDynamoDbTransformsService
var tmps4 := set t4 | t4 in tmp3.search.value.versions;
forall tmp4 :: tmp4 in tmps4 ==>
tmp4.keyStore.ValidState()
modifies set tmps5 <- set t5 <- config.tableEncryptionConfigs.Values | true
&& t5.keyring.Some?
:: t5.keyring.value,
obj <- tmps5.Modifies | obj in tmps5.Modifies :: obj
modifies set tmps6 <- set t6 <- config.tableEncryptionConfigs.Values | true
&& t6.cmm.Some?
:: t6.cmm.value,
obj <- tmps6.Modifies | obj in tmps6.Modifies :: obj
requires var tmps5 := set t5 | t5 in config.tableEncryptionConfigs.Values;
forall tmp5 :: tmp5 in tmps5 ==>
tmp5.search.Some? ==>
var tmps6 := set t6 | t6 in tmp5.search.value.versions;
forall tmp6 :: tmp6 in tmps6 ==>
tmp6.keySource.multi? ==>
tmp6.keySource.multi.cache.Some? ==>
tmp6.keySource.multi.cache.value.Shared? ==>
tmp6.keySource.multi.cache.value.Shared.ValidState()
modifies set tmps7 <- set t7 <- config.tableEncryptionConfigs.Values | true
&& t7.legacyOverride.Some?
:: t7.legacyOverride.value.encryptor,
&& t7.keyring.Some?
:: t7.keyring.value,
obj <- tmps7.Modifies | obj in tmps7.Modifies :: obj
modifies set tmps8 <- set t8 <- config.tableEncryptionConfigs.Values | true
&& t8.search.Some?
, t9 <- t8.search.value.versions :: t9.keyStore,
&& t8.cmm.Some?
:: t8.cmm.value,
obj <- tmps8.Modifies | obj in tmps8.Modifies :: obj
modifies set tmps9 <- set t9 <- config.tableEncryptionConfigs.Values | true
&& t9.legacyOverride.Some?
:: t9.legacyOverride.value.encryptor,
obj <- tmps9.Modifies | obj in tmps9.Modifies :: obj
modifies set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true
&& t10.search.Some?
, t11 <- t10.search.value.versions | true
:: t11.keyStore,
obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
modifies set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
&& t12.search.Some?
, t13 <- t12.search.value.versions | true
&& t13.keySource.multi?
&& t13.keySource.multi.cache.Some?
&& t13.keySource.multi.cache.value.Shared?
:: t13.keySource.multi.cache.value.Shared,
obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
ensures res.Success? ==>
&& fresh(res.value)
&& fresh(res.value.Modifies
- ( set tmps10 <- set t10 <- config.tableEncryptionConfigs.Values | true
&& t10.keyring.Some?
:: t10.keyring.value,
obj <- tmps10.Modifies | obj in tmps10.Modifies :: obj
) - ( set tmps11 <- set t11 <- config.tableEncryptionConfigs.Values | true
&& t11.cmm.Some?
:: t11.cmm.value,
obj <- tmps11.Modifies | obj in tmps11.Modifies :: obj
) - ( set tmps12 <- set t12 <- config.tableEncryptionConfigs.Values | true
&& t12.legacyOverride.Some?
:: t12.legacyOverride.value.encryptor,
obj <- tmps12.Modifies | obj in tmps12.Modifies :: obj
) - ( set tmps13 <- set t13 <- config.tableEncryptionConfigs.Values | true
&& t13.search.Some?
, t14 <- t13.search.value.versions :: t14.keyStore,
obj <- tmps13.Modifies | obj in tmps13.Modifies :: obj
- ( set tmps14 <- set t14 <- config.tableEncryptionConfigs.Values | true
&& t14.keyring.Some?
:: t14.keyring.value,
obj <- tmps14.Modifies | obj in tmps14.Modifies :: obj
) - ( set tmps15 <- set t15 <- config.tableEncryptionConfigs.Values | true
&& t15.cmm.Some?
:: t15.cmm.value,
obj <- tmps15.Modifies | obj in tmps15.Modifies :: obj
) - ( set tmps16 <- set t16 <- config.tableEncryptionConfigs.Values | true
&& t16.legacyOverride.Some?
:: t16.legacyOverride.value.encryptor,
obj <- tmps16.Modifies | obj in tmps16.Modifies :: obj
) - ( set tmps17 <- set t17 <- config.tableEncryptionConfigs.Values | true
&& t17.search.Some?
, t18 <- t17.search.value.versions | true
:: t18.keyStore,
obj <- tmps17.Modifies | obj in tmps17.Modifies :: obj
) - ( set tmps19 <- set t19 <- config.tableEncryptionConfigs.Values | true
&& t19.search.Some?
, t20 <- t19.search.value.versions | true
&& t20.keySource.multi?
&& t20.keySource.multi.cache.Some?
&& t20.keySource.multi.cache.value.Shared?
:: t20.keySource.multi.cache.value.Shared,
obj <- tmps19.Modifies | obj in tmps19.Modifies :: obj
) )
&& fresh(res.value.History)
&& res.value.ValidState()
ensures var tmps15 := set t15 | t15 in config.tableEncryptionConfigs.Values;
forall tmp15 :: tmp15 in tmps15 ==>
tmp15.keyring.Some? ==>
tmp15.keyring.value.ValidState()
ensures var tmps16 := set t16 | t16 in config.tableEncryptionConfigs.Values;
forall tmp16 :: tmp16 in tmps16 ==>
tmp16.cmm.Some? ==>
tmp16.cmm.value.ValidState()
ensures var tmps17 := set t17 | t17 in config.tableEncryptionConfigs.Values;
forall tmp17 :: tmp17 in tmps17 ==>
tmp17.legacyOverride.Some? ==>
tmp17.legacyOverride.value.encryptor.ValidState()
ensures var tmps18 := set t18 | t18 in config.tableEncryptionConfigs.Values;
forall tmp18 :: tmp18 in tmps18 ==>
tmp18.search.Some? ==>
var tmps19 := set t19 | t19 in tmp18.search.value.versions;
forall tmp19 :: tmp19 in tmps19 ==>
tmp19.keyStore.ValidState()
ensures var tmps21 := set t21 | t21 in config.tableEncryptionConfigs.Values;
forall tmp21 :: tmp21 in tmps21 ==>
tmp21.keyring.Some? ==>
tmp21.keyring.value.ValidState()
ensures var tmps22 := set t22 | t22 in config.tableEncryptionConfigs.Values;
forall tmp22 :: tmp22 in tmps22 ==>
tmp22.cmm.Some? ==>
tmp22.cmm.value.ValidState()
ensures var tmps23 := set t23 | t23 in config.tableEncryptionConfigs.Values;
forall tmp23 :: tmp23 in tmps23 ==>
tmp23.legacyOverride.Some? ==>
tmp23.legacyOverride.value.encryptor.ValidState()
ensures var tmps24 := set t24 | t24 in config.tableEncryptionConfigs.Values;
forall tmp24 :: tmp24 in tmps24 ==>
tmp24.search.Some? ==>
var tmps25 := set t25 | t25 in tmp24.search.value.versions;
forall tmp25 :: tmp25 in tmps25 ==>
tmp25.keyStore.ValidState()
ensures var tmps26 := set t26 | t26 in config.tableEncryptionConfigs.Values;
forall tmp26 :: tmp26 in tmps26 ==>
tmp26.search.Some? ==>
var tmps27 := set t27 | t27 in tmp26.search.value.versions;
forall tmp27 :: tmp27 in tmps27 ==>
tmp27.keySource.multi? ==>
tmp27.keySource.multi.cache.Some? ==>
tmp27.keySource.multi.cache.value.Shared? ==>
tmp27.keySource.multi.cache.value.Shared.ValidState()

// Helper functions for the benefit of native code to create a Success(client) without referring to Dafny internals
function method CreateSuccessOfClient(client: IDynamoDbEncryptionTransformsClient): Result<IDynamoDbEncryptionTransformsClient, Error> {
Expand Down
Loading
Loading