val writeable_mem_aux (t: base_typ) (addr: _) (ps: list b8) (h: vale_heap)
    : Ghost bool
      (requires sub_list ps (_ih h).ptrs)
      (ensures
        fun b ->
          b <==>
          (exists (x: buffer t).
              {:pattern (List.memP x ps)\/(valid_buffer t addr x h)\/buffer_writeable x}
              List.memP x ps /\ valid_buffer t addr x h /\ buffer_writeable x))
let rec writeable_mem_aux (t:base_typ) addr (ps:list b8) (h:vale_heap) : Ghost bool
  (requires sub_list ps (_ih h).ptrs)
  (ensures fun b -> b <==>
    (exists (x:buffer t). {:pattern (List.memP x ps) \/ (valid_buffer t addr x h) \/ buffer_writeable x}
      List.memP x ps /\ valid_buffer t addr x h /\ buffer_writeable x))
  =
  match ps with
  | [] -> false
  | a::q -> writeable_buffer t addr a h || writeable_mem_aux t addr q h
val writeable_mem_aux (t: base_typ) (addr: _) (ps: list b8) (h: vale_heap)
    : Ghost bool
      (requires sub_list ps (_ih h).ptrs)
      (ensures
        fun b ->
          b <==>
          (exists (x: buffer t).
              {:pattern (List.memP x ps)\/(valid_buffer t addr x h)\/buffer_writeable x}
              List.memP x ps /\ valid_buffer t addr x h /\ buffer_writeable x))
let rec writeable_mem_aux (t: base_typ) addr (ps: list b8) (h: vale_heap)
    : Ghost bool
      (requires sub_list ps (_ih h).ptrs)
      (ensures
        fun b ->
          b <==>
          (exists (x: buffer t).
              {:pattern (List.memP x ps)\/(valid_buffer t addr x h)\/buffer_writeable x}
              List.memP x ps /\ valid_buffer t addr x h /\ buffer_writeable x)) =
match ps with
| [] -> false
| a :: q -> writeable_buffer t addr a h || writeable_mem_aux t addr q h
Vale.X64.Memory.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.Machine_s.fst.checked Vale.Lib.Seqs_s.fst.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Types.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fst.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.ModifiesPat.fst.checked LowStar.Modifies.fst.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.UInt32.fsti.checked FStar.UInt16.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lib.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.HyperStack.ST.fsti.checked FStar.HyperStack.fst.checked FStar.Heap.fst.checked FStar.Ghost.fsti.checked FStar.Classical.fsti.checked
Vale.X64.Memory.fst
Vale.Arch.HeapTypes_s.base_typ Prims.int Prims.list Vale.X64.Memory.b8 Vale.Arch.HeapImpl.vale_heap Prims.op_BarBar Vale.X64.Memory.writeable_buffer Vale.X64.Memory.writeable_mem_aux Prims.bool Vale.X64.Memory.sub_list Vale.Interop.Heap_s.__proj__InteropHeap__item__ptrs Vale.Arch.HeapImpl._ih Prims.l_iff Prims.b2t Prims.l_Exists Vale.X64.Memory.buffer Prims.l_and FStar.List.Tot.Base.memP Vale.X64.Memory.valid_buffer Vale.X64.Memory.buffer_writeable
module Vale.X64.Memory
include Vale.Interop.Types
friend Vale.Arch.Heap
open Vale.Def.Opaque_s
open Vale.Arch.HeapImpl
open Vale.Arch.Heap
open Vale.Interop.Base
module IB = Vale.Interop.Base
module I = Vale.Interop
module HS = FStar.HyperStack
module HST = FStar.HyperStack.ST
module MB = LowStar.Monotonic.Buffer
module M = LowStar.Modifies
open LowStar.ModifiesPat
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
module H = FStar.Heap
module S = Vale.X64.Machine_Semantics_s

#reset-options "--initial_fuel 2 --max_fuel 2 --initial_ifuel 1 --max_ifuel 1"

let b8 = IB.b8

