search

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
74 stars 20 forks source link

Enforce big endian #382

Closed hackedy closed 1 year ago

hackedy commented 1 year ago

I discovered while fixing some STF tests that the poulet4 conversions between Coq N/Z values and bitvectors appear to be little endian (but, thankfully, consistently so). This PR flips the endianness to big endian, so that the value 1 encodes to a 4-bit bitvector as [0; 0; 0; 1].

Not ready to merge, I broke a bunch of proofs which show the conversions are consistent. So I will have to repair those and the type soundness proofs that depend on them.

hackedy commented 1 year ago

This is ready for review. Instead of rewriting all the old functions I renamed them to le_original_name to indicate they are little endian and wrote big-endian versions under original_name by using List.rev and le_original_name. This made the proofs easy to fix.

txyyss commented 1 year ago

I think it is OK as long as lemmas are consistency.

hackedy commented 1 year ago

Yeah all the old lemmas are still there and I proved big endian versions of them by using the old lemmas and some facts about List.rev.