val update_pointed_to_value_with_gvars_unaddressed_memories_match_on_global_variables
      (vs: list var_id_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 global_variables_unaddressed_in_pointer vs p)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationProduces s' -> states_match_on_global_variables vs s s'
          | _ -> True))
val update_pointed_to_value_with_gvars_unaddressed_memories_match_on_global_variables
      (vs: list var_id_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 global_variables_unaddressed_in_pointer vs p)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationProduces s' -> states_match_on_global_variables vs s s'
          | _ -> True))
let update_pointed_to_value_with_gvars_unaddressed_memories_match_on_global_variables
  (vs: list var_id_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   global_variables_unaddressed_in_pointer vs p)
          (ensures  (match update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer new_value s with
                      | ComputationProduces s' -> states_match_on_global_variables vs s s'
                      | _ -> True)) =
  update_pointer_with_object_with_gvars_unaddressed_memories_match_on_global_variables vs p actor writer_pc
    writer_expression_number bypassing_write_buffer new_value s.mem;
  match update_pointer p actor writer_pc writer_expression_number bypassing_write_buffer new_value s.mem with
  | ComputationProduces (optional_write_message, new_mem) -> begin
      match optional_write_message with
      | Some write_message ->
          let thread = s.threads actor in
          let new_write_buffer = build thread.write_buffer write_message in
          let new_thread = { thread with write_buffer = new_write_buffer } in
          let new_threads = Spec.Map.upd s.threads actor new_thread in
          let s' = { s with mem = new_mem; threads = new_threads; } in
          assert (states_match_on_global_variables vs s s')
      | None ->
          let s' = { s with mem = new_mem; } in
          assert (states_match_on_global_variables vs s s')
      | _ -> false_elim ()
  end
  | _ -> ()
module Strategies.GlobalVarsProof

open FStar.Sequence.Ambient
open FStar.Sequence.Base

open Util.Seq
open Util.Trigger
open Spec.List
open Spec.Ubool

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.Transition
open Armada.UnaryOp

open Strategies.Invariant
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.GlobalVars
open Strategies.GlobalVars.Util
open Strategies.GlobalVars.Unaddressed
open Strategies.ArmadaStatement

let ($$) (#a: Type) (#b: Type) (f: a -> b) (x: a): b = f x
let ($$$) (#a: Type) (f: a -> GTot (conditional_computation_t a)) (x: a): GTot (conditional_computation_t a) = f x

let memories_match_on_global_variables
  (vs: list var_id_t)
  (mem1 mem2: Armada.Memory.t)
  : GTot ubool
  = forall v . list_contains v vs ==>
      mem1 (RootIdGlobal v) == mem2 (RootIdGlobal v)

let states_match_on_global_variables
  (vs: list var_id_t)
  (s1 s2: Armada.State.t)
  : GTot ubool
  = memories_match_on_global_variables vs s1.mem s2.mem


let state_well_formed (vs: list var_id_t) (s: Armada.State.t): GTot ubool =
  roots_match s.mem /\ positions_valid_in_state s /\ global_variables_unaddressed_in_memory vs s.mem

let rec update_pointer_directly_with_gvars_unaddressed_memories_match_on_global_variables
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  (new_storage: valid_object_storage_t)
  (mem: Armada.Memory.t)
  : Lemma (requires global_variables_unaddressed_in_pointer vs p)
          (ensures  otherwise True begin
                      let? mem' = update_pointer_directly p new_storage mem in
                      return $$$ memories_match_on_global_variables vs mem mem'
                    end) =
  match p with
  | PointerField struct_ptr field_id ->
      (match dereference_computation struct_ptr mem with
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageStruct fields ->
                if   field_id >= length fields
                   || neqb (object_storage_to_td new_storage)
                          (object_storage_to_td (index fields field_id)) then
                  ()
                  else (
                  let new_parent = update_storage_child parent field_id new_storage in
                    update_pointer_directly_with_gvars_unaddressed_memories_match_on_global_variables
                      vs struct_ptr new_parent mem
                )
            | _ -> ())
      | _ -> ())
  | PointerIndex array_ptr idx ->
      (match dereference_computation array_ptr mem with
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageArray element_td elements ->
                if   idx < 0
                   || idx >= length elements
                   || neqb (object_storage_to_td new_storage) element_td then
                  ()
                else (
                  let new_parent = update_storage_child parent idx new_storage in
                  update_pointer_directly_with_gvars_unaddressed_memories_match_on_global_variables
                    vs array_ptr new_parent mem
                )
            | _ -> ())
      | _ -> ())
  | _ -> ()

let update_pointer_with_object_with_gvars_unaddressed_memories_match_on_global_variables
  (vs: list var_id_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 global_variables_unaddressed_in_pointer vs p)
          (ensures  otherwise True begin
                      let? v = update_pointer p actor writer_pc writer_expression_number bypassing_write_buffer new_value mem in
                      return $$$ memories_match_on_global_variables vs mem (snd v)
                    end) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id ->
      let root = mem root_id in
      (match root_to_storage_computation root with
       | ComputationProduces storage ->
           ()
       | _ -> ())
  | PointerField struct_ptr field_id ->
      (match dereference_computation struct_ptr mem with
       | 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
                    | 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_with_gvars_unaddressed_memories_match_on_global_variables
                            vs struct_ptr new_parent mem
                        )
                    | _ -> ()
                   ))
          | _ -> ())
       | _ -> ())
  | PointerIndex array_ptr idx ->
      (match dereference_computation array_ptr mem with
       | 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
                    | 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_with_gvars_unaddressed_memories_match_on_global_variables
                            vs array_ptr new_parent mem
                        )
                    | _ -> ()
                   ))
          | _ -> ())
       | _ -> ())
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Strategies.Invariant.fsti.checked Strategies.GlobalVars.Util.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaStatement.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.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.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.GlobalVarsProof.fst

    vs: Prims.list Armada.Base.var_id_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.global_variables_unaddressed_in_pointer vs p)
      (ensures
        ((match
              Armada.Expression.update_pointed_to_value p
                actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                new_value
                s
            with
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.GlobalVarsProof.states_match_on_global_variables vs s s'
            | _ -> Prims.l_True)
          <:
          Type0))
