val all_gvars_have_types (mem: Armada.Memory.t) (vs: list var_id_t) (tds: list object_td_t)
    : GTot ubool
val all_gvars_have_types (mem: Armada.Memory.t) (vs: list var_id_t) (tds: list object_td_t)
    : GTot ubool
let all_gvars_have_types (mem: Armada.Memory.t) (vs: list var_id_t) (tds: list object_td_t) : GTot ubool =
  lists_correspond_ubool (gvar_has_type mem) vs tds
module Strategies.GlobalVars.Types

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement
open Util.List
open Util.Tactics

let gvar_has_type (mem: Armada.Memory.t) (v: var_id_t) (td: object_td_t) : GTot ubool =
  let root_id = RootIdGlobal v in
  let root = mem root_id in
  match root with
  | RootGlobal storage -> object_storage_to_td storage == td
  | _ -> False
/
Util.Tactics.fst.checked Util.List.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.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.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.GlobalVars.Types.fst

    mem: Armada.Memory.t ->
    vs: Prims.list Armada.Base.var_id_t ->
    tds: Prims.list Armada.Type.object_td_t
  -> Prims.GTot Spec.Ubool.ubool
Armada.Memory.t Prims.list Armada.Base.var_id_t Armada.Type.object_td_t Util.List.lists_correspond_ubool Strategies.GlobalVars.Types.gvar_has_type Spec.Ubool.ubool
let all_gvars_have_types (mem: Armada.Memory.t) (vs: list var_id_t) (tds: list object_td_t)
    : GTot ubool =
  
lists_correspond_ubool (gvar_has_type mem) vs tds