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

Towards #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](#169) but is
submitted separately to avoid disrupting the ongoing review process for
that PR.

---------

Co-authored-by: Surya Togaru <stogaru@andrew.cmu.edu>
Co-authored-by: stogaru <143449212+stogaru@users.noreply.github.com>
Co-authored-by: Felipe R. Monteiro <rms.felipe@gmail.com>

Author: 3 people