val 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)
val 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)
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 ->
    storage: Armada.Memory.object_storage_t
  -> FStar.Pervasives.Lemma
      (requires Strategies.GlobalVars.global_variables_unaddressed_in_storage vs storage)
      (ensures
        Strategies.GlobalVars.global_variables_unaddressed_in_object_value vs
          (Armada.Memory.object_storage_to_value actor storage))
      (decreases FStar.Sequence.Base.rank storage)
Prims.list Armada.Base.var_id_t Armada.Base.tid_t Armada.Memory.object_storage_t Armada.Type.primitive_td_t FStar.Sequence.Base.seq Armada.Type.primitive_box_t Spec.Map.t Prims.nat Strategies.GlobalVars.Unaddressed.global_variables_unaddressed_in_storages_implies_unaddressed_in_object_values Armada.Type.object_td_t Prims.unit Strategies.GlobalVars.global_variables_unaddressed_in_storage Prims.squash Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_object_value Armada.Memory.object_storage_to_value Prims.Nil FStar.Pervasives.pattern
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 -> ()