How to distribute proofs with Rust code?

[W95Psp]

• Extrinsic proofs:
  • the assumption here is that in an extrinsic proof model, extractions always typechecks because the program is always wrapped into a monad of exception
  • separate files can provide lemma about extracted functions
• Intrinsic proofs: (the path we're currently taking with the F* backend)
  • programs are extracted as such, and type checking implies panic freedom (at least)
  • we thus sometimes need annotations:
    • pre/postcondition
    • strong types enforcing properties (see #431)
    • calls to lemmas
    • assertions
    • insert backend-specific code
    • modify backend-generated code
  • question: how do we store those proofs?

[ROMemories]

Is proof generation a deterministic/reproducible process? If so, maybe it would make sense to only store cryptographic hashes of the resulting proofs?

[github-actions[bot]]

This issue has been marked as stale due to a lack of activity for 60 days. If you believe this issue is still relevant, please provide an update or comment to keep it open. Otherwise, it will be closed in 7 days.

[W95Psp]

@ROMemories, I missed your comment here, sorry. We previously had hand-edited F* extractions, at some point. Thus, we needed to keep the generated code.

But now, we have many more ways of annotating Rust directly, and we no longer need (or want!) hand-edited code. So indeed, we don't actually need to store generated code. A locked version of Rust, its dependencies and of hax should always produce the same extraction, that's (or should be!) a deterministic process. Thus I don't think we even need a hash of the extraction.

I'm closing this issue: we are figuring out this progressively whenever we work on a new project, and I think we converge to putting all annotations in Rust. (wdyt @franziskuskiefer? feel free to reopen if you think this issue is valuable)

[ROMemories]

A locked version of Rust, its dependencies and of hax should always produce the same extraction, that's (or should be!) a deterministic process.

I think we converge to putting all annotations in Rust.

Awesome, thanks for the answer!