val dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (mem: Armada.Memory.t)
    : Lemma (requires global_variables_unaddressed_in_memory vs mem /\ roots_match mem)
      (ensures
        (match dereference_computation p mem with
          | ComputationProduces storage -> global_variables_unaddressed_in_storage vs storage
          | _ -> True))
val dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (mem: Armada.Memory.t)
    : Lemma (requires global_variables_unaddressed_in_memory vs mem /\ roots_match mem)
      (ensures
        (match dereference_computation p mem with
          | ComputationProduces storage -> global_variables_unaddressed_in_storage vs storage
          | _ -> True))
let rec dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  (mem: Armada.Memory.t)
  : Lemma (requires   global_variables_unaddressed_in_memory vs mem
                    /\ roots_match mem)
          (ensures  (match dereference_computation p mem with
                     | ComputationProduces storage -> global_variables_unaddressed_in_storage vs storage
                     | _ -> True)) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr field_id ->
      dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs struct_ptr mem
  | PointerIndex array_ptr idx ->
      dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs array_ptr mem
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

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
/
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 -> p: Armada.Pointer.t -> mem: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem)
      (ensures
        ((match Armada.Memory.dereference_computation p mem with
            | Armada.Computation.ComputationProduces #_ storage ->
              Strategies.GlobalVars.global_variables_unaddressed_in_storage vs storage
            | _ -> Prims.l_True)
          <:
          Type0))
Prims.list Armada.Base.var_id_t Armada.Pointer.t Armada.Memory.t Armada.Base.root_id_t Prims.nat Strategies.GlobalVars.Unaddressed.dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed Prims.unit Prims.l_and Strategies.GlobalVars.global_variables_unaddressed_in_memory Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.squash Armada.Memory.dereference_computation Armada.Memory.valid_object_storage_t Strategies.GlobalVars.global_variables_unaddressed_in_storage Armada.Computation.conditional_computation_t Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (mem: Armada.Memory.t)
    : Lemma (requires global_variables_unaddressed_in_memory vs mem /\ roots_match mem)
      (ensures
        (match dereference_computation p mem with
          | ComputationProduces storage -> global_variables_unaddressed_in_storage vs storage
          | _ -> True)) =
  
match p with
| PointerUninitialized -> ()
| PointerNull -> ()
| PointerRoot root_id -> ()
| PointerField struct_ptr field_id ->
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs
    struct_ptr
    mem
| PointerIndex array_ptr idx ->
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs
    array_ptr
    mem