P4cub2.0

[rudynicolop]

p4cub now used de Bruijn indices for type and term variables!

P4cub Changes

• de Bruijn indices for term and types, which affects everything from term declarations, parameter/argument binding, type substitution, and more.

• tags_t have been dropped entirely from p4cub.

• Header stacks are now derived forms in p4cub, composed of a struct including the new array type.

• Arrays of type t[n] are now included in p4cub with an indexing operation e1[e2].

• Structs and headers no longer have string field names and must be accessed with a nat like a tuple.

• Structs and header types are both represented by TStruct : bool -> list t -> t, where the bool is true to represent a header and false for a plain struct.

• Struct, header, and array literals are all represented as lists with a flag indicating which is which.

• Variable declarations now include a statement where the declaration is in scope. Variable declaration shifts the de Bruijn index.

• Parameters have de Bruijn indices. For n parameters the first has index 0 and the last index n-1.

• All p4cub architecture files were deleted as this functionality will now come from p4light's Target.v.

• Instantiation constructors now have parameters for other instances and for expression types separated.

• Parser blocks no longer have their own data type. Now parser blocks are composed of a statement where the final statement is a new transition statement.

• Parser select expressions are now no longer recursive.

• User-defined parser states are now identified by a number rather than a string.

• Tables no longer have their down data-types.

• Actions now have separate control plane and data plane parameters & arguments.

• Directionless parameters are removed b/c of the above change.

• Control and top-level declarations no longer have a sequence constructor. Now controls have a list of declarations and a program is a list of top-level declarations.

• Statement evaluation is no longer mutually recursive with parser-state-machine evaluation, and now includes this to avoid proofs about mutually defined inductive propositions.

C-Compiler Changes

• The ClightEnv of CCompEnv.v has adjusted fields reflecting the various p4cub namespaces, including term variables, instance names, function names, etc. These are mapped to a clight identifier and ClightEnv contains mappings from clight identifiers to types, functions, etc.

• Most of the definitions of CCompSel.v use a state transformer monad with ClightEnv serving as the state passed around.

P4cub Compiler Changes

• DeclCtx has a variable environment for variable declarations in controls.

• ToP4cub.v compiles header stacks to a derived form.

• A list of term names in scope is used to get the proper de Bruijn index for generated p4cub variables. Same for type names.

• p4cub now uses Target.v in statement evaluation for extern semantics.

• Tables are dynamically scoped.

GCL Changes

• Primitive operations for header stacks have been dropped b/c header stacks no longer exist in p4cub.

• There are many conversions from nat to string in places where variables are generated for GCL purposes, such as member fields (now nat in p4cub) and use-defined parser state names (now also nat in p4cub).

Testing

In a future pull-request p4cub will need to support function calls in control declarations. Until then some gcl tests will fail and have been sequestered in examples/failing_compiler_tests.

[jnfoster]

Amazing!!! Congrats on landing this.

[hackedy]

Can we merge this soon?

[rudynicolop]

I'm having trouble building with the right versions of dependencies. I updated to coq 8.15.2 on my machine but when I try to build in poulet4_Ccomp I get:

Compiled library Poulet4.P4light.Transformations.SimplExpr (in file /Users/rudypeterson/.opam/coq-8.15/lib/coq/user-contrib/Poulet4/P4light/Transformations/SimplExpr.vo) makes inconsistent assumptions over library Coq.Init.Ltac

[rudynicolop]

I'm having trouble building with the right versions of dependencies. I updated to coq 8.15.2 on my machine but when I try to build in poulet4_Ccomp I get:

Compiled library Poulet4.P4light.Transformations.SimplExpr (in file /Users/rudypeterson/.opam/coq-8.15/lib/coq/user-contrib/Poulet4/P4light/Transformations/SimplExpr.vo) makes inconsistent assumptions over library Coq.Init.Ltac

I think I've fixed it...

[hackedy]

Looks like the build failures now are just compiler tests which @ericthewry said it's OK to have fail

[ericthewry]

yes! Should we move them into a "failing tests" directory that's not run in CI?

[rudynicolop]

I moved all of the failing tests into petr4/examples/compiler_tests/failing but the script tries to run the failing directory. I'm not sure exactly how to adjust the Github actions to ignore that directory.

[rudynicolop]

I moved all of the failing tests into petr4/examples/compiler_tests/failing but the script tries to run the failing directory. I'm not sure exactly how to adjust the Github actions to ignore that directory.

Fixed.

[rudynicolop]

It seems all branches are suffering in the Github actions trying to install core_unix.

[zachary-kent]

It seems like running opam install with the --no-checksums switch may fix the issue

[rudynicolop]

Thanks! I think it's ready to merge!

[rudynicolop]

Rebased after the constant inlining update and ready to merge!

[hackedy]

Rebased after the constant inlining update and ready to merge!

Please, do the honors🫡🚢⚓️

[jnfoster]

🛬 this!