feat(LLVM): prove monotonicity of the LLVM.Byte operations

[tobiasgrosser]

Byte had no monotonicity lemmas at all. Prove that shl, lshr and trunc
are monotone with respect to refinement, together with the lemmas they need: a
bit-wise characterisation of byte refinement, the fact that the all-poison byte
refines every byte, and that refinement is preserved by shifting.

The nuw and exact no-wrap checks are the interesting part. They reject a
shift whose shifted-out bits are not zero, and they have to agree on both sides:
when the source passes the check its shifted-out bits are concrete zeros, so the
refining target has the very same bits there and passes the check too.

The three monotonicity lemmas are public, as they are meant to be used
downstream. That needs Byte.Basic and Data.Refinement to also be imported
publicly.

[github-actions]

VeIR Benchmarks

Details

Benchmark suite	Current: bb0f1ab	Previous: 9f42ace	Ratio
add-fold-worklist/create	2224000 ns (± 54438)	1806000 ns (± 84633)	1.23
add-fold-worklist/rewrite	3953000 ns (± 127525)	3534000 ns (± 29203)	1.12
add-fold-worklist-local/create	2232000 ns (± 53444)	1826000 ns (± 90007)	1.22
add-fold-worklist-local/rewrite	3806000 ns (± 154710)	3295000 ns (± 54636)	1.16
add-zero-worklist/create	2240000 ns (± 85045)	1845000 ns (± 78796)	1.21
add-zero-worklist/rewrite	2710000 ns (± 125249)	2268000 ns (± 94240)	1.19
add-zero-reuse-worklist/create	1788000 ns (± 88272)	1523000 ns (± 17544)	1.17
add-zero-reuse-worklist/rewrite	2198000 ns (± 104293)	1874000 ns (± 48317)	1.17
mul-two-worklist/create	2187000 ns (± 109901)	1777000 ns (± 14653)	1.23
mul-two-worklist/rewrite	5784000 ns (± 105942)	4984000 ns (± 27725)	1.16
add-fold-forwards/create	2199000 ns (± 69482)	1803000 ns (± 23043)	1.22
add-fold-forwards/rewrite	3069000 ns (± 86873)	2654000 ns (± 26159)	1.16
add-zero-forwards/create	2155500 ns (± 103193)	1792000 ns (± 82130)	1.20
add-zero-forwards/rewrite	1944000 ns (± 71053)	1714000 ns (± 16956)	1.13
add-zero-reuse-forwards/create	1875000 ns (± 83855)	1517000 ns (± 17421)	1.24
add-zero-reuse-forwards/rewrite	1575000 ns (± 76449)	1374000 ns (± 7036)	1.15
mul-two-forwards/create	2256000 ns (± 109974)	1810000 ns (± 91828)	1.25
mul-two-forwards/rewrite	3817000 ns (± 146510)	3223000 ns (± 112383)	1.18
add-zero-reuse-first/create	1791500 ns (± 98407)	1539500 ns (± 46488)	1.16
add-zero-reuse-first/rewrite	8000 ns (± 1710)	9000 ns (± 1762)	0.89
add-zero-lots-of-reuse-first/create	1873500 ns (± 99992)	1534000 ns (± 10498)	1.22
add-zero-lots-of-reuse-first/rewrite	857500 ns (± 64894)	783000 ns (± 20700)	1.10

This comment was automatically generated by workflow using github-action-benchmark.