val efficient_lactions_correspond_to_hactions
      (vs: list var_id_t)
      (tds: list object_td_t)
      (inv: invariant_t Armada.State.t)
      (pc_relation pc_return_relation: relation_t nat nat)
      (lstart_state hstart_state lend_state hend_state: efficient_thread_state_t)
      (mapper: list (haction_mapper_t vs tds inv))
      (lactions hactions: list Armada.Action.t)
      (lpc_indices hpc_indices: list statement_pc_indices_t)
    : GTot ubool (decreases hactions)
val efficient_lactions_correspond_to_hactions
      (vs: list var_id_t)
      (tds: list object_td_t)
      (inv: invariant_t Armada.State.t)
      (pc_relation pc_return_relation: relation_t nat nat)
      (lstart_state hstart_state lend_state hend_state: efficient_thread_state_t)
      (mapper: list (haction_mapper_t vs tds inv))
      (lactions hactions: list Armada.Action.t)
      (lpc_indices hpc_indices: list statement_pc_indices_t)
    : GTot ubool (decreases hactions)
let rec efficient_lactions_correspond_to_hactions
  (vs: list var_id_t)
  (tds: list object_td_t)
  (inv: invariant_t Armada.State.t)
  (pc_relation: relation_t nat nat)
  (pc_return_relation: relation_t nat nat)
  (lstart_state: efficient_thread_state_t)
  (hstart_state: efficient_thread_state_t)
  (lend_state: efficient_thread_state_t)
  (hend_state: efficient_thread_state_t)
  (mapper: list (haction_mapper_t vs tds inv))
  (lactions: list Armada.Action.t)
  (hactions: list Armada.Action.t)
  (lpc_indices: list statement_pc_indices_t)
  (hpc_indices: list statement_pc_indices_t)
  : GTot ubool
  (decreases hactions) =
  match mapper, lactions, hactions, lpc_indices, hpc_indices with
  | [], [], [], [], [] ->
        lend_state = lstart_state
      /\ hend_state = hstart_state
  | MapperMatching :: remaining_mapper, first_laction :: remaining_lactions, first_haction :: remaining_hactions,
      first_lpc_indices :: remaining_lpc_indices, first_hpc_indices :: remaining_hpc_indices ->
        efficient_laction_corresponds_to_haction vs pc_relation pc_return_relation first_laction first_haction
          first_lpc_indices first_hpc_indices
      /\ efficient_action_to_starting_thread_state first_lpc_indices = lstart_state
      /\ efficient_action_to_starting_thread_state first_hpc_indices = hstart_state
      /\ EfficientThreadStateAtPC? lstart_state
      /\ EfficientThreadStateAtPC? hstart_state
      /\ efficient_thread_states_match_per_pc_relation pc_relation
          (efficient_action_to_ending_thread_state first_laction first_lpc_indices)
          (efficient_action_to_ending_thread_state first_haction first_hpc_indices)
      /\ efficient_lactions_correspond_to_hactions vs tds inv pc_relation pc_return_relation
          (efficient_action_to_ending_thread_state first_laction first_lpc_indices)
          (efficient_action_to_ending_thread_state first_haction first_hpc_indices)
          lend_state hend_state remaining_mapper remaining_lactions remaining_hactions
          remaining_lpc_indices remaining_hpc_indices
  | MapperIntroduced witness :: remaining_mapper, _, first_haction :: remaining_hactions, _,
      first_hpc_indices :: remaining_hpc_indices ->
        first_haction.ok
      /\ efficient_action_to_starting_thread_state first_hpc_indices = hstart_state
      /\ efficient_thread_states_match_per_pc_relation pc_relation lstart_state
          (efficient_action_to_ending_thread_state first_haction first_hpc_indices)
      /\ valid_introduction_succeeds_witness vs tds inv first_haction.program_statement witness
      /\ statement_updates_gvars vs first_haction.program_statement.statement
      /\ efficient_lactions_correspond_to_hactions vs tds inv pc_relation pc_return_relation lstart_state
           (efficient_action_to_ending_thread_state first_haction first_hpc_indices) lend_state hend_state
           remaining_mapper lactions remaining_hactions lpc_indices remaining_hpc_indices
  | _, _, _, _, _ -> False
module Strategies.VarIntro.Efficient

