Optimize validation of arrays

[nikswamy]

In Issue #125, we note that validation for arrays like T f[:byte-size n] should be optimized in case:

• T is of a fixed size k that divides n
• Validation of T always succeeds and does not involve any actions

instead of generating a loop to validate the array element-wise, the entire array can be checked with a single arithmetic check.

This PR achieves this by first:

1. Enhancing the indexing structure of validators so that we can statically detect from the type of a validator whether or not it runs any actions
2. Revising the EverParse interpreter to target the validate_nlist_constant_size_without_actions combinator, in case the element type of the array has no actions.
3. Revising the EverParse frontend to produce the appropriate metadata, both to record whether or not a combinator has actions and whether or not the size of T is a compile-time constant (in which case, the modulus check can be statically evaluated way).

Along the way, I migrated LowParse and 3D to use the F* option --ext context_pruning and simplified away the use of various settings, including the use of --using_facts_from in generated 3D code.

[nikswamy]

@tahina-pro, I merged in your PR for pairs and also for fixed size arrays (fixing one small bug, see 688122f)

But, still I don't see tuples like { UINT8 fst; UINT8 snd[7]} getting optimized into a single check

I think the issue is that UINT8 snd[7] is represented as T_nlist (Cast.uint8_to_uint32 7uy) _ rather than literally T_nlist (T.Constant _) ...

[nikswamy]

hi @tahina-pro, I don't think coalescing checking a pair {UINT32 fst; UINT8 f[8]} is going to work in the current design, since the parser kind kind_nlist is defined as

let kind_nlist
  : parser_kind false WeakKindStrongPrefix
  = let open LP in
    {
      parser_kind_low = 0;
      parser_kind_high = None;
      parser_kind_subkind = Some ParserStrong;
      parser_kind_metadata = None
    }