Skip to main content

Browse the archive

Revision 2f522b73a954cba616a062069b5b130814f77b8b authored by Nikhil Swamy on 09 April 2019, 01:03:16 UTC, committed by Nikhil Swamy on 09 April 2019, 01:03:16 UTC 
fixing a proof after updating validity axioms (similar proofs failed before for other unrelated reasons)
1 parent 0c01c78
Raw File
CODE.md 
The following directories contain Vale and F\* sources:

* [specs](./specs): Trusted specification files that cover [basic definitions](./specs/defs/),
                    [math](./specs/defs/), [cryptographic algorithms](./specs/crypto/),
                    and [hardware assumptions](./specs/hardware/)
* [code](./code): Verified F\* support libraries and verified Vale cryptographic code
    * [arch](./code/arch): Optimized libraries for reasoning about hardware operations
    * [crypto](./code/crypto): verified cryptographic code
    * [test](./code/test): test files 
    * [thirdPartyPorts](./code/thirdPartyPorts): Code ported into Vale from external sources

Building will create the following additional directories;
all files generated by the build should be in these directories:

* obj
* bin
back to top