val mark_allocation_root_allocated_opaque : uniq: Armada.Base.root_id_uniquifier_t ->
    storage: Armada.Memory.valid_object_storage_t ->
    s: Armada.State.t
  -> Prims.GTot Armada.State.t
let mark_allocation_root_allocated_opaque = mark_allocation_root_allocated
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
/
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

    uniq: Armada.Base.root_id_uniquifier_t ->
    storage: Armada.Memory.valid_object_storage_t ->
    s: Armada.State.t
  -> Prims.GTot Armada.State.t
Armada.Statement.mark_allocation_root_allocated
let mark_allocation_root_allocated_opaque =
  
mark_allocation_root_allocated