val create_thread_statement_computation_maintains_variable_among_gvars
      (v: var_id_t)
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (method_id: method_id_t)
      (initial_pc: pc_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (parameter_var_ids: list var_id_t)
      (parameter_expressions: list expression_t)
      (local_variable_initializers: list initializer_t)
      (s: Armada.State.t)
    : Lemma (requires variable_among_gvars s.mem v)
      (ensures
        (match
            create_thread_statement_computation actor nd start_pc method_id initial_pc
              bypassing_write_buffer optional_result parameter_var_ids parameter_expressions
              local_variable_initializers s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> variable_among_gvars s'.mem v))
val create_thread_statement_computation_maintains_variable_among_gvars
      (v: var_id_t)
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (method_id: method_id_t)
      (initial_pc: pc_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (parameter_var_ids: list var_id_t)
      (parameter_expressions: list expression_t)
      (local_variable_initializers: list initializer_t)
      (s: Armada.State.t)
    : Lemma (requires variable_among_gvars s.mem v)
      (ensures
        (match
            create_thread_statement_computation actor nd start_pc method_id initial_pc
              bypassing_write_buffer optional_result parameter_var_ids parameter_expressions
              local_variable_initializers s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> variable_among_gvars s'.mem v))
let create_thread_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (method_id: method_id_t)
  (initial_pc: pc_t)
  (bypassing_write_buffer: bool)
  (optional_result: option expression_t)
  (parameter_var_ids: list var_id_t)
  (parameter_expressions: list expression_t)
  (local_variable_initializers: list initializer_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match create_thread_statement_computation actor nd start_pc method_id initial_pc
                             bypassing_write_buffer optional_result parameter_var_ids parameter_expressions
                             local_variable_initializers s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract create_thread_nd_t)
     || (   Some? optional_result
        && neqb (expression_to_td (Some?.v optional_result)) (ObjectTDPrimitive PrimitiveTDThreadId))
     || list_len parameter_var_ids <> list_len parameter_expressions then
    ()
  else (
    let create_thread_nd: create_thread_nd_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    let new_tid = create_thread_nd.new_tid in
    if new_tid = 0 then
      (match optional_result with
       | None -> ()
       | Some result ->
          let new_tid_value = ObjectValuePrimitive (PrimitiveBoxThreadId new_tid) in
          update_expression_maintains_variable_among_gvars v result actor start_pc
            (list_len parameter_var_ids + list_len local_variable_initializers) bypassing_write_buffer
            new_tid_value s)
    else (
      let frame_uniq = create_thread_nd.frame_uniq in
      match rvalues_computation parameter_expressions actor s with
      | ComputationImpossible | ComputationUndefined -> ()
      | ComputationProduces parameter_values ->
          let s2 = make_thread_running method_id initial_pc new_tid frame_uniq s in
          push_stack_parameters_maintains_variable_among_gvars v new_tid start_pc 0 method_id
            frame_uniq parameter_var_ids parameter_values s2;
          (match push_stack_parameters new_tid start_pc 0 method_id frame_uniq parameter_var_ids
                   parameter_values s2 with
           | ComputationImpossible | ComputationUndefined -> ()
           | ComputationProduces s3 ->
                push_stack_variables_maintains_variable_among_gvars v new_tid start_pc
                  (list_len parameter_var_ids) method_id frame_uniq local_variable_initializers s3;
                (match push_stack_variables new_tid start_pc (list_len parameter_var_ids) method_id frame_uniq
                         local_variable_initializers s3 with
                 | ComputationImpossible | ComputationUndefined -> ()
                 | ComputationProduces s4 ->
                     (match optional_result with
                      | None -> ()
                      | Some result ->
                         let new_tid_value = ObjectValuePrimitive (PrimitiveBoxThreadId new_tid) in
                         update_expression_maintains_variable_among_gvars v result actor start_pc
                           (list_len parameter_var_ids + list_len local_variable_initializers) bypassing_write_buffer
                           new_tid_value s4)))
    )
  )
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')

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'))
  | _ -> ()

let rec log_expressions_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (logs_clauses: list expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match log_expressions_computation actor logs_clauses s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v))
          (decreases logs_clauses) =
  match logs_clauses with
  | [] -> ()
  | first_logs_clause :: remaining_logs_clauses ->
      (match rvalue_computation first_logs_clause actor s with
       | ComputationImpossible | ComputationUndefined -> ()
       | ComputationProduces event ->
           let trace' = s.trace $:: event in
           let s' = { s with trace = trace' } in
           log_expressions_computation_maintains_variable_among_gvars v actor remaining_logs_clauses s')

let propagate_write_message_maintains_variable_among_gvars
  (v: var_id_t)
  (write_message: write_message_t)
  (receiver_tid: tid_t)
  (mem: Armada.Memory.t)
  : Lemma (requires variable_among_gvars mem v)
          (ensures  (match propagate_write_message write_message receiver_tid mem with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces mem' -> variable_among_gvars mem' v)) =
  let p = write_message.location in
  match dereference_computation p mem with
  | ComputationImpossible | ComputationUndefined -> ()
  | ComputationProduces storage ->
      (match storage with
       | ObjectStorageWeaklyConsistentPrimitive primitive_td values local_versions ->
           if   primitive_td <> write_message.primitive_td
              || write_message.version >= length values
              || local_versions receiver_tid >= write_message.version then
             ()
           else
             let new_local_versions = Spec.Map.upd local_versions receiver_tid write_message.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_maintains_variable_among_gvars v p new_storage mem
       | _ -> ())

let free_pointer_maintains_variable_among_gvars
  (v: var_id_t)
  (p: Armada.Pointer.t)
  (mem: Armada.Memory.t)
  : Lemma (requires variable_among_gvars mem v)
          (ensures  (match free_pointer p mem with
                     | ComputationProduces mem' -> variable_among_gvars mem' v
                     | _ -> True)) =
  ()

#push-options "--z3rlimit 10"

let assume_expression_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match assume_expression_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  ()

let assume_predicate_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (pred: Armada.State.t -> GTot bool)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match assume_predicate_statement_computation actor nd start_pc pred s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  ()

let assert_true_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match assert_true_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  ()

let assert_false_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match assert_false_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  ()

let conditional_jump_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match conditional_jump_statement_computation actor nd start_pc exp s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  ()

let unconditional_jump_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match unconditional_jump_statement_computation actor nd start_pc s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  ()

let update_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (src: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match update_statement_computation actor nd start_pc bypassing_write_buffer dst src s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  let cs' = update_statement_computation actor nd start_pc bypassing_write_buffer dst src s in
  if   Cons? nd
     || neqb (expression_to_td dst) (expression_to_td src) then
    ()
  else (
    match rvalue_computation src actor s with
    | ComputationImpossible | ComputationUndefined -> ()
    | ComputationProduces src_value ->
        update_expression_maintains_variable_among_gvars v dst actor start_pc 0 bypassing_write_buffer src_value s
  )

let nondeterministic_update_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match nondeterministic_update_statement_computation actor nd start_pc bypassing_write_buffer
                             dst s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  let cs' = nondeterministic_update_statement_computation actor nd start_pc bypassing_write_buffer dst s in
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (expression_to_td dst) then
    ()
  else (
    let nd_value = Cons?.hd nd in
    if not (object_value_has_all_pointers_uninitialized nd_value) then
      ()
    else
      update_expression_maintains_variable_among_gvars v dst actor start_pc 0 bypassing_write_buffer nd_value s
  )

let propagate_write_message_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match propagate_write_message_statement_computation actor nd s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract tid_t) then
     ()
  else
    let receiver_tid: tid_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    if receiver_tid = actor then // can't propagate to the same thread
      ()
    else
      let propagator_thread = s.threads actor in
      let receiver_thread = s.threads receiver_tid in
      let which_message = receiver_thread.position_in_other_write_buffers actor in
      if which_message >= length propagator_thread.write_buffer then
        ()
      else
        let write_message = index propagator_thread.write_buffer which_message in
        propagate_write_message_maintains_variable_among_gvars v write_message receiver_tid s.mem

let compare_and_swap_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (target: expression_t)
  (old_val: expression_t)
  (new_val: expression_t)
  (bypassing_write_buffer: bool)
  (optional_result: option expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match compare_and_swap_statement_computation actor nd start_pc target old_val new_val
                             bypassing_write_buffer optional_result s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  let cs' = compare_and_swap_statement_computation actor nd start_pc target old_val new_val
              bypassing_write_buffer optional_result s in
  if   Cons? nd
     || neqb (expression_to_td target) (expression_to_td old_val)
     || neqb (expression_to_td target) (expression_to_td new_val)
     || (match optional_result with
        | Some result -> neqb (expression_to_td result) (ObjectTDPrimitive PrimitiveTDBool)
        | None -> false) then
    ()
  else begin
    match check_expression_up_to_date_for_rmw target actor s, rvalue_computation old_val actor s,
          rvalue_computation target actor s, rvalue_computation new_val actor s,
          lvalue_computation target actor s  with
    | ComputationProduces _, ComputationProduces old_value,
      ComputationProduces target_value, ComputationProduces new_value,
      ComputationProduces target_ptr -> begin
        let swap = eqb target_value old_value in
        update_pointed_to_value_maintains_variable_among_gvars v target_ptr actor start_pc 0 false new_value s;
        match optional_result with
        | None -> ()
        | Some result ->
          match lvalue_computation result actor s, (if swap then update_pointed_to_value target_ptr actor start_pc 0 false new_value s else return s) with
          | ComputationProduces result_ptr, ComputationProduces s' ->
              let swap_value = ObjectValuePrimitive (PrimitiveBoxBool swap) in
              update_pointed_to_value_maintains_variable_among_gvars v result_ptr actor start_pc 1 bypassing_write_buffer swap_value s'
          | _ -> ()
      end
    | _ -> ()
  end

let atomic_exchange_statement_computation_maintains_variable_among_gvars
  (v: var_id_t)
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (old_val: expression_t)
  (target: expression_t)
  (new_val: expression_t)
  (s: Armada.State.t)
  : Lemma (requires variable_among_gvars s.mem v)
          (ensures  (match atomic_exchange_statement_computation actor nd start_pc old_val target new_val s with
                     | ComputationImpossible | ComputationUndefined -> True
                     | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  let cs' = atomic_exchange_statement_computation actor nd start_pc old_val target new_val s in
  match check_expression_up_to_date_for_rmw target actor s, rvalue_computation target actor s, rvalue_computation new_val actor s, lvalue_computation old_val actor s, lvalue_computation target actor s with
  | ComputationProduces _, ComputationProduces target_value, ComputationProduces new_value, ComputationProduces old_ptr, ComputationProduces target_ptr ->
    update_pointed_to_value_maintains_variable_among_gvars v old_ptr actor start_pc 0 false target_value s;
    begin match update_pointed_to_value old_ptr actor start_pc 0 false target_value s with
          | ComputationProduces s' ->
            update_pointed_to_value_maintains_variable_among_gvars v target_ptr actor start_pc 1 false new_value s'
          | _ -> ()
    end
  | _ -> ()
/
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 ->
    nd: Armada.Type.nondeterminism_t ->
    start_pc: Armada.Base.pc_t ->
    method_id: Armada.Base.method_id_t ->
    initial_pc: Armada.Base.pc_t ->
    bypassing_write_buffer: Prims.bool ->
    optional_result: FStar.Pervasives.Native.option Armada.Expression.expression_t ->
    parameter_var_ids: Prims.list Armada.Base.var_id_t ->
    parameter_expressions: Prims.list Armada.Expression.expression_t ->
    local_variable_initializers: Prims.list Armada.Init.initializer_t ->
    s: Armada.State.t
  -> FStar.Pervasives.Lemma
      (requires Strategies.GlobalVars.Permanent.variable_among_gvars (Mkt?.mem s) v)
      (ensures
        ((match
              Armada.Statement.create_thread_statement_computation actor nd start_pc method_id
                initial_pc bypassing_write_buffer optional_result parameter_var_ids
                parameter_expressions local_variable_initializers 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))
Armada.Base.var_id_t Armada.Base.tid_t Armada.Type.nondeterminism_t Armada.Base.pc_t Armada.Base.method_id_t Prims.bool FStar.Pervasives.Native.option Armada.Expression.expression_t Prims.list Armada.Init.initializer_t Armada.State.t Prims.op_BarBar Prims.op_disEquality Prims.int Spec.List.list_len Armada.Type.object_value_t Spec.Ubool.neqb Armada.Type.object_td_t Armada.Type.object_value_to_td Prims.__proj__Cons__item__hd Armada.Type.ObjectTDAbstract Armada.Statement.create_thread_nd_t Prims.op_AmpAmp FStar.Pervasives.Native.uu___is_Some Armada.Expression.expression_to_td FStar.Pervasives.Native.__proj__Some__item__v Armada.Type.ObjectTDPrimitive Armada.Type.PrimitiveTDThreadId Prims.nat Prims.op_Equality Strategies.GlobalVars.Permanent.update_expression_maintains_variable_among_gvars Prims.op_Addition Armada.Type.ObjectValuePrimitive Armada.Type.PrimitiveBoxThreadId Prims.unit Armada.Expression.rvalues_computation Armada.Init.push_stack_parameters Armada.Init.push_stack_variables Strategies.GlobalVars.Permanent.push_stack_variables_maintains_variable_among_gvars Strategies.GlobalVars.Permanent.push_stack_parameters_maintains_variable_among_gvars Armada.Statement.make_thread_running Armada.Base.root_id_uniquifier_t Armada.Statement.__proj__Mkcreate_thread_nd_t__item__frame_uniq Armada.Statement.__proj__Mkcreate_thread_nd_t__item__new_tid Armada.Type.__proj__ObjectValueAbstract__item__value Prims.b2t Strategies.GlobalVars.Permanent.variable_among_gvars Armada.State.__proj__Mkt__item__mem Prims.squash Armada.Statement.create_thread_statement_computation Prims.l_True Prims.Nil FStar.Pervasives.pattern
let create_thread_statement_computation_maintains_variable_among_gvars
      (v: var_id_t)
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (method_id: method_id_t)
      (initial_pc: pc_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (parameter_var_ids: list var_id_t)
      (parameter_expressions: list expression_t)
      (local_variable_initializers: list initializer_t)
      (s: Armada.State.t)
    : Lemma (requires variable_among_gvars s.mem v)
      (ensures
        (match
            create_thread_statement_computation actor nd start_pc method_id initial_pc
              bypassing_write_buffer optional_result parameter_var_ids parameter_expressions
              local_variable_initializers s
          with
          | ComputationImpossible | ComputationUndefined -> True
          | ComputationProduces s' -> variable_among_gvars s'.mem v)) =
  
if
  list_len nd <> 1 || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract create_thread_nd_t) ||
  (Some? optional_result &&
    neqb (expression_to_td (Some?.v optional_result)) (ObjectTDPrimitive PrimitiveTDThreadId)) ||
  list_len parameter_var_ids <> list_len parameter_expressions
then ()
else
  (let create_thread_nd:create_thread_nd_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    let new_tid = create_thread_nd.new_tid in
    if new_tid = 0
    then
      (match optional_result with
        | None -> ()
        | Some result ->
          let new_tid_value = ObjectValuePrimitive (PrimitiveBoxThreadId new_tid) in
          update_expression_maintains_variable_among_gvars v
            result
            actor
            start_pc
            (list_len parameter_var_ids + list_len local_variable_initializers)
            bypassing_write_buffer
            new_tid_value
            s)
    else
      (let frame_uniq = create_thread_nd.frame_uniq in
        match rvalues_computation parameter_expressions actor s with
        | ComputationImpossible | ComputationUndefined -> ()
        | ComputationProduces parameter_values ->
          let s2 = make_thread_running method_id initial_pc new_tid frame_uniq s in
          push_stack_parameters_maintains_variable_among_gvars v
            new_tid
            start_pc
            0
            method_id
            frame_uniq
            parameter_var_ids
            parameter_values
            s2;
          (match
              push_stack_parameters new_tid
                start_pc
                0
                method_id
                frame_uniq
                parameter_var_ids
                parameter_values
                s2
            with
            | ComputationImpossible | ComputationUndefined -> ()
            | ComputationProduces s3 ->
              push_stack_variables_maintains_variable_among_gvars v
                new_tid
                start_pc
                (list_len parameter_var_ids)
                method_id
                frame_uniq
                local_variable_initializers
                s3;
              (match
                  push_stack_variables new_tid
                    start_pc
                    (list_len parameter_var_ids)
                    method_id
                    frame_uniq
                    local_variable_initializers
                    s3
                with
                | ComputationImpossible | ComputationUndefined -> ()
                | ComputationProduces s4 ->
                  (match optional_result with
                    | None -> ()
                    | Some result ->
                      let new_tid_value = ObjectValuePrimitive (PrimitiveBoxThreadId new_tid) in
                      update_expression_maintains_variable_among_gvars v
                        result
                        actor
                        start_pc
                        (list_len parameter_var_ids + list_len local_variable_initializers)
                        bypassing_write_buffer
                        new_tid_value
                        s4)))))