val decode_constint32le_injective'
      (v: nat{0 <= v /\ v < 4294967296})
      (b1: bytes{Seq.length b1 == 4})
      (b2: bytes{Seq.length b2 == 4})
    : Lemma
    ((Some? (decode_constint32le v b1) \/ Some? (decode_constint32le v b2)) /\
      (decode_constint32le v b1 == decode_constint32le v b2) ==>
      Seq.equal b1 b2)
let decode_constint32le_injective'
  (v: nat { 0 <= v /\ v < 4294967296 } )
  (b1: bytes { Seq.length b1 == 4 } )
  (b2: bytes { Seq.length b2 == 4 } )
: Lemma
  ((Some? (decode_constint32le v b1) \/ Some? (decode_constint32le v b2))
   /\ (decode_constint32le v b1 == decode_constint32le v b2) 
   ==> Seq.equal b1 b2)
= let res1 = decode_constint32le v b1 in
  let res2 = decode_constint32le v b2 in
  match res1 with
  | Some v1 ->
    assert ( U32.v v1 == v );
    (match res2 with
    | Some v2 ->
      assert ( U32.v v2 == v );
      assert ( v1 == v2 );
      decode_int32le_injective b1 b2
    | None -> ())
  | None -> ()
val decode_constint32le_injective'
      (v: nat{0 <= v /\ v < 4294967296})
      (b1: bytes{Seq.length b1 == 4})
      (b2: bytes{Seq.length b2 == 4})
    : Lemma
    ((Some? (decode_constint32le v b1) \/ Some? (decode_constint32le v b2)) /\
      (decode_constint32le v b1 == decode_constint32le v b2) ==>
      Seq.equal b1 b2)
let decode_constint32le_injective'
      (v: nat{0 <= v /\ v < 4294967296})
      (b1: bytes{Seq.length b1 == 4})
      (b2: bytes{Seq.length b2 == 4})
    : Lemma
    ((Some? (decode_constint32le v b1) \/ Some? (decode_constint32le v b2)) /\
      (decode_constint32le v b1 == decode_constint32le v b2) ==>
      Seq.equal b1 b2) =
let res1 = decode_constint32le v b1 in
let res2 = decode_constint32le v b2 in
match res1 with
| Some v1 ->
  assert (U32.v v1 == v);
  (match res2 with
    | Some v2 ->
      assert (U32.v v2 == v);
      assert (v1 == v2);
      decode_int32le_injective b1 b2
    | None -> ())
| 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 LowParse.Spec.ConstInt32.constint32 LowParse.Spec.Int32le.decode_int32le_injective Prims.unit Prims._assert Prims.l_or FStar.UInt.size FStar.UInt32.n Prims.op_GreaterThanOrEqual FStar.UInt32.v FStar.Pervasives.Native.option LowParse.Spec.ConstInt32.decode_constint32le Prims.l_True Prims.squash Prims.l_imp FStar.Pervasives.Native.uu___is_Some FStar.Seq.Base.equal Prims.Nil FStar.Pervasives.pattern
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 } )
: Tot (option (constint32 v))
= let v' = decode_int32le b in
    if U32.v v' = v then
      Some v'
    else
      None

let decode_constint32le_injective'
  (v: nat { 0 <= v /\ v < 4294967296 } )
  (b1: bytes { Seq.length b1 == 4 } )
  (b2: bytes { Seq.length b2 == 4 } )
: Lemma
  ((Some? (decode_constint32le v b1) \/ Some? (decode_constint32le v b2))
   /\ (decode_constint32le v b1 == decode_constint32le v b2)
val decode_constint32le_injective'
      (v: nat{0 <= v /\ v < 4294967296})
      (b1: bytes{Seq.length b1 == 4})
      (b2: bytes{Seq.length b2 == 4})
    : Lemma
    ((Some? (decode_constint32le v b1) \/ Some? (decode_constint32le v b2)) /\
      (decode_constint32le v b1 == decode_constint32le v b2) ==>
      Seq.equal b1 b2)

    v: Prims.nat{0 <= v /\ v < 4294967296} ->
    b1: LowParse.Bytes.bytes{FStar.Seq.Base.length b1 == 4} ->
    b2: LowParse.Bytes.bytes{FStar.Seq.Base.length b2 == 4}
  -> FStar.Pervasives.Lemma
    (ensures
      (Some? (LowParse.Spec.ConstInt32.decode_constint32le v b1) \/
        Some? (LowParse.Spec.ConstInt32.decode_constint32le v b2)) /\
      LowParse.Spec.ConstInt32.decode_constint32le v b1 ==
      LowParse.Spec.ConstInt32.decode_constint32le v b2 ==>
      FStar.Seq.Base.equal b1 b2)