val statement_updates_gvars_using_constant
      (vs: list var_id_t)
      (tds: list object_td_t)
      (statement: Armada.Statement.t)
    : GTot ubool
val statement_updates_gvars_using_constant
      (vs: list var_id_t)
      (tds: list object_td_t)
      (statement: Armada.Statement.t)
    : GTot ubool
let rec statement_updates_gvars_using_constant
  (vs: list var_id_t)
  (tds: list object_td_t)
  (statement: Armada.Statement.t)
  : GTot ubool =
  match vs, tds with
  | v :: remaining_vs, td :: remaining_tds ->
        statement_updates_specific_gvar_to_constant v td statement
      \/ statement_updates_gvars_using_constant remaining_vs remaining_tds statement
  | _, _ -> False
module Strategies.GlobalVars.VarIntro

open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.GlobalVars
open Strategies.GlobalVars.Types
open Strategies.PCRelation
open Util.List

let rec pointer_among_global_variables (vs: list var_id_t) (ptr: Armada.Pointer.t) : GTot bool =
  match ptr with
  | PointerUninitialized -> false
  | PointerNull -> false
  | PointerRoot root_id -> not (global_variables_unmentioned_in_root_id vs root_id)
  | PointerField struct_ptr _ -> pointer_among_global_variables vs struct_ptr
  | PointerIndex array_ptr _ -> pointer_among_global_variables vs array_ptr

let rec lvalue_expression_among_global_variables
  (vs: list var_id_t)
  (e: expression_t)
  : GTot bool =
  match e with
  | ExpressionGlobalVariable _ var_id -> list_contains var_id vs
  | ExpressionFieldOf _ obj _ -> lvalue_expression_among_global_variables vs obj
  | _ -> false

let statement_updates_gvars
  (vs: list var_id_t)
  (statement: Armada.Statement.t)
  : GTot bool =
  match statement with
  | UpdateStatement bypassing_write_buffer dst src ->
         lvalue_expression_among_global_variables vs dst
      && global_variables_unaddressed_in_rvalue_expression vs src
  | NondeterministicUpdateStatement bypassing_write_buffer dst ->
      lvalue_expression_among_global_variables vs dst
  | _ -> false

let statement_updates_specific_gvar_to_constant
  (v: var_id_t)
  (td: object_td_t)
  (statement: Armada.Statement.t)
  : GTot ubool =
  match statement with
  | UpdateStatement bypassing_write_buffer (ExpressionGlobalVariable td' v') (ExpressionConstant value) ->
        v' = v
      /\ td' == td
      /\ object_value_to_td value == td
      /\ (ObjectValuePrimitive? value || ObjectValueAbstract? value)
  | _ -> False
/
Util.List.fst.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Types.fst.checked Strategies.GlobalVars.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.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked
Strategies.GlobalVars.VarIntro.fsti

    vs: Prims.list Armada.Base.var_id_t ->
    tds: Prims.list Armada.Type.object_td_t ->
    statement: Armada.Statement.t
  -> Prims.GTot Spec.Ubool.ubool
Prims.list Armada.Base.var_id_t Armada.Type.object_td_t Armada.Statement.t FStar.Pervasives.Native.Mktuple2 Prims.l_or Strategies.GlobalVars.VarIntro.statement_updates_specific_gvar_to_constant Strategies.GlobalVars.VarIntro.statement_updates_gvars_using_constant Prims.l_False Spec.Ubool.ubool
let rec statement_updates_gvars_using_constant
      (vs: list var_id_t)
      (tds: list object_td_t)
      (statement: Armada.Statement.t)
    : GTot ubool =
  
match vs, tds with
| v :: remaining_vs, td :: remaining_tds ->
  statement_updates_specific_gvar_to_constant v td statement \/
  statement_updates_gvars_using_constant remaining_vs remaining_tds statement
| _, _ -> False