P4light Type System Incomplete

[rudynicolop]

Refactoring of typing definitions.

In Typing.v, all of the typing rules are parameterized by a ge:genv, i.e. expression typing (expr_types) is:

(ge,path,D,G) |- e : t

ge should be hidden under the definition of expr_types, stmt_types, etc under a forall so the rule is independent of ge:

(path,D,G) |- e : t

and type soundness holds for any ge:genv. ge was added as a parameter to the typing definitions as a way to resolve enum type names in enum_member_sound, so removing ge will be tricky.

Furthermore, fundef_funtype_prop.Internal_prop needs to say that the body of the function is well-typed using block_types. B/c block_types needs fundef_funtype_prop as a constraint on the typing context & ge:genv it is necessary that these be defined in terms of one another via either a mutual Inductive or Fixpoint.

Missing Rules & Incomplete Proofs

In Rules.v type soundness for the following syntax forms is either only partially proved, entirely admitted, or not even defined yet.

• [x] casts.
• [ ] senum fields (may require a change to TypEnum : string -> P4Type + list string -> P4Type).
• [x] array size & index access.
• [ ] call cases in variable declarations.
• [x] assignment (needs lemmas for exec_read & exec_write).
• [x] blocks.
• [ ] function calls.
• [ ] method calls.
• [x] direction application.
• [ ] all program declarations.

[hackedy]

Do you still need this issue or have these things been filled in?

[rudynicolop]

Yeah there's still holes in the type system.