[PRERELEASE REGRESSION] Dafny prerelease regression from aws/aws-database-encryption-sdk-dynamodb

[robin-aws]

(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 aws/aws-database-encryption-sdk-dynamodb#1029. It's only the verification builds that need attention now.

[stefan-aws]

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

[keyboardDrummer]

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