val state_well_formed (vs: list var_id_t) (s: Armada.State.t) : GTot ubool
val state_well_formed (vs: list var_id_t) (s: Armada.State.t) : GTot ubool
let state_well_formed (vs: list var_id_t) (s: Armada.State.t): GTot ubool =
  roots_match s.mem /\ positions_valid_in_state s /\ global_variables_unaddressed_in_memory vs s.mem
module Strategies.GlobalVarsProof

open FStar.Sequence.Ambient
open FStar.Sequence.Base

open Util.Seq
open Util.Trigger
open Spec.List
open Spec.Ubool

open Armada.Base
open Armada.BinaryOp
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Armada.Transition
open Armada.UnaryOp

open Strategies.Invariant
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.Unaddressed
open Strategies.ArmadaStatement

let ($$) (#a: Type) (#b: Type) (f: a -> b) (x: a): b = f x
let ($$$) (#a: Type) (f: a -> GTot (conditional_computation_t a)) (x: a): GTot (conditional_computation_t a) = f x

let memories_match_on_global_variables
  (vs: list var_id_t)
  (mem1 mem2: Armada.Memory.t)
  : GTot ubool
  = forall v . list_contains v vs ==>
      mem1 (RootIdGlobal v) == mem2 (RootIdGlobal v)

let states_match_on_global_variables
  (vs: list var_id_t)
  (s1 s2: Armada.State.t)
  : GTot ubool
  = memories_match_on_global_variables vs s1.mem s2.mem
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaStatement.fst.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Sequence.Base.fsti.checked FStar.Sequence.Ambient.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.UnaryOp.fst.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked
Strategies.GlobalVarsProof.fst
vs: Prims.list Armada.Base.var_id_t -> s: Armada.State.t -> Prims.GTot Spec.Ubool.ubool
Prims.list Armada.Base.var_id_t Armada.State.t Prims.l_and Strategies.ArmadaInvariant.RootsMatch.roots_match Armada.State.__proj__Mkt__item__mem Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Strategies.GlobalVars.global_variables_unaddressed_in_memory Spec.Ubool.ubool
let state_well_formed (vs: list var_id_t) (s: Armada.State.t) : GTot ubool =
  
roots_match s.mem /\ positions_valid_in_state s /\ global_variables_unaddressed_in_memory vs s.mem