Is it possible to generate a reference implementation code from specs (say, in Qiskit or Q#) ?

[zeta1999]

(alternatively, can we extract basic qbricks specs - without proof! - from some Qiskit/Q# etc. code ?)

[Qbricks]

Hi,

And thank you for your interest in our work.

We don't have these features so far...

=> generating ref implem : a naive way consists in generating a classical computing circuit and then turn it reversible to feed the quantum machine --> the challenge then is not to get an implem but to get a good one, which is quite orthogonal to our scope, and NP-complete as far I Know

=> automatically extracting spec for code. Again there is a naive trivial way that we implemented and used internally. But the spec is in hardly directly exploitable form. Then all the game is to transform it toward some kind of a normal form, to make it readable against natural language specifications

[zeta1999]

Dear all, an extra question. I tried to extract the circuit from the Shor example, from within the Docker env [btw I updated libexpat version in the Docker to "u5" due to some uninteresting Debian "non breaking update"].
I add this function to show_circuit.mlw
let function shor_circ_15: circuit
= shor_circ 0 15 4
Then I try the following

why3 execute -L ../Qbricks/ -L ../math_libs/ -L . show_circuit.mlw 'Shor.shor_circ_15'
It stops with:
anomaly: File "src.mlw/pinterp.ml", line 495, characters 4-10: Assertion failed
Is there a "simple" way to export a circuit instance? I could be interested in debugging things if need be but first I would like to know if there is any fundamental roadblock to this extraction - I am not experienced with why3, although I spent some time being paid to do Haskell so I am pretty sure some of the things I am trying to do are naive ~
I also tried to export mlw code to ml/caml to no success
Ideally I would like to try to get the "circuit" and then feed it into a variety of quantum computing compilers, somehow figuring out the gates, init vectors and measures from the data structure.

[Qbricks]

Hi,

and thank you again for your interest!

About your question : first thing to have in mind is that, at the present state of development, Qbricks does not hold measurement but strictly unitary circuits, together with static analysis.

And, second, we are finalizing a release for the whole code featuring, among others, an output as Oqasm 2.0 code. I guess this will reach your needs?

[zeta1999]

And, second, we are finalizing a release for the whole code featuring,

among others, an output as Oqasm 2.0 code. I guess this will reach your needs? Yes this is perfect ;-) RB

…

On Fri, Oct 21, 2022 at 8:25 PM Qbricks ***@***.***> wrote: Hi, and thank you again for your interest! About your question : first thing to have in mind is that, at the present state of development, Qbricks does not hold measurement but strictly unitary circuits, together with static analysis. And, second, we are finalizing a release for the whole code featuring, among others, an output as Oqasm 2.0 code. I guess this will reach your needs? — Reply to this email directly, view it on GitHub <#3 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AAWZ6FX7A5GOAI5W3CJKRLTWEJ4R7ANCNFSM6AAAAAAQ25HZBY> . You are receiving this because you authored the thread.Message ID: ***@***.***>