val armada_path_atomic_indices_correct
      (lprog_actions_array: array_t Armada.Action.t)
      (hprog_actions_array: array_t (list Armada.Action.t))
      (atomic_path_infos: array_t armada_atomic_path_info_t)
    : GTot ubool
val armada_path_atomic_indices_correct
      (lprog_actions_array: array_t Armada.Action.t)
      (hprog_actions_array: array_t (list Armada.Action.t))
      (atomic_path_infos: array_t armada_atomic_path_info_t)
    : GTot ubool
let armada_path_atomic_indices_correct
  (lprog_actions_array: array_t Armada.Action.t)
  (hprog_actions_array: array_t (list Armada.Action.t))
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  : GTot ubool =
  for_all_array_ubool (armada_path_atomic_index_correct lprog_actions_array hprog_actions_array) atomic_path_infos
module Strategies.RegularToAtomic.Armada

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.Statement
open Armada.Thread
open Armada.Type
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Map
open Spec.Ubool
open Strategies.Atomic
open Strategies.PCIndices
open Strategies.RegularToAtomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.ImmutableArray
open Util.List
open Util.Nth
open Util.Range

type armada_successor_info_t = {
  action_index: nat;
  path_index: nat;
}

type armada_atomic_path_info_t = {
  path: list nat;
  atomic_action_index_or_successors: either nat (list armada_successor_info_t);
}

let armada_is_breaking_optional_pc
  (pc_index_breaking: array_t bool)
  (optional_pc_index: option nat)
  : GTot bool =
  match optional_pc_index with
  | Some pc_index -> if pc_index < array_len pc_index_breaking then array_index pc_index_breaking pc_index else true
  | None -> true

let armada_pc_breaking_correct_specific
  (pc_index_breaking: array_t bool)
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  let ps = action.program_statement in
     armada_is_breaking_optional_pc pc_index_breaking pc_indices.start_pc_index = ps.starts_atomic_block
  && armada_is_breaking_optional_pc pc_index_breaking pc_indices.end_pc_index = ps.ends_atomic_block
  && (implies (None? ps.end_pc) (armada_is_breaking_optional_pc pc_index_breaking pc_indices.start_pc_index))

let armada_pc_breaking_correct
  (actions_array: array_t Armada.Action.t)
  (pc_indices_array: array_t statement_pc_indices_t)
  (pc_index_breaking: array_t bool)
  : GTot bool =
  arrays_correspond (armada_pc_breaking_correct_specific pc_index_breaking) actions_array pc_indices_array

let armada_created_threads_initially_breaking_specific
  (pc_index_breaking: array_t bool)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  armada_is_breaking_optional_pc pc_index_breaking pc_indices.create_thread_initial_pc_index

let armada_created_threads_initially_breaking
  (pc_index_breaking: array_t bool)
  (pc_indices_array: array_t statement_pc_indices_t)
  : GTot bool =
  for_all_array (armada_created_threads_initially_breaking_specific pc_index_breaking) pc_indices_array

let armada_actions_starting_at_pc_correct_specific
  (action_indices_starting_at_no_pc: list nat)
  (action_indices_starting_at_pc_index: array_t (list nat))
  (action_index: nat)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
  match pc_indices.start_pc_index with
  | None -> list_contains action_index action_indices_starting_at_no_pc
  | Some pc_index ->
         pc_index < array_len action_indices_starting_at_pc_index
      && list_contains action_index (array_index action_indices_starting_at_pc_index pc_index)

let armada_actions_starting_at_pc_correct
  (action_indices_starting_at_no_pc: list nat)
  (action_indices_starting_at_pc_index: array_t (list nat))
  (pc_indices_array: array_t statement_pc_indices_t)
  : GTot bool =
  for_all_array_enumerated
    (armada_actions_starting_at_pc_correct_specific action_indices_starting_at_no_pc
      action_indices_starting_at_pc_index)
    pc_indices_array

let armada_singleton_path_matches_path_infos_specific
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  (action_index: nat)
  (optional_path_index: option nat)
  : GTot bool =
  match optional_path_index with
  | Some singleton_path_index ->
         singleton_path_index < array_len atomic_path_infos
      && (array_index atomic_path_infos singleton_path_index).path = [action_index]
  | None -> true

let armada_singleton_path_indices_match_path_infos
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  (singleton_path_indices: array_t (option nat))
  : GTot bool =
  for_all_array_enumerated
    (armada_singleton_path_matches_path_infos_specific atomic_path_infos)
    singleton_path_indices

