P4light typing push - Githubissues

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4

Apache License 2.0

74 stars 20 forks source link

Closed rudynicolop closed 2 years ago

rudynicolop commented 2 years ago

Initial progress on type soundness proof for p4light.

Reworked definitions for typing p4light programs (LightTyping/Typing.v).
Induction principles & lemmas for the type soundness proofs (LightTyping/Utility.v, LightTyping/ValueTyping, Typed.v).
Minor changes to p4light evaluation in Semantics.v & ValueUtil.v to aid proofs.
ValueBase data type adjusted.
Proof of concept proofs of preservation & progress for some cases (LightTyping/Rules.v).

rudynicolop commented 2 years ago

I'll merge this into poulet4 once the github checks pass.

Further changes, additions to the type system will occur on this branch & I'll pull request those when ready.

hackedy commented 2 years ago

Thanks!