Open robin-aws opened 1 month ago
https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/9469437383/job/26088100707:
dafny/StructuredEncryption/src/Canonize.dfy(665,2): Error: a postcondition could not be proved on this return path
dafny/StructuredEncryption/src/Canonize.dfy(664,12): Related location: this is the postcondition that could not be proved
dafny/StructuredEncryption/src/Canonize.dfy(670,11): Error: assertion might not hold
Failure is in
lemma {:vcs_split_on_every_assert} InputIsInput(origData : AuthList, input : CanonCryptoList)
requires forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt)
ensures forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt)
{
assert forall i | 0 <= i < |input| :: input[i] in input;
forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
var x :| x in origData && Updated2(x, input[i], DoDecrypt);
}
assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);
}
Weird thing is that the final assertion fails right after the forall which should prove the same thing.
Even if I write:
lemma {:vcs_split_on_every_assert} InputIsInput(origData : AuthList, input : CanonCryptoList)
requires forall val <- input :: exists x :: x in origData && Updated2(x, val, DoDecrypt)
ensures forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt)
{
assert forall i | 0 <= i < |input| :: input[i] in input;
forall i | 0 <= i < |input| ensures exists x :: x in origData && Updated2(x, input[i], DoDecrypt) {
var x :| x in origData && Updated2(x, input[i], DoDecrypt);
}
assume forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);
assert forall i | 0 <= i < |input| :: exists x :: x in origData && Updated2(x, input[i], DoDecrypt);
}
then the last assert
fails
(Manually cutting this since the automatic cutting is not yet hooked up on this repo)
See https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/9131391027.
Note the other Java-related nightly builds will be fixed by https://github.com/aws/aws-database-encryption-sdk-dynamodb/pull/1029. It's only the verification builds that need attention now.