https://bugzilla.redhat.com/show_bug.cgi?id=2213270 Aleksei Bavshin <alebastr89@xxxxxxxxx> changed: What |Removed |Added ---------------------------------------------------------------------------- Status|ASSIGNED |POST Flags|fedora-review? |fedora-review+ --- Comment #5 from Aleksei Bavshin <alebastr89@xxxxxxxxx> --- fiat-crypto is an interesting thing. It's, of course, way over my head (I think we need someone like jjames to translate things to a regular English), but I've got a surface grasp of the papers referenced The team behind fiat-crypto implemented several things: 1. a formally verified implementation of a set of operations on mathematical primitives used in ECC (Montgomery curves, Solinas primes, etc...) in Coq (a functional language with formal proof capabilities, which is commonly used to implement said formally verified algorithms) 2. a tooling to rewrite the algorithm of choice in a selected language, specialized for a given set of constants. 3. a proof that the operation in 2 preserves the properties of an already verified algorithm. I'd say they did that by implementing things in Coq, again, but my language comprehension skills struggle with an intermediate level Haskell so I can't read their sources. Well, if we twist a point of view a bit, we can consider 1 a part of the tooling and not a source code that gets transformed into Rust. With that interpretation I'm going to agree and approve this. (I'm finding the part with regenerating the archive with `cargo package` curious, but I guess that creates some metadata required by cargo). --- Please, ensure that the clean archive can be regenerated from the dist-git or srpm before import. -- You are receiving this mail because: You are on the CC list for the bug. You are always notified about changes to this product and component https://bugzilla.redhat.com/show_bug.cgi?id=2213270 Report this comment as SPAM: https://bugzilla.redhat.com/enter_bug.cgi?product=Bugzilla&format=report-spam&short_desc=Report%20of%20Bug%202213270%23c5 _______________________________________________ package-review mailing list -- package-review@xxxxxxxxxxxxxxxxxxxxxxx To unsubscribe send an email to package-review-leave@xxxxxxxxxxxxxxxxxxxxxxx Fedora Code of Conduct: https://docs.fedoraproject.org/en-US/project/code-of-conduct/ List Guidelines: https://fedoraproject.org/wiki/Mailing_list_guidelines List Archives: https://lists.fedoraproject.org/archives/list/package-review@xxxxxxxxxxxxxxxxxxxxxxx Do not reply to spam, report it: https://pagure.io/fedora-infrastructure/new_issue
