verified-network-toolchain / petr4

Petr4: Formal Semantics for P4
Apache License 2.0
76 stars 21 forks source link

Supported/Unsupported V1 Externs #162

Open stp59 opened 4 years ago

stp59 commented 4 years ago

I've delimited the externs I intend to support for the upcoming deadline, subject to change if deemed appropriate.

Supported:

Unsupported:

Support for most of these would involve non-trivial modifications to the architecture of the target interface (such as direct counters), or wouldn't make sense for the scope of petr4 (digest sends to the control plane). Eventually we need target-dependent table evaluation for custom table attributes introduced by architecture, but this is probably not feasible by the deadline.

*these externs have a wide range of support for various hashing algorithms, not all of which we need to support

hackedy commented 4 years ago

I'm not sure we have tests for verify_checksum_with_payload, update_checksum_with_payload, truncate, assert, or assume--why don't we leave those off?

hackedy commented 4 years ago

I grepped around and there's one test that uses update_checksum_with_payload, but it passes right now since it's only a typechecker test.

stp59 commented 4 years ago

In my understanding, the with payloads will be trivial to implement once the without payload ones are done, so I included them for good measure. I kept assert and assume and implemented them by raising a new exception. I thought it might be useful for debugging. I have yet to look further into truncate.

stp59 commented 4 years ago

Moving truncate to unsupported

hackedy commented 4 years ago

Just need to pick hash algorithms now