Verify pkg/experimental/epic

[henriman]

TODO

• Prove PutUint64 in Dafny
• Wrap sensitivity requirements on slayers.(*SCION) in the preconditions of e.g. prepareMacInput in epic.go in an IsLow function
  • Likely best to do this after pkg/slayers has been merged, which also defines such a function
• Potentially mark time.Time.After as (hyper) pure again. At the moment, this is prevented by Gobra issue 965.
• Potentially change the contract of NewCBCEncrypter s.t. it doesn't always require b and iv to be low and ensure IsLow of the returned BlockMode, by replacing the corresponding pre- and postcondition by a postcondition with an implication (as was done for BlockMode.CryptBlocks or aes.NewCipher)
  • Or, alternatively, undo this for CryptBlocks and NewCipher, depending on how general the contract should be

Besides these TODOs, this still contains workarounds for Gobra issues 846 and 955, which should be tracked by issues #14 and #15 (resp.)

OTHER KNOWN ISSUES

• The verification of the outline block in prepareMacInput is still somewhat unstable (although verification performance has increased dramatically by introducing the outline block)
• Although slices.gobra verifies successfully on its own, during the verification of pkg/experimental/epic, Gobra will consistently complain about insufficient permissions in the contract of CombineRange_Bytes (also see NOTE comment there)