val tot_parse_tagged_union
  (#kt: parser_kind)
  (#tag_t: Type)
  (pt: tot_parser kt tag_t)
  (#data_t: Type)
  (tag_of_data: (data_t -> Tot tag_t))
  (#k: parser_kind)
  (p: (t: tag_t) -> Tot (tot_parser k (refine_with_tag tag_of_data t)))
: Pure (tot_parser (and_then_kind kt k) data_t)
    (requires True)
    (ensures (fun y ->
      forall x . parse y x == parse (parse_tagged_union #kt pt tag_of_data #k p) x
    ))
let tot_parse_tagged_union #kt #tag_t pt #data_t tag_of_data #k p =
  parse_tagged_union_payload_and_then_cases_injective tag_of_data #k p;
  pt `tot_and_then` tot_parse_tagged_union_payload tag_of_data p
val tot_parse_tagged_union
  (#kt: parser_kind)
  (#tag_t: Type)
  (pt: tot_parser kt tag_t)
  (#data_t: Type)
  (tag_of_data: (data_t -> Tot tag_t))
  (#k: parser_kind)
  (p: (t: tag_t) -> Tot (tot_parser k (refine_with_tag tag_of_data t)))
: Pure (tot_parser (and_then_kind kt k) data_t)
    (requires True)
    (ensures (fun y ->
      forall x . parse y x == parse (parse_tagged_union #kt pt tag_of_data #k p) x
    ))
let tot_parse_tagged_union #kt #tag_t pt #data_t tag_of_data #k p =
parse_tagged_union_payload_and_then_cases_injective tag_of_data #k p;
pt `tot_and_then` (tot_parse_tagged_union_payload tag_of_data p)
LowParse.Spec.Combinators.fst.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.fst
LowParse.Spec.Base.parser_kind LowParse.Spec.Base.tot_parser LowParse.Spec.Base.refine_with_tag LowParse.Spec.Combinators.tot_and_then LowParse.Spec.Combinators.tot_parse_tagged_union_payload Prims.unit LowParse.Spec.Combinators.parse_tagged_union_payload_and_then_cases_injective LowParse.Spec.Combinators.and_then_kind
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'"

let and_then #k #t p #k' #t' p' =
  let f : bare_parser t' = and_then_bare p p' in
  and_then_correct p p' ;
  f

let and_then_eq
  (#k: parser_kind)
  (#t:Type)
  (p:parser k t)
  (#k': parser_kind)
  (#t':Type)
  (p': (t -> Tot (parser k' t')))
  (input: bytes)
: Lemma
  (requires (and_then_cases_injective p'))
  (ensures (parse (and_then p p') input == and_then_bare p p' input))
= ()

let tot_and_then_bare (#t:Type) (#t':Type)
                (p:tot_bare_parser t)
                (p': (t -> Tot (tot_bare_parser t'))) :
                Tot (tot_bare_parser t') =
    fun (b: bytes) ->
    match p b with
    | Some (v, l) ->
      begin
	let p'v = p' v in
	let s' : bytes = Seq.slice b l (Seq.length b) in
	match p'v s' with
	| Some (v', l') ->
	  let res : consumed_length b = l + l' in
	  Some (v', res)
	| None -> None
      end
    | None -> None

let tot_and_then #k #t p #k' #t' p' =
  let f : tot_bare_parser t' = tot_and_then_bare p p' in
  and_then_correct #k p #k' p' ;
  parser_kind_prop_ext (and_then_kind k k') (and_then_bare p p') f;
  f

let parse_synth
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
: Pure (parser k t2)
  (requires (
    synth_injective f2
  ))
  (ensures (fun _ -> True))
= coerce (parser k t2) (and_then p1 (fun v1 -> parse_fret f2 v1))

let parse_synth_eq
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
  (b: bytes)
: Lemma
  (requires (synth_injective f2))
  (ensures (parse (parse_synth p1 f2) b == parse_synth' p1 f2 b))
= ()

unfold
let tot_parse_fret' (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_bare_parser t') =
  fun (b: bytes) -> Some (f v, (0 <: consumed_length b))

unfold
let tot_parse_fret (#t #t':Type) (f: t -> Tot t') (v:t) : Tot (tot_parser parse_ret_kind t') =
  [@inline_let] let _ = parser_kind_prop_equiv parse_ret_kind (tot_parse_fret' f v) in
  tot_parse_fret' f v

let tot_parse_synth
  #k #t1 #t2 p1 f2
= coerce (tot_parser k t2) (tot_and_then p1 (fun v1 -> tot_parse_fret f2 v1))

let bare_serialize_synth_correct #k #t1 #t2 p1 f2 s1 g1 =
  ()

let serialize_synth
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
  (s1: serializer p1)
  (g1: t2 -> GTot t1)
  (u: unit {
    synth_inverse f2 g1 /\
    synth_injective f2
  })
: Tot (serializer (parse_synth p1 f2))
= bare_serialize_synth_correct p1 f2 s1 g1;
  bare_serialize_synth p1 f2 s1 g1

let serialize_synth_eq
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
  (s1: serializer p1)
  (g1: t2 -> GTot t1)
  (u: unit {
    synth_inverse f2 g1 /\
    synth_injective f2
  })
  (x: t2)
: Lemma
  (serialize (serialize_synth p1 f2 s1 g1 u) x == serialize s1 (g1 x))
= ()

let serialize_synth_upd_chain
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
  (s1: serializer p1)
  (g1: t2 -> GTot t1)
  (u: unit {
    synth_inverse f2 g1 /\
    synth_injective f2
  })
  (x1: t1)
  (x2: t2)
  (y1: t1)
  (y2: t2)
  (i': nat)
  (s' : bytes)
: Lemma
  (requires (
    let s = serialize s1 x1 in
    i' + Seq.length s' <= Seq.length s /\
    serialize s1 y1 == seq_upd_seq s i' s' /\
    x2 == f2 x1 /\
    y2 == f2 y1
  ))
  (ensures (
    let s = serialize (serialize_synth p1 f2 s1 g1 u) x2 in
    i' + Seq.length s' <= Seq.length s /\
    Seq.length s == Seq.length (serialize s1 x1) /\
    serialize (serialize_synth p1 f2 s1 g1 u) y2 == seq_upd_seq s i' s'
  ))
= (* I don't know which are THE terms to exhibit among x1, x2, y1, y2 to make the patterns trigger *)
  assert (forall w w' . f2 w == f2 w' ==> w == w');
  assert (forall w . f2 (g1 w) == w)

let serialize_synth_upd_bw_chain
  (#k: parser_kind)
  (#t1: Type)
  (#t2: Type)
  (p1: parser k t1)
  (f2: t1 -> GTot t2)
  (s1: serializer p1)
  (g1: t2 -> GTot t1)
  (u: unit {
    synth_inverse f2 g1 /\
    synth_injective f2
  })
  (x1: t1)
  (x2: t2)
  (y1: t1)
  (y2: t2)
  (i': nat)
  (s' : bytes)
: Lemma
  (requires (
    let s = serialize s1 x1 in
    i' + Seq.length s' <= Seq.length s /\
    serialize s1 y1 == seq_upd_bw_seq s i' s' /\
    x2 == f2 x1 /\
    y2 == f2 y1
  ))
  (ensures (
    let s = serialize (serialize_synth p1 f2 s1 g1 u) x2 in
    i' + Seq.length s' <= Seq.length s /\
    Seq.length s == Seq.length (serialize s1 x1) /\
    serialize (serialize_synth p1 f2 s1 g1 u) y2 == seq_upd_bw_seq s i' s'
  ))
= (* I don't know which are THE terms to exhibit among x1, x2, y1, y2 to make the patterns trigger *)
  assert (forall w w' . f2 w == f2 w' ==> w == w');
  assert (forall w . f2 (g1 w) == w)

let parse_tagged_union #kt #tag_t pt #data_t tag_of_data #k p =
  parse_tagged_union_payload_and_then_cases_injective tag_of_data p;
  pt `and_then` parse_tagged_union_payload tag_of_data p

let parse_tagged_union_eq
  (#kt: parser_kind)
  (#tag_t: Type)
  (pt: parser kt tag_t)
  (#data_t: Type)
  (tag_of_data: (data_t -> GTot tag_t))
  (#k: parser_kind)
  (p: (t: tag_t) -> Tot (parser k (refine_with_tag tag_of_data t)))
  (input: bytes)
: Lemma
  (parse (parse_tagged_union pt tag_of_data p) input == (match parse pt input with
  | None -> None
  | Some (tg, consumed_tg) ->
    let input_tg = Seq.slice input consumed_tg (Seq.length input) in
    begin match parse (p tg) input_tg with
    | Some (x, consumed_x) -> Some ((x <: data_t), consumed_tg + consumed_x)
    | None -> None
    end
  ))
= parse_tagged_union_payload_and_then_cases_injective tag_of_data p;
  and_then_eq pt (parse_tagged_union_payload tag_of_data p) input;
  match parse pt input with
  | None -> ()
  | Some (tg, consumed_tg) ->
    let input_tg = Seq.slice input consumed_tg (Seq.length input) in
    parse_synth_eq #k #(refine_with_tag tag_of_data tg) (p tg) (synth_tagged_union_data tag_of_data tg) input_tg

let parse_tagged_union_eq_gen
  (#kt: parser_kind)
  (#tag_t: Type)
  (pt: parser kt tag_t)
  (#data_t: Type)
  (tag_of_data: (data_t -> GTot tag_t))
  (#k: parser_kind)
  (p: (t: tag_t) -> Tot (parser k (refine_with_tag tag_of_data t)))
  (#kt': parser_kind)
  (pt': parser kt' tag_t)
  (lem_pt: (
    (input: bytes) -> 
    Lemma
    (parse pt input == parse pt' input)
  ))
  (k': (t: tag_t) -> Tot parser_kind)
  (p': (t: tag_t) -> Tot (parser (k' t) (refine_with_tag tag_of_data t)))
  (lem_p' : (
    (k: tag_t) ->
    (input: bytes) ->
    Lemma
    (parse (p k) input == parse (p' k) input)
  ))
  (input: bytes)
: Lemma
  (parse (parse_tagged_union pt tag_of_data p) input == bare_parse_tagged_union pt' tag_of_data k' p' input)
= parse_tagged_union_payload_and_then_cases_injective tag_of_data p;
  and_then_eq pt (parse_tagged_union_payload tag_of_data p) input;
  lem_pt input;
  match parse pt input with
  | None -> ()
  | Some (tg, consumed_tg) ->
    let input_tg = Seq.slice input consumed_tg (Seq.length input) in
    parse_synth_eq #k #(refine_with_tag tag_of_data tg) (p tg) (synth_tagged_union_data tag_of_data tg) input_tg;
    lem_p' tg input_tg
val tot_parse_tagged_union
  (#kt: parser_kind)
  (#tag_t: Type)
  (pt: tot_parser kt tag_t)
  (#data_t: Type)
  (tag_of_data: (data_t -> Tot tag_t))
  (#k: parser_kind)
  (p: (t: tag_t) -> Tot (tot_parser k (refine_with_tag tag_of_data t)))
: Pure (tot_parser (and_then_kind kt k) data_t)
    (requires True)
    (ensures (fun y ->
      forall x . parse y x == parse (parse_tagged_union #kt pt tag_of_data #k p) x
    ))

    pt: LowParse.Spec.Base.tot_parser kt tag_t ->
    tag_of_data: (_: data_t -> tag_t) ->
    p:
      (t: tag_t
          -> LowParse.Spec.Base.tot_parser k (LowParse.Spec.Base.refine_with_tag tag_of_data t))
  -> Prims.Pure
    (LowParse.Spec.Base.tot_parser (LowParse.Spec.Combinators.and_then_kind kt k) data_t)