val set_of_range (a: int) (n: nat)
    : Pure (Set.set int)
      (requires True)
      (ensures
        fun s -> (forall (i: int). {:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n))
let rec set_of_range (a:int) (n:nat) : Pure (Set.set int)
  (requires True)
  (ensures fun s -> (forall (i:int).{:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n))
  =
  if n = 0 then Set.empty else Set.union (set_of_range a (n - 1)) (Set.singleton (a + n - 1))
val set_of_range (a: int) (n: nat)
    : Pure (Set.set int)
      (requires True)
      (ensures
        fun s -> (forall (i: int). {:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n))
let rec set_of_range (a: int) (n: nat)
    : Pure (Set.set int)
      (requires True)
      (ensures
        fun s -> (forall (i: int). {:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n)) =
if n = 0 then Set.empty else Set.union (set_of_range a (n - 1)) (Set.singleton (a + n - 1))
Vale.PPC64LE.Memory_Sems.fst.checked
Vale.X64.Machine_Semantics_s.fst.checked Vale.X64.BufferViewStore.fsti.checked Vale.PPC64LE.Semantics_s.fst.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Memory.fst.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Lib.BufferViewHelpers.fst.checked Vale.Interop.Views.fsti.checked Vale.Interop.Heap_s.fst.checked Vale.Interop.Base.fst.checked Vale.Interop.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Prop_s.fst.checked Vale.Def.Opaque_s.fsti.checked Vale.Arch.MachineHeap.fsti.checked Vale.Arch.HeapImpl.fsti.checked Vale.Arch.Heap.fsti.checked prims.fst.checked LowStar.Monotonic.Buffer.fsti.checked LowStar.BufferView.Up.fsti.checked LowStar.BufferView.Down.fsti.checked FStar.UInt8.fsti.checked FStar.UInt64.fsti.checked FStar.Set.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Option.fst.checked FStar.Mul.fst.checked FStar.Map.fsti.checked FStar.List.fst.checked FStar.Classical.fsti.checked
Vale.PPC64LE.Memory_Sems.fst
Prims.int Prims.nat Prims.op_Equality FStar.Set.empty Prims.bool FStar.Set.union Vale.PPC64LE.Memory_Sems.set_of_range Prims.op_Subtraction FStar.Set.singleton Prims.op_Addition FStar.Set.set Prims.l_True Prims.l_Forall Prims.l_iff Prims.b2t FStar.Set.mem Prims.l_and Prims.op_LessThanOrEqual Prims.op_LessThan
module Vale.PPC64LE.Memory_Sems

open FStar.Mul
open Vale.Def.Prop_s
open Vale.Def.Opaque_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.Def.Words_s
module I = Vale.Interop
module S = Vale.PPC64LE.Semantics_s
module MB = LowStar.Monotonic.Buffer
module UV = LowStar.BufferView.Up
module DV = LowStar.BufferView.Down
open Vale.Lib.BufferViewHelpers
open Vale.Arch.HeapImpl
open Vale.Arch.Heap

friend Vale.PPC64LE.Memory
module IB = Vale.Interop.Base

let same_domain h m = Set.equal (IB.addrs_set (_ih h)) (Map.domain m)

let lemma_same_domains h m1 m2 = ()

let get_heap h = I.down_mem (_ih h)

let upd_heap h m = mi_heap_upd h m

//let lemma_upd_get_heap h = I.down_up_identity (_ih h)

let lemma_get_upd_heap h m = I.up_down_identity (_ih h) m

let lemma_heap_impl = ()

let lemma_heap_get_heap h = ()

let lemma_heap_taint h = ()

//let lemma_heap_upd_heap h mh mt = ()

[@"opaque_to_smt"]
let rec set_of_range (a:int) (n:nat) : Pure (Set.set int)
  (requires True)
  (ensures fun s -> (forall (i:int).{:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n))
val set_of_range (a: int) (n: nat)
    : Pure (Set.set int)
      (requires True)
      (ensures
        fun s -> (forall (i: int). {:pattern Set.mem i s} Set.mem i s <==> a <= i /\ i < a + n))
a: Prims.int -> n: Prims.nat -> Prims.Pure (FStar.Set.set Prims.int)