val inefficient_var_hiding_witness_valid_implies_refinement
  (latomic_prog: program_t (make_atomic_semantics armada_semantics))
  (hatomic_prog: program_t (make_atomic_semantics armada_semantics))
  (vw: inefficient_var_hiding_witness_t)
  : Lemma (requires   inefficient_var_hiding_witness_valid latomic_prog hatomic_prog vw
                    /\ is_armada_substep_invariant latomic_prog vw.inv
                    /\ latomic_prog.init_f == init_program vw.lprog
                    /\ hatomic_prog.init_f == init_program vw.hprog)
          (ensures (spec_refines_spec
                      (semantics_to_spec (make_atomic_semantics armada_semantics) latomic_prog)
                      (semantics_to_spec (make_atomic_semantics armada_semantics) hatomic_prog)
                      refinement_requirement))
val inefficient_var_hiding_witness_valid_implies_refinement
  (latomic_prog: program_t (make_atomic_semantics armada_semantics))
  (hatomic_prog: program_t (make_atomic_semantics armada_semantics))
  (vw: inefficient_var_hiding_witness_t)
  : Lemma (requires   inefficient_var_hiding_witness_valid latomic_prog hatomic_prog vw
                    /\ is_armada_substep_invariant latomic_prog vw.inv
                    /\ latomic_prog.init_f == init_program vw.lprog
                    /\ hatomic_prog.init_f == init_program vw.hprog)
          (ensures (spec_refines_spec
                      (semantics_to_spec (make_atomic_semantics armada_semantics) latomic_prog)
                      (semantics_to_spec (make_atomic_semantics armada_semantics) hatomic_prog)
                      refinement_requirement))
let inefficient_var_hiding_witness_valid_implies_refinement
  (latomic_prog: program_t (make_atomic_semantics armada_semantics))
  (hatomic_prog: program_t (make_atomic_semantics armada_semantics))
  (vw: inefficient_var_hiding_witness_t)
  (* see .fsti file for spec *) =
  let vr: var_hiding_relation_t = {
    lprog = vw.lprog;
    hprog = vw.hprog;
    latomic_prog = latomic_prog;
    hatomic_prog = hatomic_prog;
    vs = vw.vs;
    tds = vw.tds;
    inv = vw.inv;
    which_initializers_are_hidings = vw.which_initializers_are_hidings;
    lpc_to_hpc = vw.lpc_to_hpc;
    return_lpcs = vw.return_lpcs;
    is_nonyielding_lpc = vw.is_nonyielding_lpc;
    is_nonyielding_hpc = vw.is_nonyielding_hpc;
    corresponding_hactions_info = vw.corresponding_hactions_info;
    inv_is_substep_invariant_proof = (fun _ -> ());
    atomic_inits_match_regular_inits_proof = (fun _ -> ());
    program_inits_match_except_global_variables_proof = (fun _ -> ());
    initial_pcs_correspond_proof = (fun _ -> ());
    global_variables_unaddressed_in_initializers_proof = (fun _ -> ());
    all_introduced_global_variables_initialized_proof = (fun _ -> ());
    return_pcs_unique_proof = (fun _ -> ());
    lactions_consistent_with_is_nonyielding_pc_proof = (fun _ -> ());
    hactions_consistent_with_is_nonyielding_pc_proof = (fun _ -> ());
    each_laction_doesnt_internally_yield_proof = (fun _ -> ());
    each_haction_doesnt_internally_yield_proof = (fun _ -> ());
    each_haction_ends_atomic_block_if_necessary_proof = (fun _ -> ());
    corresponding_hactions_correspond_proof = (fun _ -> ());
  } in
  var_hiding_relation_implies_refinement vr
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.Nonyielding
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarHiding.Defs
open Strategies.VarHiding.Relation
open Util.List
open Util.Nth
open Util.Relation
/
Util.Relation.fst.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.VarHiding.Relation.fsti.checked Strategies.VarHiding.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.Nonyielding.fst.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.fst

    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
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.VarHiding.Inefficient.inefficient_var_hiding_witness_valid latomic_prog
          hatomic_prog
          vw /\
        Strategies.Invariant.Armada.AtomicSubstep.is_armada_substep_invariant latomic_prog
          (Mkinefficient_var_hiding_witness_t?.inv vw) /\
        Mkprogram_t?.init_f latomic_prog ==
        Armada.Program.init_program (Mkinefficient_var_hiding_witness_t?.lprog vw) /\
        Mkprogram_t?.init_f hatomic_prog ==
        Armada.Program.init_program (Mkinefficient_var_hiding_witness_t?.hprog vw))
      (ensures
        Spec.Behavior.spec_refines_spec (Strategies.Semantics.semantics_to_spec (Strategies.Atomic.make_atomic_semantics
                  Strategies.Semantics.Armada.armada_semantics)
              latomic_prog)
          (Strategies.Semantics.semantics_to_spec (Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics
                )
              hatomic_prog)
          Armada.State.refinement_requirement)
