val old_and_new_cl (is_new: bool) : Tot (M.cls (old_and_new_aloc is_new))
let old_and_new_cl (is_new: bool) : Tot (M.cls (old_and_new_aloc is_new)) =
  if is_new then M.raise_cls NewM.cloc_cls else OldM.cloc_cls
val old_and_new_cl (is_new: bool) : Tot (M.cls (old_and_new_aloc is_new))
let old_and_new_cl (is_new: bool) : Tot (M.cls (old_and_new_aloc is_new)) =
if is_new then M.raise_cls NewM.cloc_cls else OldM.cloc_cls
LowStar.ToFStarBuffer.fst.checked
prims.fst.checked LowStar.Modifies.fst.checked LowStar.Buffer.fst.checked FStar.UInt32.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.ModifiesGen.fsti.checked FStar.Modifies.fsti.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Buffer.fst.checked
LowStar.ToFStarBuffer.fst
Prims.bool FStar.ModifiesGen.raise_cls LowStar.Monotonic.Buffer.abuffer LowStar.Monotonic.Buffer.cloc_cls FStar.Modifies.cloc_cls FStar.ModifiesGen.cls LowStar.ToFStarBuffer.old_and_new_aloc
(*
   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.ToFStarBuffer

(* WARNING: FOR TRANSITIONAL PURPOSES ONLY *)

module Old = FStar.Buffer
module OldM = FStar.Modifies
module New = LowStar.Buffer
module NewM = LowStar.Modifies
module HST = FStar.HyperStack.ST
module HS = FStar.HyperStack
module U32 = FStar.UInt32

assume val new_to_old_ghost (#t: Type0) (b: New.buffer t) : GTot (Old.buffer t)
assume val old_to_new_ghost (#t: Type0) (b: Old.buffer t) : GTot (New.buffer t)

assume val new_to_old_st (#t: Type0) (b: New.buffer t) : HST.Stack (b' : Old.buffer t { b' == new_to_old_ghost b } )
  (requires (fun h -> New.live h b))
  (ensures (fun h b' h' -> h' == h))

assume val old_to_new_st (#t: Type0) (b: Old.buffer t) : HST.Stack (b' : New.buffer t { b' == old_to_new_ghost b })
  (requires (fun h -> Old.live h b))
  (ensures (fun h b' h' -> h' == h))

assume val new_to_old_to_new (#t: Type0) (b: New.buffer t) : Lemma
  (old_to_new_ghost (new_to_old_ghost b) == b)
  [SMTPat (old_to_new_ghost (new_to_old_ghost b))]

assume val old_to_new_to_old (#t: Type0) (b: Old.buffer t) : Lemma
  (new_to_old_ghost (old_to_new_ghost b) == b)
  [SMTPat (new_to_old_ghost (old_to_new_ghost b))]

assume val live_new_to_old (#t: Type0) (h: HS.mem) (b: New.buffer t) : Lemma
  (Old.live h (new_to_old_ghost b) <==> New.live h b)
  [SMTPat (Old.live h (new_to_old_ghost b))]

assume val live_old_to_new (#t: Type0) (h: HS.mem) (b: Old.buffer t) : Lemma
  (New.live h (old_to_new_ghost b) <==> Old.live h b)
  [SMTPat (New.live h (old_to_new_ghost b))]

assume val frameOf_new_to_old (#t: Type0) (b: New.buffer t) : Lemma
  (Old.frameOf (new_to_old_ghost b) == New.frameOf b)
  [SMTPat (Old.frameOf (new_to_old_ghost b))]

assume val frameOf_old_to_new (#t: Type0) (b: Old.buffer t) : Lemma
  (New.frameOf (old_to_new_ghost b) == Old.frameOf b)
  [SMTPat (New.frameOf (old_to_new_ghost b))]

assume val as_addr_new_to_old (#t: Type0) (b: New.buffer t) : Lemma
  (Old.as_addr (new_to_old_ghost b) == New.as_addr b)
  [SMTPat (Old.as_addr (new_to_old_ghost b))]

assume val as_addr_old_to_new (#t: Type0) (b: Old.buffer t) : Lemma
  (New.as_addr (old_to_new_ghost b) == Old.as_addr b)
  [SMTPat (New.as_addr (old_to_new_ghost b))]

assume val length_new_to_old (#t: Type0) (b: New.buffer t) : Lemma
  (Old.length (new_to_old_ghost b) == New.length b)
  [SMTPat (Old.length (new_to_old_ghost b))]

assume val length_old_to_new (#t: Type0) (b: Old.buffer t) : Lemma
  (New.length (old_to_new_ghost b) == Old.length b)
  [SMTPat (New.length (old_to_new_ghost b))]

assume val as_seq_new_to_old (#t: Type0) (h: HS.mem) (b: New.buffer t) : Lemma
  (Old.as_seq h (new_to_old_ghost b) == New.as_seq h b)
  [SMTPat (Old.as_seq h (new_to_old_ghost b))]

assume val as_seq_old_to_new (#t: Type0) (h: HS.mem) (b: Old.buffer t) : Lemma
  (New.as_seq h (old_to_new_ghost b) == Old.as_seq h b)
  [SMTPat (New.as_seq h (old_to_new_ghost b))]

assume val gsub_new_to_old (#t: Type0) (b: New.buffer t) (i: U32.t) (len: U32.t) : Lemma
  (requires (U32.v i + U32.v len <= New.length b))
  (ensures (Old.sub (new_to_old_ghost b) i len == new_to_old_ghost (New.gsub b i len)))
  [SMTPatOr [
    [SMTPat (Old.sub (new_to_old_ghost b) i len)];
    [SMTPat (new_to_old_ghost (New.gsub b i len))];
  ]]

assume val gsub_old_to_new (#t: Type0) (b: Old.buffer t) (i: U32.t) (len: U32.t) : Lemma
  (requires (U32.v i + U32.v len <= Old.length b))
  (ensures (New.gsub (old_to_new_ghost b) i len == old_to_new_ghost (Old.sub b i len)))
  [SMTPatOr [
    [SMTPat (New.gsub (old_to_new_ghost b) i len)];
    [SMTPat (old_to_new_ghost (Old.sub b i len))];
  ]]

assume val new_to_old_includes_left (#t: Type0) (b1: New.buffer t) (b2: Old.buffer t) : Lemma
  ((new_to_old_ghost b1 `Old.includes` b2) <==> (b1 `New.includes` (old_to_new_ghost b2)))
  [SMTPatOr [
    [SMTPat (new_to_old_ghost b1 `Old.includes` b2)];
    [SMTPat (b1 `New.includes` old_to_new_ghost b2)];
  ]]

assume val new_to_old_includes_right (#t: Type0) (b1: Old.buffer t) (b2: New.buffer t) : Lemma
  ((b1 `Old.includes` (new_to_old_ghost b2)) <==> (old_to_new_ghost b1 `New.includes` b2))
  [SMTPatOr [
    [SMTPat (b1 `Old.includes` new_to_old_ghost b2)];
    [SMTPat (old_to_new_ghost b1 `New.includes` b2)];
  ]]

assume val new_to_old_disjoint (#t1 #t2: Type0) (b1: New.buffer t1) (b2: Old.buffer t2) : Lemma
  ((new_to_old_ghost b1 `Old.disjoint` b2) <==> (b1 `New.disjoint` (old_to_new_ghost b2)))
  [SMTPatOr [
    [SMTPat (new_to_old_ghost b1 `Old.disjoint` b2)];
    [SMTPat (b1 `New.disjoint` old_to_new_ghost b2)];
  ]]

(* The modifies clause *)

module M = FStar.ModifiesGen

noextract
let old_and_new_aloc (is_new: bool) : Tot M.aloc_t =
  if is_new then M.raise_aloc New.abuffer else OldM.cloc_aloc

noextract
val old_and_new_cl (is_new: bool) : Tot (M.cls (old_and_new_aloc is_new))
is_new: Prims.bool -> FStar.ModifiesGen.cls (LowStar.ToFStarBuffer.old_and_new_aloc is_new)