val global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values
      (vs: list var_id_t)
      (actor: tid_t)
      (storages: seq object_storage_t)
    : Lemma (requires global_variables_unaddressed_in_storages vs storages)
      (ensures
        global_variables_unaddressed_in_object_value_seq vs
          (map_refine (object_storage_to_value actor) storages))
      (decreases rank storages)
val global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values
      (vs: list var_id_t)
      (actor: tid_t)
      (storages: seq object_storage_t)
    : Lemma (requires global_variables_unaddressed_in_storages vs storages)
      (ensures
        global_variables_unaddressed_in_object_value_seq vs
          (map_refine (object_storage_to_value actor) storages))
      (decreases rank storages)
let rec global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value
  (vs: list var_id_t)
  (actor: tid_t)
  (storage: object_storage_t)
  : Lemma (requires global_variables_unaddressed_in_storage vs storage)
          (ensures  global_variables_unaddressed_in_object_value vs (object_storage_to_value actor storage))
          (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive _ values local_versions -> ()
  | ObjectStoragePrimitive value -> ()
  | ObjectStorageStruct fields ->
      global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values vs actor fields
  | ObjectStorageArray element_td elements ->
      global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values vs actor elements
  | ObjectStorageAbstract ty value -> ()

and global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values
  (vs: list var_id_t)
  (actor: tid_t)
  (storages: seq object_storage_t)
  : Lemma (requires global_variables_unaddressed_in_storages vs storages)
          (ensures  global_variables_unaddressed_in_object_value_seq vs
                      (map_refine (object_storage_to_value actor) storages))
          (decreases rank storages) =
  let values = map_refine (object_storage_to_value actor) storages in
  introduce forall value. contains values value ==> global_variables_unaddressed_in_object_value vs value
  with
    introduce _ ==> _
    with _.
      eliminate exists storage. contains storages storage /\ value == object_storage_to_value actor storage
      returns _
      with _. global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value vs actor storage
module Strategies.GlobalVars.Unaddressed

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.UnaryOp
open FStar.Sequence.Ambient
open FStar.Sequence.Base
open Spec.List
open Spec.Ubool
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Util.Seq
open Util.Trigger
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Strategies.GlobalVars.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.Thread.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.GlobalVars.Unaddressed.fst

    vs: Prims.list Armada.Base.var_id_t ->
    actor: Armada.Base.tid_t ->
    storages: FStar.Sequence.Base.seq Armada.Memory.object_storage_t
  -> FStar.Pervasives.Lemma
      (requires Strategies.GlobalVars.global_variables_unaddressed_in_storages vs storages)
      (ensures
        Strategies.GlobalVars.global_variables_unaddressed_in_object_value_seq vs
          (Util.Seq.map_refine (Armada.Memory.object_storage_to_value actor) storages))
      (decreases FStar.Sequence.Base.rank storages)
Prims.list Armada.Base.var_id_t Armada.Base.tid_t FStar.Sequence.Base.seq Armada.Memory.object_storage_t FStar.Classical.Sugar.forall_intro Armada.Type.object_value_t Prims.l_imp FStar.Sequence.Base.contains Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_object_value FStar.Classical.Sugar.implies_intro Prims.squash FStar.Classical.Sugar.exists_elim Prims.l_and Prims.eq2 Armada.Memory.object_storage_to_value Strategies.GlobalVars.Unaddressed.global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value Prims.op_Equality Prims.nat FStar.Sequence.Base.length Prims.l_Forall Prims.op_LessThan Prims.l_True FStar.Sequence.Base.index Util.Seq.map_refine Prims.unit Strategies.GlobalVars.global_variables_unaddressed_in_storages Strategies.GlobalVars.global_variables_unaddressed_in_object_value_seq Prims.Nil FStar.Pervasives.pattern
let rec global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values
      (vs: list var_id_t)
      (actor: tid_t)
      (storages: seq object_storage_t)
    : Lemma (requires global_variables_unaddressed_in_storages vs storages)
      (ensures
        global_variables_unaddressed_in_object_value_seq vs
          (map_refine (object_storage_to_value actor) storages))
      (decreases rank storages) =
  
let values = map_refine (object_storage_to_value actor) storages in
introduce forall value . contains values value ==>
global_variables_unaddressed_in_object_value vs value
with introduce _ ==> _
with _. eliminate exists storage.
contains storages storage /\ value == object_storage_to_value actor storage
returns _
with _.
global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value vs actor storage