val efficient_lactions_all_hidden
      (vs: list var_id_t)
      (lpc_to_hpc: array_t nat)
      (lstart_state lend_state: efficient_thread_state_t)
      (lactions: list Armada.Action.t)
      (lpc_indices: list statement_pc_indices_t)
    : GTot ubool (decreases lactions)
val efficient_lactions_all_hidden
      (vs: list var_id_t)
      (lpc_to_hpc: array_t nat)
      (lstart_state lend_state: efficient_thread_state_t)
      (lactions: list Armada.Action.t)
      (lpc_indices: list statement_pc_indices_t)
    : GTot ubool (decreases lactions)
let rec efficient_lactions_all_hidden
  (vs: list var_id_t)
  (lpc_to_hpc: array_t nat)
  (lstart_state: efficient_thread_state_t)
  (lend_state: efficient_thread_state_t)
  (lactions: list Armada.Action.t)
  (lpc_indices: list statement_pc_indices_t)
  : GTot ubool
  (decreases lactions) =
  match lactions, lpc_indices with
  | [], [] -> lend_state = lstart_state
  | first_laction :: remaining_lactions, first_lpc_indices :: remaining_lpc_indices ->
         efficient_action_to_starting_thread_state first_lpc_indices = lstart_state
      /\ (match lstart_state, efficient_action_to_ending_thread_state first_laction first_lpc_indices with
         | EfficientThreadStateAtPC lpc1, EfficientThreadStateAtPC lpc2 ->
             array_nth lpc_to_hpc lpc1 = array_nth lpc_to_hpc lpc2
         | _, _ -> False)
      /\ statement_updates_gvars vs first_laction.program_statement.statement
      /\ efficient_lactions_all_hidden vs lpc_to_hpc
           (efficient_action_to_ending_thread_state first_laction first_lpc_indices)
           lend_state remaining_lactions remaining_lpc_indices
  | _, _ -> False
module Strategies.VarHiding.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.VarHiding
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.VarHiding.Defs
open Util.ImmutableArray
open Util.List
open Util.Nth
open Util.Range
open Util.Relation

let efficient_program_inits_match_except_global_variables
  (vs: list var_id_t)
  (lpcs: array_t pc_t)
  (hpcs: array_t pc_t)
  (lpc_to_hpc: array_t nat)
  (which_initializers_are_hidings: 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 lpc_to_hpc lprog_main_start_pc = Some hprog_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_hidings
       lprog.global_initializers hprog.global_initializers
  /\ lprog.main_stack_initializers == hprog.main_stack_initializers

let efficient_lpc_to_hpc_contains_valid_indices
  (num_hpcs: nat)
  (lpc_to_hpc: array_t nat)
  : GTot bool =
  for_all_array (fun (hidx: nat) -> hidx < num_hpcs) lpc_to_hpc

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

let efficient_lh_pc_return_relation (lpc_to_hpc: array_t nat) (is_return_lpc: array_t bool) : GTot (relation_t nat nat) =
  fun lidx hidx -> array_nth lpc_to_hpc lidx = Some hidx && array_nth is_return_lpc lidx = Some true
/
Util.Relation.fst.checked Util.Range.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Util.ImmutableArray.fsti.checked Strategies.VarHiding.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.VarHiding.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.VarHiding.Efficient.fsti

    vs: Prims.list Armada.Base.var_id_t ->
    lpc_to_hpc: Util.ImmutableArray.array_t Prims.nat ->
    lstart_state: Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t ->
    lend_state: Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t ->
    lactions: Prims.list Armada.Action.t ->
    lpc_indices: Prims.list Strategies.PCIndices.statement_pc_indices_t
  -> Prims.GTot Spec.Ubool.ubool
Prims.list Armada.Base.var_id_t Util.ImmutableArray.array_t Prims.nat Strategies.ArmadaStatement.ThreadState.efficient_thread_state_t Armada.Action.t Strategies.PCIndices.statement_pc_indices_t FStar.Pervasives.Native.Mktuple2 Prims.b2t Prims.op_Equality Prims.l_and Strategies.ArmadaStatement.ThreadState.efficient_action_to_starting_thread_state Strategies.ArmadaStatement.ThreadState.efficient_action_to_ending_thread_state FStar.Pervasives.Native.option Util.ImmutableArray.array_nth Prims.l_False Prims.logical Strategies.GlobalVars.VarIntro.statement_updates_gvars Armada.Action.__proj__Mkprogram_statement_t__item__statement Armada.Action.__proj__Mkt__item__program_statement Strategies.VarHiding.Efficient.efficient_lactions_all_hidden Spec.Ubool.ubool
let rec efficient_lactions_all_hidden
      (vs: list var_id_t)
      (lpc_to_hpc: array_t nat)
      (lstart_state lend_state: efficient_thread_state_t)
      (lactions: list Armada.Action.t)
      (lpc_indices: list statement_pc_indices_t)
    : GTot ubool (decreases lactions) =
  
match lactions, lpc_indices with
| [], [] -> lend_state = lstart_state
| first_laction :: remaining_lactions, first_lpc_indices :: remaining_lpc_indices ->
  efficient_action_to_starting_thread_state first_lpc_indices = lstart_state /\
  (match lstart_state, efficient_action_to_ending_thread_state first_laction first_lpc_indices with
    | EfficientThreadStateAtPC lpc1, EfficientThreadStateAtPC lpc2 ->
      array_nth lpc_to_hpc lpc1 = array_nth lpc_to_hpc lpc2
    | _, _ -> False) /\ statement_updates_gvars vs first_laction.program_statement.statement /\
  efficient_lactions_all_hidden vs
    lpc_to_hpc
    (efficient_action_to_ending_thread_state first_laction first_lpc_indices)
    lend_state
    remaining_lactions
    remaining_lpc_indices
| _, _ -> False