1  == Proven Delights
  2  
  3  This project aims to include templated C++ implementations of many of the
  4  algorithms from http://www.hackersdelight.org/[Hacker's Delight], alongside
  5  http://www.cprover.org/cbmc/[CBMC]  proofs of the implementations.  While the
  6  implementations are typically trivial, that they work at all is often
  7  nonobvious.  Proofs can show that they work for all input values.
  8  
  9  The fully built documentation of a recent version can always be found online:
 10  http://jepler.github.io/ProvenDelights/
 11  
 12  === Structure
 13  ==== The proofs/ directory
 14  Each file in proofs/ is an asciidoc document.  It must contain a code section
 15  lead off by ".Implementation" which implements the function as a C++ template
 16  or inline; and a code section lead off by ".Proof" which implements a CBMC
 17  proof of the function's properties as given in Hacker's Delight.
 18  
 19  Where an implementation or proof needs to use the implementation of another
 20  function, it can #include the definition.  For example, to use the
 21  implementation of `turn_off_rightmost_ones`, simply
 22  ----
 23  #include "turn_off_rightmost_ones.h"
 24  ----
 25  
 26  ==== The structure/ directory
 27  The asciidoc files in this directory create a structure which is intended to
 28  mirror the chapter and section numbering of Hacker's Delight (second edition).
 29  To this end, it will initially contain many empty and placeholder sections.
 30  
 31  Where appropriate, chapter and section titles the same as those in
 32  Hacker's Delight are used for the purpose of identifying the
 33  correspondence between the book and this body of proofs.
 34  
 35  ==== The include/ directory
 36  This directory holds utility code to be used in proofs, such as +assume+,
 37  +assert+, and +proof_popcnt+.
 38  
 39  ==== The gen-include/ directory
 40  This directory holds the generated header files for each function
 41  implemented.
 42  
 43  ==== The docs/ directory
 44  This directory holds the generated documentation, "proofs.html" and
 45  "proofs.pdf"
 46  
 47  === Compatibility and software versions
 48  At this time, the oldest supported environment is Debian Buster.  Generally,
 49  the oldest supported environment will be Debian stable or oldstable.
 50  
 51  This means that the minimum versions of relevant software are:
 52  
 53  * http://asciidoc.org/[asciidoc 8.6.10]
 54  * http://www.cprover.org/cbmc/[cbmc 5.10]
 55  * http://python.org[python 3.7.3]
 56  
 57  === Building
 58  The software is built by invoking +make+ in the top-level directory.
 59  By default, all functions are proven and all forms of documentation are
 60  built.  Parallelism can be used safely (+make -j4+ for a 4-thread system, for
 61  instance)
 62  
 63  Other targets include +docs+, +pdf+, and +html+ to build just (one form of)
 64  the documentation; +proofs+ to just build the proofs, and +prove-**foo**+
 65  to just prove *foo*.
 66  
 67  In the case of a successful proof, the output of CBMC is left in
 68  +.o/**foo**_proof.txt+.  In the case of a failed proof, it is left in
 69  +.o/**foo**_proof.txt.err+.
 70  
 71  === Contributing
 72  Submit contributions with github pull requests to https://github.com/jepler/ProvenDelights[].
 73  Your contributions are subject to the https://help.github.com/articles/github-terms-of-service/#6-contributions-under-repository-license[GitHub Terms of Service] and must therefore be offered under the Repository License, stated below.
 74  
 75  Respect http://www.hackersdelight.org/permissions.htm[the license
 76  of the Hacker's Delight book].  This means that code may be
 77  incorporated from the book, but prose may not.
 78  
 79  === Style
 80  For prose, use professional English writing.
 81  
 82  For code, use basic C++; make functions templates where appropriate,
 83  and inlines where inappropriate.  Use the general coding style of
 84  Hacker's Delight:
 85  
 86  * 4-space indentation
 87  * no literal tab characters
 88  * open curly braces don't get their own line
 89  * include whitespace in expressions where it improves readability
 90  
 91  === License
 92  This work is licensed under a
 93  http://creativecommons.org/licenses/by-sa/4.0/[Creative Commons
 94  Attribution-ShareAlike 4.0 International License.]
 95  
 96  Additionally, all blocks of code marked as ".Implementation" are also covered
 97  under the following license (commonly known as the "zlib license"):
 98  
 99  This software is provided 'as-is', without any express or implied
100  warranty. In no event will the authors be held liable for any damages
101  arising from the use of this software.
102  
103  Permission is granted to anyone to use this software for any purpose,
104  including commercial applications, and to alter it and redistribute it
105  freely, subject to the following restrictions:
106  
107  1. The origin of this software must not be misrepresented; you must not
108     claim that you wrote the original software. If you use this software
109     in a product, an acknowledgement in the product documentation would be
110     appreciated but is not required.
111  2. Altered source versions must be plainly marked as such, and must not be
112     misrepresented as being the original software.
113  3. This notice may not be removed or altered from any source distribution.