val 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)
val 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)
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
  )
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
/
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 ->
    exp: 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.ObjectTDAbstract Prims.bool Armada.Computation.ComputationImpossible Armada.Computation.op_let_Question Armada.Type.valid_object_value_t Strategies.ArmadaStatement.Opaque.rvalue_computation_opaque Prims.op_disEquality Armada.Type.__proj__ObjectValueAbstract__item__ty Armada.Type.__proj__ObjectValueAbstract__item__value Armada.Computation.return Armada.Computation.conditional_computation_t
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)