val inefficient_var_hiding_witness_valid
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: inefficient_var_hiding_witness_t)
    : GTot ubool
val inefficient_var_hiding_witness_valid
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: inefficient_var_hiding_witness_t)
    : GTot ubool
let inefficient_var_hiding_witness_valid
  (latomic_prog: program_t (make_atomic_semantics armada_semantics))
  (hatomic_prog: program_t (make_atomic_semantics armada_semantics))
  (vw: inefficient_var_hiding_witness_t)
  : GTot ubool =
    program_inits_match_except_global_variables vw.vs vw.lpc_to_hpc vw.which_initializers_are_hidings vw.lprog vw.hprog
  /\ vw.lpc_to_hpc vw.lprog.main_start_pc = vw.hprog.main_start_pc
  /\ global_variables_unaddressed_in_initializers vw.vs vw.lprog.global_initializers
  /\ global_variables_unaddressed_in_initializers vw.vs vw.hprog.global_initializers
  /\ global_variables_unaddressed_in_initializers vw.vs vw.lprog.main_stack_initializers
  /\ global_variables_unaddressed_in_initializers vw.vs vw.hprog.main_stack_initializers
  /\ every_variable_appears_among_initializers vw.lprog.global_initializers vw.vs vw.tds
  /\ return_pcs_unique vw.lpc_to_hpc vw.return_lpcs
  /\ each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_lpc latomic_prog.actions
  /\ each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_hpc hatomic_prog.actions
  /\ each_action_list_doesnt_internally_yield latomic_prog.actions
  /\ each_action_list_doesnt_internally_yield hatomic_prog.actions
  /\ each_action_list_ends_atomic_block_if_necessary hatomic_prog.actions
  /\ lists_correspond_ubool
       (lactions_correspond_to_hactions_per_correspondence vw.vs vw.tds vw.inv vw.lpc_to_hpc vw.return_lpcs
          hatomic_prog.actions)
       latomic_prog.actions vw.corresponding_hactions_info
module Strategies.VarHiding.Inefficient

open Armada.Action
open Armada.Base
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Threads
open Armada.Transition
open Armada.Type
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
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.Semantics
open Strategies.Semantics.Armada
open Strategies.VarHiding.Defs
open Util.List
open Util.Nth
open Util.Relation

noeq type inefficient_var_hiding_witness_t = {
  lprog: Armada.Program.t;
  hprog: Armada.Program.t;
  vs: list var_id_t;
  tds: list object_td_t;
  inv: invariant_t Armada.State.t;
  which_initializers_are_hidings: list bool;
  lpc_to_hpc: pc_t -> GTot pc_t;
  return_lpcs: list pc_t;
  is_nonyielding_lpc: pc_t -> GTot bool;
  is_nonyielding_hpc: pc_t -> GTot bool;
  corresponding_hactions_info: list (ltoh_correspondence_t vs tds inv);
}
/
Util.Relation.fst.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.VarHiding.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.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.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Threads.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.Inefficient.fsti

    latomic_prog:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    hatomic_prog:
      Strategies.Semantics.program_t (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
          ) ->
    vw: Strategies.VarHiding.Inefficient.inefficient_var_hiding_witness_t
  -> Prims.GTot Spec.Ubool.ubool
Strategies.Semantics.program_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.VarHiding.Inefficient.inefficient_var_hiding_witness_t Prims.l_and Strategies.VarHiding.Defs.program_inits_match_except_global_variables Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__vs Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__lpc_to_hpc Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__which_initializers_are_hidings Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__lprog Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__hprog Prims.b2t Prims.op_Equality Armada.Base.pc_t Armada.Program.__proj__Mkt__item__main_start_pc Strategies.GlobalVars.global_variables_unaddressed_in_initializers Armada.Program.__proj__Mkt__item__global_initializers Armada.Program.__proj__Mkt__item__main_stack_initializers Strategies.VarHiding.Defs.every_variable_appears_among_initializers Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__tds Strategies.VarHiding.Defs.return_pcs_unique Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__return_lpcs Strategies.Nonyielding.each_action_list_consistent_with_is_nonyielding_pc Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__is_nonyielding_lpc Strategies.Semantics.__proj__Mkprogram_t__item__actions Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__is_nonyielding_hpc Strategies.Nonyielding.each_action_list_doesnt_internally_yield Strategies.Nonyielding.each_action_list_ends_atomic_block_if_necessary Util.List.lists_correspond_ubool Strategies.Semantics.__proj__Mksemantics_t__item__action_t Strategies.VarHiding.Defs.ltoh_correspondence_t Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__inv Strategies.VarHiding.Defs.lactions_correspond_to_hactions_per_correspondence Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__corresponding_hactions_info Spec.Ubool.ubool
let inefficient_var_hiding_witness_valid
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: inefficient_var_hiding_witness_t)
    : GTot ubool =
  
program_inits_match_except_global_variables vw.vs
  vw.lpc_to_hpc
  vw.which_initializers_are_hidings
  vw.lprog
  vw.hprog /\ vw.lpc_to_hpc vw.lprog.main_start_pc = vw.hprog.main_start_pc /\
global_variables_unaddressed_in_initializers vw.vs vw.lprog.global_initializers /\
global_variables_unaddressed_in_initializers vw.vs vw.hprog.global_initializers /\
global_variables_unaddressed_in_initializers vw.vs vw.lprog.main_stack_initializers /\
global_variables_unaddressed_in_initializers vw.vs vw.hprog.main_stack_initializers /\
every_variable_appears_among_initializers vw.lprog.global_initializers vw.vs vw.tds /\
return_pcs_unique vw.lpc_to_hpc vw.return_lpcs /\
each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_lpc latomic_prog.actions /\
each_action_list_consistent_with_is_nonyielding_pc vw.is_nonyielding_hpc hatomic_prog.actions /\
each_action_list_doesnt_internally_yield latomic_prog.actions /\
each_action_list_doesnt_internally_yield hatomic_prog.actions /\
each_action_list_ends_atomic_block_if_necessary hatomic_prog.actions /\
lists_correspond_ubool (lactions_correspond_to_hactions_per_correspondence vw.vs
      vw.tds
      vw.inv
      vw.lpc_to_hpc
      vw.return_lpcs
      hatomic_prog.actions)
  latomic_prog.actions
  vw.corresponding_hactions_info