val default_error_handler
      (typename_s fieldname reason: string)
      (error_code: U64.t)
      (context: B.pointer LPE.error_frame)
      (input: input_buffer)
      (start_pos: U64.t)
    : HST.Stack unit
      (requires (fun h -> B.live h context))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer context) h h'))
let default_error_handler
  (typename_s: string)
  (fieldname: string)
  (reason: string)
  (error_code: U64.t)
  (context: B.pointer LPE.error_frame)
  (input: input_buffer)
  (start_pos: U64.t)
: HST.Stack unit
  (requires (fun h -> B.live h context))
  (ensures (fun h _ h' -> B.modifies (B.loc_buffer context) h h'))
=
  if not ( !* context ).LPE.filled then begin
    context *= {
      LPE.filled = true;
      LPE.start_pos = start_pos;
      LPE.typename_s = typename_s;
      LPE.fieldname = fieldname;
      LPE.reason = reason;
      LPE.error_code = error_code;
    }
  end
val default_error_handler
      (typename_s fieldname reason: string)
      (error_code: U64.t)
      (context: B.pointer LPE.error_frame)
      (input: input_buffer)
      (start_pos: U64.t)
    : HST.Stack unit
      (requires (fun h -> B.live h context))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer context) h h'))
let default_error_handler
      (typename_s fieldname reason: string)
      (error_code: U64.t)
      (context: B.pointer LPE.error_frame)
      (input: input_buffer)
      (start_pos: U64.t)
    : HST.Stack unit
      (requires (fun h -> B.live h context))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer context) h h')) =
if not (!*context).LPE.filled
then
  context *=
  {
    LPE.filled = true;
    LPE.start_pos = start_pos;
    LPE.typename_s = typename_s;
    LPE.fieldname = fieldname;
    LPE.reason = reason;
    LPE.error_code = error_code
  }
EverParse3d.InputStream.Extern.Type.fst.checked
prims.fst.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.Pervasives.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked EverParse3d.InputStream.Extern.Base.fsti.checked EverParse3d.ErrorCode.fst.checked
EverParse3d.InputStream.Extern.Type.fst
Prims.string FStar.UInt64.t LowStar.Buffer.pointer EverParse3d.ErrorCode.error_frame EverParse3d.InputStream.Extern.Type.input_buffer LowStar.BufferOps.op_Star_Equals LowStar.Buffer.trivial_preorder EverParse3d.ErrorCode.Mkerror_frame Prims.unit Prims.bool Prims.op_Negation EverParse3d.ErrorCode.__proj__Mkerror_frame__item__filled LowStar.BufferOps.op_Bang_Star FStar.Monotonic.HyperStack.mem LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer
module EverParse3d.InputStream.Extern.Type
include EverParse3d.InputStream.Extern.Base

module B = LowStar.Buffer
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module U32 = FStar.UInt32
module U8 = FStar.UInt8
module LPE = EverParse3d.ErrorCode
module U64 = FStar.UInt64

noeq
type input_buffer = {
  base: t;
  has_length: bool;
  length: LPE.pos_t;
  position: B.pointer (Ghost.erased LPE.pos_t);
  prf: squash (
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    (has_length == true ==> U64.v length <= U64.v (len_all base))
  );
}

open LowStar.BufferOps

let make_input_buffer
  (base: t)
  (position: B.pointer (Ghost.erased LPE.pos_t))
: HST.Stack input_buffer
  (requires (fun h ->
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    B.live h position
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer position) h h' 
  ))
= position *= 0uL;
  {
    base = base;
    has_length = false;
    length = 0uL;
    position = position;
    prf = ();
  }

let make_input_buffer_with_length
  (base: t)
  (position: B.pointer (Ghost.erased LPE.pos_t))
  (length: LPE.pos_t)
: HST.Stack input_buffer
  (requires (fun h ->
    B.loc_disjoint (footprint base) (B.loc_buffer position) /\
    B.live h position /\
    U64.v length <= U64.v (len_all base)
  ))
  (ensures (fun h _ h' ->
    B.modifies (B.loc_buffer position) h h' 
  ))
= position *= 0uL;
  {
    base = base;
    has_length = true;
    length = length;
    position = position;
    prf = ();
  }

let default_error_handler
  (typename_s: string)
  (fieldname: string)
  (reason: string)
  (error_code: U64.t)
  (context: B.pointer LPE.error_frame)
  (input: input_buffer)
  (start_pos: U64.t)
: HST.Stack unit
  (requires (fun h -> B.live h context))
  (ensures (fun h _ h' -> B.modifies (B.loc_buffer context) h h'))
val default_error_handler
      (typename_s fieldname reason: string)
      (error_code: U64.t)
      (context: B.pointer LPE.error_frame)
      (input: input_buffer)
      (start_pos: U64.t)
    : HST.Stack unit
      (requires (fun h -> B.live h context))
      (ensures (fun h _ h' -> B.modifies (B.loc_buffer context) h h'))

    typename_s: Prims.string ->
    fieldname: Prims.string ->
    reason: Prims.string ->
    error_code: FStar.UInt64.t ->
    context: LowStar.Buffer.pointer EverParse3d.ErrorCode.error_frame ->
    input: EverParse3d.InputStream.Extern.Type.input_buffer ->
    start_pos: FStar.UInt64.t
  -> FStar.HyperStack.ST.Stack Prims.unit