val statement_effect_independent_of_global_variables
      (vs: list var_id_t)
      (statement: Armada.Statement.t)
    : GTot bool
val statement_effect_independent_of_global_variables
      (vs: list var_id_t)
      (statement: Armada.Statement.t)
    : GTot bool
let statement_effect_independent_of_global_variables
  (vs: list var_id_t)
  (statement: Armada.Statement.t)
  : GTot bool =
  match statement with
  | AssumeExpressionStatement exp ->
      global_variables_unmentioned_in_expression vs exp
  | AssumePredicateStatement pred ->
      false
  | AssertTrueStatement exp ->
      global_variables_unmentioned_in_expression vs exp
  | AssertFalseStatement exp ->
      global_variables_unmentioned_in_expression vs exp
  | ConditionalJumpStatement cond ->
      global_variables_unmentioned_in_expression vs cond
  | UnconditionalJumpStatement ->
      true
  | UpdateStatement _ dst src ->
         global_variables_unmentioned_in_expression vs dst
      && global_variables_unmentioned_in_expression vs src
  | NondeterministicUpdateStatement _ dst ->
      global_variables_unmentioned_in_expression vs dst
  | PropagateWriteMessageStatement ->
      false
  | CompareAndSwapStatement target old_val new_val bypassing_write_buffer optional_result ->
         global_variables_unmentioned_in_expression vs target
      && global_variables_unmentioned_in_expression vs old_val
      && global_variables_unmentioned_in_expression vs new_val
      && global_variables_unmentioned_in_optional_expression vs optional_result
  | AtomicExchangeStatement old_val target new_val ->
         global_variables_unmentioned_in_expression vs old_val
      && global_variables_unmentioned_in_expression vs target
      && global_variables_unmentioned_in_expression vs new_val
  | CreateThreadStatement _ _ _ option_result _ parameter_expressions local_variable_initializers ->
         global_variables_unmentioned_in_optional_expression vs option_result
      && global_variables_unmentioned_in_expressions vs parameter_expressions
      && global_variables_unaddressed_in_initializers vs local_variable_initializers
  | MethodCallStatement _ _ parameter_var_ids parameter_expressions local_variable_initializers stack_overflow ->
         global_variables_unmentioned_in_expressions vs parameter_expressions
      && global_variables_unaddressed_in_initializers vs local_variable_initializers
  | ReturnStatement _ _ output_dsts output_srcs ->
         global_variables_unmentioned_in_expressions vs output_dsts
      && global_variables_unmentioned_in_expressions vs output_srcs
  | TerminateThreadStatement _ ->
      true
  | TerminateProcessStatement _ ->
      true
  | JoinStatement join_tid ->
      global_variables_unmentioned_in_expression vs join_tid
  | MallocSuccessfulStatement _ result _ count ->
         global_variables_unmentioned_in_expression vs result
      && global_variables_unmentioned_in_expression vs count
  | MallocReturningNullStatement _ result count ->
         global_variables_unmentioned_in_expression vs result
      && global_variables_unmentioned_in_expression vs count
  | CallocSuccessfulStatement _ result _ count ->
         global_variables_unmentioned_in_expression vs result
      && global_variables_unmentioned_in_expression vs count
  | CallocReturningNullStatement _ result count ->
         global_variables_unmentioned_in_expression vs result
      && global_variables_unmentioned_in_expression vs count
  | DeallocStatement ptr ->
      global_variables_unmentioned_in_expression vs ptr

  // For SomehowStatement, we have no idea what's put into the
  // destinations specified in modifies clauses.  So all we can do is
  // make sure that none of those destinations has any pointer fields.
  
  | SomehowStatement undefined_unless_cond _ modifies_clauses ensures_cond ->
         global_variables_unmentioned_in_expression vs undefined_unless_cond
      && global_variables_unmentioned_in_expressions vs modifies_clauses
      && expressions_lack_pointer_field modifies_clauses
      && global_variables_unmentioned_in_expression vs ensures_cond

  | FenceStatement ->
      true

  // For ExternalMethodStartStatement and
  // ExternalMethodMiddleStatement, we have no idea what's put into
  // the destinations specified in modifies clauses.  So all we can do
  // is make sure that none of those destinations has any pointer
  // fields.

  | ExternalMethodStartStatement await_cond undefined_unless_cond _ modifies_clauses reads_clauses ->
         global_variables_unmentioned_in_expression vs await_cond
      && global_variables_unmentioned_in_expression vs undefined_unless_cond
      && global_variables_unmentioned_in_expressions vs modifies_clauses
      && expressions_lack_pointer_field modifies_clauses
      && global_variables_unmentioned_in_reads_clauses vs reads_clauses
  | ExternalMethodMiddleStatement _ modifies_clauses reads_clauses ->
         global_variables_unmentioned_in_expressions vs modifies_clauses
      && expressions_lack_pointer_field modifies_clauses
      && global_variables_unmentioned_in_reads_clauses vs reads_clauses

  | ExternalMethodEndStatement ensures_cond logs_clauses ->
         global_variables_unmentioned_in_expression vs ensures_cond
      && global_variables_unmentioned_in_expressions vs logs_clauses
