val get128_aux (ptr: int) (heap: machine_heap) (v: quad32) (k: nat{k < 16})
    : Lemma (requires get_heap_val128 ptr heap == v)
      (ensures heap.[ ptr + k ] == UInt8.v (Seq.index (put128 v) k))
let get128_aux (ptr:int) (heap:machine_heap) (v:quad32) (k:nat{k < 16}) : Lemma
  (requires get_heap_val128 ptr heap == v)
  (ensures heap.[ptr + k] == UInt8.v (Seq.index (put128 v) k)) =
  get_heap_val128_reveal ();
  get_heap_val32_reveal ();
  put128_reveal ();
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  reveal_opaque (`%le_quad32_to_bytes) le_quad32_to_bytes;
  four_to_nat_8_injective ()
val get128_aux (ptr: int) (heap: machine_heap) (v: quad32) (k: nat{k < 16})
    : Lemma (requires get_heap_val128 ptr heap == v)
      (ensures heap.[ ptr + k ] == UInt8.v (Seq.index (put128 v) k))
let get128_aux (ptr: int) (heap: machine_heap) (v: quad32) (k: nat{k < 16})
    : Lemma (requires get_heap_val128 ptr heap == v)
      (ensures heap.[ ptr + k ] == UInt8.v (Seq.index (put128 v) k)) =
get_heap_val128_reveal ();
get_heap_val32_reveal ();
put128_reveal ();
reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
reveal_opaque (`%le_quad32_to_bytes) le_quad32_to_bytes;
four_to_nat_8_injective ()
Vale.X64.BufferViewStore.fst.checked
Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Two.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Seq.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Arch.Types.fsti.checked Vale.Arch.MachineHeap.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferView.Up.fst.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Math.Lemmas.fst.checked FStar.HyperStack.fst.checked FStar.Classical.fsti.checked FStar.Calc.fsti.checked
Vale.X64.BufferViewStore.fst
Prims.int Vale.Arch.MachineHeap_s.machine_heap Vale.Def.Types_s.quad32 Prims.nat Prims.b2t Prims.op_LessThan Vale.Def.Words.Seq.four_to_nat_8_injective Prims.unit FStar.Pervasives.reveal_opaque FStar.Seq.Base.seq Vale.Def.Types_s.nat8 Prims.l_True Prims.eq2 FStar.Seq.Base.length Vale.Def.Types_s.le_quad32_to_bytes Vale.Def.Words_s.four Vale.Def.Words_s.nat8 FStar.Mul.op_Star Vale.Def.Words.Seq_s.seq_four_to_seq_LE Vale.Interop.Views.put128_reveal Vale.Arch.MachineHeap_s.get_heap_val32_reveal Vale.Arch.MachineHeap_s.get_heap_val128_reveal Vale.Arch.MachineHeap_s.get_heap_val128 Prims.squash Prims.l_or Prims.l_and Prims.op_GreaterThanOrEqual Vale.Def.Words_s.pow2_8 FStar.UInt.size FStar.UInt8.n Vale.Interop.op_String_Access Prims.op_Addition FStar.UInt8.v FStar.Seq.Base.index FStar.UInt8.t Vale.Interop.Views.put128 Prims.Nil FStar.Pervasives.pattern
module Vale.X64.BufferViewStore

open FStar.Mul
open Vale.Interop.Views
open Vale.Interop
module MB = LowStar.Monotonic.Buffer
module HS = FStar.HyperStack
open Vale.Lib.BufferViewHelpers
open Vale.Def.Types_s
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Two
open Vale.Def.Words.Four_s
open Vale.Def.Words.Seq_s
open Vale.Def.Words.Seq
open Vale.Arch.Types

open FStar.Calc

friend LowStar.BufferView.Up

#reset-options "--z3rlimit 10 --max_fuel 0 --initial_fuel 0 --max_ifuel 1 --initial_ifuel 1"

let math_aux (a b c:int) : Lemma (a + b + (c - b) == a + c) = ()

let map_aux (ptr1 ptr2:int) (v:int) (m:machine_heap) : Lemma
  (requires ptr1 == ptr2 /\ m.[ptr1] == v)
  (ensures m.[ptr2] == v) = ()

let get64_aux (ptr:int) (heap:machine_heap) (v:nat64) (k:nat{k < 8}) : Lemma
  (requires get_heap_val64 ptr heap == v)
  (ensures heap.[ptr + k] == UInt8.v (Seq.index (put64 (UInt64.uint_to_t v)) k)) =
  get_heap_val64_reveal ();
  put64_reveal ();
  le_nat64_to_bytes_reveal ();
  reveal_opaque (`%seq_four_to_seq_LE) (seq_four_to_seq_LE #nat8);
  four_to_nat_8_injective ();
  two_to_nat_32_injective ()

let get128_aux (ptr:int) (heap:machine_heap) (v:quad32) (k:nat{k < 16}) : Lemma
  (requires get_heap_val128 ptr heap == v)
val get128_aux (ptr: int) (heap: machine_heap) (v: quad32) (k: nat{k < 16})
    : Lemma (requires get_heap_val128 ptr heap == v)
      (ensures heap.[ ptr + k ] == UInt8.v (Seq.index (put128 v) k))

    ptr: Prims.int ->
    heap: Vale.Arch.MachineHeap_s.machine_heap ->
    v: Vale.Def.Types_s.quad32 ->
    k: Prims.nat{k < 16}
  -> FStar.Pervasives.Lemma (requires Vale.Arch.MachineHeap_s.get_heap_val128 ptr heap == v)
      (ensures
        heap.[ ptr + k ] == FStar.UInt8.v (FStar.Seq.Base.index (Vale.Interop.Views.put128 v) k))