Added <dyn Trait> Proof for Contracts for byte_add, byte_sub, and byte_offset (model-checking#188)

Towards model-checking#76 

This pull request impelments proof for contracts for `byte_add`,
`byte_sub` and `byte_offset` for `<dyn Trait>`. Both `const` and `mut`
versions are included.

It serves as an addition to an existing
[PR](model-checking#169) but is
submitted separately to avoid disrupting the ongoing review process for
that PR.

---------

Co-authored-by: Surya Togaru <[email protected]>
Co-authored-by: stogaru <[email protected]>
Co-authored-by: Felipe R. Monteiro <[email protected]>

Author: 3 people