module Strategies.GlobalVars.Statement

open Armada.Action
open Armada.Base
open Armada.Computation
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Spec.Ubool
open Strategies.ArmadaInvariant.RootsMatch
open Strategies.ArmadaInvariant.PositionsValid
open Strategies.ArmadaInvariant.UnstartedThreads
open Strategies.GlobalVars
open Strategies.PCIndices
open Strategies.PCRelation
open Util.ImmutableArray
open Util.Relation

let statements_match_per_pc_relation
  (relation: relation_t pc_t pc_t)
  (return_relation: relation_t pc_t pc_t)
  (statement1: Armada.Statement.t)
  (statement2: Armada.Statement.t)
  : GTot ubool =
  match statement1 with
  | CreateThreadStatement method_id1 initial_pc1 bypassing_write_buffer1 optional_result1 parameter_var_ids1
                          parameter_expressions1 local_variable_initializers1 ->
      (match statement2 with
       | CreateThreadStatement method_id2 initial_pc2 bypassing_write_buffer2 optional_result2 parameter_var_ids2
                               parameter_expressions2 local_variable_initializers2 ->
              method_id1 = method_id2
           /\ relation initial_pc1 initial_pc2
           /\ bypassing_write_buffer1 = bypassing_write_buffer2
           /\ optional_result1 == optional_result2
           /\ parameter_var_ids1 = parameter_var_ids2
           /\ parameter_expressions1 == parameter_expressions2
           /\ local_variable_initializers1 == local_variable_initializers2
       | _ -> False)
  | MethodCallStatement method_id1 return_pc1 parameter_var_ids1 parameter_expressions1 local_variable_initializers1
                          stack_overflow1 ->
      (match statement2 with
       | MethodCallStatement method_id2 return_pc2 parameter_var_ids2 parameter_expressions2
                             local_variable_initializers2 stack_overflow2 ->
              method_id1 = method_id2
           /\ relation return_pc1 return_pc2
           /\ return_relation return_pc1 return_pc2
           /\ parameter_var_ids1 = parameter_var_ids2
           /\ parameter_expressions1 == parameter_expressions2
           /\ local_variable_initializers1 == local_variable_initializers2
           /\ stack_overflow1 = stack_overflow2
       | _ -> False)
  | _ -> statement2 == statement1

let efficient_statements_match_per_pc_relation
  (relation: relation_t nat nat)
  (return_relation: relation_t nat nat)
  (statement1: Armada.Statement.t)
  (statement2: Armada.Statement.t)
  (pc_indices1: statement_pc_indices_t)
  (pc_indices2: statement_pc_indices_t)
  : GTot ubool =
  match statement1 with
  | CreateThreadStatement method_id1 initial_pc1 bypassing_write_buffer1 optional_result1 parameter_var_ids1
                          parameter_expressions1 local_variable_initializers1 ->
      (match statement2 with
       | CreateThreadStatement method_id2 initial_pc2 bypassing_write_buffer2 optional_result2 parameter_var_ids2
                               parameter_expressions2 local_variable_initializers2 ->
              method_id1 = method_id2
           /\ bypassing_write_buffer1 = bypassing_write_buffer2
           /\ optional_result1 == optional_result2
           /\ parameter_var_ids1 = parameter_var_ids2
           /\ parameter_expressions1 == parameter_expressions2
           /\ local_variable_initializers1 == local_variable_initializers2
           /\ (match pc_indices1.create_thread_initial_pc_index, pc_indices2.create_thread_initial_pc_index with
              | Some idx1, Some idx2 -> relation idx1 idx2
              | _, _ -> False)
       | _ -> False)
  | MethodCallStatement method_id1 return_pc1 parameter_var_ids1 parameter_expressions1 local_variable_initializers1
                          stack_overflow1 ->
      (match statement2 with
       | MethodCallStatement method_id2 return_pc2 parameter_var_ids2 parameter_expressions2
                             local_variable_initializers2 stack_overflow2 ->
              method_id1 = method_id2
           /\ parameter_var_ids1 = parameter_var_ids2
           /\ parameter_expressions1 == parameter_expressions2
           /\ local_variable_initializers1 == local_variable_initializers2
           /\ stack_overflow1 = stack_overflow2
           /\ (match pc_indices1.method_call_return_pc_index, pc_indices2.method_call_return_pc_index with
              | Some idx1, Some idx2 -> relation idx1 idx2 /\ return_relation idx1 idx2
              | _, _ -> False)
       | _ -> False)
  | _ -> statement2 == statement1

