val buffer128_write (b: buffer128) (i: int) (v: quad32) (h: vale_heap)
    : Ghost vale_heap (requires buffer_readable h b /\ buffer_writeable b) (ensures fun _ -> True)
let buffer128_write (b:buffer128) (i:int) (v:quad32) (h:vale_heap) : Ghost vale_heap
  (requires buffer_readable h b /\ buffer_writeable b)
  (ensures fun _ -> True)
  =
  buffer_write b i v h
val buffer128_write (b: buffer128) (i: int) (v: quad32) (h: vale_heap)
    : Ghost vale_heap (requires buffer_readable h b /\ buffer_writeable b) (ensures fun _ -> True)
let buffer128_write (b: buffer128) (i: int) (v: quad32) (h: vale_heap)
    : Ghost vale_heap (requires buffer_readable h b /\ buffer_writeable b) (ensures fun _ -> True) =
buffer_write b i v h
Vale.PPC64LE.InsVector.fsti.checked
Vale.SHA.PPC64LE.SHA_helpers.fsti.checked Vale.PPC64LE.State.fsti.checked Vale.PPC64LE.QuickCode.fst.checked Vale.PPC64LE.Memory.fsti.checked Vale.PPC64LE.Machine_s.fst.checked Vale.PPC64LE.InsMem.fsti.checked Vale.PPC64LE.InsBasic.fsti.checked Vale.PPC64LE.Decls.fsti.checked Vale.Math.Poly2_s.fsti.checked Vale.Math.Poly2.Bits_s.fsti.checked Vale.Def.Words_s.fsti.checked Vale.Def.Words.Two_s.fsti.checked Vale.Def.Words.Seq_s.fsti.checked Vale.Def.Words.Four_s.fsti.checked Vale.Def.Types_s.fst.checked Vale.Def.Sel.fst.checked Vale.Arch.Types.fsti.checked Vale.AES.AES_common_s.fst.checked Vale.AES.AES_BE_s.fst.checked Spec.SHA2.fsti.checked Spec.Hash.Definitions.fst.checked prims.fst.checked FStar.Seq.Base.fsti.checked FStar.Seq.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Mul.fst.checked
Vale.PPC64LE.InsVector.fsti
Vale.PPC64LE.Memory.buffer128 Prims.int Vale.PPC64LE.Memory.quad32 Vale.PPC64LE.Memory.vale_heap Vale.PPC64LE.Memory.buffer_write Vale.PPC64LE.Memory.vuint128 Prims.l_and Vale.PPC64LE.Memory.buffer_readable Vale.PPC64LE.Memory.buffer_writeable Prims.l_True
module Vale.PPC64LE.InsVector
open FStar.Seq
open FStar.Mul
open Vale.Def.Words_s
open Vale.Def.Words.Two_s
open Vale.Def.Words.Four_s
open Vale.Def.Types_s
open Vale.PPC64LE.Machine_s
open Vale.PPC64LE.State
open Vale.PPC64LE.Decls
open Vale.PPC64LE.QuickCode
open Vale.PPC64LE.InsBasic
open Vale.PPC64LE.InsMem
open Vale.PPC64LE.Memory
open Vale.Def.Sel
open Spec.SHA2
open Spec.Hash.Definitions
open Vale.SHA.PPC64LE.SHA_helpers
open Vale.AES.AES_BE_s
open Vale.Math.Poly2_s
open Vale.Math.Poly2.Bits_s

let buffer128_write (b:buffer128) (i:int) (v:quad32) (h:vale_heap) : Ghost vale_heap
  (requires buffer_readable h b /\ buffer_writeable b)
  (ensures fun _ -> True)
val buffer128_write (b: buffer128) (i: int) (v: quad32) (h: vale_heap)
    : Ghost vale_heap (requires buffer_readable h b /\ buffer_writeable b) (ensures fun _ -> True)

    b: Vale.PPC64LE.Memory.buffer128 ->
    i: Prims.int ->
    v: Vale.PPC64LE.Memory.quad32 ->
    h: Vale.PPC64LE.Memory.vale_heap
  -> Prims.Ghost Vale.PPC64LE.Memory.vale_heap