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'm wondering if we should actually remove ValSetValueSet.

[rudynicolop]

I'm happy to remove ValSetValueSet. @MollyDream @txyyss what are your thoughts on this?

[MollyDream]

How do you plan to cover the value set in parsers without ValSetValueSet?
https://p4.org/p4-spec/docs/P4-16-v-1.2.3.html#sec-select

[rudynicolop]

Is ValSetValueSet a "value" of a parser select? Sorry if I'm misunderstanding.

[MollyDream]

Yes, you can scroll the bottom of section 13.6 for reference and examples.

[QinshiWang]

Sounds like what the control plane can store to pvs is
ValSetValueSet (sets: list ValueSet).

[jnfoster]

I confess I'm pretty confused. If these are control-plane values, why does P4Light need to represent them as Values? Seems like a different kind of object. Also, since these depend on an arch-specific @match annotation, isn't it hopeless to try to capture the kinds of elements that can arise in the control plane?

[QinshiWang]

Okay. I don't fully understand it, but let me try to make it more clear. Value-set values are needed at two places: table entries and parser "select" entries. For tables, constant entries are evaluated to value-set values during instantiation, and control plane entries are fed from the control plane as value-set values (so the semantics do not need to evaluate). For parser "select" entries, there are constant entries and control plane entries (using the value_set keyword), too. I think constant entries are also evaluated to value-set values during instantiation. Each value_set contains a list of control plane entries, and the semantics needs to fetch them when encountering a value_set. I assume combining them in one entry is not allowed, e.g.

value_set<vsk_t>(4) pvs;
select (p.tcp.port) {
    (1, pvs): runtime_defined_port;
    _: other_port;
}

I don't know how to formalize @match.

[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. #402 (comment)

[QinshiWang]

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