let efficient_statements_match_per_pc_relation_implies_statements_match_per_pc_relation
  (pcs1: array_t pc_t)
  (pcs2: array_t pc_t)
  (idx_relation: relation_t nat nat)
  (idx_return_relation: relation_t nat nat)
  (pc_relation: relation_t pc_t pc_t)
  (pc_return_relation: relation_t pc_t pc_t)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  (pc_indices1: statement_pc_indices_t)
  (pc_indices2: statement_pc_indices_t)
  : Lemma (requires   program_statement_corresponds_to_statement_pc_indices pcs1 ps1 pc_indices1
                    /\ program_statement_corresponds_to_statement_pc_indices pcs2 ps2 pc_indices2
                    /\ efficient_statements_match_per_pc_relation idx_relation idx_return_relation
                        ps1.statement ps2.statement pc_indices1 pc_indices2
                    /\ (forall (idx1: nat) (idx2: nat). idx1 < array_len pcs1 /\ idx2 < array_len pcs2 ==>
                         (let pc1 = array_index pcs1 idx1 in
                          let pc2 = array_index pcs2 idx2 in
                            (idx_relation idx1 idx2 ==> pc_relation pc1 pc2)
                          /\ (idx_return_relation idx1 idx2 ==> pc_return_relation pc1 pc2))))
          (ensures statements_match_per_pc_relation pc_relation pc_return_relation ps1.statement ps2.statement) =
  ()

let program_statement_end_pcs_match_per_pc_relation
  (relation: relation_t pc_t pc_t)
  (return_relation: relation_t pc_t pc_t)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  : GTot ubool =
  match ps1.end_pc, ps2.end_pc with
  | Some pc1, Some pc2 -> relation pc1 pc2 /\ (ReturnStatement? ps1.statement ==> return_relation pc1 pc2)
  | None, None -> True
  | _, _ -> False

let efficient_program_statement_end_pcs_match_per_pc_relation
  (relation: relation_t nat nat)
  (return_relation: relation_t nat nat)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  (pc_indices1: statement_pc_indices_t)
  (pc_indices2: statement_pc_indices_t)
  : GTot ubool =
  match pc_indices1.end_pc_index, pc_indices2.end_pc_index with
  | Some pc1, Some pc2 -> relation pc1 pc2 /\ (ReturnStatement? ps1.statement ==> return_relation pc1 pc2)
  | None, None -> True
  | _, _ -> False

let efficient_statement_end_pcs_match_per_pc_relation_implies_program_statement_end_pcs_match_per_pc_relation
  (pcs1: array_t pc_t)
  (pcs2: array_t pc_t)
  (idx_relation: relation_t nat nat)
  (idx_return_relation: relation_t nat nat)
  (pc_relation: relation_t pc_t pc_t)
  (pc_return_relation: relation_t pc_t pc_t)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  (pc_indices1: statement_pc_indices_t)
  (pc_indices2: statement_pc_indices_t)
  : Lemma (requires   program_statement_corresponds_to_statement_pc_indices pcs1 ps1 pc_indices1
                    /\ program_statement_corresponds_to_statement_pc_indices pcs2 ps2 pc_indices2
                    /\ efficient_program_statement_end_pcs_match_per_pc_relation idx_relation idx_return_relation
                        ps1 ps2 pc_indices1 pc_indices2
                    /\ (forall (idx1: nat) (idx2: nat). idx1 < array_len pcs1 /\ idx2 < array_len pcs2 ==>
                         (let pc1 = array_index pcs1 idx1 in
                          let pc2 = array_index pcs2 idx2 in
                            (idx_relation idx1 idx2 ==> pc_relation pc1 pc2)
                          /\ (idx_return_relation idx1 idx2 ==> pc_return_relation pc1 pc2))))
          (ensures program_statement_end_pcs_match_per_pc_relation pc_relation pc_return_relation ps1 ps2) =
  ()

