There are some problems with semantics for headers and header unions.
The comment about write_header_field_undef is wrong. write_header_field_undef is needed. Consider the case
a[n].x = y;
for out-of-bounds n.
The execution relation is constructed by (let us use expressions like (a[n].x) to denote values)
exec_write (a[n].x) y
exec_read (a[n]) (ValBaseHeader unit_fields None)
update_member (ValBaseHeader unit_fields None) "x" y (ValBaseHeader unit_fields None)
exec_write (a[n]) (ValBaseHeader unit_fields None)
write_header_field_undef is needed to complete this write.
write_header_field_invalid and write_header_field_undef are unfriendly with (abstract) symbolic execution, it's better to set uninitialized fields instead of doing nothing.
There are some problems with semantics for headers and header unions.
write_header_field_undefis wrong.write_header_field_undefis needed. Consider the casefor out-of-bounds
n. The execution relation is constructed by (let us use expressions like(a[n].x)to denote values)write_header_field_undefis needed to complete this write.write_header_field_invalidandwrite_header_field_undefare unfriendly with (abstract) symbolic execution, it's better to set uninitialized fields instead of doing nothing.update_union_memberviolates the global invariant that invalid headers must have initialized fields. That's violated by https://github.com/verified-network-toolchain/petr4/blob/poulet4/deps/poulet4/lib/Semantics.v#L1093 and https://github.com/verified-network-toolchain/petr4/blob/poulet4/deps/poulet4/lib/Semantics.v#L1095.