val efficient_program_statement_end_pcs_match_per_pc_relation
      (relation return_relation: relation_t nat nat)
      (ps1 ps2: program_statement_t)
      (pc_indices1 pc_indices2: statement_pc_indices_t)
    : GTot ubool
val efficient_program_statement_end_pcs_match_per_pc_relation
      (relation return_relation: relation_t nat nat)
      (ps1 ps2: program_statement_t)
      (pc_indices1 pc_indices2: statement_pc_indices_t)
    : GTot ubool
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
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
/
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

    relation: Util.Relation.relation_t Prims.nat Prims.nat ->
    return_relation: Util.Relation.relation_t Prims.nat Prims.nat ->
    ps1: Armada.Action.program_statement_t ->
    ps2: Armada.Action.program_statement_t ->
    pc_indices1: Strategies.PCIndices.statement_pc_indices_t ->
    pc_indices2: Strategies.PCIndices.statement_pc_indices_t
  -> Prims.GTot Spec.Ubool.ubool
Util.Relation.relation_t Prims.nat Armada.Action.program_statement_t Strategies.PCIndices.statement_pc_indices_t FStar.Pervasives.Native.Mktuple2 FStar.Pervasives.Native.option Strategies.PCIndices.__proj__Mkstatement_pc_indices_t__item__end_pc_index Prims.l_and Prims.b2t Prims.l_imp Armada.Statement.uu___is_ReturnStatement Armada.Action.__proj__Mkprogram_statement_t__item__statement Prims.l_True Prims.l_False Spec.Ubool.ubool
let efficient_program_statement_end_pcs_match_per_pc_relation
      (relation return_relation: relation_t nat nat)
      (ps1 ps2: program_statement_t)
      (pc_indices1 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