Kwxm/specification/bitwise

[kwxm]

This adds the specifications of the new bytestring operations and rimpemd_160 to the PLC specification. Most of the new content is in Section 4.3.2 (in cardano/builtins-5.tex). I had to rearrange the notation a bit and also "improved" some of the LaTeX, which has added some changes that are irrelevant to the main purpose of the PR.

A PDF including the updates is attached (recent changes included).
plutus-core-specification.pdf

[kwxm]

This fixes #6304 and #6394.

[kwxm]

Oops. I totally messed up the specification of and/or/xorByteString. When the inputs have different lengths the padding/truncation happens on the right,not the left. I'll fix that.

[kwxm]

The and/or/xor problem should be fixed now.

[kwxm]

We'll probably need to move writeBits into the Chang+2 section, but that only exists in this PR, which will have to be rebased on this one. The best approach is probably to merge this PR and that one first, then move writeBits into the appropriate section.

[zliu41]

This is outdated, and I don't think writeBits will make it to Chang+1, as node 10.0 release is imminent, so you may want to remove this.

[kwxm]

See the previous comment.

[zliu41]

This is for future work: we'll need to rework or remove this table, since it would no longer make sense when we start enabling existing builtins for Plutus V1 and V2.

[kwxm]

See this issue and this comment in @bezirg 's PR.

[zliu41]

We'll probably need to move writeBits into the Chang+2 section

Since we are changing the type signature of writeBits, I'd suggest removing it from this PR and re-adding it later.

[kwxm]

We'll probably need to move writeBits into the Chang+2 section

Since we are changing the type signature of writeBits, I'd suggest removing it from this PR and re-adding it later.

It looks like it'll get into Chang+1, so I'll leave it in. I've updated the specification of writeBits to reflect the change as well: it's a lot simpler now.