P4cub Refactor

[rudynicolop]

Semantics

• [ ] p4cub should be using Target.v. This relates to #324 .
• [ ] Properties such as progress & preservation remain unproven.

Syntax

• [ ] tags_t should be removed from p4cub.
• [ ] There are multiple constructors for a list data-type: structs, headers, & tuples which generate multiple proof goals that are nearly identical There should only be one constructor for this with a flag or witness to distinguish them.
• [ ] The current notations are cumbersome & unintuitive. They should be replaced with a Scope based notation system.
• [ ] A de Bruijn style syntax may benefit p4cub, for both type & expression variables.

Dependently-typed Syntax??

It may be preferable to enforce some properties of p4cub programs in their construction.

For example, there is a proper_nesting for p4cub expression types Expr.t predicate in P4cub/Syntax/Auxilary.v to enforce which types may enclose others, mainly to prevent headers from being nested too deeply. It's possible to enforce this in the definition of Expr.t as:

Inductive t : nat -> Type :=
 | TBool : t 0
 | TBit : N ->  t 0
 | TTuple : forall n : nat,  list (t n) -> t (S n)
 | THeader : forall n : nat, n <= 1 -> F.fs string (t n) -> t (S n)
(* other constructors... *).

Another issue with p4cub proofs is the need to defined induction principles for them & any predicate or relation defined for them. This is because p4cub terms are defined in terms of lists. To avoid this it's possible to redefine Expr.t as:

Inductive t : Type :=
| TBool
| TBit : N -> t
| TTupleNil : t
| TTupleCons : t -> t -> t
(* other constructors...*).

But this allows one to form ill-formed terms such as TTupleCons TBool TBool.

To prevent this Expr.t may depend upon a bool indicating whether or not the constructor is a tuple/list constructor:

Inductive t : bool -> Type :=
| TBool : t false
| TBit : N -> t false
| TTupleNil : t true
| TTupleCons : forall b : bool, t b -> t true -> t true
(* other constructors...*).

Furthermore it is possible to define p4cub terms as well-typed by construction. The signature for p4cub expressions Expr.e would be adjusted to:

Inductive e (gamma : string -> option t) : t -> Type :=
| EBool :  forall b: bool, e gamma TBool
| EVar : forall x t, gamma x = Some t -> e gamma t
(* other constructors... *).

Constructing proofs of gamma x = Some t may be annoying, so a de Bruijn style may better suit this change:

Inductive e (gamma : list t) : t -> Type :=
| EBool :  forall b: bool, e gamma TBool
| EVar : forall n t, gamma at n is t -> e gamma t
(* other constructors... *).

p4cub programs well-typed by construction would ensure type preservation by the definition of their dynamic semantics.

This approach will complicate any p4cub functions, particularly those that must construct them. The most difficult will be the p4light -> p4cub compiler, which by definition must be a verified type checker for p4light.

I think combining many of these changes would overall help the P4cub code. There would be no need to manually defined boilerplate induction principles and other predicates. While including propositions in the definitions of p4cub terms entails more overhead, ideally these subgoals may solved via refine & automation, & likely will not be extracted to OCaml.

Refactoring p4cub may be guided by this framework by @ericthewry & @jnfoster.

[rudynicolop]

I think my original proposal to correctly deal with type nesting was not faithful to the spec.

A better definition of Expr.t to enforce type nesting would be:

Inductive t : bool -> Set :=
| TBool : t true
| TBit : N -> t true
| TError : t false
| TStruct : forall b, list (string * t b) -> t b
| THeader : list (string * t true) -> t false