val rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
      (vs: list var_id_t)
      (exps: list expression_t)
      (actor: tid_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        global_variables_unaddressed_in_rvalue_expressions vs exps /\ positions_valid_in_state s /\
        global_variables_unaddressed_in_memory vs s.mem /\ roots_match s.mem)
      (ensures
        (match rvalues_computation exps actor s with
          | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
          | _ -> True))
      (decreases exps)
val rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
      (vs: list var_id_t)
      (exps: list expression_t)
      (actor: tid_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        global_variables_unaddressed_in_rvalue_expressions vs exps /\ positions_valid_in_state s /\
        global_variables_unaddressed_in_memory vs s.mem /\ roots_match s.mem)
      (ensures
        (match rvalues_computation exps actor s with
          | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
          | _ -> True))
      (decreases exps)
let rec rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
  (vs: list var_id_t)
  (exp: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires   global_variables_unaddressed_in_rvalue_expression vs exp
                    /\ positions_valid_in_state s
                    /\ global_variables_unaddressed_in_memory vs s.mem
                    /\ roots_match s.mem)
          (ensures  (match rvalue_computation exp actor s with
                     | ComputationProduces value -> global_variables_unaddressed_in_object_value vs value
                     | _ -> True))
          (decreases exp) =
  if not (expression_valid exp) then
    ()
  else
    match exp with
    | ExpressionConstant value -> ()
    | ExpressionGlobalVariable td var_id ->
        dereference_as_td_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs
          (PointerRoot (RootIdGlobal var_id)) td actor s.mem
    | ExpressionLocalVariable td var_id ->
        let thread = s.threads actor in
        if list_contains var_id thread.top.local_variables then
          dereference_as_td_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs
            (PointerRoot (RootIdStack actor thread.top.method_id thread.top.frame_uniq var_id)) td actor s.mem
        else
          ()
    | ExpressionUnaryOperator _ _ operator operand ->
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs operand actor s
    | ExpressionBinaryOperator _ _ _ operator operand1 operand2 ->
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs operand1 actor s;
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs operand2 actor s
    | ExpressionIf _ cond operand_then operand_else ->
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs cond actor s;
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs operand_then actor s;
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs operand_else actor s
    | ExpressionDereference td ptr ->
        (match rvalue_computation ptr actor s with
         | ComputationProduces ptr_value ->
             let p = PrimitiveBoxPointer?.ptr (ObjectValuePrimitive?.value ptr_value) in
             dereference_as_td_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs p td actor
               s.mem
         | _ -> ())
    | ExpressionAddressOf obj ->
        lvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs obj actor s
    | ExpressionPointerOffset ptr offset ->
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs ptr actor s
    | ExpressionFieldOf td obj field_id ->
        (match lvalue_computation obj actor s with
         | ComputationProduces obj_ptr ->
             dereference_as_td_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs
               (PointerField obj_ptr field_id) td actor s.mem
         | _ -> ())
    | ExpressionAllocated ptr ->
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs ptr actor s
    | ExpressionApplyFunction td operands return_type operand_types fn ->
        rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs operands actor s
    | ExpressionIfUndefined td potentially_unsafe safe_substitution ->
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs
          potentially_unsafe actor s;
        rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs
          safe_substitution actor s
    | ExpressionInitialTid -> ()
    | ExpressionUniqsUsed -> ()
    | ExpressionStopReason -> ()

and lvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
  (vs: list var_id_t)
  (exp: expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires   global_variables_unaddressed_in_lvalue_expression vs exp
                    /\ positions_valid_in_state s
                    /\ global_variables_unaddressed_in_memory vs s.mem
                    /\ roots_match s.mem)
          (ensures  (match lvalue_computation exp actor s with
                     | ComputationProduces p -> global_variables_unaddressed_in_pointer vs p
                     | _ -> True))
          (decreases exp) =
  match exp with
  | ExpressionGlobalVariable _ var_id -> ()
  | ExpressionLocalVariable _ var_id -> ()
  | ExpressionDereference _ ptr ->
      rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs ptr actor s
  | ExpressionFieldOf td obj field_id ->
      lvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs obj actor s
  | _ -> ()
  
and rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
  (vs: list var_id_t)
  (exps: list expression_t)
  (actor: tid_t)
  (s: Armada.State.t)
  : Lemma (requires   global_variables_unaddressed_in_rvalue_expressions vs exps
                    /\ positions_valid_in_state s
                    /\ global_variables_unaddressed_in_memory vs s.mem
                    /\ roots_match s.mem)
          (ensures  (match rvalues_computation exps actor s with
                     | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
                     | _ -> True))
          (decreases exps) =
  match exps with
  | [] -> ()
  | exp :: exps' ->
      rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs exp actor s;
      rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs exps' actor s
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


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

let dereference_as_td_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  (td: object_td_t)
  (actor: tid_t)
  (mem: Armada.Memory.t)
  : Lemma (requires   global_variables_unaddressed_in_memory vs mem
                    /\ roots_match mem)
          (ensures  (match dereference_as_td_computation p td actor mem with
                     | ComputationProduces value -> global_variables_unaddressed_in_object_value vs value
                     | _ -> True)) =
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs p mem;
  match dereference_computation p mem with
  | ComputationProduces storage ->
      global_variables_unaddressed_in_storage_implies_unaddressed_in_object_value vs actor storage
  | _ -> ()

#push-options "--z3rlimit 30"
/
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 ->
    exps: Prims.list Armada.Expression.expression_t ->
    actor: Armada.Base.tid_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.global_variables_unaddressed_in_rvalue_expressions vs exps /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs (Mkt?.mem s) /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match (Mkt?.mem s))
      (ensures
        ((match Armada.Expression.rvalues_computation exps actor s with
            | Armada.Computation.ComputationProduces #_ values ->
              Strategies.GlobalVars.global_variables_unaddressed_in_object_values vs values
            | _ -> Prims.l_True)
          <:
          Type0))
      (decreases exps)
Prims.list Armada.Base.var_id_t Armada.Expression.expression_t Armada.Base.tid_t Armada.State.t Strategies.GlobalVars.Unaddressed.rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed Prims.unit Strategies.GlobalVars.Unaddressed.rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed Prims.l_and Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_rvalue_expressions Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Strategies.GlobalVars.global_variables_unaddressed_in_memory Armada.State.__proj__Mkt__item__mem Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.squash Armada.Expression.rvalues_computation Armada.Type.object_value_t Strategies.GlobalVars.global_variables_unaddressed_in_object_values Armada.Computation.conditional_computation_t Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed
      (vs: list var_id_t)
      (exps: list expression_t)
      (actor: tid_t)
      (s: Armada.State.t)
    : Lemma
      (requires
        global_variables_unaddressed_in_rvalue_expressions vs exps /\ positions_valid_in_state s /\
        global_variables_unaddressed_in_memory vs s.mem /\ roots_match s.mem)
      (ensures
        (match rvalues_computation exps actor s with
          | ComputationProduces values -> global_variables_unaddressed_in_object_values vs values
          | _ -> True))
      (decreases exps) =
  
match exps with
| [] -> ()
| exp :: exps' ->
  rvalue_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs exp actor s;
  rvalues_computation_when_gvars_unaddressed_produces_value_with_gvars_unaddressed vs exps' actor s