Refactoring Kyber ref for F-star proofs

[xvzcf]

Make compress::compress_q in the reference code look more like compress::compress_d in the specification.

[karthikbhargavan]

This looks more explicit and will help proofs in short-run, but we don't have to do it this way just to make the proofs work. If you preferred the earlier code that would be fine too, this just makes it a 1-1 correspondence, which is more convenient.

[xvzcf]

This looks more explicit and will help proofs in short-run, but we don't have to do it this way just to make the proofs work. If you preferred the earlier code that would be fine too, this just makes it a 1-1 correspondence, which is more convenient.

I think the change makes the code look nicer anyway, what do you think @franziskuskiefer?

[franziskuskiefer]

I think the change makes the code look nicer anyway, what do you think @franziskuskiefer?

Yeah this looks nice, lets keep it.