Prims.list Armada.Base.var_id_t Armada.Pointer.t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Armada.Type.object_value_t Armada.State.t Armada.Memory.update_pointer Armada.State.__proj__Mkt__item__mem FStar.Pervasives.Native.option Armada.Thread.write_message_t Armada.Memory.t Prims._assert Strategies.GlobalVarsProof.states_match_on_global_variables Armada.State.Mkt Armada.State.__proj__Mkt__item__initial_tid Armada.State.__proj__Mkt__item__uniqs_used Armada.State.__proj__Mkt__item__trace Armada.State.__proj__Mkt__item__stop_reason Spec.Map.t Armada.Thread.t Spec.Map.upd Armada.State.__proj__Mkt__item__threads Armada.Thread.Mkt Armada.Thread.__proj__Mkt__item__status Armada.Thread.__proj__Mkt__item__pc Armada.Thread.__proj__Mkt__item__top Armada.Thread.__proj__Mkt__item__stack Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers FStar.Sequence.Base.seq FStar.Sequence.Base.build Armada.Thread.__proj__Mkt__item__write_buffer FStar.Pervasives.false_elim Prims.unit Armada.Computation.conditional_computation_t FStar.Pervasives.Native.tuple2 Strategies.GlobalVarsProof.update_pointer_with_object_with_gvars_unaddressed_memories_match_on_global_variables Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_pointer Prims.squash Armada.Expression.update_pointed_to_value Prims.l_True Prims.Nil FStar.Pervasives.pattern
let update_pointed_to_value_with_gvars_unaddressed_memories_match_on_global_variables
      (vs: list var_id_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 global_variables_unaddressed_in_pointer vs p)
      (ensures
        (match
            update_pointed_to_value p
              actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              new_value
              s
          with
          | ComputationProduces s' -> states_match_on_global_variables vs s s'
          | _ -> True)) =
  
update_pointer_with_object_with_gvars_unaddressed_memories_match_on_global_variables vs
  p
  actor
  writer_pc
  writer_expression_number
  bypassing_write_buffer
  new_value
  s.mem;
match
  update_pointer p actor writer_pc writer_expression_number bypassing_write_buffer new_value s.mem
with
| ComputationProduces (optional_write_message, new_mem) ->
  (match optional_write_message with
    | Some write_message ->
      let thread = s.threads actor in
      let new_write_buffer = build thread.write_buffer write_message in
      let new_thread = { thread with write_buffer = new_write_buffer } in
      let new_threads = Spec.Map.upd s.threads actor new_thread in
      let s' = { s with mem = new_mem; threads = new_threads } in
      assert (states_match_on_global_variables vs s s')
    | None ->
      let s' = { s with mem = new_mem } in
      assert (states_match_on_global_variables vs s s')
    | _ -> false_elim ())
| _ -> ()