val lstep_corresponds_to_hstep
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (lstep hstep: Armada.Step.t)
    : GTot ubool
val lstep_corresponds_to_hstep
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (lstep hstep: Armada.Step.t)
    : GTot ubool
let lstep_corresponds_to_hstep
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (lstep: Armada.Step.t)
  (hstep: Armada.Step.t)
  : GTot ubool =
  let lps, hps = lstep.action.program_statement, hstep.action.program_statement in
    lstep.nd == hstep.nd
  /\ statement_effect_independent_of_global_variables vs lps.statement
  /\ statements_match_per_pc_relation pc_relation.relation pc_relation.return_relation lps.statement hps.statement
  /\ (match lps.end_pc, hps.end_pc with
     | Some lpc, Some hpc ->
           pc_relation.relation lpc hpc
         /\ (ReturnStatement? lps.statement ==> pc_relation.return_relation lpc hpc)
     | None, None -> True
     | _, _ -> False)
module Strategies.VarHiding.Helpers

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Init
open Armada.Memory
open Armada.Program
open Armada.State
open Armada.Step
open Armada.Statement
open Armada.Thread
open Armada.Threads
open Armada.Transition
open Armada.Type
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open FStar.WellFoundedRelation
open Spec.Behavior
open Spec.List
open Spec.Logic
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.ArmadaStatement.Propagate
open Strategies.ArmadaStatement.Status
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars
open Strategies.GlobalVars.Init
open Strategies.GlobalVars.Permanent
open Strategies.GlobalVars.Statement
open Strategies.GlobalVars.Types
open Strategies.GlobalVars.Unaddressed
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.VarIntro
open Strategies.Lift.Generic
open Strategies.Invariant
open Strategies.PCRelation
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarHiding.Defs
open Util.List
open Util.Nth
open Util.Seq

/// Definitions

let return_pcs_unique_proof_t (lpc_to_hpc: pc_t -> GTot pc_t) (return_lpcs: list pc_t) =
  unit -> Lemma (return_pcs_unique lpc_to_hpc return_lpcs)

let var_hiding_pc_relation
  (lpc_to_hpc: pc_t -> GTot pc_t)
  (return_lpcs: list pc_t)
  (return_pcs_unique_proof: return_pcs_unique_proof_t lpc_to_hpc return_lpcs)
  : pc_relation_t =
  return_pcs_unique_proof ();
  let return_relation = (fun lpc hpc -> list_contains lpc return_lpcs && lpc_to_hpc lpc = hpc) in
  {
    relation = (fun lpc hpc -> lpc_to_hpc lpc = hpc);
    return_relation = return_relation;
  }

let rec compute_hsteps_from_hactions
  (hactions: list Armada.Action.t)
  : Ghost (list Armada.Step.t)
    (requires True)
    (ensures fun hsteps -> map_ghost armada_step_to_action hsteps == hactions) =
  match hactions with
  | [] -> []
  | first_haction :: remaining_hactions ->
      let first_hstep = { nd = []; action = first_haction } in
      first_hstep :: compute_hsteps_from_hactions remaining_hactions

/// Correspondence between lsteps and hsteps
/
Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.VarHiding.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCRelation.fst.checked Strategies.Lift.Generic.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.VarIntro.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.Statement.fsti.checked Strategies.GlobalVars.Permanent.fst.checked Strategies.GlobalVars.Init.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Strategies.ArmadaStatement.Propagate.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Logic.fst.checked Spec.List.fst.checked Spec.Behavior.fst.checked prims.fst.checked FStar.WellFoundedRelation.fsti.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.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.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.VarHiding.Helpers.fst

    vs: Prims.list Armada.Base.var_id_t ->
    pc_relation: Strategies.PCRelation.pc_relation_t ->
    lstep: Armada.Step.t ->
    hstep: Armada.Step.t
  -> Prims.GTot Spec.Ubool.ubool
Prims.list Armada.Base.var_id_t Strategies.PCRelation.pc_relation_t Armada.Step.t Armada.Action.program_statement_t Prims.l_and Prims.eq2 Armada.Type.nondeterminism_t Armada.Step.__proj__Mkt__item__nd Prims.b2t Strategies.GlobalVars.Statement.statement_effect_independent_of_global_variables Armada.Action.__proj__Mkprogram_statement_t__item__statement Strategies.GlobalVars.Statement.statements_match_per_pc_relation Strategies.PCRelation.__proj__Mkpc_relation_t__item__relation Strategies.PCRelation.__proj__Mkpc_relation_t__item__return_relation FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option Armada.Base.pc_t Armada.Action.__proj__Mkprogram_statement_t__item__end_pc Prims.l_imp Armada.Statement.uu___is_ReturnStatement Prims.l_True Prims.l_False Prims.logical Spec.Ubool.ubool FStar.Pervasives.Native.tuple2 Armada.Action.__proj__Mkt__item__program_statement Armada.Step.__proj__Mkt__item__action
let lstep_corresponds_to_hstep
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (lstep hstep: Armada.Step.t)
    : GTot ubool =
  
let lps, hps = lstep.action.program_statement, hstep.action.program_statement in
lstep.nd == hstep.nd /\ statement_effect_independent_of_global_variables vs lps.statement /\
statements_match_per_pc_relation pc_relation.relation
  pc_relation.return_relation
  lps.statement
  hps.statement /\
(match lps.end_pc, hps.end_pc with
  | Some lpc, Some hpc ->
    pc_relation.relation lpc hpc /\
    (ReturnStatement? lps.statement ==> pc_relation.return_relation lpc hpc)
  | None, None -> True
  | _, _ -> False)