val 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)
val 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)
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)))
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)
  )
/
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 -> s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state s)
      (ensures
        Strategies.GlobalVars.states_match_except_global_variables vs
          Strategies.PCRelation.equality_pc_relation
          s
          s)
Prims.list Armada.Base.var_id_t Armada.State.t FStar.Classical.Sugar.forall_intro Armada.Base.tid_t Prims.l_Forall Prims.l_imp Prims.b2t Strategies.ArmadaInvariant.PositionsValid.sender_receiver_trigger Strategies.GlobalVars.write_buffers_match_except_global_variables Strategies.GlobalVars.unread_write_buffer Armada.State.__proj__Mkt__item__threads FStar.Classical.Sugar.implies_intro Prims.squash Strategies.PCRelation.equality_pc_relation_implies_write_buffer_matches_itself Strategies.GlobalVars.remove_global_variables_from_write_buffer Util.Seq.seq_to_list Armada.Thread.write_message_t Prims.unit Prims._assert Strategies.PCRelation.threads_match_except_write_buffers_per_pc_relation Strategies.PCRelation.equality_pc_relation Strategies.PCRelation.stacks_match_per_pc_relation Armada.Thread.__proj__Mkt__item__stack Strategies.PCRelation.equality_pc_relation_implies_stack_matches_itself Strategies.ArmadaInvariant.PositionsValid.positions_valid_in_state Strategies.GlobalVars.states_match_except_global_variables Prims.Nil FStar.Pervasives.pattern
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)))