P4light typing push Part 2

verified-network-toolchain / petr4

Petr4: Formal Semantics for P4

Apache License 2.0

74 stars 20 forks source link

P4light typing push Part 2 #318

Closed rudynicolop closed 2 years ago

rudynicolop commented 2 years ago

More typing rules for p4light expressions proven (enum, other member, lists, records, unary & binary operations) (Rules.v).

Typing definitions adjusted (Typing.v) (Utility.v) (ValueTypeing.v).

Minor changes to the p4light semantics in Ops.v to prove progress (well-typed terms do not fail) of expression evaluation (garbage in, garbage out).

Dividing & modulo by 0 no longer fails, now the dividend is returned.
Shifting by a negative integer no longer fails, the absolute value taken.

rudynicolop commented 2 years ago

I'm not sure why the build failed...I uninstalled poulet4 and cleaned the build on my machine & everything works...It looks like there's a similar issue with #317 .

QinshiWang commented 2 years ago

I'm not sure why the build failed...I uninstalled poulet4 and cleaned the build on my machine & everything works...It looks like there's a similar issue with #317.

It's because CompCert just release v3.10 and caused incompatibility. It's okay as long as we can build locally.

rudynicolop commented 2 years ago

I think this is good to merge in poulet4. Idk whether or not #317 should be merged first...

rudynicolop commented 2 years ago

I'm not sure why the build failed...I uninstalled poulet4 and cleaned the build on my machine & everything works...It looks like there's a similar issue with #317.

It's because CompCert just release v3.10 and caused incompatibility. It's okay as long as we can build locally.

Ok yeah makes sense. I re-ran the checks that previously passed on poulet4 & those failed with the same error.

rudynicolop commented 2 years ago

Hello everyone! Proofs of progress & preservation are complete for many p4light expressions.

I haven't yet had a chance to fill in the proofs for statements yet, & there should probably be a typing definition (progress & preservation) for l-expressions.

If any of you are interested & available to help fill some of the holes in the type system that would be great! If not that's ok.

I think it would be great to have proven a few of the theorems for statements such as assignment & blocks maybe, & that would probably require rules for l-expressions.

I will try to get some of these definitions & proofs going, & I'd be happy to meet with anyone who may be interested in the p4light type-system.

I'll try to get this pr merged into poulet4 soon, & I'll document what's been done so far.

Thanks everyone!

jnfoster commented 2 years ago

Amazing!

rudynicolop commented 2 years ago

Will merge after workflow confirms successful build