val make_total_constant_size_parser
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot t))
    : Pure (parser (total_constant_size_parser_kind sz) t)
      (requires (make_total_constant_size_parser_precond sz t f))
      (ensures (fun _ -> True))
let make_total_constant_size_parser
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot t))
: Pure (
    parser
      (total_constant_size_parser_kind sz)
      t
  )
  (requires (
    make_total_constant_size_parser_precond sz t f
  ))
  (ensures (fun _ -> True))
= let p : bare_parser t = make_constant_size_parser sz t (fun x -> Some (f x)) in
  parser_kind_prop_equiv (total_constant_size_parser_kind sz) p;
  p
val make_total_constant_size_parser
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot t))
    : Pure (parser (total_constant_size_parser_kind sz) t)
      (requires (make_total_constant_size_parser_precond sz t f))
      (ensures (fun _ -> True))
let make_total_constant_size_parser
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot t))
    : Pure (parser (total_constant_size_parser_kind sz) t)
      (requires (make_total_constant_size_parser_precond sz t f))
      (ensures (fun _ -> True)) =
let p:bare_parser t = make_constant_size_parser sz t (fun x -> Some (f x)) in
parser_kind_prop_equiv (total_constant_size_parser_kind sz) p;
p
LowParse.Spec.Combinators.fsti.checked
prims.fst.checked LowParse.Spec.Base.fsti.checked FStar.UInt8.fsti.checked FStar.UInt32.fsti.checked FStar.Tactics.fst.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.fsti.checked
LowParse.Spec.Combinators.fsti
Prims.nat LowParse.Bytes.bytes Prims.eq2 FStar.Seq.Base.length LowParse.Bytes.byte Prims.unit LowParse.Spec.Base.parser_kind_prop_equiv LowParse.Spec.Base.total_constant_size_parser_kind LowParse.Spec.Base.bare_parser LowParse.Spec.Combinators.make_constant_size_parser FStar.Pervasives.Native.Some FStar.Pervasives.Native.option LowParse.Spec.Base.parser LowParse.Spec.Combinators.make_total_constant_size_parser_precond Prims.l_True
module LowParse.Spec.Combinators
include LowParse.Spec.Base

module Seq = FStar.Seq
module U8 = FStar.UInt8
module U32 = FStar.UInt32

module T = FStar.Tactics

#reset-options "--using_facts_from '* -FStar.Tactis -FStar.Reflection'"

(** Constant-size parsers *)

let make_constant_size_parser_aux
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: Tot (bare_parser t)
= fun (s: bytes) ->
  if Seq.length s < sz
  then None
  else begin
    let s' : bytes = Seq.slice s 0 sz in
    match f s' with
    | None -> None
    | Some v ->
      let (sz: consumed_length s) = sz in
      Some (v, sz)
  end

let make_constant_size_parser_precond_precond
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
  (s1: bytes { Seq.length s1 == sz } )
  (s2: bytes { Seq.length s2 == sz } )
: GTot Type0
= (Some? (f s1) \/ Some? (f s2)) /\ f s1 == f s2

let make_constant_size_parser_precond
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: GTot Type0
= forall (s1: bytes {Seq.length s1 == sz}) (s2: bytes {Seq.length s2 == sz}) . {:pattern (f s1); (f s2)}
    make_constant_size_parser_precond_precond sz t f s1 s2 ==> Seq.equal s1 s2

let make_constant_size_parser_precond'
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: GTot Type0
= forall (s1: bytes {Seq.length s1 == sz}) (s2: bytes {Seq.length s2 == sz}) . {:pattern (f s1); (f s2)}
    make_constant_size_parser_precond_precond sz t f s1 s2 ==> s1 == s2

let make_constant_size_parser_injective
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: Lemma
  (requires (
    make_constant_size_parser_precond sz t f
  ))
  (ensures (
    injective (make_constant_size_parser_aux sz t f)
  ))
= let p : bare_parser t = make_constant_size_parser_aux sz t f in
  let prf1
    (b1 b2: bytes)
  : Lemma
    (requires (injective_precond p b1 b2))
    (ensures (injective_postcond p b1 b2))
  = assert (Some? (parse p b1));
    assert (Some? (parse p b2));
    let (Some (v1, len1)) = parse p b1 in
    let (Some (v2, len2)) = parse p b2 in
    assert ((len1 <: nat) == (len2 <: nat));
    assert ((len1 <: nat) == sz);
    assert ((len2 <: nat) == sz);
    assert (make_constant_size_parser_precond_precond sz t f (Seq.slice b1 0 len1) (Seq.slice b2 0 len2));
    assert (make_constant_size_parser_precond' sz t f)
  in
  Classical.forall_intro_2 (fun (b1: bytes) -> Classical.move_requires (prf1 b1))

let constant_size_parser_kind
  (sz: nat)
: Tot parser_kind
= strong_parser_kind sz sz None

let make_constant_size_parser
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot (option t)))
: Pure (
    parser
      (constant_size_parser_kind sz)
      t
  )
  (requires (
    make_constant_size_parser_precond sz t f
  ))
  (ensures (fun _ -> True))
= let p : bare_parser t = make_constant_size_parser_aux sz t f in
  make_constant_size_parser_injective sz t f;
  parser_kind_prop_equiv (constant_size_parser_kind sz) p;
  p

let tot_make_constant_size_parser_aux
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> Tot (option t)))
: Tot (tot_bare_parser t)
= fun (s: bytes) ->
  if Seq.length s < sz
  then None
  else begin
    let s' : bytes = Seq.slice s 0 sz in
    match f s' with
    | None -> None
    | Some v ->
      let (sz: consumed_length s) = sz in
      Some (v, sz)
  end

let tot_make_constant_size_parser
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> Tot (option t)))
: Pure (
    tot_parser
      (constant_size_parser_kind sz)
      t
  )
  (requires (
    make_constant_size_parser_precond sz t f
  ))
  (ensures (fun _ -> True))
= let p : tot_bare_parser t = tot_make_constant_size_parser_aux sz t f in
  make_constant_size_parser_injective sz t f;
  parser_kind_prop_equiv (constant_size_parser_kind sz) p;
  p

let make_total_constant_size_parser_precond
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot t))
: GTot Type0
= forall (s1: bytes {Seq.length s1 == sz}) (s2: bytes {Seq.length s2 == sz}) . {:pattern (f s1); (f s2)}
  f s1 == f s2 ==> Seq.equal s1 s2

let make_total_constant_size_parser
  (sz: nat)
  (t: Type)
  (f: ((s: bytes {Seq.length s == sz}) -> GTot t))
: Pure (
    parser
      (total_constant_size_parser_kind sz)
      t
  )
  (requires (
    make_total_constant_size_parser_precond sz t f
  ))
val make_total_constant_size_parser
      (sz: nat)
      (t: Type)
      (f: (s: bytes{Seq.length s == sz} -> GTot t))
    : Pure (parser (total_constant_size_parser_kind sz) t)
      (requires (make_total_constant_size_parser_precond sz t f))
      (ensures (fun _ -> True))

    sz: Prims.nat ->
    t: Type ->
    f: (s: LowParse.Bytes.bytes{FStar.Seq.Base.length s == sz} -> Prims.GTot t)
  -> Prims.Pure
    (LowParse.Spec.Base.parser (LowParse.Spec.Base.total_constant_size_parser_kind sz) t)