val push_stack_variable_doesnt_depend_on_gvars_helper
      (vs: list var_id_t)
      (actor: tid_t)
      (writer_pc1 writer_pc2: pc_t)
      (writer_expression_number1 writer_expression_number2: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (initializer: initializer_t)
      (s1 s2: Armada.State.t)
      (thread1 thread2: Armada.Thread.t)
      (local_variables1' local_variables2': list var_id_t)
      (top1' top2': stack_frame_t)
      (thread1' thread2': Armada.Thread.t)
      (threads1' threads2': Armada.Threads.t)
    : Lemma
      (requires
        positions_valid_in_state s1 /\ positions_valid_in_state s2 /\
        positions_in_write_buffers_match_except_global_variables vs s1.threads s2.threads /\
        thread1 == s1.threads actor /\ thread2 == s2.threads actor /\
        local_variables1' == initializer.var_id :: thread1.top.local_variables /\
        local_variables2' == initializer.var_id :: thread2.top.local_variables /\
        top1' == { thread1.top with local_variables = local_variables1' } /\
        top2' == { thread2.top with local_variables = local_variables2' } /\
        thread1' == { thread1 with top = top1' } /\ thread2' == { thread2 with top = top2' } /\
        threads1' == Spec.Map.upd s1.threads actor thread1' /\
        threads2' == Spec.Map.upd s2.threads actor thread2' /\ positions_valid_in_threads threads1' /\
        positions_valid_in_threads threads2')
      (ensures positions_in_write_buffers_match_except_global_variables vs threads1' threads2')
val push_stack_variable_doesnt_depend_on_gvars_helper
      (vs: list var_id_t)
      (actor: tid_t)
      (writer_pc1 writer_pc2: pc_t)
      (writer_expression_number1 writer_expression_number2: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (initializer: initializer_t)
      (s1 s2: Armada.State.t)
      (thread1 thread2: Armada.Thread.t)
      (local_variables1' local_variables2': list var_id_t)
      (top1' top2': stack_frame_t)
      (thread1' thread2': Armada.Thread.t)
      (threads1' threads2': Armada.Threads.t)
    : Lemma
      (requires
        positions_valid_in_state s1 /\ positions_valid_in_state s2 /\
        positions_in_write_buffers_match_except_global_variables vs s1.threads s2.threads /\
        thread1 == s1.threads actor /\ thread2 == s2.threads actor /\
        local_variables1' == initializer.var_id :: thread1.top.local_variables /\
        local_variables2' == initializer.var_id :: thread2.top.local_variables /\
        top1' == { thread1.top with local_variables = local_variables1' } /\
        top2' == { thread2.top with local_variables = local_variables2' } /\
        thread1' == { thread1 with top = top1' } /\ thread2' == { thread2 with top = top2' } /\
        threads1' == Spec.Map.upd s1.threads actor thread1' /\
        threads2' == Spec.Map.upd s2.threads actor thread2' /\ positions_valid_in_threads threads1' /\
        positions_valid_in_threads threads2')
      (ensures positions_in_write_buffers_match_except_global_variables vs threads1' threads2')
