blob: 18e4874242209c25d6b472fe62d35685184c0c06 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
|
+++
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
|
