1 files changed, 50 insertions, 0 deletions
diff --git a/content/zettel/3b6.md b/content/zettel/3b6.md
new file mode 100644
index 0000000..18e4874
--- /dev/null
+++ b/content/zettel/3b6.md
@@ -0,0 +1,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