P4 spec states that hs.lastIndex may only be used in a parser but Petr4 doesn't enforce this.

Petr4 code

The expression hs.lastIndex is an expression membership that is type-checked by function type_expression_member in Petr4 and type_expression_member calls the following helper for header stacks.

and type_expression_member_builtin env (ctx: Typed.ExprContext.t) tags typ (name: P4String.t) : Typed.Type.t =
  let open Typed.Type in
  let fail () =
    raise_unfound_member tags name.string in
  match typ with
  | Array { typ; _ } ->
     let idx_typ = Bit { width = 32 } in
     begin match name.string with
     | "size"
     | "lastIndex" ->
        idx_typ
     | "next"
     | "last" ->
        begin match ctx with
        | ParserState ->
           typ
        | _ -> failwith "can only use .last or .next within a parser"
        end
     | _ -> fail ()
     end
  | _ -> fail ()

While Petr4 limits next and last memberships to parser context, it does not do so for lastIndex.

P4 spec (v1.2.3)

Section operation on header stacks states that:
"hs.lastIndex: produces a 32-bit unsigned integer that encodes the index hs.nextIndex - 1. May only be used in a parser. If the nextIndex counter is 0, then evaluating this expression produces an undefined value."

Easy fix

This fix is easy, just add the check of context for lastIndex.