let betole32 (x: U32.t) =
  let open U32 in
  logor (logor (logor (logand (shift_right x 24ul) 0x000000FFul)
    (logand (shift_right x 8ul) 0x0000FF00ul))
    (logand (shift_left x 8ul) 0x00FF0000ul))
    (logand (shift_left x 24ul) 0xFF000000ul)
let betole32 (x: U32.t) =
let open U32 in
logor (logor (logor (logand (shift_right x 24ul) 0x000000FFul)
          (logand (shift_right x 8ul) 0x0000FF00ul))
      (logand (shift_left x 8ul) 0x00FF0000ul))
  (logand (shift_left x 24ul) 0xFF000000ul)
WasmSupport.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Int64.fsti.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked C.Loops.fst.checked
WasmSupport.fst
FStar.UInt32.t FStar.UInt32.logor FStar.UInt32.logand FStar.UInt32.shift_right FStar.UInt32.__uint_to_t FStar.UInt32.shift_left
module WasmSupport

open FStar.HyperStack.ST

module C = FStar.Int.Cast
module I64 = FStar.Int64
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module B = LowStar.Buffer

open LowStar.BufferOps
open FStar.Mul

(* Functions implemented primitively in JS. No F* client should call those! *)

assume val trap: Prims.string -> Stack unit (fun _ -> True) (fun _ _ _ -> False)

(* Really not meant to be called by F* clients... *)
assume val malloc: U32.t -> Stack U32.t (fun _ -> False) (fun _ _ _ -> False)

(* Functions that the code-generator expects to find, either at the Ast, CFlat
 * or Wasm levels. In SimplifyWasm.ml, we prefix these with their module (before
 * "to_c_names". After that, e.g. in CFlatToWasm.ml, we can refer to them with
 * their short names, e.g. align_64. *)

(* Round up to the nearest multiple of 64. *)
let align_64 (x: U32.t): Tot U32.t =
  if not ( U32.((x &^ 0x07ul) =^ 0ul) ) then
    U32.( (x &^ lognot 0x07ul) +%^ 0x08ul )
  else
    x

(* Non-zero sizes are not supported, period. *)
let check_buffer_size (s: U32.t): Stack unit (fun _-> True) (fun _ _ _ -> True) =
  if U32.( s =^ 0ul ) then
    trap "Zero-sized arrays are not supported in C and in WASM either. See WasmSupport.fst"

let betole16 (x: FStar.UInt16.t) =
  let open FStar.UInt16 in
  logor
    (logand (shift_right x 8ul) 0x00FFus)
    (logand (shift_left x 8ul) 0xFF00us)
val betole32 : x: FStar.UInt32.t -> FStar.UInt32.t
x: FStar.UInt32.t -> FStar.UInt32.t