val old_to_union_loc_none:squash (old_to_union_loc OldM.loc_none == M.loc_none)
let old_to_union_loc_none : squash (old_to_union_loc OldM.loc_none == M.loc_none) =
  OldM.cloc_of_loc_none ();
  M.union_loc_of_loc_none old_and_new_cl false
val old_to_union_loc_none:squash (old_to_union_loc OldM.loc_none == M.loc_none)
let old_to_union_loc_none:squash (old_to_union_loc OldM.loc_none == M.loc_none) =
OldM.cloc_of_loc_none ();
M.union_loc_of_loc_none old_and_new_cl false
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
FStar.ModifiesGen.union_loc_of_loc_none LowStar.ToFStarBuffer.old_and_new_aloc LowStar.ToFStarBuffer.old_and_new_cl Prims.unit FStar.Modifies.cloc_of_loc_none
(*
   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
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

noextract
let old_and_new_cl_union : M.cls (M.aloc_union old_and_new_aloc) = M.cls_union old_and_new_cl

let old_to_union_loc (l: OldM.loc) : GTot (M.loc old_and_new_cl_union) =
  M.union_loc_of_loc old_and_new_cl false (OldM.cloc_of_loc l)

let new_to_union_loc (l: NewM.loc) : GTot (M.loc old_and_new_cl_union) =
  M.union_loc_of_loc old_and_new_cl true (M.raise_loc (NewM.cloc_of_loc l))

let old_to_new_modifies (old_l: OldM.loc) (new_l: NewM.loc) (h h' : HS.mem) : Lemma
  (requires (OldM.modifies old_l h h' /\ old_to_union_loc old_l == new_to_union_loc new_l))
  (ensures (NewM.modifies new_l h h'))
= OldM.modifies_to_cloc old_l h h';
  M.modifies_union_loc_of_loc old_and_new_cl false (OldM.cloc_of_loc old_l) h h';
  M.modifies_union_loc_of_loc old_and_new_cl true (M.raise_loc (NewM.cloc_of_loc new_l)) h h';
  M.modifies_raise_loc (NewM.cloc_of_loc new_l) h h';
  NewM.modifies_to_cloc new_l h h'
val old_to_union_loc_none:squash (old_to_union_loc OldM.loc_none == M.loc_none)
Prims.squash (LowStar.ToFStarBuffer.old_to_union_loc FStar.Modifies.loc_none ==
    FStar.ModifiesGen.loc_none)