Strategies.Semantics.program_t Strategies.Atomic.make_atomic_semantics Strategies.Semantics.Armada.armada_semantics Strategies.VarHiding.Inefficient.inefficient_var_hiding_witness_t Strategies.VarHiding.Relation.var_hiding_relation_implies_refinement Strategies.VarHiding.Defs.var_hiding_relation_t Strategies.VarHiding.Defs.Mkvar_hiding_relation_t Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__lprog Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__hprog Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__vs Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__tds Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__inv Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__which_initializers_are_hidings Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__lpc_to_hpc Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__return_lpcs Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__is_nonyielding_lpc Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__is_nonyielding_hpc Strategies.VarHiding.Inefficient.__proj__Mkinefficient_var_hiding_witness_t__item__corresponding_hactions_info Prims.unit Prims.squash Strategies.Invariant.Armada.AtomicSubstep.is_armada_substep_invariant Prims.l_and Prims.eq2 Armada.State.t Spec.Ubool.ubool Strategies.Semantics.__proj__Mkprogram_t__item__init_f Armada.Program.init_program Strategies.VarHiding.Defs.program_inits_match_except_global_variables 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.Defs.return_pcs_unique Strategies.Nonyielding.each_action_list_consistent_with_is_nonyielding_pc Strategies.Semantics.__proj__Mkprogram_t__item__actions 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.Defs.lactions_correspond_to_hactions_per_correspondence
let inefficient_var_hiding_witness_valid_implies_refinement
      (latomic_prog hatomic_prog: program_t (make_atomic_semantics armada_semantics))
      (vw: inefficient_var_hiding_witness_t)
     =
  
let vr:var_hiding_relation_t =
  {
    lprog = vw.lprog;
    hprog = vw.hprog;
    latomic_prog = latomic_prog;
    hatomic_prog = hatomic_prog;
    vs = vw.vs;
    tds = vw.tds;
    inv = vw.inv;
    which_initializers_are_hidings = vw.which_initializers_are_hidings;
    lpc_to_hpc = vw.lpc_to_hpc;
    return_lpcs = vw.return_lpcs;
    is_nonyielding_lpc = vw.is_nonyielding_lpc;
    is_nonyielding_hpc = vw.is_nonyielding_hpc;
    corresponding_hactions_info = vw.corresponding_hactions_info;
    inv_is_substep_invariant_proof = (fun _ -> ());
    atomic_inits_match_regular_inits_proof = (fun _ -> ());
    program_inits_match_except_global_variables_proof = (fun _ -> ());
    initial_pcs_correspond_proof = (fun _ -> ());
    global_variables_unaddressed_in_initializers_proof = (fun _ -> ());
    all_introduced_global_variables_initialized_proof = (fun _ -> ());
    return_pcs_unique_proof = (fun _ -> ());
    lactions_consistent_with_is_nonyielding_pc_proof = (fun _ -> ());
    hactions_consistent_with_is_nonyielding_pc_proof = (fun _ -> ());
    each_laction_doesnt_internally_yield_proof = (fun _ -> ());
    each_haction_doesnt_internally_yield_proof = (fun _ -> ());
    each_haction_ends_atomic_block_if_necessary_proof = (fun _ -> ());
    corresponding_hactions_correspond_proof = (fun _ -> ())
  }
in
var_hiding_relation_implies_refinement vr