let store_post
  (#a:Type) (#rrel #rel:MB.srel a) (b:MB.mbuffer a rrel rel)
  (i:nat) (j:nat{i + j <= MB.length b}) (predicate:Seq.seq a -> Type0)
   = fun (h0:HS.mem) (_:unit) (h1:HS.mem) ->
     MB.live h1 b /\
     MB.(modifies (loc_buffer b) h0 h1) /\
     (let s1 = MB.as_seq h0 b in
      let s2 = MB.as_seq h1 b in
      let len = MB.length b in

      //the buffer only changes in the interval [i, j) as per the predicate
      Seq.equal (Seq.slice s2 0 i) (Seq.slice s1 0 i) /\
      Seq.equal (Seq.slice s2 (i + j) len) (Seq.slice s1 (i + j) len) /\
      predicate (Seq.slice s2 i (i + j)))
let store_post
      (#a: Type)
      (#rrel #rel: MB.srel a)
      (b: MB.mbuffer a rrel rel)
      (i: nat)
      (j: nat{i + j <= MB.length b})
      (predicate: (Seq.seq a -> Type0))
     =
fun (h0: HS.mem) (_: unit) (h1: HS.mem) ->
  MB.live h1 b /\ MB.(modifies (loc_buffer b) h0 h1) /\
  (let s1 = MB.as_seq h0 b in
    let s2 = MB.as_seq h1 b in
    let len = MB.length b in
    Seq.equal (Seq.slice s2 0 i) (Seq.slice s1 0 i) /\
    Seq.equal (Seq.slice s2 (i + j) len) (Seq.slice s1 (i + j) len) /\
    predicate (Seq.slice s2 i (i + j)))
LowStar.Endianness.fst.checked
prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferOps.fst.checked LowStar.Buffer.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.UInt128.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Endianness.fsti.checked FStar.Classical.fsti.checked
LowStar.Endianness.fst
LowStar.Monotonic.Buffer.srel LowStar.Monotonic.Buffer.mbuffer Prims.nat Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition LowStar.Monotonic.Buffer.length FStar.Seq.Base.seq FStar.Monotonic.HyperStack.mem Prims.unit Prims.l_and LowStar.Monotonic.Buffer.live LowStar.Monotonic.Buffer.modifies LowStar.Monotonic.Buffer.loc_buffer FStar.Seq.Base.equal FStar.Seq.Base.slice LowStar.Monotonic.Buffer.as_seq Prims.logical
module LowStar.Endianness

/// Stateful operations between machine integers and buffers of uint8s. Most of
/// these operations are implemented natively using the target's system endianness
/// headers, relying on macros or static inline declarations.
///
/// .. note::
///
///    This module supersedes ``C.Endianness``.

module MB = LowStar.Monotonic.Buffer
module B = LowStar.Buffer

open FStar.HyperStack.ST
open FStar.Endianness
open LowStar.BufferOps

module U8 = FStar.UInt8
module U16 = FStar.UInt16
module U32 = FStar.UInt32
module U64 = FStar.UInt64
module U128 = FStar.UInt128

module HS = FStar.HyperStack

inline_for_extraction
type u8 = U8.t
inline_for_extraction
type u16 = U16.t
inline_for_extraction
type u32 = U32.t
inline_for_extraction
type u64 = U64.t
inline_for_extraction
type u128 = U128.t

/// Byte-swapping operations
/// ------------------------
///
/// TODO these are totally unspecified

assume val htole16: u16 -> u16
assume val le16toh: u16 -> u16

assume val htole32: u32 -> u32
assume val le32toh: u32 -> u32

assume val htole64: u64 -> u64
assume val le64toh: u64 -> u64

assume val htobe16: u16 -> u16
assume val be16toh: u16 -> u16

assume val htobe32: u32 -> u32
assume val be32toh: u32 -> u32

assume val htobe64: u64 -> u64
assume val be64toh: u64 -> u64

/// Precondition for store functions
///
/// Parametrized by the predicate that different store functions can pass accordingly
///
/// Typically saying sequence contents are le_to_n or be_to_n etc.

unfold let store_pre
  (#a:Type) (#rrel #rel:MB.srel a) (b:MB.mbuffer a rrel rel)
  (i:nat) (j:nat{i + j <= MB.length b}) (predicate:Seq.seq a -> Type0)
  = fun (h:HS.mem) ->
    let sb = MB.as_seq h b in
    let len = MB.length b in

    MB.live h b /\

    (forall (s:Seq.seq a).  //monotonicity precondition that once the contents of the buffer
                       //between [i, j) are replaced as per the predicate, the
                       //preorder rel is satisfied

       (Seq.length s == len  /\
        Seq.equal (Seq.slice s 0 i) (Seq.slice sb 0 i) /\
        Seq.equal (Seq.slice s (i + j) len) (Seq.slice sb (i + j) len) /\
        predicate (Seq.slice s i (i + j)))

       ==> rel sb s)


/// Common postcondition

unfold let store_post
  (#a:Type) (#rrel #rel:MB.srel a) (b:MB.mbuffer a rrel rel)
val store_post : b: LowStar.Monotonic.Buffer.mbuffer a rrel rel ->
    i: Prims.nat ->
    j: Prims.nat{i + j <= LowStar.Monotonic.Buffer.length b} ->
    predicate: (_: FStar.Seq.Base.seq a -> Type0) ->
    h0: FStar.Monotonic.HyperStack.mem ->
    _: Prims.unit ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.logical

    b: LowStar.Monotonic.Buffer.mbuffer a rrel rel ->
    i: Prims.nat ->
    j: Prims.nat{i + j <= LowStar.Monotonic.Buffer.length b} ->
    predicate: (_: FStar.Seq.Base.seq a -> Type0) ->
    h0: FStar.Monotonic.HyperStack.mem ->
    _: Prims.unit ->
    h1: FStar.Monotonic.HyperStack.mem
  -> Prims.GTot Prims.logical