search

dafny-lang / dafny

Dafny is a verification-aware programming language
https://dafny.org
Other
2.84k stars 254 forks source link

[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-encryption-sdk-dafny #5486

Open aws-crypto-tools-ci-bot opened 1 month ago

aws-crypto-tools-ci-bot commented 1 month ago

Failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9211666378

aws-crypto-tools-ci-bot commented 1 month ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9227140544

aws-crypto-tools-ci-bot commented 1 month ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9236815228

aws-crypto-tools-ci-bot commented 1 month ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9244715971

aws-crypto-tools-ci-bot commented 1 month ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9257938778

aws-crypto-tools-ci-bot commented 4 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9273093986

aws-crypto-tools-ci-bot commented 4 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9289827790

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9306045571

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9321390870

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9331694046

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9339721493

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9353929762

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9370853269

aws-crypto-tools-ci-bot commented 3 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9387903056

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9404585893

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9420268072

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9430116572

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9438002598

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9452153802

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9469448084

aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9469448084

keyboardDrummer commented 2 weeks ago

Can locally reproduce using Z3 4.12.1, although not with Z3 4.12.6

dafny/AwsEncryptionSdk/src/MessageBody.dfy(1034,13): Error: Verification of 'MessageBody.ReadFramedMessageBody' timed out after 30 seconds
     |
1034 |       assert CorrectlyRead(buffer, Success(SuccessfulRead(nextRegularFrames, regularFrame.tail)), WriteMessageRegularFrames) by {
     |              ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

dafny/AwsEncryptionSdk/src/Serialize/SerializeFunctions.dfy(71,6): Related location: this proposition could not be proved
   |
71 |       CorrectlyReadRange(buffer, res.value.tail, inversionFunction(res.value.data))
   |       ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
keyboardDrummer commented 2 weeks ago

The ReadFramedMessageBody proof uses 48E6 resources on Dafny 4.2.0, so it might just be a verification brittleness issue.

Running on 4.2.0, this assertion batch which has an assertion with the correct line number, uses 1.6E6 resources, which could indicate brittleness. I've seen some teams use a resource limit of 1E6 to limit brittleness.

  Assertion batch 53:
    Outcome: Valid
    Duration: 00:00:00.3280123
    Resource count: 1633338

    Assertions:
      /Users/rwillems/SourceCode/aws-encryption-sdk-dafny/AwsEncryptionSDK/dafny/AwsEncryptionSdk/src/MessageBody.dfy(1034,14): assertion always holds
aws-crypto-tools-ci-bot commented 2 weeks ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9486351892

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9503400131

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9519390028

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9529462132

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9537427454

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9551375658

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9568835960

aws-crypto-tools-ci-bot commented 1 week ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9585480412

aws-crypto-tools-ci-bot commented 6 days ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9601126800

aws-crypto-tools-ci-bot commented 5 days ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9616861258

aws-crypto-tools-ci-bot commented 4 days ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9626860618

aws-crypto-tools-ci-bot commented 3 days ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9634918724

aws-crypto-tools-ci-bot commented 2 days ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9649036258

aws-crypto-tools-ci-bot commented 1 day ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9666265289

aws-crypto-tools-ci-bot commented 2 hours ago

Another failure in aws/aws-encryption-sdk-dafny/.github/workflows/nighly_dafny.yml@refs/heads/mainline. See https://github.com/aws/aws-encryption-sdk-dafny/actions/runs/9683423041