Some of the code in this directory is generated by Fiat and thus these files are licensed under the MIT license. (See LICENSE file.)