let live_slice (h:HS.mem) (c:const_slice) =
    C.live h c.base
let live_slice (h: HS.mem) (c: const_slice) =
C.live h c.base
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
FStar.Monotonic.HyperStack.mem LowParse.Repr.const_slice LowStar.ConstBuffer.live LowParse.Bytes.byte LowParse.Repr.__proj__MkSlice__item__base
(*
  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
val live_slice : h: FStar.Monotonic.HyperStack.mem -> c: LowParse.Repr.const_slice -> Type0
h: FStar.Monotonic.HyperStack.mem -> c: LowParse.Repr.const_slice -> Type0