The Coq mailing list

[mukesh tiwari <mukeshtiwari.iiitm AT gmail.com>]

Thanks Li-yao.  I will try it and see how it goes.

Best,
Mukesh

On Thu, May 30, 2019 at 8:33 PM Li-yao Xia 
<lysxia AT gmail.com>
 wrote:
>
> 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
> >