unfold let (.[]) = Map.sel
unfold let (.[]<-) = Map.upd

let get_heaplet_id h =
  h.heapletId

let tuint8 = UInt8.t
let tuint16 = UInt16.t
let tuint32 = UInt32.t
let tuint64 = UInt64.t

let v_of_typ (t:base_typ) (v:base_typ_as_vale_type t) : base_typ_as_type t =
  match t with
  | TUInt8 -> UInt8.uint_to_t v
  | TUInt16 -> UInt16.uint_to_t v
  | TUInt32 -> UInt32.uint_to_t v
  | TUInt64 -> UInt64.uint_to_t v
  | TUInt128 -> v

let v_to_typ (t:base_typ) (v:base_typ_as_type t) : base_typ_as_vale_type t =
  match t with
  | TUInt8 -> UInt8.v v
  | TUInt16 -> UInt16.v v
  | TUInt32 -> UInt32.v v
  | TUInt64 -> UInt64.v v
  | TUInt128 -> v

let lemma_v_to_of_typ (t:base_typ) (v:base_typ_as_vale_type t) : Lemma
  (ensures v_to_typ t (v_of_typ t v) == v)
  [SMTPat (v_to_typ t (v_of_typ t v))]
  =
  ()

let uint8_view = Vale.Interop.Views.up_view8
let uint16_view = Vale.Interop.Views.up_view16
let uint32_view = Vale.Interop.Views.up_view32
let uint64_view = Vale.Interop.Views.up_view64
let uint128_view = Vale.Interop.Views.up_view128

let uint_view (t:base_typ) : (v:UV.view UInt8.t (IB.base_typ_as_type t){UV.View?.n v == view_n t}) =
  match t with
  | TUInt8 -> uint8_view
  | TUInt16 -> uint16_view
  | TUInt32 -> uint32_view
  | TUInt64 -> uint64_view
  | TUInt128 -> uint128_view

let buffer_as_seq #t h b =
  let s = UV.as_seq (IB.hs_of_mem (_ih h)) (UV.mk_buffer (get_downview b.bsrc) (uint_view t)) in
  Vale.Lib.Seqs_s.seq_map (v_to_typ t) s

