val external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars
      (v: var_id_t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (reads_clauses: list (var_id_t * expression_t))
      (s: Armada.State.t)
    : Lemma (requires variable_among_gvars s.mem v)
      (ensures
        (match
            external_method_take_snapshot_of_reads_clauses_computation actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              reads_clauses
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> variable_among_gvars s'.mem v))
      (decreases reads_clauses)
val external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars
      (v: var_id_t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (reads_clauses: list (var_id_t * expression_t))
      (s: Armada.State.t)
    : Lemma (requires variable_among_gvars s.mem v)
      (ensures
        (match
            external_method_take_snapshot_of_reads_clauses_computation actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              reads_clauses
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> variable_among_gvars s'.mem v))
      (decreases reads_clauses)
let rec external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (reads_clauses: list (var_id_t * expression_t))
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match external_method_take_snapshot_of_reads_clauses_computation actor writer_pc
                             writer_expression_number bypassing_write_buffer reads_clauses s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v))
          (decreases reads_clauses) =
  match reads_clauses with
  | [] -> ()
  | (first_var_id, first_reads_expression) :: remaining_reads_clauses ->
      (match rvalue_computation first_reads_expression actor s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces first_value ->
           let td = expression_to_td first_reads_expression in
           let local_var = ExpressionLocalVariable td first_var_id in
           update_expression_maintains_variable_among_gvars v local_var actor writer_pc writer_expression_number
             bypassing_write_buffer first_value s;
           (match update_expression local_var actor writer_pc writer_expression_number bypassing_write_buffer
                    first_value s with
            | ComputationImpossible | ComputationUndefined -> ()
            | ComputationProduces s' ->
                external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars v
                  actor writer_pc (writer_expression_number + 1) bypassing_write_buffer remaining_reads_clauses s'))
  | _ -> ()
module Strategies.GlobalVars.Permanent

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.Program
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Transition
open Armada.Type
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Map
open Spec.Ubool
open Strategies.ArmadaStatement
open Util.List
open Util.Tactics

let variable_among_gvars (mem: Armada.Memory.t) (v: var_id_t) : GTot bool =
  let root_id = RootIdGlobal v in
  let root = mem root_id in
  RootGlobal? root

let all_variables_among_gvars (mem: Armada.Memory.t) (vs: list var_id_t) : GTot bool =
  for_all_ghost (variable_among_gvars mem) vs

let rec update_pointer_directly_maintains_variable_among_gvars
  (v: var_id_t)
  (p: Armada.Pointer.t)
  (new_storage: valid_object_storage_t)
  (mem: Armada.Memory.t)
  : Lemma (requires variable_among_gvars mem v)
          (ensures  (match update_pointer_directly p new_storage mem with
                     | ComputationProduces mem' -> variable_among_gvars mem' v
                     | _ -> True)) =
  match update_pointer_directly p new_storage mem with
  | ComputationImpossible | ComputationUndefined -> ()
  | ComputationProduces mem' ->
      (match p with
       | PointerField struct_ptr field_id ->
           let parent = ComputationProduces?.result (dereference_computation struct_ptr mem) in
           (match parent with
            | ObjectStorageStruct fields ->
                let new_parent = update_storage_child parent field_id new_storage in
                update_pointer_directly_maintains_variable_among_gvars v struct_ptr new_parent mem)
       | PointerIndex array_ptr idx ->
           let parent = ComputationProduces?.result (dereference_computation array_ptr mem) in
           (match parent with
            | ObjectStorageArray element_td elements ->
                let new_parent = update_storage_child parent idx new_storage in
                update_pointer_directly_maintains_variable_among_gvars v array_ptr new_parent mem)
       | PointerRoot root_id -> ()
       | _ -> ())

#push-options "--z3rlimit 10"

let update_pointer_maintains_variable_among_gvars
  (v: var_id_t)
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (mem: Armada.Memory.t)
  : Lemma (requires variable_among_gvars mem v)
          (ensures  (match update_pointer p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value mem with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces (optional_write_message, mem') -> variable_among_gvars mem' v)) =
  match p with
  | PointerUninitialized -> ()
  | PointerNull -> ()
  | PointerRoot root_id -> ()
  | PointerField struct_ptr field_id ->
      (match dereference_computation struct_ptr mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageStruct fields ->
                if field_id >= length fields then
                  ()
                else
                  let field = index fields field_id in
                  if   not (object_storage_valid field)
                     || neqb (object_storage_to_td field) (object_value_to_td new_value) then
                    ()
                  else
                    (match update_storage p actor writer_pc writer_expression_number
                             bypassing_write_buffer field new_value with
                     | ComputationImpossible | ComputationUndefined -> ()
                     | ComputationProduces (write_message, new_field) ->
                         if (not (can_update_storage_child parent field_id new_field)) then
                           ()
                         else
                           let new_parent = update_storage_child parent field_id new_field in
                           update_pointer_directly_maintains_variable_among_gvars v struct_ptr new_parent mem)
            | _ -> ()))
  | PointerIndex array_ptr idx ->
      (match dereference_computation array_ptr mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces parent ->
           (match parent with
            | ObjectStorageArray element_td elements ->
                if idx < 0 || idx >= length elements then
                  ()
                else
                  let element = index elements idx in
                  if not (object_storage_valid element) then
                    ()
                  else
                    (match update_storage p actor writer_pc writer_expression_number
                             bypassing_write_buffer element new_value with
                     | ComputationImpossible | ComputationUndefined -> ()
                     | ComputationProduces (write_message, new_element) ->
                         if not (can_update_storage_child parent idx new_element) then
                           ()
                         else
                           let new_parent = update_storage_child parent idx new_element in
                           update_pointer_directly_maintains_variable_among_gvars v array_ptr new_parent mem)
            | _ -> ()))

#pop-options

let update_pointed_to_value_maintains_variable_among_gvars
  (v: var_id_t)
  (p: Armada.Pointer.t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match update_pointed_to_value p actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  update_pointer_maintains_variable_among_gvars v p actor writer_pc writer_expression_number bypassing_write_buffer
    new_value s.mem

let update_expression_maintains_variable_among_gvars
  (v: var_id_t)
  (exp: expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_value: object_value_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
                             new_value s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  let s' = update_expression exp actor writer_pc writer_expression_number bypassing_write_buffer
             new_value s in
  if   not (expression_valid exp)
     || not (object_value_valid new_value)
     || neqb (object_value_to_td new_value) (expression_to_td exp) then
    ()
  else (
    match lvalue_computation exp actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces p ->
        update_pointed_to_value_maintains_variable_among_gvars v p actor writer_pc writer_expression_number
          bypassing_write_buffer new_value s
  )

let rec update_expressions_maintains_variable_among_gvars
  (v: var_id_t)
  (exps: list expression_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (bypassing_write_buffer: bool)
  (new_values: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match update_expressions exps actor writer_pc writer_expression_number bypassing_write_buffer
                             new_values s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v))
          (decreases exps) =
  match exps, new_values with
  | [], [] -> ()
  | first_exp :: remaining_exps, first_new_value :: remaining_new_values ->
      update_expression_maintains_variable_among_gvars v first_exp actor writer_pc writer_expression_number
        bypassing_write_buffer first_new_value s;
      (match update_expression first_exp actor writer_pc writer_expression_number
               bypassing_write_buffer first_new_value s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           update_expressions_maintains_variable_among_gvars v remaining_exps actor writer_pc
             (writer_expression_number + 1) bypassing_write_buffer remaining_new_values s')
  | _ -> ()

let push_stack_variable_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializer: initializer_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq
                             initializer s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  let root_id = RootIdStack actor method_id frame_uniq initializer.var_id in
  let root = s.mem root_id in
  if not (stack_variable_ready_for_push root initializer) then
    ()
  else
    let thread = s.threads actor in
    let var_id = initializer.var_id in
    if list_contains var_id thread.top.local_variables then
      ()
    else
      let local_variables' = var_id :: thread.top.local_variables in
      let top' = { thread.top with local_variables = local_variables' } in
      let thread' = { thread with top = top' } in
      let threads' = Spec.Map.upd s.threads actor thread' in
      let root' = RootStackVariable true false (RootStackVariable?.storage root) in
      let mem' = upd s.mem root_id root' in
      let s' = { s with mem = mem'; threads = threads' } in
      (match initializer.iv with
       | InitializerArbitrary td -> ()
       | InitializerSpecific value ->
           let td = (object_value_to_td value) in
           update_expression_maintains_variable_among_gvars v (ExpressionLocalVariable td var_id) actor writer_pc
             writer_expression_number false value s')

let rec push_stack_variables_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (initializers: list initializer_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match push_stack_variables actor writer_pc writer_expression_number method_id
                             frame_uniq initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v))
          (decreases initializers) =
  match initializers with
  | [] -> ()
  | first_initializer :: remaining_initializers ->
      push_stack_variable_maintains_variable_among_gvars v actor writer_pc writer_expression_number method_id frame_uniq
        first_initializer s;
      (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq first_initializer s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           push_stack_variables_maintains_variable_among_gvars v actor writer_pc (writer_expression_number + 1)
             method_id frame_uniq remaining_initializers s')

let rec push_stack_parameters_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (writer_pc: pc_t)
  (writer_expression_number: nat)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (parameters: list object_value_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match push_stack_parameters actor writer_pc writer_expression_number method_id frame_uniq
                             var_ids parameters s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v))
          (decreases parameters) =
  match parameters, var_ids with
  | [], [] -> ()
  | first_parameter :: remaining_parameters, first_var_id :: remaining_var_ids ->
      let first_initializer =
        { var_id = first_var_id; iv = InitializerSpecific first_parameter; weakly_consistent = false } in
      push_stack_variable_maintains_variable_among_gvars v actor writer_pc writer_expression_number method_id frame_uniq
        first_initializer s;
      (match push_stack_variable actor writer_pc writer_expression_number method_id frame_uniq first_initializer s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces s' ->
           push_stack_parameters_maintains_variable_among_gvars v actor writer_pc (writer_expression_number + 1)
             method_id frame_uniq remaining_var_ids remaining_parameters s')
  | _ -> ()

let rec pop_stack_variables_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (method_id: method_id_t)
  (frame_uniq: root_id_uniquifier_t)
  (var_ids: list var_id_t)
  (mem: Armada.Memory.t)
  : Lemma (requires variable_among_gvars mem v)
          (ensures  (match pop_stack_variables actor method_id frame_uniq var_ids mem with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces mem' -> variable_among_gvars mem' v)) =
  match var_ids with
  | [] -> ()
  | first_var_id :: remaining_var_ids ->
      (match pop_stack_variable actor method_id frame_uniq first_var_id mem with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces mem' ->
           pop_stack_variables_maintains_variable_among_gvars v actor method_id frame_uniq remaining_var_ids mem')
/
Util.Tactics.fst.checked Util.List.fst.checked Strategies.ArmadaStatement.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked FStar.Classical.Sugar.fsti.checked Armada.Type.fst.checked Armada.Transition.fst.checked Armada.Thread.fst.checked Armada.Step.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Program.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.GlobalVars.Permanent.fst

    v: Armada.Base.var_id_t ->
    actor: Armada.Base.tid_t ->
    writer_pc: Armada.Base.pc_t ->
    writer_expression_number: Prims.nat ->
    bypassing_write_buffer: Prims.bool ->
    reads_clauses: Prims.list (Armada.Base.var_id_t * Armada.Expression.expression_t) ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.GlobalVars.Permanent.variable_among_gvars (Mkt?.mem s) v)
      (ensures
        ((match
              Armada.Statement.external_method_take_snapshot_of_reads_clauses_computation actor
                writer_pc
                writer_expression_number
                bypassing_write_buffer
                reads_clauses
                s
            with
            | Armada.Computation.ComputationImpossible #_ -> Prims.l_True
            | Armada.Computation.ComputationUndefined #_ -> Prims.l_True
            | Armada.Computation.ComputationProduces #_ s' ->
              Strategies.GlobalVars.Permanent.variable_among_gvars (Mkt?.mem s') v)
          <:
          Type0))
      (decreases reads_clauses)
Armada.Base.var_id_t Armada.Base.tid_t Armada.Base.pc_t Prims.nat Prims.bool Prims.list FStar.Pervasives.Native.tuple2 Armada.Expression.expression_t Armada.State.t Armada.Expression.rvalue_computation Armada.Type.valid_object_value_t Armada.Expression.expression_to_td Armada.Expression.update_expression Strategies.GlobalVars.Permanent.external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars Prims.op_Addition Prims.unit Strategies.GlobalVars.Permanent.update_expression_maintains_variable_among_gvars Armada.Expression.ExpressionLocalVariable Armada.Type.object_td_t Prims.b2t Strategies.GlobalVars.Permanent.variable_among_gvars Armada.State.__proj__Mkt__item__mem Prims.squash Armada.Statement.external_method_take_snapshot_of_reads_clauses_computation Prims.l_True Prims.Nil FStar.Pervasives.pattern
let rec external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars
      (v: var_id_t)
      (actor: tid_t)
      (writer_pc: pc_t)
      (writer_expression_number: nat)
      (bypassing_write_buffer: bool)
      (reads_clauses: list (var_id_t * expression_t))
      (s: Armada.State.t)
    : Lemma (requires variable_among_gvars s.mem v)
      (ensures
        (match
            external_method_take_snapshot_of_reads_clauses_computation actor
              writer_pc
              writer_expression_number
              bypassing_write_buffer
              reads_clauses
              s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> variable_among_gvars s'.mem v))
      (decreases reads_clauses) =
  
match reads_clauses with
| [] -> ()
| (first_var_id, first_reads_expression) :: remaining_reads_clauses ->
  (match rvalue_computation first_reads_expression actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces first_value ->
      let td = expression_to_td first_reads_expression in
      let local_var = ExpressionLocalVariable td first_var_id in
      update_expression_maintains_variable_among_gvars v
        local_var
        actor
        writer_pc
        writer_expression_number
        bypassing_write_buffer
        first_value
        s;
      (match
          update_expression local_var
            actor
            writer_pc
            writer_expression_number
            bypassing_write_buffer
            first_value
            s
        with
        | ComputationImpossible | ComputationUndefined -> ()
        | ComputationProduces s' ->
          external_method_take_snapshot_of_reads_clauses_computation_maintains_variable_among_gvars v
            actor
            writer_pc
            (writer_expression_number + 1)
            bypassing_write_buffer
            remaining_reads_clauses
            s'))
| _ -> ()