let program_statements_match_per_pc_relation
  (relation: relation_t pc_t pc_t)
  (return_relation: relation_t pc_t pc_t)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  : GTot ubool =
     statements_match_per_pc_relation relation return_relation ps1.statement ps2.statement
   /\ program_statement_end_pcs_match_per_pc_relation relation return_relation ps1 ps2

let efficient_program_statements_match_per_pc_relation
  (relation: relation_t nat nat)
  (return_relation: relation_t nat nat)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  (pc_indices1: statement_pc_indices_t)
  (pc_indices2: statement_pc_indices_t)
  : GTot ubool =
     efficient_statements_match_per_pc_relation relation return_relation ps1.statement ps2.statement pc_indices1
       pc_indices2
   /\ efficient_program_statement_end_pcs_match_per_pc_relation relation return_relation ps1 ps2 pc_indices1 pc_indices2

let efficient_program_statements_match_per_pc_relation_implies_program_statements_match_per_pc_relation
  (pcs1: array_t pc_t)
  (pcs2: array_t pc_t)
  (idx_relation: relation_t nat nat)
  (idx_return_relation: relation_t nat nat)
  (pc_relation: relation_t pc_t pc_t)
  (pc_return_relation: relation_t pc_t pc_t)
  (ps1: program_statement_t)
  (ps2: program_statement_t)
  (pc_indices1: statement_pc_indices_t)
  (pc_indices2: statement_pc_indices_t)
  : Lemma (requires   program_statement_corresponds_to_statement_pc_indices pcs1 ps1 pc_indices1
                    /\ program_statement_corresponds_to_statement_pc_indices pcs2 ps2 pc_indices2
                    /\ efficient_program_statements_match_per_pc_relation idx_relation idx_return_relation
                        ps1 ps2 pc_indices1 pc_indices2
                    /\ (forall (idx1: nat) (idx2: nat). idx1 < array_len pcs1 /\ idx2 < array_len pcs2 ==>
                         (let pc1 = array_index pcs1 idx1 in
                          let pc2 = array_index pcs2 idx2 in
                            (idx_relation idx1 idx2 ==> pc_relation pc1 pc2)
                          /\ (idx_return_relation idx1 idx2 ==> pc_return_relation pc1 pc2))))
          (ensures program_statements_match_per_pc_relation pc_relation pc_return_relation ps1 ps2) =
  efficient_statement_end_pcs_match_per_pc_relation_implies_program_statement_end_pcs_match_per_pc_relation
    pcs1 pcs2 idx_relation idx_return_relation pc_relation pc_return_relation ps1 ps2 pc_indices1 pc_indices2;
  efficient_statements_match_per_pc_relation_implies_statements_match_per_pc_relation pcs1 pcs2 idx_relation
    idx_return_relation pc_relation pc_return_relation ps1 ps2 pc_indices1 pc_indices2
/
Util.Relation.fst.checked Util.ImmutableArray.fsti.checked Strategies.PCRelation.fst.checked Strategies.PCIndices.fst.checked Strategies.GlobalVars.fst.checked Strategies.ArmadaInvariant.UnstartedThreads.fsti.checked Strategies.ArmadaInvariant.RootsMatch.fst.checked Strategies.ArmadaInvariant.PositionsValid.fsti.checked Spec.Ubool.fst.checked prims.fst.checked FStar.Pervasives.Native.fst.checked FStar.Pervasives.fsti.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Computation.fst.checked Armada.Base.fst.checked Armada.Action.fst.checked
Strategies.GlobalVars.Statement.fsti
vs: Prims.list Armada.Base.var_id_t -> statement: Armada.Statement.t -> Prims.GTot Prims.bool
Prims.list Armada.Base.var_id_t Armada.Statement.t Armada.Expression.expression_t Strategies.GlobalVars.global_variables_unmentioned_in_expression Armada.State.t Prims.bool Prims.op_AmpAmp FStar.Pervasives.Native.option Strategies.GlobalVars.global_variables_unmentioned_in_optional_expression Armada.Base.method_id_t Armada.Base.pc_t Armada.Init.initializer_t Strategies.GlobalVars.global_variables_unmentioned_in_expressions Strategies.GlobalVars.global_variables_unaddressed_in_initializers Armada.Type.object_td_t Strategies.GlobalVars.expressions_lack_pointer_field FStar.Pervasives.Native.tuple2 Strategies.GlobalVars.global_variables_unmentioned_in_reads_clauses
let statement_effect_independent_of_global_variables
      (vs: list var_id_t)
      (statement: Armada.Statement.t)
    : GTot bool =
  