open Armada.Action
open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaStatement.Propagate
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.Breaking
open Strategies.GlobalVars
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.VarIntro
open Strategies.Invariant
open Strategies.Invariant.Armada.AtomicSubstep
open Strategies.Nonyielding
open Strategies.PCIndices
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarIntro.Defs
open Util.ImmutableArray
open Util.List
open Util.Nth
open Util.Range
open Util.Relation

noeq type efficient_hpc_info_t (vs: list var_id_t) (tds: list object_td_t) (inv: invariant_t Armada.State.t) =
  | EfficientHPCInfoNormal: efficient_hpc_info_t vs tds inv
  | EfficientHPCInfoIntroduced:
      (idx: nat) ->
      (end_pc: nat) ->
      (introduction_succeeds_witnesses: list (introduction_succeeds_witness_t vs tds inv)) ->
      (progress: nat) ->
      efficient_hpc_info_t vs tds inv

let efficient_program_inits_match_except_global_variables
  (vs: list var_id_t)
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (hpc_to_lpc: array_t nat)
  (which_initializers_are_intros: list bool)
  (lprog: Armada.Program.t)
  (hprog: Armada.Program.t)
  (lprog_main_start_pc: nat)
  (hprog_main_start_pc: nat)
  : GTot ubool =
    lprog.main_method_id = hprog.main_method_id
  /\ array_nth hpc_to_lpc hprog_main_start_pc = Some lprog_main_start_pc
  /\ array_nth lpcs lprog_main_start_pc = Some lprog.main_start_pc
  /\ array_nth hpcs hprog_main_start_pc = Some hprog.main_start_pc
  /\ initializers_match_except_global_variables vs which_initializers_are_intros
       lprog.global_initializers hprog.global_initializers
  /\ lprog.main_stack_initializers == hprog.main_stack_initializers

let efficient_lpc_to_hpcs_contain_valid_indices
  (num_hpcs: nat)
  (lpc_to_hpcs: array_t (list nat))
  : GTot bool =
  for_all_array (for_all_ghost (fun (idx: nat) -> idx < num_hpcs)) lpc_to_hpcs

let efficient_start_pc_of_actions (pc_indices_list: list statement_pc_indices_t) : GTot (option nat) =
  match pc_indices_list with
  | [] -> None
  | pc_indices :: _ -> pc_indices.start_pc_index

let efficient_hl_pc_relation (hpc_to_lpc: array_t nat) : GTot (relation_t nat nat) =
  fun lidx hidx -> array_nth hpc_to_lpc hidx = Some lidx

let efficient_hl_pc_return_relation (hpc_to_lpc: array_t nat) (is_return_hpc: array_t bool) : GTot (relation_t nat nat) =
  fun lidx hidx -> array_nth hpc_to_lpc hidx = Some lidx && array_nth is_return_hpc hidx = Some true

let efficient_laction_corresponds_to_haction
  (vs: list var_id_t)
  (pc_relation: relation_t nat nat)
  (pc_return_relation: relation_t nat nat)
  (laction: Armada.Action.t)
  (haction: Armada.Action.t)
  (lpc_indices: statement_pc_indices_t)
  (hpc_indices: statement_pc_indices_t)
  : GTot ubool =
  let lps, hps = laction.program_statement, haction.program_statement in
     statement_effect_independent_of_global_variables vs lps.statement
  /\ efficient_program_statements_match_per_pc_relation pc_relation pc_return_relation lps hps lpc_indices hpc_indices
/
Util.Relation.fst.checked Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCIndices.fst.checked Strategies.Nonyielding.fst.checked Strategies.Invariant.Armada.AtomicSubstep.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.fst.checked Strategies.Breaking.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Propagate.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.VarIntro.Efficient.fsti

    vs: Prims.list Armada.Base.var_id_t ->
    tds: Prims.list Armada.Type.object_td_t ->
    inv: Strategies.Invariant.invariant_t Armada.State.t ->
    pc_relation: Util.Relation.relation_t Prims.nat Prims.nat ->
    pc_return_relation: Util.Relation.relation_t Prims.nat Prims.nat ->
    lstart_state: Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t ->
    hstart_state: Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t ->
    lend_state: Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t ->
    hend_state: Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t ->
    mapper: Prims.list (Strategies.VarIntro.Defs.haction_mapper_t vs tds inv) ->
    lactions: Prims.list Armada.Action.t ->
    hactions: Prims.list Armada.Action.t ->
    lpc_indices: Prims.list Strategies.PCIndices.statement_pc_indices_t ->
    hpc_indices: Prims.list Strategies.PCIndices.statement_pc_indices_t
  -> Prims.GTot Spec.Ubool.ubool
