val live_same_addresses_equal_types_and_preorders
  (#a1 #a2: Type0)
  (#rrel1 #rel1: srel a1)
  (#rrel2 #rel2: srel a2)
  (b1: mbuffer a1 rrel1 rel1)
  (b2: mbuffer a2 rrel2 rel2)
  (h: HS.mem)
: Lemma
  ((frameOf b1 == frameOf b2 /\ as_addr b1 == as_addr b2 /\ live h b1 /\ live h b2 /\ (~ (g_is_null b1 /\ g_is_null b2))) ==> (a1 == a2 /\ rrel1 == rrel2))
let live_same_addresses_equal_types_and_preorders
  #_ #_ #_ #_ #_ #_ b1 b2 h
= Classical.move_requires (live_same_addresses_equal_types_and_preorders' b1 b2) h
val live_same_addresses_equal_types_and_preorders
  (#a1 #a2: Type0)
  (#rrel1 #rel1: srel a1)
  (#rrel2 #rel2: srel a2)
  (b1: mbuffer a1 rrel1 rel1)
  (b2: mbuffer a2 rrel2 rel2)
  (h: HS.mem)
: Lemma
  ((frameOf b1 == frameOf b2 /\ as_addr b1 == as_addr b2 /\ live h b1 /\ live h b2 /\ (~ (g_is_null b1 /\ g_is_null b2))) ==> (a1 == a2 /\ rrel1 == rrel2))
let live_same_addresses_equal_types_and_preorders #_ #_ #_ #_ #_ #_ b1 b2 h =
Classical.move_requires (live_same_addresses_equal_types_and_preorders' b1 b2) h
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.Monotonic.HyperStack.mem FStar.Classical.move_requires Prims.l_and Prims.eq2 FStar.Monotonic.HyperHeap.rid LowStar.Monotonic.Buffer.frameOf Prims.nat LowStar.Monotonic.Buffer.as_addr LowStar.Monotonic.Buffer.live Prims.l_not Prims.b2t LowStar.Monotonic.Buffer.g_is_null FStar.Preorder.relation FStar.Seq.Base.seq Prims.l_or FStar.Preorder.preorder_rel LowStar.Monotonic.Buffer.live_same_addresses_equal_types_and_preorders' 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 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 #_ #_ #_ _ _ = ()

let len #_ #_ #_ b =
  match b with
  | Null -> 0ul
  | Buffer _ _ _ len -> len

let len_null a _ _ = ()

let as_seq #_ #_ #_ h b =
  match b with
  | Null -> Seq.empty
  | Buffer max_len content idx len ->
    Seq.slice (HS.sel h content) (U32.v idx) (U32.v idx + U32.v len)

let length_as_seq #_ #_ #_ _ _ = ()

let mbuffer_injectivity_in_first_preorder () = ()

let mgsub #a #rrel #rel sub_rel b i len =
  match b with
  | Null -> Null
  | Buffer max_len content idx length ->
    Buffer max_len content (U32.add idx i) (Ghost.hide len)

let live_gsub #_ #rrel #rel _ b i len sub_rel =
  match b with
  | Null -> ()
  | Buffer max_len content idx length ->
    let prf () : Lemma
      (requires (buffer_compatible b))
      (ensures (buffer_compatible (mgsub sub_rel b i len)))
    =
    lemma_seq_sub_compatibility_is_transitive (U32.v max_len) rrel
                                              (U32.v idx) (U32.v idx + U32.v length) rel
		         	              (U32.v i) (U32.v i + U32.v len) sub_rel
    in
    Classical.move_requires prf ()

let gsub_is_null #_ #_ #_ _ _ _ _ = ()

let len_gsub #_ #_ #_ _ _ _ _ = ()

let frameOf_gsub #_ #_ #_ _ _ _ _ = ()

let as_addr_gsub #_ #_ #_ _ _ _ _ = ()

let mgsub_inj #_ #_ #_ _ _ _ _ _ _ _ _ = ()

#push-options "--z3rlimit 20"
let gsub_gsub #_ #_ #rel b i1 len1 sub_rel1 i2 len2 sub_rel2 =
  let prf () : Lemma
    (requires (compatible_sub b i1 len1 sub_rel1 /\  compatible_sub (mgsub sub_rel1 b i1 len1) i2 len2 sub_rel2))
    (ensures (compatible_sub b (U32.add i1 i2) len2 sub_rel2))
  =
  lemma_seq_sub_compatibility_is_transitive (length b) rel (U32.v i1) (U32.v i1 + U32.v len1) sub_rel1
                                            (U32.v i2) (U32.v i2 + U32.v len2) sub_rel2
  in
  Classical.move_requires prf ()
#pop-options

/// A buffer ``b`` is equal to its "largest" sub-buffer, at index 0 and
/// length ``len b``.

let gsub_zero_length #_ #_ #rel b = lemma_seq_sub_compatilibity_is_reflexive (length b) rel

let as_seq_gsub #_ #_ #_ h b i len _ =
  match b with
  | Null -> ()
  | Buffer _ content idx len0 ->
    Seq.slice_slice (HS.sel h content) (U32.v idx) (U32.v idx + U32.v len0) (U32.v i) (U32.v i + U32.v len)

let lemma_equal_instances_implies_equal_types (a:Type) (b:Type) (s1:Seq.seq a) (s2:Seq.seq b)
  : Lemma (requires s1 === s2)
          (ensures a == b)
  = Seq.lemma_equal_instances_implies_equal_types ()

let s_lemma_equal_instances_implies_equal_types (_:unit)
  : Lemma (forall (a:Type) (b:Type) (s1:Seq.seq a) (s2:Seq.seq b).
          {:pattern (has_type s1 (Seq.seq a));
                    (has_type s2 (Seq.seq b)) }
          s1 === s2 ==> a == b)
  = Seq.lemma_equal_instances_implies_equal_types()
  
let live_same_addresses_equal_types_and_preorders'
  (#a1 #a2: Type0)
  (#rrel1 #rel1: srel a1)
  (#rrel2 #rel2: srel a2)
  (b1: mbuffer a1 rrel1 rel1)
  (b2: mbuffer a2 rrel2 rel2)
  (h: HS.mem)
: Lemma
  (requires 
    frameOf b1 == frameOf b2 /\
    as_addr b1 == as_addr b2 /\
    live h b1 /\
    live h b2 /\
    (~ (g_is_null b1 /\ g_is_null b2)))
  (ensures 
    a1 == a2 /\
    rrel1 == rrel2)
=   Heap.lemma_distinct_addrs_distinct_preorders ();
    Heap.lemma_distinct_addrs_distinct_mm ();
    let s1 : Seq.seq a1 = as_seq h b1 in
    assert (Seq.seq a1 == Seq.seq a2);
    let s1' : Seq.seq a2 = coerce_eq _ s1 in
    assert (s1 === s1');
    lemma_equal_instances_implies_equal_types a1 a2 s1 s1'

let live_same_addresses_equal_types_and_preorders
val live_same_addresses_equal_types_and_preorders
  (#a1 #a2: Type0)
  (#rrel1 #rel1: srel a1)
  (#rrel2 #rel2: srel a2)
  (b1: mbuffer a1 rrel1 rel1)
  (b2: mbuffer a2 rrel2 rel2)
  (h: HS.mem)
: Lemma
  ((frameOf b1 == frameOf b2 /\ as_addr b1 == as_addr b2 /\ live h b1 /\ live h b2 /\ (~ (g_is_null b1 /\ g_is_null b2))) ==> (a1 == a2 /\ rrel1 == rrel2))

    b1: LowStar.Monotonic.Buffer.mbuffer a1 rrel1 rel1 ->
    b2: LowStar.Monotonic.Buffer.mbuffer a2 rrel2 rel2 ->
    h: FStar.Monotonic.HyperStack.mem
  -> FStar.Pervasives.Lemma
    (ensures
      LowStar.Monotonic.Buffer.frameOf b1 == LowStar.Monotonic.Buffer.frameOf b2 /\
      LowStar.Monotonic.Buffer.as_addr b1 == LowStar.Monotonic.Buffer.as_addr b2 /\
      LowStar.Monotonic.Buffer.live h b1 /\ LowStar.Monotonic.Buffer.live h b2 /\
      ~(LowStar.Monotonic.Buffer.g_is_null b1 /\ LowStar.Monotonic.Buffer.g_is_null b2) ==>
      a1 == a2 /\ rrel1 == rrel2)