val modifies_stacktaint (lo_r1 hi_r1: nat) (h h': memtaint) : Vale.Def.Prop_s.prop0
let modifies_stacktaint (lo_r1 hi_r1:nat) (h h':memtaint) : Vale.Def.Prop_s.prop0 =
  forall addr t. {:pattern (valid_taint_stack64 addr t h') }
    (addr + 8 <= lo_r1 || addr >= hi_r1) ==>
      valid_taint_stack64 addr t h == valid_taint_stack64 addr t h'
val modifies_stacktaint (lo_r1 hi_r1: nat) (h h': memtaint) : Vale.Def.Prop_s.prop0
let modifies_stacktaint (lo_r1 hi_r1: nat) (h h': memtaint) : Vale.Def.Prop_s.prop0 =
forall addr t. {:pattern (valid_taint_stack64 addr t h')}
  (addr + 8 <= lo_r1 || addr >= hi_r1) ==>
  valid_taint_stack64 addr t h == valid_taint_stack64 addr t 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.Memory.memtaint Prims.l_Forall Prims.int Vale.Arch.HeapTypes_s.taint Prims.l_imp Prims.b2t Prims.op_BarBar Prims.op_LessThanOrEqual Prims.op_Addition Prims.op_GreaterThanOrEqual Prims.eq2 Vale.Def.Prop_s.prop0 Vale.PPC64LE.Stack_i.valid_taint_stack64
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'

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

(* Validity preservation *)

val lemma_store_stack_same_valid64 (ptr:int) (v:nat64) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack64 i h /\
    (i >= ptr + 8 \/ i + 8 <= ptr))
  (ensures valid_src_stack64 i (store_stack64 ptr v h))
  [SMTPat (valid_src_stack64 i (store_stack64 ptr v h))]

val lemma_free_stack_same_valid64 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack64 ptr h /\
    (ptr >= finish \/ ptr + 8 <= start))
  (ensures valid_src_stack64 ptr (free_stack64 start finish h))
  [SMTPat (valid_src_stack64 ptr (free_stack64 start finish h))]

val lemma_store_stack_same_valid128 (ptr:int) (v:quad32) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack128 i h /\
    (i >= ptr + 16 \/ i + 16 <= ptr))
  (ensures valid_src_stack128 i (store_stack128 ptr v h))
  [SMTPat (valid_src_stack128 i (store_stack128 ptr v h))]

val lemma_free_stack_same_valid128 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures valid_src_stack128 ptr (free_stack128 start finish h))
  [SMTPat (valid_src_stack128 ptr (free_stack128 start finish h))]

(* Validity update *)

val lemma_store_new_valid64 (ptr:int) (v:nat64) (h:vale_stack) : Lemma
  (valid_src_stack64 ptr (store_stack64 ptr v h))
  [SMTPat (valid_src_stack64 ptr (store_stack64 ptr v h))]

val lemma_store_new_valid128 (ptr:int) (v:quad32) (h:vale_stack) : Lemma
  (valid_src_stack128 ptr (store_stack128 ptr v h))
  [SMTPat (valid_src_stack128 ptr (store_stack128 ptr v h))]

(* Classic select/update lemmas *)
val lemma_correct_store_load_stack64 (ptr:int) (v:nat64) (h:vale_stack) : Lemma
  (load_stack64 ptr (store_stack64 ptr v h) == v)
  [SMTPat (load_stack64 ptr (store_stack64 ptr v h))]

val lemma_frame_store_load_stack64 (ptr:int) (v:nat64) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack64 i h /\
    (i >= ptr + 8 \/ i + 8 <= ptr))
  (ensures (load_stack64 i (store_stack64 ptr v h) == load_stack64 i h))
  [SMTPat (load_stack64 i (store_stack64 ptr v h))]

val lemma_free_stack_same_load64 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack64 ptr h /\
    (ptr >= finish \/ ptr + 8 <= start))
  (ensures load_stack64 ptr h == load_stack64 ptr (free_stack64 start finish h))
  [SMTPat (load_stack64 ptr (free_stack64 start finish h))]

val lemma_correct_store_load_stack128 (ptr:int) (v:quad32) (h:vale_stack) : Lemma
  (load_stack128 ptr (store_stack128 ptr v h) == v)
  [SMTPat (load_stack128 ptr (store_stack128 ptr v h))]

val lemma_frame_store_load_stack128 (ptr:int) (v:quad32) (h:vale_stack) (i:int) : Lemma
  (requires valid_src_stack128 i h /\
    (i >= ptr + 16 \/ i + 16 <= ptr))
  (ensures (load_stack128 i (store_stack128 ptr v h) == load_stack128 i h))
  [SMTPat (load_stack128 i (store_stack128 ptr v h))]

val lemma_free_stack_same_load128 (start:int) (finish:int) (ptr:int) (h:vale_stack) : Lemma
  (requires valid_src_stack128 ptr h /\
    (ptr >= finish \/ ptr + 16 <= start))
  (ensures load_stack128 ptr h == load_stack128 ptr (free_stack128 start finish h))
  [SMTPat (load_stack128 ptr (free_stack128 start finish h))]

(* Free composition *)
val lemma_compose_free_stack64 (start:int) (inter:int) (finish:int) (h:vale_stack) : Lemma
  (requires start <= inter /\ inter <= finish)
  (ensures free_stack64 inter finish (free_stack64 start inter h) == free_stack64 start finish h)
  [SMTPat (free_stack64 inter finish (free_stack64 start inter h))]

(* Preservation of the initial stack pointer *)
val lemma_same_init_r1_free_stack64 (start:int) (finish:int) (h:vale_stack) : Lemma
  (init_r1 (free_stack64 start finish h) == init_r1 h)
  [SMTPat (init_r1 (free_stack64 start finish h))]

val lemma_same_init_r1_store_stack64 (ptr:int) (v:nat64) (h:vale_stack) : Lemma
  (init_r1 (store_stack64 ptr v h) == init_r1 h)
  [SMTPat (init_r1 (store_stack64 ptr v h))]

val lemma_same_init_r1_free_stack128 (start:int) (finish:int) (h:vale_stack) : Lemma
  (init_r1 (free_stack128 start finish h) == init_r1 h)
  [SMTPat (init_r1 (free_stack128 start finish h))]

val lemma_same_init_r1_store_stack128 (ptr:int) (v:quad32) (h:vale_stack) : Lemma
  (init_r1 (store_stack128 ptr v h) == init_r1 h)
  [SMTPat (init_r1 (store_stack128 ptr v h))]

// Taint for the stack

val valid_taint_stack64 (ptr:int) (t:taint) (stackTaint:memtaint) : GTot prop0
val valid_taint_stack128 (ptr:int) (t:taint) (stackTaint:memtaint) : GTot prop0
val store_taint_stack64 (ptr:int) (t:taint) (stackTaint:memtaint) : GTot memtaint

val store_taint_stack128 (ptr:int) (t:taint) (stackTaint:memtaint) : GTot memtaint

val lemma_valid_taint_stack64 (ptr:int) (t:taint) (stackTaint:memtaint) : Lemma
  (requires valid_taint_stack64 ptr t stackTaint)
  (ensures forall i.{:pattern Map.sel stackTaint i} i >= ptr /\ i < ptr + 8 ==> Map.sel stackTaint i == t)

val lemma_valid_taint_stack128 (ptr:int) (t:taint) (stackTaint:memtaint) : Lemma
  (requires valid_taint_stack128 ptr t stackTaint)
  (ensures forall i.{:pattern Map.sel stackTaint i} i >= ptr /\ i < ptr + 16 ==> Map.sel stackTaint i == t)

val lemma_valid_taint_stack64_reveal (ptr:int) (t:taint) (stackTaint:memtaint) : Lemma
  (requires forall i.{:pattern Map.sel stackTaint i} i >= ptr /\ i < ptr + 8 ==> Map.sel stackTaint i == t)
  (ensures valid_taint_stack64 ptr t stackTaint)

val lemma_correct_store_load_taint_stack64 (ptr:int) (t:taint) (stackTaint:memtaint) : Lemma
  (valid_taint_stack64 ptr t (store_taint_stack64 ptr t stackTaint))
  [SMTPat (valid_taint_stack64 ptr t (store_taint_stack64 ptr t stackTaint))]

val lemma_frame_store_load_taint_stack64 (ptr:int) (t:taint) (stackTaint:memtaint) (i:int) (t':taint) : Lemma
  (requires i >= ptr + 8 \/ i + 8 <= ptr)
  (ensures valid_taint_stack64 i t' stackTaint == valid_taint_stack64 i t' (store_taint_stack64 ptr t stackTaint))
  [SMTPat (valid_taint_stack64 i t' (store_taint_stack64 ptr t stackTaint))]

val lemma_valid_taint_stack128_reveal (ptr:int) (t:taint) (stackTaint:memtaint) : Lemma
  (requires forall i.{:pattern Map.sel stackTaint i} i >= ptr /\ i < ptr + 16 ==> Map.sel stackTaint i == t)
  (ensures valid_taint_stack128 ptr t stackTaint)

val lemma_correct_store_load_taint_stack128 (ptr:int) (t:taint) (stackTaint:memtaint) : Lemma
  (valid_taint_stack128 ptr t (store_taint_stack128 ptr t stackTaint))
  [SMTPat (valid_taint_stack128 ptr t (store_taint_stack128 ptr t stackTaint))]

val lemma_frame_store_load_taint_stack128 (ptr:int) (t:taint) (stackTaint:memtaint) (i:int) (t':taint) : Lemma
  (requires i >= ptr + 16 \/ i + 16 <= ptr)
  (ensures valid_taint_stack128 i t' stackTaint == valid_taint_stack128 i t' (store_taint_stack128 ptr t stackTaint))
  [SMTPat (valid_taint_stack128 i t' (store_taint_stack128 ptr t stackTaint))]

let valid_stack_slot64 (ptr:int) (h:vale_stack) (t:taint) (stackTaint:memtaint) =
  valid_src_stack64 ptr h /\ valid_taint_stack64 ptr t stackTaint

let valid_stack_slot64s (base num_slots:nat) (h:vale_stack) (t:taint) (stackTaint:memtaint) : Vale.Def.Prop_s.prop0 =
  forall addr . {:pattern (valid_src_stack64 addr h) \/ (valid_taint_stack64 addr t stackTaint) \/
    (valid_stack_slot64 addr h t stackTaint)}
    (base <= addr) && (addr < base + num_slots * 8) && (addr - base) % 8 = 0 ==>
      valid_src_stack64 addr h /\ valid_taint_stack64 addr t stackTaint
val modifies_stacktaint (lo_r1 hi_r1: nat) (h h': memtaint) : Vale.Def.Prop_s.prop0

    lo_r1: Prims.nat ->
    hi_r1: Prims.nat ->
    h: Vale.PPC64LE.Memory.memtaint ->
    h': Vale.PPC64LE.Memory.memtaint
  -> Vale.Def.Prop_s.prop0