val my_is_breaking_state (pc_breaking: (pc_t -> GTot bool)) (s: Armada.State.t) (tid: tid_t)
    : GTot bool
val my_is_breaking_state (pc_breaking: (pc_t -> GTot bool)) (s: Armada.State.t) (tid: tid_t)
    : GTot bool
let my_is_breaking_state
  (pc_breaking: pc_t -> GTot bool)
  (s: Armada.State.t)
  (tid: tid_t)
  : GTot bool =
  if NotStopped? s.stop_reason then
    let thread = s.threads tid in
    if ThreadStatusRunning? thread.status then
      pc_breaking thread.pc
    else
      true
  else
    true
module Strategies.RegularToAtomic.Armada.Helper

open Armada.Action
open Armada.Base
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.List.Tot
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement.Status
open Strategies.Atomic
open Strategies.RegularToAtomic
open Strategies.Semantics
open Strategies.Semantics.Armada
open Util.Behavior
open Util.List
open Util.Nth

let is_breaking_optional_pc
  (pc_breaking: pc_t -> GTot bool)
  (optional_pc: option pc_t)
  : GTot bool =
  match optional_pc with
  | Some pc -> pc_breaking pc
  | None -> true

let pc_breaking_correct_specific
  (pc_breaking: pc_t -> GTot bool)
  (ps: program_statement_t)
  : GTot bool =
     is_breaking_optional_pc pc_breaking ps.start_pc = ps.starts_atomic_block
  && is_breaking_optional_pc pc_breaking ps.end_pc = ps.ends_atomic_block
  && (implies (None? ps.end_pc) (is_breaking_optional_pc pc_breaking ps.start_pc))

let pc_breaking_correct
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  : GTot bool =
  for_all_ghost (pc_breaking_correct_specific pc_breaking) lprog.program_statements

let created_threads_initially_breaking_specific
  (pc_breaking: pc_t -> GTot bool)
  (ps: program_statement_t)
  : GTot bool =
  match ps.statement with
  | CreateThreadStatement _ initial_pc _ _ _ _ _ -> pc_breaking initial_pc
  | _ -> true

let created_threads_initially_breaking
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  : GTot bool =
  for_all_ghost (created_threads_initially_breaking_specific pc_breaking) lprog.program_statements

let actions_starting_at_pc_correct_specific
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  (action: Armada.Action.t)
  : GTot ubool =
  contains_ubool action (actions_starting_at_pc action.program_statement.start_pc)

let actions_starting_at_pc_correct
  (lprog: Armada.Program.t)
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  : GTot ubool =
  for_all_ubool (actions_starting_at_pc_correct_specific actions_starting_at_pc) (all_actions lprog.program_statements)

let starting_successors_match_path_infos_specific
  (starting_successors: list (successor_info_t armada_semantics))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
    successor.path_index < length atomic_path_infos
  /\ (index atomic_path_infos successor.path_index).path == [successor.action]

let starting_successors_match_path_infos
  (starting_successors: list (successor_info_t armada_semantics))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool
    (starting_successors_match_path_infos_specific starting_successors atomic_path_infos)
    starting_successors

let path_successor_matches_path_info
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
     successor.path_index < length atomic_path_infos
  /\ (index atomic_path_infos successor.path_index).path == append atomic_path_info.path [successor.action]

let path_successors_match_path_infos_specific
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  : GTot ubool =
  for_all_ubool (path_successor_matches_path_info atomic_path_infos atomic_path_info) atomic_path_info.successors

let path_successors_match_path_infos
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool (path_successors_match_path_infos_specific atomic_path_infos) atomic_path_infos

let is_breaking_armada_action (pc_breaking: pc_t -> GTot bool) (action: Armada.Action.t) : GTot bool =
    not action.ok
  || is_breaking_optional_pc pc_breaking action.program_statement.end_pc
  || (match action.program_statement.statement with
     | AssertFalseStatement _
     | TerminateProcessStatement _
     | TerminateThreadStatement _
     | MethodCallStatement _ _ _ _ _ true -> true
     | _ -> false)

let path_breaking_correct_specific
  (pc_breaking: pc_t -> GTot bool)
  (atomic_path_info: atomic_path_info_t armada_semantics)
  : GTot bool =
     Cons? atomic_path_info.path
  && atomic_path_info.breaking = is_breaking_armada_action pc_breaking (last atomic_path_info.path)

let path_breaking_correct
  (pc_breaking: pc_t -> GTot bool)
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot bool =
  for_all_ghost (path_breaking_correct_specific pc_breaking) atomic_path_infos

let path_atomic_index_correct
  (hprog_actions: list (list Armada.Action.t))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  : GTot ubool =
  atomic_path_info.breaking ==>
      atomic_path_info.atomic_action_index < length hprog_actions
    /\ atomic_path_info.path == index hprog_actions atomic_path_info.atomic_action_index

let path_atomic_indices_correct
  (hprog_actions: list (list Armada.Action.t))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool (path_atomic_index_correct hprog_actions) atomic_path_infos

let path_action_in_lprog
  (lprog: Armada.Program.t)
  (action: Armada.Action.t)
  : GTot ubool =
  contains_ubool action.program_statement lprog.program_statements

