Requires a recent Lem version that supports generating session-qualified
imports, e.g. revision rems-project/lem@d92b077f1781765a65082c815ff363ef79499860

Makes CheckAndUpdateDescriptor respect endianness

Use nondeterministic choice by default instead of a deterministic bitstream
generator in the state, which is slightly awkward to reason about, because
every use of undefined_boolS changes the state.  The previous behaviour can be
implemented as Sail code, if desired.

Also add a default implementation of internal_pick that nondeterministically
chooses an element from a list.

- Initialise fault typ field of result record to avoid an unitialised read that
  can lead to an early return with a fault.  This looks like a bug in the ASL
  specification (the ASL tests probably assume that this field is initialised
  with Fault_None).

- In ZeroExtend_slice_append (one of the helper functions for monomorphisation
  rewrites), use extzv instead of ZeroExtend.  It allows not only extension,
  but also truncation, and in AArch64_TranslationTableWalk the
  ZeroExtend_slice_append function is used to construct a 52 bit physical address
  using parts of the 64 bit input address.

- Use the Lem library function for reversing endianness

Worked around problem with the model where it tries to use bound variables
in patterns