Prims.list Armada.Base.var_id_t Armada.Type.object_td_t Strategies.Invariant.invariant_t Armada.State.t Util.Relation.relation_t Prims.nat Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t Strategies.VarIntro.Defs.haction_mapper_t Armada.Action.t Strategies.PCIndices.statement_pc_indices_t FStar.Pervasives.Native.Mktuple5 Prims.l_and Prims.b2t Prims.op_Equality Strategies.VarIntro.Efficient.efficient_laction_corresponds_to_haction Strategies.ArmadaStatement.ThreadState.efficient_action_to_starting_thread_state Strategies.ArmadaStatement.ThreadState.uu___is_EfficientThreadStateAtPC Strategies.ArmadaStatement.ThreadState.efficient_thread_states_match_per_pc_relation Strategies.ArmadaStatement.ThreadState.efficient_action_to_ending_thread_state Strategies.VarIntro.Efficient.efficient_lactions_correspond_to_hactions Strategies.VarIntro.Defs.introduction_succeeds_witness_t Armada.Action.__proj__Mkt__item__ok Strategies.VarIntro.Defs.valid_introduction_succeeds_witness Armada.Action.__proj__Mkt__item__program_statement Strategies.GlobalVars.VarIntro.statement_updates_gvars Armada.Action.__proj__Mkprogram_statement_t__item__statement Prims.l_False Spec.Ubool.ubool
let rec efficient_lactions_correspond_to_hactions
      (vs: list var_id_t)
      (tds: list object_td_t)
      (inv: invariant_t Armada.State.t)
      (pc_relation pc_return_relation: relation_t nat nat)
      (lstart_state hstart_state lend_state hend_state: efficient_thread_state_t)
      (mapper: list (haction_mapper_t vs tds inv))
      (lactions hactions: list Armada.Action.t)
      (lpc_indices hpc_indices: list statement_pc_indices_t)
    : GTot ubool (decreases hactions) =
  
match mapper, lactions, hactions, lpc_indices, hpc_indices with
| [], [], [], [], [] -> lend_state = lstart_state /\ hend_state = hstart_state
| MapperMatching :: remaining_mapper,
first_laction :: remaining_lactions,
first_haction :: remaining_hactions,
first_lpc_indices :: remaining_lpc_indices,
first_hpc_indices :: remaining_hpc_indices ->
  efficient_laction_corresponds_to_haction vs
    pc_relation
    pc_return_relation
    first_laction
    first_haction
    first_lpc_indices
    first_hpc_indices /\ efficient_action_to_starting_thread_state first_lpc_indices = lstart_state /\
  efficient_action_to_starting_thread_state first_hpc_indices = hstart_state /\
  EfficientThreadStateAtPC? lstart_state /\ EfficientThreadStateAtPC? hstart_state /\
  efficient_thread_states_match_per_pc_relation pc_relation
    (efficient_action_to_ending_thread_state first_laction first_lpc_indices)
    (efficient_action_to_ending_thread_state first_haction first_hpc_indices) /\
  efficient_lactions_correspond_to_hactions vs tds inv pc_relation pc_return_relation
    (efficient_action_to_ending_thread_state first_laction first_lpc_indices)
    (efficient_action_to_ending_thread_state first_haction first_hpc_indices) lend_state hend_state
    remaining_mapper remaining_lactions remaining_hactions remaining_lpc_indices
    remaining_hpc_indices
| MapperIntroduced witness :: remaining_mapper,
_,
first_haction :: remaining_hactions,
_,
first_hpc_indices :: remaining_hpc_indices ->
  first_haction.ok /\ efficient_action_to_starting_thread_state first_hpc_indices = hstart_state /\
  efficient_thread_states_match_per_pc_relation pc_relation
    lstart_state
    (efficient_action_to_ending_thread_state first_haction first_hpc_indices) /\
  valid_introduction_succeeds_witness vs tds inv first_haction.program_statement witness /\
  statement_updates_gvars vs first_haction.program_statement.statement /\
  efficient_lactions_correspond_to_hactions vs tds inv pc_relation pc_return_relation lstart_state
    (efficient_action_to_ending_thread_state first_haction first_hpc_indices) lend_state hend_state
    remaining_mapper lactions remaining_hactions lpc_indices remaining_hpc_indices
| _, _, _, _, _ -> False