Extract package:sbv

Given a machine state, compute a value out of it

Monads which support IO operations and can extract all IO behavior for interoperation with functions like catches, which takes an IO action in negative position. This function can not be implemented for transformers like ReaderT r or StateT s, whose resultant IO actions are a function of some environment or state.

A simpler variant of getModelAssignment to get a model out without the fuss.

Return all the models from an allSat call, similar to extractModel but is suitable for the case of multiple results.

Law: the m a yielded by IO is pure with respect to IO.

Grab the program from a running symbolic simulation state.

Prove that extraction and depositing with the same mask restore the source in all masked positions:

>>> extractThenDeposit
Q.E.D.

Extract the final key for on-the-fly decryption. This will extract exactly the number of blocks we need.

Extract the extended key for on-the-fly decryption. This will extract 4-blocks for 128-bit decryption, but 256 bit for both 192 and 256-bit variants

Extract a portion of bits to form a smaller bit-vector.

>>> prove $ \x -> bvExtract (Proxy @7) (Proxy @3) (x :: SWord 12) .== bvDrop (Proxy @4) (bvTake (Proxy @9) x)
Q.E.D.

Variant of sTestBit, where we want to extract multiple bit positions.

Extract bit-sequences.

Extract a portion of bits to form a smaller bit-vector.

Prove that depositing and extracting with the same mask will push preserve the bottom n-bits of the source, where n is the number of bits set in the mask.

>>> depositThenExtract
Q.E.D.

Demonstrates use of programmatic model extraction. When programming with SBV, we typically use sat/allSat calls to compute models automatically. In more advanced uses, however, the user might want to use programmable extraction features to do fancier programming. We demonstrate some of these utilities here.