val rvalue_computation_opaque : exp: Armada.Expression.expression_t -> actor: Armada.Base.tid_t -> s: Armada.State.t
  -> Prims.GTot
    (Armada.Computation.conditional_computation_t (Armada.Type.valid_object_value_t (Armada.Expression.expression_to_td
                exp)))
let rvalue_computation_opaque = rvalue_computation
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
/
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
exp: Armada.Expression.expression_t -> actor: Armada.Base.tid_t -> s: Armada.State.t
  -> Prims.GTot
    (Armada.Computation.conditional_computation_t (Armada.Type.valid_object_value_t (Armada.Expression.expression_to_td
                exp)))
Armada.Expression.rvalue_computation
let rvalue_computation_opaque =
  
rvalue_computation