no match in valset

[rudynicolop]

Proposed changes

• Remove P4light's Match from ValueSet.
• Replace Match with ValueSet in Target.v

Questions:

1. In ValSetValueSet what is is the purpose of the members list? It was a list of list of Match but this has been replaced with ValueSet.
2. In Semantics.v unwrap_table_entry was used in load_decl to map a TableEntry to a table_entry and put it in a genv. Now the Matchs in a TableEntry need to be converted to ValueSet which requires a relation. Perhaps should TableEntry be used in place of table_entry in FTable, so matches in tables are evaluated upon table invocation? Or maybe load_decl needs to be a relation too...

[QinshiWang]

I think ValueSet type is for both table entries and value_sets in parsers, so we need to consider both use cases. I'm trying to find where ValSetValueSet is used but they are only used in coq/lib/P4light/Architecture/Tofino.v and coq/lib/P4light/Architecture/V1ModelTarget.v and it seems members is ignored. @MollyDream should know better about the situation.

For the second question, because we want to use ValueSet instead of Match, table_entry in FTable should use ValueSet, too. This avoids evaluating table entries (from constant expressions) at runtime and will remove the only axiom currently in Verifiable P4. load_decl should evaluate Match to ValueSet. I hope this is deterministic for constant expressions.

[rudynicolop]

I think this is ready.

[QinshiWang]

Should we consider using value instead of Expression in table entries? For constant entries, they are compile-time known values. For nonconstant entries, they are supplied by the control plane which uses values, not expressions. But on the other hand, this action_ref will be handled by exec_call which requires a function call whose parameters are expressions.

Inductive action_ref :=
  mk_action_ref (action : ident) (args : list (option Expression)).

[QinshiWang]

I see. In let+ x := a in b, b's type is B. In let* x := a in b, b's type is result Err B.

[rudynicolop]

Should we consider using value instead of Expression in table entries? For constant entries, they are compile-time known values. For nonconstant entries, they are supplied by the control plane which uses values, not expressions. But on the other hand, this action_ref will be handled by exec_call which requires a function call whose parameters are expressions.

Inductive action_ref :=
  mk_action_ref (action : ident) (args : list (option Expression)).

Sounds good to me.

[hackedy]

We talked about the action_ref changes in a Cornell meeting today. I don't think that should happen in this pull request because action_refs need to be refactored more invasively to fix #394. Really action_refs should have two lists of parameters and the first list (data plane arguments) should be expressions and the second list (control plane arguments) should be values.

I can do that refactor in a separate PR and we can discuss the details then.

[QinshiWang]

We talked about the action_ref changes in a Cornell meeting today. I don't think that should happen in this pull request because action_refs need to be refactored more invasively to fix #394. Really action_refs should have two lists of parameters and the first list (data plane arguments) should be expressions and the second list (control plane arguments) should be values.

I can do that refactor in a separate PR and we can discuss the details then.

Okay. Yes. There are two parts in the list of arguments, normal arguments and action data from table entries (either from the control plane or the P4 program). I think the former should be removed from action_refs. But let's leave it for now.

[QinshiWang]

There's still one pending comment from me. https://github.com/verified-network-toolchain/petr4/pull/402#discussion_r1120744089

[QinshiWang]

Looks good now. I recommend a squash merge for better history.