verified-network-toolchain / petr4

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

Petr4 doesn't have nextIndex for header stacks #407

Open pataei opened 1 year ago

pataei commented 1 year ago

The title says it all.

P4 spec (v1.2.3)

Section operations on header stack states that "Intuitively, a header stack can be thought of as a struct containing an ordinary array of headers hs and a counter nextIndex that can be used to simplify the construction of parsers for header stacks, as discussed below. The nextIndex counter is initialized to 0."