Mirror of forum.nim-lang.org

9752 :: Formal verification in Nim using COQ and other proof assistants

• Mustapha (orginal) [2022-12-23T12:14:28+01:00] view original

  So I was looking for a language in which i could verify the logical properties of it's own code. And since Nim is a relatively easy language, I would love to use it, but I didn't know if this was possible to for example use Coq or some other proof assistant to do so, so I asked ChatGPT.

  So that ai told me that I could, but I'm not sure if it is telling the truth or not, because i've noticed it isn't 100% accurate so I'll paste the conversation I had with it, could you help explain to me if what it is saying is viable or not.

  here is some information ChatGPT gave me from the very leading questions i asked it.

  So could anyone tell me if you had the patience to read the following if chatgpt has the correct idea or was it off somewhere and by how much? thankyou very much.

  MUSTAPHA: how would i extract logical properties in Nim to prove in coq or other proof assistants?

  CHATGPT: To extract logical properties of a Nim program for analysis by Coq or other proof assistants, you can use Nim's support for contracts and specifications to define the expected behavior of your program.

  In Nim, you can use contracts to specify the preconditions, postconditions, and invariants of functions and procedures. Contracts are checked at runtime and can help ensure that your program is behaving as expected.

  For example, consider the following Nim function:

  Copy code

  proc add(x: int, y: int): int {.contract.} =

  let result = x + y return result

  To extract the logical properties of this function, you can specify contracts for the preconditions, postconditions, and invariants of the function. For example, you might specify that the function requires the x and y arguments to be non-negative integers, and that the result is equal to the sum of x and y.

  To extract the contracts from this function, you can use the --extract-contracts flag when compiling your Nim program. This will generate a separate file containing the contracts in a format that can be easily imported into Coq or other proof assistants.

  Once you have extracted the contracts from your Nim program, you can use the Coq proof language (Gallina) or the proof language of another proof assistant to define data types and functions that correspond to the data structures and operations in your Nim program,

  ME: so could i use contracts to specify the preconditions and postconditions such that there is no memory leak when disabling the gc and that there are no thread races and then extract the logical properties to coq and other proof assistants?

  CHATGPT: Yes, it is possible to use contracts in Nim to specify the preconditions and postconditions of a program that disables the garbage collector (GC) in order to ensure the absence of memory leaks and thread races. You can then extract the contracts from your Nim program and use them to construct formal proofs in Coq or other proof assistants.

  To do this, you can use contracts to specify the conditions under which the GC is disabled and the conditions that must be satisfied after the GC has been disabled. For example, you might specify that the GC must not be disabled if there are any live references to objects, and that all objects must be properly deallocated after the GC has been disabled.

  Here's an example of how you might specify these conditions in Nim using contracts:

  Copy code import gc

  proc disable_gc() {.contract.} =

  Preconditions

  Ensure that there are no live references to objects

  assert len(gc.liveObjects()) == 0

  Disable the GC

  Gc.set { (Gc.get()) with Gc.max_overhead = 0 }

  Postconditions

  Ensure that all objects have been deallocated

  assert len(gc.liveObjects()) == 0

  To extract the contracts from this function, you can use the --extract-contracts flag when compiling your Nim program. This will generate a separate file containing the contracts in a format that can be easily imported into Coq or other proof assistants.

  Once you have extracted the contracts from your Nim program, you can use the Coq proof language (Gallina) or the proof language of another proof assistant to define data types and functions that correspond to the data structures and operations in your Nim program, and use proof tactics to prove properties about these programs. This can be a powerful technique for ensuring the correctness and reliability of critical software.

  ME: and i could make a contract which says that a while loop is non decreasing?

  CHATGPT: Yes, it is possible to use contracts in Nim to specify the expected behavior of a while loop, including conditions such as non-decreasing behavior.

  To specify that a while loop is non-decreasing, you can use contracts to specify a loop invariant that expresses this property. A loop invariant is a logical predicate that must hold before and after each iteration of the loop.

  Here's an example of how you might specify a non-decreasing loop invariant in Nim using contracts:

  Copy code var i = 0

  while i < 10:

  Loop invariant: i is non-decreasing

  assert i >= 0

  Do something

  i += 1

  In this example, the loop invariant states that the value of i is non-decreasing, which means that it is either increasing or staying the same. This ensures that the loop will terminate after a finite number of iterations.

  To extract the contracts from this loop, you can use the --extract-contracts flag when compiling your Nim program. This will generate a separate file containing the contracts in a format that can be easily imported into Coq or other proof assistants.

  Once you have extracted the contracts from your Nim program, you can use the Coq proof language (Gallina) or the proof language of another proof assistant to define data types and functions that correspond to the data structures and operations in your Nim program, and use proof tactics to prove properties about these programs. This can be a powerful technique for ensuring the correctness and reliability of critical software.

  ME: and could i use contracts to require a certificate from say coq to compile in nim?

  CHATGPT:Yes, it is possible to use contracts in Nim to require a certificate from Coq or another proof assistant in order to compile a Nim program.

  To do this, you can use contracts to specify the conditions that must be satisfied in order for the program to be considered correct, and then use Coq or another proof assistant to prove that these conditions are satisfied.

  For example, consider the following Nim function:

  Copy code

  proc add(x: int, y: int): int {.contract.} =

  let result = x + y return result

  To require a certificate from Coq or another proof assistant in order to compile this function, you can specify contracts for the preconditions, postconditions, and invariants of the function. For example, you might specify that the function requires the x and y arguments to be non-negative integers, and that the result is equal to the sum of x and y.

  To extract the contracts from this function, you can use the --extract-contracts flag when compiling your Nim program. This will generate a separate file containing the contracts in a format that can be easily imported into Coq or other proof assistants.

  You can then use Coq or another proof assistant to prove that the conditions specified in the contracts are satisfied. Once the proof is complete, you can use the generated certificate to compile the Nim program. This can be a powerful technique for ensuring the correctness and reliability of critical software.

  ME: so could i use the certificate as a sort of a type in nim?

  CHATGPT: It is not possible to directly use a certificate from Coq or another proof assistant as a type in Nim. However, you can use contracts in Nim to specify the conditions that must be satisfied in order for a program to be considered correct, and then use Coq or another proof assistant to prove that these conditions are satisfied.

  For example, consider the following Nim function:

  Copy code

  proc add(x: int, y: int): int {.contract.} =

  let result = x + y return result

  To require a certificate from Coq or another proof assistant in order to compile this function, you can specify contracts for the preconditions, postconditions, and invariants of the function. For example, you might specify that the function requires the x and y arguments to be non-negative integers, and that the result is equal to the sum of x and y.

  To extract the contracts from this function, you can use the --extract-contracts flag when compiling your Nim program. This will generate a separate file containing the contracts in a format that can be easily imported into Coq or other proof assistants.

  You can then use Coq or another proof assistant to prove that the conditions specified in the contracts are satisfied. Once the proof is complete, you can use the generated certificate as evidence that the Nim program satisfies the specified conditions. This can be a powerful technique for ensuring the correctness and reliability of critical software.

  ME: i mean doesn't nim allow us to define types because of it's powerful metaprogramming capabilities

  CHATGPT: Yes, Nim does have powerful metaprogramming capabilities that allow you to define and manipulate types at runtime. This can be useful for a wide range of tasks, including defining custom data structures, generating code automatically, and implementing advanced type-level operations.

  To define a new type in Nim, you can use the type keyword to create a type alias or the struct keyword to create a struct type. You can then use these types like any other type in your Nim code.

  For example, consider the following Nim code, which defines a custom Point type:

  Copy code

  type

  Point* = object

  x*: float y*: float

  var p: Point p.x = 1.0 p.y = 2.0 You can also use Nim's metaprogramming facilities to define types that are generated at runtime based on other types or values. For example, you can use templates to define types that are parameterized by other types, or use eval to define types based on values computed at runtime.

  It's worth noting that Nim's metaprogramming capabilities can be quite complex to work with and may require a significant amount of expertise to use effectively. However, they can be a powerful tool for implementing advanced type-level operations and generating code automatically.

  ME: so i could potentially use this technique to create types for coq certificates.

  CHATGPT: Yes, it is possible to use Nim's metaprogramming capabilities to create types that represent Coq certificates or other proof artifacts.

  To do this, you can use Nim's type keyword to define a type alias that represents a Coq certificate, and then use Nim's metaprogramming facilities to manipulate this type and extract the necessary information from the certificate.

  For example, consider the following Nim code, which defines a CoqCertificate type and a function that extracts the proof obligations from a Coq certificate:

  Copy code

  type

  CoqCertificate* = object

  The proof obligations contained in the certificate

  obligations*: seq[string]

  proc extractObligations(cert: CoqCertificate): seq[string] =

  Extract the proof obligations from the certificate

  return cert.obligations

  You can then use this function to extract the proof obligations from a Coq certificate and use them to ensure the correctness of your Nim program.

  It's worth noting that this technique requires a significant amount of work and expertise, and may not be practical for all Nim programs. It's generally recommended to use testing and debugging techniques to ensure the correctness of Nim programs, rather than relying on formal verification. However, using Coq certificates to prove the correctness of Nim programs can be a powerful technique for ensuring the correctness and reliability of critical software.

