3 ms·

You can axiomatize uniqueness of hashes in proof systems.

• ethbr0 5y ago
  This would require a hash input (or combination of inputs) to be unique over a limited / expected domain, right?
  • ncallaway 5y ago
    I mean, you could take anything as an axiom so there are no real requirements for it. I would imagine you would want to demonstrate the P(collision|domain+operating lifetime) << acceptable level or risk, and after you’d done that, take the uniqueness of hashes as a axiom for the proof system? That’s just speculation on my part, since I haven’t done much with formal proofs of working code
  • dnautics 5y ago
    No you just special case the function call and tell the proof analyzer "this never happens". Strictly speaking, a lie, but probably a sophisticated prover could even be rigged to keep track of those conditions (not in x years, e.g.) if you so chose