val position_valid (threads: Armada.Threads.t) (sender_tid receiver_tid: tid_t) : GTot bool
val position_valid (threads: Armada.Threads.t) (sender_tid receiver_tid: tid_t) : GTot bool
let position_valid (threads: Armada.Threads.t) (sender_tid: tid_t) (receiver_tid: tid_t) : GTot bool =
  let sender_thread = threads sender_tid in
  let receiver_thread = threads receiver_tid in
  let position = receiver_thread.position_in_other_write_buffers sender_tid in
  position <= length sender_thread.write_buffer
module Strategies.ArmadaInvariant.PositionsValid

open Armada.Base
open Armada.Computation
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Type
open FStar.Sequence.Base
open Spec.Ubool
/
Spec.Ubool.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked
Strategies.ArmadaInvariant.PositionsValid.fsti
threads: Armada.Threads.t -> sender_tid: Armada.Base.tid_t -> receiver_tid: Armada.Base.tid_t
  -> Prims.GTot Prims.bool
Armada.Threads.t Armada.Base.tid_t Prims.op_LessThanOrEqual FStar.Sequence.Base.length Armada.Thread.write_message_t Armada.Thread.__proj__Mkt__item__write_buffer Prims.nat Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers Armada.Thread.t Prims.bool
let position_valid (threads: Armada.Threads.t) (sender_tid receiver_tid: tid_t) : GTot bool =
  
let sender_thread = threads sender_tid in
let receiver_thread = threads receiver_tid in
let position = receiver_thread.position_in_other_write_buffers sender_tid in
position <= length sender_thread.write_buffer