val join_statement_computation_redacted
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (join_tid: expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
val join_statement_computation_redacted
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (join_tid: expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
let join_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (join_tid: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td join_tid) (ObjectTDPrimitive PrimitiveTDThreadId) then
    ComputationImpossible
  else (
    let? tid_value = rvalue_computation_opaque join_tid actor s in
    let other_tid = PrimitiveBoxThreadId?.tid (ObjectValuePrimitive?.value tid_value) in
    let thread = s.threads other_tid in
    match thread.status with
    | ThreadStatusNotStarted -> ComputationImpossible // can't get a handle to a non-started thread
    | ThreadStatusRunning -> ComputationImpossible    // not possible since join would block
    | ThreadStatusPostJoin -> ComputationUndefined    // not defined to join a thread twice
    | ThreadStatusJoinable ->
        let thread' = { thread with status = ThreadStatusPostJoin } in
        let threads' = Spec.Map.upd s.threads other_tid thread' in
        let s' = { s with threads = threads' } in
        return s'
  )
module Strategies.ArmadaStatement.Opaque

open Armada.Base
open Armada.BinaryOp
open Armada.BoundedInt
open Armada.Computation
open Armada.Expression
open Armada.Init
open Armada.Memory
open Armada.Pointer
open Armada.State
open Armada.Statement
open Armada.Thread
open Armada.Type
open Armada.UnaryOp
open FStar.Sequence.Base
open FStar.Tactics.V2
open Spec.List
open Spec.Ubool
open Util.List

/// Opaque versions of complex functions called from statement definitions

[@"opaque_to_smt"]
let rvalue_computation_opaque = rvalue_computation

[@"opaque_to_smt"]
let rvalues_computation_opaque = rvalues_computation

[@"opaque_to_smt"]
let update_pointed_to_value_opaque = update_pointed_to_value

[@"opaque_to_smt"]
let update_expression_opaque = update_expression

[@"opaque_to_smt"]
let update_expressions_opaque = update_expressions

[@"opaque_to_smt"]
let propagate_write_message_opaque = propagate_write_message

[@"opaque_to_smt"]
let check_expression_up_to_date_for_rmw_opaque = check_expression_up_to_date_for_rmw

[@"opaque_to_smt"]
let push_stack_variables_opaque = push_stack_variables

[@"opaque_to_smt"]
let push_stack_parameters_opaque = push_stack_parameters

[@"opaque_to_smt"]
let pop_stack_variables_opaque = pop_stack_variables

[@"opaque_to_smt"]
let free_pointer_opaque = free_pointer

[@"opaque_to_smt"]
let external_method_take_snapshot_of_reads_clauses_computation_opaque =
  external_method_take_snapshot_of_reads_clauses_computation

[@"opaque_to_smt"]
let external_method_check_snapshot_computation_opaque = external_method_check_snapshot_computation

[@"opaque_to_smt"]
let log_expressions_computation_opaque = log_expressions_computation

[@"opaque_to_smt"]
let make_thread_running_opaque = make_thread_running

[@"opaque_to_smt"]
let push_stack_frame_opaque = push_stack_frame

[@"opaque_to_smt"]
let pop_stack_frame_opaque = pop_stack_frame

[@"opaque_to_smt"]
let mark_allocation_root_allocated_opaque = mark_allocation_root_allocated

/// Redacted versions of statement definitions that complex functions called from statement definitions

let assume_expression_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation_opaque exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )

let assume_predicate_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (pred: Armada.State.t -> GTot bool)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || not (pred s) then
    ComputationImpossible
  else
    return s

let assert_true_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation_opaque exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )

let assert_false_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
     ComputationImpossible
  else (
    let? value = rvalue_computation_opaque exp actor s in
    if ObjectValueAbstract?.value value <> false then
      ComputationImpossible
    else
      let s' = { s with stop_reason = StopReasonAssertionFailure } in
      return s'
  )

let conditional_jump_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (exp: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td exp) (ObjectTDAbstract bool) then
    ComputationImpossible
  else (
    let? value = rvalue_computation_opaque exp actor s in
    if ObjectValueAbstract?.value value <> true then
      ComputationImpossible
    else
      return s
  )

let unconditional_jump_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if Cons? nd then
    ComputationImpossible
  else
    return s
  
