PacketStream depacketizer remove redundant buffer

[t-wallet]

This is a small optimization that saves a couple registers and multiplexers. But unfortunately it requires a proof. Steps:

1. Prove that Mod headerBytes dataWidth > 0 => headerBytes + ( dataWidth - (Mod headerBytes dataWidth)) ~ dataWidth * DivRU headerBytes dataWidth
2. Remove _fwdBuf from DepacketizerState and use the last dataWidth - Mod headerBytes dataWidth bytes of _parseBuf instead. Manually handle the case Mod headerBytes dataWidth ~ 0 because that case deviates from the rule, there are no bytes to buffer.

[rowanG077]

You can do the nice "proof from nothing" I did once. You can also defer it to a runtime check similar to compareSNat by using sameNat.

[martijnbastiaan]

For a bunch of examples:

https://github.com/bittide/bittide-hardware/blob/f1bfb20fff007d7b0b8f2d4ee5d3e2d5396019ad/bittide/src/Data/Constraint/Nat/Extra.hs#L4

Each proof has an associated test:

https://github.com/bittide/bittide-hardware/blob/93a785b1603273f81949d25c05b1a119ac1c70eb/bittide/tests/Tests/Haxioms.hs

(Though these have been partially replaced by Agda proofs.)

[t-wallet]

Implemented in #85.

Thank you for the resources! clash-protocols now has its very own "haxioms" :)