Petr4 is more general in the use of fixed-length integers

[pataei]

Compared to P4 spec, Petr4 is more general when fixed-length integers are used. For example, P4 spec restricts the underlying type of a serializable enum to bit<W> or int<W> where W is constant. However, Petr4 only requires such fixed-length integers to have a compile-time-known expression and does not require them to be constants. This is also the case for allowed nesting types for a header type declaration. I'm sure there will be more instances of this.

As of now, the formalization follows P4 and limits W to be a constant in places where the p4 spec uses W. That of course is assuming that p4 spec has used W consistently throughout and that bit<W> and int<W> always require W to be a constant.

Petr4 code

Petr4 translates bit<exp> to bit<W> and it never checks if W is a constant. So it's less restrictive than P4 spec since it just ensures that exp is compile-time-known. It does the same thing for int<exp> and varbit<exp>.

translate_type' ?(gen_wildcards=false) (env: CheckerEnv.t) (vars: string list) (typ: Types.Type.t) : Typed.Type.t * string list =
  let open Types.Type in
  let ret (t: Typed.Type.t) = t, [] in
  match typ with
  ...
  | IntType {tags; expr} -> ret @@ Int {width = eval_to_positive_int env tags expr}
  | BitType {tags; expr} -> ret @@ Bit {width = eval_to_positive_int env tags expr}
  | VarBit {tags; expr} -> ret @@ VarBit {width = eval_to_positive_int env tags expr}
  ...

and eval_to_positive_int env tags expr =
  let value =
    expr
    |> type_expression env Constant
    |> compile_time_eval_bigint env
    |> Bigint.to_int_exn
  in
  if value > 0
  then value
  else raise_s [%message "expected positive integer" ~info:(tags: Info.t)]

P4 spec (v1.2.3)

Enumeration types states that: "It is also possible to specify an enum with an underlying representation. These are sometimes called serializable enums, because headers are allowed to have fields with such enum types. This requires the programmer provide both the fixed-width unsigned (or signed) integer type and an associated integer value for each symbolic entry in the enumeration. The symbol typeRef in the grammar above must be one of the following types:

• an unsigned integer, i.e. bit<W> for some constant W.
• a signed integer, i.e. int<W> for some constant W."

Type nesting rules uses bit<W> and int<W> and varbit<W> but it doesn't say if W is a constant or not.

Fix

• [x] ensure that there is a reason for P4 to force W to be a constant.
• [x] either correct P4 spec or discuss if Petr4 wants to conform to P4 spec.

[pataei]

This has been in P4 spec (see PR) and Petr4 is now consistent with P4 spec.