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.
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.
-
ocaml. Tested with version 4.14.1. (But other versions should work too).
-
ocamlbuild. Tested with 0.14.2. (But other versions should work too).
-
coq. Tested with versions 8.16.1.
After cloning, just change directory for a building directory (see below), and run make.
coq_src/ contains the Coq sources. Other directories aims to build examples of binaries.
-
FixTypeSafety/ builds an executable from coq_src/FixTypeSafety.v. It first provides an example from David Monniaux illustrating that linking Coq extracted and OCaml code without caution may break type-safety. Then, it illustrates how this example cannot break type-safety by wrapping the OCaml code within the Impure monad.
-
FibExample/ builds an executable from coq_src/FibExample.v. It illustrates the use of ImpLoops in order to certify in Coq the memoized fixpoint of the naive recursive definition of Fibonacci's function.
-
CanonNatExample/ builds an executable from coq_src/CanonNatExample.v. It illustrates the use of ImpHCons in order to define in Coq hash-consed Peano's numbers.
-
BasicImpExample/ builds an executable from coq_src/BasicImpExample.v. It explores basic features/limitations of the Impure library.