comp package:sbv

Complement of regular expression

Given a symbolic computation, render it as an equivalent collection of files that make up a C program:

• The first argument is the directory name under which the files will be saved. To save files in the current directory pass Just ".". Use Nothing for printing to stdout.
• The second argument is the name of the C function to generate.
• The final argument is the function to be compiled.

Compilation will also generate a Makefile, a header file, and a driver (test) program, etc. As a result, we return whatever the code-gen function returns. Most uses should simply have () as the return type here, but the value can be useful if you want to chain the result of one compilation act to the next.

Create code to generate a library archive (.a) from given symbolic functions. Useful when generating code from multiple functions that work together as a library.

• The first argument is the directory name under which the files will be saved. To save files in the current directory pass Just ".". Use Nothing for printing to stdout.
• The second argument is the name of the archive to generate.
• The third argument is the list of functions to include, in the form of function-name/code pairs, similar to the second and third arguments of compileToC, except in a list.

Lower level version of compileToC, producing a CgPgmBundle

Lower level version of compileToCLib, producing a CgPgmBundle

Complement.

>>> empty .== complement (full :: SSet Integer)
True

Complementing twice gets us back the original set:

>>> prove $ \(s :: SSet Integer) -> complement (complement s) .== s
Q.E.D.

Ordering for floats, avoiding the +0-0NaN issues. Note that this is essentially used for indexing into a map, so we need to be total. Thus, the order we pick is: NaN -oo -0 +0 +oo The placement of NaN here is questionable, but immaterial.

Inverse transformation to sFloatAsComparableSWord32. Note that this isn't a perfect inverse, since -0 maps to 0 and back to 0. Otherwise, it's faithful:

>>> prove  $ \x -> let f = sComparableSWord32AsSFloat x in fpIsNaN f .|| fpIsNegativeZero f .|| sFloatAsComparableSWord32 f .== x
Q.E.D.

>>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWord32AsSFloat (sFloatAsComparableSWord32 x) `fpIsEqualObject` x
Q.E.D.

Inverse transformation to sDoubleAsComparableSWord64. Note that this isn't a perfect inverse, since -0 maps to 0 and back to 0. Otherwise, it's faithful:

>>> prove  $ \x -> let d = sComparableSWord64AsSDouble x in fpIsNaN d .|| fpIsNegativeZero d .|| sDoubleAsComparableSWord64 d .== x
Q.E.D.

>>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWord64AsSDouble (sDoubleAsComparableSWord64 x) `fpIsEqualObject` x
Q.E.D.

Inverse transformation to sFloatingPointAsComparableSWord. Note that this isn't a perfect inverse, since -0 maps to 0 and back to 0. Otherwise, it's faithful:

>>> prove  $ \x -> let d :: SFPHalf = sComparableSWordAsSFloatingPoint x in fpIsNaN d .|| fpIsNegativeZero d .|| sFloatingPointAsComparableSWord d .== x
Q.E.D.

>>> prove $ \x -> fpIsNegativeZero x .|| sComparableSWordAsSFloatingPoint (sFloatingPointAsComparableSWord x) `fpIsEqualObject` (x :: SFPHalf)
Q.E.D.

Convert a double to a comparable SWord64. The trick is to ignore the sign of -0, and if it's a negative value flip all the bits, and otherwise only flip the sign bit. This is known as the lexicographic ordering on doubles and it works as long as you do not have a NaN.

Convert a float to a comparable SWord32. The trick is to ignore the sign of -0, and if it's a negative value flip all the bits, and otherwise only flip the sign bit. This is known as the lexicographic ordering on floats and it works as long as you do not have a NaN.

Convert a float to the correct size word, that can be used in lexicographic ordering. Used in optimization.

map f . map g == map (f . g)

>>> runTP $ mapCompose @Integer @Bool @String (uninterpret "f") (uninterpret "g")
Inductive lemma: mapCompose
Step: Base                            Q.E.D.
Step: 1                               Q.E.D.
Step: 2                               Q.E.D.
Step: 3                               Q.E.D.
Step: 4                               Q.E.D.
Step: 5                               Q.E.D.
Result:                               Q.E.D.
[Proven] mapCompose :: Ɐxs ∷ [Integer] → Bool

Components of the AES implementation that the library is generated from. For each case, we provide the driver values from the AES test-vectors.