match statement with
| AssumeExpressionStatement exp -> global_variables_unmentioned_in_expression vs exp
| AssumePredicateStatement pred -> false
| AssertTrueStatement exp -> global_variables_unmentioned_in_expression vs exp
| AssertFalseStatement exp -> global_variables_unmentioned_in_expression vs exp
| ConditionalJumpStatement cond -> global_variables_unmentioned_in_expression vs cond
| UnconditionalJumpStatement -> true
| UpdateStatement _ dst src ->
  global_variables_unmentioned_in_expression vs dst &&
  global_variables_unmentioned_in_expression vs src
| NondeterministicUpdateStatement _ dst -> global_variables_unmentioned_in_expression vs dst
| PropagateWriteMessageStatement -> false
| CompareAndSwapStatement target old_val new_val bypassing_write_buffer optional_result ->
  global_variables_unmentioned_in_expression vs target &&
  global_variables_unmentioned_in_expression vs old_val &&
  global_variables_unmentioned_in_expression vs new_val &&
  global_variables_unmentioned_in_optional_expression vs optional_result
| AtomicExchangeStatement old_val target new_val ->
  global_variables_unmentioned_in_expression vs old_val &&
  global_variables_unmentioned_in_expression vs target &&
  global_variables_unmentioned_in_expression vs new_val
| CreateThreadStatement _ _ _ option_result _ parameter_expressions local_variable_initializers ->
  global_variables_unmentioned_in_optional_expression vs option_result &&
  global_variables_unmentioned_in_expressions vs parameter_expressions &&
  global_variables_unaddressed_in_initializers vs local_variable_initializers
| MethodCallStatement
  _
  _
  parameter_var_ids
  parameter_expressions
  local_variable_initializers
  stack_overflow ->
  global_variables_unmentioned_in_expressions vs parameter_expressions &&
  global_variables_unaddressed_in_initializers vs local_variable_initializers
| ReturnStatement _ _ output_dsts output_srcs ->
  global_variables_unmentioned_in_expressions vs output_dsts &&
  global_variables_unmentioned_in_expressions vs output_srcs
| TerminateThreadStatement _ -> true
| TerminateProcessStatement _ -> true
| JoinStatement join_tid -> global_variables_unmentioned_in_expression vs join_tid
| MallocSuccessfulStatement _ result _ count ->
  global_variables_unmentioned_in_expression vs result &&
  global_variables_unmentioned_in_expression vs count
| MallocReturningNullStatement _ result count ->
  global_variables_unmentioned_in_expression vs result &&
  global_variables_unmentioned_in_expression vs count
| CallocSuccessfulStatement _ result _ count ->
  global_variables_unmentioned_in_expression vs result &&
  global_variables_unmentioned_in_expression vs count
| CallocReturningNullStatement _ result count ->
  global_variables_unmentioned_in_expression vs result &&
  global_variables_unmentioned_in_expression vs count
| DeallocStatement ptr -> global_variables_unmentioned_in_expression vs ptr
| SomehowStatement undefined_unless_cond _ modifies_clauses ensures_cond ->
  global_variables_unmentioned_in_expression vs undefined_unless_cond &&
  global_variables_unmentioned_in_expressions vs modifies_clauses &&
  expressions_lack_pointer_field modifies_clauses &&
  global_variables_unmentioned_in_expression vs ensures_cond
| FenceStatement -> true
| ExternalMethodStartStatement await_cond undefined_unless_cond _ modifies_clauses reads_clauses ->
  global_variables_unmentioned_in_expression vs await_cond &&
  global_variables_unmentioned_in_expression vs undefined_unless_cond &&
  global_variables_unmentioned_in_expressions vs modifies_clauses &&
  expressions_lack_pointer_field modifies_clauses &&
  global_variables_unmentioned_in_reads_clauses vs reads_clauses
| ExternalMethodMiddleStatement _ modifies_clauses reads_clauses ->
  global_variables_unmentioned_in_expressions vs modifies_clauses &&
  expressions_lack_pointer_field modifies_clauses &&
  global_variables_unmentioned_in_reads_clauses vs reads_clauses
| ExternalMethodEndStatement ensures_cond logs_clauses ->
  global_variables_unmentioned_in_expression vs ensures_cond &&
  global_variables_unmentioned_in_expressions vs logs_clauses