search

dafny-lang / dafny

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

Code verifies with VS Code IDE but not CLI #5797

Closed lucasmcdonald3 closed 2 months ago

lucasmcdonald3 commented 2 months ago

Dafny version

4.8.1

Code to produce this issue

https://github.com/aws/aws-database-encryption-sdk-dynamodb/pull/1391

This isn't minimal, but I really can't produce a minimal example here.

Command to run and resulting output

<Check out the repo/branch>

In VS Code IDE, open DynamoDbEncryption/dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy
Notice that the file verifies; in particular the requires/modifies/ensures clauses on `method DynamoDbEncryptionTransforms` on line 742

cd DynamoDbEncryption/
make verify

<Fails, pointing at some part of the requires/modifies/ensures clauses on `method DynamoDbEncryptionTransforms` on line 742>

dafny/DynamoDbEncryptionTransforms/src/Index.dfy(115,2): Error: a postcondition could not be proved on this return path
    |
115 |   {
    |   ^

dafny/DynamoDbEncryptionTransforms/Model/AwsCryptographyDbEncryptionSdkDynamoDbTransformsTypes.dfy(846,12): Related location: this is the postcondition that could not be proved
    |
846 |             forall tmp26 :: tmp26 in tmps26 ==>
    |             ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

What happened?

Crypto Tools recently updated a Smithy model and re-generated Dafny code with Smithy-Dafny. The generated Dafny fails to verify using the CLI (and in CI that uses the CLI), but verifies in the VS Code IDE. See example failure in CI: https://github.com/aws/aws-database-encryption-sdk-dynamodb/actions/runs/11074702103/job/30774100254

What type of operating system are you experiencing the problem on?

Linux, Mac

robin-aws commented 2 months ago

I find if I open dafny/DynamoDbEncryptionTransforms/src/Index.dfy in the IDE, I do see the same error as the CLI produces.

The issue is not in the ...Types.dfy file that defines the ensures clause on the DynamoDbEncryptionTransforms method defined by the abstract module, it's that the concrete refining modules in the ...Index.dfy file doesn't satisfy that ensures clause (or rather Dafny isn't able to prove it does).