let buffer_readable #t h b = List.memP b (IB.ptrs_of_mem (_ih h))
let buffer_writeable #t b = b.writeable
let buffer_length #t b = UV.length (UV.mk_buffer (get_downview b.bsrc) (uint_view t))
let loc = M.loc
let loc_none = M.loc_none
let loc_union = M.loc_union
let loc_buffer #t b = M.loc_buffer b.bsrc
let loc_disjoint = M.loc_disjoint
let loc_includes = M.loc_includes
let modifies s h h' =
  M.modifies s (_ih h).hs (_ih h').hs /\
  h.heapletId == h'.heapletId /\
  (_ih h).ptrs == (_ih h').ptrs /\
  (_ih h).addrs == (_ih h').addrs /\
  HST.equal_domains (_ih h).hs (_ih h').hs

let buffer_addr #t b h = IB.addrs_of_mem (_ih h) b

open FStar.Mul

#set-options "--z3rlimit 20"

let index64_heap_aux (s:Seq.lseq UInt8.t 8) (heap:S.machine_heap) (ptr:int) : Lemma
  (requires forall (j:nat{j < 8}). UInt8.v (Seq.index s j) == heap.[ptr+j])
  (ensures UInt64.v (Vale.Interop.Views.get64 s) == S.get_heap_val64 ptr heap) =
  let open Vale.Def.Words.Seq_s in
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  Vale.Interop.Views.get64_reveal ();
  S.get_heap_val64_reveal ();
  Vale.Def.Types_s.le_bytes_to_nat64_reveal ()

let index_helper (x y:int) (heap:S.machine_heap) : Lemma
  (requires x == y)
  (ensures heap.[x] == heap.[y])
  =
  ()

let index_mul_helper (addr i n j:int) : Lemma
  (addr + (i * n + j) == addr + n * i + j) =
 ()

#set-options "--max_fuel 0 --max_ifuel 0"

let index64_get_heap_val64
    (h:vale_heap)
    (b:buffer64{List.memP b (_ih h).ptrs})
    (heap:S.machine_heap{IB.correct_down (_ih h) heap})
    (i:nat{i < buffer_length b})
  : Lemma (Seq.index (buffer_as_seq h b) i == S.get_heap_val64 (buffer_addr b h + scale8 i) heap)
  =
  let db = get_downview b.bsrc in
  let ub = UV.mk_buffer db uint64_view in
  let ptr = buffer_addr b h + scale8 i in
  let s = DV.as_seq (_ih h).hs db in
  let t = TUInt64 in
  let addr = buffer_addr b h in
  UV.length_eq ub;
  UV.as_seq_sel (_ih h).hs ub i;
  UV.get_sel (_ih h).hs ub i;
  let s' = Seq.slice s (i*8) (i*8 + 8) in
  let aux (j:nat{j < 8}) : Lemma (UInt8.v (Seq.index s' j) == heap.[ptr+j]) =
    assert (UInt8.v (Seq.index s (i*8 + j)) == heap.[addr + (i*8+j)]);
    Seq.lemma_index_slice s (i*8) (i*8+8) j;
    assert (UInt8.v (Seq.index s' j) == heap.[addr+(i*8+j)]);
    index_mul_helper addr i 8 j;
    ()
  in Classical.forall_intro aux;
  index64_heap_aux s' heap ptr

#set-options "--z3rlimit 50"

open Vale.Def.Words_s
open Vale.Def.Types_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Four_s
open Vale.Lib.Seqs_s

let index128_get_heap_val128_aux (s:Seq.lseq UInt8.t 16) (ptr:int) (heap:S.machine_heap) : Lemma
  (requires (forall (j:nat) . j < 16 ==> UInt8.v (Seq.index s j) == heap.[ptr+j]))
  (ensures Vale.Interop.Views.get128 s == Mkfour
    (S.get_heap_val32 ptr heap)
    (S.get_heap_val32 (ptr+4) heap)
    (S.get_heap_val32 (ptr+8) heap)
    (S.get_heap_val32 (ptr+12) heap)) =
  reveal_opaque (`%seq_to_seq_four_LE) (seq_to_seq_four_LE #nat8);
  S.get_heap_val32_reveal ();
  Vale.Interop.Views.get128_reveal ();
  Vale.Def.Types_s.le_bytes_to_quad32_reveal ()

let index128_get_heap_val128
    (h:vale_heap)
    (b:buffer128{List.memP b (_ih h).ptrs})
    (heap:S.machine_heap{IB.correct_down (_ih h) heap})
    (i:nat{i < buffer_length b})
  : Lemma
    (ensures (
      let addr = buffer_addr b h in
      Seq.index (buffer_as_seq h b) i ==
        Mkfour
          (S.get_heap_val32 (addr + scale16 i) heap)
          (S.get_heap_val32 (addr + scale16 i+4) heap)
          (S.get_heap_val32 (addr + scale16 i+8) heap)
          (S.get_heap_val32 (addr + scale16 i +12) heap)
    ))
  =
  let db = get_downview b.bsrc in
  let vb = UV.mk_buffer db uint128_view in
  let ptr = buffer_addr b h + scale16 i in
  let s = DV.as_seq (_ih h).hs db in
  let addr = buffer_addr b h in
  UV.length_eq vb;
  UV.as_seq_sel (_ih h).hs vb i;
  UV.get_sel (_ih h).hs vb i;
  let sl = Seq.slice s (i*16) (i*16+16) in
  let aux (j:nat{j < 16}) : Lemma (UInt8.v (Seq.index sl j) == heap.[ptr+j]) =
    assert (UInt8.v (Seq.index s (i*16 + j)) == heap.[addr + (i*16+j)]);
    Seq.lemma_index_slice s (i*16) (i*16+16) j;
    assert (UInt8.v (Seq.index sl j) == heap.[addr+(i*16+j)]);
    index_mul_helper addr i 16 j
  in Classical.forall_intro aux;
  index128_get_heap_val128_aux sl ptr heap

let modifies_goal_directed s h1 h2 = modifies s h1 h2
let lemma_modifies_goal_directed s h1 h2 = ()

let buffer_length_buffer_as_seq #t h b = ()

let same_underlying_seq (#t:base_typ) (h1 h2:vale_heap) (b:buffer t) : Lemma
  (requires Seq.equal (DV.as_seq (_ih h1).hs (get_downview b.bsrc)) (DV.as_seq (_ih h2).hs (get_downview b.bsrc)))
  (ensures Seq.equal (buffer_as_seq h1 b) (buffer_as_seq h2 b))
  =
  let db = get_downview b.bsrc in
  let rec aux (i:nat{i <= buffer_length b}) : Lemma
    (requires (forall (j:nat{j < i}). Seq.index (buffer_as_seq h1 b) j == Seq.index (buffer_as_seq h2 b) j) /\
    (Seq.equal (DV.as_seq (_ih h1).hs db) (DV.as_seq (_ih h2).hs db)))
    (ensures (forall (j:nat{j < buffer_length b}). Seq.index (buffer_as_seq h1 b) j == Seq.index (buffer_as_seq h2 b) j))
    (decreases %[(buffer_length b) - i]) =
    if i = buffer_length b then ()
    else (
      let bv = UV.mk_buffer db (uint_view t) in
      UV.get_sel (_ih h1).hs bv i;
      UV.get_sel (_ih h2).hs bv i;
      UV.as_seq_sel (_ih h1).hs bv i;
      UV.as_seq_sel (_ih h2).hs bv i;
      aux (i+1)
    )
  in aux 0

let modifies_buffer_elim #t1 b p h h' =
  let db = get_downview b.bsrc in
  lemma_dv_equal (down_view b.src) b.bsrc (_ih h).hs (_ih h').hs;
  same_underlying_seq h h' b;
  assert (Seq.equal (buffer_as_seq h b) (buffer_as_seq h' b))

let modifies_buffer_addr #t b p h h' = ()
let modifies_buffer_readable #t b p h h' = ()

let loc_disjoint_none_r s = M.loc_disjoint_none_r s
let loc_disjoint_union_r s s1 s2 = M.loc_disjoint_union_r s s1 s2
let loc_includes_refl s = M.loc_includes_refl s
let loc_includes_trans s1 s2 s3 = M.loc_includes_trans s1 s2 s3
let loc_includes_union_r s s1 s2 = M.loc_includes_union_r s s1 s2
let loc_includes_union_l s1 s2 s = M.loc_includes_union_l s1 s2 s
let loc_includes_union_l_buffer #t s1 s2 b = M.loc_includes_union_l s1 s2 (loc_buffer b)
let loc_includes_none s = M.loc_includes_none s
let modifies_refl s h = M.modifies_refl s (_ih h).hs
let modifies_goal_directed_refl s h = M.modifies_refl s (_ih h).hs
let modifies_loc_includes s1 h h' s2 = M.modifies_loc_includes s1 (_ih h).hs (_ih h').hs s2
let modifies_trans s12 h1 h2 s23 h3 = M.modifies_trans s12 (_ih h1).hs (_ih h2).hs s23 (_ih h3).hs

let modifies_goal_directed_trans s12 h1 h2 s13 h3 =
  modifies_trans s12 h1 h2 s13 h3;
  modifies_loc_includes s13 h1 h3 (loc_union s12 s13);
  ()

let modifies_goal_directed_trans2 s12 h1 h2 s13 h3 = modifies_goal_directed_trans s12 h1 h2 s13 h3

let default_of_typ (t:base_typ) : base_typ_as_vale_type t =
  allow_inversion base_typ;
  match t with
  | TUInt8 -> 0
  | TUInt16 -> 0
  | TUInt32 -> 0
  | TUInt64 -> 0
  | TUInt128 -> Vale.Def.Words_s.Mkfour #nat32 0 0 0 0

let buffer_read #t b i h =
  if i < 0 || i >= buffer_length b then default_of_typ t else
  Seq.index (buffer_as_seq h b) i

let seq_upd
    (#b:_)
    (h:HS.mem)
    (vb:UV.buffer b{UV.live h vb})
    (i:nat{i < UV.length vb})
    (x:b)
  : Lemma
    (Seq.equal
      (Seq.upd (UV.as_seq h vb) i x)
      (UV.as_seq (UV.upd h vb i x) vb))
  =
  let old_s = UV.as_seq h vb in
  let new_s = UV.as_seq (UV.upd h vb i x) vb in
  let upd_s = Seq.upd old_s i x in
  let rec aux (k:nat) : Lemma
    (requires (k <= Seq.length upd_s /\ (forall (j:nat). j < k ==> Seq.index upd_s j == Seq.index new_s j)))
    (ensures (forall (j:nat). j < Seq.length upd_s ==> Seq.index upd_s j == Seq.index new_s j))
    (decreases %[(Seq.length upd_s) - k]) =
    if k = Seq.length upd_s then ()
    else begin
      UV.sel_upd vb i k x h;
      UV.as_seq_sel h vb k;
      UV.as_seq_sel (UV.upd h vb i x) vb k;
      aux (k+1)
    end
  in aux 0

let buffer_write #t b i v h =
  if i < 0 || i >= buffer_length b then h else
  begin
    let view = uint_view t in
    let db = get_downview b.bsrc in
    let bv = UV.mk_buffer db view in
    UV.upd_modifies (_ih h).hs bv i (v_of_typ t v);
    UV.upd_equal_domains (_ih h).hs bv i (v_of_typ t v);
    let hs' = UV.upd (_ih h).hs bv i (v_of_typ t v) in
    let ih' = InteropHeap (_ih h).ptrs (_ih h).addrs hs' in
    let mh' = Vale.Interop.down_mem ih' in
    let h':vale_heap = ValeHeap mh' (Ghost.hide ih') h.heapletId in
    seq_upd (_ih h).hs bv i (v_of_typ t v);
    assert (Seq.equal (buffer_as_seq h' b) (Seq.upd (buffer_as_seq h b) i v));
    h'
  end

unfold let scale_t (t:base_typ) (index:int) : int = scale_by (view_n t) index

// Checks if address addr corresponds to one of the elements of buffer ptr
let addr_in_ptr (#t:base_typ) (addr:int) (ptr:buffer t) (h:vale_heap) : Ghost bool
  (requires True)
  (ensures fun b -> not b <==>
    (forall (i:int).{:pattern (scale_t t i)} 0 <= i /\ i < buffer_length ptr ==>
      addr <> (buffer_addr ptr h) + scale_t t i))
  =
  let n = buffer_length ptr in
  let base = buffer_addr ptr h in
  let rec aux (i:nat) : Tot (b:bool{not b <==> (forall j. i <= j /\ j < n ==>
    addr <> base + scale_t t j)})
    (decreases %[n-i]) =
    if i >= n then false
    else if addr = base + scale_t t i then true
    else aux (i+1)
  in aux 0

let valid_offset (t:base_typ) (n base:nat) (addr:int) (i:nat) =
  exists j.{:pattern (scale_t t j)} i <= j /\ j < n /\ base + scale_t t j == addr

let rec get_addr_in_ptr (t:base_typ) (n base addr:nat) (i:nat) : Ghost nat
  (requires valid_offset t n base addr i)
  (ensures fun j -> base + scale_t t j == addr)
  (decreases %[n - i])
  =
  if base + scale_t t i = addr then i
  else get_addr_in_ptr t n base addr (i + 1)

let valid_buffer (t:base_typ) (addr:int) (b:b8) (h:vale_heap) : GTot bool =
  DV.length (get_downview b.bsrc) % (view_n t) = 0 &&
  addr_in_ptr #t addr b h

let writeable_buffer (t:base_typ) (addr:int) (b:b8) (h:vale_heap) : GTot bool =
  valid_buffer t addr b h && b.writeable

#set-options "--max_fuel 1 --max_ifuel 1"
let sub_list (p1 p2:list 'a) = forall x. {:pattern List.memP x p2} List.memP x p1 ==> List.memP x p2

let rec valid_mem_aux (t:base_typ) addr (ps:list b8) (h:vale_heap) : Ghost bool
  (requires sub_list ps (_ih h).ptrs)
  (ensures fun b ->
    b <==> (exists (x:buffer t). {:pattern (List.memP x ps) \/ (valid_buffer t addr x h)}
      List.memP x ps /\ valid_buffer t addr x h))
  =
  match ps with
  | [] -> false
  | a::q -> valid_buffer t addr a h || valid_mem_aux t addr q h
let valid_mem (t:base_typ) addr (h:vale_heap) = valid_mem_aux t addr (_ih h).ptrs h
let valid_mem64 ptr h = valid_mem (TUInt64) ptr h

let rec find_valid_buffer_aux (t:base_typ) (addr:int) (ps:list b8) (h:vale_heap) : Ghost (option (buffer t))
  (requires sub_list ps (_ih h).ptrs)
  (ensures fun o ->
    match o with
    | None -> not (valid_mem_aux t addr ps h)
    | Some a -> valid_buffer t addr a h /\ List.memP a ps)
  =
  match ps with
  | [] -> None
  | a::q -> if valid_buffer t addr a h then Some a else find_valid_buffer_aux t addr q h

let find_valid_buffer (t:base_typ) (addr:int) (h:vale_heap) = find_valid_buffer_aux t addr (_ih h).ptrs h

let rec find_valid_buffer_aux_ps (t:base_typ) (addr:int) (ps:list b8) (h1:vale_heap) (h2:vale_heap) : Lemma
  (requires (_ih h1).ptrs == (_ih h2).ptrs /\ sub_list ps (_ih h1).ptrs)
  (ensures find_valid_buffer_aux t addr ps h1 == find_valid_buffer_aux t addr ps h2)
  =
  match ps with
  | [] -> ()
  | a::q -> find_valid_buffer_aux_ps t addr q h1 h2

let find_valid_buffer_ps (t:base_typ) (addr:int) (h1:vale_heap) (h2:vale_heap) : Lemma
  (requires (_ih h1).ptrs == (_ih h2).ptrs)
  (ensures find_valid_buffer t addr h1 == find_valid_buffer t addr h2)
  =
  find_valid_buffer_aux_ps t addr (_ih h1).ptrs h1 h2

let find_valid_buffer_valid_offset (t:base_typ) (addr:int) (h:vale_heap) : Lemma
  (ensures (
    match find_valid_buffer t addr h with
    | None -> True
    | Some a ->
      let base = buffer_addr a h in
      valid_offset t (buffer_length a) base addr 0
  ))
  =
  ()

let rec writeable_mem_aux (t:base_typ) addr (ps:list b8) (h:vale_heap) : Ghost bool
  (requires sub_list ps (_ih h).ptrs)
  (ensures fun b -> b <==>
    (exists (x:buffer t). {:pattern (List.memP x ps) \/ (valid_buffer t addr x h) \/ buffer_writeable x}
      List.memP x ps /\ valid_buffer t addr x h /\ buffer_writeable x))
val writeable_mem_aux (t: base_typ) (addr: _) (ps: list b8) (h: vale_heap)
    : Ghost bool
      (requires sub_list ps (_ih h).ptrs)
      (ensures
        fun b ->
          b <==>
          (exists (x: buffer t).
              {:pattern (List.memP x ps)\/(valid_buffer t addr x h)\/buffer_writeable x}
              List.memP x ps /\ valid_buffer t addr x h /\ buffer_writeable x))

    t: Vale.Arch.HeapTypes_s.base_typ ->
    addr: Prims.int ->
    ps: Prims.list Vale.X64.Memory.b8 ->
    h: Vale.Arch.HeapImpl.vale_heap
  -> Prims.Ghost Prims.bool