val slice_of_repr_ptr (#t: _) (p: repr_ptr t) : GTot (LP.slice (preorder p.b) (preorder p.b))
let slice_of_repr_ptr #t (p:repr_ptr t)
  : GTot (LP.slice (preorder p.b) (preorder p.b))
  = slice_of_const_buffer p.b p.meta.len
val slice_of_repr_ptr (#t: _) (p: repr_ptr t) : GTot (LP.slice (preorder p.b) (preorder p.b))
let slice_of_repr_ptr #t (p: repr_ptr t) : GTot (LP.slice (preorder p.b) (preorder p.b)) =
slice_of_const_buffer p.b p.meta.len
LowParse.Repr.fsti.checked
prims.fst.checked LowStar.ImmutableBuffer.fst.checked LowStar.ConstBuffer.fsti.checked LowStar.Buffer.fst.checked LowParse.Spec.Base.fsti.checked LowParse.SLow.Base.fst.checked LowParse.Low.Base.fst.checked FStar.UInt32.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Integers.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Ghost.fsti.checked FStar.Bytes.fsti.checked
LowParse.Repr.fsti
LowParse.Repr.repr_ptr LowParse.Repr.slice_of_const_buffer LowParse.Repr.__proj__Ptr__item__b LowParse.Repr.__proj__Mkmeta__item__len LowParse.Repr.__proj__Ptr__item__meta LowParse.Slice.slice LowParse.Repr.preorder
(*
  Copyright 2015--2019 INRIA and Microsoft Corporation

  Licensed under the Apache License, Version 2.0 (the "License");
  you may not use this file except in compliance with the License.
  You may obtain a copy of the License at

    http://www.apache.org/licenses/LICENSE-2.0

  Unless required by applicable law or agreed to in writing, software
  distributed under the License is distributed on an "AS IS" BASIS,
  WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
  See the License for the specific language governing permissions and
  limitations under the License.

  Authors: T. Ramananandro, A. Rastogi, N. Swamy, A. Fromherz
*)
module LowParse.Repr

module LP = LowParse.Low.Base
module LS = LowParse.SLow.Base
module B = LowStar.Buffer
module HS = FStar.HyperStack
module C = LowStar.ConstBuffer
module U32 = FStar.UInt32

open FStar.Integers
open FStar.HyperStack.ST

module ST = FStar.HyperStack.ST
module I = LowStar.ImmutableBuffer

(* Summary:

   A pointer-based representation type.

   See
   https://github.com/mitls/mitls-papers/wiki/The-Memory-Model-of-miTLS#pointer-based-transient-reprs

   Calling it LowParse.Ptr since it should eventually move to everparse/src/lowparse
 *)

/// `strong_parser_kind`: We restrict our attention to the
/// representation of types whose parsers have the strong-prefix
/// property.
let strong_parser_kind =
    k:LP.parser_kind{
      LP.(k.parser_kind_subkind == Some ParserStrong)
    }

let preorder (c:C.const_buffer LP.byte) = C.qbuf_pre (C.as_qbuf c)

inline_for_extraction noextract
let slice_of_const_buffer (b:C.const_buffer LP.byte) (len:uint_32{U32.v len <= C.length b})
  : LP.slice (preorder b) (preorder b)
  =
    LP.({
       base = C.cast b;
       len = len
    })

let mut_p = LowStar.Buffer.trivial_preorder LP.byte


/// A slice is a const uint_8* and a length.
///
/// It is a layer around LP.slice, effectively guaranteeing that no
/// writes are performed via this pointer.
///
/// It allows us to uniformly represent `ptr t` backed by either
/// mutable or immutable arrays.
noeq
type const_slice =
  | MkSlice:
      base:C.const_buffer LP.byte ->
      slice_len:uint_32 {
        UInt32.v slice_len <= C.length base//  /\
        // slice_len <= LP.validator_max_length
      } ->
      const_slice

let to_slice (x:const_slice)
  : Tot (LP.slice (preorder x.base) (preorder x.base))
  = slice_of_const_buffer x.base x.slice_len

let of_slice (x:LP.slice mut_p mut_p)
  : Tot const_slice
  = let b = C.of_buffer x.LP.base in
    let len = x.LP.len in
    MkSlice b len

let live_slice (h:HS.mem) (c:const_slice) =
    C.live h c.base

let slice_as_seq (h:HS.mem) (c:const_slice) =
    Seq.slice (C.as_seq h c.base) 0 (U32.v c.slice_len)

(*** Pointer-based Representation types ***)

/// `meta t`: Each representation is associated with
/// specification metadata that records
///
///  -- the parser(s) that defines its wire format
///  -- the represented value
///  -- the bytes of its wire format
///
///  We retain both the value and its wire format for convenience.
///
///  An alternative would be to also retain here a serializer and then
///  compute the bytes when needed from the serializer. But that's a
///  bit heavy
[@erasable]
noeq
type meta (t:Type) = {
  parser_kind: strong_parser_kind;
  parser:LP.parser parser_kind t;
  parser32:LS.parser32 parser;
  v: t;
  len: uint_32;
  repr_bytes: Seq.lseq LP.byte (U32.v len);
  meta_ok: squash (LowParse.Spec.Base.parse parser repr_bytes == Some (v, U32.v len))//  /\
                   // 0ul < len /\
                   // len < LP.validator_max_length)
}

/// `repr_ptr t`: The main type of this module.
///
///   * The const pointer `b` refers to a representation of `t`
///
///   * The representation is described by erased the `meta` field
///
/// Temporary fields:
///
///   * At this stage, we also keep a real high-level value (vv). We
///     plan to gradually access instead its ghost (.meta.v) and
///     eventually get rid of it to lower implicit heap allocations.
///
///   * We also retain a concrete length field to facilitate using the
///     LowParse APIs for accessors and jumpers, which are oriented
///     towards using slices rather than pointers. As those APIs
///     change, we will remove the length field.
noeq
type repr_ptr (t:Type) =
  | Ptr: b:C.const_buffer LP.byte ->
         meta:meta t ->
         vv:t ->
         length:U32.t { U32.v meta.len == C.length b /\
                       meta.len == length /\
                       vv == meta.v } ->
       repr_ptr t

let region_of #t (p:repr_ptr t) : GTot HS.rid = B.frameOf (C.cast p.b)

let value #t (p:repr_ptr t) : GTot t = p.meta.v

let repr_ptr_p (t:Type) (#k:strong_parser_kind) (parser:LP.parser k t) =
  p:repr_ptr t{ p.meta.parser_kind == k /\ p.meta.parser == parser }

let slice_of_repr_ptr #t (p:repr_ptr t)
val slice_of_repr_ptr (#t: _) (p: repr_ptr t) : GTot (LP.slice (preorder p.b) (preorder p.b))
p: LowParse.Repr.repr_ptr t
  -> Prims.GTot
    (LowParse.Slice.slice (LowParse.Repr.preorder (Ptr?.b p)) (LowParse.Repr.preorder (Ptr?.b p)))