---

• Araq (orginal) [2022-12-23T14:48:28+01:00] view original

  so I asked ChatGPT

  Er, ok. ChatGPT doesn't know what it's talking about.

---

• auxym (orginal) [2022-12-23T15:31:30+01:00] view original

  https://nim-lang.org/docs/drnim.html ?

---

• pietroppeter (orginal) [2022-12-23T17:13:59+01:00] view original

  ChatGPT is delightful and lots of fun (and might even be useful), but technically speaking is still a bullshit generator, in the sense that it has absolutely no concern about the truth. As a side effect, the cost of generating long texts that look reasonable are going down to zero (well at the moment is VC money keeping up the service for free), while the cost of making a insightful critique and pointing out mistakes are still very high (possibly higher in terms of chatgpt generated text, since there has been no self censoring editing to be friendly towards to a reader). The relevant part of your questions is:

  So I was looking for a language in which i could verify the logical properties of it's own code. And since Nim is a relatively easy language, I would love to use it, but I didn't know if this was possible to for example use Coq or some other proof assistant to do so

  This has been answered by @auxym (DrNim indeed provides that functionality; it seems to be very little used as far as I can see, but is where one would start working in the direction of proving code). The specific theorem prover it uses is z3 which is very nice in itself (z3nim examples). Another interesting project in that area is forematics by treeform.

  The rest of text consisting of chatgpt conversation I am not going to comment for reasons explained above. ;)

---

• Mustapha (orginal) [2022-12-23T17:24:04+01:00] view original

  i have a feeling when you have to modify a neural network to meet certain standards of what can or cannot be said, it might have unintended consequences elsewhere. for example it might not be "inclusive" according to chatgpt to say it cannot interact with coq so it tries really hard to make it seem in a way that it sounds convincing, but this is just me bullshitting lol.

---