let path_actions_in_lprog_specific
  (lprog: Armada.Program.t)
  (atomic_path_info: atomic_path_info_t armada_semantics)
  : GTot ubool =
  for_all_ubool (path_action_in_lprog lprog) atomic_path_info.path

let path_actions_in_lprog
  (lprog: Armada.Program.t)
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool (path_actions_in_lprog_specific lprog) atomic_path_infos

let action_matches_successor
  (action: Armada.Action.t)
  (successor: successor_info_t armada_semantics)
  : GTot ubool =
  action == successor.action

let successors_include_action
  (successors: list (successor_info_t armada_semantics))
  (action: Armada.Action.t)
  : GTot ubool =
  exists_ubool (action_matches_successor action) successors

let starting_successors_reflect_action
  (pc_breaking: pc_t -> GTot bool)
  (starting_successors: list (successor_info_t armada_semantics))
  (action: Armada.Action.t)
  : GTot ubool =
  is_breaking_optional_pc pc_breaking action.program_statement.start_pc ==>
    successors_include_action starting_successors action

let starting_successors_complete
  (lprog: Armada.Program.t)
  (pc_breaking: pc_t -> GTot bool)
  (starting_successors: list (successor_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool (starting_successors_reflect_action pc_breaking starting_successors)
    (all_actions lprog.program_statements)

let path_successors_complete_specific
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  (atomic_path_info: atomic_path_info_t armada_semantics)
  : GTot ubool =
  not atomic_path_info.breaking ==>
       length atomic_path_info.path > 0
    /\ (let final_action = last atomic_path_info.path in
       let actions = actions_starting_at_pc (final_action.program_statement.end_pc) in
       for_all_ubool (successors_include_action atomic_path_info.successors) actions)

let path_successors_complete
  (actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t))
  (atomic_path_infos: list (atomic_path_info_t armada_semantics))
  : GTot ubool =
  for_all_ubool (path_successors_complete_specific actions_starting_at_pc) atomic_path_infos

noeq type regular_refines_atomic_params_t = {
  sem: semantics_t;
  lprog: program_t sem;
  hprog: program_t (make_atomic_semantics sem);
  is_breaking_state: sem.state_t -> sem.actor_t -> GTot bool;
  starting_successors: list (successor_info_t sem);
  atomic_path_infos: list (atomic_path_info_t sem);
}

noeq type armada_refines_atomic_relation_t = {
  lprog: Armada.Program.t;
  hprog: program_t (make_atomic_semantics armada_semantics);
  pc_breaking: pc_t -> GTot bool;
  actions_starting_at_pc: option pc_t -> GTot (list Armada.Action.t);
  starting_successors: list (successor_info_t armada_semantics);
  atomic_path_infos: list (atomic_path_info_t armada_semantics);

  actions_starting_at_pc_correct_proof: unit ->
    squash (actions_starting_at_pc_correct lprog actions_starting_at_pc);

  starting_successors_match_path_infos_proof: unit ->
    squash (starting_successors_match_path_infos starting_successors atomic_path_infos);

  path_successors_match_path_infos_proof: unit ->
    squash (path_successors_match_path_infos atomic_path_infos);

  path_breaking_correct_proof: unit ->
    squash (path_breaking_correct pc_breaking atomic_path_infos);

  path_atomic_indices_correct_proof: unit ->
    squash (path_atomic_indices_correct hprog.actions atomic_path_infos);

  path_actions_in_lprog_proof: unit ->
    squash (path_actions_in_lprog lprog atomic_path_infos);

  starting_successors_complete_proof: unit ->
    squash (starting_successors_complete lprog pc_breaking starting_successors);

  path_successors_complete_proof: unit ->
    squash (path_successors_complete actions_starting_at_pc atomic_path_infos);

  created_threads_initially_breaking_proof: unit ->
    squash (created_threads_initially_breaking lprog pc_breaking);

  pc_breaking_correct_proof: unit ->
    squash (pc_breaking_correct lprog pc_breaking);

  main_start_pc_breaking_proof: unit ->
    squash (pc_breaking lprog.main_start_pc);

  inits_identical_proof: unit ->
    squash (Armada.Program.init_program lprog == hprog.init_f);
}
/
Util.Nth.fst.checked Util.List.fst.checked Util.Behavior.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.RegularToAtomic.fsti.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.Status.fsti.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.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.RegularToAtomic.Armada.Helper.fst

    pc_breaking: (_: Armada.Base.pc_t -> Prims.GTot Prims.bool) ->
    s: Armada.State.t ->
    tid: Armada.Base.tid_t
  -> Prims.GTot Prims.bool
Armada.Base.pc_t Prims.bool Armada.State.t Armada.Base.tid_t Armada.State.uu___is_NotStopped Armada.State.__proj__Mkt__item__stop_reason Armada.Thread.uu___is_ThreadStatusRunning Armada.Thread.__proj__Mkt__item__status Armada.Thread.__proj__Mkt__item__pc Armada.Thread.t Armada.State.__proj__Mkt__item__threads
let my_is_breaking_state (pc_breaking: (pc_t -> GTot bool)) (s: Armada.State.t) (tid: tid_t)
    : GTot bool =
  
if NotStopped? s.stop_reason
then
  let thread = s.threads tid in
  if ThreadStatusRunning? thread.status then pc_breaking thread.pc else true
else true