val update_pointer_directly_among_gvars_s2_only_maintains_states_match
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (new_storage: valid_object_storage_t)
      (mem1 mem2: Armada.Memory.t)
    : Lemma
      (requires
        pointer_among_global_variables vs p /\
        global_variables_unaddressed_in_storage vs new_storage /\
        global_variables_unaddressed_in_memory vs mem1 /\
        global_variables_unaddressed_in_memory vs mem2 /\
        memories_match_except_global_variables vs mem1 mem2 /\ roots_match mem1 /\ roots_match mem2 /\
        (ComputationProduces? (update_pointer_directly p new_storage mem2)))
      (ensures
        (match update_pointer_directly p new_storage mem2 with
          | ComputationProduces mem2' ->
            global_variables_unaddressed_in_memory vs mem2' /\
            memories_match_except_global_variables vs mem1 mem2' /\ roots_match mem2'))
val update_pointer_directly_among_gvars_s2_only_maintains_states_match
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (new_storage: valid_object_storage_t)
      (mem1 mem2: Armada.Memory.t)
    : Lemma
      (requires
        pointer_among_global_variables vs p /\
        global_variables_unaddressed_in_storage vs new_storage /\
        global_variables_unaddressed_in_memory vs mem1 /\
        global_variables_unaddressed_in_memory vs mem2 /\
        memories_match_except_global_variables vs mem1 mem2 /\ roots_match mem1 /\ roots_match mem2 /\
        (ComputationProduces? (update_pointer_directly p new_storage mem2)))
      (ensures
        (match update_pointer_directly p new_storage mem2 with
          | ComputationProduces mem2' ->
            global_variables_unaddressed_in_memory vs mem2' /\
            memories_match_except_global_variables vs mem1 mem2' /\ roots_match mem2'))
let rec update_pointer_directly_among_gvars_s2_only_maintains_states_match
  (vs: list var_id_t)
  (p: Armada.Pointer.t)
  (new_storage: valid_object_storage_t)
  (mem1: Armada.Memory.t)
  (mem2: Armada.Memory.t)
  : Lemma (requires   pointer_among_global_variables vs p
                    /\ global_variables_unaddressed_in_storage vs new_storage
                    /\ global_variables_unaddressed_in_memory vs mem1
                    /\ global_variables_unaddressed_in_memory vs mem2
                    /\ memories_match_except_global_variables vs mem1 mem2
                    /\ roots_match mem1
                    /\ roots_match mem2
                    /\ (ComputationProduces? (update_pointer_directly p new_storage mem2)))
          (ensures  (match update_pointer_directly p new_storage mem2 with
                     | ComputationProduces mem2' ->
                           global_variables_unaddressed_in_memory vs mem2'
                         /\ memories_match_except_global_variables vs mem1 mem2'
                         /\ roots_match mem2')) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr field_id ->
      dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs struct_ptr mem2;
      (match dereference_computation struct_ptr mem2 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_among_gvars_s2_only_maintains_states_match vs struct_ptr
                    new_parent mem1 mem2
                )
            | _ -> ())
      | _ -> ())
  | PointerIndex array_ptr idx ->
      dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs array_ptr mem2;
      (match dereference_computation array_ptr mem2 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_among_gvars_s2_only_maintains_states_match vs array_ptr
                    new_parent mem1 mem2
                )
            | _ -> ())
      | _ -> ())
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

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

let adding_write_message_among_gvars_s2_only_maintains_positions_match_and_positions_valid_for_tid_pair
  (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)
  (sender_tid: tid_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 sender_tid receiver_tid)
                         (unread_write_buffer threads2' sender_tid receiver_tid)))) =
  if sender_tid <> actor then
    assert (sender_receiver_trigger sender_tid receiver_tid)
  else
    adding_write_message_among_gvars_s2_only_maintains_positions_in_write_buffers_match_and_positions_valid_for_receiver
      vs pc_relation actor write_message threads1 threads2 receiver_tid

let adding_write_message_among_gvars_s2_only_maintains_positions_in_write_buffers_match_and_positions_valid
  (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)
  : 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'
                     /\ positions_in_write_buffers_match_except_global_variables vs threads1 threads2')) =
  let threads2' = append_to_thread_write_buffer threads2 actor write_message in
  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 adding_write_message_among_gvars_s2_only_maintains_positions_match_and_positions_valid_for_tid_pair
         vs pc_relation actor write_message threads1 threads2 sender_tid receiver_tid

#push-options "--z3rlimit 30"

let rec lvalue_computation_among_gvars_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   lvalue_expression_among_global_variables vs exp
                    /\ 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)
          (ensures  lvalue_computation exp actor s1 == lvalue_computation exp actor s2
                    /\ (match lvalue_computation exp actor s1 with
                       | ComputationProduces p -> pointer_among_global_variables vs p
                       | _ -> True)) =
  match exp with
  | ExpressionGlobalVariable _ var_id -> ()
  | ExpressionFieldOf td obj field_id ->
      lvalue_computation_among_gvars_doesnt_depend_on_gvars vs pc_relation obj actor s1 s2
  | _ -> ()

#pop-options
#push-options "--z3rlimit 30"
/
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 ->
    p: Armada.Pointer.t ->
    new_storage: Armada.Memory.valid_object_storage_t ->
    mem1: Armada.Memory.t ->
    mem2: Armada.Memory.t
  -> FStar.Pervasives.Lemma
      (requires
        Strategies.GlobalVars.VarIntro.pointer_among_global_variables vs p /\
        Strategies.GlobalVars.global_variables_unaddressed_in_storage vs new_storage /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem1 /\
        Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem2 /\
        Strategies.GlobalVars.memories_match_except_global_variables vs mem1 mem2 /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem1 /\
        Strategies.ArmadaInvariant.RootsMatch.roots_match mem2 /\
        ComputationProduces? (Armada.Memory.update_pointer_directly p new_storage mem2))
      (ensures
        ((let Armada.Computation.ComputationProduces #_ mem2' =
              Armada.Memory.update_pointer_directly p new_storage mem2
            in
            Strategies.GlobalVars.global_variables_unaddressed_in_memory vs mem2' /\
            Strategies.GlobalVars.memories_match_except_global_variables vs mem1 mem2' /\
            Strategies.ArmadaInvariant.RootsMatch.roots_match mem2')
          <:
          Type0))
Prims.list Armada.Base.var_id_t Armada.Pointer.t Armada.Memory.valid_object_storage_t Armada.Memory.t Armada.Base.root_id_t Prims.nat Armada.Memory.dereference_computation FStar.Sequence.Base.seq Armada.Memory.object_storage_t Prims.op_BarBar Prims.op_GreaterThanOrEqual FStar.Sequence.Base.length Spec.Ubool.neqb Armada.Type.object_td_t Armada.Memory.object_storage_to_td FStar.Sequence.Base.index Prims.bool Strategies.GlobalVars.VarIntro.update_pointer_directly_among_gvars_s2_only_maintains_states_match Armada.Memory.update_storage_child Prims.unit Armada.Computation.conditional_computation_t Strategies.GlobalVars.Unaddressed.dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed Prims.op_LessThan Prims.l_and Prims.b2t Strategies.GlobalVars.VarIntro.pointer_among_global_variables Strategies.GlobalVars.global_variables_unaddressed_in_storage Strategies.GlobalVars.global_variables_unaddressed_in_memory Strategies.GlobalVars.memories_match_except_global_variables Strategies.ArmadaInvariant.RootsMatch.roots_match Armada.Computation.uu___is_ComputationProduces Armada.Memory.update_pointer_directly Prims.squash Prims.Nil FStar.Pervasives.pattern
let rec update_pointer_directly_among_gvars_s2_only_maintains_states_match
      (vs: list var_id_t)
      (p: Armada.Pointer.t)
      (new_storage: valid_object_storage_t)
      (mem1 mem2: Armada.Memory.t)
    : Lemma
      (requires
        pointer_among_global_variables vs p /\
        global_variables_unaddressed_in_storage vs new_storage /\
        global_variables_unaddressed_in_memory vs mem1 /\
        global_variables_unaddressed_in_memory vs mem2 /\
        memories_match_except_global_variables vs mem1 mem2 /\ roots_match mem1 /\ roots_match mem2 /\
        (ComputationProduces? (update_pointer_directly p new_storage mem2)))
      (ensures
        (match update_pointer_directly p new_storage mem2 with
          | ComputationProduces mem2' ->
            global_variables_unaddressed_in_memory vs mem2' /\
            memories_match_except_global_variables vs mem1 mem2' /\ roots_match mem2')) =
  
match p with
| PointerUninitialized -> ()
| PointerNull -> ()
| PointerRoot root_id -> ()
| PointerField struct_ptr field_id ->
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs
    struct_ptr
    mem2;
  (match dereference_computation struct_ptr mem2 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_among_gvars_s2_only_maintains_states_match vs
                struct_ptr
                new_parent
                mem1
                mem2)
        | _ -> ())
    | _ -> ())
| PointerIndex array_ptr idx ->
  dereference_computation_when_gvars_unaddressed_produces_storage_with_gvars_unaddressed vs
    array_ptr
    mem2;
  (match dereference_computation array_ptr mem2 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_among_gvars_s2_only_maintains_states_match vs
                array_ptr
                new_parent
                mem1
                mem2)
        | _ -> ())
    | _ -> ())