val update_pointed_to_value_maintains_gvar_has_type
      (v: var_id_t)
      (td: object_td_t)
      (p: Armada.Pointer.t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma (requires gvar_has_type s.mem v td)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> gvar_has_type s'.mem v td))
val update_pointed_to_value_maintains_gvar_has_type
      (v: var_id_t)
      (td: object_td_t)
      (p: Armada.Pointer.t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma (requires gvar_has_type s.mem v td)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> gvar_has_type s'.mem v td))
let update_pointed_to_value_maintains_gvar_has_type
  (v: var_id_t)
  (td: object_td_t)
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (requires gvar_has_type s.mem v td)
          (ensures  (match update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> gvar_has_type s'.mem v td)) =
  update_pointer_maintains_gvar_has_type v td p actor writer_pc writer_expression_number bypassing_write_buffer
    new_value s.mem
module Strategies.GlobalVars.Types

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement
open Util.List
open Util.Tactics

let gvar_has_type (mem: Armada.Memory.t) (v: var_id_t) (td: object_td_t) : GTot ubool =
  let root_id = RootIdGlobal v in
  let root = mem root_id in
  match root with
  | RootGlobal storage -> object_storage_to_td storage == td
  | _ -> False

let all_gvars_have_types (mem: Armada.Memory.t) (vs: list var_id_t) (tds: list object_td_t) : GTot ubool =
  lists_correspond_ubool (gvar_has_type mem) vs tds

let rec update_pointer_directly_maintains_gvar_has_type
  (v: var_id_t)
  (td: object_td_t)
  (p: Armada.Pointer.t)
  (new_storage: valid_object_storage_t)
  (mem: Armada.Memory.t)
  : Lemma (requires gvar_has_type mem v td)
          (ensures  (match update_pointer_directly p new_storage mem with
                     | ComputationProduces mem' -> gvar_has_type mem' v td
                     | _ -> True)) =
  match update_pointer_directly p new_storage mem with
  | ComputationImpossible | ComputationUndefined -> ()
  | ComputationProduces mem' ->
      (match p with
       | PointerField struct_ptr field_id ->
           let parent = ComputationProduces?.result (dereference_computation struct_ptr mem) in
           (match parent with
            | ObjectStorageStruct fields ->
                let new_parent = update_storage_child parent field_id new_storage in
                update_pointer_directly_maintains_gvar_has_type v td struct_ptr new_parent mem)
       | PointerIndex array_ptr idx ->
           let parent = ComputationProduces?.result (dereference_computation array_ptr mem) in
           (match parent with
            | ObjectStorageArray element_td elements ->
                let new_parent = update_storage_child parent idx new_storage in
                update_pointer_directly_maintains_gvar_has_type v td array_ptr new_parent mem)
       | PointerRoot root_id -> ()
       | _ -> ())

#push-options "--z3rlimit 10"

let update_pointer_maintains_gvar_has_type
  (v: var_id_t)
  (td: object_td_t)
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (mem: Armada.Memory.t)
  : Lemma (requires gvar_has_type mem v td)
          (ensures  (match update_pointer p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value mem with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces (optional_write_message, mem') -> gvar_has_type mem' v td)) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr field_id ->
      (match dereference_computation struct_ptr mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageStruct fields ->
                if field_id >= length fields then
                  ()
                else
                  let field = index fields field_id in
                  if   not (object_storage_valid field)
                     || neqb (object_storage_to_td field) (object_value_to_td new_value) then
                    ()
                  else
                    (match update_storage p actor writer_pc writer_expression_number
                             bypassing_write_buffer field new_value with
                     | ComputationImpossible | ComputationUndefined -> ()
                     | ComputationProduces (write_message, new_field) ->
                         if (not (can_update_storage_child parent field_id new_field)) then
                           ()
                         else
                           let new_parent = update_storage_child parent field_id new_field in
                           update_pointer_directly_maintains_gvar_has_type v td struct_ptr new_parent mem)
            | _ -> ()))
  | PointerIndex array_ptr idx ->
      (match dereference_computation array_ptr mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageArray element_td elements ->
                if idx < 0 || idx >= length elements then
                  ()
                else
                  let element = index elements idx in
                  if not (object_storage_valid element) then
                    ()
                  else
                    (match update_storage p actor writer_pc writer_expression_number
                             bypassing_write_buffer element new_value with
                     | ComputationImpossible | ComputationUndefined -> ()
                     | ComputationProduces (write_message, new_element) ->
                         if not (can_update_storage_child parent idx new_element) then
                           ()
                         else
                           let new_parent = update_storage_child parent idx new_element in
                           update_pointer_directly_maintains_gvar_has_type v td array_ptr new_parent mem)
            | _ -> ()))

#pop-options
/
Util.Tactics.fst.checked Util.List.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.GlobalVars.Types.fst

    v: Armada.Base.var_id_t ->
    td: Armada.Type.object_td_t ->
    p: Armada.Pointer.t ->
    actor: Armada.Base.tid_t ->
    writer_pc: Armada.Base.pc_t ->
    writer_expression_number: Prims.nat ->
    bypassing_write_buffer: Prims.bool ->
    new_value: Armada.Type.object_value_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma (requires Strategies.GlobalVars.Types.gvar_has_type (Mkt?.mem s) v td)
      (ensures
        ((match
              Armada.Expression.update_pointed_to_value p
                actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                new_value
                s
            with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.GlobalVars.Types.gvar_has_type (Mkt?.mem s') v td)
          <:
          Type0))
Armada.Base.var_id_t Armada.Type.object_td_t Armada.Pointer.t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Armada.Type.object_value_t Armada.State.t Strategies.GlobalVars.Types.update_pointer_maintains_gvar_has_type Armada.State.__proj__Mkt__item__mem Prims.unit Strategies.GlobalVars.Types.gvar_has_type Prims.squash Armada.Expression.update_pointed_to_value Prims.l_True Prims.Nil FStar.Pervasives.pattern
let update_pointed_to_value_maintains_gvar_has_type
      (v: var_id_t)
      (td: object_td_t)
      (p: Armada.Pointer.t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (new_value: object_value_t)
      (s: Armada.State.t)
    : Lemma (requires gvar_has_type s.mem v td)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> gvar_has_type s'.mem v td)) =
  
update_pointer_maintains_gvar_has_type v
  td
  p
  actor
  writer_pc
  writer_expression_number
  bypassing_write_buffer
  new_value
  s.mem