+++
title = "Unsoundness of Coq FFI"
author = "Yann Herklotz"
tags = []
categories = []
backlinks = ["3b6a", "3b5"]
forwardlinks = ["3a", "3b7", "3b6a"]
zettelid = "3b6"
+++

There are examples where reasoning about the Coq FFI by using the
`Parameter` declaration can actually result in unsoundness of the proof
\[1\]. This happens in CompCert ([\#3a]) quite a lot when something is
proven by translation validation. For example, in the following code
there are quite a few possibilities that could introduce unsoundness.

``` coq
Definition one: nat := (S O).
Axiom test: nat -> bool.
Extract Constant test => "oracle".

Lemma cong: test one = test (S O).
  auto.
Qed.
```

The first option which could introduce this unsoundness is that the
`cong` lemma might not hold if if equality is implemented using `==` in
Ocaml, which does equality on pointers.

Second, if one relies on the fact that $\forall x, f(x) = f(x)$, this
might not be true because the function might rely on external state and
therefore might not be pure.

<div id="refs" class="references csl-bib-body" markdown="1">

<div id="ref-boulmé19_embed_untrus_imper_ml_oracl" class="csl-entry"
markdown="1">

<span class="csl-left-margin">\[1\]
</span><span class="csl-right-inline">S. Boulmé and T. Vandendorpe,
“<span class="nocase">Embedding Untrusted Imperative ML Oracles into Coq
Verified Code</span>,” Jul. 2019. Available:
<https://hal.archives-ouvertes.fr/hal-02062288></span>

</div>

</div>

  [\#3a]: /zettel/3a