let armada_path_successor_matches_path_info
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  (atomic_path_info: armada_atomic_path_info_t)
  (successor: armada_successor_info_t)
  : GTot bool =
     successor.path_index < array_len atomic_path_infos
  && (array_index atomic_path_infos successor.path_index).path
     = (append atomic_path_info.path [successor.action_index])

let armada_path_successors_match_path_infos_specific
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  (atomic_path_info: armada_atomic_path_info_t)
  : GTot bool =
  match atomic_path_info.atomic_action_index_or_successors with
  | Inl atomic_action_index -> true
  | Inr successors ->
    for_all_ghost (armada_path_successor_matches_path_info atomic_path_infos atomic_path_info) successors

let armada_path_successors_match_path_infos
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  : GTot bool =
  for_all_array (armada_path_successors_match_path_infos_specific atomic_path_infos) atomic_path_infos

let armada_is_breaking_action
  (pc_index_breaking: array_t bool)
  (action: Armada.Action.t)
  (pc_indices: statement_pc_indices_t)
  : GTot bool =
    not action.ok
  || armada_is_breaking_optional_pc pc_index_breaking pc_indices.end_pc_index
  || (match action.program_statement.statement with
     | AssertFalseStatement _
     | TerminateProcessStatement _
     | TerminateThreadStatement _
     | MethodCallStatement _ _ _ _ _ true -> true
     | _ -> false)

let armada_path_breaking_correct_specific
  (pc_index_breaking: array_t bool)
  (actions_array: array_t Armada.Action.t)
  (pc_indices_array: array_t statement_pc_indices_t)
  (atomic_path_info: armada_atomic_path_info_t)
  : GTot bool =
     Cons? atomic_path_info.path
  && (let action_index = last atomic_path_info.path in
         action_index < array_len actions_array
      && action_index < array_len pc_indices_array
      && (Inl? atomic_path_info.atomic_action_index_or_successors) =
           armada_is_breaking_action pc_index_breaking (array_index actions_array action_index)
             (array_index pc_indices_array action_index))

let armada_path_breaking_correct
  (pc_index_breaking: array_t bool)
  (actions_array: array_t Armada.Action.t)
  (pc_indices_array: array_t statement_pc_indices_t)
  (atomic_path_infos: array_t armada_atomic_path_info_t)
  : GTot bool =
  for_all_array (armada_path_breaking_correct_specific pc_index_breaking actions_array pc_indices_array)
    atomic_path_infos

let armada_path_entry_correct
  (actions_array: array_t Armada.Action.t)
  (action_index: nat)
  (action: Armada.Action.t)
  : GTot ubool =
  array_nth actions_array action_index == Some action

let armada_path_atomic_index_correct
  (lprog_actions_array: array_t Armada.Action.t)
  (hprog_actions_array: array_t (list Armada.Action.t))
  (atomic_path_info: armada_atomic_path_info_t)
  : GTot ubool =
  match atomic_path_info.atomic_action_index_or_successors with
  | Inl atomic_action_index ->
         atomic_action_index < array_len hprog_actions_array
      /\ lists_correspond_ubool (armada_path_entry_correct lprog_actions_array) atomic_path_info.path
           (array_index hprog_actions_array atomic_action_index)
  | Inr successors -> true
/
Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.fsti.checked Strategies.PCIndices.fst.checked Strategies.Atomic.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked FStar.List.Tot.fst.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.Armada.fsti

    lprog_actions_array: Util.ImmutableArray.array_t Armada.Action.t ->
    hprog_actions_array: Util.ImmutableArray.array_t (Prims.list Armada.Action.t) ->
    atomic_path_infos:
      Util.ImmutableArray.array_t Strategies.RegularToAtomic.Armada.armada_atomic_path_info_t
  -> Prims.GTot Spec.Ubool.ubool
Util.ImmutableArray.array_t Armada.Action.t Prims.list Strategies.RegularToAtomic.Armada.armada_atomic_path_info_t Util.ImmutableArray.for_all_array_ubool Strategies.RegularToAtomic.Armada.armada_path_atomic_index_correct Spec.Ubool.ubool
let armada_path_atomic_indices_correct
      (lprog_actions_array: array_t Armada.Action.t)
      (hprog_actions_array: array_t (list Armada.Action.t))
      (atomic_path_infos: array_t armada_atomic_path_info_t)
    : GTot ubool =
  
for_all_array_ubool (armada_path_atomic_index_correct lprog_actions_array hprog_actions_array)
  atomic_path_infos