let push_stack_variable_doesnt_depend_on_gvars_helper
  (vs: list var_id_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializer: initializer_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  (thread1: Armada.Thread.t)
  (thread2: Armada.Thread.t)
  (local_variables1': list var_id_t)
  (local_variables2': list var_id_t)
  (top1': stack_frame_t)
  (top2': stack_frame_t)
  (thread1': Armada.Thread.t)
  (thread2': Armada.Thread.t)
  (threads1': Armada.Threads.t)
  (threads2': Armada.Threads.t)
  : Lemma (requires   positions_valid_in_state s1
                    /\ positions_valid_in_state s2
                    /\ positions_in_write_buffers_match_except_global_variables vs s1.threads s2.threads
                    /\ thread1 == s1.threads actor
                    /\ thread2 == s2.threads actor
                    /\ local_variables1' == initializer.var_id :: thread1.top.local_variables
                    /\ local_variables2' == initializer.var_id :: thread2.top.local_variables
                    /\ top1' == { thread1.top with local_variables = local_variables1' }
                    /\ top2' == { thread2.top with local_variables = local_variables2' }
                    /\ thread1' == { thread1 with top = top1' }
                    /\ thread2' == { thread2 with top = top2' }
                    /\ threads1' == Spec.Map.upd s1.threads actor thread1'
                    /\ threads2' == Spec.Map.upd s2.threads actor thread2'
                    /\ positions_valid_in_threads threads1'
                    /\ positions_valid_in_threads threads2')
          (ensures  positions_in_write_buffers_match_except_global_variables vs threads1' threads2') =
  introduce forall sender_tid receiver_tid. write_buffers_match_except_global_variables vs
                                         (unread_write_buffer threads1' sender_tid receiver_tid)
                                         (unread_write_buffer threads2' sender_tid receiver_tid)
  with (
    assert (sender_receiver_trigger sender_tid receiver_tid);
    assert (write_buffers_match_except_global_variables vs
               (unread_write_buffer s1.threads sender_tid receiver_tid)
               (unread_write_buffer s2.threads sender_tid receiver_tid));
    assert (unread_write_buffer threads1' sender_tid receiver_tid ==
              unread_write_buffer s1.threads sender_tid receiver_tid);
    assert (unread_write_buffer threads2' sender_tid receiver_tid ==
              unread_write_buffer s2.threads sender_tid receiver_tid)
  );
  assert (positions_in_write_buffers_match_except_global_variables vs threads1' threads2')
module Strategies.GlobalVars.Util

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

let memories_match_except_global_variables_reflexive (vs: list var_id_t) (mem: Armada.Memory.t)
  : Lemma (memories_match_except_global_variables vs mem mem) =
  ()

let memories_match_except_global_variables_commutative
  (vs: list var_id_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (memories_match_except_global_variables vs mem1 mem2 <==>
             memories_match_except_global_variables vs mem2 mem1) =
  ()

let memories_match_except_global_variables_transitive
  (vs: list var_id_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  (mem3: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ memories_match_except_global_variables vs mem2 mem3)
          (ensures  memories_match_except_global_variables vs mem1 mem3) =
  introduce forall root_id. (match root_id with
                        | RootIdGlobal v -> list_contains v vs \/ (mem1 root_id == mem3 root_id)
                        | _ -> mem1 root_id == mem3 root_id)
  with (
    match root_id with
    | RootIdGlobal v ->
        assert (list_contains v vs \/ (mem1 root_id == mem2 root_id));
        assert (list_contains v vs \/ (mem2 root_id == mem3 root_id))
    | _ ->
        assert (mem1 root_id == mem2 root_id);
        assert (mem2 root_id == mem3 root_id)
  )

let equality_pc_relation_implies_state_matches_itself_except_global_variables
  (vs: list var_id_t)
  (s: Armada.State.t)
  : Lemma (requires positions_valid_in_state s)
          (ensures  states_match_except_global_variables vs equality_pc_relation s s) =
  introduce forall tid. stacks_match_per_pc_relation equality_pc_relation (s.threads tid).stack (s.threads tid).stack
  with equality_pc_relation_implies_stack_matches_itself (s.threads tid).stack;
  assert (threads_match_except_write_buffers_per_pc_relation equality_pc_relation s.threads s.threads);
  introduce forall sender_tid receiver_tid.
              sender_receiver_trigger sender_tid receiver_tid ==>
              write_buffers_match_except_global_variables vs
                (unread_write_buffer s.threads sender_tid receiver_tid)
                (unread_write_buffer s.threads sender_tid receiver_tid)
  with introduce _ ==> _
  with _.
    equality_pc_relation_implies_write_buffer_matches_itself
      (remove_global_variables_from_write_buffer vs
        (seq_to_list (unread_write_buffer s.threads sender_tid receiver_tid)))

#push-options "--z3rlimit 60"

let update_expression_lacking_pointer_field_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expression vs exp
                    /\ object_td_lacks_pointer_field (expression_to_td exp))
          (ensures  (match update_expression exp actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_value s1,
                           update_expression exp actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_value s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                           states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else (
    lvalue_computation_doesnt_depend_on_global_variables vs pc_relation exp actor s1 s2;
    assert (lvalue_computation exp actor s1 == lvalue_computation exp actor s2);
    let td = expression_to_td exp in
    match lvalue_computation exp actor s1 with
    | ComputationProduces p ->
        update_pointed_to_value_lacking_pointer_field_maintains_states_match vs pc_relation p actor
          writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2 bypassing_write_buffer
          td new_value s1 s2;
        (match update_pointed_to_value p actor writer_pc1 writer_expression_number1 bypassing_write_buffer
                 new_value s1,
               update_pointed_to_value p actor writer_pc2 writer_expression_number2 bypassing_write_buffer
                 new_value s2 with
         | ComputationProduces s1', ComputationProduces s2' -> ()
         | ComputationImpossible, ComputationImpossible -> ()
         | ComputationUndefined, ComputationUndefined -> ()
         | _, _ -> false_elim ())
    | _ -> ()
  )

#pop-options
#push-options "--z3rlimit 80"

let update_expression_with_gvars_unaddressed_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expression vs exp
                    /\ global_variables_unaddressed_in_object_value vs new_value)
          (ensures  (match update_expression exp actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_value s1,
                           update_expression exp actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_value s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                           states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else (
    lvalue_computation_doesnt_depend_on_global_variables vs pc_relation exp actor s1 s2;
    assert (lvalue_computation exp actor s1 == lvalue_computation exp actor s2);
    let td = expression_to_td exp in
    match lvalue_computation exp actor s1 with
    | ComputationProduces p ->
        update_pointed_to_value_with_gvars_unaddressed_maintains_states_match vs pc_relation
          p actor writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2 bypassing_write_buffer
          new_value s1 s2;
        (match update_pointed_to_value p actor writer_pc1 writer_expression_number1 bypassing_write_buffer
                 new_value s1,
               update_pointed_to_value p actor writer_pc2 writer_expression_number2 bypassing_write_buffer
                 new_value s2 with
         | ComputationProduces s1', ComputationProduces s2' -> ()
         | ComputationImpossible, ComputationImpossible -> ()
         | ComputationUndefined, ComputationUndefined -> ()
         | _, _ -> false_elim ())
    | _ -> ()
  )

#pop-options
#push-options "--z3rlimit 10"

let rec update_expressions_with_gvars_unaddressed_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expressions vs exps
                    /\ global_variables_unaddressed_in_object_values vs new_values)
          (ensures  (match update_expressions exps actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_values s1,
                           update_expressions exps actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_values s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                            states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_with_gvars_unaddressed_maintains_states_match vs pc_relation
        first_exp actor writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2
        bypassing_write_buffer first_new_value s1 s2;
      (match update_expression first_exp actor writer_pc1 writer_expression_number1
               bypassing_write_buffer first_new_value s1,
             update_expression first_exp actor writer_pc2 writer_expression_number2
               bypassing_write_buffer first_new_value s2 with
       | ComputationProduces s1_next, ComputationProduces s2_next ->
           update_expressions_with_gvars_unaddressed_maintains_states_match vs pc_relation
             remaining_exps actor writer_pc1 writer_pc2 (writer_expression_number1 + 1) (writer_expression_number2 + 1)
             bypassing_write_buffer remaining_new_values s1_next s2_next;
           (match update_expressions exps actor writer_pc1 writer_expression_number1
                    bypassing_write_buffer new_values s1,
                  update_expressions exps actor writer_pc2 writer_expression_number2
                    bypassing_write_buffer new_values s2 with
            | ComputationProduces s1', ComputationProduces s2' -> ()
            | ComputationImpossible, ComputationImpossible -> ()
            | ComputationUndefined, ComputationUndefined -> ()
            | _, _ -> ())
       | ComputationImpossible, ComputationImpossible -> ()
       | ComputationUndefined, ComputationUndefined -> ()
       | _, _ -> ())
  | _, _ -> ()

let rec update_expressions_lacking_pointer_field_maintains_states_match
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc1: pc_t)
  (writer_pc2: pc_t)
  (writer_expression_number1: nat)
  (writer_expression_number2: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expressions vs exps
                    /\ expressions_lack_pointer_field exps)
          (ensures  (match update_expressions exps actor writer_pc1 writer_expression_number1
                             bypassing_write_buffer new_values s1,
                           update_expressions exps actor writer_pc2 writer_expression_number2
                             bypassing_write_buffer new_values s2 with
                     | ComputationProduces s1', ComputationProduces s2' ->
                           states_match_except_global_variables vs pc_relation s1' s2'
                         /\ global_variables_unaddressed_in_memory vs s1'.mem
                         /\ global_variables_unaddressed_in_memory vs s2'.mem
                         /\ roots_match s1'.mem
                         /\ roots_match s2'.mem
                         /\ ThreadStatusRunning? (s1'.threads actor).status
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_lacking_pointer_field_maintains_states_match vs pc_relation
        first_exp actor writer_pc1 writer_pc2 writer_expression_number1 writer_expression_number2
        bypassing_write_buffer first_new_value s1 s2;
      (match update_expression first_exp actor writer_pc1 writer_expression_number1
               bypassing_write_buffer first_new_value s1,
             update_expression first_exp actor writer_pc2 writer_expression_number2
               bypassing_write_buffer first_new_value s2 with
       | ComputationProduces s1_next, ComputationProduces s2_next ->
           update_expressions_lacking_pointer_field_maintains_states_match vs pc_relation
             remaining_exps actor writer_pc1 writer_pc2 (writer_expression_number1 + 1) (writer_expression_number2 + 1)
             bypassing_write_buffer remaining_new_values s1_next s2_next;
           (match update_expressions exps actor writer_pc1 writer_expression_number1
                    bypassing_write_buffer new_values s1,
                  update_expressions exps actor writer_pc2 writer_expression_number2
                    bypassing_write_buffer new_values s2 with
            | ComputationProduces s1', ComputationProduces s2' -> ()
            | ComputationImpossible, ComputationImpossible -> ()
            | ComputationUndefined, ComputationUndefined -> ()
            | _, _ -> ())
       | ComputationImpossible, ComputationImpossible -> ()
       | ComputationUndefined, ComputationUndefined -> ()
       | _, _ -> ())
  | _, _ -> ()

let propagate_write_message_maintains_states_match
  (vs: list var_id_t)
  (write_message1: write_message_t)
  (write_message2: write_message_t)
  (receiver_tid: tid_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ global_variables_unaddressed_in_memory vs mem1
                    /\ global_variables_unaddressed_in_memory vs mem2
                    /\ roots_match mem1
                    /\ roots_match mem2
                    /\ global_variables_unaddressed_in_write_message vs write_message1
                    /\ global_variables_unaddressed_in_write_message vs write_message2
                    /\ write_messages_match write_message1 write_message2)
          (ensures  (match propagate_write_message write_message1 receiver_tid mem1,
                           propagate_write_message write_message2 receiver_tid mem2 with
                     | ComputationProduces mem1', ComputationProduces mem2' ->
                           memories_match_except_global_variables vs mem1' mem2'
                         /\ global_variables_unaddressed_in_memory vs mem1'
                         /\ global_variables_unaddressed_in_memory vs mem2'
                         /\ roots_match mem1'
                         /\ roots_match mem2'
                     | ComputationImpossible, ComputationImpossible -> True
                     | ComputationUndefined, ComputationUndefined -> True
                     | _ -> False)) =
  let p = write_message1.location in
  dereference_computation_doesnt_depend_on_global_variables vs p mem1 mem2;
  match dereference_computation p mem1 with
  | ComputationProduces storage ->
      (match storage with
       | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
           if   primitive_td <> write_message1.primitive_td
              || write_message1.version >= length values
              || local_versions receiver_tid >= write_message1.version then
             ()
           else
             let new_local_versions = Spec.Map.upd local_versions receiver_tid write_message1.version in
             let new_storage = ObjectStorageWeaklyConsistentPrimitive primitive_td values
                                 new_local_versions in
             if not (object_storage_valid new_storage) then
               ()
             else
               update_pointer_directly_with_gvars_unaddressed_maintains_states_match vs p
                 new_storage mem1 mem2
       | _ -> ()
     )
  | _ -> ()

let propagate_write_message_s1_only_among_gvars_maintains_states_match
  (vs: list var_id_t)
  (write_message1: write_message_t)
  (receiver_tid: tid_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ global_variables_unaddressed_in_memory vs mem1
                    /\ global_variables_unaddressed_in_memory vs mem2
                    /\ roots_match mem1
                    /\ roots_match mem2
                    /\ not (global_variables_unaddressed_in_write_message vs write_message1))
          (ensures  (match propagate_write_message write_message1 receiver_tid mem1 with
                     | ComputationProduces mem1' ->
                           memories_match_except_global_variables vs mem1' mem2
                         /\ global_variables_unaddressed_in_memory vs mem1'
                         /\ roots_match mem1'
                     | ComputationImpossible -> True
                     | ComputationUndefined -> True)) =
  let p = write_message1.location in
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs p mem1;
  match dereference_computation p mem1 with
  | ComputationProduces storage ->
      (match storage with
       | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
           if   primitive_td <> write_message1.primitive_td
              || write_message1.version >= length values
              || local_versions receiver_tid >= write_message1.version then
             ()
           else (
             let new_local_versions = Spec.Map.upd local_versions receiver_tid write_message1.version in
             let new_storage = ObjectStorageWeaklyConsistentPrimitive primitive_td values
                                 new_local_versions in
             assert (global_variables_unaddressed_in_storage vs new_storage);
             if not (object_storage_valid new_storage) then
               ()
             else
               update_pointer_directly_s1_only_among_gvars_maintains_states_match vs p new_storage mem1 mem2
           )
       | _ -> ()
     )
  | _ -> ()

let propagate_write_message_s2_only_among_gvars_maintains_states_match
  (vs: list var_id_t)
  (write_message2: write_message_t)
  (receiver_tid: tid_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (requires   memories_match_except_global_variables vs mem1 mem2
                    /\ global_variables_unaddressed_in_memory vs mem1
                    /\ global_variables_unaddressed_in_memory vs mem2
                    /\ roots_match mem1
                    /\ roots_match mem2
                    /\ not (global_variables_unaddressed_in_write_message vs write_message2))
          (ensures  (match propagate_write_message write_message2 receiver_tid mem2 with
                     | ComputationProduces mem2' ->
                           memories_match_except_global_variables vs mem1 mem2'
                         /\ global_variables_unaddressed_in_memory vs mem2'
                         /\ roots_match mem2'
                     | ComputationImpossible -> True
                     | ComputationUndefined -> True)) =
  let p = write_message2.location in
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs p mem2;
  match dereference_computation p mem2 with
  | ComputationProduces storage ->
      (match storage with
       | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
           if   primitive_td <> write_message2.primitive_td
              || write_message2.version >= length values
              || local_versions receiver_tid >= write_message2.version then
             ()
           else (
             let new_local_versions = Spec.Map.upd local_versions receiver_tid write_message2.version in
             let new_storage = ObjectStorageWeaklyConsistentPrimitive primitive_td values
                                 new_local_versions in
             assert (global_variables_unaddressed_in_storage vs new_storage);
             if not (object_storage_valid new_storage) then
               ()
             else
               update_pointer_directly_s2_only_among_gvars_maintains_states_match vs p new_storage mem1 mem2
           )
       | _ -> ()
     )
  | _ -> ()

let check_expression_up_to_date_for_rmw_doesnt_depend_on_gvars
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (exp: expression_t)
  (actor: tid_t)
  (s1: Armada.State.t)
  (s2: Armada.State.t)
  : Lemma (requires   states_match_except_global_variables vs pc_relation s1 s2
                    /\ global_variables_unaddressed_in_memory vs s1.mem
                    /\ global_variables_unaddressed_in_memory vs s2.mem
                    /\ roots_match s1.mem
                    /\ roots_match s2.mem
                    /\ ThreadStatusRunning? (s1.threads actor).status
                    /\ global_variables_unmentioned_in_expression vs exp)
          (ensures  check_expression_up_to_date_for_rmw exp actor s1 ==
                    check_expression_up_to_date_for_rmw exp actor s2) =
  if not (expression_valid exp) then
    ()
  else (
    lvalue_computation_doesnt_depend_on_global_variables vs pc_relation exp actor s1 s2;
    match lvalue_computation exp actor s1 with
    | ComputationProduces p -> dereference_computation_doesnt_depend_on_global_variables vs p s1.mem s2.mem
    | _ -> ()
  )

let rec if_object_value_has_all_pointers_uninitialized_then_it_doesnt_depend_on_gvars
  (vs: list var_id_t)
  (value: object_value_t)
  : Lemma (requires object_value_has_all_pointers_uninitialized value)
          (ensures  global_variables_unaddressed_in_object_value vs value)
          (decreases rank value) =
  match value with
  | ObjectValuePrimitive primitive_value -> ()
  | ObjectValueStruct fields ->
      assert (forall field. contains fields field ==> rank field << rank fields);
      introduce forall field. contains fields field ==> global_variables_unaddressed_in_object_value vs field
      with introduce _ ==> _
      with _. if_object_value_has_all_pointers_uninitialized_then_it_doesnt_depend_on_gvars vs field
  | ObjectValueArray element_td elements ->
      assert (forall element. contains elements element ==> rank element << rank elements);
      introduce forall element. contains elements element ==> global_variables_unaddressed_in_object_value vs element
      with introduce _ ==> _
      with _. if_object_value_has_all_pointers_uninitialized_then_it_doesnt_depend_on_gvars vs element
  | ObjectValueAbstract ty value -> ()

let rec object_storage_arbitrarily_initialized_correctly_doesnt_depend_on_gvars
  (vs: list var_id_t)
  (storage: object_storage_t)
  : Lemma (requires object_storage_arbitrarily_initialized_correctly storage)
          (ensures  global_variables_unaddressed_in_storage vs storage)
          (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive _ values local_versions -> ()
  | ObjectStoragePrimitive primitive_value -> ()
  | ObjectStorageStruct fields ->
      assert (forall field. contains fields field ==> rank field << rank fields);
      introduce forall field. contains fields field ==> global_variables_unaddressed_in_storage vs field
      with introduce _ ==> _
      with _. object_storage_arbitrarily_initialized_correctly_doesnt_depend_on_gvars vs field
  | ObjectStorageArray element_td elements ->
      assert (forall element. contains elements element ==> rank element << rank elements);
      introduce forall element. contains elements element ==> global_variables_unaddressed_in_storage vs element
      with introduce _ ==> _
      with _. object_storage_arbitrarily_initialized_correctly_doesnt_depend_on_gvars vs element
  | ObjectStorageAbstract ty value -> ()

let rec object_storage_zero_filled_doesnt_depend_on_gvars
  (vs: list var_id_t)
  (storage: object_storage_t)
  : Lemma (requires is_storage_zero_filled storage)
          (ensures  global_variables_unaddressed_in_storage vs storage)
          (decreases rank storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive _ values local_versions -> ()
  | ObjectStoragePrimitive primitive_value -> ()
  | ObjectStorageStruct fields ->
      assert (forall field. contains fields field ==> rank field << rank fields);
      introduce forall field. contains fields field ==> global_variables_unaddressed_in_storage vs field
      with introduce _ ==> _
      with _. object_storage_zero_filled_doesnt_depend_on_gvars vs field
  | ObjectStorageArray element_td elements ->
      assert (forall element. contains elements element ==> rank element << rank elements);
      introduce forall element. contains elements element ==> global_variables_unaddressed_in_storage vs element
      with introduce _ ==> _
      with _. object_storage_zero_filled_doesnt_depend_on_gvars vs element
  | ObjectStorageAbstract ty value -> ()

let rec object_storage_initialized_correctly_doesnt_depend_on_gvars
  (vs: list var_id_t)
  (storage: object_storage_t)
  (value: object_value_t)
  : Lemma (requires   global_variables_unaddressed_in_object_value vs value
                    /\ object_storage_initialized_correctly storage value)
          (ensures  global_variables_unaddressed_in_storage vs storage) =
  match storage with
  | ObjectStorageWeaklyConsistentPrimitive _ values local_versions -> ()
  | ObjectStoragePrimitive value -> ()
  | ObjectStorageStruct fields ->
      global_variables_unaddressed_in_storages_equivalent_to_forall vs fields;
      introduce forall field. contains fields field ==> global_variables_unaddressed_in_storage vs field
      with introduce _ ==> _
      with _. (
        let i = seq_contains_to_index fields field in
        let field_values = ObjectValueStruct?.fields value in
        let field_value = index field_values i in
        assert (rank field << rank fields);
        object_storage_initialized_correctly_doesnt_depend_on_gvars vs field field_value
      )
  | ObjectStorageArray element_td elements ->
      global_variables_unaddressed_in_storages_equivalent_to_forall vs elements;
      introduce forall element. contains elements element ==> global_variables_unaddressed_in_storage vs element
      with introduce _ ==> _
      with _. (
        let i = seq_contains_to_index elements element in
        let element_values = ObjectValueArray?.elements value in
        let element_value = index element_values i in
        assert (rank element << rank elements);
        object_storage_initialized_correctly_doesnt_depend_on_gvars vs element element_value
      )
  | ObjectStorageAbstract ty value -> ()

#pop-options
#push-options "--z3rlimit 40"
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Util.Nth.fst.checked Util.List.fst.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Value.fst.checked Strategies.GlobalVars.Unaddressed.fst.checked Strategies.GlobalVars.Pointer.fst.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.Threads.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.Util.fst

    vs: Prims.list Armada.Base.var_id_t ->
    actor: Armada.Base.tid_t ->
    writer_pc1: Armada.Base.pc_t ->
    writer_pc2: Armada.Base.pc_t ->
    writer_expression_number1: Prims.nat ->
    writer_expression_number2: Prims.nat ->
    method_id: Armada.Base.method_id_t ->
    frame_uniq: Armada.Base.root_id_uniquifier_t ->
    initializer: Armada.Init.initializer_t ->
    s1: Armada.State.t ->
    s2: Armada.State.t ->
    thread1: Armada.Thread.t ->
    thread2: Armada.Thread.t ->
    local_variables1': Prims.list Armada.Base.var_id_t ->
    local_variables2': Prims.list Armada.Base.var_id_t ->
    top1': Armada.Thread.stack_frame_t ->
    top2': Armada.Thread.stack_frame_t ->
    thread1': Armada.Thread.t ->
    thread2': Armada.Thread.t ->
    threads1': Armada.Threads.t ->
    threads2': Armada.Threads.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s1 /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s2 /\
        Strategies.GlobalVars.positions_in_write_buffers_match_except_global_variables vs
          (Mkt?.threads s1)
          (Mkt?.threads s2) /\ thread1 == Mkt?.threads s1 actor /\ thread2 == Mkt?.threads s2 actor /\
        local_variables1' ==
        Mkinitializer_t?.var_id initializer :: Mkstack_frame_t?.local_variables (Mkt?.top thread1) /\
        local_variables2' ==
        Mkinitializer_t?.var_id initializer :: Mkstack_frame_t?.local_variables (Mkt?.top thread2) /\
        top1' ==
        (let _ = Mkt?.top thread1 in
          Armada.Thread.Mkstack_frame_t (Mkstack_frame_t?.method_id _)
            (Mkstack_frame_t?.frame_uniq _)
            local_variables1') /\
        top2' ==
        (let _ = Mkt?.top thread2 in
          Armada.Thread.Mkstack_frame_t (Mkstack_frame_t?.method_id _)
            (Mkstack_frame_t?.frame_uniq _)
            local_variables2') /\
        thread1' ==
        Armada.Thread.Mkt (Mkt?.status thread1)
          (Mkt?.pc thread1)
          top1'
          (Mkt?.stack thread1)
          (Mkt?.write_buffer thread1)
          (Mkt?.position_in_other_write_buffers thread1) /\
        thread2' ==
        Armada.Thread.Mkt (Mkt?.status thread2)
          (Mkt?.pc thread2)
          top2'
          (Mkt?.stack thread2)
          (Mkt?.write_buffer thread2)
          (Mkt?.position_in_other_write_buffers thread2) /\
        threads1' == Spec.Map.upd (Mkt?.threads s1) actor thread1' /\
        threads2' == Spec.Map.upd (Mkt?.threads s2) actor thread2' /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads1' /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads2')
      (ensures
        Strategies.GlobalVars.positions_in_write_buffers_match_except_global_variables vs
          threads1'
          threads2')
Prims.list Armada.Base.var_id_t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Armada.Base.method_id_t Armada.Base.root_id_uniquifier_t Armada.Init.initializer_t Armada.State.t Armada.Thread.t Armada.Thread.stack_frame_t Armada.Threads.t Prims._assert Strategies.GlobalVars.positions_in_write_buffers_match_except_global_variables Prims.unit FStar.Classical.Sugar.forall_intro Prims.l_Forall Strategies.GlobalVars.write_buffers_match_except_global_variables Strategies.GlobalVars.unread_write_buffer Prims.eq2 FStar.Sequence.Base.seq Armada.Thread.write_message_t Armada.State.__proj__Mkt__item__threads Prims.b2t Strategies.ArmadaInvariant.PositionsValid.sender_receiver_trigger Prims.squash Prims.l_and Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Prims.Cons Armada.Init.__proj__Mkinitializer_t__item__var_id Armada.Thread.__proj__Mkstack_frame_t__item__local_variables Armada.Thread.__proj__Mkt__item__top Armada.Thread.Mkstack_frame_t Armada.Thread.__proj__Mkstack_frame_t__item__method_id Armada.Thread.__proj__Mkstack_frame_t__item__frame_uniq Armada.Thread.Mkt Armada.Thread.__proj__Mkt__item__status Armada.Thread.__proj__Mkt__item__pc Armada.Thread.__proj__Mkt__item__stack Armada.Thread.__proj__Mkt__item__write_buffer Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers Spec.Map.t Spec.Map.upd Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads Prims.Nil FStar.Pervasives.pattern
let push_stack_variable_doesnt_depend_on_gvars_helper
      (vs: list var_id_t)
      (actor: tid_t)
      (writer_pc1 writer_pc2: pc_t)
      (writer_expression_number1 writer_expression_number2: nat)
      (method_id: method_id_t)
      (frame_uniq: root_id_uniquifier_t)
      (initializer: initializer_t)
      (s1 s2: Armada.State.t)
      (thread1 thread2: Armada.Thread.t)
      (local_variables1' local_variables2': list var_id_t)
      (top1' top2': stack_frame_t)
      (thread1' thread2': Armada.Thread.t)
      (threads1' threads2': Armada.Threads.t)
    : Lemma
      (requires
        positions_valid_in_state s1 /\ positions_valid_in_state s2 /\
        positions_in_write_buffers_match_except_global_variables vs s1.threads s2.threads /\
        thread1 == s1.threads actor /\ thread2 == s2.threads actor /\
        local_variables1' == initializer.var_id :: thread1.top.local_variables /\
        local_variables2' == initializer.var_id :: thread2.top.local_variables /\
        top1' == { thread1.top with local_variables = local_variables1' } /\
        top2' == { thread2.top with local_variables = local_variables2' } /\
        thread1' == { thread1 with top = top1' } /\ thread2' == { thread2 with top = top2' } /\
        threads1' == Spec.Map.upd s1.threads actor thread1' /\
        threads2' == Spec.Map.upd s2.threads actor thread2' /\ positions_valid_in_threads threads1' /\
        positions_valid_in_threads threads2')
      (ensures positions_in_write_buffers_match_except_global_variables vs threads1' threads2') =
  
introduce forall sender_tid receiver_tid . write_buffers_match_except_global_variables vs
  (unread_write_buffer threads1' sender_tid receiver_tid)
  (unread_write_buffer threads2' sender_tid receiver_tid)
with (assert (sender_receiver_trigger sender_tid receiver_tid);
  assert (write_buffers_match_except_global_variables vs
        (unread_write_buffer s1.threads sender_tid receiver_tid)
        (unread_write_buffer s2.threads sender_tid receiver_tid));
  assert (unread_write_buffer threads1' sender_tid receiver_tid ==
      unread_write_buffer s1.threads sender_tid receiver_tid);
  assert (unread_write_buffer threads2' sender_tid receiver_tid ==
      unread_write_buffer s2.threads sender_tid receiver_tid));
assert (positions_in_write_buffers_match_except_global_variables vs threads1' threads2')