val lemma_arefs_2: s1:TSet.set abuffer -> s2:TSet.set abuffer -> Lemma
  (requires True)
  (ensures  (arefs (s1 ++ s2) == Set.union (arefs s1) (arefs s2)))
  [SMTPatOr [
    [SMTPat (arefs (s2 ++ s1))];
    [SMTPat (arefs (s1 ++ s2))]
  ]]
let lemma_arefs_2 s1 s2 =
  Set.lemma_equal_intro (arefs (s1 ++ s2)) (Set.union (arefs s1) (arefs s2))
val lemma_arefs_2: s1:TSet.set abuffer -> s2:TSet.set abuffer -> Lemma
  (requires True)
  (ensures  (arefs (s1 ++ s2) == Set.union (arefs s1) (arefs s2)))
  [SMTPatOr [
    [SMTPat (arefs (s2 ++ s1))];
    [SMTPat (arefs (s1 ++ s2))]
  ]]
let lemma_arefs_2 s1 s2 =
Set.lemma_equal_intro (arefs (s1 ++ s2)) (Set.union (arefs s1) (arefs s2))
FStar.Buffer.fst.checked
prims.fst.checked FStar.UInt32.fsti.checked FStar.UInt.fsti.checked FStar.TSet.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Map.fsti.checked FStar.List.Tot.fst.checked FStar.Int32.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
FStar.Buffer.fst
FStar.TSet.set FStar.Buffer.abuffer FStar.Set.lemma_equal_intro Prims.nat FStar.Buffer.arefs FStar.Buffer.op_Plus_Plus FStar.Set.union Prims.unit
(*
   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 FStar.Buffer
 
open FStar.Seq
open FStar.UInt32
module Int32 = FStar.Int32
open FStar.HyperStack
open FStar.HyperStack.ST
open FStar.Ghost


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

#set-options "--initial_fuel 0 --max_fuel 0"

//17-01-04 usage? move to UInt? 
let lemma_size (x:int) : Lemma (requires (UInt.size x n))
				     (ensures (x >= 0))
				     [SMTPat (UInt.size x n)]
  = ()

let lseq (a: Type) (l: nat) : Type =
  (s: seq a { Seq.length s == l } )

(* Buffer general type, fully implemented on FStar's arrays *)
noeq private type _buffer (a:Type) =
  | MkBuffer: max_length:UInt32.t
    -> content:reference (lseq a (v max_length))
    -> idx:UInt32.t
    -> length:UInt32.t{v idx + v length <= v max_length}
    -> _buffer a

(* Exposed buffer type *)
type buffer (a:Type) = _buffer a

(* Ghost getters for specifications *)
// TODO: remove `contains` after replacing all uses with `live`
let contains #a h (b:buffer a) : GTot Type0 = HS.contains h b.content
let unused_in #a (b:buffer a) h : GTot Type0 = HS.unused_in b.content h

(* In most cases `as_seq` should be used instead of this one. *)
let sel #a h (b:buffer a) : GTot (seq a) = HS.sel h b.content

let max_length #a (b:buffer a) : GTot nat = v b.max_length
let length #a (b:buffer a) : GTot nat = v b.length
let idx #a (b:buffer a) : GTot nat = v b.idx

//17-01-04 rename to container or ref? 
let content #a (b:buffer a) :
  GTot (reference (lseq a (max_length b))) = b.content

(* Lifting from buffer to reference *)
let as_ref #a (b:buffer a) = as_ref (content b)
let as_addr #a (b:buffer a) = as_addr (content b)
let frameOf #a (b:buffer a) : GTot HS.rid = HS.frameOf (content b)

(* Liveliness condition, necessary for any computation on the buffer *)
let live #a (h:mem) (b:buffer a) : GTot Type0 = HS.contains h b.content
let unmapped_in #a (b:buffer a) (h:mem) : GTot Type0 = unused_in b h

val recall: #a:Type
  -> b:buffer a{is_eternal_region (frameOf b) /\ not (is_mm b.content)} -> Stack unit
  (requires (fun m -> True))
  (ensures  (fun m0 _ m1 -> m0 == m1 /\ live m1 b))
let recall #a b = recall b.content
 
(* Ghostly access an element of the array, or the full underlying sequence *)
let as_seq #a h (b:buffer a) : GTot (s:seq a{Seq.length s == length b}) =
  Seq.slice (sel h b) (idx b) (idx b + length b)

let get #a h (b:buffer a) (i:nat{i < length b}) : GTot a =
  Seq.index (as_seq h b) i

(* Equality predicate on buffer contents, without quantifiers *)
//17-01-04 revise comment? rename?
let equal #a h (b:buffer a) h' (b':buffer a) : GTot Type0 =
  as_seq h b == as_seq h' b'

(* y is included in x / x contains y *)
let includes #a (x:buffer a) (y:buffer a) : GTot Type0 =
  x.max_length == y.max_length /\
  x.content === y.content /\
  idx y >= idx x /\
  idx x + length x >= idx y + length y

let includes_live #a h (x: buffer a) (y: buffer a)
: Lemma
  (requires (x `includes` y))
  (ensures (live h x <==> live h y))
= ()

let includes_as_seq #a h1 h2 (x: buffer a) (y: buffer a)
: Lemma
  (requires (x `includes` y /\ as_seq h1 x == as_seq h2 x))
  (ensures (as_seq h1 y == as_seq h2 y))
= Seq.slice_slice (sel h1 x) (idx x) (idx x + length x) (idx y - idx x) (idx y  - idx x + length y);
  Seq.slice_slice (sel h2 x) (idx x) (idx x + length x) (idx y - idx x) (idx y  - idx x + length y)

let includes_trans #a (x y z: buffer a)
: Lemma
  (requires (x `includes` y /\ y `includes` z))
  (ensures (x `includes` z))
= ()

(* Disjointness between two buffers *)
let disjoint #a #a' (x:buffer a) (y:buffer a') : GTot Type0 =
  frameOf x =!= frameOf y \/ as_addr x =!= as_addr y
  \/ (a == a' /\ as_addr x == as_addr y /\ frameOf x == frameOf y /\ x.max_length == y.max_length /\
     (idx x + length x <= idx y \/ idx y + length y <= idx x))

(* Disjointness is symmetric *)
let lemma_disjoint_symm #a #a' (x:buffer a) (y:buffer a') : Lemma
  (requires True)
  (ensures (disjoint x y <==> disjoint y x))
  [SMTPat (disjoint x y)]
  = ()

let lemma_disjoint_sub #a #a' (x:buffer a) (subx:buffer a) (y:buffer a') : Lemma
  (requires (includes x subx /\ disjoint x y))
  (ensures  (disjoint subx y))
  [SMTPat (disjoint subx y); SMTPat (includes x subx)]
  = ()

let lemma_disjoint_sub' #a #a' (x:buffer a) (subx:buffer a) (y:buffer a') : Lemma
  (requires (includes x subx /\ disjoint x y))
  (ensures  (disjoint subx y))
  [SMTPat (disjoint y subx); SMTPat (includes x subx)]
  = ()

val lemma_live_disjoint: #a:Type -> #a':Type -> h:mem -> b:buffer a -> b':buffer a' -> Lemma
  (requires (live h b /\ b' `unused_in` h))
  (ensures (disjoint b b'))
  [SMTPat (disjoint b b'); SMTPat (live h b)]
let lemma_live_disjoint #a #a' h b b' = ()

(* Heterogeneous buffer type *)
noeq type abuffer = | Buff: #t:Type -> b:buffer t -> abuffer

(* let empty : TSet.set abuffer = TSet.empty #abuffer *)
let only #t (b:buffer t) : Tot (TSet.set abuffer) = FStar.TSet.singleton (Buff #t b)
(* let op_Plus_Plus #a s (b:buffer a) : Tot (TSet.set abuffer) = TSet.union s (only b) *)
(* let op_Plus_Plus_Plus set1 set2 : Tot (TSet.set abuffer) = FStar.TSet.union set1 set2 *)

let op_Bang_Bang = TSet.singleton
let op_Plus_Plus = TSet.union

(* Maps a set of buffer to the set of their references *)
assume val arefs: TSet.set abuffer -> Tot (Set.set nat)

assume Arefs_def: forall (x:nat) (s:TSet.set abuffer). {:pattern (Set.mem x (arefs s))}
  Set.mem x (arefs s) <==> (exists (y:abuffer). TSet.mem y s /\ as_addr y.b == x)

val lemma_arefs_1: s:TSet.set abuffer -> Lemma
  (requires (s == TSet.empty #abuffer))
  (ensures  (arefs s == Set.empty #nat))
  [SMTPat (arefs s)]
let lemma_arefs_1 s = Set.lemma_equal_intro (arefs s) (Set.empty)

val lemma_arefs_2: s1:TSet.set abuffer -> s2:TSet.set abuffer -> Lemma
  (requires True)
  (ensures  (arefs (s1 ++ s2) == Set.union (arefs s1) (arefs s2)))
  [SMTPatOr [
    [SMTPat (arefs (s2 ++ s1))];
    [SMTPat (arefs (s1 ++ s2))]
  ]]
val lemma_arefs_2: s1:TSet.set abuffer -> s2:TSet.set abuffer -> Lemma
  (requires True)
  (ensures  (arefs (s1 ++ s2) == Set.union (arefs s1) (arefs s2)))
  [SMTPatOr [
    [SMTPat (arefs (s2 ++ s1))];
    [SMTPat (arefs (s1 ++ s2))]
  ]]
s1: FStar.TSet.set FStar.Buffer.abuffer -> s2: FStar.TSet.set FStar.Buffer.abuffer
  -> FStar.Pervasives.Lemma
      (ensures
        FStar.Buffer.arefs (s1 ++ s2) ==
        FStar.Set.union (FStar.Buffer.arefs s1) (FStar.Buffer.arefs s2))
      [
        SMTPatOr [
            [SMTPat (FStar.Buffer.arefs (s2 ++ s1))];
            [SMTPat (FStar.Buffer.arefs (s1 ++ s2))]
          ]
      ]