verified-network-toolchain / petr4

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

Header union semantics #313

Open QinshiWang opened 2 years ago

QinshiWang commented 2 years ago

https://github.com/p4lang/p4-spec/issues/995 https://github.com/p4lang/p4-spec/pull/1007

QinshiWang commented 2 years ago

The current semantics does not obey the current P4 spec, but it's already coherent with the proposed change in the links. So we only need to add union.setInvalid() when the change is accepted.