val var_intro_pc_progress_measure (vr: var_intro_relation_t) (hs: Armada.State.t) (actor: tid_t)
    : GTot nat
val var_intro_pc_progress_measure (vr: var_intro_relation_t) (hs: Armada.State.t) (actor: tid_t)
    : GTot nat
let var_intro_pc_progress_measure
  (vr: var_intro_relation_t)
  (hs: Armada.State.t)
  (actor: tid_t)
  : GTot nat =
  let hthread = hs.threads actor in
  match (vr.hpc_info hthread.pc) with
  | HPCInfoNormal -> 0
  | HPCInfoIntroduced _ _ _ progress -> progress + 1
module Strategies.VarIntro.Invariant

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 FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Strategies.ArmadaStatement.Breaking
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.ArmadaStatement.Status
open Strategies.ArmadaStatement.ThreadState
open Strategies.Atomic
open Strategies.GlobalVars
open Strategies.GlobalVars.Types
open Strategies.Invariant
open Strategies.PCRelation
open Strategies.Semantics
open Strategies.Semantics.Armada
open Strategies.VarIntro.Defs
open Strategies.VarIntro.Helpers
open Strategies.VarIntro.Initialization

let var_intro_invariant
  (ls: Armada.State.t)
  : GTot ubool =
  True

let var_intro_lh_relation_between_steps
  (vr: var_intro_relation_t)
  (u: unit)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  : GTot ubool =
  let pc_relation = var_intro_pc_relation vr.hpc_to_lpc vr.return_hpcs vr.return_pcs_unique_proof in
    states_match_except_global_variables vr.vs pc_relation ls hs
  /\ all_running_threads_have_pcs_in_list vr.hpcs hs
  /\ global_variables_unaddressed_in_memory vr.vs ls.mem
  /\ global_variables_unaddressed_in_memory vr.vs hs.mem
  /\ roots_match ls.mem
  /\ roots_match hs.mem
  /\ all_gvars_have_types hs.mem vr.vs vr.tds
  /\ unstarted_threads_have_empty_write_buffers ls
  /\ unstarted_threads_have_empty_write_buffers hs
  /\ (NotStopped? hs.stop_reason ==> vr.inv hs)

let var_intro_lh_relation
  (vr: var_intro_relation_t)
  (u: unit)
  (ls: Armada.State.t)
  (hs: Armada.State.t)
  : GTot ubool =
    var_intro_lh_relation_between_steps vr u ls hs
  /\ all_threads_breaking vr.is_breaking_hpc hs
/
Strategies.VarIntro.Initialization.fsti.checked Strategies.VarIntro.Helpers.fst.checked Strategies.VarIntro.Defs.fst.checked Strategies.Semantics.Armada.fsti.checked Strategies.Semantics.fst.checked Strategies.PCRelation.fst.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.fst.checked Strategies.Atomic.fst.checked Strategies.ArmadaStatement.ThreadState.fst.checked Strategies.ArmadaStatement.Status.fsti.checked Strategies.ArmadaStatement.Breaking.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.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.Base.fst.checked
Strategies.VarIntro.Invariant.fst
vr: Strategies.VarIntro.Defs.var_intro_relation_t -> hs: Armada.State.t -> actor: Armada.Base.tid_t
  -> Prims.GTot Prims.nat
Strategies.VarIntro.Defs.var_intro_relation_t Armada.State.t Armada.Base.tid_t Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__hpc_info Armada.Thread.__proj__Mkt__item__pc Prims.nat Armada.Base.pc_t Prims.list Strategies.VarIntro.Defs.introduction_succeeds_witness_t Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__vs Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__tds Strategies.VarIntro.Defs.__proj__Mkvar_intro_relation_t__item__inv Prims.op_Addition Armada.Thread.t Armada.State.__proj__Mkt__item__threads
let var_intro_pc_progress_measure (vr: var_intro_relation_t) (hs: Armada.State.t) (actor: tid_t)
    : GTot nat =
  
let hthread = hs.threads actor in
match (vr.hpc_info hthread.pc) with
| HPCInfoNormal -> 0
| HPCInfoIntroduced _ _ _ progress -> progress + 1