/**CFile**************************************************************** FileName [bmc.h] SystemName [ABC: Logic synthesis and verification system.] PackageName [SAT-based bounded model checking.] Synopsis [External declarations.] Author [Alan Mishchenko] Affiliation [UC Berkeley] Date [Ver. 1.0. Started - June 20, 2005.] Revision [$Id: bmc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $] ***********************************************************************/ #ifndef ABC___sat_bmc_BMC_h #define ABC___sat_bmc_BMC_h //////////////////////////////////////////////////////////////////////// /// INCLUDES /// //////////////////////////////////////////////////////////////////////// #include "aig/saig/saig.h" #include "aig/gia/gia.h" //////////////////////////////////////////////////////////////////////// /// PARAMETERS /// //////////////////////////////////////////////////////////////////////// ABC_NAMESPACE_HEADER_START //////////////////////////////////////////////////////////////////////// /// BASIC TYPES /// //////////////////////////////////////////////////////////////////////// // unrolling manager typedef struct Unr_Man_t_ Unr_Man_t; typedef struct Saig_ParBmc_t_ Saig_ParBmc_t; struct Saig_ParBmc_t_ { int nStart; // starting timeframe int nFramesMax; // maximum number of timeframes int nConfLimit; // maximum number of conflicts at a node int nConfLimitJump; // maximum number of conflicts after jumping int nFramesJump; // the number of tiemframes to jump int nTimeOut; // approximate timeout in seconds int nTimeOutGap; // approximate timeout in seconds since the last change int nTimeOutOne; // timeout per output in multi-output solving int nPisAbstract; // the number of PIs to abstract int fSolveAll; // does not stop at the first SAT output int fStoreCex; // enable storing CEXes in the MO mode int fUseBridge; // use bridge interface int fDropSatOuts; // replace sat outputs by constant 0 int nFfToAddMax; // max number of flops to add during CBA int fSkipRand; // skip random decisions int fNoRestarts; // disables periodic restarts int nLearnedStart; // starting learned clause limit int nLearnedDelta; // delta of learned clause limit int nLearnedPerce; // ratio of learned clause limit int fVerbose; // verbose int fNotVerbose; // skip line-by-line print-out char * pLogFileName; // log file name int fSilent; // completely silent int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs int nDropOuts; // the number of dropped outputs abctime timeLastSolved; // the time when the last output was solved int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode }; typedef struct Bmc_AndPar_t_ Bmc_AndPar_t; struct Bmc_AndPar_t_ { int nStart; // starting timeframe int nFramesMax; // maximum number of timeframes int nFramesAdd; // the number of additional frames int nConfLimit; // maximum number of conflicts at a node int nTimeOut; // timeout in seconds int nLutSize; // LUT size for cut computation int fLoadCnf; // dynamic CNF loading int fDumpFrames; // dump unrolled timeframes int fUseSynth; // use synthesis int fUseOldCnf; // use old CNF construction int fVerbose; // verbose int fVeryVerbose; // very verbose int fNotVerbose; // skip line-by-line print-out int iFrame; // explored up to this frame int nFailOuts; // the number of failed outputs int nDropOuts; // the number of dropped outputs }; typedef struct Bmc_BCorePar_t_ Bmc_BCorePar_t; struct Bmc_BCorePar_t_ { int iFrame; // timeframe int iOutput; // property output int nTimeOut; // timeout in seconds char * pFilePivots; // file name with AIG IDs of pivot objects char * pFileProof; // file name to write the resulting proof int fVerbose; // verbose output }; typedef struct Bmc_MulPar_t_ Bmc_MulPar_t; struct Bmc_MulPar_t_ { int TimeOutGlo; int TimeOutLoc; int TimeOutInc; int TimeOutGap; int TimePerOut; int fUseSyn; int fDumpFinal; int fVerbose; int fVeryVerbose; }; typedef struct Bmc_ParFf_t_ Bmc_ParFf_t; struct Bmc_ParFf_t_ { char * pFileName; char * pFormStr; int Algo; int fComplVars; int fStartPats; int nTimeOut; int nIterCheck; int nCardConstr; int fNonStrict; int fBasic; int fFfOnly
.. hazmat::

.. module:: cryptography.hazmat.primitives.keywrap

Key wrapping
============

Key wrapping is a cryptographic construct that uses symmetric encryption to
encapsulate key material. Key wrapping algorithms are occasionally utilized
to protect keys at rest or transmit them over insecure networks. Many of the
protections offered by key wrapping are also offered by using authenticated
:doc:`symmetric encryption </hazmat/primitives/symmetric-encryption>`.

.. function:: aes_key_wrap(wrapping_key, key_to_wrap, backend)

    .. versionadded:: 1.1

    This function performs AES key wrap (without padding) as specified in
    :rfc:`3394`.

    :param bytes wrapping_key: The wrapping key.

    :param bytes key_to_wrap: The key to wrap.

    :param backend: A
        :class:`~cryptography.hazmat.backends.interfaces.CipherBackend`
        provider that supports
        :class:`~cryptography.hazmat.primitives.ciphers.algorithms.AES`.

    :return bytes: The wrapped key as bytes.

.. function:: aes_key_unwrap(wrapping_key, wrapped_key, backend)

    .. versionadded:: 1.1

    This function performs AES key unwrap (without padding) as specified in
    :rfc:`3394`.

    :param bytes wrapping_key: The wrapping key.

    :param bytes wrapped_key: The wrapped key.

    :param backend: A
        :class:`~cryptography.hazmat.backends.interfaces.CipherBackend`
        provider that supports
        :class:`~cryptography.hazmat.primitives.ciphers.algorithms.AES`.

    :return bytes: The unwrapped key as bytes.

    :raises cryptography.hazmat.primitives.keywrap.InvalidUnwrap: This is
        raised if the key is not successfully unwrapped.

Exceptions
~~~~~~~~~~

.. class:: InvalidUnwrap

    This is raised when a wrapped key fails to unwrap. It can be caused by a
    corrupted or invalid wrapped key or an invalid wrapping key.
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-05 11:25:26 +0000