val valid_src_stack64s (base num_slots: nat) (h: vale_stack) : Vale.Def.Prop_s.prop0
let valid_src_stack64s (base num_slots:nat) (h:vale_stack) : Vale.Def.Prop_s.prop0 =
  forall addr . {:pattern (valid_src_stack64 addr h)}
    (base <= addr) && (addr < base + num_slots * 8) && (addr - base) % 8 = 0 ==>
      valid_src_stack64 addr h
val valid_src_stack64s (base num_slots: nat) (h: vale_stack) : Vale.Def.Prop_s.prop0
let valid_src_stack64s (base num_slots: nat) (h: vale_stack) : Vale.Def.Prop_s.prop0 =
forall addr. {:pattern (valid_src_stack64 addr h)}
  (base <= addr) && (addr < base + num_slots * 8) && (addr - base) % 8 = 0 ==>
  valid_src_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.b2t Prims.op_AmpAmp Prims.op_LessThanOrEqual Prims.op_LessThan Prims.op_Addition FStar.Mul.op_Star Prims.op_Equality Prims.op_Modulus Prims.op_Subtraction Vale.PPC64LE.Stack_i.valid_src_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})

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 valid_src_stack64s (base num_slots: nat) (h: vale_stack) : Vale.Def.Prop_s.prop0
base: Prims.nat -> num_slots: Prims.nat -> h: Vale.PPC64LE.Stack_i.vale_stack
  -> Vale.Def.Prop_s.prop0