val propagate_write_message_maintains_states_match
      (vs: list var_id_t)
      (write_message1 write_message2: write_message_t)
      (receiver_tid: tid_t)
      (mem1 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))
val propagate_write_message_maintains_states_match
      (vs: list var_id_t)
      (write_message1 write_message2: write_message_t)
      (receiver_tid: tid_t)
      (mem1 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 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
       | _ -> ()
     )
  | _ -> ()
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 -> ()
       | _, _ -> ())
  | _, _ -> ()
/
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 ->
    write_message1: Armada.Thread.write_message_t ->
    write_message2: Armada.Thread.write_message_t ->
    receiver_tid: 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_memory vs mem1 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem2 /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem1 /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem2 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_write_message vs write_message1 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_write_message vs write_message2 /\
        Strategies.PCRelation.write_messages_match write_message1 write_message2)
      (ensures
        ((match
              Armada.Memory.propagate_write_message write_message1 receiver_tid mem1,
              Armada.Memory.propagate_write_message write_message2 receiver_tid mem2
            with
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (Armada.Computation.ComputationProduces #_ mem1')
              (Armada.Computation.ComputationProduces #_ mem2') ->
              Strategies.GlobalVars.memories_match_except_global_variables vs mem1' mem2' /\
              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'
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (Armada.Computation.ComputationImpossible #_)
              (Armada.Computation.ComputationImpossible #_) ->
              Prims.l_True
            | FStar.Pervasives.Native.Mktuple2
              #_
              #_
              (Armada.Computation.ComputationUndefined #_)
              (Armada.Computation.ComputationUndefined #_) ->
              Prims.l_True
            | _ -> Prims.l_False)
          <:
          Type0))
Prims.list Armada.Base.var_id_t Armada.Thread.write_message_t Armada.Base.tid_t Armada.Memory.t Armada.Memory.dereference_computation Armada.Memory.valid_object_storage_t Armada.Type.primitive_td_t FStar.Sequence.Base.seq Armada.Type.primitive_box_t Spec.Map.t Prims.nat Prims.op_BarBar Prims.op_disEquality Armada.Thread.__proj__Mkwrite_message_t__item__primitive_td Prims.op_GreaterThanOrEqual Armada.Thread.__proj__Mkwrite_message_t__item__version FStar.Sequence.Base.length Prims.bool Prims.op_Negation Armada.Memory.object_storage_valid Strategies.GlobalVars.Pointer.update_pointer_directly_with_gvars_unaddressed_maintains_states_match Prims.unit Armada.Memory.object_storage_t Armada.Memory.ObjectStorageWeaklyConsistentPrimitive Spec.Map.upd Armada.Computation.conditional_computation_t Strategies.GlobalVars.Value.dereference_computation_doesnt_depend_on_global_variables Armada.Pointer.t Armada.Thread.__proj__Mkwrite_message_t__item__location Prims.l_and Strategies.GlobalVars.memories_match_except_global_variables Strategies.GlobalVars.global_variables_unaddressed_in_memory Strategies.ArmadaInvariant.RootsMatch.roots_match Prims.b2t Strategies.GlobalVars.global_variables_unaddressed_in_write_message Strategies.PCRelation.write_messages_match Prims.squash FStar.Pervasives.Native.Mktuple2 Armada.Memory.propagate_write_message Prims.l_True FStar.Pervasives.Native.tuple2 Prims.l_False Prims.Nil FStar.Pervasives.pattern
let propagate_write_message_maintains_states_match
      (vs: list var_id_t)
      (write_message1 write_message2: write_message_t)
      (receiver_tid: tid_t)
      (mem1 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
    | _ -> ())
| _ -> ()