val modifies_stack (lo_r1 hi_r1: nat) (h h': vale_stack) : Vale.Def.Prop_s.prop0
let modifies_stack (lo_r1 hi_r1:nat) (h h':vale_stack) : Vale.Def.Prop_s.prop0 =
  forall addr . {:pattern (load_stack64 addr h') \/ (valid_src_stack64 addr h') }
    valid_src_stack64 addr h /\ (addr + 8 <= lo_r1 || addr >= hi_r1) ==>
      valid_src_stack64 addr h' /\
      load_stack64 addr h == load_stack64 addr h'
val modifies_stack (lo_r1 hi_r1: nat) (h h': vale_stack) : Vale.Def.Prop_s.prop0
let modifies_stack (lo_r1 hi_r1: nat) (h h': vale_stack) : Vale.Def.Prop_s.prop0 =
forall addr. {:pattern (load_stack64 addr h')\/(valid_src_stack64 addr h')}
  valid_src_stack64 addr h /\ (addr + 8 <= lo_r1 || addr >= hi_r1) ==>
  valid_src_stack64 addr h' /\ load_stack64 addr h == load_stack64 addr h'
Vale.PPC64LE.Stack_i.fsti.checked
Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.Def.Prop_s.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked FStar.Map.fsti.checked
Vale.PPC64LE.Stack_i.fsti
Prims.nat Vale.PPC64LE.Stack_i.vale_stack Prims.l_Forall Prims.int Prims.l_imp Prims.l_and Prims.b2t Vale.PPC64LE.Stack_i.valid_src_stack64 Prims.op_BarBar Prims.op_LessThanOrEqual Prims.op_Addition Prims.op_GreaterThanOrEqual Prims.eq2 Vale.PPC64LE.Memory.nat64 Vale.PPC64LE.Stack_i.load_stack64 Vale.Def.Prop_s.prop0
module Vale.PPC64LE.Stack_i

open FStar.Mul
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.Memory
open Vale.Def.Prop_s

val vale_stack : Type u#0

val valid_src_stack64 (ptr:int) (h:vale_stack) : GTot bool
val load_stack64 (ptr:int) (h:vale_stack) : GTot nat64
val store_stack64 (ptr:int) (v:nat64) (h:vale_stack) : GTot vale_stack
val free_stack64 (start:int) (finish:int) (h:vale_stack) : GTot vale_stack

val valid_src_stack128 (ptr:int) (h:vale_stack) : GTot bool
val load_stack128 (ptr:int) (h:vale_stack) : GTot quad32
val store_stack128 (ptr:int) (v:quad32) (h:vale_stack) : GTot vale_stack
val free_stack128 (start:int) (finish:int) (h:vale_stack) : GTot vale_stack

val init_r1 (h:vale_stack) : (n:nat64{n >= 65536})
val modifies_stack (lo_r1 hi_r1: nat) (h h': vale_stack) : Vale.Def.Prop_s.prop0

    lo_r1: Prims.nat ->
    hi_r1: Prims.nat ->
    h: Vale.PPC64LE.Stack_i.vale_stack ->
    h': Vale.PPC64LE.Stack_i.vale_stack
  -> Vale.Def.Prop_s.prop0