More P4Cub Interpreters

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4

Apache License 2.0

76 stars 21 forks source link

Closed zachary-kent closed 1 year ago

zachary-kent commented 1 year ago

Implements and verifies various interpreters for P4Cub, including those for l-values, parser expressions, and table entries.

rudynicolop commented 1 year ago

Looks great!

Would it be possible to move P4cub/Semantics/Interpreter.v to P4cub/Semantics/Dynamic/BigStep/Interpreter.v?