The Coq mailing list

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

Hi Li-yao, and everyone,

I managed to extract OCaml code from Coq code, but I believe
extracting Coq type to OCaml polymorphic types [1] in my case is
causing compiler error

File "Top.ml", line 79, characters 20-31:
Error: Unbound type parameter 'ciphertext

A quick Google search led me to [2], but I am not sure how to simulate
Andreas Rossberg's solution in my extraction. Any hint or suggestion
would be appreciated.

Best,
Mukesh

[1] 
https://github.com/mukeshtiwari/Encschulze_module/blob/master/Instance.v#L64
[2] 
https://stackoverflow.com/questions/8869678/polymorphic-type-inside-a-module-ocaml

On Fri, May 31, 2019 at 11:12 AM mukesh tiwari
<mukeshtiwari.iiitm AT gmail.com>
 wrote:
>
> 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
> > >