https://formal.land/blog/2024/05/22/translation-of-python-code-simulations-from-trace

[giscus[bot]]

https://formal.land/blog/2024/05/22/translation-of-python-code-simulations-from-trace

In order to formally verify Python code in Coq our approach is the following:

https://formal.land/blog/2024/05/22/translation-of-python-code-simulations-from-trace

[Sumayya-rizwan]

Dear Sir,
can you please explain me how to write simulation for the coq file created by coq-of-python tool. the coq file created by the tool is too complex and also of large size that understanding that and then writing simulation understanding the syntax of this tool will make this tool usability limited. isnt it?????
if there is any argumentation or papers regarding this tool and verification by this tool, kindly refer to me for more understanding.
thanks and regards
kindly reply me soon
i am very much interested in understanding of this tool and want to use it.

[clarus]

Hello,

Thanks for your interest in the coq-of-python tool! This is still a work in progress, as we are waiting for use cases that could fund the tool. Currently the development is on hold.

So the blog post is mainly to present the general idea, but the details should be refined with more experiments. We hope to verify some real examples at some point, what would offer a documentation by the example.

Best,
Guillaume

[Sumayya-rizwan]

i have gone through the websites but these websites are way too complex for the beginners. also they have not explained the steps for writing simulation, instead code is given which make it difficult to understand.

[Sumayya-rizwan]

Its an interesting project and i liked teh idea how you translated systematically python to coq with formatted output for understanding. but what i cant understand is that there are some limitations of this tool, correct me if i am wrong
Limitations of coq-of-python:
Don't support all python features: this tool do not support all Python features or constructs.
Expertise Requirements: Using coq-of-python effectively requires expertise in:
* Python
* Coq
* The coq-of-python tool itself
* Formal verification techniques
Complexity of Generated Code: The Coq code generated by this tool is complex and often hard to read. This is a significant drawback, as it makes understanding and working with the generated code challenging.
Need for Simulation: Writing a separate simulation (Coq specification) adds another layer of complexity and required expertise.
Verification Challenges: Verifying the complex generated code against a hand-written simulation is a also a challenging task that requires deep understanding of both the original Python code and Coq.
testcase challenges: The complexity and structure of the generated code make it challenging to write and run simple tests due to which we can't use compute or eval of coq directly.

What i wanted to understand,

1. why we cant verify directly in coq when it take less lines of code and less expertise?
2. what is motivating you to go through such complexity when we can verify with less complexity?
3. How can this tool be used without having expertise in tool, coq and python?
   thanks and regards

[clarus]

You are right with the limitations. To answer to your points:

1. If a project can be written from scratch in Coq it is simpler to verify it that way. With coq-of-python we want to address the case of verifying an existing code base that is already written in Python and cannot be rewritten in another language, for historical reasons or because Python developers need to understand the code.
2. So this is the answer above.
3. This tool requires expertise in both Python and Coq, and we do not think there is a way to go around that. Automated provers can simplify the work, but to our knowledge they are no available for Python and are more limited in terms of what properties can be verified.

Best

[Sumayya-rizwan]

With the knowledge of python and coq, user must know about the syntax of this tool also, as simulation should be written such that it should be aligned with the syntax of this tool....Isn't it?
Is there any other document/ explanation regarding writing simulation according to this tool because i am not able to understand it with the blog. I have used this tool and wants to verify the code translated by this tool....but i am having trouble

• in making test cases (like eval or compute) to check the simple functions working in my generated code
• in writing simulation
  and im hoping that if i can write simulation correctly then verification wont be challenging as said in blog that it would be just reflexivity. kindly correct me if am wrong in any understanding of this tool working.

[clarus]

With the knowledge of python and coq, user must know about the syntax of this tool also, as simulation should be written such that it should be aligned with the syntax of this tool....Isn't it?

Yes!

im hoping that if i can write simulation correctly then verification wont be challenging as said in blog that it would be just reflexivity. kindly correct me if am wrong in any understanding of this tool working.

Yes, that is the hope with this design, although we have not tested it yet except on very small examples.

Is there any other document/ explanation regarding writing simulation

No there are no other documents except these blog posts. We do not currently have the bandwidth to work more on coq-of-python. What would be your use case?

[Sumayya-rizwan]

meanwhile i was just exploring it verifying a simple counter example but i got stucked while writing simulation. I can write simulation in simple coq also. but verifying it with the coq file generated by this tool would be challenging then.......