The Coq mailing list

[Li-yao Xia <lysxia AT gmail.com>]

Hi Mukesh,

Extraction has commands to explicitly define how a given identifier gets 
extracted. For example, you can define a module of axioms for extraction 
looking like this:


Module KeyInstance <: Keys.
Parameter Prime : Type.
Parameter prime : Prime.

Extract Constant prime => "(* OCaml code here *)".
(* etc. *)
(* Might need to extract types too, I don't remember offhand. *)
End KeyInstance.


Cheers,
Li-yao

On 5/30/19 3:50 AM, mukesh tiwari wrote:
> 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