4 ms·

For a tool to be of "practical use, significance, or relevance" requires that the work it produces also is of "practical use, significance, or relevance". Block

For a tool to be of "practical use, significance, or relevance" requires that the work it produces also is of "practical use, significance, or relevance". Blockchains are not. And the best way to verify a compiled binary is correctly compiled is to do the compilation. That's a trivial amount of work. Constructing a ZKP of the same is certainly more cost intensive.

A1kmm 2y ago
> Constructing a ZKP of the same is certainly more cost intensive. That is certainly true for the compilation phase (i.e. constructing the ZKP). But for the verifier, that isn't so obviously true: - Firstly, the verifier might not even have access to the formal proof that the program meets the memory correctness guarantees. It might have access to a binary code, plus a proof that the binary code compiled from a completely memory safe language. The verifier would need zero knowledge of the code (which might be proprietary). - Secondly, proofs aren't necessarily that big (especially for Groth16 circuits), and can be applied recursively (you prove that you had a proof that something was true), and aren't that expensive to verify. If verifying a program once when you download it means it can be flagged as being safe to run without expensive bounds and MMU checks, it could open up new types of more performant CPUs, and potentially save far more than it costs to verify.
sabas123 2y ago
> And the best way to verify a compiled binary is correctly compiled is to do the compilation. That's a trivial amount of work. Constructing a ZKP of the same is certainly more cost intensive. This makes the assumption that you both have the source code and that the compiler is deterministic. With the latter one being not the case for (most?) modern compilers.
- dumbo-octopus 2y ago
  Ah yes, the totally-valid use case of ensuring that a third party has properly compiled source code that you don't have access to. I'm sure this comes up in industry all the time.
  - Ar-Curunir 2y ago
    I mean, do you ever run any closed-source software?
    - dumbo-octopus 2y ago
      Can you provide an example of a ZKP of memory safety of a compiled output that would be less computationally expensive than static analysis of the binary?
- OJFord 2y ago
  It doesn't assume the compiler is deterministic, because you don't need to use the result for verification, you can just use the result.
Ar-Curunir 2y ago
You can’t just recompile a binary in many scenarios. Eg: when the source code is proprietary, or when there are time constraints.

A1kmm 2y ago

> Constructing a ZKP of the same is certainly more cost intensive. That is certainly true for the compilation phase (i.e. constructing the ZKP). But for the verifier, that isn't so obviously true: - Firstly, the verifier might not even have access to the formal proof that the program meets the memory correctness guarantees. It might have access to a binary code, plus a proof that the binary code compiled from a completely memory safe language. The verifier would need zero knowledge of the code (which might be proprietary). - Secondly, proofs aren't necessarily that big (especially for Groth16 circuits), and can be applied recursively (you prove that you had a proof that something was true), and aren't that expensive to verify. If verifying a program once when you download it means it can be flagged as being safe to run without expensive bounds and MMU checks, it could open up new types of more performant CPUs, and potentially save far more than it costs to verify.

sabas123 2y ago

> And the best way to verify a compiled binary is correctly compiled is to do the compilation. That's a trivial amount of work. Constructing a ZKP of the same is certainly more cost intensive. This makes the assumption that you both have the source code and that the compiler is deterministic. With the latter one being not the case for (most?) modern compilers.

dumbo-octopus 2y ago
Ah yes, the totally-valid use case of ensuring that a third party has properly compiled source code that you don't have access to. I'm sure this comes up in industry all the time.
- Ar-Curunir 2y ago
  I mean, do you ever run any closed-source software?
  - dumbo-octopus 2y ago
    Can you provide an example of a ZKP of memory safety of a compiled output that would be less computationally expensive than static analysis of the binary?
OJFord 2y ago
It doesn't assume the compiler is deterministic, because you don't need to use the result for verification, you can just use the result.

Ar-Curunir 2y ago

You can’t just recompile a binary in many scenarios. Eg: when the source code is proprietary, or when there are time constraints.