val align_64 (x: U32.t) : Tot U32.t
let align_64 (x: U32.t): Tot U32.t =
  if not ( U32.((x &^ 0x07ul) =^ 0ul) ) then
    U32.( (x &^ lognot 0x07ul) +%^ 0x08ul )
  else
    x
val align_64 (x: U32.t) : Tot U32.t
let align_64 (x: U32.t) : Tot U32.t =
if not (let open U32 in (x &^ 0x07ul) =^ 0ul)
then let open U32 in (x &^ lognot 0x07ul) +%^ 0x08ul
else x
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 Prims.op_Negation FStar.UInt32.op_Equals_Hat FStar.UInt32.op_Amp_Hat FStar.UInt32.__uint_to_t FStar.UInt32.op_Plus_Percent_Hat FStar.UInt32.lognot Prims.bool
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. *)
val align_64 (x: U32.t) : Tot U32.t
x: FStar.UInt32.t -> FStar.UInt32.t