val positions_valid_in_threads (threads: Armada.Threads.t) : GTot ubool
val positions_valid_in_threads (threads: Armada.Threads.t) : GTot ubool
let positions_valid_in_threads (threads: Armada.Threads.t) : GTot ubool =
  forall sender_tid receiver_tid.{:pattern sender_receiver_trigger sender_tid receiver_tid}
    sender_receiver_trigger sender_tid receiver_tid
    ==> position_valid threads sender_tid receiver_tid
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

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

let sender_receiver_trigger (sender_tid: tid_t) (receiver_tid: tid_t) : GTot bool =
  true
/
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 -> Prims.GTot Spec.Ubool.ubool
Armada.Threads.t Prims.l_Forall Armada.Base.tid_t Prims.l_imp Prims.b2t Strategies.ArmadaInvariant.PositionsValid.sender_receiver_trigger Strategies.ArmadaInvariant.PositionsValid.position_valid Spec.Ubool.ubool
let positions_valid_in_threads (threads: Armada.Threads.t) : GTot ubool =
  
forall sender_tid receiver_tid. {:pattern sender_receiver_trigger sender_tid receiver_tid}
  sender_receiver_trigger sender_tid receiver_tid ==> position_valid threads sender_tid receiver_tid