val validate_constint32le_slow (v: U32.t{0 <= U32.v v /\ U32.v v < 4294967296})
    : Tot (validator (parse_constint32le (U32.v v)))
let validate_constint32le_slow
  (v: U32.t { 0 <= U32.v v /\ U32.v v < 4294967296 } )
: Tot (validator (parse_constint32le (U32.v v)))
= fun #rrel #rel (input: slice rrel rel) pos ->
  let h = HST.get() in
    let _ =
      valid_constint32le (U32.v v) h input (uint64_to_uint32 pos);    
      valid_equiv parse_int32le h input (uint64_to_uint32 pos)
    in
  if U64.lt (Cast.uint32_to_uint64 input.len `U64.sub` pos) 4uL
  then
    validator_error_not_enough_data
  else
    let v' = read_int32le input (uint64_to_uint32 pos) in
    if U32.eq v v' then
      pos `U64.add` 4uL
    else
      validator_error_generic
val validate_constint32le_slow (v: U32.t{0 <= U32.v v /\ U32.v v < 4294967296})
    : Tot (validator (parse_constint32le (U32.v v)))
let validate_constint32le_slow (v: U32.t{0 <= U32.v v /\ U32.v v < 4294967296})
    : Tot (validator (parse_constint32le (U32.v v))) =
fun #rrel #rel (input: slice rrel rel) pos ->
  let h = HST.get () in
  let _ =
    valid_constint32le (U32.v v) h input (uint64_to_uint32 pos);
    valid_equiv parse_int32le h input (uint64_to_uint32 pos)
  in
  if U64.lt ((Cast.uint32_to_uint64 input.len) `U64.sub` pos) 4uL
  then validator_error_not_enough_data
  else
    let v' = read_int32le input (uint64_to_uint32 pos) in
    if U32.eq v v' then pos `U64.add` 4uL else validator_error_generic
LowParse.Low.ConstInt32.fst.checked
prims.fst.checked LowStar.Buffer.fst.checked LowParse.Spec.Int32le.fst.checked LowParse.Spec.ConstInt32.fst.checked LowParse.Low.Int32le.fst.checked LowParse.Low.Combinators.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Int.Cast.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Endianness.fsti.checked
LowParse.Low.ConstInt32.fst
FStar.UInt32.t Prims.l_and Prims.b2t Prims.op_LessThanOrEqual FStar.UInt32.v Prims.op_LessThan LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt64.t FStar.UInt64.lt FStar.UInt64.sub FStar.Int.Cast.uint32_to_uint64 LowParse.Slice.__proj__Mkslice__item__len FStar.UInt64.__uint_to_t LowParse.Low.ErrorCode.validator_error_not_enough_data Prims.bool FStar.UInt32.eq FStar.UInt64.add LowParse.Low.ErrorCode.validator_error_generic LowParse.Low.Int32le.read_int32le LowParse.Low.ErrorCode.uint64_to_uint32 Prims.unit LowParse.Low.Base.Spec.valid_equiv LowParse.Spec.Base.total_constant_size_parser_kind LowParse.Spec.Int32le.parse_int32le LowParse.Low.ConstInt32.valid_constint32le FStar.Monotonic.HyperStack.mem FStar.HyperStack.ST.get LowParse.Low.Base.validator LowParse.Spec.ConstInt32.parse_constint32le_kind LowParse.Spec.ConstInt32.constint32 LowParse.Spec.ConstInt32.parse_constint32le
module LowParse.Low.ConstInt32

(* LowParse implementation module for 32 bits contants *)

include FStar.Endianness

include LowParse.Spec.ConstInt32
include LowParse.Spec.Int32le
include LowParse.Low.Combinators
include LowParse.Low.Int32le

module U32 = FStar.UInt32
module U8 = FStar.UInt8
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module B = LowStar.Buffer
module Cast = FStar.Int.Cast
module U64 = FStar.UInt64

let valid_constint32le
  (v: nat { 0 <= v /\ v < 4294967296 } )
  (h: HS.mem)
  (#rrel #rel: _)
  (input: slice rrel rel)
  (pos: U32.t)
: Lemma (valid (parse_constint32le v) h input pos 
    <==> 
    (valid parse_int32le h input pos /\
    U32.v (contents parse_int32le h input pos) == v))
= valid_facts (parse_constint32le v) h input pos;
  valid_facts parse_int32le h input pos;
  parse_constint32le_unfold v (bytes_of_slice_from h input pos)

inline_for_extraction
let validate_constint32le_slow
  (v: U32.t { 0 <= U32.v v /\ U32.v v < 4294967296 } )
val validate_constint32le_slow (v: U32.t{0 <= U32.v v /\ U32.v v < 4294967296})
    : Tot (validator (parse_constint32le (U32.v v)))
v: FStar.UInt32.t{0 <= FStar.UInt32.v v /\ FStar.UInt32.v v < 4294967296}
  -> LowParse.Low.Base.validator (LowParse.Spec.ConstInt32.parse_constint32le (FStar.UInt32.v v))