Skip to content

A Coq library to embed Impure OCaml oracles in certified Coq code

License

Notifications You must be signed in to change notification settings

boulme/ImpureDemo

Folders and files

NameName
Last commit message
Last commit date

Latest commit

 

History

35 Commits
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 
 

Repository files navigation

ImpureDemo: importing OCaml functions as non-deterministic ones.

This repository contains a few demonstrations of using Impure library located here at coq_src/Impure/ as a git-subrepo.

The principle of the Impure library is to encode the type A -> B of an OCaml function as a type A -> ?? B in Coq, where ?? B is the type of an axiomatized monad that can be interpreted as B -> Prop. In other word, this encoding abstracts an OCaml function as a function returning a postcondition on its possible results (ie a relation between its parameter and its result). Side-effects are simply ignored. And reasoning on such a function is only possible in partial correctness.

A major feature of this cooperation between Coq and OCaml typechecker is to provide very simple parametric proofs about polymorphic OCaml functions. They correspond here to prove, by reasoning only on their type, that these functions preserve some invariants. As an example, we prove the partial correctness of a generic memoizing fixpoint operator: see rec_correct lemma at the end of ImpLoops. This lemma is applied in FibExample to prove the partial correctness of a memoized version of the naive Fibonacci function. However, currently, the soundness of these parametric proofs is still a conjecture. The Linking Types technique of Daniel Patterson, Andrew Wagner and Amal Ahmed (published as a TypeDe'2023 paper) could provide an approach to tackle it!

For more details, see this document.

Other Significant Use Cases

Impure/ is part of Chamois CompCert. An older version is used by satans-cert -- a certified checker of (Boolean) sat-solver answers. The ancester of Impure is also present in the Verified Polyhedra Library.

Credits

Sylvain Boulmé.

Installation

Requirements

  1. ocaml. Tested with version 4.14.1. (But other versions should work too).

  2. ocamlbuild. Tested with 0.14.2. (But other versions should work too).

  3. coq. Tested with versions 8.16.1.

Compilation

After cloning, just change directory for a building directory (see below), and run make.

Code Overview

coq_src/ contains the Coq sources. Other directories aims to build examples of binaries.

About

A Coq library to embed Impure OCaml oracles in certified Coq code

Topics

Resources

License

Stars

Watchers

Forks

Releases

No releases published

Packages

No packages published