val adding_write_message_among_gvars_s2_only_maintains_positions_in_write_buffers_match_and_positions_valid_for_receiver
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (actor: tid_t)
      (write_message: write_message_t)
      (threads1 threads2: Armada.Threads.t)
      (receiver_tid: tid_t)
    : Lemma
      (requires
        positions_valid_in_threads threads1 /\ positions_valid_in_threads threads2 /\
        threads_match_except_global_variables vs pc_relation threads1 threads2 /\
        pointer_among_global_variables vs write_message.location /\
        positions_valid_in_threads threads1 /\ positions_valid_in_threads threads2)
      (ensures
        (let threads2' = append_to_thread_write_buffer threads2 actor write_message in
          positions_valid_in_threads threads2' /\
          write_buffers_match_except_global_variables vs
            (unread_write_buffer threads1 actor receiver_tid)
            (unread_write_buffer threads2' actor receiver_tid)))
val adding_write_message_among_gvars_s2_only_maintains_positions_in_write_buffers_match_and_positions_valid_for_receiver
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (actor: tid_t)
      (write_message: write_message_t)
      (threads1 threads2: Armada.Threads.t)
      (receiver_tid: tid_t)
    : Lemma
      (requires
        positions_valid_in_threads threads1 /\ positions_valid_in_threads threads2 /\
        threads_match_except_global_variables vs pc_relation threads1 threads2 /\
        pointer_among_global_variables vs write_message.location /\
        positions_valid_in_threads threads1 /\ positions_valid_in_threads threads2)
      (ensures
        (let threads2' = append_to_thread_write_buffer threads2 actor write_message in
          positions_valid_in_threads threads2' /\
          write_buffers_match_except_global_variables vs
            (unread_write_buffer threads1 actor receiver_tid)
            (unread_write_buffer threads2' actor receiver_tid)))
let adding_write_message_among_gvars_s2_only_maintains_positions_in_write_buffers_match_and_positions_valid_for_receiver
  (vs: list var_id_t)
  (pc_relation: pc_relation_t)
  (actor: tid_t)
  (write_message: write_message_t)
  (threads1: Armada.Threads.t)
  (threads2: Armada.Threads.t)
  (receiver_tid: tid_t)
  : Lemma (requires   positions_valid_in_threads threads1
                    /\ positions_valid_in_threads threads2
                    /\ threads_match_except_global_variables vs pc_relation threads1 threads2
                    /\ pointer_among_global_variables vs write_message.location
                    /\ positions_valid_in_threads threads1
                    /\ positions_valid_in_threads threads2)
          (ensures  (let threads2' = append_to_thread_write_buffer threads2 actor write_message in
                       positions_valid_in_threads threads2'
                     /\ write_buffers_match_except_global_variables vs
                         (unread_write_buffer threads1 actor receiver_tid)
                         (unread_write_buffer threads2' actor receiver_tid))) =
  assert (sender_receiver_trigger actor receiver_tid);
  append_among_gvars_s2_only_preserves_write_buffers_match_except_global_variables vs
    (unread_write_buffer threads1 actor receiver_tid)
    (unread_write_buffer threads2 actor receiver_tid)
    write_message;
  unread_write_buffer_commutes_with_append threads2 actor receiver_tid write_message
module Strategies.GlobalVars.VarIntro

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.Util
open Strategies.PCRelation
open Util.Seq
open Util.Trigger

let rec pointer_among_gvars_implies_gvars_addressed
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  : Lemma (requires pointer_among_global_variables vs p)
          (ensures  not (global_variables_unaddressed_in_pointer vs p)) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr _ -> pointer_among_gvars_implies_gvars_addressed vs struct_ptr
  | PointerIndex array_ptr _ -> pointer_among_gvars_implies_gvars_addressed vs array_ptr
  
let append_among_gvars_s2_only_preserves_write_buffer_lists_match_except_global_variables
  (vs: list var_id_t)
  (write_buffer1: list write_message_t)
  (write_buffer2: list write_message_t)
  (write_message: write_message_t)
  : Lemma (requires   write_buffers_match (remove_global_variables_from_write_buffer vs write_buffer1)
                        (remove_global_variables_from_write_buffer vs write_buffer2)
                    /\ pointer_among_global_variables vs write_message.location)
          (ensures  (let write_buffer2' = FStar.List.Tot.append write_buffer2 [write_message] in
                     write_buffers_match (remove_global_variables_from_write_buffer vs write_buffer1)
                       (remove_global_variables_from_write_buffer vs write_buffer2'))) =
  pointer_among_gvars_implies_gvars_addressed vs write_message.location;
  append_effect_on_remove_global_variables_from_write_buffer_list vs write_buffer2 write_message

let append_among_gvars_s2_only_preserves_write_buffers_match_except_global_variables
  (vs: list var_id_t)
  (write_buffer1: seq write_message_t)
  (write_buffer2: seq write_message_t)
  (write_message: write_message_t)
  : Lemma (requires   write_buffers_match_except_global_variables vs write_buffer1 write_buffer2
                    /\ pointer_among_global_variables vs write_message.location)
          (ensures  (let write_buffer2' = build write_buffer2 write_message in
                     write_buffers_match_except_global_variables vs write_buffer1 write_buffer2'))
          (decreases length write_buffer1 + length write_buffer2) =
  build_equivalent_to_append write_buffer2 write_message;
  append_among_gvars_s2_only_preserves_write_buffer_lists_match_except_global_variables vs (seq_to_list write_buffer1)
    (seq_to_list write_buffer2) write_message
/
Util.Trigger.fst.checked Util.Seq.fsti.checked Strategies.PCRelation.fst.checked Strategies.GlobalVars.Util.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.List.Tot.fst.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.VarIntro.fst

    vs: Prims.list Armada.Base.var_id_t ->
    pc_relation: Strategies.PCRelation.pc_relation_t ->
    actor: Armada.Base.tid_t ->
    write_message: Armada.Thread.write_message_t ->
    threads1: Armada.Threads.t ->
    threads2: Armada.Threads.t ->
    receiver_tid: Armada.Base.tid_t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads1 /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads2 /\
        Strategies.GlobalVars.threads_match_except_global_variables vs pc_relation threads1 threads2 /\
        Strategies.GlobalVars.VarIntro.pointer_among_global_variables vs
          (Mkwrite_message_t?.location write_message) /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads1 /\
        Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads2)
      (ensures
        (let threads2' =
            Armada.Expression.append_to_thread_write_buffer threads2 actor write_message
          in
          Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads threads2' /\
          Strategies.GlobalVars.write_buffers_match_except_global_variables vs
            (Strategies.GlobalVars.unread_write_buffer threads1 actor receiver_tid)
            (Strategies.GlobalVars.unread_write_buffer threads2' actor receiver_tid)))
Prims.list Armada.Base.var_id_t Strategies.PCRelation.pc_relation_t Armada.Base.tid_t Armada.Thread.write_message_t Armada.Threads.t Strategies.GlobalVars.Pointer.unread_write_buffer_commutes_with_append Prims.unit Strategies.GlobalVars.VarIntro.append_among_gvars_s2_only_preserves_write_buffers_match_except_global_variables Strategies.GlobalVars.unread_write_buffer Prims._assert Prims.b2t Strategies.ArmadaInvariant.PositionsValid.sender_receiver_trigger Prims.l_and Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_threads Strategies.GlobalVars.threads_match_except_global_variables Strategies.GlobalVars.VarIntro.pointer_among_global_variables Armada.Thread.__proj__Mkwrite_message_t__item__location Prims.squash Strategies.GlobalVars.write_buffers_match_except_global_variables Armada.Expression.append_to_thread_write_buffer Prims.Nil FStar.Pervasives.pattern
let adding_write_message_among_gvars_s2_only_maintains_positions_in_write_buffers_match_and_positions_valid_for_receiver
      (vs: list var_id_t)
      (pc_relation: pc_relation_t)
      (actor: tid_t)
      (write_message: write_message_t)
      (threads1 threads2: Armada.Threads.t)
      (receiver_tid: tid_t)
    : Lemma
      (requires
        positions_valid_in_threads threads1 /\ positions_valid_in_threads threads2 /\
        threads_match_except_global_variables vs pc_relation threads1 threads2 /\
        pointer_among_global_variables vs write_message.location /\
        positions_valid_in_threads threads1 /\ positions_valid_in_threads threads2)
      (ensures
        (let threads2' = append_to_thread_write_buffer threads2 actor write_message in
          positions_valid_in_threads threads2' /\
          write_buffers_match_except_global_variables vs
            (unread_write_buffer threads1 actor receiver_tid)
            (unread_write_buffer threads2' actor receiver_tid))) =
  
assert (sender_receiver_trigger actor receiver_tid);
append_among_gvars_s2_only_preserves_write_buffers_match_except_global_variables vs
  (unread_write_buffer threads1 actor receiver_tid)
  (unread_write_buffer threads2 actor receiver_tid)
  write_message;
unread_write_buffer_commutes_with_append threads2 actor receiver_tid write_message