Require Import monad.proofs.exec_specs.
Require Import monad.asts.ext.
Require Import monad.asts.storage_page_cpp.
Require Import monad.proofs.libspecs.optional_specs.
Require Import Lens.Lens.

Section with_Sigma.
  Context `{Sigma:cpp_logic} {CU: genv} {hh: HasOwn mpredI fracR}.
  Context {hf: fracG () _Σ}.
  Context {MODd : ext.module ⊧ CU}.



















Definition SpecFor_optional_u256_ctor_rv :=
  RegisterSpec (optional_specs.optional_ctor_rv_spec u256t u256R).
#[global] Existing Instance SpecFor_optional_u256_ctor_rv.

Definition SpecFor_optional_u256_ctor_const_rv :=
  RegisterSpec (optional_specs.optional_ctor_const_rv_spec u256t u256R).
#[global] Existing Instance SpecFor_optional_u256_ctor_const_rv.

Definition SpecFor_optional_u256_ctor_nullopt :=
  RegisterSpec (optional_specs.optional_ctor_nullopt_spec u256t u256R).
#[global] Existing Instance SpecFor_optional_u256_ctor_nullopt.

End with_Sigma.

#[global] Hint Opaque uint256_int_ctor_spec : sl_opacity.