val 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))
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)
val 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))
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)
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
Prims.nat Prims.l_and Prims.b2t Prims.op_LessThanOrEqual Prims.op_LessThan FStar.Monotonic.HyperStack.mem LowParse.Slice.srel LowParse.Bytes.byte LowParse.Slice.slice FStar.UInt32.t LowParse.Spec.ConstInt32.parse_constint32le_unfold LowParse.Slice.bytes_of_slice_from Prims.unit LowParse.Low.Base.Spec.valid_facts LowParse.Spec.Base.total_constant_size_parser_kind LowParse.Spec.Int32le.parse_int32le LowParse.Spec.ConstInt32.parse_constint32le_kind LowParse.Spec.ConstInt32.constint32 LowParse.Spec.ConstInt32.parse_constint32le Prims.l_True Prims.squash Prims.l_iff LowParse.Low.Base.Spec.valid Prims.eq2 Prims.int Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_GreaterThanOrEqual FStar.UInt32.v LowParse.Low.Base.Spec.contents Prims.Nil FStar.Pervasives.pattern
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 /\
val 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))

    v: Prims.nat{0 <= v /\ v < 4294967296} ->
    h: FStar.Monotonic.HyperStack.mem ->
    input: LowParse.Slice.slice rrel rel ->
    pos: FStar.UInt32.t
  -> FStar.Pervasives.Lemma
    (ensures
      LowParse.Low.Base.Spec.valid (LowParse.Spec.ConstInt32.parse_constint32le v) h input pos <==>
      LowParse.Low.Base.Spec.valid LowParse.Spec.Int32le.parse_int32le h input pos /\
      FStar.UInt32.v (LowParse.Low.Base.Spec.contents LowParse.Spec.Int32le.parse_int32le
            h
            input
            pos) ==
      v)