let update_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (src: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td dst) (expression_to_td src) then
    ComputationImpossible
  else (
    let? src_value = rvalue_computation_opaque src actor s in
    update_expression_opaque dst actor start_pc 0 bypassing_write_buffer src_value s
  )
  
let nondeterministic_update_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (bypassing_write_buffer: bool)
  (dst: expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (expression_to_td dst) then
    ComputationImpossible
  else (
    let nd_value = Cons?.hd nd in
    if not (object_value_has_all_pointers_uninitialized nd_value) then
      ComputationImpossible
    else
      update_expression_opaque dst actor start_pc 0 bypassing_write_buffer nd_value s
  )

let propagate_write_message_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract tid_t) then
    ComputationImpossible
  else
    let receiver_tid: tid_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    if receiver_tid = actor then // can't propagate to the same thread
      ComputationImpossible
    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
        ComputationImpossible
      else
        let write_message = index propagator_thread.write_buffer which_message in
        let position_in_other_write_buffers' =
          Spec.Map.upd receiver_thread.position_in_other_write_buffers actor (which_message + 1) in
        let receiver_thread' =
          { receiver_thread with position_in_other_write_buffers = position_in_other_write_buffers' } in
        let threads' = Spec.Map.upd s.threads receiver_tid receiver_thread' in
        match propagate_write_message_opaque write_message receiver_tid s.mem with
        | ComputationImpossible
        | ComputationUndefined ->
            // If propagate would trigger undefined behavior (e.g., by propagating to freed memory),
            // it just leaves memory unchanged.
            return ({ s with threads = threads'; })
        | ComputationProduces mem' ->
            return ({ s with mem = mem'; threads = threads'; })

let compare_and_swap_statement_computation_redacted
  (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)
  : GTot (conditional_computation_t Armada.State.t) =
  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
     ComputationImpossible
  else (
    let? _ = check_expression_up_to_date_for_rmw_opaque target actor s in
    let? old_value = rvalue_computation_opaque old_val actor s in
    let? target_value = rvalue_computation_opaque target actor s in
    let? new_value = rvalue_computation_opaque new_val actor s in
    let? target_ptr = lvalue_computation target actor s in
    let swap = eqb target_value old_value in
    let? s' = (if swap then update_pointed_to_value_opaque target_ptr actor start_pc 0 false new_value s else return s)
    in
    match optional_result with
    | None -> return s'
    | Some result ->
        // this line is deceptive, and we might be potentially bitten by it later
        // but it simplify the control flow
        let? result_ptr = lvalue_computation result actor s in
        let swap_value = ObjectValuePrimitive (PrimitiveBoxBool swap) in
        update_pointed_to_value_opaque result_ptr actor start_pc 1 bypassing_write_buffer swap_value s'
  )

let atomic_exchange_statement_computation_redacted
  (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)
  : GTot (conditional_computation_t Armada.State.t) =
  if   Cons? nd
     || neqb (expression_to_td target) (expression_to_td old_val)
     || neqb (expression_to_td target) (expression_to_td new_val) then
    ComputationImpossible
  else (
    // pre-update
    let? _ = check_expression_up_to_date_for_rmw_opaque target actor s in
    let? target_value = rvalue_computation_opaque target actor s in
    let? new_value = rvalue_computation_opaque new_val actor s in
    let? old_ptr = lvalue_computation old_val actor s in
    let? target_ptr = lvalue_computation target actor s in
    // post-update
    let? s' = update_pointed_to_value_opaque old_ptr actor start_pc 0 false target_value s in
    update_pointed_to_value_opaque target_ptr actor start_pc 1 false new_value s'
  )

let create_thread_statement_computation_redacted
  (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)
  : GTot (conditional_computation_t Armada.State.t) =
  // Nondeterminism must have exactly one element, of type create_thread_nd_t
  // If there is a target, then it must be of type thread ID
  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
    ComputationImpossible
  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 // thread creation failed, so just set the result to 0
      (match optional_result with
       | None -> return s
       | Some result ->
           let new_tid_value = ObjectValuePrimitive (PrimitiveBoxThreadId new_tid) in
           update_expression_opaque 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
      let new_thread = s.threads new_tid in
      if   new_thread.status <> ThreadStatusNotStarted
         || length new_thread.write_buffer <> 0
         || list_contains frame_uniq s.uniqs_used then
        ComputationImpossible
      else (
        // Evaluate parameter expressions
        let? parameter_values = rvalues_computation_opaque parameter_expressions actor s in
        // Set the new thread's parameters, and give it status "running".
        let s2 = make_thread_running_opaque method_id initial_pc new_tid frame_uniq s in
        // Initialize the input parameters on the stack of the new thread.
        // All input variables are assumed to be strongly consistent.
        let? s3 = push_stack_parameters_opaque new_tid start_pc 0 method_id frame_uniq parameter_var_ids
                    parameter_values s2 in
        // Initialize all remaining parameters on the stack of the new thread.
        let? s4 = push_stack_variables_opaque new_tid start_pc (list_len parameter_var_ids) method_id frame_uniq
                    local_variable_initializers s3 in
        // Set the target to the new thread's thread ID, if there is a target
        (match optional_result with
         | None -> return s4
         | Some result ->
             let new_tid_value = ObjectValuePrimitive (PrimitiveBoxThreadId new_tid) in
             update_expression_opaque result actor start_pc
               (list_len parameter_var_ids + list_len local_variable_initializers)
               bypassing_write_buffer new_tid_value s4)
    )
  )

let method_call_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (method_id: method_id_t)
  (return_pc: pc_t)
  (parameter_var_ids: list var_id_t)
  (parameter_expressions: list expression_t)
  (local_variable_initializers: list initializer_t)
  (stack_overflow: bool)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  // Nondeterminism must have exactly one element, of type method_call_nd_t
  if   list_len nd <> 1
     || neqb (object_value_to_td (Cons?.hd nd)) (ObjectTDAbstract method_call_nd_t) then
    ComputationImpossible
  else
    let method_call_nd: method_call_nd_t = ObjectValueAbstract?.value (Cons?.hd nd) in
    let frame_uniq = method_call_nd.frame_uniq in
    if list_contains frame_uniq s.uniqs_used then
      ComputationImpossible
    else (
      // Evaluate parameter expressions on old stack, in case they reference local variables
      let? parameter_values = rvalues_computation_opaque parameter_expressions actor s in
      let s2 = push_stack_frame_opaque actor method_id return_pc frame_uniq s in
      // All input variables are assumed to be strongly consistent, so pass weakly_consistent=false
      let? s3 = push_stack_parameters_opaque actor start_pc 0 method_id frame_uniq parameter_var_ids
                  parameter_values s2 in
      let? s4 = push_stack_variables_opaque actor start_pc (list_len parameter_var_ids) method_id frame_uniq
                  local_variable_initializers s3 in
      if stack_overflow then
        return ({ s4 with stop_reason = StopReasonStackOverflow })
      else
        return s4
    )

let return_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (end_pc: option pc_t)
  (method_id: method_id_t)
  (bypassing_write_buffer: bool)
  (output_dsts: list expression_t)
  (output_srcs: list expression_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  let thread = s.threads actor in
  if   Cons? nd
     || eqb thread.stack []
     || thread.top.method_id <> method_id
     || end_pc <> Some (Cons?.hd thread.stack).return_pc then
    ComputationImpossible
  else (
    // First, evaluate output sources, before we pop the stack.
    let? output_values = rvalues_computation_opaque output_srcs actor s in
    // Second, free the stack variables and pop the stack.
    let? mem' = pop_stack_variables_opaque actor method_id thread.top.frame_uniq thread.top.local_variables s.mem in
    let s2 = pop_stack_frame_opaque actor mem' s in
    // Third, assign output values to output destinations.
    update_expressions_opaque output_dsts actor start_pc 0 bypassing_write_buffer output_values s2
  )

let terminate_thread_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (method_id: method_id_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  let thread = s.threads actor in
  if   Cons? nd
     || neqb thread.stack []
     || thread.top.method_id <> method_id
     || actor = s.initial_tid then // returning from main in the initial thread terminates the process, not the thread
    ComputationImpossible
  else (
    // Otherwise, mark thread as joinable and free all stack variables
    let? mem' = pop_stack_variables_opaque actor method_id thread.top.frame_uniq thread.top.local_variables s.mem in
    let thread' = { thread with status = ThreadStatusJoinable } in
    let threads' = Spec.Map.upd s.threads actor thread' in
    let s' = { s with mem = mem'; threads = threads' } in
    return s'
  )

let terminate_process_statement_computation_redacted
  (actor: tid_t)
  (nd: nondeterminism_t)
  (start_pc: pc_t)
  (method_id: method_id_t)
  (s: Armada.State.t)
  : GTot (conditional_computation_t Armada.State.t) =
  let thread = s.threads actor in
  if   Cons? nd
     || neqb thread.stack []
     || thread.top.method_id <> method_id
     || actor <> s.initial_tid then // the process is terminated by having the initial thread terminate
    ComputationImpossible
  else
    let s' = { s with stop_reason = StopReasonTerminated } in
    return s'
/
Util.List.fst.checked Spec.Ubool.fst.checked Spec.Map.fst.checked Spec.List.fst.checked prims.fst.checked FStar.Tactics.V2.fst.checked FStar.Tactics.Effect.fsti.checked FStar.Sequence.Base.fsti.checked FStar.Pervasives.fsti.checked Armada.UnaryOp.fst.checked Armada.Type.fst.checked Armada.Thread.fst.checked Armada.Statement.fst.checked Armada.State.fst.checked Armada.Pointer.fst.checked Armada.Memory.fst.checked Armada.Init.fst.checked Armada.Expression.fst.checked Armada.Computation.fst.checked Armada.BoundedInt.fst.checked Armada.BinaryOp.fst.checked Armada.Base.fst.checked
Strategies.ArmadaStatement.Opaque.fst

    actor: Armada.Base.tid_t ->
    nd: Armada.Type.nondeterminism_t ->
    start_pc: Armada.Base.pc_t ->
    join_tid: Armada.Expression.expression_t ->
    s: Armada.State.t
  -> Prims.GTot (Armada.Computation.conditional_computation_t Armada.State.t)
Armada.Base.tid_t Armada.Type.nondeterminism_t Armada.Base.pc_t Armada.Expression.expression_t Armada.State.t Prims.op_BarBar Prims.uu___is_Cons Armada.Type.object_value_t Spec.Ubool.neqb Armada.Type.object_td_t Armada.Expression.expression_to_td Armada.Type.ObjectTDPrimitive Armada.Type.PrimitiveTDThreadId Armada.Computation.ComputationImpossible Prims.bool Armada.Computation.op_let_Question Armada.Type.valid_object_value_t Strategies.ArmadaStatement.Opaque.rvalue_computation_opaque Armada.Thread.__proj__Mkt__item__status Armada.Computation.ComputationUndefined Armada.Computation.return Armada.State.Mkt Armada.State.__proj__Mkt__item__initial_tid Armada.State.__proj__Mkt__item__uniqs_used Armada.State.__proj__Mkt__item__mem Armada.State.__proj__Mkt__item__trace Armada.State.__proj__Mkt__item__stop_reason Spec.Map.t Armada.Thread.t Spec.Map.upd Armada.State.__proj__Mkt__item__threads Armada.Thread.Mkt Armada.Thread.ThreadStatusPostJoin Armada.Thread.__proj__Mkt__item__pc Armada.Thread.__proj__Mkt__item__top Armada.Thread.__proj__Mkt__item__stack Armada.Thread.__proj__Mkt__item__write_buffer Armada.Thread.__proj__Mkt__item__position_in_other_write_buffers Armada.Computation.conditional_computation_t Armada.Type.__proj__PrimitiveBoxThreadId__item__tid Armada.Type.__proj__ObjectValuePrimitive__item__value
let join_statement_computation_redacted
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (join_tid: expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t) =
  
if Cons? nd || neqb (expression_to_td join_tid) (ObjectTDPrimitive PrimitiveTDThreadId)
then ComputationImpossible
else
  (let? tid_value = rvalue_computation_opaque join_tid actor s in
    let other_tid = PrimitiveBoxThreadId?.tid (ObjectValuePrimitive?.value tid_value) in
    let thread = s.threads other_tid in
    match thread.status with
    | ThreadStatusNotStarted -> ComputationImpossible
    | ThreadStatusRunning -> ComputationImpossible
    | ThreadStatusPostJoin -> ComputationUndefined
    | ThreadStatusJoinable ->
      let thread' = { thread with status = ThreadStatusPostJoin } in
      let threads' = Spec.Map.upd s.threads other_tid thread' in
      let s' = { s with threads = threads' } in
      return s')