coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Extracting Coq function into OCaml function

From: mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>
To: coq-club AT inria.fr
Subject: [Coq-Club] Extracting Coq function into OCaml function
Date: Thu, 30 May 2019 17:50:49 +1000
Authentication-results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=mukeshtiwari.iiitm AT gmail.com; spf=Pass smtp.mailfrom=mukeshtiwari.iiitm AT gmail.com; spf=None smtp.helo=postmaster AT mail-it1-f193.google.com
Ironport-phdr: 9a23:xC6KfhQc17PVMevQFUhmX7l9Fdpsv+yvbD5Q0YIujvd0So/mwa69bRWN2/xhgRfzUJnB7Loc0qyK6vmmADZQqs/b6TgrS99lb1c9k8IYnggtUoauKHbQC7rUVRE8B9lIT1R//nu2YgB/Ecf6YEDO8DXptWZBUhrwOhBoKevrB4Xck9q41/yo+53Ufg5EmCexbal9IRmrsAndrNQajZVhJ6o+1xfFvGZEcPlKyG11Il6egwzy7dqq8p559CRQtfMh98peXqj/Yq81U79WAik4Pm4s/MHkugXNQgWJ5nsHT2UZiQFIDBTf7BH7RZj+rC33vfdg1SaAPM32Sbc0WSm+76puVRTlhjsLOyI//WrKjMF7kaBVrw+7pxFnzIHaYI+bOvljcK3DYdwXXnZBUtpLWiBdHo+wc4kCAuwcNuhYtYn9oF4OoAO7BQmxB+Pg1CRIhn/r1q0m0uQgHxvJ3BYhH9kTt3nUqcj1NKQMXuCuzKnI0TTDbv1M1jfn6YjEaBEhofCNXbJsdMrc0kYvFwbfgVWRrYzpJS+a1uMIs2WC6edrSOyhi2kiqw5rozivwN8hiobIhoIJylDE6D52zJwpKt2/TU52Z8OvHphItyyCKYd6XscvT3trtSs60LEKpJ+2cSkQxJg6wxPSZfqKeJWS7B35TuaeOzJ4iWpleL2hgxay9lCtyujmWcm11FZGtytFksXRunwU2Rzf98yKR/Vn8keu3jaP0A/T6uVaLkwuiaXbLJshzqYxlpoVr0vDAjf7lFvqgKKSbEkp+eil5/76brjnp5KQLZJ4hwXwP6g2n8ywG+U4MgwAX2iB/uS80aXu/UjkQLVJkPI2ianZsIzbJcUVvKG5GQ5V3pwi6xa+DjemzNEYkGIILFJAYh2HjozpN0vSL/D/CPezm06snytzx/DaIr3hBY3AIWTEkLf4ZLpy90pcyBcowt1E/JJVCrQBIOrpVUPrtdzYCAU5Mw2uzOr9BtV9zNBWZWXaCaiAdajWrFWg5+Q1IuDKapVGliz6Lq0g+v3jln9xhV4CdLOolc8SdXO1BfR6IlqQe3uqg9YADWIisQ83Teisg1qHB20AL02uVr4xs2loQLmtCp3OE9j03O6xmRyjF5gTXVhoT0iWGC6xJYqBUvYILimVJ505y2FWZf2aU4YkkCqWmkr6xr5gdLSG/yQZsdfiyIEw6bSCzlc98jt7C8nb2GaIHTktzzE4AgQu1aU6mnRTj1KK0Kx2mftdTIUB6PZAUwN8PpnZnbV3

Hi Everyone,
I am trying to extract a Coq function [1] into OCaml function. I
understand that I need to pass a instance of Cand, Keys and
CryptoAxioms to Encschulze module to extract this function. Something
like this ? [2]

Module CandInstance <: Cand.
(* Definition and proof obligation *)
End CandInstance.

Module KeyInstance <: Keys.
(* Crypto Parameters *)
End KeyInstance.

Module CryptoAxiomInstance <: CryptoAxioms CandInstance KeyInstance.
(* Definition and proofs *)
End CryptoAxiomInstance.

Module E := Encschulze CandInstance KeyInstance CryptoAxiomInstance.

Extraction Language Ocaml.
Extraction "lib.ml" E.pschulze_winners.

My problem is, I can not produce instance of Keys and CryptoAxioms,
because we have taken them as axioms. The values and functions inside
these modules will be instantiated by external OCaml code [3] which is
a wrapper of cryptographic library unicrypt [4].

My question is, how can I extract the pshulze_winners function without
giving the instance of Keys and CryptoAxoims ? One potential solution
I can think of is giving some dummy values and admitting all the
proofs in Keys and CryptoAxioms module to create a instance to
facilitate the extraction. After extraction change all the values in
extracted code, but I am wondering if there is any better solution
than this.

(* Feel free to skip the paragraph *)
I have a working repo of this project [5], but it's very messy. The
reason this repo is working is that the whole development is in single
file, and all the cryptographic values and functions are lambda
abstracted [6] during the extraction.

Best regards,
Mukesh Tiwari

[1]
https://github.com/mukeshtiwari/Encschulze_module/blob/master/Encryptionschulze.v#L492
[2]
https://github.com/mukeshtiwari/Encschulze_module/blob/master/Instance.v#L37
3]
https://github.com/mukeshtiwari/Encschulze_module/blob/master/cryptobinding.ml
[4] https://github.com/bfh-evg/unicrypt/
[5]
https://github.com/mukeshtiwari/EncryptionSchulze/tree/master/code/Workingcode
[6]
https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/Workingcode/main.ml#L45

[Coq-Club] Extracting Coq function into OCaml function, mukesh tiwari, 05/30/2019
- Re: [Coq-Club] Extracting Coq function into OCaml function, Li-yao Xia, 05/30/2019
  - Re: [Coq-Club] Extracting Coq function into OCaml function, mukesh tiwari, 05/31/2019