val dereference_as_td_computation_doesnt_depend_on_global_variables
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (td: object_td_t)
      (actor: tid_t)
      (mem1 mem2: Armada.Memory.t)
    : Lemma
      (requires
        memories_match_except_global_variables vs mem1 mem2 /\
        global_variables_unaddressed_in_pointer vs p /\
        global_variables_unaddressed_in_memory vs mem1 /\
        global_variables_unaddressed_in_memory vs mem2 /\ roots_match mem1 /\ roots_match mem2)
      (ensures
        dereference_as_td_computation p td actor mem1 ==
        dereference_as_td_computation p td actor mem2 /\
        (match dereference_as_td_computation p td actor mem1 with
          | ComputationProduces value -> global_variables_unaddressed_in_object_value vs value
          | _ -> True))
val dereference_as_td_computation_doesnt_depend_on_global_variables
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (td: object_td_t)
      (actor: tid_t)
      (mem1 mem2: Armada.Memory.t)
    : Lemma
      (requires
        memories_match_except_global_variables vs mem1 mem2 /\
        global_variables_unaddressed_in_pointer vs p /\
        global_variables_unaddressed_in_memory vs mem1 /\
        global_variables_unaddressed_in_memory vs mem2 /\ roots_match mem1 /\ roots_match mem2)
      (ensures
        dereference_as_td_computation p td actor mem1 ==
        dereference_as_td_computation p td actor mem2 /\
        (match dereference_as_td_computation p td actor mem1 with
          | ComputationProduces value -> global_variables_unaddressed_in_object_value vs value
          | _ -> True))
let dereference_as_td_computation_doesnt_depend_on_global_variables
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  (td: object_td_t)
  (actor: tid_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ global_variables_unaddressed_in_pointer vs p
                    /\ global_variables_unaddressed_in_memory vs mem1
                    /\ global_variables_unaddressed_in_memory vs mem2
                    /\ roots_match mem1
                    /\ roots_match mem2)
          (ensures  dereference_as_td_computation p td actor mem1 == dereference_as_td_computation p td actor mem2
                    /\ (match dereference_as_td_computation p td actor mem1 with
                       | ComputationProduces value -> global_variables_unaddressed_in_object_value vs value
                       | _ -> True)) =
  dereference_computation_doesnt_depend_on_global_variables vs p mem1 mem2;
  match dereference_computation p mem1 with
  | ComputationProduces storage ->
      global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value vs actor storage
  | _ -> ()
module Strategies.GlobalVars.Value

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 Strategies.GlobalVars.Unaddressed
open Strategies.PCRelation
open Util.List
open Util.Nth
open Util.Seq
open Util.Trigger

#push-options "--z3rlimit 30"

let rec dereference_computation_doesnt_depend_on_global_variables
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ global_variables_unaddressed_in_pointer vs p
                    /\ global_variables_unaddressed_in_memory vs mem1
                    /\ global_variables_unaddressed_in_memory vs mem2
                    /\ roots_match mem1
                    /\ roots_match mem2)
          (ensures  dereference_computation p mem1 == dereference_computation p mem2
                    /\ (match dereference_computation p mem1 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_doesnt_depend_on_global_variables vs struct_ptr mem1 mem2
  | PointerIndex array_ptr idx ->
      dereference_computation_doesnt_depend_on_global_variables vs array_ptr mem1 mem2
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.fst.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.Sequence.Ambient.fst.checked FStar.Pervasives.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.Value.fst

    vs: Prims.list Armada.Base.var_id_t ->
    p: Armada.Pointer.t ->
    td: Armada.Type.object_td_t ->
    actor: Armada.Base.tid_t ->
    mem1: Armada.Memory.t ->
    mem2: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.memories_match_except_global_variables vs mem1 mem2 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_pointer vs p /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem1 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem2 /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem1 /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem2)
      (ensures
        Armada.Memory.dereference_as_td_computation p td actor mem1 ==
        Armada.Memory.dereference_as_td_computation p td actor mem2 /\
        (match Armada.Memory.dereference_as_td_computation p td actor mem1 with
          | Armada.Computation.ComputationProduces #_ value ->
            Strategies.GlobalVars.global_variables_unaddressed_in_object_value vs value
          | _ -> Prims.l_True))
Prims.list Armada.Base.var_id_t Armada.Pointer.t Armada.Type.object_td_t Armada.Base.tid_t Armada.Memory.t Armada.Memory.dereference_computation Armada.Memory.valid_object_storage_t Strategies.GlobalVars.Unaddressed.global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value Armada.Computation.conditional_computation_t Prims.unit Strategies.GlobalVars.Value.dereference_computation_doesnt_depend_on_global_variables Prims.l_and Strategies.GlobalVars.memories_match_except_global_variables Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_pointer Strategies.GlobalVars.global_variables_unaddressed_in_memory Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.squash Prims.eq2 Armada.Type.valid_object_value_t Armada.Memory.dereference_as_td_computation Strategies.GlobalVars.global_variables_unaddressed_in_object_value Prims.l_True Prims.logical Prims.Nil FStar.Pervasives.pattern
let dereference_as_td_computation_doesnt_depend_on_global_variables
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (td: object_td_t)
      (actor: tid_t)
      (mem1 mem2: Armada.Memory.t)
    : Lemma
      (requires
        memories_match_except_global_variables vs mem1 mem2 /\
        global_variables_unaddressed_in_pointer vs p /\
        global_variables_unaddressed_in_memory vs mem1 /\
        global_variables_unaddressed_in_memory vs mem2 /\ roots_match mem1 /\ roots_match mem2)
      (ensures
        dereference_as_td_computation p td actor mem1 ==
        dereference_as_td_computation p td actor mem2 /\
        (match dereference_as_td_computation p td actor mem1 with
          | ComputationProduces value -> global_variables_unaddressed_in_object_value vs value
          | _ -> True)) =
  
dereference_computation_doesnt_depend_on_global_variables vs p mem1 mem2;
match dereference_computation p mem1 with
| ComputationProduces storage ->
  global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value vs actor storage
| _ -> ()