val compare_and_swap_statement_computation_redacted
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (target old_val new_val: expression_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
val compare_and_swap_statement_computation_redacted
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (target old_val new_val: expression_t)
      (bypassing_write_buffer: bool)
      (optional_result: option expression_t)
      (s: Armada.State.t)
    : GTot (conditional_computation_t Armada.State.t)
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'
  )
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'; })
/
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 ->
    target: Armada.Expression.expression_t ->
    old_val: Armada.Expression.expression_t ->
    new_val: Armada.Expression.expression_t ->
    bypassing_write_buffer: Prims.bool ->
    optional_result: FStar.Pervasives.Native.option 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 Prims.bool FStar.Pervasives.Native.option 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.PrimitiveTDBool Armada.Computation.ComputationImpossible Armada.Computation.op_let_Question Prims.unit Strategies.ArmadaStatement.Opaque.check_expression_up_to_date_for_rmw_opaque Armada.Type.valid_object_value_t Strategies.ArmadaStatement.Opaque.rvalue_computation_opaque Armada.Pointer.t Armada.Expression.lvalue_computation Strategies.ArmadaStatement.Opaque.update_pointed_to_value_opaque Armada.Computation.return Armada.Computation.conditional_computation_t Armada.Type.ObjectValuePrimitive Armada.Type.PrimitiveBoxBool Spec.Ubool.eqb Prims.l_or Prims.l_and Prims.b2t Armada.Type.object_value_valid Prims.eq2 Armada.Type.object_value_to_td
let compare_and_swap_statement_computation_redacted
      (actor: tid_t)
      (nd: nondeterminism_t)
      (start_pc: pc_t)
      (target old_val 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 ->
      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')