P4light typing push: Beginnings of Statement Typing

[rudynicolop]

Will be merged when the github checks pass.

Type System

In LightTyping:

• Syntactic typing of l-values (LvalueTyping.v).
• Semantic typing of l-expressions (Typing.v).
• Adjusted proofs for l-expression cases (Rules.v).
• Changes to predicates for typing environments (Typing.v).
• Type soundness of conditional & return statements & ternary expressions (Rules.v).
• Partially filled in proofs for variable declaration & assignment (Rules.v). Need lemmas for exec_write, exec_read, & gamma_func_prop.

Dynamic Semantics

Minor changes in Semantics.v.

• Fix array_access_idx.
• Remove largely unused sv in exec_stmt_assign_func_call.