val len (#a:Type0) (#rrel #rel:srel a) (b:mbuffer a rrel rel) :GTot U32.t
let len #_ #_ #_ b =
  match b with
  | Null -> 0ul
  | Buffer _ _ _ len -> len
val len (#a:Type0) (#rrel #rel:srel a) (b:mbuffer a rrel rel) :GTot U32.t
let len #_ #_ #_ b =
match b with
| Null -> 0ul
| Buffer _ _ _ len -> len
LowStar.Monotonic.Buffer.fst.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Preorder.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.ModifiesGen.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
LowStar.Monotonic.Buffer.fst
LowStar.Monotonic.Buffer.srel LowStar.Monotonic.Buffer.mbuffer FStar.UInt32.__uint_to_t FStar.UInt32.t FStar.HyperStack.ST.mreference FStar.Seq.Properties.lseq FStar.UInt32.v LowStar.Monotonic.Buffer.srel_to_lsrel FStar.Ghost.erased Prims.b2t Prims.op_LessThanOrEqual Prims.op_Addition FStar.Ghost.reveal
(*
   Copyright 2008-2018 Microsoft Research

   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.
*)
module LowStar.Monotonic.Buffer

module P = FStar.Preorder
module G = FStar.Ghost
module U32 = FStar.UInt32
module Seq = FStar.Seq

module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST

private let srel_to_lsrel (#a:Type0) (len:nat) (pre:srel a) :P.preorder (Seq.lseq a len) = pre

(*
 * Counterpart of compatible_sub from the fsti but using sequences
 *
 * The patterns are guarded tightly, the proof of transitivity gets quite flaky otherwise
 * The cost is that we have to additional asserts as triggers
 *)
let compatible_sub_preorder (#a:Type0)
  (len:nat) (rel:srel a) (i:nat) (j:nat{i <= j /\ j <= len}) (sub_rel:srel a)
  = compatible_subseq_preorder len rel i j sub_rel

(*
 * Reflexivity of the compatibility relation
 *)
let lemma_seq_sub_compatilibity_is_reflexive (#a:Type0) (len:nat) (rel:srel a)
  :Lemma (compatible_sub_preorder len rel 0 len rel)
  = assert (forall (s1 s2:Seq.seq a). Seq.length s1 == Seq.length s2 ==>
                                 Seq.equal (Seq.replace_subseq s1 0 (Seq.length s1) s2) s2)

(*
 * Transitivity of the compatibility relation
 *
 * i2 and j2 are relative offsets within [i1, j1) (i.e. assuming i1 = 0)
 *)
let lemma_seq_sub_compatibility_is_transitive (#a:Type0)
  (len:nat) (rel:srel a) (i1 j1:nat) (rel1:srel a) (i2 j2:nat) (rel2:srel a)
  :Lemma (requires (i1 <= j1 /\ j1 <= len /\ i2 <= j2 /\ j2 <= j1 - i1 /\
                    compatible_sub_preorder len rel i1 j1 rel1 /\
                    compatible_sub_preorder (j1 - i1) rel1 i2 j2 rel2))
	 (ensures  (compatible_sub_preorder len rel (i1 + i2) (i1 + j2) rel2))
  = let t1 (s1 s2:Seq.seq a) = Seq.length s1 == len /\ Seq.length s2 == len /\ rel s1 s2 in
    let t2 (s1 s2:Seq.seq a) = t1 s1 s2 /\ rel2 (Seq.slice s1 (i1 + i2) (i1 + j2)) (Seq.slice s2 (i1 + i2) (i1 + j2)) in

    let aux0 (s1 s2:Seq.seq a) :Lemma (t1 s1 s2 ==> t2 s1 s2)
      = Classical.arrow_to_impl #(t1 s1 s2) #(t2 s1 s2)
          (fun _ ->
           assert (rel1 (Seq.slice s1 i1 j1) (Seq.slice s2 i1 j1));
	   assert (rel2 (Seq.slice (Seq.slice s1 i1 j1) i2 j2) (Seq.slice (Seq.slice s2 i1 j1) i2 j2));
	   assert (Seq.equal (Seq.slice (Seq.slice s1 i1 j1) i2 j2) (Seq.slice s1 (i1 + i2) (i1 + j2)));
	   assert (Seq.equal (Seq.slice (Seq.slice s2 i1 j1) i2 j2) (Seq.slice s2 (i1 + i2) (i1 + j2))))
    in


    let t1 (s s2:Seq.seq a) = Seq.length s == len /\ Seq.length s2 == j2 - i2 /\
                              rel2 (Seq.slice s (i1 + i2) (i1 + j2)) s2 in
    let t2 (s s2:Seq.seq a) = t1 s s2 /\ rel s (Seq.replace_subseq s (i1 + i2) (i1 + j2) s2) in
    let aux1 (s s2:Seq.seq a) :Lemma (t1 s s2 ==> t2 s s2)
      = Classical.arrow_to_impl #(t1 s s2) #(t2 s s2)
          (fun _ ->
           assert (Seq.equal (Seq.slice s (i1 + i2) (i1 + j2)) (Seq.slice (Seq.slice s i1 j1) i2 j2));
           assert (rel1 (Seq.slice s i1 j1) (Seq.replace_subseq (Seq.slice s i1 j1) i2 j2 s2));
	   assert (rel s (Seq.replace_subseq s i1 j1 (Seq.replace_subseq (Seq.slice s i1 j1) i2 j2 s2)));
	   assert (Seq.equal (Seq.replace_subseq s i1 j1 (Seq.replace_subseq (Seq.slice s i1 j1) i2 j2 s2))
	                     (Seq.replace_subseq s (i1 + i2) (i1 + j2) s2)))
    in

    Classical.forall_intro_2 aux0; Classical.forall_intro_2 aux1

noeq type mbuffer (a:Type0) (rrel:srel a) (rel:srel a) :Type0 =
  | Null
  | Buffer:
    max_length:U32.t ->
    content:HST.mreference (Seq.lseq a (U32.v max_length)) (srel_to_lsrel (U32.v max_length) rrel) ->
    idx:U32.t ->
    length:Ghost.erased U32.t{U32.v idx + U32.v (Ghost.reveal length) <= U32.v max_length} ->
    mbuffer a rrel rel

let g_is_null #_ #_ #_ b = Null? b

let mnull #_ #_ #_ = Null

let null_unique #_ #_ #_ _ = ()

let unused_in #_ #_ #_ b h =
  match b with
  | Null -> False
  | Buffer _ content _ _ -> content `HS.unused_in` h

let buffer_compatible (#t: Type) (#rrel #rel: srel t) (b: mbuffer t rrel rel) : GTot Type0 =
  match b with
  | Null -> True
  | Buffer max_length content idx length ->
      compatible_sub_preorder (U32.v max_length) rrel
        (U32.v idx) (U32.v idx + U32.v length) rel  //proof of compatibility

let live #_ #rrel #rel h b =
  match b with
  | Null -> True
  | Buffer max_length content idx length ->
      h `HS.contains` content /\
      buffer_compatible b

let live_null _ _ _ _ = ()

let live_not_unused_in #_ #_ #_ _ _ = ()

let lemma_live_equal_mem_domains #_ #_ #_ _ _ _ = ()

let frameOf #_ #_ #_ b = if Null? b then HS.root else HS.frameOf (Buffer?.content b)

let as_addr #_ #_ #_  b = if g_is_null b then 0 else HS.as_addr (Buffer?.content b)

let unused_in_equiv #_ #_ #_ b h =
  if g_is_null b then Heap.not_addr_unused_in_nullptr (Map.sel (HS.get_hmap h) HS.root) else ()

let live_region_frameOf #_ #_ #_ _ _ = ()
val len (#a:Type0) (#rrel #rel:srel a) (b:mbuffer a rrel rel) :GTot U32.t
b: LowStar.Monotonic.Buffer.mbuffer a rrel rel -> Prims.GTot FStar.UInt32.t