val decode_constint32le (v: nat{0 <= v /\ v < 4294967296}) (b: bytes{Seq.length b == 4})
    : Tot (option (constint32 v))
let decode_constint32le
  (v: nat {0 <= v /\ v < 4294967296 } )
  (b: bytes { Seq.length b == 4 } )
: Tot (option (constint32 v))
= let v' = decode_int32le b in
    if U32.v v' = v then
      Some v'
    else
      None
val decode_constint32le (v: nat{0 <= v /\ v < 4294967296}) (b: bytes{Seq.length b == 4})
    : Tot (option (constint32 v))
let decode_constint32le (v: nat{0 <= v /\ v < 4294967296}) (b: bytes{Seq.length b == 4})
    : Tot (option (constint32 v)) =
let v' = decode_int32le b in
if U32.v v' = v then Some v' else None
LowParse.Spec.ConstInt32.fst.checked
prims.fst.checked LowParse.Spec.Int32le.fst.checked LowParse.Spec.Combinators.fsti.checked LowParse.Spec.Base.fsti.checked LowParse.Math.fst.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.ConstInt32.fst
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan LowParse.Bytes.bytes Prims.eq2 Prims.int FStar.Seq.Base.length LowParse.Bytes.byte Prims.op_Equality Prims.l_or Prims.op_GreaterThanOrEqual FStar.UInt.size FStar.UInt32.n FStar.UInt32.v FStar.Pervasives.Native.Some LowParse.Spec.ConstInt32.constint32 Prims.bool FStar.Pervasives.Native.None FStar.Pervasives.Native.option FStar.UInt32.t LowParse.Spec.Int32le.decode_int32le
module LowParse.Spec.ConstInt32

(* LowParse specification module for parsing 32 bits = 4 bytes unsigned constants

   Examples:

   uint32 foo = 5
   uint32_le foo = 7

*)

(* TODO: support big endian constants *)

include FStar.Endianness

include LowParse.Spec.Base
include LowParse.Spec.Combinators
include LowParse.Spec.Int32le

module U32 = FStar.UInt32
module U8 = FStar.UInt8
module Seq = FStar.Seq
module M = LowParse.Math

let constint32
  (v: nat { 0 <= v /\ v < 4294967296 } )
: Tot Type
= (u: U32.t { U32.v u == v } )

inline_for_extraction
let parse_constint32le_kind
: parser_kind
= strong_parser_kind 4 4 None

let decode_constint32le
  (v: nat {0 <= v /\ v < 4294967296 } )
  (b: bytes { Seq.length b == 4 } )
val decode_constint32le (v: nat{0 <= v /\ v < 4294967296}) (b: bytes{Seq.length b == 4})
    : Tot (option (constint32 v))
v: Prims.nat{0 <= v /\ v < 4294967296} -> b: LowParse.Bytes.bytes{FStar.Seq.Base.length b == 4}
  -> FStar.Pervasives.Native.option (LowParse.Spec.ConstInt32.constint32 v)