Skip to content
/ verith Public

A small coq library for verifying OCaml native integer computations

License

Notifications You must be signed in to change notification settings

MRandl/verith

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

29 Commits
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

Verith

Verith (VERIfied aRITHmetic) is a Coq library that proves several results about arithmetic on native integers. It enables users to write safe programs that make use of native integers without dealing with the complex, ceremonial and low-level manipulations usually required by the certification of such programs. Verith is intended to be used in combination with the extraction mechanism to help certifying programs in OCaml. It can also be used as is for regular Coq programs.

It has no dependencies other than the Coq standard library. While it does not assume controversial axioms, it is up to the user to extract correctly to maintain the guarantees of the library. Most notably, the underlying implementation of native integers must respect all axioms of U/Sint63. This usually means that you should only extract U- and SInt63 objects towards standard OCaml integers. You should also map their respective operations correctly.

License

This library is licensed under the MIT License. See the license for more details. The license takes precedence over any comment and/or description provided in this project.

Install

git clone [email protected]:MRandl/verith
cd verith
make

Note that this assumes coqc and coq-makefile to be accessible on PATH.

About

A small coq library for verifying OCaml native integer computations

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published