Hi Xavier, and Gabriel,
Thank you very much for reply. Let me give me general understanding of my
project. I am trying to count encrypted ballots (Additive Elgamal) which is
matrix of ciphertext. We multiply these ballots (matrices) point wise and
decrypt it to get additive final value in plaintext [2]. For encryption,
decryption and zero knowledge proof, we are using unicrypt library [3]. You
can see the encryption part in Coq as Axiom [4] and will be realized by
java functions from unicrypt library in extracted OCaml code [5].  We will
replace the Z [6] with big_int in OCaml.

I am also wondering if these things (unicrypt functionality of encryption,
decryption and zero knowledge proof) can be realized by CertiCrypt [7] ?

Best regards,
Mukesh Tiwari


[1]
https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/ballot_mat.txt
[2] https://nvotes.com/multiplicative-vs-additive-homomorphic-elgamal/
[3] https://github.com/bfh-evg/unicrypt
[4]
https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/EncryptionSchulze.v#L713
[5]
https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/lib.ml
[6]
https://github.com/mukeshtiwari/EncryptionSchulze/blob/master/code/lib.ml#L74
[7] https://github.com/EasyCrypt

On Fri, Apr 13, 2018 at 4:57 AM, forum@x9c.fr <forum@x9c.fr> wrote:

>
> Le 12 avr. 2018 à 10:40, mukesh tiwari <mukeshtiwari.iiitm@gmail.com> a
> écrit :
>
> Hi Everyone,
> I am trying to call some Java functions from OCaml (Extracted from Coq if
> it matters). I am familiar with ocamljava [1], but it says that "*The
> generated code usually runs faster than OCaml bytecode but slower than
> native code. Memory consumption and startup time are also higher, but
> leveraging the multiple cores of a machine can help reaching the
> performance level of native code.*", and I don't want to leave the OCaml
> native code. One suggestion I got on #ocaml channel is using RPC and a
> quick Google search leads to ocaml-rpc [2].  I am wondering if experts from
> OCaml community could please give me some suggestions.
>
>
> For the record, the performance of ocamljava-compiled code
> heavily depends on the programming style. Numerical imperative
> or i/o-bound code can be on par with ocamlopt-compiled code,
> while code based on exceptions for control flow or abundant indirect
> calls can be slower than ocamlc-compiled code. I am afraid
> extracted code is likely to fall in the second category.
>
> It is also noteworthy that you can run into problems with extracted
> code. I suspect extracted code might contain call to "Obj.magic",
> as the type system of Coq is slightly more powerful than the one
> of OCaml. The issue is that that OCaml-Java uses a different
> memory layout, so that "Obj.magic" might not yield the same result
> as in vanilla OCaml.
>
>
> Best regards,
>
> Xavier Clerc
>
> PS: if you are able to share your code, I might be able to give you
> a less generic assessment.
>

-- 
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs