verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
76 stars 21 forks source link

Index should be Z or N in ValLeftArrayAccess? #315

Closed QinshiWang closed 2 years ago

QinshiWang commented 2 years ago

This could be a bit counter-intuitive, but if we use Z instead of N in the lvalue, we don't need to use the trick that converts a negative index value to a positive out-of-bounds index value, in order to conform P4 manual.

hackedy commented 2 years ago

Thanks for this!