val size32_u32:size32 serialize_u32
let size32_u32: size32 serialize_u32 =
  assert_norm (size32_constant_precond serialize_u32 4ul);
  size32_constant serialize_u32 4ul ()
val size32_u32:size32 serialize_u32
let size32_u32:size32 serialize_u32 =
assert_norm (size32_constant_precond serialize_u32 4ul);
size32_constant serialize_u32 4ul ()
LowParse.SLow.Int.fsti.checked
prims.fst.checked LowParse.Spec.Int.fsti.checked LowParse.SLow.Base.fst.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked
LowParse.SLow.Int.fsti
LowParse.SLow.Base.size32_constant LowParse.Spec.Int.parse_u32_kind FStar.UInt32.t LowParse.Spec.Int.parse_u32 LowParse.Spec.Int.serialize_u32 FStar.UInt32.__uint_to_t Prims.unit FStar.Pervasives.assert_norm LowParse.SLow.Base.size32_constant_precond
module LowParse.SLow.Int
include LowParse.Spec.Int
include LowParse.SLow.Base

inline_for_extraction
val parse32_u8: parser32 parse_u8

inline_for_extraction
val serialize32_u8 : serializer32 serialize_u8

inline_for_extraction
val parse32_u16: parser32 parse_u16

inline_for_extraction
val serialize32_u16 : serializer32 serialize_u16

inline_for_extraction
val parse32_u32: parser32 parse_u32

inline_for_extraction
val serialize32_u32 : serializer32 serialize_u32

inline_for_extraction
val parse32_u64: parser32 parse_u64

inline_for_extraction
val serialize32_u64 : serializer32 serialize_u64

// the `assert_norm`s are for the .fst, interleaving semantics again

inline_for_extraction
let size32_u8: size32 serialize_u8 =
  assert_norm (size32_constant_precond serialize_u8 1ul);
  size32_constant serialize_u8 1ul ()

inline_for_extraction
let size32_u16: size32 serialize_u16 =
  assert_norm (size32_constant_precond serialize_u16 2ul);
  size32_constant serialize_u16 2ul ()

inline_for_extraction
val size32_u32:size32 serialize_u32
LowParse.SLow.Base.size32 LowParse.Spec.Int.serialize_u32